つまり「この文が正しいならば証明できない」をカリー命題の一種として承認できるとする。
するとC「Cは証明できない」と同値だから、C=Gとなってゲーデル命題はカリー命題の一種だと出るのであった。そりゃ否定できないわけだが、その否定されないわけをこそ明らかにしなければならないのであるから、次へ行く。なぜならば「そのカリー命題が数論の数学命題として存在するから」とやられたら振出しに戻るからである。
ゲーデル命題はカリー命題の特殊な姿であるとして、カリー命題もまた述語文に主語の名前を付けたクォーク命題の仲間である。
Qua.X(X)=X⇔X is A. クォーク命題
¬Qua.X(X)=X⇔X is not A. 否定クォーク命題
¬Qua.¬X(X)=¬X⇔X is not A. 反クォーク命題
¬Qua.¬X(¬X)=¬X⇔¬X is not A. 反対クォーク命題
カリー命題は否定形のつもりで反クォーク命題を造ったとしても否定されずに中間子文を形成してしまう文型であることが分かった。
意味論的にはカリー命題「この文が正しいならばA」を否定するには「その文が正しいならば¬A」を持ってこなくてはならず、そうした定式はこの系列にはなくて不可能である、すなわち「Aだ」と言っている人間に「¬Aだ」という言葉をぶつけても相互に矛盾するだけで否定することが出来ないのと事情は同じであるしかない。
ゲーデル命題と同値な内容を丁寧に述べたら「この命題が正しいならばこの命題は証明できない」であろう。さらにこのことは不完全性定理というよりはゲーデル命題の定義より明らかなのだが、結局のところ数学体系の無矛盾性とは同義反復の証明にほかならず、そして数学では同義反復は証明ではなく悪循環だから避けるということ以外の何事でもなかろう。
問題はそれがどうして全数学の無矛盾性にかかわる大事件だったのか、という話である。
数学体系の無矛盾性とは公理から導かれる命題に相互矛盾がないこと、すなわち公理が背理法によって覆さないことではなかったのか、クルト・ゲーデルの論証はそのような具体的な検討にはまったく無用の長物だったのであった。
数学と論理学の勝負はたった今、始まったばかりだと思われてならない。
するとC「Cは証明できない」と同値だから、C=Gとなってゲーデル命題はカリー命題の一種だと出るのであった。そりゃ否定できないわけだが、その否定されないわけをこそ明らかにしなければならないのであるから、次へ行く。なぜならば「そのカリー命題が数論の数学命題として存在するから」とやられたら振出しに戻るからである。
ゲーデル命題はカリー命題の特殊な姿であるとして、カリー命題もまた述語文に主語の名前を付けたクォーク命題の仲間である。
Qua.X(X)=X⇔X is A. クォーク命題
¬Qua.X(X)=X⇔X is not A. 否定クォーク命題
¬Qua.¬X(X)=¬X⇔X is not A. 反クォーク命題
¬Qua.¬X(¬X)=¬X⇔¬X is not A. 反対クォーク命題
カリー命題は否定形のつもりで反クォーク命題を造ったとしても否定されずに中間子文を形成してしまう文型であることが分かった。
意味論的にはカリー命題「この文が正しいならばA」を否定するには「その文が正しいならば¬A」を持ってこなくてはならず、そうした定式はこの系列にはなくて不可能である、すなわち「Aだ」と言っている人間に「¬Aだ」という言葉をぶつけても相互に矛盾するだけで否定することが出来ないのと事情は同じであるしかない。
ゲーデル命題と同値な内容を丁寧に述べたら「この命題が正しいならばこの命題は証明できない」であろう。さらにこのことは不完全性定理というよりはゲーデル命題の定義より明らかなのだが、結局のところ数学体系の無矛盾性とは同義反復の証明にほかならず、そして数学では同義反復は証明ではなく悪循環だから避けるということ以外の何事でもなかろう。
問題はそれがどうして全数学の無矛盾性にかかわる大事件だったのか、という話である。
数学体系の無矛盾性とは公理から導かれる命題に相互矛盾がないこと、すなわち公理が背理法によって覆さないことではなかったのか、クルト・ゲーデルの論証はそのような具体的な検討にはまったく無用の長物だったのであった。
数学と論理学の勝負はたった今、始まったばかりだと思われてならない。
でも、数学で問題なのは相互矛盾であって個々の矛盾性ではない・・、ゲーデル敗れたり・・w)