「ゲーデル 不完全性発見への道」P66にて、
「述語論理の公理1,4および2,3は同値であること」を示すのは演習問題になっている。
たとえば、2,3が同値であることを示せ、っていうのはこれでいいはず。
とおもったけど、これだと述語公理2,3を使ってしまっているのでダメそうだ。
これができると任意の2つの公理が等しいことになってしまう。
同値であることを示すので、同値であることを否定した仮定をおくと
矛盾が導けることを示せばよい。
つまり
|- ^((P => Q) and (Q => P))
において、
P -> (forall x F(x) => F(t)) : [述語公理2]
Q -> (F(t) => exists x F(x)) : [述語公理3]
として、矛盾(Eと^E)を導けばよい。
(1) (Q => (P => Q)) : [公理1]
(2) P => Q : [mp{(1),述語公理3}]
(3) (P => (Q => P)) : [公理1]
(4) Q => P : [mp{(3),述語公理2}]
(5) ((P => Q) => ((Q => P) => ((P => Q) and (Q => P)))) : [公理4]
(6) ((P => Q) and (Q => P)) : [mp{(2),(4),(5)}]
(7) ((P => Q) and (Q => P)) => (E => ((P => Q) and (Q => P))) : [公理1]
(8) (E => ((P => Q) and (Q => P))) : [mp{(6),(7)}]
(9) ^((P => Q) and (Q => P)) => (E => ^((P => Q) and (Q => P))) : [公理1]
(10) (E => ^((P => Q) and (Q => P))) : [mp{仮定,(9)}]
(11) ((E => ((P => Q) and (Q => P))) => ((E => ^((P => Q) and (Q => P))) => ^E)): [公理10]
(12) ^E : [mp{(8),(10),(11)}]
(13) ((P => Q) and (Q => P)) => (^E => ((P => Q) and (Q => P))) : [公理1]
(14) (^E => ((P => Q) and (Q => P))) : [mp{(6),(13)}]
(15) ^((P => Q) and (Q => P)) => (^E => ^((P => Q) and (Q => P))) : [公理1]
(16) (^E => ^((P => Q) and (Q => P))) : [mp{仮定,(15)}]
(17) ((^E => ((P => Q) and (Q => P))) => ((^E => ^((P => Q) and (Q => P))) => ^^E)): [公理10]
(18) ^^E : [mp{(14),(16),(17)}]
(19) ^^E => E : [公理11]
(20) E : [mp{(18),(19)}]
(12)において^E、(20)においてEとなっており矛盾。
原因は、仮定
^((P => Q) and (Q => P))
を追加したことにある。
よって、
((P => Q) and (Q => P))
つまり、
((forall x F(x) => F(t)) => (F(t) => exists x F(x))) and ((F(t) => exists x F(x)) => (forall x F(x) => F(t)))
が定理である。背理法が使える、ということであれば、何でもこれでいけるのではないか。
