数学基礎論・数理論理学のスレッド　その7

1 名前：１３２人目の素数さん mailto:sage [2010/11/11(木) 22:13:57 ] 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、 19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。 現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、 多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。 （「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。） 応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、 英米系哲学の一部などを含み、多岐にわたります。 （数学セミナー98年6月号、「数学基礎論の学び方」 ttp://www.math.tohoku.ac.jp/~tanaka/intro.html 或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照） 従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。 他のスレで御質問なさるようにお願いします。 前スレ 数学基礎論・数理論理学のスレッド　その6 kamome.2ch.net/test/read.cgi/math/1265884076/ 7 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 03:10:13 ] >>3 数学板名物　強迫観念的過剰整理集約者 8 名前：１３２人目の素数さん [2010/11/12(金) 07:21:26 ] Well-Pointed 付き圏が形成するような、 ZFC、GBなどの代替2階述語空間では バベリアン・ライブラリ圏を定義できます。 これはバベルの図書館的情報海をヒントに作られた 表現可能宇宙全体をスタックとして移動していきます。 つまるところ定義自体が定義の生成圏となっています。 9 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 07:38:54 ] >>8 隔離スレへ帰れ！ハウスハウス！ 10 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 07:44:02 ] 無限集合論のアーレフなんかも 数種類知られているが、 キリスト教徒による無限の解釈は 濃度の非切断性による圏論的定式化だったといわれている>>8 11 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 07:46:46 ] 荒らしに何言っても無駄だとは思うが、とりあえず圏論はスレ違いってことで。 12 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 08:46:56 ] こんだけ無内容なレスできるのも一種の ポストモダン的な才能だな 13 名前：１３２人目の素数さん [2010/11/12(金) 13:04:51 ] モデル理論は、何を研究するの？ 14 名前：１３２人目の素数さん [2010/11/12(金) 19:08:54 ] >>13 数学全体の基礎に述語論理があるけども、 モデルというのはススリンの木によるダイアモンド原理を 実現するためにクリプキによって導入された理論。 基本的にはドゥルーズ以前の樹形図による発展的論理学。 ポストの定理が証明されてからはリゾームへ移行している。 15 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 19:17:49 ] 隔離スレ池谷カス 16 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 19:35:11 ] Model theory is the geography of tame mathematics. (Hrushovski) 17 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 20:03:08 ] >>14 で、何を研究すんの？ 18 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 20:20:56 ] 397 ：23世紀の論理学の提唱 ：2010/04/25(日) 11:16:36 さて、スペンサーブラウンが提唱した形式の法則であるが、 これはCalculusに基くブール代数の構成を可能にした「区別」と 呼ばれるシステムの自己観察機能による再循環−これは マトゥラーナ＝ヴァレラ図式によるもの−に「拡大」可能となっている。 例えば「横断」による算法、これは自己同型写像による対象aの分布関数 R：Spec(�農N0)；B(a,ε)→Vll(-<>r) を意味するもので、primary algebra の公理からアイオーンの時間の固体化、 即ちリンデンバウム補数の位相が閉であること(ArrX/R)、 また複素散乱ウカシェベッチ型ベクトルの縮減対応から得られる 「埋め込み」が線型写像であること⇔Θ：ξ(Asc(3))ΛΓ(A_0)→Γ(A_0)の作用が存在する。 直線的被覆が「シミュラークルの質料」というXの規定、これが即ち論理学である。 山之内　彰 19 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 20:24:55 ] ◆ 略　歴 ◆ 　山之内　彰（やまのうち・あきら）八戸市出身。 保健体育教諭。八戸高―早大。 卒業後に教員となり、八戸工高、八戸南高などを経て、９６年に八戸高に赴任。 20 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 20:29:54 ] 　model theory = universal algebra + logic by Chang & Keisler "Model theory" 　algebraic geometry - field = model theory by W. Hodges by "A shorter model theory" らしいよ。universal algebraは知名度的に微妙にマイナーだから 後者の方が分かりやすいと思う。 代数幾何は体Fに対して代数式で定義されるようなF^n内部の「図形」を 研究する。もっと一般的に対象領域Dがあるときに、 論理式（代数式、不等式なども含むけど量化論理式なども含む）で 定義されるようなD^n内の「図形」を研究するのがモデル理論だと思っとけば良い。 だから代数幾何には応用しやすくて、実際に代数幾何の定理が モデル理論を用いてどんどん証明されていたりするわけだ。 21 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 20:33:18 ] 代数幾何学が盛んな筈の日本で、モデル理論知らんて代数幾何学の研究者が殆どなのは何故？ 22 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 20:59:31 ] 小耳に挟んだことくらいはある方が普通だと思うけど。 23 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 21:21:15 ] 乞食が殺到する程の有効性が無いのだろう 24 名前：１３２人目の素数さん [2010/11/12(金) 21:32:12 ] 極小モデル理論とは関係ないの？ 25 名前：１３２人目の素数さん [2010/11/12(金) 21:59:41 ] 以前書いたが例えば ヒルベルトの既約性定理をモデル理論で証明 するより、Puiseux級数を使ったりして、 具体的な構造を見る方が重要なんだって。 26 名前：１３２人目の素数さん mailto:sage [2010/11/12(金) 22:01:16 ] 基礎論を学ばない言い訳w 27 名前：１３２人目の素数さん mailto:sage [2010/11/13(土) 00:33:40 ] >>22 同意 日本でだって、『幾何的モデル理論入門』 by 板井昌典　（日本評論社）なんて教科書まで一応は出てるんだし その本にも出てるHrushovskiの仕事ぐらいは知ってる代数幾何屋は少なくないんじゃないの？ 少なくともモデル理論は基礎論極右というか基礎論原理主義者の巣窟の証明論よりは 普通の数学者(Mac Lane風に言えば working mathematicians、「現場の数学者」とでも訳すのが正解かな？)にも 「数学の分野として存在意義アリ」と認知されてるんじゃないの？ その点、証明論はなあ 最近は "Applied Proof Theory"なんて本も出てるみたいだけど、コンピュータサイエンスの理論屋にはともかくとして 普通の数学者からはどこまで存在意義を認められてる事やら 28 名前：１３２人目の素数さん mailto:sage [2010/11/13(土) 00:53:51 ] working mathematician は職業数学者じゃねーの？ 29 名前：１３２人目の素数さん mailto:sage [2010/11/13(土) 02:23:02 ] 今読んでる本にλ計算というのが出てきたんだが、何だこの記号…すげえ見辛い… 30 名前：１３２人目の素数さん mailto:sage [2010/11/13(土) 02:51:33 ] λカリキュラスなんて、あんなもんやってもなあ・・・ 31 名前：１３２人目の素数さん [2010/11/13(土) 14:38:01 ] こんちには みさなん おんげき ですか？　わしたは げんき です。 この ぶんょしう は いりぎす の ケブンッリジ だがいく の けゅきんう の けっか にんんげ は もじ を にしんき する とき その さしいょ と さいご の もさじえ あいてっれば じばんゅん は めくちちゃゃ でも ちんゃと よめる という けゅきんう に もづいとて わざと もじの じんばゅん を いかれえて あまりす。 どでうす？　ちんゃと よゃちめう でしょ？ ちんゃと よためら はのんう よしろく 32 名前：１３２人目の素数さん [2010/11/13(土) 16:34:39 ] >>25 一般的には具体的な計算が困難（実際的には不可能）だから非構成的な証明が考案されるわけでしょ。 ゴルダンに戻るわけ？ 33 名前：１３２人目の素数さん mailto:sage [2010/11/13(土) 17:01:18 ] ヒルベルトの神学、なんて言われた時代もあったんだってねえ 34 名前：１３２人目の素数さん mailto:sage [2010/11/13(土) 17:18:02 ] 数学を形式的に記述していって、例えば実際に微積分まで形式化した人はいるんでしょうか プリンキピア・マテマティカでさえ実数論までだと聞いていますが 35 名前：１３２人目の素数さん [2010/11/13(土) 17:39:00 ] >>34 ツァリス（ツァリス・エントロピーの考案者）が、 多重線形積分まで形式化した。 トラック・サンジャイロ構成や第3層制限解釈によって 分裂しやすい論理学を生成してからカリー・ハワード対応を与えることで。 36 名前：１３２人目の素数さん mailto:sage [2010/11/13(土) 19:43:32 ] Coq coq.inria.fr/ などのアプローチは >>34 に該当するだろうか ライブラリには derivative の文字も見えるが 37 名前：１３２人目の素数さん mailto:sage [2010/11/28(日) 22:50:53 ] バートランド・ラッセルのプリンキピア・マテマティカと ヒルベルトの形式系はどの点で違うんでしょうか？ 素人向きの解説書、どなたかご存じありませんか？ 38 名前：１３２人目の素数さん mailto:sage [2010/11/28(日) 23:03:46 ] プリンキピア・マテマティカは型付きの体系なのが一番の違い 解説書としては「確かさを求めて」とか 39 名前：１３２人目の素数さん [2010/12/17(金) 05:16:50 ] 超数学と数学基礎論の違いを教えてください。 全く異なる分野なのですか, それとも片方が他方の一分野の関係になっているのでしょうか? 40 名前：１３２人目の素数さん mailto:sage [2010/12/18(土) 01:16:09 ] 『算術的命題、すなわち一階算術で記述可能な命題に関しては、 選択公理を使った証明があればそれを使わなくても証明できる。』 この定理の証明が載っている文献をどなたか御存知ありませんか？ 41 名前：１３２人目の素数さん mailto:sage [2010/12/20(月) 16:53:54 ] 多くの公理的集合論の本に載っている有名な基本的な定理の系。 オリジナルに近いものを読みたいならば、Goedel の本をどうぞ。 Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory. Princeton University Press 42 名前：１３２人目の素数さん mailto:sage [2010/12/20(月) 17:59:37 ] >>41 ありがとうございます。 趣味で基礎論を勉強している身ですが、やっと公理的集合論に取り掛かる決心がつきました。 43 名前：１３２人目の素数さん mailto:sage [2010/12/23(木) 15:45:33 ] 俺もやるよ。 44 名前：１３２人目の素数さん [2010/12/29(水) 10:14:23 ] 初歩的な質問で申し訳有りませんが2つ質問させてください 1. 命題論理や一階述語論理よりも基本的な公理系はありますか？ あるのでしたら教えてくださいませんか？ 2. 公理的集合論は一階述語論理の上に定義されるから "公理系"の"系"って公理的集合の一種にはなりませんよね？ だとすると"系"っていったい何なんですか？ "系"を組み立てるための"公理系"が存在してしまったら循環論法になりませんか？ あるいは「まず素朴に定義しておいて、後に公理的集合論を定義したあと、 その素朴な定義が、公理的集合論と矛盾しないことを示す」 みたいな回避方法を取るのでしょうか 45 名前：１３２人目の素数さん mailto:sage [2010/12/29(水) 13:25:40 ] 形式化というのは飽くまでも無矛盾性を示したり 或る命題が独立であることを示したり、或いは 証明が厳密に行われることを保障するために行うものなので、 別に循環論法だとかそういうことは無いと思う。 集合論やら述語論理やらを記号列に関する形式的なルールの集まりとして表現した時に、 そのルール自体は、元の理論で直接扱うようなものでは無いんです。 46 名前：１３２人目の素数さん mailto:sage [2010/12/29(水) 13:38:38 ] 「より基本的」というのが「証明できる論理式がより少ない」という意味なら 最小論理、直観主義論理、etc...があるけども 47 名前：１３２人目の素数さん mailto:sage [2010/12/29(水) 15:47:20 ] 公理系ってのは あるパラダイムの中でしか 意味を為さない 48 名前：１３２人目の素数さん mailto:sage [2010/12/29(水) 15:51:01 ] そりゃそうだ 49 名前：１３２人目の素数さん mailto:sage [2010/12/29(水) 16:04:50 ] 哲学に憧れて厨二的誇大解釈をしてしまう人も稀にいるのかもしれない 50 名前：44 [2010/12/29(水) 17:08:00 ] >>45 なるほど・・・ では間接的になら扱うことが可能なのでしょうか >>46 二階述語論理に対する一階述語論理、 一階述語論理に対する命題論理のような意味での基本的という意味です 論理ではなくて単なる記号の規則でも良いです 51 名前：１３２人目の素数さん mailto:sage [2010/12/29(水) 18:25:32 ] 間接的にで良いなら、自己言及「的な」現象が起こることがあって、 その良い例が不完全性定理。 基本的と言うか、より一般的な記号列の機械的な書き換えということになると オートマトンだとかチューリングマシンだとかの話になるけど、 だんだん数理論理というより計算機科学よりの話になる。 52 名前：１３２人目の素数さん mailto:sage [2010/12/30(木) 00:31:12 ] >>45 完全性定理の証明に選択公理が使われてても問題ないのか？ 納得できん 53 名前：１３２人目の素数さん [2010/12/30(木) 03:05:37 ] ゲーデルによる不完全性定理の証明に中国剰余定理が使われているようなもの。 計算量理論の観点からすると問題になるらしく、この定理を使わない改良版もあるそうだ。 54 名前：１３２人目の素数さん mailto:sage [2010/12/30(木) 08:05:03 ] 確か前スレに完全性定理と選択公理の話あったぞ 55 名前：１３２人目の素数さん mailto:sage [2010/12/30(木) 22:01:05 ] 選択公理を無くせ 56 名前：１３２人目の素数さん mailto:sage [2010/12/31(金) 17:24:04 ] >>54 前スレ見たけどいまいち。 「式の集合」がZFCのモデルになっているとは考えにくいし。 57 名前：１３２人目の素数さん mailto:sage [2010/12/31(金) 17:28:09 ] 「式の集合」がZFCのモデルになっているなんて話あったかなあ、 58 名前：１３２人目の素数さん mailto:sage [2010/12/31(金) 19:08:16 ] >>57 あ、そこまでは言ってないや。 でもZornの補題とほぼ同じような論拠で極大理論をもってきてるでしょ。 理論＝公理の集合。つまりは式、というか文字列の集合だし、そんなものが ZFC（の一部かな？）のモデルになってるわけないや、と。 59 名前：１３２人目の素数さん mailto:sage [2010/12/31(金) 20:58:41 ] ごめん前スレよく見たら131あたりで議論してるね。 有限な立場では完全性定理の証明はできないってところまでは合意済み（？）のようだ。 それと上記の疑問はまた別物と言うことで。 60 名前：１３２人目の素数さん mailto:sage [2010/12/31(金) 21:16:55 ] 人間や計算機が実際に扱うような理論は、有限個の記号しか扱わないから 論理式を整列できるし、選択公理も別に要らない。 だから認識論的なことを話題にする限りは別に問題にはならなくて、 選択公理が問題になるのは、そもそも理論で使う基本的な記号の集まり自体が 基数を持たない、みたいな場合なので、別に問題ないんじゃないかと。 61 名前：１３２人目の素数さん mailto:sage [2010/12/31(金) 22:54:53 ] >>60 そうなのか？ 記号が有限、個々の論理式の長さは有限、全体としては可算無限まで。 その中から矛盾にならないよう論理式を選んでいって極大理論に至る。 これが論理式が整列できるなら選択公理いらない？ 62 名前：１３２人目の素数さん mailto:sage [2010/12/31(金) 23:20:03 ] ところで完全性「定理」っていうけど何理論の定理？ 一階述語論理における真理ではあるんだろうけど、「定理」って？ 63 名前：１３２人目の素数さん mailto:sage [2010/12/31(金) 23:38:16 ] A1 A2 A3 …：閉論理式の枚挙 �@Γ_0 ：無矛盾集合 �AΓ_i まで得られたとして、Γ_i+1 を次のように定める 　Γ_i │─ ¬A_i+1 ならば Γ_i+1 ＝ Γ_i 　Γ_i │─ ¬A_i+1 でないならばΓ_i+1 ＝ Γ_i ∪ { A_i+1 } Γ_∞ ＝ Γ_0 ∪ Γ_1 ∪ Γ_2 ∪ … と定めると、これは無矛盾かつ完全（どの閉論理式も証明可能or反証可能） 記号が可算個なら閉論理式は可算個なので、 選択公理の替わりに上の事実を用いて極大無矛盾集合を作ればよい 64 名前：１３２人目の素数さん mailto:sage [2011/01/01(土) 01:00:12 ] 2011明けましたおめでとう >>63 各 A_i+1 または ¬A_i+1 を追加する箇所でどっちが無矛盾か判定する手続きはないから作ることはできないよね。 「作ることができる」じゃなくて「存在するよ」だったら言えるのか。 枚挙された閉論理式の集合の冪集合の中に「すべてをうまく選んだ例」が一つは存在するよ、って主張だろうか。 選択公理の使用だけじゃなく他にもいろいろ気になるなあ。 65 名前：１３２人目の素数さん [2011/01/01(土) 08:02:53 ] ゲーデル解釈っぽく考えたら心理的な違和感はだいぶ解消する つまりＡという命題を「Ａでないということはない」、 「Ｇ（ｘ）となるｘが存在する」を「全てのｘに対してＧ（ｘ）でない、ということはない」と解釈する 66 名前：１３２人目の素数さん mailto:sage [2011/01/01(土) 16:16:48 ] >>65が流れと関係あるのかどうかわからんね。 完全性定理への選択公理の使用有無は>>63にもう一度聞きたいな。 67 名前：１３２人目の素数さん [2011/01/01(土) 22:23:43 ] 存在という言葉にこだわるのは楕円曲線を考えるとき楕円をイメージするくらい意味のない行為 68 名前：１３２人目の素数さん mailto:sage [2011/01/01(土) 22:31:41 ] だって素手でやっていい範囲でって言われても、その範囲がわかりにくいじゃん。 楕円曲線とかは抽象的存在と割り切って議論進めてるんでしょ？使っていい道具も決まってるんだろうし。 論理式の集合だと実在してるものを相手にしてる感じだし〜 69 名前：東大生 mailto:AGE [2011/01/01(土) 23:13:34 ] おまえら馬鹿なんだから、蘊蓄はいいよw 70 名前：１３２人目の素数さん mailto:sage [2011/01/01(土) 23:18:02 ] > 蘊蓄 へー、なんて読むんですか〜？ 71 名前：１３２人目の素数さん mailto:sage [2011/01/02(日) 00:32:47 ] うんち 72 名前：１３２人目の素数さん mailto:sage [2011/01/02(日) 01:16:41 ] くいたい 73 名前：１３２人目の素数さん mailto:sage [2011/01/02(日) 02:37:57 ] eのe乗、πのπ乗、πのe乗が有理数でないことの証明をお願いします。 ウィキのゲルフォントの証明のページで、eのπ乗しか証明されておらず驚きました。 できないものなのでしょうか？ 74 名前：１３２人目の素数さん mailto:sage [2011/01/02(日) 11:19:17 ] ここ数論のスレじゃないから。 >>69-72みたいな話するところでもないけど。 75 名前：68 mailto:sage [2011/01/02(日) 11:45:49 ] 集合論とかの道具を使っていいのかってよりも、成り立たない場合をどう考えればいいのか、とか 正直よくわからないんだよねー。 あれから少しぐぐったところ完全性定理への選択公理の使用有無については >>63と同じ様なこと書いてあるサイト見つけたんだけど、 　ttp://ysserve.int-univ.com/Lecture/SymbolLogic/node42.html やっぱり冪集合公理や選択公理を使用してるのかしてないのか、成り立つとしていいのか ダメなのかについて理解が進展しないや。 76 名前：１３２人目の素数さん mailto:sage [2011/01/02(日) 15:27:50 ] そもそも無限公理は使って良いの？ 外延性公理は？ 77 名前：１３２人目の素数さん mailto:sage [2011/01/02(日) 19:44:58 ] 論理式を「実在するもの」と考えるのなら、構文論的に考察することにならない？ 述語論理の「意味」なんて考え出したら超越的議論が必要になるのは、感覚的に自然 78 名前：１３２人目の素数さん mailto:sage [2011/01/02(日) 22:32:30 ] >>76 少なくとも無矛盾性を問題にしているときに無限公理を疑うってのは極悪過ぎない？ >>77 論理式を実在物として構文論的に考察しているときのことを言ってるんだが。 「理論」の拡張時に無矛盾性を保ちながら極大集合を得る話でしょ。構文論だと認識してるが。 79 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 00:44:17 ] >>44 ＞公理的集合論は一階述語論理の上に定義されるから ＞"公理系"の"系"って公理的集合の一種にはなりませんよね？ 俺も初心者だけど まさに>>78の言うように「構文論的」に考察しているからこそ たとえ集合論が一階述語論理を用いて定義されていようが 「一階述語論理で記述された公理系の性質」について調べるときは 公理系を論理式の集合と考えて、集合論という道具を使って調べるんじゃないかな 80 名前：79 mailto:sage [2011/01/03(月) 00:59:47 ] >>79の最後が抜けてた だから公理系は公理的集合の一種になると思う 81 名前：79 mailto:sage [2011/01/03(月) 01:37:26 ] ごめん>>80はちょっといろいろ言い切りすぎてるか 「一階述語論理の公理系がなにがしかの性質をもつことを、厳密に示す場合」には 公理系を集合とみなして、集合論を道具として使って議論を進めて その集合論に基づく議論によって得られた結果をもってして 「一階述語論理の公理系はこれこれの性質をもつことが示された」 と考えるんだと思う。 あと、もちろん、その超数学的議論の中では その発想のおおもとや意味が有限的なものではない 集合論のいろいろな公理とか、モデルや解釈や それを集めるとか一つ選ぶとかいった概念が登場するけど それは普通は問題とは考えない。 ・・・あれ、なんだろ なんか今になって急に恥ずかしくなってきた もしかして俺、場違い？ 82 名前：79 mailto:sage [2011/01/03(月) 02:11:44 ] ありゃ >>52からの流れで >>56みたいな疑問が出てきて さらに>>64の論点も追加で出てきて 本当に集合論？という話になってるのか すいません場違いでした 83 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 02:18:47 ] 極大イデアルの存在を言うために選択公理を使うのは抵抗ないのに 極大無矛盾理論のときはなんかひっかかる 考えてみればおかしな話だ 84 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 02:32:38 ] 公理的集合論を組み立てていくときに 述語論理の完全性だとか、極大無矛盾理論の存在だとかは 無関係、必要ない情報なんじゃないかと思うのだけど そうして、既に組み立てられた公理的集合論を用いて、 「論理式からなる集合」について一層詳しい性質を調べることは 別におかしくない 85 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 09:50:46 ] おはよう。 誰が誰やらわからんけど、>>82の言うとおりの流れだと思ってる。 >>84の >公理的集合論を組み立てていくときに・・・必要ない情報 も、必要な部分だけつまみ食いすればいいだけという意味であってると思うが、 論理式の集合がZFCのモデルになっていると素直には認められないんで、その点で いろんな立場があり得るんじゃないかと考えてる。 またその流れで>>62の疑問も出てきてる。 86 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 13:04:25 ] 無限公理を疑うのは極悪過ぎる（？）、だから認めて良い、とか 理屈になってないと思うんだけど…… だいたい「論理式の集合がZFCのモデルになっている」 ってどういう意味で言ってるんだろうか。普通こういう言い方はしないと思うけどなあ。 論理式の集合が即理論のモデルになるわけじゃなくて 論理式の無矛盾な極大集合を一つ取って、そいつが持ってる情報から モデルを組み立てる、ということをやってるだけなんだけど。 87 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 13:48:48 ] >>86 無限集合の存在を認めて初めて理論の無矛盾性を問題にできるんだから、 理論の無矛盾性を問題にしておきながら無限集合の存在は認めません、という態度は 話にならないと思ったんだが。 論理式の無矛盾な極大集合を一つ取るってことがどうして可能になるの？ 論理式の集合がZFCのモデルになってると考えてるからでは？ 88 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 13:52:14 ] ＞「論理式の集合がZFCのモデルになっている」 完全性定理の証明の過程で、 一階理論（これはZFCを特別な場合として含む）のモデルの存在を示す ことを指していると推測 >>86に加えて言うと、 モデルを組み立てられるのは、元々の理論が無矛盾という仮定の下での話 ZFCが本当に無矛盾かどうかは未だに不明 ＞論理式の集合がZFCのモデルになっていると素直には認められないんで これを認めるのは、ZFCが無矛盾であると認めるのと同じこと 89 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 15:31:10 ] 無矛盾ってのはφ ∧ not φがどちらとも証明できてしまうようなことが起きない、 ということなのだから、構文論的にはある記号変形手続きが存在しないことで、 すべての自然数が〜〜を満たさない、程度のことは扱える必要があるけど 無限集合を扱う必要はないと思うけど。 だいたい完全性定理を前提にしない限り、モデルと無矛盾性は直接関係無い。 とりあえず完全性定理の証明を良く読んで 自分で証明を再構成できるようになるのが一番の近道な気が 90 名前：イスラエルの数学 [2011/01/03(月) 16:23:33 ] サラハやシュピロなどによる、 数理論理学・集合論的位相空間論・無限組み合わせ論や保型関数論などの発達が近年目覚しいが、 なぜかまったく話題にならない数学世界。 91 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 16:42:29 ] 保型関数論がどうしてそこに付いてるのか良く分からん 92 名前：イスラエルの数学 [2011/01/03(月) 17:02:56 ] シュピロの保型関数研究は有名ですが。 いずれにしろシェラハに全く言及できていない時点で 日本数学界の世界数学からの取り残され感がするのですが。 93 名前：イスラエルの数学 mailto:sage [2011/01/03(月) 17:08:14 ] そもそもシェラハのやっている数学を理解できている人間が日本にいるのだろうか。 いまだにグロタンディークで盛り上がるような世界では Ω-logicもpcf-thoryも知られていないでしょうが・・・。 94 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 17:58:45 ] >>89 論理式の長さやその総数に制約を付けないという前提で A ∧ not Aの証明があるか、ないか を問題にしてるんですよね？ 論理式や証明というものが無限にある、という主張などいちいちせずとも構文論的な考察はできる というのが「無限集合を扱う必要はない」という意味でしょうか？ >>88 中段と後段はわかります。なので 「論理式の集合がZFCのモデルになってると証明できない（←当然だが）だけでなく、 モデルになっていないと感じている」 ぐらいの言い方に変更します。 95 名前：79 mailto:sage [2011/01/03(月) 19:57:46 ] すいません 流れが読めてないついでにもうちょっと聞いてみたいんですけど >>56 = >>88 さんの主張は 「閉論理式の集まりは，ZFCで集合として取り扱えるものではない」 あるいは 「極大無矛盾集合の構成には，ZFCでは許されていない操作が含まれている」 ということなんでしょうか？ それとも 「完全性定理の証明にはなんらかの超越的な公理が必要だが それはかくかくしかじかの点で問題がある」 ということなんでしょうか？ 96 名前：１３２人目の素数さん mailto:sage [2011/01/03(月) 21:44:30 ] >>95 まず>>56 ≠ >>88 なんだけど、自分の主張は 「閉論理式の集まりは，ZFCで集合として取り扱えるものではない」 が一番近いと思う。>>85もそういう気持ちで書いている。 だけど、逆（モデルになっている）の捉え方をされていたかも。（>>86とか>>88とか） 97 名前：79 mailto:sage [2011/01/03(月) 22:34:08 ] >>96 56 = 87 と書くつもりが間違えました．ごめんなさい． ＞「閉論理式の集まりは，ZFCで集合として取り扱えるものではない」 ＞が一番近いと思う。>>85もそういう気持ちで書いている。 近い，とは・・・？ 98 名前：１３２人目の素数さん mailto:sage [2011/01/04(火) 00:10:09 ] ＞「閉論理式の集まりは，ZFCで集合として取り扱えるものではない」 ZFCの枠組みの中で、帰納的に定義された集合について調べよう。その集合はたまたまZFCの公理系と読めるものだ。 というだけの話では？ ZFCに用意された記号、論理式をZFCの考察の対象とすることに 自己言及のような気持ち悪さを感じているのだろうか。 はたまた、さらにそこから新しい記号を導入して、元のZFCから拡張されてしまうことになるから、 拡張された体系は一体何物なんだ、ということか。 そうではなくて、例えば… 自然数1を¬　自然数3を⇒　自然数5を∀ 自然数8n+7を関数記号f_n 等とみなして、これら自然数の（帰納的に定義された）特定の列からなる集合を考える。 ということ。 自己言及ではない。 見当違いの指摘だったらｽﾏｿ 99 名前：１３２人目の素数さん mailto:sage [2011/01/04(火) 00:11:55 ] >>97 とは・・・？　って聞かれても．．． ただ素朴なモノの集まりとしてみた場合に、集合論が成り立ってる気が全然しないというだけ。 ベキ集合の公理とか、選択公理とか。 100 名前：99 mailto:sage [2011/01/04(火) 00:21:11 ] >>98 すれ違いになっちゃったけど・・・ > 記号、論理式をZFCの考察の対象とすること これ自体は何の違和感も感じてないつもり。 ZFCを拡張してるなんてことも思ってないです。 ごめんなさい。何か決定的な勘違いしてるんじゃないかと不安になってきた。 101 名前：１３２人目の素数さん mailto:sage [2011/01/04(火) 03:46:53 ] >>93 何年か前の数セミでも、PCFは紹介されてた。 102 名前：１３２人目の素数さん mailto:sage [2011/01/04(火) 09:17:07 ] 論理式の集まり F があったときにその冪集合の元は別に論理式じゃないんだから 論理式の全体の中でいくら探してもその中に F の冪集合なんか無い訳だけど、 当然の話だし、何も問題ないと思うけどなあ。 論理式の集まりがZFCのモデルになるんじゃなくて ZFC（のモデル）が論理式を扱える、というだけでしょ。 だからZFCの方に論理式を素朴に扱う上で必要の無い余計な公理 がちょっと位付いててもそんなに大きな問題は無いと思うんだけど。 103 名前：ノニ [2011/01/04(火) 17:49:14 ] >>101 そうでしたか。 日本でシェラハがここまで無視されているのは、 なぜなんでしょうか。 104 名前：ノニ [2011/01/04(火) 17:57:07 ] >>102 一見したところ、それが正しい理解のようでした。 自身をもって結構ですよ。 確かにZFCのモデルは論理式を扱えますが、 それが２階の述語論理に基づくものだということを確かめてくださいね。 バベルの図書館的宇宙はモデルより先にあるのですから。 105 名前：１３２人目の素数さん mailto:sage [2011/01/04(火) 19:10:45 ] うっせ帰れ 106 名前：猫は作業 ◆MuKUnGPXAY mailto:age [2011/01/04(火) 19:42:51 ] >>105 まあエエがな。ソレともワシがアンタの相手をスルかァ！ 猫 107 名前：99 mailto:sage [2011/01/04(火) 21:53:52 ] >>102 もともとは完全性定理の証明に超越的な方法が使われているかどうかが 問題だったのに、ZFCのモデルなどという話にしちゃったのは申し訳ないです。 冪集合のこともおっしゃる通り。 で、>ZFC（のモデル）が論理式を扱える　ってとこだけど、論理式を素朴に扱う上で 必要の「ある」公理って何を指してますか？ 冪集合公理は関係ないとしても、選択公理がそこに含まれるかどうかが最初の疑問 だったわけですが、そこらへんは>>64あたりから前に進めていない気がする。 >>83 環とかは最初から（集合論でいうところの）"集合"として考えるわけで、構成手続きを経て文字から 組み立てられる具体的な論理式は同次元に捉えられないです。 それに極大イデアルの存在は選択公理に依存している、と言うとみんな「その通り」と返してくると思うけど、 極大無矛盾理論のときはそういうすっきりした回答が無いのでは？

---

---

[ 続きを読む ] / [ 携帯版 ]

read.cgi ver5.27 [feat.BBS2 +1.6] / e.0.2 (02/09/03) / eucaly.net products.
担当:undef