-
- いいね！0
ぼんてんぴょん(Bontenpøn)
@y_bonten
「├G」と必要十分なのは「あるyに対し├PROOF(y,[G]~)」だが、これは上記「├∃y[PROOF(y,[G]~)」の十分条件なのである。真ん中を省略すると (○)├Gである ⇒ (├￢G)である (×)├Gでない ⇒ (├ G)である
2013-09-18 16:22:18
ぼんてんぴょん(Bontenpøn)
@y_bonten
したがって、THEOREM(v)のときと同様の「├Gであり、しかも├￢G（体系が矛盾する）」という場合のほかに、今度は「├Gでない」という場合の可能性が残る。これを、￢Gの証明可能性によってさらに場合分けすると、├￢Gのときはω矛盾することが分かる。
2013-09-18 16:23:27
ぼんてんぴょん(Bontenpøn)
@y_bonten
結局、起こりうるのは(1) 体系がガッツリ矛盾する、(2)体系がω矛盾するにとどまる、(3)Gも￢Gも証明不可能、の3つの場合に限られる。したがって体系がω矛盾を回避できている――このとき必ず矛盾も回避できている――場合には、Gが決定不能となる（第一不完全性定理）。
2013-09-18 16:23:50
ぼんてんぴょん(Bontenpøn)
@y_bonten
講義資料には、「├Gのとき├￢G」の説明を「先ほどとまったく同様にして」としているが、ここは表現定理を使っているわけではないのでちょっと不親切ではないかと思う。
2013-09-18 16:24:58
ぼんてんぴょん(Bontenpøn)
@y_bonten
ω矛盾と矛盾、ω無矛盾と無矛盾、どっちが強い条件か、頭が混乱するけれど、矛盾を何か「良くないこと」と仮想するならば、「ω矛盾で踏みとどまる」という言い回しを覚えておくと良いと思う。もちろん内容を考えるべきなのは当然として。
2013-09-18 16:31:13
ぼんてんぴょん(Bontenpøn)
@y_bonten
├Aである（すなわち、あるyに対し├PROOF(y,[A]~)） ⇒ ├ ∃y(PROOF(y,[A]~) の矢印が一方通行であるのはかなり不思議だが、よく考えたら、逆の反例においては必ずω矛盾が生じている。
2013-09-19 05:56:13
ぼんてんぴょん(Bontenpøn)
@y_bonten
├∃y[PROOF(y,[A]~)]であっても、その一方で同時に、すべてのyの各々に対して├￢[PROOF(y,[A]~)]となってしまうことがある（これがω矛盾）。ω矛盾を許さないなら、PROOFが述語Proofを表現することを用いて、矢印の逆が言える。
2013-09-19 05:56:59
ぼんてんぴょん(Bontenpøn)
@y_bonten
表現可能性の定義の後半の対偶「￢Pが証明不可能 ⇒ pである」と、前半をつなぐと、「￢Pが証明不可能 ⇒ Pが証明可能」。いまω矛盾を許さなければ、￢PROOF(y,[A]~)が証明不可能となるyがとれて、そのようなyに対してはPROOF(y,[A]~)のほうが証明可能になる。
2013-09-19 06:27:50
ぼんてんぴょん(Bontenpøn)
@y_bonten
体系がω矛盾していなければ、 ├Aである ⇔ ├∃y(PROOF(y,[A]~) と逆方向も言えるので、 ├Aでない ⇒ ├∃y(PROOF(y,[A]~)でない も言えるが、それと表現可能性とはまた別の話。
2013-09-19 07:10:03
ぼんてんぴょん(Bontenpøn)
@y_bonten
論理式∃y(PROOF(y,[A]~)が述語「├A」を表現していると言えるためには、 ├Aでない ⇒ ├￢∃y(PROOF(y,[A]~)である が言えないといけない。
2013-09-19 07:12:20
ぼんてんぴょん(Bontenpøn)
@y_bonten
その意味でこの発言（ https://t.co/Sunj8wAgLJ )は、前半と後半はそれぞれ正しいと思うが、つながりは薄かった。たとえ論理式が述語を表現していたとしても、もともと表現可能性の矢印は片方向なのだ。
2013-09-19 07:12:57
ぼんてんぴょん(Bontenpøn)
@y_bonten
いまさらだが、「論理式Aが述語pを表現する」の定義の後半は、「pでないとき、Aは証明不可能」ではない！「pでないとき、Aの否定が証明可能」だ。
2013-09-19 07:20:40
ぼんてんぴょん(Bontenpøn)
@y_bonten
質問です。「『あるyに対し├PROOF(y~,[A]~)』ならば『├∃y[PROOF(y~,[A]~)]』」は、「ω矛盾を許せば、逆は言えない」と理解しましたが、では順方向は常識的に受け入れて構わないのでしょうか？なにか説明の付けようがあるでしょうか？
2013-09-19 12:35:44
ぼんてんぴょん(Bontenpøn)
@y_bonten
@silver_pork あるyに対し成り立つなら、そのyの一つをとって体系に放り込み、しかるのち体系内で∃導入、という寸法ですね？自分でも、正当化するならそれだと考えましたが、それでよいのかどうか自信がありませんでした。ありがとうございます。
2013-09-19 12:40:19
ぼんてんぴょん(Bontenpøn)
@y_bonten
述語Proof(y,x)の表現可能性を使えるだけ使っておいて、一方で対角化定理から肯定と否定の証明可能性の一致を切り出しておけば、不完全性定理の証明のフィナーレはかなり見通しよくできそうだな。
2013-09-19 13:15:38
ぼんてんぴょん(Bontenpøn)
@y_bonten
（もちろん、肯定と否定との間で証明可能性が一致するのではありません。├A⇔Bのとき、AとBの肯定同士、否定同士の証明可能性が各々一致する）
2013-09-19 13:17:31
ぼんてんぴょん(Bontenpøn)
@y_bonten
対角化定理から (*)├∃y[PROOF(y~,[G]~) ⇔ ├￢G となるGがとれる。PROOFがProofを表現することから、 ├Gである ⇒ あるyに対し├ PROOF(y~,[G]~)(#) ├Gでない ⇒ 全てのyに対し├￢PROOF(y~,[G]~)
2013-09-19 13:31:48
ぼんてんぴょん(Bontenpøn)
@y_bonten
(#)⇒(*)と繋ぐことができ ├Gである ⇒ あるyに対し├ PROOF(y~,[G]~) ⇒ ├∃y[PROOF(y~,[G]~) ⇔ ├￢G ├Gでない ⇒ 全てのyに対し├￢PROOF(y~,[G]~) 上行の3つ目と下行の2つ目を見比べると、互いにω矛盾している。
2013-09-19 13:32:31
ぼんてんぴょん(Bontenpøn)
@y_bonten
つまり、図式を切り詰めると ├Gである ⇒ ├￢G ↑ω矛盾↓ ├Gでない ⇒ □ これを満たすG,￢Gの証明可能性の組合せを表にすると ├￢Gである ├￢Gでない ├Gである 体系が矛盾 起こり得ない ├Gでない 体系がω矛盾 Gが決定不能
2013-09-19 13:34:43
トリのオリンピック
@wato_d
@y_bonten すいません、すごく初歩的なことを質問させてください！「⊢Gである」というのは「【Gが証明可能】である」であって「【Gである】が証明可能」ではないということでいいんですよね？
2013-09-19 16:07:50
ぼんてんぴょん(Bontenpøn)
@y_bonten
@wato_d そのとおりです。誤解を生むので、そこははっきりさせないといけませんね。否定についても同様ですが、体系内の否定は記号￢で、メタな言明の否定は日本語で書くようにしています。
2013-09-19 16:13:09
ぼんてんぴょん(Bontenpøn)
@y_bonten
もう全く好みの問題だが、オブジェクトの体系が矛盾する事態は「コップの中の嵐」に過ぎないのだから、あまり初めから「体系が無矛盾」といった仮定を置いてメタ証明を進めるのはどうもしっくり来ない。淡々と場合分けして結論を得てから、「体系が無矛盾ならば」といった形に書き直せばよいと感じる。
2013-09-19 21:40:36