-
- いいね！0
ぼんてんぴょん(Bontenpøn)
@y_bonten
『数学ガール(G)』で述語を構成していく過程の最後に、原始再帰的でないIsProvableという述語が登場して、その後の議論におけるこの述語の扱いがいま一つ分からなくてモヤモヤしていた。実はそこが超重要ポイントなんだけれど。今回の講義でそこを明瞭に理解できたのが嬉しい。
2013-09-16 23:01:41
ぼんてんぴょん(Bontenpøn)
@y_bonten
この述語に限ったことではないけれど、IsProvable(x)の定義∃p[Proves(p,x)]の「∃p」は、論理式としての∃pではなく、述語の言明の一部。分かりにくければ日本語で「Proves(p,x)を満たすpがとれる」などと書けばよい。
2013-09-16 23:02:08
ぼんてんぴょん(Bontenpøn)
@y_bonten
で、この述語は（pに上界がなく）原始再帰的でないから表現不可能とはいうけれど、Proves(p,x)を表現する論理式（PROVES(p~,x~)とする）の頭に単純に∃pを付けてやればいいのではないか？という気がする。
2013-09-16 23:03:23
ぼんてんぴょん(Bontenpøn)
@y_bonten
Proves(p,x)が原始再帰的なので、確かにそういう論理式は構成できる。だが、それはIsProvable(x)を表現する論理式ではない！という点が重要。
2013-09-16 23:03:51
ぼんてんぴょん(Bontenpøn)
@y_bonten
つまり、「『論理式PROVES(p~,x~)が証明可能』となるようなpが取れること」と、「論理式『∃p[PROVES(p~,x~)]』が証明可能であること」とは全く違うということだ。IsProvableは前者だが、後者の論理式はこの述語を表現しない。
2013-09-16 23:04:19
ぼんてんぴょん(Bontenpøn)
@y_bonten
実際、IsProvableを表現する論理式は構成できないことが示せるが、だからと言ってこの「パチモン論理式」を捨て去ってしまうのではなく、これを元にして構成された論理式がゲーデル文だ。
2013-09-16 23:04:36
ぼんてんぴょん(Bontenpøn)
@y_bonten
ゲーデル文が「この文は証明可能ではない」という意味を持つとみなして直感的に理解する際には、パチモンであることを重々承知の上で慎重に考えなければならない。
2013-09-16 23:05:12
ぼんてんぴょん(Bontenpøn)
@y_bonten
なんちゅうか言葉で「藤田先生ありがとう」って言いたいのはもちろんだけれども、自分なりのゼミの成果をアウトプットして謝意を示したいのよね。まぁこれくらいにして今日は寝ます。
2013-09-16 23:21:14
ぼんてんぴょん(Bontenpøn)
@y_bonten
メタ数学的考察の「メタ」と、「メタ理論と対象理論」の「メタ」とが同じなのか違うのかも私はよく分かっていない。「メタ理論」の住人は自分がメタ理論であることをあずかり知らないわけで（比喩）、「メタ理論と対象理論」と呼んだ時点で、我々はさらにメタにいるだろうか。
2013-09-18 06:57:25
ぼんてんぴょん(Bontenpøn)
@y_bonten
├(A⇔B)というのは凄い条件だな。⇔自体は体系の中の論理式で、(A→B)∧(B→A)の略記に過ぎない。だが、├(A⇔B)のとき、AとBの証明可能性の是非は一致するし、さらに￢Aと￢Bの証明可能性まで一致する。その根拠は（自然演繹なら）∧除去やMPという(^^;)
2013-09-18 07:01:00
ぼんてんぴょん(Bontenpøn)
@y_bonten
いや「⇔」が論理式の中の記号だからこそ、このようなメタ的な条件を一つの式で表せてしまうのか。冗長だが「AとB、￢Aと￢Bの証明可能性の是非がそれぞれ一致する」という概念を表す記号を作るのもアリかもしれない。
2013-09-18 07:07:05
ぼんてんぴょん(Bontenpøn)
@y_bonten
「├(P⇔Q)のとき、『PとQ』および『￢Pと￢Q』の証明可能性の是非が各組で一致する」ということを先に切り出しておいて納得し、これを念頭に置いて、「├Aである」を表現する論理式THEOREM(v)がもしも存在すれば体系が矛盾することを示す。
2013-09-18 14:18:49
ぼんてんぴょん(Bontenpøn)
@y_bonten
表現可能性の定義から、 (├X)である ⇒ ├ THEOREM([X]~) (├X)でない ⇒ ├￢THEOREM([X]~) ただし[X]~は「論理式Xのゲーデル数を数項化したもの」。
2013-09-18 14:19:13
ぼんてんぴょん(Bontenpøn)
@y_bonten
いま、対角化定理を￢THEOREM(v)に適用し、それによって存在が保証される論理式をAとすれば、先ほど念頭に置いたことから、こういう構図を書き足すことができる：
2013-09-18 14:20:12
ぼんてんぴょん(Bontenpøn)
@y_bonten
(├A)である ⇒ ├ THEOREM([X]~) ⇔ (├￢A)である (├A)でない ⇒ ├￢THEOREM([X]~) ⇔ (├ A)である 表現定理による矢印の方向が一方通行であることと、左端と右端に書いてあることの違いに注意。
2013-09-18 14:21:12
ぼんてんぴょん(Bontenpøn)
@y_bonten
真ん中のTHEOREMのところを省略すると (├A)である ⇒ (├￢A)である (├A)でない ⇒ (├ A)である さて問題、上記を満たすようなAと￢Aの証明可能性の組み合わせのうち、ありうるのはどれか？
2013-09-18 14:21:48
ぼんてんぴょん(Bontenpøn)
@y_bonten
少し考えれば「├Aであり、しかも├￢Aである」場合だけが残ることが分かり、これは体系が矛盾する場合である。ちゃんと可能性が残るのだから、メタ的には矛盾していない。■
2013-09-18 14:22:31
ぼんてんぴょん(Bontenpøn)
@y_bonten
THEOREM(v)がもしも存在すれば体系が矛盾することが分かったが、ではパチモン論理式∃y[PROVES(y,v)]では議論がどう変わるのか？ここからは講義資料に合わせてPROVESをPROOFと書くことにする。
2013-09-18 16:19:35
ぼんてんぴょん(Bontenpøn)
@y_bonten
PROOF(y,v)は構成可能であることが分かっているので、それに∃yを付けたものは構成できる。だが、THEOREM(v)のときのように、それが何か述語を表現するのかどうか分からない。とりあえず対角化定理から分かることは：
2013-09-18 16:20:05
ぼんてんぴょん(Bontenpøn)
@y_bonten
├ ∃y(PROOF(y, [G]~) ⇔ (├￢G)である ├￢∃y(PROOF(y, [G]~) ⇔ (├ G)である ところが――ここからがこの論理式の微妙なところだが――Gの証明可能性に対して、表現定理の前半（肯定に関する部分）だけはTHEOREMと同様に成り立つのだ。
2013-09-18 16:20:46
ぼんてんぴょん(Bontenpøn)
@y_bonten
(○)├Gである ⇒ ├ ∃y(PROOF(y,[G]~) ⇔ (├￢G)である (×)├Gでない ⇒ ├￢∃y(PROOF(y,[G]~) ⇔ (├ G)である
2013-09-18 16:21:41