【MoL】24 Prenexity and Purity

• お、schema のことを formula とも呼ぶんだな。
  
• prenex form : monadic quantificational schemata の形態。すべての quantifiers が先頭に来ているもの。
  
• pure form : monadic quantificational schemata の形態。quantifiers について、それぞれの a quantifier のスコープの中には、the quantifier がもつ the variable について free occurrences を含むもののみを含むようにしたもの。
  
  
• このような form の変形に、the rules of passage を使う。
  例： a prenex form へ変換。
  p <-> ∀x[Fx -> ∃y(Fy . Gx)].
  p -> ∀x[Fx -> ∃y(Fy . Gx)] . ∀x[Fx -> ∃y(Fy . Gx)] -> p. [paraphrasing a biconditional]
  p -> ∀x[Fx -> ∃y(Fy . Gx)] . ∀z[Fz -> ∃w(Fw . Gz)] -> p. [reletting]
  ∀x[ p ->. Fx -> ∃y(Fy . Gx)] . ∃z[Fz -> ∃w(Fw . Gz) .-> p]. [the rules of passage]
  ∀x∃z[ p ->. Fx -> ∃y(Fy . Gx) : Fz -> ∃w(Fw . Gz) .-> p]. [the rules of passage]
  ∀x∃z[ p -> ∃y(Fx ->. Fy . Gx) . ∃w(Fz ->. Fw . Gz) .-> p]. [the rules of passage]
  ∀x∃z[ ∃y(p ->: Fx ->. Fy . Gx) . ∀w(Fz ->. Fw . Gz :-> p)]. [the rules of passage]
  ∀x∃z∃y∀w(p ->: Fx ->. Fy . Gx :. Fz ->. Fw . Gz :-> p). [the rules of passage]
  
  例：a pure form への変換。
  ∃x(Fx . p .∨. Fx . Gx).
  ∃x(Fx . p) ∨ ∃x(Fx . Gx). [distributiveness]
  ∃xFx . p . ∨ ∃x(Fx . Gx). [the rules of passage]
  
  例：a pure form への変換。
  ∀x[∃y(Fx <-> Gy) ∨ ∃yFy] . ∀x(Fx ∨ Gx).
  ∀x∃y(Fx <-> Gy) ∨ ∃yFy . ∀x(Fx ∨ Gx). [the rules of passage]
  ∀x[∃y(Fx . Gy)∨∃y(-Fx . -Gy)] ∨ ∃yFy . ∀x(Fx ∨ Gx). [paraphrasing a biconditional]
  ∀x[Fx . ∃yGy .∨.-Fx .∃y -Gy] ∨ ∃yFy . ∀x(Fx ∨ Gx). [the rules of passage]
  ※[]の中を conjunction normal formに変形
  Fx . ∃yGy .∨.-Fx . ∃y -Gy
  (Fx . ∃yGy) ∨ (-Fx . ∃y -Gy)
  (Fx . ∃yGy) ∨ (-Fx . ∃y -Gy)
  (Fx ∨ (-Fx . ∃y-Gy)) . (∃yGy ∨ (-Fx . ∃y-Gy))
  [(Fx ∨ -Fx) . (Fx ∨ ∃y-Gy)] . [(∃yGy ∨ -Fx) . (∃yGy ∨ ∃y-Gy)]
  Fx ∨ ∃y-Gy . ∃yGy ∨ -Fx . ∃yGy ∨ ∃y-Gy
  ∀x[Fx ∨ ∃y-Gy . ∃yGy ∨ -Fx . ∃yGy ∨ ∃y-Gy] ∨ ∃yFy . ∀x(Fx ∨ Gx).
  ∀x(Fx ∨ ∃y-Gy) . ∀x(∃yGy ∨ -Fx) . ∃yGy ∨ ∃y-Gy .∨ ∃yFy : ∀x(Fx ∨ Gx). [the rules of passage and distributiveness]
  ∀xFx ∨ ∃y-Gy . ∃yGy ∨ ∀x-Fx . ∃yGy ∨ ∃y-Gy .∨ ∃yFy : ∀x(Fx ∨ Gx). [the rules of passage]
  
  
• a monadic quantificational schema は、stacked quantifiers がある限り、impurities を持つ。
  
• monadic schemata が closed であるならば、pure にできる。open だとできるとは限らない。
  
  
• これらの話は、monadic な限り必須ではない。これは、'Fxy'といった polyadic schemata を導入するための準備である。
  

こつこつ。