命題論理の自然演繹

アルファベットは {¬,⋀,p1,p2,...}と括弧。p,q,r,...は任意の原子命題を指示、α,β,...は任意の式を指示、X,Y,Z,...は任意の式の集合を指示。他の論理記号は定義: ⊥:=p1⋀¬p1, ⊤:=¬⊥, α⋁β:=¬(¬α⋀¬β), α→β:=¬(α⋀¬β), α↔β:=(α→β)⋀(β→α)。メタでの and,or,if,iff を &&,||,⇒,⇔と表記。(X,α)なるシーケントが導出できるとき X⊢αと記述。X⊢α,βは X⊢α && X⊢βの略記であり、X⊢Yも同様。⊢αは{}⊢αの略記。仮定は Hy と略記。

基本則は (IS)(MR)(EFQ)(CASE)(⋀I)(⋀E):

(IS) 前提なしに α⊢α  ; (MR) X⊢α ⇒ X'⊢α where X ⊆ X';
(EFQ) X⊢α,¬α ⇒ X⊢β ; (CASE) X,α⊢β && X,¬α⊢β ⇒ X⊢β
(⋀I) X⊢α,β ⇒ X⊢α⋀β; (⋀E) X⊢α⋀β ⇒ X⊢α,β

最重要な派生規則:

(¬E) X,¬α⊢α ⇒ X⊢α 類似規則は X,α⊢¬α ⇒ X⊢¬α
(RAA) X,¬α⊢β,¬β ⇒ X⊢α 類似規則は X,α⊢β,¬β ⇒ X⊢¬α
(DT) X⊢α→β ⇔ X,α ⊢β
(CUT) X⊢α && X,α⊢β ⇒ X⊢β; 類似規則は X,α⊢β && Y⊢α ⇒ X∪Y ⊢ β

派生規則の証明:

• (¬E-1):(IS,MR)で X,α⊢α。これと Hyで(CASE)。
• (¬E-2):(IS,MR)で X,¬α⊢¬α。これと Hyで(CASE)。
• (RAA-1):Hy,(EFQ)より X,¬α⊢α。(¬E)。
• (RAA-2):Hy,(EFQ)より X,α⊢¬α。(¬E)。
• (DT⇒):(IS,MR,⋀I)より X,α,¬β⊢α⋀¬β。Hy,(MR)より X,α,¬β⊢¬(α⋀¬β)。(EFQ)より X,α,¬β⊢β。(¬E)。
• (CUT-1):(IS,MR)よりX,¬α⊢¬α。Hy,(MR)より X,¬α⊢α。(EFQ)でX,¬α⊢β。これとHyで(CASE)。
• (CUT-2): Hy,(MR)より X∪Y,α⊢β。Hy,(MR)より X∪Y⊢α。(CUT-1)。
• (DT⇐):(IS,MR)よりX,α⋀¬β⊢α。これと Hy,で(CUT)するとX,α⋀¬β⊢β。(⋀2)より X,α⋀¬β⊢¬β。よって(EFQ)よりX,α⋀¬β⊢α→β。一方(IS,MR),→の定義より X,¬(α⋀¬β)⊢α→β。(CASE)。

二重否定に関する諸性質(DN):

• α≈¬¬α
  • α⊢¬¬α: (IS,MR)よりα,¬α⊢α,¬α。(EFQ)で α,¬α⊢¬¬α。(¬E)。
  • ¬¬α⊢α: (IS,MR)より¬α,¬¬α⊢¬α,¬¬α。(EFQ)で¬α,¬¬α⊢α。(¬E)。
• X⊢α ⇔ X⊢¬¬α: 証明済みな α⊢¬¬α or ¬¬α⊢α と Hyで(CUT)。
• X,α⊢β ⇔ X,¬¬α⊢β: 証明済みな ¬¬α⊢α or α⊢¬¬α と Hyで(CUT)。

⋀の諸性質:

• α,β ≈ α⋀β ≈ β⋀α: α,β⊢α,βに(⋀1)。α⋀β⊢α⋀βに(⋀2)。よって α,β≈α⋀β。左辺は集合なので同様に α,β≈β⋀α。
• ⊢⊤,⊢¬⊥: 一つ上より、p1⋀¬p1 ⊢ p1,¬p1。(RAA) より ⊢¬(p1⋀¬p1)
• ¬(α⋀β)≈α→¬β:¬(α→¬β)=¬¬(α⋀¬¬β)≈α,β≈α⋀β。よって ¬(α⋀β),¬(α→¬β)⊢⊥。(RAA)。
• α,β⊢α→β: α,β⊢αより(DT)を利用。
• ¬p⊢p→q: ¬(p→q)=¬¬(p⋀¬q)⊢p,¬q より、¬p,¬(p→q)⊢p,¬p。(RAA)。
• p,q⊢p→q: p,q⊢qに(DT)と(MR)。

ドモルガン:

• ¬(α⋁β)≈¬α,¬β: ¬(α⋁β)=¬¬(¬α⋀¬β)≈¬α⋀¬β≈¬α,¬β
• ¬(α⋀β)≈¬α⋁¬β: ¬(¬α⋁¬β)=¬¬(¬¬α⋀¬¬β)≈¬¬α,¬¬β≈α,β≈α⋀βよって¬(α⋀β),¬α⋁¬β⊢⊥より(RAA)。逆:(RAA)と(DN)。

対偶と三段論法:

• p→q≈¬q→¬p: ¬(¬q→¬p)≈¬¬(¬q⋀¬¬p)≈¬q,p≈p⋀¬q≈¬¬(p⋀¬q)≈¬(p→q)より p→q,¬(¬q→¬p)⊢⊥より(RAA)。逆:(RAA)にDN除去。
• p⊢q⇔¬q⊢¬p: Hy,(IS,MR)で p,¬q⊢q,¬q。(RAA')より ¬q⊢¬p。逆に ¬q,¬¬p⊢¬p,¬¬p。(RAA)より¬¬p⊢q。よってp⊢q
• X⊢p→q⇔X⊢¬q→¬p: 証明済みの式 p→q⊢¬q→¬p or ¬q→¬p⊢p→q に(CUT)。
• p,p→q⊢q: (IS)より p→q⊢p→q。(DT)。
• X⊢p,p→q⇒X⊢q: Hy,(DT)よりX,p⊢q。これともう一つのHyで(CUT)
• ¬q,p→q⊢¬p: 証明済みの p→q⊢¬q→¬p。(DT)。

含意の定理式

• ⊢p→p: (IS)より p⊢p。(DT)。
• ⊢p→q→p: (IS)(MR)より p,q⊢p。(DT)。
• ⊢(p→q)→(q→r)→(p→r): (MP)より、p,p→q⊢q, q,q→r⊢r。(CUT)より p,p→q,q→r⊢r。(DT)。
• ⊢(p→q→r)→(q→p→r): MPを2回使って p,q,p→q→r⊢q,q→r⊢r。これに(DT)を2回。
• ⊢((p→q)→p)→p: DTより(p→q)→p⊢p,さらに対偶より¬p⊢¬((p→q)→p)に同値変形できる。証明済みの¬p⊢p→qと(IS)より ¬p⊢p→q,¬p⊢(p→q)⋀¬p⊢¬¬((p→q)⋀¬p)=¬((p→q)→p)。

⋁関連: ⋁は定義される

• α⊢α⋁β: (IS)(MR)(⋀2)より α,¬α⋀¬β⊢α,¬α (RAA')より α⊢¬(¬α⋀¬β)=α⋁β。
• α⋁β≈β⋁α: ¬(β⋁α)=¬¬(¬α⋀¬β)⊢¬α,¬β⊢¬β⋀¬α=¬(α⋁β)より α⋁β,¬(β⋀α)⊢⊥。RAA。
• α⋁β≈¬α→β: 定義より α⋁β=¬(¬α⋀¬β), ¬α→β=¬(¬α⋀¬β)。
• α⋁β≈¬¬α⋁β: ¬(¬¬α⋁β)=¬¬(¬¬¬α⋀¬β)≈¬¬¬α⋀¬β⊢¬¬¬α,¬β≈¬α,¬β⊢¬(α⋁β)より、α⋁β,¬(¬¬α⋁β)⊢⊥`。RAA。
• X⊢α⋁β⇔X⊢¬¬α⋁β: 証明済みの α⋁β⊢¬¬α⋁βにHyをCUT。
• X⊢α⇒X⊢α⋁β: 証明済みの α⊢α⋁β に対し Hy,(CUT)を利用。
• X,α⊢γ&&X,β⊢γ⇒X,α⋁β⊢γ: (DT),仮定よりX⊢α→γ,X⊢β→γ。証明済みの α⋁β,α→γ,β→γ⊢γに(CUT)。

α→γ, β→γ, α⋁β ⊢ γ ¬(α⋀¬γ),¬(β⋀¬γ), α⋁β ⊢ γ ¬((α⋀¬γ)⋁(β⋀¬γ)),α⋁β ⊢ γ ¬((α⋁β)⋀¬γ),α⋁β⊢γ

α,¬(α⋀β) ⊢ ¬β α,α→¬β ⊢ ¬β

(α⋀β)→γ ⊢ (α→γ),(β→γ) ¬(α⋀β⋀¬γ)

¬((α⋀β)→γ)≈α,β,¬γ⊢α⋀¬γ,β⋀¬γ≈¬(α→γ),¬(β→γ)

(p⋁q)⋀r ⊢ p⋀r ⋁ q⋀r (p⋁q)⋀r ⊢ ¬(p⋀r) → q⋀r p⋁q,r,¬(p⋀r) ⊢ q,r ¬p→q,r,¬(p⋀r) ⊢ q ¬p→q,r,¬(p⋀r) ⊢ r -> OK