「ゲーデル 不完全性発見への旅」の排中律の証明(途中)

P50に

|- E \/ ^E

を示せ、という演習問題がある。

公理系は以下の通り。

[公理1] A => (B => A)
[公理2] (A => B) => ((A => (B => C)) => (A => C))
[公理3] A => ((A => B) => B)
[公理4] A => (B => (A /\ B))
[公理5] (A /\ B) => A
[公理6] (A /\ B) => B
[公理7] A => (A \/ B)
[公理8] B => (A \/ B)
[公理9] (A => C) => ((B => C) => ((A \/ B) => C))
[公理10] (A => B) => ((A => ^B) => ^A)
[公理11] ^^A => A

目標となる証明はこれ。

* (E \/ ^E) ; [排中律]
(1) (E => E) ; [同一律]
(2) (A => B) => (^A \/ B) ; [含意から連言への変換]
(3) (E => E) => (^E \/ E) ; [(2){A -> E, B -> E}]
(4) (^E \/ E) ; [mp{(1),(3)}]
(5) (A \/ B) = (B \/ A) ; [連言交換律]
(6) (^E \/ E) => (E \/ ^E) ; [(5){A -> ^E, B -> E}]
(7) (E \/ ^E) ; [mp{(4),(6)}]

なので、元の公理系から、同一律、含意から連言への変換、連言交換律の3つが証明できれば、排中律は証明可能となる。

この証明をお手軽に扱う上では、演繹定理が非常に便利。

  • メタ定理
    • 演繹定理
    • 逆演繹定理
      • Γを論理式の集合，φとψを論理式とするとき， Γ|-φ⇒ψ ならば Γ∪{φ}|-ψ である．
    • 健全性定理
      • 任意の論理式φに対して，|-φ ならば |=φである．
    • 完全性定理
      • 任意の論理式φに対して，|=φ ならば |-φである．

まだ「含意から連弦への変換」までたどり着いていないが、一通り整理しておく。

* A |- (B => A) ; [仮定付前件付加]
(1) A => (B => A) ; [公理1{A -> A, B -> B}]
(2) A ; [仮定1]
(3) (B => A) ; [mp{(2),(1)]

* A => A ; [同一律]
(1) (A => (A => A)) => ((A => ((A => A) => A)) => (A => A)) ; [公理2{A -> A, B -> (A => A), C -> A}]
(2) (A => (A => A)) ; [公理1{A -> A, B -> A}]
(3) (A => ((A => A) => A)) => (A => A) ; [mp{(2),(1)}]
(4) A => ((A => A) => A) ; [公理4{A -> A, B -> A}]
(5) A => A ; [mp{(4),(3)}]

* (A \/ B) => (B \/ A) ; [連言交換律]
(1) (B => (B \/ A)) => ((A => (B \/ A)) => ((A \/ B) => (B \/ A))) ; [公理9{A -> B, B -> A, C -> (B \/ A)}]
(2) B => (B \/ A) ; [公理7{A -> B, A -> A}]
(3) (A => (B \/ A)) => ((A \/ B) => (B \/ A)) ; [mp{(2),(1)]
(4) A => (B \/ A) ; [公理8{A -> B, B -> A}]
(5) (A \/ B) => (B \/ A) ; [mp{(4),(3)}]

* A => B, B => C |- (A => C) ; [三段論法]
(1) (A => B) => ((A => (B => C)) => (A => C)) ; [公理2{A -> A, B -> B, C -> C}]
(2) A => B ; [仮定1]
(3) (A => (B => C)) => (A => C) ; [mp{(2),(1)}]
(4) B => C ; [仮定2]
(5) A => (B => C) ; [仮定付前件追加{A -> (B => C), B -> A}]
(6) A => C ; [mp{(5),(3)}]

* (A => B) |- (B => C) => (A => C) ; [仮定付後件前件後件付加]
(1) (A => B) => ((A => (B => C)) => (A => C)) ; [公理2{A -> A, B -> B, C -> C}]
(2) A => B ; [仮定1]
(3) (A => (B => C)) => (A => C) ; [mp{(2),(1)}]
(4) (B => C) => (A => (B => C)) [公理1{A -> (B => C), B -> A}]
(5) (B => C) => (A => C) [三段論法{(A => B) -> (4),(B => C) -> (3)}]

* (B => C) |- (A => B) => (A => C) ; [仮定付前件後件前件付加]
(1) ((A => B) => (A => (B => C))) => (((A => B) => ((A => (B => C)) => (A => C))) => ((A => B) => (A => C))) ; [公理2{A -> (A => B), B -> (A => (B => C)), C -> (A => C)}]
(2) A => (B => C) ; [仮定付前件付加{A -> (B => C), B -> A]
(3) (A => B) => (A => (B => C)) ; [仮定付前件付加{A -> (2), B -> (A => B)}]
(4) ((A => B) => ((A => (B => C)) => (A => C))) => ((A => B) => (A => C)) ; [mp{(3),(1)}]
(5) (A => B) => (A => C) ; [mp{公理2,(4)}]

* A, (^B => ^A) |- B ; [仮定付対偶律]
(1) (^B => A) => ((^B => ^A) => ^^B) ; [公理10{A -> ^B, B -> A}]
(2) A [仮定1]
(3) ^B => A ; [仮定付前件付加{A -> A, B -> ^B}]
(4) (^B => ^A) => ^^B ; [mp{(3),(1)}]
(5) ^B => ^A ; [仮定2]
(6) ^^B ; [mp{(5),(4)}]
(7) B ; [公理11{A -> B}]

* (^B => ^A) => (A => B) ; [対偶律]
(1) (^B => ^A) |- (A => B) ; [演繹定理{仮定付対偶律}]
(2) (^B => ^A) => (A => B) ; [演繹定理{(1)}]

* A => ^^A ; [二重否定付加]
(1) ^^^A => ^A ; [公理11{A -> ^A}]
(2) (^^^A => ^A) => (A => ^^A) ; [対偶律{A -> A, B -> ^^A}]
(3) (A => ^^A) ; [mp{(1),(2)}]


対偶をわざと出してなかったり、公理2が一般に紹介されるヒルベルト系と違ってたりするのはなぜなんだろう。演繹定理を使わずに対偶律を証明したい。

参考情報。これがなかったらできなかった。多謝。
http://www.at-akada.org/blog/2008/12/post-277.html