基礎論なぜなにスレッド その{φ,{φ},{φ,{φ}}}

1 名前：１３２人目の素数さん mailto:sage [03/01/20 16:53] ちょと見ない間に前スレ消えちゃったので新スレ立てます。 基礎論なぜなにスレッド cheese.2ch.net/math/kako/970/970523340.html 基礎論なぜなにスレッド その{φ,{φ}} science.2ch.net/test/read.cgi/math/1014140987/l50(dat落ち) 数理論理学　基礎 science.2ch.net/test/read.cgi/math/1035210795/l50 フォン・ノイマンVSアラン・チューリング science.2ch.net/test/read.cgi/math/1009039204/l50 91 名前：１３２人目の素数さん mailto:sage [03/03/02 22:04] >>89 世代の問題ではなく、一階述語論理上の公理系として 考えることが、数学としての成果を上げるのに好都合 だからだろう。 >>90 高階だから、ではなく、形式系だから、ということ。 高橋氏も新井氏もPrawitzもHenkinも、その結果が 「本来の二階論理」のものではないことは分かって いるはず。又、本来の二階論理が形式的に取り扱えない からといって、それを無視してよいことにはならない。 現に>>79は、standard modelといっている。これは 本来の二階論理こそが数学を規定しているという意識 の現れである。 92 名前：１３２人目の素数さん mailto:sage [03/03/02 22:15] >>90 本来の二階論理を持ち出したからといって、 形式的な論証を超えた”魔術”があるとは 思わないでいただきたい。 そのような意図は毛頭ない。 93 名前：１３２人目の素数さん mailto:sage [03/03/02 22:17] 2階論理の証明論とモデル理論ではどちらが先にできたのですか？ 94 名前：１３２人目の素数さん mailto:sage [03/03/02 22:27] >>93 こう質問するべきでは？ 「論理は、形式系か？」 95 名前：１３２人目の素数さん mailto:sage [03/03/02 22:32] >>94の質問に、然り、と答える人にとって、 完全性定理とはどんな意味があるのだろう？ >>76のいう意味論的完全性は、論理の意味と 形式系を分けるからこそ問われることだろう。 96 名前：１３２人目の素数さん mailto:sage [03/03/02 22:35] 最初にニ階論理の形式系が考案されて、 それから本来の二階論理が考案されて、 それから本来の二階論理ではない二階論理の形式系に対する 完全なモデルの研究がなぜか続いてHenkinモデルが考案された ということでファイナルアンサー？ 97 名前：１３２人目の素数さん mailto:sage [03/03/02 22:43] >>96 最初に考えられたのは形式系ではないと思う。 98 名前：基礎論 mailto:sage [03/03/03 02:43] >>81 ありがとうございます。 Ｑ５については、意味が分かりにくかったと思うので書き直します。 「不完全性定理」 算術の標準モデルＮ＝（Ｎ，＋，・，Ｓ，０）をモデルにもつ再帰的に公理化可能な理論には、 証明も反証もできない文が存在する。 （証明論的に完全な理論ＴＡは存在するが、これは再帰的に公理化可能でない） と理解しています（おかしかったら指摘してください）。 ところで、 一階述語論理上で理論を展開する場合、 理論Ｔに証明も反証もできない文φが存在する ⇒φに異なる真理値を与えるＴのモデルが存在する （φがＴの全てのモデルで同じ真理値をとるなら、完全性定理によりφは証明可能か反証可能） ⇒Ｔには複数の（同型でない）モデルが存在する 99 名前：基礎論 mailto:sage [03/03/03 02:44] また、『数学基礎論講義』のＰ１８３には、 次のような第二不完全性定理を用いたＰＡの超準モデルの存在証明があります。 ＞[第二不完全性定理を用いた証明] ＞まず，ＮはＰＡのモデルなので，完全性定理からＰＡは無矛盾． ＞よって，ＰＡが無矛盾であることを意味する論理式Ｃｏｎ(PA)は正しい． ＞すなわちＮ|= Ｃｏｎ(PA)． ＞また，第二不完全性定理からＣｏｎ(PA)はＰＡから証明できない． ＞よってＰＡ＋¬Ｃｏｎ(PA)は無矛盾なのでモデルＭをもつ． ＞Ｍ|= ¬Ｃｏｎ(PA)なのでＭ≠Ｎ． ＞ゆえにＭはＰＡの超準モデル．□ (Ｑ５)以上のことから、不完全性定理はある意味でモデルの複数性を示唆しているともとれませんか？ (Ｑ６)他方、完全性定理の証明と本質的な部分を共有するレーヴェンハイム-スコーレムの定理も、 モデルの複数性を含意しているので、「モデルの複数性」という観点からは、 完全性定理と不完全性定理は意外に近い内容を含んでいるといえないでしょうか？ 100 名前：基礎論 mailto:sage [03/03/03 02:44] (Ｑ７)Henkin の general モデルでは、二階論理の意味論的完全性が証明されるということですが、 このときはやはり算術のモデルは範疇的ではなくなりますよね？ (Ｑ８)一階述語論理にとどまって算術の超準モデルを許容するか、 二階論理のstandard モデルをとって算術のモデルを範疇的にする代わりに 意味論的完全性を犠牲にするか、この選択に決め手はないですか？ また、実際の研究者はこれについてどう考えていますか？ (Ｑ９)『数学基礎論講義』によると、 Ｎ＝（Ｎ，＋，・，Ｓ，０） Ｎ上での正しい文全体から成る理論ＴＡは再帰的に公理化可能でないが証明論的完全性を満たす。 Ｎ’＝（Ｎ，＋，Ｓ，０） Ｎ’上での正しい文全体から成る理論ＴＡ’は再帰的に公理化可能で証明論的完全性を満たす。 ということですが、 ・Ｎ’をモデルとする自然数の体系に関して、不完全性定理の反証にあたる定理が証明されたんですか？ ・算術の標準モデルがＮ’ではなくＮでなければならないのはなぜですか？ ・Ｎ’について考える意義はあまりないんですか？ ・これらのことついて詳しく書いてある本はありますか？ 101 名前：１３２人目の素数さん mailto:sage [03/03/03 07:47] Ａ６　一階述語論理の上の自然数論の公理系を満足するモデルは多数あります。 近い遠いとか、意味する意味しないはナンセンスないいまわしでしょう。 Ａ７　generalモデルは、本来の二階論理のモデルではありません。 したがって、二階論理上の自然数論のgeneralモデルが 多数あったところで、本来の自然数論のモデル（これを standardモデルという）の範疇性には影響しません。 Ａ８　あなたはω矛盾する体系を許容できますか？ これは一階述語論理上で公理化する場合排除できません。 しかしながら二階論理ではこのようなことはおきません。 Ａ９　乗算がない場合には、決定手続きが存在することが 直接示されています。 それは、乗算のない体系では自身の証明可能性を 表す述語が表現できないことを意味します。 102 名前：１３２人目の素数さん mailto:sage [03/03/03 07:58] 「算術の標準モデルがＮ’ではなくＮでなければならないのはなぜですか？」 ＮとＮ’は異なる理論です。 つまり、Ｎで表現できるが、Ｎ’では表現できない命題があります。 答えとしてはこれで充分でしょう。 「Ｎ’について考える意義はあまりないんですか？」 あなたのいう”意義”が、Ｎ’がＮを代替する可能性を指すのであれば そのようなことはあり得ません。 「これらのことについて詳しく書いてある本はありますか？」 Ｎ’＝（Ｎ，＋，Ｓ，０）については田中一之氏の 「数の体系と超準モデル　Logic of Arithmetic −Formal Systems and Non-standard Models− 」 をご覧になられるのがよいでしょう。 www.shokabo.co.jp/mybooks/ISBN4-7853-1530-X.htm 数の体系と超準モデル Logic of Arithmetic −Formal Systems and Non-standard Models− www.shokabo.co.jp/mybooks/ISBN4-7853-1530-X.htm 103 名前：１３２人目の素数さん mailto:sage [03/03/04 01:05] >>91 ＞世代の問題ではなく、一階述語論理上の公理系として ＞考えることが、数学としての成果を上げるのに好都合 ＞だからだろう。 そればかりではなく、思想的な問題もあると思うわけさ。 歴史的にはクワインの存在論的テーゼがあるわけで、あのテーゼを 信じるものにとっては２階以上の述語論理には居心地の悪さを感じ るのは仕方ないだろ。 まあ、歴史の話じゃないのでどうでもいいといえばどうでもいいん だけど、今出回ってる教科書を書いた世代がどういう思想的な影響下に あったのか、っていうのは知ってて損はしないだろ。 104 名前：１３２人目の素数さん mailto:sage [03/03/04 01:16] >>93 歴史の話をすれば、まず最初はそういう区別はない。ラッセルやフレーゲ、 ウカシェビッツなどの当時の仕事を見ると、どっちに分類するか微妙な 仕事も多いが、基本的にはシンタクティカルな手法のものが多いだろう。 ２階の論理の誕生自体は、そもそも、述語論理の始祖であるフレーゲの著作 からして高階のシステムであったわけで、現代数理論理学の誕生とともに 生まれたといってもよいだろう。 今で言うモデル理論はゲーデルやタルスキの仕事の後に誕生するから、 順序で言えばモデル理論のが後。 105 名前：１３２人目の素数さん mailto:sage [03/03/04 01:22] ちらちらさんさくするに、 W ORKSHOP IN THE PHILOSOPHY OF MATHEMATICS Spring 2002 Neo-Logicism and Second-Order Logic なるものを発見。はやってるのか。面白そうだな。 106 名前：基礎論 mailto:sage [03/03/04 02:30] >>101-102 よくわかりました。 ありがとうございます。 ここからは、もう少し初等的で細かい点について質問をしてみます。 (Ｑ１) 算術の標準モデルについて、 Ｎ＝（Ｎ，＋，・，Ｓ，０） Ｎ＝（Ｎ，＋，・，０，１，＜） という２種類の書き方がされていることがありますが、この違いは何ですか？ (Ｑ２) 『数学基礎論講義』のＰ２４に、ある構造における０変数関数を定数と呼び、 ０項関係（述語）Ｒ＝{()}は真理値定数ＴまたはＦと見なせる と書いてありますが、通常の定数が０変数関数として、 Ｎ＝（Ｎ，＋，・，Ｓ，０）の「０」のように規定されるのに対して、 真理値定数Ｔ、Ｆはどのように規定されるのでしょうか？ 107 名前：１３２人目の素数さん mailto:sage [03/03/04 07:29] >>103 ＞そればかりではなく、思想的な問題もあると思うわけさ。 君は、数学者はクワインの存在論的相対性を支持していると 主張するのかい？ >>104 ＞歴史の話をすれば、まず最初はそういう区別はない。 （中略） ＞基本的にはシンタクティカルな手法のものが多いだろう。 しかし、シンタクスがセマンティクスを定めるという発想はなかった筈。 Henkinのモデル云々は、シンタクスに合わせたセマンティクスを考える 試みだが、それはフレーゲが意図したものではない。 ＞今で言うモデル理論はゲーデルやタルスキの仕事の後に誕生するから、 ＞順序で言えばモデル理論のが後。 それはモデル理論という名前がいつ現れたか、という話だろう？ しかし、セマンティクスという発想が無ければ、完全性定理もなかったし、 その前にレーヴェンハイム・スコーレムの結果もなかったんじゃないか？ 108 名前：１３２人目の素数さん mailto:sage [03/03/04 07:33] >>106 書かれていた本（多分、田中氏の「数学基礎論講義」と思われる）に 定義がある筈ですから、ご自分で読んで確かめてください。 　 109 名前：１３２人目の素数さん [03/03/04 12:47] >>107 ＞君は、数学者はクワインの存在論的相対性を支持していると ＞主張するのかい？ 論理と数学の線引きでクワインの議論に依拠して、二階以上の 高階論理を「数学」とする主張を何度か目にしてきたからね。 少なくとも高階論理があまり研究されなかったことはクワインの影響といえ ないのではなかろか、と思うんだよ。 110 名前：１３２人目の素数さん mailto:sage [03/03/04 13:15] >>109 ＞論理と数学の線引きでクワインの議論に依拠して、 ＞二階以上の高階論理を「数学」とする主張を ＞何度か目にしてきた でもそれは数学者の発言じゃないでしょ。 数理哲学者ならともかく ＞高階論理があまり研究されなかったことは ＞クワインの影響といえないのではなかろか クワインがそういったから、ではないと思うね。 クワインがいっているようなことが、理由の一つ だというならともかく 111 名前：１３２人目の素数さん mailto:sage [03/03/04 13:16] >>107 ＞しかし、シンタクスがセマンティクスを定めるという発想はなかった筈。 ないと思う。意味の自然な形式的記述としてシンタクスがあるとしていると 考えられる。 ＞Henkinのモデル云々は、シンタクスに合わせたセマンティクスを考える ＞試みだが、それはフレーゲが意図したものではない。 大ざっぱに言って、フレーゲにとって正しい「意味」は複数あってはならず、 その「意味」を規定するモデルが複数あるとか、モデルを構築するという発想はそもそもなかったと 思う。この発想は、初期ラッセルも共有してるだろう。ただ、ウカシェビッツに 関してはわかんない。 ところで、モデルの複数性、モデルを構築するという発想は、ゲーデルやカルマールが 完全性定理を証明している時点でもまだ存在しないという印象なんだが、 どう思う？ 112 名前：１３２人目の素数さん mailto:sage [03/03/04 13:22] >>111 スコーレムの仕事は、モデルを構築する発想のものだと思う。 そして、彼の逆理は、モデルの唯一性に対する異議とも考えられる。 113 名前：基礎論 mailto:sage [03/03/04 16:24] >>108 よく読んでみたんですけど、それ以上のことは書いてなかったです。 述語論理における「真理値定数」を０項関係{()}と見なすということについて、 それを理論上、具体的にどう扱っているのか、誰か知っている人はいませんか？ 114 名前：１３２人目の素数さん [03/03/05 00:04] >>110 ＞でもそれは数学者の発言じゃないでしょ。 ＞数理哲学者ならともかく 現状ならともかく、WW2 前後から60年代の状況ではそのわけ方に あまり意味はないような気もするな。 まあ、ぱっと調べても、ソースを吉田夏彦の著作ぐらいしか出せなかっ たので今はこれ以上しつこく主張するのはやめとくよ（笑。無理筋の議論して 「基礎論」氏の勉強の邪魔するのもあれだし。 115 名前：１３２人目の素数さん mailto:sage [03/03/05 00:11] >>112 歴史的な事実はちょっと違うのではないかな？ スコーレムは、集合論が数学の基礎として不適切であることを 示すためにあの定理を示したのだから。つまり、あのような 複数の解釈を持ってしまうことはよろしくないと考えていたので はないかと思うわけで。 少なくともスコーレムはモデルの複数性を許容してないと思うんだが。 116 名前：基礎論 mailto:sage [03/03/05 00:46] 再帰的（recursive）な関係と 再帰的に枚挙可能（recursively enumerable）な関係 という２つの概念を置く意義がいまいち分かりません。 117 名前：１３２人目の素数さん mailto:sage [03/03/05 08:03] >>114 ＞現状ならともかく、WW2 前後から60年代の状況では ＞そのわけ方にあまり意味はないような気もするな。 B.C.(Before Cohen)の話をしても仕方ないな。 例えば、Cohenのforcingは、Quineの見解の反映ってことかい？ それはいくらなんでも無理筋だろう。 >>115 スコーレムの思惑とは無関係に、結果は形式系が複数の解釈を 持ち得ることを示していることは貴方も否定できない筈だが。 118 名前：１３２人目の素数さん mailto:sage [03/03/05 08:05] >>116 単純に定義を知らないか、よく読んでいないために 区別できていないと思われるので、定義を読みなおして ください。定義なら岩波数学辞典にも載ってますよね。 119 名前：１３２人目の素数さん mailto:sage [03/03/05 11:04] >>117 無理筋のほうはお手上げだね（笑）この話はやめよう（笑） モデル理論的な手法の話は数学史的な話題だよ。最初からこっちは 歴史の話だって断ってあるだろ？ 歴史の話を考える場合には、その当時の証明者の思惑を無視する わけにはいかない。現代の我々は、あの定理が形式系が複数の解釈 を持ちうることを示す肯定的な結果であると捕らえるが、 スコーレムは当時の形式的な研究が不適切であることを示す否定的な 結果であるとしていたわけで、この差異は重要だと思うが？ 「いつから我々のような定理解釈が主流になったのか？」が問題なのだよ。 当時からじゃないとおもわない？ ゲーデルBBSでふったほうがいいかなこの話題は。 120 名前：１３２人目の素数さん mailto:sage [03/03/05 12:05] >>119 ＞無理筋のほうはお手上げだね（笑）この話はやめよう（笑） そうそう、Quineを持ち出すべきではなかったね。 ＞モデル理論的な手法の話は数学史的な話題だよ。 ＞最初からこっちは歴史の話だって断ってあるだろ？ 君のいう歴史とは、モデル理論という言葉が 文献に用いられた時期を特定することかな？ しかし、 ＞その当時の証明者の思惑を無視するわけにはいかない。 というなら、それ以前についても考えるということだね。 121 名前：１３２人目の素数さん mailto:sage [03/03/05 12:10] ＞現代の我々は、あの定理が ＞形式系が複数の解釈を持ちうること ＞を示す肯定的な結果であると捕らえるが、 ＞スコーレムは ＞当時の形式的な研究が不適切であること ＞を示す否定的な結果であるとしていたわけで、 スコーレムが、形式系の研究は不適切、とした理由は 形式系が意図された意味をもつとは限らない、と 分かったからだろう。 それなら、我々とスコーレムの間に差異はない。 122 名前：１３２人目の素数さん mailto:sage [03/03/05 12:16] ＞「いつから我々のような定理解釈が主流になったのか？」 ＞が問題なのだよ。 君がどのように定理を解釈しているのか明らかでないが、 形式系に基づく証明によって定理と考えるということかい？ 123 名前：基礎論 mailto:sage [03/03/06 00:14] 再帰的（recursive）な関係Ｒは χ_R(x_1,…x_n)＝ １：Ｒ(x_1,…x_n)のとき ０：そうでないとき となる特性関数χ_R：Ｎ＾n → {0,1}が再帰的になるもので、 再帰的に枚挙可能（recursively enumerable）な関係Ｒは ｆ(x_1,…x_n)＝ １：Ｒ(x_1,…x_n)のとき 未定義：そうでないとき となる部分関数ｆ が再帰的になるものという定義は分かるんですけど、 Ｒ(x_1,…x_n)でないときを０とするか未定義とするかの違いに どういう意味があるのかがよく分かりません。 124 名前：基礎論 [03/03/06 00:21] 理論ＴのΣ_1（シグマワン）論理式とΠ_1（パイワン）論理式の定義は分かったんですけど、 Σ_1論理式でもΠ_1論理式でもない論理式ってあるんですか？ 125 名前：１３２人目の素数さん mailto:sage [03/03/06 00:47] >>121 > スコーレムが、形式系の研究は不適切、とした理由は > 形式系が意図された意味をもつとは限らない、と > 分かったからだろう。 歴史の話でひっぱっちゃって恐縮ですが、スコーレムがそう考えて いたという話には興味あるので（というか今やらされてる仕事で結構 重要になりそうなので）、ソースをお教えいただけませんか。 126 名前：１３２人目の素数さん mailto:sage [03/03/06 05:49] >>125 もう読まれたかもしれませんが、 P. Benacerraf, "Skolem and the skeptic," Proceedings of the Aristotelian Society, Suppl, 59, 1985, pp.85-115. あたりは参考になるかも。 127 名前：１３２人目の素数さん mailto:sage [03/03/06 06:09] >>121 ＞それなら、我々とスコーレムの間に差異はない。 うーん。彼はその結果を受けて constructivism に傾斜したんじゃなかったっけ？ 我々はそうではないのだから「差異はない」というのはどうかなあ。 128 名前：１３２人目の素数さん mailto:sage [03/03/06 06:53] >>113 106 の Q1: この２つの場合定義可能な Nx...xN の部分集合全体は変わらない。 ただ、例えば {(x,y):x<y } は下の場合、量化子なしに定義可能だが上の場合 そうではない。例えば、このようなことを証明することをしようとすれば 非常によくわかるようになる。 116, 123, 124 も定義の違いを形式的にしかとらえていないから起こること である。その定義の関係した定理の内容とともに定義を理解することをこころ がけてください。定義を見ただけで定義をわかったという人は、字が読める といっているに過ぎない。定理は原理的には論理的帰結に過ぎないのだから。 蛇足ですが、最後のことがよく理解できるために 124 について。２種類の 量化子が沢山ついた論理式は 124 にある定義のどちらを満たすのですか？ つまり、124 の質問は論理式の定義や Π_1 ,Σ_1 の定義がわかっていない といっていることと同じように見えます。 129 名前：１３２人目の素数さん mailto:sage [03/03/06 07:49] >>125　スコーレムのパラドックス >>126　ベナセラフは読んでいない >>127　>>122に答えてくれるかな？ それから君だけの考えを「我々」というのはいけないな。 130 名前：１３２人目の素数さん mailto:sage [03/03/06 08:03] >>123 関数と部分関数の区別が分かってないんじゃない？ 関数といったら、定義域全域で、値が決まっているもの。 部分関数は、そうではないよね。 これで、０と未定義の違いは分かったかい？ 131 名前：1億円ください mailto:sage [03/03/06 08:03] 議論が錯綜してきたので仮こてをつけよう。 >>129 >>122 ？ Skolem's paradox を君も僕も paradox とは考えていないということ。 君はあれを paradox とは思っていないだろ？じゃあ「我々」でかまわないわけだ。 132 名前：1億円ください mailto:sage [03/03/06 08:08] >>125 ネット上で、 www.hf.uio.no/filosofi/njpl/vol1no2/howlogic/eklund-html.html www.hf.uio.no/filosofi/njpl/vol1no2/pioneer/jervell-html.html なんてのもありますね。まだ読んでないですが（笑 133 名前：１３２人目の素数さん mailto:sage [03/03/06 09:01] >>131 所謂paradoxだとはいっていないよ。 しかし、ここでいってるのはそんな表面の話ではないだろう。 134 名前：125 mailto:sage [03/03/06 11:52] >>126 どうもありがとうございます。何の因果かスコーレムを歴史的に研究する 用事ができたもので、スコーレム自身が>>121のようなことを言っているの ならおさえておかなくてはならず・・・。2次文献にももう少しあたってみます。 >>127 スコーレムの“パラドクス”を我々がそう解釈できる、ということから我々の （あるいはあなただけの）考えを「スコーレムの」というのはいけないと思い ます。特に歴史的研究ではそういうアナクロニズムは禁じ手ですので。 「歴史的研究なんてくだらないな」とおっしゃるでしょうけどね。私もできれば あまり関わりたくはないんですが。 135 名前：125 mailto:sage [03/03/06 11:54] すみません、134でのアンカー「127」は「>>129」の間違いでした。 >>132 これまたありがとうございます。 　　　As Paul Benacerraf has argued, Skolem argued that because of the 　　　Lowenheim-Skolem theorem, set-theoretic notions cannot be captured 　　　within any formal system; but they are perfectly well understood within 　　　informal language. And since Skolem's metalanguage is informal it 　　　seems that in so far as one can speak of its underlying logic, its 　　　underlying logic must not have the Lowenheim-Skolem property. 　　　Needless to say, Skolem neither had the concept of a metalanguage 　　　nor that of the underlying logic of a language. Often the metalanguage 　　　is left informal also today, and I would think that it is an open question 　　　with what right one may speak of the underlying logic of an informal 　　　language. なんて記述もありますね。>>125さんのおっしゃる通り、やはりベナセラフに あたる必要があるようです。 この記述だけ見ていると、形式体系でスコーレムの定理が成り立つからと いって、すぐに「だからモデル理論で」という考えをスコーレムに帰属させる のは、形式体系とモデルという2分法に慣れ過ぎた人のアナクロニズムだと 思えますが・・・。 ところでどなたが>>121さんなんですか？ 136 名前：基礎論 mailto:sage [03/03/06 16:26] >>128 ありがとうございます。 Π_1 ,Σ_1 について考えてみました。 Σ_1論理式でもΠ_1論理式でもない論理式の例とは、 ∀x∃yΣ_1¬(x+y=0) のようなものでしょうか？ 再帰的（recursive）な関係と 再帰的に枚挙可能（recursively enumerable）な関係 については、クリーネの標準形定理やパラメタ定理、再帰定理など、 関連する定理のチューリング機械のモデルを用いた証明の粗筋を読んでみたんですけど、 そもそもそういう概念の区別をする必要性がどこにあるのか分からないので、 いまいちしっくり掴めない感じでした。 137 名前：基礎論 mailto:sage [03/03/06 16:35] >>130 その違いは分かったんですけど、 帰納的関数に対して帰納的部分関数を持ち出す理由が、 最小化の関数 ｆ(x_1,…,x_n)＝μy（ｇ(x_1,…,x_n,y)＝０） についての、 ∀x_1…∀x_n∃yｇ(x_1,…,x_n,y)＝０ という条件を取り除くことにあるということですけど、 その必要性というか目的がよく分かりません。 138 名前：１３２人目の素数さん mailto:sage [03/03/06 18:10] >>134 解釈なんてないよ。それから自分の考えを我々というのは禁じ手だよ。 歴史とは関係なく、自分の主張の責任は自分だけで引き受けるべきだよ。 >>135 「形式体系でスコーレムの定理が成り立つ」 という言い方は数学として誤り。 139 名前：１３２人目の素数さん mailto:sage [03/03/06 18:16] ベナセラフは 「スコーレムは集合論は、形式化できない、非形式的なものだ」 といってるじゃない。 140 名前：１３２人目の素数さん mailto:sage [03/03/06 21:56] >>138 130 さんではないのですが。 ∀x_1…∀x_n∃yｇ(x_1,…,x_n,y)＝０という条件の成立がどうして わかるのか？という点こそが帰納関数定義で超越的なところで、これ がアルゴリズムの存在と計算可能性が同値だということが一致して いるという Church's Thesis が必ずしも認めにくいところと関係 していると思うので大切な点にたどりついているのでしょう。 その条件はデータにたいしてコンピューターが止まるかどうかという 問題が一般には recursive ではないが recursive enumerable である ということに直接つながるので、他の質問も含めてわかるようになる ところなので集中して勉強してわかるようにしてください。 141 名前：１３２人目の素数さん mailto:sage [03/03/07 02:11] >>138 ＞自分の主張の責任は自分だけで引き受けるべきだよ。 結構ナイスなジョークだね。 142 名前：1億円ください mailto:sage [03/03/07 03:18] >>131 じゃあ、こうしよう。 「モデル理論」の成立に、少なくともメタ論理の概念は必要条件と考える。 こう考えた場合、Skolem はその概念を持っていないというのが定説なので、 Skolem の段階では、「モデル理論にとって先駆的な仕事がなされているが、 モデル理論はいまだ確立していない」という結論になる。 ここで設定した必要条件を認めないというなら、それは見解の相違という ことになるね。 143 名前：１３２人目の素数さん mailto:sage [03/03/07 11:41] >>142 ＞「モデル理論」の成立に、少なくともメタ論理の概念は必要条件と考える。 ＞こう考えた場合、Skolem はその概念を持っていないというのが定説なので、 意味不明の主張をして、それが定説だといっても無意味だよ。 見解の相違というよりも、>>142の理解に問題があるということだね。 144 名前：１３２人目の素数さん mailto:sage [03/03/07 11:50] >>143の補足 ゲーデルの完全性定理は、実質的にはスコーレムによって 得られていたが、スコーレムが完全性定理に気づかなかった のは、形式的体系及び証明を明確に意識していなかったせい だといわれている。また、エルブランも完全性定理に肉薄 していたが、この場合には、証明の有限な手続きにこだわって 今で云うモデルの考えに気づいていなかったために、そこに たどり着けなかったといわれている。 145 名前：1億円ください mailto:sage [03/03/07 12:28] >>143 「メタ論理」ではなく、「メタ言語」な。 146 名前：125 mailto:sage [03/03/07 12:44] >>142でおっしゃるように、スコーレムがメタ言語の概念を持っていないと いうのはほとんど定説ですよ。>>135で引用した文にも 　　　Needless to say, Skolem neither had the concept of a metalanguage 　　　nor that of the underlying logic of a language. とあるでしょう。「言うまでもないこと」だそうですね。 147 名前：１３２人目の素数さん mailto:sage [03/03/07 13:51] >>146 君は>>135を読まずに書き写したわけではないよね？ 　And since Skolem's metalanguage is informal it seems that 　in so far as one can speak of its underlying logic, its 　underlying logic must not have the Lowenheim-Skolem property. これは>>121と同じだってことが君には読めないかな？ 148 名前：１３２人目の素数さん mailto:sage [03/03/07 14:00] ところで、125氏も>>142氏も、自分に都合のよい文章だけ 読んではいけないな。それでは歴史研究にならない。 149 名前：１３２人目の素数さん mailto:sage [03/03/07 14:10] >>137,>>140 ∀x_1…∀x_n∃yｇ(x_1,…,x_n,y)＝０という条件がないってことは、 あるx_1…x_nでは、ｇ(x_1,…,x_n,y)＝０となるｙがないってことだよね。 そういう場合、ｆ(x_1,…,x_n)＝μy（ｇ(x_1,…,x_n,y)＝０）は 値が未定義ってことなんだよ。 ざっくばらんにいえばｇ(x_1,…,x_n,y)＝０となるｙを 探しに行ったまま戻ってこなくなるということ。 150 名前：１３２人目の素数さん mailto:sage [03/03/07 16:27] >>137 140で「同値だということが」が余分になって文章が変なので訂正します。 部分帰納関数を導入する意味は、枚挙可能定理にあります。これは�農1 述語の枚挙定理と同等のもんです。これを帰納関数だけの族に限ると 帰納関数によって枚挙できないので、部分帰納関数の族は枚挙の意味で 閉じているという意味でも導入する意味があるのではないでしょうか？ 151 名前：125 mailto:sage [03/03/07 16:44] >>147 >>121は > スコーレムが、形式系の研究は不適切、とした理由は > 形式系が意図された意味をもつとは限らない、と > 分かったからだろう。 と述べた後で、 > それなら、我々とスコーレムの間に差異はない。 と結論していますね。 ところが一方、147の引用文の直後では、「スコーレムはメタ言語の概念を 持っていなかった」という、我々とスコーレムの間の差異の具体例が挙げ られていますよね。121と147の引用文とが本当に同じことを言っているなら 我々とスコーレムの間に差異はないはずなんですが。 152 名前：基礎論 mailto:sage [03/03/07 18:03] >>140 >>149 わかりました。この辺りのことをもう少し詳しく知りたいんですけど、 田中さん編の『数学基礎論講義』では簡単に纏められすぎててちょっと難しいし、 前原さんの『数学基礎論入門』にはそこまでの内容には触れられてないので、 何かいい本はありませんか？洋書じゃないとだめですか？ >>150 全域的な部分帰納関数が帰納関数になるので、 ｎ変数の任意の帰納関数は、ｎ＋１変数の具体的な部分帰納関数で 枚挙できるということでしょうか？ この場合、枚挙するｎ＋１変数の部分帰納関数は必ずしも全域的にならないということですか？ 153 名前：基礎論 mailto:sage [03/03/07 18:50] あと少し気になったんですけど、 第一不完全性定理はロビンソン算術Ｑを含む全ての理論では、 >>76に書いた証明論的完全性を持ちえず、 Ｑを含まない理論で、Ｎ’＝（Ｎ，＋，Ｓ，０）のような算術モデルの命題を 全て表現する完全な理論（プレスバーガー算術？）なら存在するということだったと思いますが、 Ｑを含まずに、算術の標準モデルＮ＝（Ｎ，＋，・，Ｓ，０） での全ての命題を表現できる完全な理論が存在しないことは厳密に証明されているんですか？ 154 名前：１３２人目の素数さん mailto:sage [03/03/07 21:36] >>152 部分帰納関数の件はよく解釈すればそんとおりです。ただ多少心配も ありますがこれ以上は掲示板では無理。153のなかの表現でも「、、、モデル の命題をすべて表現する完全な理論」というものがありますが正確な表現 をしないとなんだかわかりません。また数学の証明という言葉に厳密という 形容詞をつける人は数学を理解する態度となっていないといわれます。 155 名前：１３２人目の素数さん mailto:sage [03/03/07 22:09] >>151 ＞一方、147の引用文の直後では、 ＞「スコーレムはメタ言語の概念を持っていなかった」という、 ＞我々とスコーレムの間の差異の具体例が挙げられていますよね。 自分一人の考えに、我々という二人以上の人を想定した 主語を用いるべきではないね。 それはともかく、何がどう差異だと君は思っているんだい？ それをはっきりと口にしてごらんよ。 156 名前：１３２人目の素数さん mailto:sage [03/03/07 22:14] ＞Ｑを含まずに、算術の標準モデルＮ＝（Ｎ，＋，・，Ｓ，０） 算術の標準モデルＮ＝（Ｎ，＋，・，Ｓ，０）はＱを含むんじゃないのかい？ 157 名前：１３２人目の素数さん [03/03/08 01:12] 155はメタ言語の概念を持ってないらしいぞ 158 名前：１３２人目の素数さん mailto:sage [03/03/08 01:22] >>155は>>151の > 「スコーレムはメタ言語の概念を持っていなかった」という、 > 我々とスコーレムの間の差異の具体例 を256回読み直してから「メタ言語」と1024回叫んだ後 生命保険に入り回線で首を吊って1億円捻出するのがいいと思う 159 名前：１３２人目の素数さん mailto:sage [03/03/08 02:39] >>144 Skolem は10年代後半から20年代前半、Herbrand は20年代後半から30年代前半。 時期が少々違う。 問題となる論文は、Skolem は1920と1922、Herbrand は確か1930。 160 名前：１３２人目の素数さん mailto:sage [03/03/08 10:17] >>157-158 >>151はただメタ言語という文字列を呪文かなにかのように 有難がっているように見えるなあ。それって学問じゃないよね。 一億円が欲しいんなら、働いたら？ 161 名前：１３２人目の素数さん mailto:sage [03/03/08 11:22] >>160 >>138 162 名前：1億円ください mailto:sage [03/03/08 11:41] >>160 ＞一億円が欲しいんなら、働いたら いや、前原スレで1億円くれるといっている人と君は別人なんだろ？ 何で気にする必要があるの？？ そいつに、>>138 みたいなことを びしっといってあげてくらさい。 163 名前：１３２人目の素数さん mailto:sage [03/03/08 14:10] >>162 ここは前原スレじゃないよ。君が一億円をくれといってる人かどうか 僕には分からないけど、ここの議論とは関係ないよ。 それより、君のいうメタ言語とはなにかちゃんと説明したらどう？ >>138は 「「形式体系でスコーレムの定理が成り立つ」 　という言い方は数学として誤り。」 といってるけど、それは君にも正しいと分かるよね。 164 名前：１３２人目の素数さん mailto:sage [03/03/08 19:32] YahooBBの規制が解除されたせいで、論理関係のスレが再び荒れはじめました。 わかりやすいですね 165 名前：１３２人目の素数さん mailto:sage [03/03/08 23:09] >>147 >>148 166 名前：１３２人目の素数さん mailto:sage [03/03/09 01:22] >>164 YahooBB？？関係ないでしょ。ご存じないのでしょうか？ 基礎論関係のスレッドが荒れるのは YahooBB 以前からの問題で、 2ch どころか、インターネットがまだ一般的でない時代から ずーっと続いていることです。 167 名前：164 mailto:sage [03/03/09 02:19] そっち（NGとか）じゃなくて「最近の2ch数学板の基礎論系スレ」についての考察でつ まあマターリといきましょうよ、みなさん・・・ 168 名前：加護天使 ◆j/LLggzims mailto:sage [03/03/09 02:29] スレが荒れるのも、ＮＧが荒れるのも、 ぜんぶ、日本での数学基礎論をめぐるデフレスパイラルが悪いのだ。 ということでここはまったりと、、。 169 名前：１３２人目の素数さん mailto:sage [03/03/09 02:33] >>167 それでも過去スレ読み返すとわかりますが、しょっちゅう荒れてますが。 >>168 そうですね。 170 名前：１３２人目の素数さん mailto:sage [03/03/09 13:21] >>125がいいたいのは、モデルを考える場合に、 一階述語論理の公理系で満足されるようなもの だけに限定する、という考え方は、スコーレム も、ゲーデルもしていないってことかな？ 171 名前：基礎論 mailto:sage [03/03/09 22:24] >>154 >>156 すみません。カン違いから無意味な質問をしてしまいました。 自然数上の述語を「意味すること」と「表現すること」を次のように整理してみました。 ＜自然数上のｋ項関係（述語）Ｒ(n_1,…,n_k)がＴにおいて意味されることの可能性＞ ・Ｒ(n_1,…,n_k)が成り立つ　⇔　Ｎ |= φ(n_1,…,n_k) を満たす論理式φ(x_1,…,x_k)が存在する ＜自然数上のｋ項関係（述語）Ｒ(n_1,…,n_k)のＴにおける表現可能性＞ ・Ｒ(n_1,…,n_k)が成り立つときにはＴ |- φ(n_1,…,n_k) ・Ｒ(n_1,…,n_k)が成り立たないときにはＴ |- ¬φ(n_1,…,n_k) を満たす論理式φ(x_1,…,x_k)が存在する 172 名前：基礎論 mailto:sage [03/03/09 22:29] (Ｑ１)そこで、ロビンソン算術Ｑを含む理論Ｔについて、自然数上の述語 Ｐｒｏｖ(n,m) ⇔　ｍは論理式（φとする）のゲーデル数であって，ｎは「Ｔにおけるφの証明」のゲーデル数である． はＴにおいて意味され表現されることが可能であるが、 Ｐｒ(n) ⇔　ｎは論理式（φとする）のゲーデル数であって，「Ｔにおけるφの証明」のゲーデル数が存在する． はＴにおいて意味されることは可能でも表現可能ではない、 ということでいいでしょうか？ (Ｑ２)そして、Ｎ’＝（Ｎ，＋，Ｓ，０）モデルの完全な理論（プレスバーガー算術？）の場合は、 そもそもＰｒ(n)のような述語を意味する論理式が存在しないために、 理論上で存在する文の範囲では証明論的完全性が保たれるということでいいでしょうか？ あるいは、文自身の証明不可能性や理論自身の無矛盾性を意味する文を体系内に存在させなければ、 その体系内では証明も反証もできない文は存在しなくなると言ってもいいでしょうか？ 173 名前：基礎論 [03/03/09 22:31] (Ｑ３)不完全性定理は、理論Ｔに証明も反証もできない文φが存在し、 仮にそれを公理に加えた理論Ｔ’を作ったとしても再び同種の文がその理論に表れるというような、 普遍的な型の決定不能命題の存在を示したということだと思いますが、 例えばロビンソン算術Ｑでは∀x(0+x=x)が証明できないというような場合の、 普遍的ではない単なる公理の能力不足による相対的な決定不能命題というのもあると思いますが、 このように両者を区別して語ることは許されますか？ (Ｑ４)そのような区別ができるとすると、 パリス-ハーリントンの命題はどちらのタイプになるのでしょうか？ 174 名前：基礎論 mailto:sage [03/03/09 22:48] >>172について訂正 ＞あるいは、文自身の証明不可能性や理論自身の無矛盾性を意味する文を体系内に存在させなければ、 ＞その体系内では証明も反証もできない文は存在しなくなると言ってもいいでしょうか？ ↓ あるいは、文自身の証明不可能性や理論自身の無矛盾性を意味する文を体系内に存在させないようにすることで、 その体系内では証明も反証もできない文を存在させなくすることができると言ってもいいでしょうか？ 175 名前：１３２人目の素数さん mailto:sage [03/03/10 09:06] >>171 数理論理学の基本は、syntax と semantics を分けて考えるということ だと本に書いてありました。 「意味する」というのは普通でなく、N で定義可能というはずです、 「表現する」は普通でしょう。 172 の Q2 はゲーデルの不完全性定理の対象とならない公理系は証明論的 に完全かというような質問で、これは「そんなことはない」というのが 答えでしょう。 Q3, Q4 も同種の質問です。 論理式という形式的対象を解釈したところでの概念で分類しようとすれば syntax と semantics を混然とさせるという、ネット数学ではよく知られて いるエムシラ系あるいはマツシン系の論理哲学と似かよってくるのじゃない でしょうか？まあ、そのような議論も楽しくてよいのでしょうが。 176 名前：１３２人目の素数さん mailto:sage [03/03/10 09:07] （Ａ１）御自分では正しいとわかりませんか？ （Ａ２）逆は真ならず。 　　　　プレスバーガー算術の場合、直接完全性を示しています。 （Ａ３）Ｑ３の命題の証明不能性は、ゲーデル命題の証明不能性とは 　　　　無関係に示されます。 （Ａ４）パリス＝ハーリントンの命題の証明不能性の証明は 　　　　この命題から自然数論の無矛盾性が導かれることを 　　　　利用しているので、ゲーデル命題の証明不能性と 　　　　関係しています。 　　　　ただし、今後、ゲーデル命題を用いない形の 　　　　証明不能性の証明が行われる可能性はないとは 　　　　いえません。（あるともいえませんが） 177 名前：１３２人目の素数さん mailto:sage [03/03/10 10:45] >>175 ＞論理式という形式的対象を解釈したところでの概念で分類しようとすれば ＞syntax と semantics を混然とさせるという、ネット数学ではよく知られている ＞エムシラ系あるいはマツシン系の論理哲学と似かよってくるのじゃないでしょうか？ M_SHIRAISHI氏のRLには、syntaxはなくて、全部semanticsみたいな感じ。 逆にsemanticsを排除して、全部syntaxで議論しようとするのは、 例えばStromdorf氏がやってるようなことだな。 前者は単純素朴なプラトニスト、後者は検証主義者ってところだな。 "ﾏﾂｼﾝの論理哲学"というのが具体的に何を指すのか分からないけど、 一時期数学板を騒がせたヴィトとかいう奴は、形はちがうが、 後者のタイプだし、「一階論理と二階論理は違う」とかいう 御仁は、もし、二階論理のsemanticsが数学の存在を定める と考えているなら、プラトニストといえるだろうね。 もし、この二人が同一人物だとしたら、 まさにジキルとハイドのような二重人格者だな。 178 名前：１３２人目の素数さん mailto:sage [03/03/10 11:34] ところで、>>175=>>90かな？ ＞ここで主張されている「本来の二階論理」というのは ＞エムシラのいう二階のベン図でものがわかるという ＞主張からそれほど遠いものとは思えない。 君に聞きたいんだけど、君はstandard-modelは どのように定められていると理解してるの？ 179 名前：１３２人目の素数さん mailto:sage [03/03/10 17:08] >178 standard-model は各人によって定められているわけで、non-standard model をもっていない人の頭のなかにあるものは standard model とは 呼ばない。ただ non-standard model を理解しない数学者の研究対象は standard model と決めつけることになっていると思う。 基礎論に詳しい方のなかには、standard model が集合論の中で一意に 定義されたものであるという人もいるようだが、それは数学を集合論 のなかに形式化すれば、standard model の定義はそれになる、という ことであって、形式化されないところでのものをさすのが普通だと思う。 このような意味でエムシラモデル、マツシンモデルが「ネット数学」に 存在し、通常、standard model は数学者各人がもち、ある程度の共通 認識をもてる対象として数学に存在していると理解しております。 180 名前：１３２人目の素数さん mailto:sage [03/03/10 17:32] >>179 ＞standard-model は各人によって定められているわけで standard-modelは各人によって定められたものではないよ。 ＞standard model が集合論の中で ＞一意に定義されたものである ＞という人もいるようだが、 ちょっと違うな。 例えば自然数論における数学的帰納法を定式化すると、 述語に対する限量子を用いることになるけど、 その限量子の意味を集合論の中でモデル化すれば 自然に一意化されてしまうんだよ。 （これを示したのはデデキントだと思った。 　もちろん、デデキントは二階論理と意識してたわけではない） ＞それは数学を集合論のなかに形式化すれば、 ＞standard model の定義はそれになる、 ＞ということであって、形式化されないところ ＞でのものをさすのが普通だと思う。 モデルは数学理論の意味を集合論の中で定式化したものだよ。 だから定式化すれば、じゃなく、定式化しなくてはならない。 standard-modelが定式化されないというのは間違ってるよ。 181 名前：１３２人目の素数さん mailto:sage [03/03/10 17:40] で、standardとnon-standardの区別はどこから出てくるかというと >>180で述べた自然数論のモデルは二階論理のもので、 自然数論の数学的帰納法を一階論理で表現しなおしたものに ついてモデルを考えると、二階論理のモデルに対応するような もののほかに、それとは異なるモデルがいくらも出来るわけ。 で、もともと意図していた二階論理のモデルに対応する 一階論理のモデルをstandardといい、それとは異なるものを non-standardといってるわけだよ。 数学的な定式化もなしに気分でstandardとかnon-standardとか いってるわけじゃないんだよ。 それじゃ、君、エムシラとおんなじだよ。 182 名前：１３２人目の素数さん mailto:sage [03/03/10 17:44] もし、自然数論を二階論理でなしに、 最初っから一階論理の公理系として 実現したのなら、そのモデルに standardとかnon-standardとかいう 区別をすることが出来ないと思わないかい？>>179 183 名前：１３２人目の素数さん mailto:sage [03/03/10 17:53] ああ、それから、>>181でいうような考え方からいえば standard-modelは何も一つでなくてもいいんだよ。 つまり、二階論理を用いれば、なんでもかんでも モデルが一意化できるわけではないんだ。 184 名前：１３２人目の素数さん mailto:sage [03/03/10 18:14] なかなか議論が盛んですがね、standard model というのは、まあ何の かんのいって御自分のモデルなんですよ。だから179に書いてあるじゃない。 180に書いてある二階の論理なんていってられるかたは集合論の standard model に意識が欠如している古臭い論理のなかに生きている人でほぼ マツシン論理にちかい。 185 名前：１３２人目の素数さん mailto:sage [03/03/10 20:22] >>184 君、マツシンが某掲示板で「出来の悪い学生の誤り」って、 云われたことって実は今君がいってること、つまり>>179 だって知ってたかい？（笑） つまりね、君がマツシンなんだ。わかる？ よりにもよって、自分が馬鹿にしているマツシンと 同じことを自分で主張してたなんてまったく笑っちゃうだろ？ 186 名前：１３２人目の素数さん mailto:sage [03/03/10 20:24] まったくわらっちゃうよな。匿名君は。 一階述語論理しか書いてない日本語の基礎論の本だけ読んで 全て分かった気になって、あの生半可のマツシンと全く同じ 間違いを堂々と口にしてるんだからね。ああ、おかしい（笑） 187 名前：１３２人目の素数さん mailto:sage [03/03/10 20:31] >>184こそ古臭いんじゃないかな？ 最近じゃ、小野さんの論理の本だって二階論理の意味論くらい書いてあるよ。 二階論理は主構造に関しては完全性を満たすように公理化できないともあるよ。 いい加減、自分の無知と強弁を認めたらどうかな？ ここで突っ張りとおすと、マツシンどころかエムシラ、ヤマジンの道を つき進むことになっちゃうよ。Kitty Guyなんていわれたくないだろ？ 188 名前：１３２人目の素数さん mailto:sage [03/03/10 21:11] 相変わらずお元気ですね、179に書いてあることにつきています。 ただ同じことをマツシンがいえばそれは「わかっていない」って ことになりますな、それは中味がないからですな。 189 名前：１３２人目の素数さん mailto:sage [03/03/10 21:20] >>184 ＞だから179に書いてあるじゃない。 >>188 ＞179に書いてあることにつきています。 179のうち 「standard-model は各人によって定められているわけで」 「（standard modelは）形式化されないところでのものを 　さすのが普通だと思う。」 「通常、standard model は数学者各人がもち、 　ある程度の共通認識をもてる対象として 　数学に存在している」 は”マツシンと同じく”、中身のない誤り。 190 名前：１３２人目の素数さん mailto:sage [03/03/10 21:32] >>189のつづき >>179で唯一数学的に意味のある個所はここだけ。 「基礎論に詳しい方のなかには、 　standard model が集合論の中で 　一意に定義されたものであるという 　人もいるようだが、それは数学を 　集合論のなかに形式化すれば、 　standard model の定義はそれになる、 　ということであって」 君は口にしていないが、これは transitive set model のことを云いたいのかな？ ただ、ここでtransitive set modelがstandardであるという 「根拠」を考えた場合、二階論理に頼らざるを得ないんじゃ ないかな？例えば濃度について考えるためには、二階論理に よらざるを得ないよ。一階論理ではいくらでも「ゴマカシ」 がきくことは知ってるよね？ 191 名前：１３２人目の素数さん mailto:sage [03/03/10 21:41] >>179=>>184=>>188の匿名君は、一階論理によることができない場合 「個々人の中にある形式化されないもの」とかいう精神的なものとして 宗教に逃避せざるを得なくなるわけだけど、それじゃエムシラと何ら かわるところがないよね。 そうじゃなくて、二階論理による「述語についての限量」という考えで ある程度説明できるところに数学としてのもっともらしさがあるわけで そこを蔑ろにしてはいけないよね。

---

---

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

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