-
- いいね！0
ぼんてんぴょん(Bontenpøn)
@y_bonten
@functional_yy ああ！メタ理論によってはモデル存在定理が成り立たないのかもしれないのですね。
2013-09-26 21:22:17
Hiroyasu Kamo
@kamo_hiroyasu
@y_bonten ZFC⊢∀T(∃M"M⊨T"→Con(T)) と ZFC⊢"⟨ω,0,1,+,∙⟩⊨PA" から ZFC⊢Con(PA) が導かれます。
2013-09-26 22:35:58
ぼんてんぴょん(Bontenpøn)
@y_bonten
@kamo_hiroyasu ありがとうございます。本来、「メタ理論⊢Con(オブジェクト理論)」という形でしか、無矛盾性は語りえないのでしょうか？
2013-09-26 22:44:55
ぼんてんぴょん(Bontenpøn)
@y_bonten
@kamo_hiroyasu なるほど、ご説明のすべてを理解できてはいない自覚がありますが、少し道が開けてきました。
2013-09-26 23:09:46
ぼんてんぴょん(Bontenpøn)
@y_bonten
なんだろうな、先生がこういう式を書くということは、とか、こういう表現をするということは、ということから、間接的につかめる何かがある。
2013-09-26 23:10:45
ぼんてんぴょん(Bontenpøn)
@y_bonten
私が読んでいる教科書では、どれもメタ数学的考察（例えば完全性定理や不完全性定理の証明）のフィールドに名前が付いていない。単に体系に対して外からいろいろ常識に基づいて議論しているだけに見える。
2013-09-27 10:52:06
ぼんてんぴょん(Bontenpøn)
@y_bonten
その一方で、メタ理論とオブジェクト理論という言葉をよく耳にする。じゃあ、ここはどこ？これが「有限の立場」？
2013-09-27 10:52:15
ぼんてんぴょん(Bontenpøn)
@y_bonten
例えばZFC├Con(PA)と書いてあったとき、ZFCをメタ理論、PAをオブジェクト理論と呼ぶと思いますが、この「├」はZFCのさらに外の記号ですよね。
2013-09-27 10:57:19
ぼんてんぴょん(Bontenpøn)
@y_bonten
@tkoidejp そうですね。メタ理論とオブジェクト理論の両方を俯瞰できる立場が真のメタレベルだと思うのですが、どうなのでしょうね。
2013-09-27 11:05:35
ぼんてんぴょん(Bontenpøn)
@y_bonten
@tkoidejp 「正当性の担保」という面からは、「最後は信じるしかない」「信じるに足るほど素朴な操作に限る」、あるいは「どこまで許せば何が言えるかを定量すればよい」という理解で、個人的には受け入れています。ただ一般になされている議論でメタレベルが何段階あるのかが謎で(^^;)
2013-09-27 11:28:26
ぼんてんぴょん(Bontenpøn)
@y_bonten
@tkoidejp 初心者のハマりポイントとしては重大だと思うので、識者はみんな理解していることだと信じたいですが（笑）
2013-09-27 12:25:43
ぼんてんぴょん(Bontenpøn)
@y_bonten
@tkoidejp 前に他の方に教えていただいた http://t.co/Sd5J0ew3iA が、今の議論に関係するのかどうか、まだ調べてないので分からないのですが、時間があれば検討したいと思っています。
2013-09-27 12:35:40
ぼんてんぴょん(Bontenpøn)
@y_bonten
@kamo_hiroyasu @tkoidejp ありがとうございます。「Cで書かれたCコンパイラ」には何の違和感もないのに、なぜ形式体系だとこうも悩ましいのか、たぶん実装が具体的にイメージできているかどうかの違いだと思うので、体系についても具体的に学ぼうと思います。
2013-09-27 15:46:10
ぼんてんぴょん(Bontenpøn)
@y_bonten
合宿講義資料、自然演繹における「証明可能」の定義がどこにも書いてないような気がする。p26に「最終的にすべての仮定が除去された証明図に到達したら，その終式は仮定なしに証明されたとされる．」が一番近いか。
2013-09-28 04:12:06
ぼんてんぴょん(Bontenpøn)
@y_bonten
ヒルベルト流の体系では、「形式的証明」というと直列に並んだ論理式の有限列がたぶん本来の姿で、木構造の導出図はそれを見やすくしたもの、と考えるのがしっくり来る。いっぽう自然演繹はどうなのだろう。鹿島本では木構造の導出図が存在すること自体を「証明可能」の定義としている。
2013-09-28 10:01:32
ぼんてんぴょん(Bontenpøn)
@y_bonten
自然演繹でも、導出図を直列に書き直す（もちろん一意にならなくてよい）ことは可能だろうけれど、仮定の解消をどう盛り込むのか、自明とは言えない。例えば証明の列をデータ構造として実装するなら、どういう情報が必要だろう。
2013-09-28 10:01:53
ぼんてんぴょん(Bontenpøn)
@y_bonten
「仮定が解消される」ということはどういうことなのか、立ち止って考えると結構むずかしい。当初は、証明の各ステップでフラグが立ったり倒れたりするイメージを持っていた。
2013-09-28 10:02:20
ぼんてんぴょん(Bontenpøn)
@y_bonten
しかし、実際に導出図を書いてみるとむしろ、すべての論理式のひとつひとつが「自分が依存する仮定」というリストを持っていて、仮定が解消されるときには「解消されない仮定への依存だけをリストとして引き継ぐ」というイメージのほうが良いのではないかと感じた。
2013-09-28 10:03:23
ぼんてんぴょん(Bontenpøn)
@y_bonten
合宿で近所の人が議論していたような気がするが、実際に自然演繹で導出図を書いていると、なんというか、「ここで仮定を解消してもいいのに、解消したくないよー、ってときは？強制？」みたいな疑問にブチ当たることがある。あるいは2つの仮定が同時に解消できるときに1個だけ残したい、とか。
2013-09-28 10:09:02
白露に風の吹きしくゼルプスト殿下
@tenapi
@y_bonten 導出された式が背後霊のように仮定を引き連れている形で推論図を書いた方がいいのかもしれませんね。
2013-09-28 10:09:35
ぼんてんぴょん(Bontenpøn)
@y_bonten
.@tenapi そう思います。こんな感じで勉強してました。http://t.co/ZCjZkB3j9J
2013-09-28 10:12:14
拡大
ぼんてんぴょん(Bontenpøn)
@y_bonten
「仮定をあえて解消したくないな」と感じたとき、私がどう思おうとも、導出された論理式の依存リストからその仮定が外れるという事実は変わらない。解消したくなければ、改めて同じ仮定を立てて、それに依存する論理式を導出すればよいだけか。
2013-09-28 10:21:31