【自分用まとめ】数学とロジック

キルミーしぶや( ⚪︎д⚪︎)ﾉ田 @bestmove68gin

I「おっ、君なんの本読んでるの？」 ぼく「えっと数学基礎論です」 I「えっ…基礎論なんていうのはゲーデルの不完全性定理で全部決着がついて終わったはずなんだけどなぁ……」 絵に描いたような老害

ytb @ytb_at_twt

数学基礎論を終わらせたのは、ゲーデルではなく数学者の無関心です(断言)。

ytb @ytb_at_twt

数学基礎論は、非ユークリッド幾何学とルベーグ積分の衝撃の中で生まれ、全ての学問の基礎付けが論理学の手法で提供できるという誤解の中で呻吟し、「学問の基礎付け」というアイディアが人気を失う中数学者に忘れられて死んだ。 今でも同じ名前の学問はあるが、あれは「基礎付け」とは全く関係無い。

ytb @ytb_at_twt

数学基礎論ってなに — かつては、不確かな数学という学問に確固とした基礎を提供するという研究プロジェクトでした。今は、数学者が数学をする時に行う推論がなす数学的構造を数学的に分析する学問です。現在は大人しい通常科学の一つで、大変… l.ask.fm/igoto/45DKECN7…

ytb @ytb_at_twt

数学基礎論を終わらせたのは、ゲーデルではなく数学者の無関心です(断言)。

ぴあのん @piano2683

数学基礎論の人はどれだけ数学者に関心を持ってもらおうとしてるんですかねぇ。

dif_engine @dif_engine

@piano2683 そんなっ…まるで数学基礎論が数学の分野の外にあるみたいな言い方じゃないですか

ぴあのん @piano2683

@dif_engine ここで言う数学基礎論とは狭義（基礎づけの人々）なのか広義（≒数理論理学）なのかどちらでしょうか。 少なくとも基礎づけの研究に関しては、あまり数学に対する意識が向いていないように思うのでこう言いました。個人的には数学とロジックの手法の融合を夢見ています。

dif_engine @dif_engine

@piano2683 正直「基礎づけ」の方に限ってもその語の示す範囲が不明確な気がします。例えば証明論なんかは「基礎づけ」でしょうか？

ぴあのん @piano2683

@dif_engine 私の意図としては「数学を記述するための（形式）体系」についての研究を意図しています。 なので、証明論は（主に論理体系そのものの性質を調べることを念頭に置いているので）数学の基礎づけではないと思っています。

dif_engine @dif_engine

@piano2683 うーん、（私の理解では）証明論、モデル理論、（フレーゲ以降の）論理学は何らかの意味で数学の基礎づけの問題だし、集合論や型理論も数学の基礎づけの問題なんだよなぁ。

dif_engine @dif_engine

証明論は数学の証明の構造を研究する学問としてスタートしたけど後にカリハワで型の理論と結びついて、型の理論に刺激を与える存在になってるし、モデル理論は超準解析の基礎づけに使えるし、一階述語論理は集合論と組み合わせて「数学の平民用日常語」になってるんだよなぁ。

dif_engine @dif_engine

数学を記述する体系ってのがいまいちわからないけど、集合論とか型の理論のことかなぁ。

dif_engine @dif_engine

数学基礎論が何を意味してるかはともかく、可換環論の本を普通に読める人でも一階述語論理の最初の方、基礎論の人が当たり前に思ってる「言語」で躓くことがあるってはっきりわかんだね。

スマートコン @mr_konn

証明論は証明木と呼ばれる構造を研究する分野だし、ZFC集合論は∈という関係を研究する分野ですね

スマートコン @mr_konn

基礎付けにもつかえる、ということと基礎付けとしてその分野を研究するというのは別でしょ。

スマートコン @mr_konn

HoTT ひとつとっても、Univalence Axiom 等の公理を追加した型理論を研究する分野で、さらにAwodey はそれを基礎づけに使って計算機上でverifyできる数学を実現しようといっている、という風に両者はちょっと違う

スマートコン @mr_konn

集合論は基礎付けにも使えるし、今修論でやってる Solovay-Shelah なんかは現代的な意味で Foundational な意味を持ちうる結果ですね。そういう話も面白いと思うしやるけれど、それとは無関係に集合論単体としての研究というものがある。

スマートコン @mr_konn

っていうこと半世紀くらいずっと言われてると思うんですけど

スマートコン @mr_konn

Solovay-Shelah はまだ30年前🙅

ぴあのん @piano2683

基礎づけ云々、私が論点にしたいのは「数学を記述する体系について考える」という立場に類するものがあるかどうかです

ぴあのん @piano2683

私の認識だと、 ・（狭義の）数学基礎論＝数学を記述するための体系についての研究（e.g.型理論、トポスによる基礎づけと集合論の比較） ・（狭義の）数理論理学＝数学的な手法を用いた論理学（証明論） となっていて、要は何を研究対象として見ているかに着目した用語の使い分けをしたいです。

ぴあのん @piano2683

で、本来の話題に戻ります。数学者の（広義の）数学基礎論への無理解を嘆く気持ちはわかるけれど、じゃあ実際に数学に歩み寄ろうとする研究してる人はモデル理論と集合論の一部（？）の人＋αしかいない気がする。

ぴあのん @piano2683

以下、便宜上、広義の数学基礎論のことを「ロジック」と言うことにしましょう。 数学者にとって魅力的な結果がない限りは、ロジックはあくまで言葉・道具であって本質的だとは思ってもらえないでしょう。この点でロジックから数学への歩み寄りが必要だと思います。