F(t) => exists x F(x)
から
forall x F(x) => F(t)
を導く。
(1) F(t) => exists x F(x)
(2) ^ exists x F(x) => ^F(t) : [対偶{(1)}]
(3) ^ exists x F(x) => forall x ^F(x) : [I2{(2)}]
(4) ^ exists x ^F(x) => forall x ^^F(x) : [(3){F -> ^F}]
(5) ^ exists x ^F(x) => forall x F(x) : [二重否定除去]
(6) ^F(t) => exists x ^F(x) : [述語公理3{F -> ^F]
(7) ^ exists x ^F(x) => ^^F(t) : [対偶{(6)}]
(8) ^ exists x ^F(x) => F(t) : [二重否定除去]
(9) forall x F(x) => F(t) : [(5)](A => B) => ((exists x A) => B) から (B => A) => (B => (forall x A)) を導く。 (1) (^A => ^B) => ((exists x ^A) => ^B) : [述語公理4] (2) (B => A) => (B => (^ exists x ^A)) : [対偶] (3) (B => A) => (B => (forall x A)) : [上記(5)より]
結構省略気味ですが、合ってるかな。ちょっとあやしいなぁ。
これ、方針としては簡単かもしれないけど、
対偶とか、公理の一部に別の公理を適用するところまで証明したら相当な規模になる気がするよ。
「容易に示せる」って本文で言うからには、もっと簡単な証明があるんじゃないか。
それにしても、形式的証明は「分かったから解けた」というより
「神様の気まぐれにより答えを授かった」感じ。
理解とは無縁のパズルな気がする。
「数学基礎論入門」(前原 昭二著)を参考にしました。
