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

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 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の匿名君は、一階論理によることができない場合 「個々人の中にある形式化されないもの」とかいう精神的なものとして 宗教に逃避せざるを得なくなるわけだけど、それじゃエムシラと何ら かわるところがないよね。 そうじゃなくて、二階論理による「述語についての限量」という考えで ある程度説明できるところに数学としてのもっともらしさがあるわけで そこを蔑ろにしてはいけないよね。 192 名前：１３２人目の素数さん mailto:sage [03/03/10 21:53] 一階の論理であり、二階の論理であり、形式体系　syntax と semantics の区別をが大切、とくに、この区別を syntax の なかですることがゲーデルの第二不完全性定理と関係があり semantics の中ですることが 179 にあること。 二階の論理を持ち出したからといってそれらが解決するわけでは ない。そう思うのはマツシンモデルにおけるマツシン論理。 訂正184の「ほぼマツシン論理にちかい」というのは日本語として おかしい。「限りなくマツシン論理にちかい」というべきであった。 193 名前：１３２人目の素数さん mailto:sage [03/03/10 22:39] >>192 君、文章が崩壊してきてるよ（笑） syntaxと、semanticsの区別をsyntaxのなかでするとか semanticsのなかでするとかって何がいいたいの？ いっとくけど二階の論理をもちだしたから ゲーデルの不完全性定理を乗り越えられるなんて 誰も一言もいってないよ。むしろ、不完全性定理は 二階の論理のsyntaxとsemanticsの関係が、 一階の論理とは違うものであることを示している といってるんだけど、何でそれがわからないかな？ 君の云ってることこそ、かつての一階論理マンセー といってた頃のマツシンと同じなんだけど（笑） そういえば、無矛盾性とかモデルとかに異様なほど 固執するのもかつてのマツシンとまるっきり同じ。 194 名前：１３２人目の素数さん mailto:sage [03/03/10 22:46] あのさ、>>192はいままでどんな勉強したの？ なんか云ってることがつぎはぎだらけで 一貫性がみられなくておかしいんだけど。 195 名前：１３２人目の素数さん mailto:sage [03/03/10 22:50] ほんとマジでおかしいよ。>>192 196 名前：１３２人目の素数さん mailto:sage [03/03/10 22:53] >>194 >>195 興奮しているのはわかるが、二度も書かなくていい。 197 名前：１３２人目の素数さん mailto:sage [03/03/10 23:20] >>186-187 ＞一階述語論理しか書いてない日本語の基礎論の本だけ読んで ＞最近じゃ、小野さんの論理の本だって二階論理の意味論くらい書いてあるよ。 そうそう。原因はともかく、少なくとも日本においては一時期 ２階論理に関する資料が極端に少なかった時期があるよね。君もそ う思うでしょ？ その時期のテキストで論理の学習をした世代は、２階論理になじみ がないと思う。ふるい、古くないの発言が出ている以上、このよう な意味で、「２階算術になじみのない世代」という世代の問題はあ るとお考えなわけですね。 198 名前：1億円ください mailto:sage [03/03/10 23:30] >>186 ＞まったくわらっちゃうよな。匿名君は。 え、君の自作自演じゃないの（笑）？君もなー。 誰が何を言ってるかわからないんじゃ議論にならないよ。熱弁を振る いたいのならば、仮コテぐらい付けてくれない？せっかくの書き込みが 意味ないよ。 199 名前：１３２人目の素数さん mailto:sage [03/03/11 01:05] >>196 訂正。三度も書かなくていい。 200 名前：１３２人目の素数さん mailto:sage [03/03/11 01:53] ゲーデルの不完全性定理を理解したいのですが、 前原「数学基礎論入門」とスマリヤン（高橋訳） 「ゲーデルの不完全性定理」とでは、みなさんど ちらがお勧めですか？それぞれの長所・短所を合 わせて教えて頂けると幸いです。 201 名前：１３２人目の素数さん mailto:sage [03/03/11 03:12] >>200 やっぱ、スマリヤンでしょう。 202 名前：１３２人目の素数さん mailto:sage [03/03/11 07:00] >>199 １つにまとめられる書き込みを3つにするのはマツシンの特徴。 ときどき2つあるいは4つであることもあるが3つが圧倒的に多い。 203 名前：１３２人目の素数さん mailto:sage [03/03/11 07:42] >>197 匿名をいいことに他人事で語るかい？ まあ、いいか。>>179、>>184、>>188、>>192の トンデモぶりは記録されたわけだし。 「マツシン叩きがマツシンになる」ことの好例だね。 204 名前：１３２人目の素数さん mailto:sage [03/03/11 07:51] >>200 ＞ゲーデルの不完全性定理を理解したいのですが 何でもいいから読んでみな。 205 名前：１３２人目の素数さん mailto:sage [03/03/11 09:47] どうも>>179は感情的になっているので、 頭を冷やしていただくために、議論の 発端である>>79までさかのぼってみよう。 ＞２階論理だと完全性定理が成立しないというのは、 ＞どういう意味でしょうか？ ＞それは、２階の部分を部分集合全体で解釈する、 ＞いわゆる standard modelに限れば完全性定理は成立しませんが、 ＞そうではないものもいれれば完全性定理は成立しているのではないですか？ ＞L. Henkin: Completeness of types, J.S.L. (1950) 81-91 ＞general model という枠組で完全性定理が証明されています。 これに対して>>82では、二階論理の本来の意味論は standard modelであり、それに対して、Henkinの general modelは一階論理の意味論にあわせたもので、 non-standardなものであるといっているわけである。 206 名前：１３２人目の素数さん mailto:sage [03/03/11 10:03] >>205 >>82に対して、>>83の「強制法による結果は無意味か？」と >>84の「cut-eliminationは無意味か？」という反論？があるが これに対しては>>85で>>82の主張が、これらの技法による結果を ただちに無意味とするものでないことを暗に述べている。 また、>>86で述べているのは、cut-eliminationが形式化された 推論系に対する議論であるから、それと対応するgeneral model を用いるのは妥当であるが、我々が二階論理において理論を 表現する場合には、推論系による証明能力まで考慮しているわけ ではなく、本来の意味論で考えているわけだから、完全性を 満足させるために無理矢理general modelを考えるのは、 本末転倒であるといっているわけである。 これに対する>>90の反論は、どうみても、二階論理の 推論系(syntax)と、モデル(semantics)が、それぞれ 別個のものであることを無視して、論理といえば、 推論系のことであり、モデルは推論系の都合に 合わせればいいのだといわんがばかりである。 真の誤解は、論理＝推論と考えることにある。 207 名前：１３２人目の素数さん mailto:sage [03/03/11 10:25] ＞真の誤解は、論理＝推論と考えることにある。 このような発言に対して、それではM_SHIRAISHIのRLと同じだ、 という反論があるだろうが、そうではない。 論理が推論ではない、からといって、例えば 「「ならば」の意味が間違っているから、 　ゲーデルの不完全性定理は間違っている」 とかいう荒唐無稽な結果を支持することにはならない。 M_SHIRAISHIが「ならば」と「不完全性定理」に 着目したこと自体は悪くないが、その結果としての RLに関しては、残念ながら見るべきものはない。 208 名前：１３２人目の素数さん mailto:sage [03/03/11 10:35] マツシンに関していえば、某掲示板においては >>90と同様の推論至上主義に凝り固まっていた。 その意味では、この誤解はマツシン固有のものではない。 （ここではネットにおける振る舞いの問題については置いておく） どうも数学板ではマツシンの「誤解」が明確になされることなく、 自分の「常識」に反する主張を、マツシンの誤解、とする行動が まかりとおっている。 しかし、実際には、その常識は、マツシンと同じ「迷信」であり やっていることも、感情的反応に走っている点で、自分達が 批判しているものとそっくりになってしまっている。 まさに同じ穴のムジナである。 209 名前：１３２人目の素数さん mailto:sage [03/03/11 10:44] 閑話休題。本題に戻ろう。 ところで、論理は推論ではない、といったからといって 「摩訶不思議な術によって、あらゆる命題の真偽が分かる」 などということを主張しているわけではないことを重ねて 主張しておきたい。 そうではなく、論理の「意味」を考えるということは、 その意味を明らかにする手段の有無とは独立であると いうことである。 例えば二階論理上の自然数論のモデルが同形だという定理は 自然数論の命題の真偽判定手続きとは無関係に示されるのである。 デデキントは決して曖昧な直感的議論を行ったわけではない。 210 名前：１億円ください mailto:sage [03/03/11 11:39] >>203 ＞匿名をいいことに他人事で語るかい？ なんか勘違いしてないか？197=198 であって、私が書いたのですが？ 他人の投稿だから他人事として語るんですけど（苦笑） それよりも、君は、>>197 で言っているような世代の問題はあるって 思ってるよね、という内容のほうに答えてもらえないでしょうか？ 僕は以前、この手の世代の話題を出したら、誰かにそんなものはない、 的にあしらわれたんだけど（笑）、ある時期の日本語テキストで ２階述語論理に触れているものはすくないという印象は捨てがたいんだよね。 君も同じような印象を持っているようだから聞いてるだけなんですが。 211 名前：１３２人目の素数さん mailto:sage [03/03/11 11:55] >>210 世代の問題ではなく地域の問題だよ。 日本はロジックでは辺境の地なんだよ。 日本で数学基礎論といえば昔は竹内の証明論だったわけですが それは単純に時期がどうこうというより、辺境である日本の 特殊な事情があるわけ。 212 名前：１３２人目の素数さん mailto:sage [03/03/11 12:01] >>210は>>79=>>179なのかい？ 違うなら、別の話題を振るのは遠慮してくれよ。興味ないから。 213 名前：1億円ください mailto:sage [03/03/11 12:19] >>211 同意。まあ、竹内先生が日本の logic の代表者であった世代の問題でも ある（僕はそちらを強調した）ので、「日本という特殊な地域でのある 世代の問題」が正確じゃないかな。 前原先生が亡くなったときの数学セミナーの追悼記事で、 往時のモデル論軽視の風潮が忍ばれる回想記事があったよね。 今手元に数セミがないのでわからないが、誰の記事だったっけ？ 持ってない？ そろそろ、日本の logic 史もある程度まとめる時期だよね。はやくしないと 証人が死んでしまう（苦笑） 214 名前：1億円ください mailto:sage [03/03/11 12:31] >>212 信じる信じないは勝手だが、おれはこのハンドルを定めてから、ミスを除いて このハンドルで書き込んでるよ。 俺もまねしようかな。>>91 = >>211 = >>212 かね？発言が少々矛盾してないか？ 215 名前：１３２人目の素数さん mailto:sage [03/03/11 12:36] >>200 その質問にマッチするスレを紹介しましょう。 前原本 science.2ch.net/test/read.cgi/math/1043852921/l50 スマリヤン本 academy.2ch.net/test/read.cgi/philo/1024981591/l50 この２スレを読んでみては。 216 名前：１３２人目の素数さん mailto:sage [03/03/11 13:21] >>214 ＞信じる信じないは勝手だが 信じよう。 ＞>>91 = >>211 = >>212 かね？ ＞発言が少々矛盾してないか？ それをいうなら>>89と>>210は ニュアンスが違うだろ。 >>89は世界的レベルの話で >>210は日本ローカルだと 思ったわけさ。 217 名前：１３２人目の素数さん mailto:sage [03/03/11 13:28] >>213 ＞そろそろ、日本の logic 史もある程度まとめる時期だよね。 ＞はやくしないと証人が死んでしまう（苦笑） Ｇ．Ｔ氏ですか？（をひをひ） もっとも、logic史を総括するなら、 Xデーの後のほうがいいかと（笑） 218 名前：１３２人目の素数さん mailto:sage [03/03/11 14:21] 二階の論理を持ち出さないと standard, non-standard の区別が できないと思っているのは錯覚。大体、数学をしているとき、 だれも一階だ二階だなどと気にしない。つまり自分がいるところ がすべてである。それでなにも気にしなければ形式論理など無関係。 ところが哲学関係あるいは論理学のみって人たちは妙にうるさくいう。 しかし、論理なんて数学以外のところではそんなに複雑なものを使う わけではない。そこで部分集合の関係した命題がいかに複雑で直感 からほど遠いものだということを知らない。それでどうもエムシラ モデルとマツシン論理の域からそれほど遠くないところで終わって しまうってことなのだろうか？ 219 名前：１３２人目の素数さん mailto:sage [03/03/11 14:38] ＞二階の論理を持ち出さないと ＞standard, non-standard の区別が ＞できないと思っているのは錯覚。 R.Montagueが、以下の文章でいっているよ。 Set theory and higher order logic. Formal systems and recursive function, pp131-148. North Holland, Amsterdam 220 名前：１３２人目の素数さん mailto:sage [03/03/11 14:42] ＞大体、数学をしているとき、だれも一階だ二階だなどと気にしない。 ＞つまり自分がいるところがすべてである。 ＞それでなにも気にしなければ形式論理など無関係。 普通の数学者が論理を意識しなくても結構だが、 standard modelは論理において明確に決められた 専門用語なんだよ。君が知らないだけ。 「自分がいるところがすべて」とかいう発言は、 マツシンというより、エムシラの域に達してるよ（笑） 221 名前：１３２人目の素数さん mailto:sage [03/03/11 14:51] ＞ところが哲学関係あるいは論理学のみって人たちは妙にうるさくいう。 君が鈍感なんだよ。 ＞しかし、論理なんて数学以外のところでは ＞そんなに複雑なものを使うわけではない。 ＞そこで部分集合の関係した命題がいかに複雑で ＞直感からほど遠いものだということを知らない。 君さ、論理に敏感だっていうなら、数学的帰納法で 二階論理で述語の全称化をするのと、一階論理で 任意の述語について全部公理にしちゃうのとの 違いに気づいてほしいね。 つまりね、後者のスタイルでは、 一階論理の中で書ける述語しか、 しばれないんだよ。 222 名前：１３２人目の素数さん mailto:sage [03/03/11 14:53] ＞それでどうもエムシラモデルとマツシン論理の域から ＞それほど遠くないところで終わってしまうってこと ＞なのだろうか？ 君が一番のﾃﾞﾑﾊﾟだよ（笑） 223 名前：１３２人目の素数さん mailto:sage [03/03/11 18:17] >222 つまりエムシラモデルとマツシン論理の域に限りなく近い人と ﾃﾞﾑﾊﾟの議論ってことだね。 224 名前：223 mailto:sage [03/03/12 07:42] 192 のﾃﾞﾑﾊﾟの議論は筋があることの説明をしてみよう。 「syntax のなかでsyntax と semantics の区別をする」というとき もちろん2つの syntax を同じ意味でとってはおかしくなる。通常 syntax と semantics の区別というとき、それは普通の数学を考えるのと同じく形式化 されていないところで考えている。 171 にある表現可能性というのは semantics と syntax をつなぐ関係で ある。この関係の成立の証明がどのような形式体系で実行できるかをみて これを形式体系(syntax) で実行した結果を使うと第2不完全性定理がみち びかれる。一方、普通の数学を考える場をカント−ルユニバ−スのような ものと思い、これが semantcis と思えば 179 のような説明になるだろう。 standard というのは公理化するとき想定した1つあるいはいくつかのもの をいい、そうでないものを non-standard というのが普通の数学のなかで の使い方であり、数理論理学のなかでもそんなものだろう。 ﾃﾞﾑﾊﾟであろうがエムシラモデルであろうがマツシン論理であろうが、 問題は数学的に面白い定理が証明されれば数学としてはよいわけで、それが なければ、いくら力こぶをいれても数学的には意味がない。逆にいえば、 間違っているか間違っていないかより、結果的に数学的に面白い定理が証明 されるほうが重要だろう。 225 名前：１３２人目の素数さん mailto:sage [03/03/12 09:51] 224(=192)　がﾃﾞﾑﾊﾟであることの証明をしてみよう。 まず、はじめに、 ＞171 にある表現可能性というのは ＞semantics と syntax をつなぐ関係である。 君のいう表現可能性はこれかな？ 「＜自然数上のｋ項関係（述語）Ｒ(n_1,…,n_k)のＴにおける表現可能性＞ 　・Ｒ(n_1,…,n_k)が成り立つときにはＴ |- φ(n_1,…,n_k) 　・Ｒ(n_1,…,n_k)が成り立たないときにはＴ |- ¬φ(n_1,…,n_k) 　を満たす論理式φ(x_1,…,x_k)が存在する」 つまり、君は表現可能性＝決定可能性と考えるわけね。 奇妙な理解だね。 ＞この関係の成立の証明がどのような形式体系で実行できるかをみて ＞これを形式体系(syntax) で実行した結果を使うと ＞第2不完全性定理がみちびかれる。 あのね、Ｔ |- φ(n_1,…,n_k)とかＴ |- ¬φ(n_1,…,n_k)とかいうのが そもそもＴという形式体系からφ(･･･)とか¬φ（･･･）が証明できる ということをいってるんだよ？ で、これと第二不完全性定理（つまりＴでＣｏｎ（Ｔ）が証明できない） との関係を君はどう理解してるのかな？ 226 名前：１３２人目の素数さん mailto:sage [03/03/12 10:04] 次に ＞一方、普通の数学を考える場をカント−ルユニバ−スのようなものと思い、 ＞これが semantics と思えば 179 のような説明になるだろう。 179の説明とはこれかな？ 「基礎論に詳しい方のなかには、standard model が集合論の中で 　一意に定義されたものであるという人もいるようだが、それは 　数学を集合論のなかに形式化すれば、standard model の定義は 　それになる、ということであって、形式化されないところでのものを 　さすのが普通だと思う。」 もしかして、前段の第二不完全性定理云々も、この主張も 「standard modelは形式化できない」ということをいいたい のかな？ （それなら、むしろ第二より第一不完全性定理だと思うんだが 　もしかして、君、無矛盾性と完全性を混同してる？） あのね、modelを定義するのと、modelを"構成"するのは違うよ。 君がいってるのは、 「modelを、形式的体系によって"構成"できない」 ってことでしょ。 そうじゃなくて、「modelとは・・・なものだ」という定義はできるんだよ。 それでその定義に従って、一階論理では完全性が成り立つが、 二階論理はそうではないとかいう議論はできるわけだよ。 上の区別が出来てないってことは、 形式的体系の意味も、完全性定理の意味も 分かってないってことだよ。 227 名前：１３２人目の素数さん mailto:sage [03/03/12 10:19] さらに ＞standard というのは公理化するとき想定した ＞1つあるいはいくつかのものをいい、 ＞そうでないものを non-standard というのが ＞普通の数学のなかでの使い方であり、 ＞数理論理学のなかでもそんなものだろう。 それは完全に無知による独断の誤り。 君が今までに何がstandard modelかについての 説明を目にしてこなかったからといって、そこから 直ちに「ああ、standardって個々人の想定したもの なんだ」ということにはならないよ。 濃度について説明してみよう。 一階論理上での集合論で可算モデルが存在するのは 「実際は自然数と対象領域の間に一対一対応が存在するけど 　その対応は一階論理の中では表現されないからOK」 ってことでしょ。 で、二階論理でそれが通用しないのは、 「実際には存在するけど」という可能性を 述語に関する全称化で排除しちゃったから。 228 名前：１３２人目の素数さん mailto:sage [03/03/12 10:36] ところで ＞数学的に面白い定理が証明されれば数学としてはよいわけで、 ＞それがなければ、いくら力こぶをいれても数学的には意味がない。 ＞逆にいえば、間違っているか間違っていないかより、 ＞結果的に数学的に面白い定理が証明されるほうが重要だろう。 それって君の誤りの言い訳かい？ 君が、この誤りと関係なく、数学的に面白い定理を証明していたとしても、 この誤りの「罪」を免れることにはならないよ。 そもそも、本当にそう考えているなら、君は自分の仕事をするべきで 自分が何の知識も持ち合わせず、何の実績もあげられない場所で 力こぶをいれて自分の信条を語っても意味がないだろう。 しかも、その信条は数学的に間違った思い込みに根ざしている。 君に、ｴﾑｼﾗやﾏﾂｼﾝを馬鹿にすることなんてできないよ。 229 名前：１３２人目の素数さん mailto:sage [03/03/12 10:55] とにかく>>223クンは、以下の基本的誤解を正してね １．形式的体系で決定可能な述語として表すことが ”モデルを形式的体系として表すこと”と思っている誤り ２．「命題かその否定のいずれかが証明可能」という完全性と 「命題とその否定のどちらも証明されることがない」という無矛盾性を 混同する誤り ３．モデルの定義と構成を混同する誤り 特に１、２、はﾏﾂｼﾝ以前だね。 230 名前：１３２人目の素数さん mailto:sage [03/03/13 07:14] まあ滔々と書いてはいらっしゃるし、妙に２階論理を振り回す以外、まあそう 変なことを書いているわけではないのだが、理解力に難があるようで（とはいえ イマイの爺さんよりははるかにましだが）デムパの筋がわかるまでにはなって ないようだ。これ以上説明しても無理だろうが、なかに真面目に勉強している 人もいるかもしれないから、225 に関するところだけ説明しよう。 もちろん、semantics と syntax をつなぐ関係というのは同値という意味では ない。述語 R の表現可能性ということだが、不完全性定理に関し、この概念を 使う R は原始帰納的述語である。さてこの述語の主語となる自然数というのは どこにあるものか？ということを考える。すると、これは自分のものを考えて いる場にあるものだと気づく。つぎに述語 R からどのように論理式 phi をつ くるかということ、そして第２不完全性定理の証明でこの表現可能性が成立し ていることを論理式で書くことを考えれば、R に何らかの論理式が対応してい ないとそのようなことが実行できないことがわかる。 このような背景で自分のものを考える場の自然数というのが自然数論の standard model の自然数であると考えられるということになる。 231 名前：１３２人目の素数さん mailto:sage [03/03/13 07:57] >>230 君の書いてることは変。 君のいう「(syntaxによるsemanticsの)表現可能性」とは 「決定可能性」のことなのね。でも普通そういうひねくれた 誤解はしないよ。 で、君はもしかして原始帰納的でない述語は 論理式として書き表すことができないとか 思ってるわけじゃないだろうね？ 誠に残念ですが、それは完全な誤解。 自然数論の中で表現可能な述語は、 原始帰納的述語に限らない。 ところで君はどの本を読んでそのような奇妙な誤解に至ったのかい？ 232 名前：１３２人目の素数さん mailto:sage [03/03/13 08:09] ああ、分かったよ。前原の本を読んだんだね。 いいかい、君のいう「表現可能」は、前原の本では 「強い意味で表現可能(p154)」となってるんだ。 それに対して、論理式として書けるという意味の 表現可能は、それ以前のp114に定義されている。 なぜ、このような概念を導入したか、といえば、 それは第二不完全性定理が、無矛盾性という、 証明手続きに関係した性質についての証明だから。 233 名前：１３２人目の素数さん mailto:sage [03/03/13 09:44] >>232 ＞論理式として書けるという意味の表現可能は、 ＞それ以前のp114に定義されている。 おっと違った。p101の定義7.1には 君のいう「表現できる」と同じ定義 があるな。 ただ、ここの定義の問題は議論の本筋に影響していない。 君は第二不完全性定理がどうこういってるが、それは 完全性定理にまつわる一階と二階の違いとは関係がない ということ。わかるかな？ 234 名前：１３２人目の素数さん [03/03/13 10:17] 命題などを記述する際に、われわれは記号を使うわけだが、それらの記号の 数は特に決まっておらず、有限個であるとしているようだ。 　今�狽ﾆいう記号が含まれていない場合に、それを新たな記号として追加 しようとしたとすれば、その�狽ｪ何を意味する記号であるかを、それまで の記号で説明しなければ、無定義用語・記号になってしまう。 逆にいえば、xは掛け算、＋は加算、9は８の次、、、、などと それ以前の記号のセットだけで新しい記号の意味を説明して付け加えた ものだと考えれば、その説明自身に現われる記号は既定義でなければ ならないわけですよね。そのようなことが可能な最小の記号の組とは どのようなものでしょうか？ 　そもそもなんらかの情報を伝えるのですから、記述用記号は１種類 ではだめで少なくとも２種類なければだめですが、果たして２種類だけ あれば、それで任意の数学的概念を、自己完結して記述できるんだろう かというのが僕の疑問です。たしかに計算機では二進数あるいは二状態 のみをつかって通信ができますが、たとえばアスキー記号の定義自身は その外部で通信するもの双方が暗黙の了解で共有しているとみなすなら、 実は記号はアスキー表の分だけはあらかじめ既定義であるということに なりそうです。数学の記述に十進数を使うのなら、すくなくとも数字の 記号としては１０通り用意せねばなりません。すると二進数で数学の 命題や記述をすれば記号の種類を減らせるのです。このようにして、 最小だが、それをベースにして任意の数学命題をきちんと定義を追加して 拡張しながら記述できるようになるためには何種類の記号・符号が 必要なのでしょうか？ 235 名前：１３２人目の素数さん mailto:sage [03/03/13 10:26] ＞述語 R からどのように論理式 phi をつくるかということ、 ＞そして第２不完全性定理の証明でこの表現可能性が ＞成立していることを論理式で書くことを考えれば、 ＞R に何らかの論理式が対応していないとそのようなことが ＞実行できないことがわかる。 ああ、なるほど。君は以下の比較がしたかったわけね。 論理式Phiと述語Rとの対応。 syntactical: 前原の定義７．１（ただし完全ではない） semantical:　個々人の心の中 僕が批判しているのは、後者のsemanticalな対応 について、全く心の中の出来事だといいきってしまって いるところ。 例えば、君はDedekindが、自然数はcategoricalだと 証明したことを「全くナンセンス」だと思ってるのかい？ 236 名前：１３２人目の素数さん mailto:sage [03/03/13 10:40] >>234 そもそも、記号は意味を記述しているんだろうか？（笑） 理論はそれを理解する主体を必要とする。 ただそのことがただちに 「二階論理では完全性定理が成り立たない」 という主張をHenkinモデルまで持ち出して 拒絶する理由にはならないよ。 237 名前：１３２人目の素数さん mailto:sage [03/03/13 12:01] >234 記述したものをどう読むかということとの組で考える話だと思う。 またブランクを文字と思うかということもある。 まあこういったことはあるが、Turing 機械に関するところでよく 知られていることはテープ上のブランク B と 1 で十分ということ。 だから2つっていうのかな? 238 名前：山崎渉 mailto:（＾＾） [03/03/13 12:53] （＾＾） 239 名前：１３２人目の素数さん mailto:sage [03/03/14 02:12] マツシン（＝松本真吾）のガキが、一丁前づらしてゴトクを並べてるのは、ここか？ 240 名前：１３２人目の素数さん mailto:sage [03/03/14 07:13] このような人の書き込みは多いし、まあもっとすごいのはいくらでも あるが、それらしいことを書いているが数学としてわかっているわけ ではないということが顕著になっているので指摘しておこう。 171 の表現可能性に関することである。これはこのスレッドでの書き込 みにあるように semantics と syntax とつなぐ概念で、不完全性定理 では大切な概念である。171 の記述は semantics における x_i と対応する syntax の numeral が同じ記号となっているが印刷物では間違わない ように違う字体の文字あるいは下線、上線などを使う。しかし、これは その定義を意味あるものとして理解しようとすれば、これ以外の理解はで きないものである。 さて 225 でこれをコピーした人はこれが決定可能性と関係があるという 解釈を展開する。決定可能性というのは言葉は「肯定あるいは否定が証 明できる」という意味、あるいは「無限個の命題があるとき、その真偽 を決める、定まった手続きがある」という意味である。いくらなんでも 第一の意味では受け取れないであろうから第二の意味で解釈したのであ ろうと思う。しかし、その理解も想像を絶する。まあ相手がデンパだと 思っているということで割り引いて話を進めるが、232,233,235に至り、 ほぼ正しい理解に到達したらしい。 この前原本は、ゲーデルの原論文の内容とそれほど違いはないの は著者がいってるとおりで、上記の概念は不完全性定理の証明がわかって いる人は当然理解していることである。つまり、この書き込みをしている 人は全くこれを理解していなかったのだ。そしてなおかつ、不完全性定理 についての見解を披露し続けてきていたわけである。 241 名前：１３２人目の素数さん mailto:sage [03/03/14 07:50] >>240 >>224で云ってることが>>232-235のことなら、 まさに決定可能性のことだよ。 ＞＜自然数上のｋ項関係（述語）Ｒ(n_1,…,n_k)のＴにおける表現可能性＞ ＞・Ｒ(n_1,…,n_k)が成り立つときにはＴ |- φ(n_1,…,n_k) ＞・Ｒ(n_1,…,n_k)が成り立たないときにはＴ |- ¬φ(n_1,…,n_k) ＞を満たす論理式φ(x_1,…,x_k)が存在する は、個々の数値に対して「肯定あるいは否定が証明できる」 φとして表現できるといってるわけだからね。 で、224はそうできないφは 「述語を表現していない」 といっているんだろう？それがﾃﾞﾑﾊﾟ。 まあ、前原本しか読んでいないのであれば分かりようがないな。 242 名前：１３２人目の素数さん mailto:sage [03/03/14 08:01] >>241について、補足説明しよう。 前原のいう"形式的な表現"は、決定可能性によるものであるが、 それのみが意味を確定するわけではない。 ところでゲーデルの原論文及び前原本では 「自然数論における非決定命題の存在」 を示すことが目的である。そのレベルにおいては 一階と二階の論理の違いは問題にならない。 ここでいっているのはデデキントによる自然数論の範疇性証明と 非決定性命題の存在が、二階論理において 「どのようなモデルでも真ではあるが、証明不可能な問題がある」 ことを結論することであるから、議論の力点は非決定性命題よりも 自然数論の範疇性にある。 243 名前：１３２人目の素数さん mailto:sage [03/03/14 11:22] >>240は辻下・角田の主張をどう理解しているのだろうか？ 244 名前：基礎論 mailto:sage [03/03/14 15:14] 「表現可能性」や「強い意味での表現可能性」なんかの定義は 明確に書かれていることが多いですけど、 例えば、第一不完全性定理では自分自身の証明不可能性を「意味する」命題の存在が示される と言う場合の「意味する」可能性についてはあまりはっきり書かれていない気がします。 つまり、自然数上の述語Ｒを意味する論理式の定義可能性ということを考えると、 プレスバーガー算術などでは、自分自身の証明不可能性を「意味する」論理式が定義されないがゆえに、 定義可能な文の範囲では、証明も反証もできないものが存在しない、 つまり証明論的に完全ということではないでしょうか？ 自然数上の述語を意味する論理式の定義可能性を単純に「定義可能性」と呼ぶことにして、 次のように整理してみました。 245 名前：基礎論 mailto:sage [03/03/14 15:15] ＜自然数上のｋ項関係（述語）Ｒ(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)が存在する 論理式φのゲーデル数を[φ]と表記し、 自然数上の述語 Ｐｒ(n) ⇔　ｎは論理式（φとする）のゲーデル数であって，「Ｔにおけるφの証明」のゲーデル数が存在する． を表現する論理式をPr(n)とする ＜自然数上のｋ項関係（述語）Ｒ(n_1,…,n_k)のＴにおける強い意味での表現可能性＞ ・Ｒ(n_1,…,n_k)が成り立つ ⇒ Ｔ |- φ(n_1,…,n_k) ・Ｒ(n_1,…,n_k)が成り立たない ⇒ Ｔ |- ¬φ(n_1,…,n_k) ・Ｔ |- φ(n_1,…,n_k) → Pr([φ(n_1,…,n_k)]) ・Ｔ |- ¬φ(n_1,…,n_k) → Pr([¬φ(n_1,…,n_k)]) を満たす論理式φ(x_1,…,x_k)が存在する 246 名前：基礎論 [03/03/14 15:33] このような理解で問題ないでしょうか？ 247 名前：１３２人目の素数さん mailto:sage [03/03/14 15:49] >>244 ＞第一不完全性定理では自分自身の証明不可能性を ＞「意味する」命題の存在が示されると言う場合の ＞「意味する」可能性についてはあまりはっきり ＞書かれていない気がします。 「第一不完全性定理では」はいらないでしょう。 前原の本では、第二不完全性定理でも、はっきり 書かれるわけではないから。 前原の本ではモデルについては論じていないし、 論じたとしても一階論理のモデルでは、逆に 論理式の意味に不確定性が生まれる。 辻下・角田の両氏の「数学における不定性」は 数学を一階論理上の公理系として考えるなら、 当然出てくる考えである。 しかし（二階論理の妥当性はともかくとして） 我々は数学を考える際に、実に無意識に二階の 定式化を用いているし、その意味で考えた場合 には自然数というものは一つに決まってしまう。 自然数は、群や位相のようにもともと不定な 抽象構造とは違うんですよ。 248 名前：１３２人目の素数さん mailto:sage [03/03/14 16:03] >>245 ＞＜自然数上のｋ項関係（述語）Ｒ(n_1,…,n_k)のＴにおける定義可能性＞ ＞・Ｒ(n_1,…,n_k)が成り立つ　⇔　Ｎ |= φ(n_1,…,n_k) ＞を満たす論理式φ(x_1,…,x_k)が存在する 君はこれをどう理解するの？ 例えば>>179や>>230は左辺のＲも、右辺のＮも 「頭のなかにあるもの」 「自分のものを考えている場」 といってるわけだよね。 でも、それだけなら、ﾃﾞﾑﾊﾟと同じ主張だよね（笑） 249 名前：１３２人目の素数さん mailto:sage [03/03/14 16:11] >>248 ところで、Ｔにおいて定義不可能な述語も当然あるよ。 例えば、Ｔ中の論理式の真偽なんていうのはＴでは定義不能。 つまり、Ｔの中のどんな式φを持ってきても、 Ｔの中の論理式のゲーデル数に対して真偽を 割り付けるような述語とは一致しないってこと。 250 名前：基礎論 mailto:sage [03/03/15 02:20] >>247 すいません、誤解しやすい書き方でしたが、その引用の部分は ＞例えば、 ＞「第一不完全性定理では自分自身の証明不可能性を「意味する」命題の存在が示される」 ＞と言う（ような）場合の「意味する」可能性についてはあまりはっきり書かれていない気がします。 ということです。あくまで例えとして「」内の文章を取り上げたので、別に限定する意味はありません。 >>248 自然数上の関係Ｒなんかは、便宜的に言葉で表記していても、実際指示しているのはその内容であって、 φ(n_1,…,n_k)のような形式的な、解釈なしではその表記自体しか指示しない式とは 区別されるものではないですか？ 数学の立場では、算術の標準モデルＮの存在は自明の前提としているので、 当然、関係Ｒもアプリオリに存在するものとしておいて、 後はいかにそれを「意味する」論理式を理論Ｔにおいて構成するかが問題で、それは ・Ｒ(n_1,…,n_k)が成り立つ　⇔　Ｎ |= φ(n_1,…,n_k) が成り立つ論理式φ(n_1,…,n_k)を定義できるかどうかということになるのではないですか？ 251 名前：基礎論 [03/03/15 02:26] >>249 自分自身の証明不可能性を意味する文を定義できない理論なら、 不完全性定理を回避できるということになりますよね？ 252 名前：１３２人目の素数さん mailto:sage [03/03/15 07:05] >>250 内容って何？ 「数学の立場では、算術の標準モデルＮの存在は自明の前提としている」 って本当？ 標準モデルの存在は、自明の前提じゃないよ。 関係Ｒもアプリオリに存在すると考えるべきではないよ。 >>251 必ず回避できるわけではないよ。 逆に、決定可能な理論では、自分自身の証明可能性を意味する文を 定義できないってこと。なぜならそんな文は決定不能だから。 実は>>249の定理（タルスキーの定理）も 「自分自身が偽である」を意味する文が存在すると 矛盾することを利用して体系自身の真偽定義が 常に不可能であることを示している。

---

---

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

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