- 1 名前：1 [04/10/13 18:26:50]
-
数学基礎論の質問スレッドが、今、無いようなので、新しくたてました。
ほかに質問のある方、どしどしと、質問してみてください。誰かが、教えてくれることもあるでしょう。
さて、私の質問ですが、
『論理学をつくる』という本の、一階述語論理の公理系の例のところに、
公理として、 ∀ξ（ξ=ζ） ξ、ζは個体変項をあらわす図式文字
というものがあがっていました。
公理ということは、恒真式なはずなんだけど、それが、なぜ、恒真式なのかが、わからなくて、疑問におもっています。
どなたか、わかる方、お教えください。
- 29 名前：１３２人目の素数さん [04/10/28 23:42:41]
- 数学基礎論って数学入門のことと思ってた
- 30 名前：28 [04/10/29 00:16:01]
- あ、誰か教えてくれたか？と思ったらｗ
\mathfracは\mathfrakの間違いね
- 31 名前：１３２人目の素数さん mailto:sage [04/11/02 02:41:11]
- >>28
今考えている状況ではその二つは同値なので、違いは何かと聞かれても答えが難しい。
同じであると思っていてかまわないと思う。
この同値は「Σ_1-完全性」から導かれる構文論的な事実なので、
\mathfrak{N}\models \text{Prov}_T(\overline{n},\overline{m})
では \mathfrak{N} に制限しなくとも成立するし、これよりも
PA \vdash \text{Prov}_T(\overline{n},\overline{m}) や
PRA \vdash \text{Prov}_T(\overline{n},\overline{m}) と同値になると
書く方が気分が出ている。
- 32 名前：28 mailto:sage [04/11/04 17:18:08]
- >>31
御教示有難うございます。PRAなどそちらの方面はあまり知らないのですが
\mathbfの太字で書いた述語のニュアンスが
良く分からなかったので質問させて頂きました。
>>今考えている状況では
ということは状況によっては異なる、ということだと思うのですが
具体的にはどういう状況になるのでしょうか……
確かにこれはSyntacticalな超定理なので\vdashの左側に
個別の自然数論の名前を書いたほうが本質的ですね。
全然関係ない雑談ですがこの本はTeXの書き方が汚すぎると
思うのですがどうでしょう？QuineのG\"odel数の記号も
本当は例えば\ulcorner,\urcornerを使ったほうがいいのに
天井関数\lceil,\rceilで代用しているから見るに耐えなくなっているし
また\vdashの否定が、\nvdashではなく\notをそのまま重ねているから
ちょっと斜線の配置がおかしい。（これは趣味の問題ですが）
そもそもTeXで証明可能のターンスタイルには\vdashを使わざるを得ないのに
恒真のターンスタイルにはサイズの違う\modelsが用意されているのも
変ですね。この二つは一階述語論理では対になる概念なので
同じサイズにするのが適当なのに。なんか雑談ばっかりになっちゃいました。
- 33 名前：１３２人目の素数さん mailto:age [04/11/06 02:27:06]
- さて、今から、図書館から借りた『二十世紀数学思想』でも読みますか
この本二十世紀数学といいながら基礎論のことしか
書いてないような気がするけど漏れには好都合ｗ
- 34 名前：１３２人目の素数さん mailto:sage [04/11/07 02:24:40]
- >>32
出版の時期から考えて、著者達が LATeX2ε に乗り換えていたかどうかは微妙。
- 35 名前：質問！ [04/11/07 02:32:14]
- P=NP 問題って、なんですか？
- 36 名前：１３２人目の素数さん mailto:sage [04/11/08 04:37:18]
- >>34
なるほど、だからあんなに書き方が微妙なんですね。納得。
- 37 名前：１３２人目の素数さん mailto:sage [04/11/09 12:52:57]
- >>35
ペニスはぬるぽかという問題です。
- 38 名前：１３２人目の素数さん mailto:sage [04/11/09 21:16:08]
- >>35
ペニスはぬるぽじゃないっていう意見が支持されてるよ！
- 39 名前：あぼーん mailto:あぼーん [あぼーん]
- あぼーん
- 40 名前：１３２人目の素数さん [04/11/16 22:33:57]
- ぬれぽ
- 41 名前：１３２人目の素数さん [04/11/16 22:40:31]
- ぬるーつポンチ
- 42 名前：あぼーん mailto:あぼーん [あぼーん]
- あぼーん
- 43 名前：山本エミ子 ◆YH4ME.Qywg [04/12/05 18:10:11]
- Aは２行２列の行列。
固有値pに対する固有ベクトルの一つをu、固有値qに対する固有ベクトルの一つをvとする。
uとvの内積をu･vと表しAの転置行列をBとすると
(Au)･v=u･(Bv)
であることを証明せよ。
即出だと思いますが
だなたか証明してください。
よろしくお願します。
- 44 名前：１３２人目の素数さん mailto:sage [04/12/05 19:00:47]
- スレ違いのマルチ嵐
- 45 名前：１３２人目の素数さん [04/12/09 11:09:13]
-
『記号論理学』 清水義夫
この本の一階述語論理の公理系の公理のところの記述に以下のようなものがあります。
A4 ∀xiAｘi→Axi/t
Axi/tで、Aにふくまれる自由変項xiのすべてのところに項ｔを代入した式を表わす。
A5 ∀xi（A→Bxi）→（A→∀ｘiBxi）
ただしAにはxiは自由変項としては現れていないとする。
この本では、
縛られている個体変更に束縛変項、縛られていない個体変項に自由変項、という語を用いているようです。
A4、A5、の記述についてですが、自由変項と束縛変項の語を使い間違っているように思うのですが、
どなたか、わかる方、お教えください。
- 46 名前：１３２人目の素数さん mailto:sage [04/12/09 11:26:36]
- ちょっとこの本持って無いから適当なレスしか
出来ないけど、多分間違ってないと思うよ？
具体的にどういう風に書き直されるべきだ、と思うんですか？
- 47 名前：１３２人目の素数さん [04/12/09 13:08:57]
-
∀ｘ（Aｘ→Bｘ） 前提
∀ｘ（Aｘ→Bｘ）→（（A（ある項）→B（ある項）） A4
というような証明の過程を見たときに、
あれ、ｘ、縛られてるじゃん、というように思いました。
- 48 名前：１３２人目の素数さん mailto:sage [04/12/09 13:27:54]
- >>45
「A にふくまれる」とか「A には」と書いてあるところでは、
A だけを独立して考えていて、A がどのような論理式の部分
論理式であるかは考えていません。
- 49 名前：１３２人目の素数さん mailto:sage [04/12/09 15:46:20]
- >>48
なるほど、そういうことですね。
ありがとうございました。
- 50 名前：１３２人目の素数さん [04/12/10 19:07:19]
- 一階の理論はモデルをもてば無矛盾。
一階の自然数論はモデルをもつ。
一階の自然数論は無矛盾。
何がおかしいのか教えてください。
- 51 名前：伊丹公理 [04/12/10 19:30:44]
- ＞一階の自然数論はモデルをもつ。
の証明が無い。
- 52 名前：１３２人目の素数さん [04/12/10 19:41:03]
- >>51
普通に解釈の下では公理がすべて真になりますよね？
超準モデルとかいうやつもありますよね？
もっと詳しく教えてください。
- 53 名前：１３２人目の素数さん mailto:sage [04/12/10 19:41:36]
- >>52
普通の解釈 でした。
- 54 名前：伊丹公理 [04/12/10 19:49:36]
- ＞普通の解釈
とは？
普通の解釈はペアノの自然数論等２階になる。
（これも無矛盾かどうか分からない。）
- 55 名前：１３２人目の素数さん [04/12/10 19:56:28]
- 二階になるのは帰納法の公理のせいですか？
十分に適用対象を制限すれば大丈夫じゃないですか？
また、ロビンソン算術は上記の論証により無矛盾と言えますか？
- 56 名前：伊丹公理 [04/12/10 20:01:36]
- ＞二階になるのは帰納法の公理のせいですか？
そうです。
＞十分に適用対象を制限すれば大丈夫じゃないですか？
公理が無限個になるので簡単にはいきません。
＞ロビンソン算術
って何?
- 57 名前：１３２人目の素数さん [04/12/10 20:10:42]
- >>56
何度もありがとうございます。
一階の自然数論から帰納法の公理を抜いた体系がロビンソン算術です。
一階の自然数論の対象となる論理式（可算）に制限すれば、二階になりませんよね？
そもそも、解釈が二階になってもそれがモデルであれば、
モデルが存在するのであり、問題ないように思えるのですが。
- 58 名前：１３２人目の素数さん [04/12/10 20:16:26]
- ＞モデルが存在するのであり
それが証明されていない。
- 59 名前：１３２人目の素数さん [04/12/10 20:23:38]
- >>58
ありがとうございます。
すると、みんなが自然数論の通常のモデルとか超準モデルとか言っているのは
全部嘘っぱちだったってことですか？思い込みなんですか？まじですか？
公理がすべて真になるような解釈がモデルですよね？
そういえば、明らかに真になりそうだと思って、実際にそうなるかは確かめたことがありません。
本にも当然のように、次がモデルとなる、とか書かれていたし・・・。
ちょっとやってみます。
- 60 名前：伊丹公理 [04/12/10 20:26:25]
- 正しいと信じられては居るが
証明は無い。
- 61 名前：１３２人目の素数さん mailto:sage [04/12/10 21:46:00]
- >>50
> 一階の自然数論はモデルをもつ。
集合論を仮定すれば正しい。
本に当然のように正しいと書いてあるのも、この仮定の下での議論。
> みんなが自然数論の通常のモデルとか超準モデルとか言っているのは
> 全部嘘っぱちだったってことですか？
これも、集合論を仮定して議論しています。
- 62 名前：１３２人目の素数さん mailto:sage [04/12/11 05:40:29]
- >>59
モデルになるのは\omega とか
あるいはそれにさらに手を加えて作ったモデルじゃないんでしょうか？
まあ集合論が矛盾していたら
モデルも何もないんですけどね。
（そういう概念自体が成立しない）
- 63 名前：１３２人目の素数さん mailto:age [04/12/11 05:47:41]
- しかし、伊丹公理って基礎論の知識もある程度はあるんだ。凄いな
>>56
RobinsonのQとかいう奴です。第一不完全性定理の証明で必要な
最低限度の公理を集めたもので、こういう公理です
PA - （数学的帰納法の公理図式） + （∀x(x≠0→∃y( S(y) = x ) ) ）
要するに、帰納法の公理は無くとも第一不完全性
（つまり命題の集合の中での定理の極大性）は証明できる、ということね。
Robonsonは超準解析を殆ど一人で作ったあのRobonsonです。
（↑…でいいよね？第十問題の女性の方じゃないよね？）
ってか自然数の標準モデルの定義
（Th(\mathfrak{N]\mathbb(N)の定義ならなお嬉しい）
ご存知なら誰か教えて下さいm(_ _)m
- 64 名前：１３２人目の素数さん mailto:sage [04/12/11 07:32:41]
- >>63
> Robonsonは超準解析を殆ど一人で作ったあのRobonsonです。
> （↑…でいいよね？第十問題の女性の方じゃないよね？）
違います。Robinson の Q は Raphael M. Robinson.
Hilbert の第十問題の Julia Robinson とは夫婦だったはず。
超準解析は Abraham Robinson.
- 65 名前：１３２人目の素数さん mailto:sage [04/12/11 07:56:56]
- えー、じゃあRobinsonって基礎論には三人も居るんだ。。。
もうダメポ
- 66 名前：１３２人目の素数さん mailto:sage [04/12/11 10:35:15]
- すると導出原理(resolution principle)のRobinsonはどのRobinsonなんだ？
- 67 名前：１３２人目の素数さん mailto:sage [04/12/11 18:42:19]
- >>65
Raphael は基礎論にも関心が深かったけど，専門は解析です．
>>66
それは John Alan Robinson というまた別の Robinson だったりする．ﾏｷﾞﾗﾜｼｲ('A`)
- 68 名前：１３２人目の素数さん [04/12/11 19:18:49]
- >>67
裸はエロ？
- 69 名前：１３２人目の素数さん [04/12/11 19:19:35]
- 裸婦はエロ
- 70 名前：BlackLightOfStar ◆ifsBJ/KedU [04/12/11 20:32:33]
- Re:>68-69 ここはどこ？
- 71 名前：１３２人目の素数さん [04/12/11 21:59:55]
- ５９とかです。レスしてくれたみなさんありがとうございます。
>>61
集合論はＺＦのことですか？
また、集合論をどう仮定するんでしょうか。無矛盾性を仮定するんですか？
でも、集合論を仮定すれば、どうしてモデルをもつことの証明ができるんですか？
モデルを持つことの証明の困難さの根源は集合論の性質（無矛盾性？）にあるんですか？
だとすると、それはなぜですか？モデルには集合論の言葉が使われるからですか？
あれだけのために、ＺＦのいろんな公理は不必要だろうから、違いますよね？
？マークばっかですみません。教えてください。
>>62
オメガって何ですか。順序数のオメガですか。
後半部分も理解できません。モデルと集合論はどう関係しているんですか。
モデルのどういった部分に集合論が関わるんですか。
つか、なんでこんな重要なことが本に書いてないんですか？
読んだ本がわるかったですか？分かりやすい説明がある本ないですか？
- 72 名前：１３２人目の素数さん mailto:sage [04/12/11 22:23:09]
- ttp://wwwhep.s.kanazawa-u.ac.jp/users/tomoya/sikatan/occult/daigo/19.htm
こんなページを発見しました。
今までの話と真逆のことが書いてあります。
でも、選択公理は独立だそうですから、
もしモデル理論が正しければ、ＺＦ集合論は矛盾している
これは間違ってますよね？
- 73 名前：１３２人目の素数さん mailto:sage [04/12/11 23:01:40]
- Con(AC)∧Con(¬AC)が矛盾すると勘違いしている
アフォのページですな
- 74 名前：１３２人目の素数さん mailto:sage [04/12/11 23:26:16]
- やっぱりそうですか。びっくりしました。
ありがとうございます。71もどなたか助言ください。（最後以外を特に教えて欲しいです）
- 75 名前：１３２人目の素数さん mailto:sage [04/12/12 00:22:34]
- >>71
> 集合論をどう仮定するんでしょうか。無矛盾性を仮定するんですか？
>> 一階の理論はモデルをもてば無矛盾。
>> 一階の自然数論はモデルをもつ。
>> 一階の自然数論は無矛盾。
これらを、集合論の命題として表現し、集合論の公理の下で証明する。
> 集合論を仮定すれば、どうしてモデルをもつことの証明ができるんですか？
無限公理があるので楽勝。
>>72
検索した文書の素性を確かめることができない人は、検索をしても時間の無駄だと思う。
- 76 名前：１３２人目の素数さん mailto:sage [04/12/12 02:16:13]
- >>75
ありがとうございます。
モデルをもつことの証明には無限集合の存在が重要ということですか。
その理由もどうやって集合論の言葉で書くのかも良く分かりませんね。
たぶんここで説明していただくには膨大すぎるでしょうから、
そういう話が載っている本などをご紹介していただければ嬉しいのですが。
（なるたけ易しく書かれたものなら、なおありがたいです）
- 77 名前：１３２人目の素数さん mailto:sage [04/12/12 13:35:00]
- >そういえば、明らかに真になりそうだと思って、実際にそうなるかは確かめたことがありません。
>本にも当然のように、次がモデルとなる、とか書かれていたし・・・。
ぶっちゃけ、反証待ち、それまでは、公然と材料として用いる、ということでよくね？
- 78 名前：１３２人目の素数さん mailto:age [04/12/12 23:45:47]
- >>67
そういうのってどうやって調べたら良いんだろう？
やっぱ原論文の著者名を確認したりしないと駄目？
>>71
集合論が意味を持った理論なら、集合論の言葉を用いて、
「理論Tのモデル」とかの術語が定義できて、
「ある構造（というか集合）がある理論のモデルになっていること」が
定義でき、証明できる、という事です。
究極的には記号の羅列と見做せるような形式的な理論が意味を持つのはなぜだろう？
そもそも本当にそのような理論が意味を持つのだろうか？とかいった疑問は、
分析哲学とかを勉強してくださいです。その種の問題意識は数学の範疇ではありません。
>>72
書いてる人が全然分かってないだけです。不完全性定理とかも多分巷間の
トンデモ本程度の理解しかないんでしょう。
ってか誰かこの金沢大学の教員も大変だな。。。
こんなDQNも教えないといけないなんて
- 79 名前：１３２人目の素数さん mailto:sage [04/12/13 23:41:19]
- 数学基礎論というのはドイツ語 (それもテクニカルターム) からの翻訳でしょ。
- 80 名前：１３２人目の素数さん [04/12/14 21:00:57]
- 数学を発展させたのはデカルト、ライプニッツ、フレーゲ、ラッセル、
ウィトゲンシュタイン、ポパー等の哲学者です
- 81 名前：１３２人目の素数さん [04/12/15 19:43:30]
- 嘘コケ馬鹿
- 82 名前：１３２人目の素数さん [04/12/15 20:55:15]
- >>72
> 一方、ＡＣと¬ＡＣのうちどちらかは偽の命題です。
> このとき、２つの数学理論ＺＦ＋ＡＣとＺＦ＋¬ＡＣのうちどちらかは、
> 偽の命題を仮定として有する矛盾した数学理論です。
> したがって、ＺＦ＋ＡＣとＺＦ＋¬ＡＣがともに無矛盾ということはあり得ず
- 83 名前：１３２人目の素数さん [04/12/16 08:08:27]
- >>78
ん？ページを辿るとこんな文章があるが･･･
wwwhep.s.kanazawa-u.ac.jp/users/tomoya/sikatan/occult/daigo/daigo.htm
>これは、数年前にうちの研究室に 匿名で 郵送されてきた文書です。
- 84 名前：78 mailto:sage [04/12/16 09:37:22]
- まあじゃあ匿名で郵送した人
（か元の文章を書いた人）が分かってないんでしょう
72の書き方はミスリーディングだと思う
- 85 名前：１３２人目の素数さん mailto:sage [04/12/16 10:11:45]
- >>79
つか数学基礎論は日本でも死語
数学者以外の時代遅れの素人が用いてるだけ
- 86 名前：１３２人目の素数さん mailto:sage [04/12/16 10:24:40]
- うそつけ
- 87 名前：１３２人目の素数さん mailto:sage [04/12/16 11:17:03]
- ってか基礎論自体が時代錯（りゃ
- 88 名前：１３２人目の素数さん mailto:sage [04/12/16 21:57:23]
- >>85はさすがに大嘘だな
- 89 名前：１３２人目の素数さん mailto:sage [04/12/16 23:13:37]
- 岩波数学辞典の数学基礎論の項目の記述がなかなか面白い。
この意味で使っている人はどれくらいいるのか。
- 90 名前：１３２人目の素数さん mailto:sage [04/12/17 03:26:27]
- 自分の専門分野に「数学基礎論 foundations of mathematics」を挙げている数学者。
Harvey Friedman
www.math.ohio-state.edu/people/display/display.php?ID=104
Stephen Simpson
www.math.psu.edu/simpson/foundations/
Edward Nelson
www.math.princeton.edu/~nelson/
田中一之
www.math.tohoku.ac.jp/~tanaka/myself.html
- 91 名前：１３２人目の素数さん mailto:sage [04/12/17 03:30:30]
- Simpson の主張する「数理論理学」と「数学基礎論」との区別
www.cs.nyu.edu/pipermail/fom/2001-January/004712.html
- 92 名前：１３２人目の素数さん [04/12/21 21:23:14]
- 質問させてください。
某板棒スレで意見が分かれています。
>ふと思ったがL9999999999999^99999999999999って実際どのくらいの値になるの？
>10の14乗に15掛けたくらいかな。まちがてるとおもうけどそんなもん。
>10の14乗を15乗したくらいだろ
>(10^13-1)^(10^14-1)と考えて二項展開どうかなって思ったけど
>対数をとれば桁数はでるんじゃない？
>それでやったんだけど間違ってるかな、9の数かぞえまちがえたかな。
>普通に10^{13*(10^14-1)}=10^1299999999999987くらいになる希ガス
数学板的な正解はどうなんでしょう？
- 93 名前：１３２人目の素数さん [04/12/21 22:00:57]
- >>78
７１とかです。遅レスですが、ありがとうございます。
集合論のなかでモデル理論を展開できるということだったんですね。
そういうことの具体的な話は細かく言うとどういう分野に該当するんでしょうか。
少し見た限りでは普通の集合論の本にもモデル理論の本にも載っていないようでした。
（といっても、まだ集合論とかほとんど分からないので、実際に学べるのはもう少し先になりそうですが・・）
何か哲学では、公理の無矛盾性を保証するためには構造が存在しなければならないが、
現実世界に無限的構造の存在を立証することは難しい、といわれたりするそうですが、
なんで現実世界に構造（モデルのことですよね？）が存在すればよいのか、
現実世界にモデルのような抽象概念が存在するとはどういったことなのか、よくわかりませんでした。
基礎論で業績のあるひとでも、こういう哲学の話に興味を持つということからすると、
何かのもっともな根拠があるのに、ぼくが気づいていないだけでしょうか。
- 94 名前：１３２人目の素数さん mailto:sage [04/12/21 22:07:38]
- あと、自然数が存在するとか、そうではなくてオメガ列という構造が存在するんだとか、
哲学では言われるようですが、なんで存在を現実世界の意味で捉えるのか良く分かりませんでした。
想定できる、と言っても同じことだと思うんですが。
ペガサスを想像（想定）できますが、べつに現実に存在する必要はないですよね・・。
スレ違いだったらごめんなさい。
ここの見識のある皆さんならどう思われるのか興味があるので・・。
- 95 名前：１３２人目の素数さん mailto:sage [04/12/21 22:10:42]
- >>93
根拠というのは問題意識の源泉というような意味合いで用いました。
どういう発想なのだろう、ということです。
- 96 名前：１３２人目の素数さん [04/12/21 22:31:15]
- 体 From：はな(大学3)
04/12/21(Tue) 21:53:12 No. 16081 / 34 [RES]
からだの理論を1階の理論として表しなさい
- 97 名前：１３２人目の素数さん mailto:sage [04/12/22 00:39:27]
- そういうことの具体的な話
おまいさんが先ずもっと具体的に分かるように書いてくれ
意味が分からん
あと哲学は、漏れも知らんので哲学板の分析哲学スレにいけ
∀∃ 分析哲学総合III ∃∀
academy3.2ch.net/test/read.cgi/philo/1087594214/l50
- 98 名前：１３２人目の素数さん [04/12/22 22:26:39]
- >>97
すんません。
集合論を仮定すればモデルの存在が証明できるという話についての具体的な議論を知りたいんです。
レスをお借りすれば、↓のような事柄です。よろしくお願いします。
集合論の言葉を用いて、
「理論Tのモデル」とかの術語が定義できて、
「ある構造（というか集合）がある理論のモデルになっていること」が
定義でき、証明できる、という事です。
- 99 名前：１３２人目の素数さん mailto:sage [04/12/22 22:27:42]
- （たぶん今のぼくにはこれ以上具体的に書くことはできないと思います。何とか意を汲み取ってやって下さい・・）
- 100 名前：１３２人目の素数さん mailto:sage [04/12/22 22:28:00]
- >>99
- 101 名前：１３２人目の素数さん mailto: [04/12/23 19:37:29]
- どなたか、わかる方、お教えください。
- 102 名前：９８とか [04/12/24 15:53:38]
- （紛らわしいひとですね・・。９２の中の人ですか・・。）
前原さんの本のクライゼルの注意の箇所をつまみ読みしたんですが、
ロッサーの論理式？を用いて1=0が証明できないことを表した論理式
が証明可能になるのは、無矛盾性の仮定の下でですよね？
実際、その証明に使われている定理のなかに無矛盾性を仮定して導かれている定理があるので、
無矛盾性を仮定しているように思われるんですが、前原さんは言及していないことが気になります。
他の定理では、いちいち無矛盾性の仮定に言及してあるんで、余計に気がかりです。
しかも、別の部分では、無矛盾性を表すロッサー型の論理式は「つねに証明できる」と書かれています。
ここには、どういった意図があるんですか？ぼくは何か愚かな勘違いを犯してるんですか？
助言お願いしたいです。
- 103 名前：１３２人目の素数さん mailto:sage [04/12/24 16:00:57]
- あと、他の本でクライゼルの注意への言及があるものは見たことがないんですが、
たいして重要なことではないと考えるひとが多いのですか？
素人目にはびっくり仰天の話だと思うんですが・・・。
それにこの注意を考慮すると、「無矛盾性は体系内で証明できない」
と無制限に主張することはできないと思うのですが、
実際には「」のような書き方がなされていることが多いですよね？
これはどういう観点からなんですか？
いろいろと質問しましたが、部分的にでも答えてもらえれば、ありがたいです。
- 104 名前：１３２人目の素数さん mailto:sage [04/12/24 16:43:22]
- >>102
＞前原さんの本のクライゼルの注意の箇所をつまみ読みしたんですが、
残念ですがそれでは理解できないでしょう。
＞ロッサーの論理式？を用いて1=0が証明できないことを表した
＞論理式が証明可能になるのは、無矛盾性の仮定の下でですよね？
私の懸念は的中しました。上の質問の答えは「いいえ」です。
そもそも無矛盾でないなら何でも証明できますから。
＞無矛盾性を表すロッサー型の論理式は
＞「つねに証明できる」と書かれています。
ええ、その通りです。
＞ここには、どういった意図があるんですか？
なんの意図もありません。正しいから書いたのでしょう。
＞ぼくは何か愚かな勘違いを犯してるんですか？
愚かかどうかはともかくとして勘違いをしています。
断言します。
- 105 名前：１３２人目の素数さん mailto:sage [04/12/24 16:51:23]
- ＞あと、他の本でクライゼルの注意への言及があるものは
＞見たことがないんですが、
林晋氏の「パラドックス」には書いてあります。
ただしクライゼルの名前は出していませんが。
＞たいして重要なことではないと考えるひとが多いのですか？
重要です。ただし”数学”としてではなく。
＞素人目にはびっくり仰天の話だと思うんですが・・・。
本当に理解すればあなたの心臓が止まるかもしれません。
＞それにこの注意を考慮すると、
＞「無矛盾性は体系内で証明できない」
＞と無制限に主張することはできないと思うのですが、
そもそも、無矛盾性を体系内で表現できると単純素朴に
考えることができません。林晋氏が「パラドックス」で
いいたかったのはそういうことです。
- 106 名前：１３２人目の素数さん mailto:sage [04/12/24 16:59:36]
- >>104-105
早速のレスありがとうございます。
レスを手がかりに考え直してみます。
- 107 名前：１３２人目の素数さん mailto:sage [04/12/24 16:59:45]
- >>104
でも勘違いなのでしょうか？
「無矛盾性は体系内で証明できない」というとき、どう書くか?
を問題としなければ、矛盾していることがでてきても勘違いじゃ
ないんじゃないでしょうか?
- 108 名前：１３２人目の素数さん mailto:sage [04/12/24 17:01:41]
- 確かに無矛盾性の過程は要りませんでした。阿呆でした。逝ってきます。
- 109 名前：１３２人目の素数さん mailto:sage [04/12/24 17:03:36]
- ＞実際には「無矛盾性は体系内で証明できない」
＞のような書き方がなされていることが多いですよね？
まあ、そうですね。
＞これはどういう観点からなんですか？
例えばゲーデルの定義したBewとロッサー型のBewは
体系が無矛盾であるなら同じ意味ですが、両者の
同値性は、体系内では証明できません。
これがクライゼルの指摘からみちびかれる結論の
真に驚愕すべき点です。
- 110 名前：１３２人目の素数さん mailto:sage [04/12/24 17:10:46]
- >>109
林晋は証明論による無矛盾性証明が、クライゼルが指摘するような
別のBew（カットのない証明）を利用している点を問題だと指摘している。
ただし、この場合にはカットのある証明から、それ抜きの証明への
変換を用いており、その手順の停止性の証明は体系内ではできない
ので、ゲーデルの第二不完全性定理に抵触するわけではない。
- 111 名前：１０２とか mailto:sage [04/12/24 17:14:23]
- 帰ってきました。ちなみに１０７はぼくじゃないです。
＞そもそも、無矛盾性を体系内で表現できると単純素朴に
＞考えることができません。
そういえば、前原さんも「数値別に正確に表現しているわけではない」と書いておられました。
林さんの本も読んでみます。いろいろとありがとうございました。
どなたとどなたが同一なのか分かりませんが、レスをくれた方にはすべて感謝したいです。
（なんかもう110さんみたいな賢者がでてくるなんて、2chはすごすぎる・・・）
- 112 名前：１３２人目の素数さん mailto:sage [04/12/24 17:25:27]
- >>107
＞どう書くか? を問題としなければ、
そう。まさにそこが問題であると林晋は言っている。
しかし、それはもはや”数学”の問題ではない。
はっきりいえば、数学よりももっと根本的な
言語とそれを用いる自分にかかわる”哲学”
の問題である。
- 113 名前：１３２人目の素数さん mailto: [04/12/29 05:50:41]
- どなたか、わかる方、お教えください。
- 114 名前：１３２人目の素数さん [05/01/02 23:36:49]
- 651
- 115 名前：１３２人目の素数さん [05/01/05 13:15:52]
- 自然数の和と積に関する理論（いわゆる、ロビンソン算術）を作りたい、と考えて、
まず、語彙、項、論理式の定義を設定する、と、
これで、論理式はつくることができる、と、
で、その論理式が、自然数の和と積に関する一連の内容を表現できるように、と、モデルを設定する、と、
これで、十分なんじゃないか、と、
なんで、公理系をつくるんだろう？、と、
具体的に、論理式の集まりを把握したい、という目的とか、
その理論の意味論的完全性を示せば、その理論の公理系で証明できることを示すことによって、
すなわち、（意味論的に）真である、が言える（別にいらんなぁ）、とか、
そこらへんの目的からっすかね？
誰か詳しい人、教えてください
- 116 名前：１３２人目の素数さん mailto:sage [05/01/05 13:25:25]
- >>115
意味不明。公理系も無いのに、モデルが作られるか。
- 117 名前：１３２人目の素数さん mailto:sage [05/01/05 15:15:51]
- >>116
確かに、115のいうモデルは、数理論理学でいう
それとは異なるようだね。
115は漫然とモデルという言葉を使わずに
全く別の言葉で説明するように。
- 118 名前：１３２人目の素数さん mailto:sage [05/01/05 15:20:25]
- ところで115は、ロビンソン算術の命題が
どんなものか知っているのかな？
- 119 名前：１３２人目の素数さん mailto:sage [05/01/05 15:29:38]
- １１５はのいうモデルはモーデルのことだな。
- 120 名前：１３２人目の素数さん [05/01/05 16:08:38]
- >>116
なんといったらいいのか、意味論的な諸設定とでも、いいましょうか、
115で言いたかった内容を、もう一度繰り返すと、
まず、語彙、項、論理式の定義を設定する、と、
これで、
#a＋##a＝###a
# 後続者関数、
項、論理式の定義は、ロビンソン算術とよばれているもののそれと同じいうことで
という論理式がつくれる、と、
で、
これに
一足す二は三
という内容をもたせるべくして、意味論的な諸設定（論議領域に自然数を設定したり、個体定項aに自然数0割り当てたり、関数に付値したり、・・ ここんところを、115では、モデルという語を用いてあらわしました）、を設定する、と、
これで、いいじゃん、と、（他の命題の表現についても、同様。で、これをもって、自然数の和と積に関する理論、ということでいいじゃん、と）
以下、115の内容へと続く
- 121 名前：１３２人目の素数さん mailto:sage [05/01/05 17:10:36]
- ＞論議領域に自然数を設定したり
簡単にいうけど、そもそも自然数全体が
無限個あるってことが問題なわけなんだけど。
単純に列挙なんかできないよ。どうするの？
- 122 名前：１３２人目の素数さん mailto:sage [05/01/05 20:51:33]
- つーか、だって、それが、一階の理論の意味論なんやねんもん、
そんなところ批判されたって、言葉につまるというか、
最初に言い出した奴に言ってくれというか、
違うねん、そういうところにひっかかると、話が遠ざかってしまう。
そうじゃなくて、
ロビンソン算術の意味論は、上でも言ってるように、論理式に、意味みたいなもん、与えてくれてる。
これは、この理論が、自然数の和と積というものを表現しようとしているかぎり必要、ということはわかる。
俺が聞いてるのは、じゃあ、構文論とか、形式的体系（公理系）は、自然数の和と積を表現しようとしたやつに、
いったい、何を与えてくれてんねん、ということ、
- 123 名前：115とか mailto:sage [05/01/05 21:15:36]
- ごめんごめんごめんごめん
自爆、
よくよく考えてみると、いるな、公理系、
上での書き方もまずかった、
なんか、標準モデルひとつおいて、意味論、みたいな書き方してる
あほや、俺
ごめん、質問、なかったことにしてください・・逝ってくる・・
- 124 名前：１３２人目の素数さん [05/01/07 17:01:17]
- 自然数の公理系Nが無矛盾であるなら、その肯定形も否定形もNで証明できないようなNの閉じた式が存在する
ということらしいですが、
その肯定形も否定形もNで証明できないようなNの閉じた式を仮定された論理式としてその形式的体系に設定した場合、
形式的体系の無矛盾性は崩れて、Nの任意の論理式を演繹することができる、ということであってますか？
- 125 名前：１３２人目の素数さん [05/01/07 17:28:26]
- >>124
矛盾することはない。
ふたたび別の論理式が決定不能になる。（証明を学べば簡単に分かる）
- 126 名前：１３２人目の素数さん mailto:sage [05/01/07 18:24:07]
- >>125さんの言うとおりです
Nは公理を勝手に増やしたり増やしたりしたらN'≠Nになってしまいます。
つまり、証明能力が変わってしまうと言うことです。当たり前ですね。
でもN'にも（一気に無限種類の公理を考えたりする荒業をしなければ）
閉論理式でN'から独立なものは存在します。（NにN'を代入するだけ）
- 127 名前：１３２人目の素数さん mailto:sage [05/01/07 19:08:16]
- >>125
>>126
ある「その肯定形も否定形もNで証明できないようなNの閉じた式」を、形式的体系に加えようとも、
まだ、他に、その形式的体系にとって、「その肯定形も否定形もNで証明できないようなNの閉じた式」はある、ということでしょうか？
- 128 名前：１３２人目の素数さん mailto:sage [05/01/07 19:51:01]
- うん。
N'で証明できない式はNでも証明できないからね。
ちなみに、
公理の集合Σからφが証明できない
⇔Σ∪{¬φ}は無矛盾な公理系
だけどこういうことはご存知ですよね？
- 129 名前：１３２人目の素数さん mailto:sage [05/01/07 20:09:15]
- Σの無矛盾性を仮定するのを忘れておったわ
ハァッハッハハハ
|
 |
