数学の基礎づけ

谷口一平 A.k.a.hani-an @Taroupho

結局、数理論理学と公理的集合論とは、どちらがどちらを基礎付けていると考えればいいの？　ZFCは1階論理上に建てられて、だから1階論理はZFCに先行すると考えてよい筈だが、1階論理の完全性定理の証明に選択公理が必要という話になると、これは先にZFCが存在しないとまずいよね。

谷口一平 A.k.a.hani-an @Taroupho

1階論理上に建てたZFC上に建てた1階論理に関する定理、と考えることも出来る筈だけど、すると、初めに存在した「1階論理」と「ZFC上に建てた1階論理」とが＜同じもの＞だということの保証は何がするのだろう？　もやもーや。

谷口一平 A.k.a.hani-an @Taroupho

詳細はよく知りませんが、数理論理学や公理的集合論に加えて絶対数学だの圏論だの関係代数だの、現代数学にユニヴァーサル性を謳った分野が多数出現して来ているというのは、数学の領域でも島宇宙化の進行と全体性への希求とが前景化し出しているということなんですかね。

谷口一平 A.k.a.hani-an @Taroupho

尤も、20世紀以降の数学者というのは基本、無節操なので、東浩紀風に表現すれば、最初から動物化していたと言えるかも知れません。スノッブな数学というのは魔術と哲学とに取り込まれて、現代では実在していない？

谷口一平 A.k.a.hani-an @Taroupho

ああ、スノッブな数学って、区体論とか角の三等分家とか新千年紀においての論理改革とか自然数解が存在する全構造の解明とか、あの界隈のことですか？　ごめん、なら余裕で実在するわｗ

Jun Inoue @jun0inoue

@Taroupho また懲りずに答えてみますw 式φのゲーデル数を#φで表わすとして、∀theories T. (T⊢φ)↔(T⊢∃#proof(ZFC⊢φ)) というメタ定理を証明できれば直観レベルでは最初の一階論理と#の下に作った一階論理が同じ物といえます。

Jun Inoue @jun0inoue

@Taroupho そのメタ定理自体を更に#して ZFC⊢∀#T. #proof((T⊢φ)↔略)) とかすればZFCがその同値性まで示した事になります。Coq は #Con(Coq) を構築できるけど件の定理を#の下では証明できないから不完全性定理に反しないとか何とか。

Jun Inoue @jun0inoue

@Taroupho これは前より難しい話で、専門外なので信憑性は「知ってるのか雷電」程度だと思って下さい。 http://t.co/jA2TJv3 と http://t.co/lAANvxQ も参照。

Jun Inoue @jun0inoue

@Taroupho あ、そっかハッシュってタグになるんだったw 進歩がねぇww

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue 毎度お世話になっておりますｗ　えーと、式の意味が微妙に取りにくいため確認させていただきますと、まず #φ は1階論理の論理式 φ のゲーデル数に対応する ZFC の対象式、と読んで大丈夫ですよね？　そして、T が1階論理の形式的体系を表わす、と。

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue すると、ZFC 上の T に関する可証性述語を Bew(x) として、最初のメタ定理は「任意の論理式 φ に対して、(T |- φ)⇔(ZFC |- Bew(#φ)) となる」のことと理解してオーケーでしょうか。でしたら、確かに両者は同じものと言えそうです。

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue えー、このメタ定理は……証明可能なんですかねｗ　これが、もし (ZFC |- φ)⇔(ZFC |- Bew(#φ)) の形をしていたら、真理述語の定義不能性に反してしまい証明出来ない感じですが、当座は左辺を T の範囲で考えていますから、何とも微妙なｗ

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue それと、完全性定理に限定して言えば、ZFC 上の T に関して完全性定理を示すには、「モデル」とか「充足関係」とかを ZFC の言葉で定義しないといけないわけですが、「充足関係は ZFC では定義出来ない」という話を風聞したような。間違っていたらすみません。

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue 仮に先のメタ定理が証明可能で、完全性定理など ZFC で形式化可能とすると、好きなときに1階論理に敷かれている ZFC を仮定したり、その逆を仮定したりしてよい、ということになるのでしょうかね。なんだか、直観的には不思議な感じがしてしまいますねー。

Jun Inoue @jun0inoue

@Taroupho #φについてはそんな感じです。式φとか言いましたけど、要するに構文全般をゲーデル数 (に対応する集合) に置き換えるものです。T は公理系というか、theory です。日本語で形式的体系と呼んでるものの事かわかりませんが、推論に使える式の集合です。

Jun Inoue @jun0inoue

@Taroupho Bew の定義に T を取り込むなら(T |- φ)⇔(ZFC |- Bew(#φ)) って事です、はい。可証性述語が T もパラメータとして取るように考えてましたけど、そういや閉包する (取り込む) 方が一般的でしたね。

Jun Inoue @jun0inoue

@Taroupho できる…はずです (チェックしてません、すいません。ここら辺が畑違いの限界…w) 要するにZFC⊢φ に使える論理規則を全部 Bew がちゃんと含んでるかどうかって事ですから。例えば Bew は modus ponens について閉じてるとかチェックします。

Jun Inoue @jun0inoue

@Taroupho http://t.co/lAANvxQ　では (T⊢φ)⇒(T⊢Bew(#φ)) になってますね。逆向きは要らんのかしら。

Jun Inoue @jun0inoue

@Taroupho 真理述語に関しては詳細を知らないので教えてほしいのですが、多分(T⊢P(φ))⇔(T⊨φ) なPの事ではないですか? そういうPは可能なモデルを検討するので導出を検討するBewとはまた違うはずです。だからどうなのかはこれから考えないといけませんがww

Jun Inoue @jun0inoue

@Taroupho 充足関係が定義不能はちょっと信じがたいです。例えば "Mは∃x.∀y.¬y∈xを充足" は "∃x. x∈M∧∃y. y∈M→¬y∈x" とできます。しかしZFCの言語に"Mは現在推論を行っているZFCの公理を満たす"という述語を追加することはできません。

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue 申しわけない、色々勘違いしていた気がします。T は「任意の」理論でしたね（1階述語計算の頭しかなく、多少混乱しておりました）。可証性述語に関しても、閉包したことしかないため、違和感に引っぱられてしまいました。ご説明感謝します。

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue で、本題の (T |- φ)⇔(ZFC |- Bew(#φ)) ですが、ごめんなさい、これは成立しますね、確かｗ　不完全性定理によって成立しないのは、(￢(T |- φ))⇔(ZFC |- ￢Bew(#φ)) の方でしたか。真理述語の話などは勘違いでしたｗ

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue 本筋から逸れますが、真理述語の定義不能性に関しては、意味論を介入させずとも定式化できた記憶があります。T |- φ⇔P(#φ) なる P は存在しない、という形で。対角化定理から A⇔￢P(#A) な A が存在して、一方 A⇔P(#A) となり矛盾します。

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue ……これは別の話だったかも。自信ないです。一般的には (T |= φ)⇔(T |- P(#φ)) の形をよく見かけますね。両者とも「Tarski の定理」という名前で紹介されていた気がします。どういう関係なんだろう？

谷口一平 A.k.a.hani-an @Taroupho

@jun0inoue さて、何だか当初の疑問をすっかり忘れてしまった感じですｗ　えーと、例のメタ定理は成立するとして、ただ証明可能性は可証性述語では表現されなかった筈ですが……これでよかったんでしたっけ。結局、不完全性定理の理解の浅さに足を引っぱられている気がしますねー。