メモ：カリーのパラドックス

普通のC++使い、銀天すばる @SubaruG

古典論理的に考えれば，ある命題の真偽は，公理系と命題が well-defined なら，真か偽かのどちらかに定まる（無矛盾律と排中律）か，もしくは「そんな命題は構成できない」という結論が得られるはず．（完全性と無矛盾性を同時に満たした公理系は存在しないらしいので云々）

普通のC++使い、銀天すばる @SubaruG

あくまで古典論理の話． あと，数学の設問に関して言うなら，「～を満たすものを一つ挙げよ」という問題も考えうるので，少なくともそういう設問に関しては，正解は一つじゃない．

くるる @kururu_goedel

@SubaruG ちょっと誤解が見られるような。モデルを決まれば命題の真偽は定まりますが、公理系だけからは真偽が決定できない命題はいくらでもあり得ます。というか、十分強い公理系では常に存在する、というのが不完全性定理。この命題はwell-definedです。

普通のC++使い、銀天すばる @SubaruG

@kururu_goedel 「真偽が決定できない」ことを表して「そんな命題は構成できない」と記述したつもりです． 典型例はカリーのパラドックス辺りですね．

普通のC++使い、銀天すばる @SubaruG

@kururu_goedel 「全ての命題は真か偽かを確定できるか，確定できないかのいずれかである」という命題自体が「真か偽かを確定できない命題」である（記憶が正しければ）辺り，結構いい加減ですけど．

普通のC++使い、銀天すばる @SubaruG

@kururu_goedel 少なくとも，排中律と無矛盾律を持った論理体系では，全ての命題は真偽のいずれかになるので（それが排中律と無矛盾律の意味する所），真偽のいずれにも定まらない命題は，そもそも命題ではない，とするのが自然だという認識です．

普通のC++使い、銀天すばる @SubaruG

「この文が真ならば，カリーのパラドックスは起こらない」

@ta_shim_at_nhn

@SubaruG その論では、群の公理系において、∀x,y (xy=yx) は命題ではないということになりますが。真の概念と恒真の概念との混同があるように見えます。

普通のC++使い、銀天すばる @SubaruG

@ta_shim_at_nhn ふむ． では，排中律および無矛盾律から得られる ∀x ( x xor ￢x ) は，どのように解釈するべきなのでしょう？ 真偽が決定できない命題を命題として認めると，排中律が成り立たなくなると思うのですが，それは僕の理解が浅いからでしょうか．

@ta_shim_at_nhn

@SubaruG x と ¬x のうち一方だけが真ということです。 それを、x と ¬x のうち一方だけが恒真と読んでしまうのが間違いです。

普通のC++使い、銀天すばる @SubaruG

@ta_shim_at_nhn いや，別に恒真だとは一言も言ってないですが…． 僕が件の post で言及しているのは，嘘つきのパラドクスやカリーのパラドクスのような，そもそも真偽が確定できない命題についてなのですが．

普通のC++使い、銀天すばる @SubaruG

@ta_shim_at_nhn 「この命題は偽である」のような矛盾した命題（のようなもの）は，別に量化子とか使ってないですよね．

@ta_shim_at_nhn

@SubaruG なるほど、読み返してみて、こちらがどこを恒真と読んいたのかわかりました。

普通のC++使い、銀天すばる @SubaruG

@ta_shim_at_nhn すみません，今になって分かりました． 要するに， p : ￢q q : ￢p のような命題 p, q があった時，この命題対は無矛盾律も排中律も満たしますが，どちらが真でどちらが偽かは原理的に判別不能ですね．

くるる @kururu_goedel

@SubaruG 例えばZFCからは連続体仮説は真とも偽とも証明できない、ということはいいですか？だからといって、連続体仮説が命題でないというわけではありません。また、「連続体仮説は真であるかまたは偽である」ならば証明できます。言いたかったのはそういうことだけです。