04/10/13 18:31:09
なんだ結局単発質問スレか
3:（・人ζもみもみ ◆Momi/T3ouE
04/10/13 19:34:00
駄スレ保守
4:１３２人目の素数さん
04/10/13 21:35:07
>>1
それ、何ページ？
5:１３２人目の素数さん
04/10/13 21:46:16
>>1
∀ξ（ξ=ξ）の誤植だと思う。
6:1
04/10/13 22:41:17
>>4
P322です。
前後の文脈を読んだ結果、おそらく、∀ξ（ξ=ζ）の、ζに関する条件が、はしょられてる？結果の、混乱だったのではないだろうか、と考えています。
間違っていたら、ぜひ訂正していただきたいのですが、
おそらく、
∀ξ（ξ=ζ）という公理図式が意味するところは、
「ξに入る個体変項」となんらかの関係をもった「ζに入る個体変項」を、∀ξ（ξ=ζ）という公理図式に代入してつくった論理式を、公理と用いることができますよ、
ということなんじゃないだろうか、と考えています。
7:１３２人目の素数さん
04/10/13 22:56:55
うはー
誤植ﾏｼﾞ勘弁
8:1
04/10/15 14:41:51
おさわがせしました。
∀ξ（ξ=ξ）の誤植みたいです。
あと、その次につづく公理
(ξ=ζ)→(ρ(・・ξ・・)=(ρ(・・ζ・・)) ρはｎ変数関数記号をあらわす図式文字
ただし、ρは任意のｎ変数関数記号で、ρ(・・ξ・・)は項ρ(・・ξ・・)の個体変数ξの現れの１つ以上（いくつでもよい）をζで置き換えてえられる項とする
について、
本に例などがなく、つまるところ、これは、何だ？、ということで悩んでいます。
どなたか、おわかりの方、この公理図式からつくることができる論理式の、具体的な例を、挙げていただけないでしょうか。
9:１３２人目の素数さん
04/10/15 14:44:44
862
10:1
04/10/15 15:56:03
ちょっと、わかったかも、
間違っていたら訂正してください
ｓ 後続者関数
+ 前の項と後ろの項の和を割り当てる関数
として、
ｓ０＋ｓ０=ｓｓ０
と
ｓ０+ｓ０+ｓ０+ｓ０＝ｓ０+ｓ０+ｓ０+ｓ０
から
ｓ０+ｓ０+ｓ０+ｓ０＝ｓ０+ｓｓ０+ｓ０
が言える、とか、そういう内容のこと言ってるのかな？これは
11:１３２人目の素数さん
04/10/15 16:00:00
あんた質問ばっかだね
12:１３２人目の素数さん
04/10/15 23:29:01
>>8
ゲンツェンの自然推論というのがあるが、
(ξ=ζ)→(ρ(・・ξ・・)=(ρ(・・ζ・・))
というのは、等号の「導入規則」である
∀ξ（ξ=ξ）
に「共役」な（一意的に定まる）等号の「消去規則」だ。
13:１３２人目の素数さん
04/10/16 09:23:47
∀x(King はまっとうな人間である ⇒ 1 ≠ 0) は正しいんですか
14:あぼーん
あぼーん
あぼーん
15:LettersOfLiberty ◆rCz1Zr6hLw
04/10/16 14:18:32
Re:>14 捏造すんな。
16:１３２人目の素数さん
04/10/19 03:32:16
>>13
どっちかというと
King はまっとうな人間である ⇒ 0 ≠ 0
が正解かな。
17:LettersOfLiberty ◆rCz1Zr6hLw
04/10/19 11:40:39
Re:>16 お前に何が分かるというのか？
18:高校生
04/10/21 22:42:26
質問です。
東北大の田中一之教授はどのような研究をされているか誰かご存じですか。
名古屋大理学部では基礎論の講座はあるのでしょうか。
19:１３２人目の素数さん
04/10/21 23:00:55
King はまっとうな人間である ⇒ 0 ≠ 0
大正解
20:１３２人目の素数さん
04/10/21 23:27:08
CoiKing
21:１３２人目の素数さん
04/10/22 00:28:37
スイングジャズの代名詞
KingKingKing
22:LettersOfLiberty ◆rCz1Zr6hLw
04/10/22 09:10:17
Re:>19 お前に何が分かるというのか？
23:１３２人目の素数さん
04/10/22 13:46:06
King はまっとうな人間である ⇒ 1 ≠ 1
大正解
24:LettersOfLiberty ◆rCz1Zr6hLw
04/10/22 16:50:34
Re:>23 お前に何が分かるというのか？
25:１３２人目の素数さん
04/10/22 19:25:59
順序列というのがよくわかりません・・・・・
あと、集合AのN乗積というのもよくわからないのですが・・どういう意味なのでしょうか？
26:１３２人目の素数さん
04/10/22 20:09:26
>名古屋大理学部では基礎論の講座はあるのでしょうか。
あってもなくても大抵その前に落ちこぼれるから心配なし。
27:１３２人目の素数さん
04/10/22 21:22:02
Porca King
28:『数学基礎論講義』で勉強中です
04/10/28 05:43:08
幾つか質問させてください。
p.87の議論で、
\mathbf{Prov}_T(n,m)
と
\mathfrac{N}\models \text{Prov}_T(\overline{n},\overline{m})
ではどんな意味の違いがあるんでしょうか？（煩雑な書き方ですみません）
そもそも\mathfrac{N}の定義がよくわからない
（というより書いてある本を見たことが無い）のですが……
不完全性定理の証明に必要な標準モデル固有の性質は
有限個しかないと思うのですが。
標準モデルの特徴づけなら何かの本に書いてあったような気もするのですが……
29:１３２人目の素数さん
04/10/28 23:42:41
数学基礎論って数学入門のことと思ってた
30:28
04/10/29 00:16:01
あ、誰か教えてくれたか？と思ったらｗ
\mathfracは\mathfrakの間違いね
31:１３２人目の素数さん
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
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:１３２人目の素数さん
04/11/06 02:27:06
さて、今から、図書館から借りた『二十世紀数学思想』でも読みますか
この本二十世紀数学といいながら基礎論のことしか
書いてないような気がするけど漏れには好都合ｗ
34:１３２人目の素数さん
04/11/07 02:24:40
>>32
出版の時期から考えて、著者達が LATeX2ε に乗り換えていたかどうかは微妙。
35:質問！
04/11/07 02:32:14
P=NP 問題って、なんですか？
36:１３２人目の素数さん
04/11/08 04:37:18
>>34
なるほど、だからあんなに書き方が微妙なんですね。納得。
37:１３２人目の素数さん
04/11/09 12:52:57
>>35
ペニスはぬるぽかという問題です。
38:１３２人目の素数さん
04/11/09 21:16:08
>>35
ペニスはぬるぽじゃないっていう意見が支持されてるよ！
39:あぼーん
あぼーん
あぼーん
40:１３２人目の素数さん
04/11/16 22:33:57
ぬれぽ
41:１３２人目の素数さん
04/11/16 22:40:31
ぬるーつポンチ
42:あぼーん
あぼーん
あぼーん
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:１３２人目の素数さん
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:１３２人目の素数さん
04/12/09 11:26:36
ちょっとこの本持って無いから適当なレスしか
出来ないけど、多分間違ってないと思うよ？
具体的にどういう風に書き直されるべきだ、と思うんですか？
47:１３２人目の素数さん
04/12/09 13:08:57
∀ｘ（Aｘ→Bｘ） 前提
∀ｘ（Aｘ→Bｘ）→（（A（ある項）→B（ある項）） A4
というような証明の過程を見たときに、
あれ、ｘ、縛られてるじゃん、というように思いました。
48:１３２人目の素数さん
04/12/09 13:27:54
>>45
「A にふくまれる」とか「A には」と書いてあるところでは、
A だけを独立して考えていて、A がどのような論理式の部分
論理式であるかは考えていません。
49:１３２人目の素数さん
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:１３２人目の素数さん
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:１３２人目の素数さん
04/12/10 21:46:00
>>50
> 一階の自然数論はモデルをもつ。
集合論を仮定すれば正しい。
本に当然のように正しいと書いてあるのも、この仮定の下での議論。
> みんなが自然数論の通常のモデルとか超準モデルとか言っているのは
> 全部嘘っぱちだったってことですか？
これも、集合論を仮定して議論しています。
62:１３２人目の素数さん
04/12/11 05:40:29
>>59
モデルになるのは\omega とか
あるいはそれにさらに手を加えて作ったモデルじゃないんでしょうか？
まあ集合論が矛盾していたら
モデルも何もないんですけどね。
（そういう概念自体が成立しない）
63:１３２人目の素数さん
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:１３２人目の素数さん
04/12/11 07:32:41
>>63
> Robonsonは超準解析を殆ど一人で作ったあのRobonsonです。
> （↑…でいいよね？第十問題の女性の方じゃないよね？）
違います。Robinson の Q は Raphael M. Robinson.
Hilbert の第十問題の Julia Robinson とは夫婦だったはず。
超準解析は Abraham Robinson.
65:１３２人目の素数さん
04/12/11 07:56:56
えー、じゃあRobinsonって基礎論には三人も居るんだ。。。
もうダメポ
66:１３２人目の素数さん
04/12/11 10:35:15
すると導出原理(resolution principle)のRobinsonはどのRobinsonなんだ？
67:１３２人目の素数さん
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:１３２人目の素数さん
04/12/11 22:23:09
URLﾘﾝｸ(wwwhep.s.kanazawa-u.ac.jp)
こんなページを発見しました。
今までの話と真逆のことが書いてあります。
でも、選択公理は独立だそうですから、
もしモデル理論が正しければ、ＺＦ集合論は矛盾している
これは間違ってますよね？
73:１３２人目の素数さん
04/12/11 23:01:40
Con(AC)∧Con(￢AC)が矛盾すると勘違いしている
アフォのページですな
74:１３２人目の素数さん
04/12/11 23:26:16
やっぱりそうですか。びっくりしました。
ありがとうございます。71もどなたか助言ください。（最後以外を特に教えて欲しいです）
75:１３２人目の素数さん
04/12/12 00:22:34
>>71
> 集合論をどう仮定するんでしょうか。無矛盾性を仮定するんですか？
>> 一階の理論はモデルをもてば無矛盾。
>> 一階の自然数論はモデルをもつ。
>> 一階の自然数論は無矛盾。
これらを、集合論の命題として表現し、集合論の公理の下で証明する。
> 集合論を仮定すれば、どうしてモデルをもつことの証明ができるんですか？
無限公理があるので楽勝。
>>72
検索した文書の素性を確かめることができない人は、検索をしても時間の無駄だと思う。
76:１３２人目の素数さん
04/12/12 02:16:13
>>75
ありがとうございます。
モデルをもつことの証明には無限集合の存在が重要ということですか。
その理由もどうやって集合論の言葉で書くのかも良く分かりませんね。
たぶんここで説明していただくには膨大すぎるでしょうから、
そういう話が載っている本などをご紹介していただければ嬉しいのですが。
（なるたけ易しく書かれたものなら、なおありがたいです）
77:１３２人目の素数さん
04/12/12 13:35:00
>そういえば、明らかに真になりそうだと思って、実際にそうなるかは確かめたことがありません。
>本にも当然のように、次がモデルとなる、とか書かれていたし・・・。
ぶっちゃけ、反証待ち、それまでは、公然と材料として用いる、ということでよくね？
78:１３２人目の素数さん
04/12/12 23:45:47
>>67
そういうのってどうやって調べたら良いんだろう？
やっぱ原論文の著者名を確認したりしないと駄目？
>>71
集合論が意味を持った理論なら、集合論の言葉を用いて、
「理論Tのモデル」とかの術語が定義できて、
「ある構造（というか集合）がある理論のモデルになっていること」が
定義でき、証明できる、という事です。
究極的には記号の羅列と見做せるような形式的な理論が意味を持つのはなぜだろう？
そもそも本当にそのような理論が意味を持つのだろうか？とかいった疑問は、
分析哲学とかを勉強してくださいです。その種の問題意識は数学の範疇ではありません。
>>72
書いてる人が全然分かってないだけです。不完全性定理とかも多分巷間の
トンデモ本程度の理解しかないんでしょう。
ってか誰かこの金沢大学の教員も大変だな。。。
こんなDQNも教えないといけないなんて
79:１３２人目の素数さん
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
ん？ページを辿るとこんな文章があるが･･･
URLﾘﾝｸ(wwwhep.s.kanazawa-u.ac.jp)
>これは、数年前にうちの研究室に 匿名で 郵送されてきた文書です。
84:78
04/12/16 09:37:22
まあじゃあ匿名で郵送した人
（か元の文章を書いた人）が分かってないんでしょう
72の書き方はミスリーディングだと思う
85:１３２人目の素数さん
04/12/16 10:11:45
>>79
つか数学基礎論は日本でも死語
数学者以外の時代遅れの素人が用いてるだけ
86:１３２人目の素数さん
04/12/16 10:24:40
うそつけ
87:１３２人目の素数さん
04/12/16 11:17:03
ってか基礎論自体が時代錯（りゃ
88:１３２人目の素数さん
04/12/16 21:57:23
>>85はさすがに大嘘だな
89:１３２人目の素数さん
04/12/16 23:13:37
岩波数学辞典の数学基礎論の項目の記述がなかなか面白い。
この意味で使っている人はどれくらいいるのか。
90:１３２人目の素数さん
04/12/17 03:26:27
自分の専門分野に「数学基礎論 foundations of mathematics」を挙げている数学者。
Harvey Friedman
URLﾘﾝｸ(www.math.ohio-state.edu)
Stephen Simpson
URLﾘﾝｸ(www.math.psu.edu)
Edward Nelson
URLﾘﾝｸ(www.math.princeton.edu)
田中一之
URLﾘﾝｸ(www.math.tohoku.ac.jp)
91:１３２人目の素数さん
04/12/17 03:30:30
Simpson の主張する「数理論理学」と「数学基礎論」との区別
URLﾘﾝｸ(www.cs.nyu.edu)
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:１３２人目の素数さん
04/12/21 22:07:38
あと、自然数が存在するとか、そうではなくてオメガ列という構造が存在するんだとか、
哲学では言われるようですが、なんで存在を現実世界の意味で捉えるのか良く分かりませんでした。
想定できる、と言っても同じことだと思うんですが。
ペガサスを想像（想定）できますが、べつに現実に存在する必要はないですよね・・。
スレ違いだったらごめんなさい。
ここの見識のある皆さんならどう思われるのか興味があるので・・。
95:１３２人目の素数さん
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:１３２人目の素数さん
04/12/22 00:39:27
そういうことの具体的な話
おまいさんが先ずもっと具体的に分かるように書いてくれ
意味が分からん
あと哲学は、漏れも知らんので哲学板の分析哲学スレにいけ
∀∃ 分析哲学総合III ∃∀
ｽﾚﾘﾝｸ(philo板)l50
98:１３２人目の素数さん
04/12/22 22:26:39
>>97
すんません。
集合論を仮定すればモデルの存在が証明できるという話についての具体的な議論を知りたいんです。
レスをお借りすれば、↓のような事柄です。よろしくお願いします。
集合論の言葉を用いて、
「理論Tのモデル」とかの術語が定義できて、
「ある構造（というか集合）がある理論のモデルになっていること」が
定義でき、証明できる、という事です。
99:１３２人目の素数さん
04/12/22 22:27:42
（たぶん今のぼくにはこれ以上具体的に書くことはできないと思います。何とか意を汲み取ってやって下さい・・）
100:１３２人目の素数さん
04/12/22 22:28:00
>>99
101:１３２人目の素数さん
04/12/23 19:37:29
どなたか、わかる方、お教えください。
102:９８とか
04/12/24 15:53:38
（紛らわしいひとですね・・。９２の中の人ですか・・。）
前原さんの本のクライゼルの注意の箇所をつまみ読みしたんですが、
ロッサーの論理式？を用いて1=0が証明できないことを表した論理式
が証明可能になるのは、無矛盾性の仮定の下でですよね？
実際、その証明に使われている定理のなかに無矛盾性を仮定して導かれている定理があるので、
無矛盾性を仮定しているように思われるんですが、前原さんは言及していないことが気になります。
他の定理では、いちいち無矛盾性の仮定に言及してあるんで、余計に気がかりです。
しかも、別の部分では、無矛盾性を表すロッサー型の論理式は「つねに証明できる」と書かれています。
ここには、どういった意図があるんですか？ぼくは何か愚かな勘違いを犯してるんですか？
助言お願いしたいです。
103:１３２人目の素数さん
04/12/24 16:00:57
あと、他の本でクライゼルの注意への言及があるものは見たことがないんですが、
たいして重要なことではないと考えるひとが多いのですか？
素人目にはびっくり仰天の話だと思うんですが・・・。
それにこの注意を考慮すると、「無矛盾性は体系内で証明できない」
と無制限に主張することはできないと思うのですが、
実際には「」のような書き方がなされていることが多いですよね？
これはどういう観点からなんですか？
いろいろと質問しましたが、部分的にでも答えてもらえれば、ありがたいです。
104:１３２人目の素数さん
04/12/24 16:43:22
>>102
＞前原さんの本のクライゼルの注意の箇所をつまみ読みしたんですが、
残念ですがそれでは理解できないでしょう。
＞ロッサーの論理式？を用いて1=0が証明できないことを表した
＞論理式が証明可能になるのは、無矛盾性の仮定の下でですよね？
私の懸念は的中しました。上の質問の答えは「いいえ」です。
そもそも無矛盾でないなら何でも証明できますから。
＞無矛盾性を表すロッサー型の論理式は
＞「つねに証明できる」と書かれています。
ええ、その通りです。
＞ここには、どういった意図があるんですか？
なんの意図もありません。正しいから書いたのでしょう。
＞ぼくは何か愚かな勘違いを犯してるんですか？
愚かかどうかはともかくとして勘違いをしています。
断言します。
105:１３２人目の素数さん
04/12/24 16:51:23
＞あと、他の本でクライゼルの注意への言及があるものは
＞見たことがないんですが、
林晋氏の「パラドックス」には書いてあります。
ただしクライゼルの名前は出していませんが。
＞たいして重要なことではないと考えるひとが多いのですか？
重要です。ただし”数学”としてではなく。
＞素人目にはびっくり仰天の話だと思うんですが・・・。
本当に理解すればあなたの心臓が止まるかもしれません。
＞それにこの注意を考慮すると、
＞「無矛盾性は体系内で証明できない」
＞と無制限に主張することはできないと思うのですが、
そもそも、無矛盾性を体系内で表現できると単純素朴に
考えることができません。林晋氏が「パラドックス」で
いいたかったのはそういうことです。
106:１３２人目の素数さん
04/12/24 16:59:36
>>104-105
早速のレスありがとうございます。
レスを手がかりに考え直してみます。
107:１３２人目の素数さん
04/12/24 16:59:45
>>104
でも勘違いなのでしょうか？
「無矛盾性は体系内で証明できない」というとき、どう書くか?
を問題としなければ、矛盾していることがでてきても勘違いじゃ
ないんじゃないでしょうか?
108:１３２人目の素数さん
04/12/24 17:01:41
確かに無矛盾性の過程は要りませんでした。阿呆でした。逝ってきます。
109:１３２人目の素数さん
04/12/24 17:03:36
＞実際には「無矛盾性は体系内で証明できない」
＞のような書き方がなされていることが多いですよね？
まあ、そうですね。
＞これはどういう観点からなんですか？
例えばゲーデルの定義したBewとロッサー型のBewは
体系が無矛盾であるなら同じ意味ですが、両者の
同値性は、体系内では証明できません。
これがクライゼルの指摘からみちびかれる結論の
真に驚愕すべき点です。
110:１３２人目の素数さん
04/12/24 17:10:46
>>109
林晋は証明論による無矛盾性証明が、クライゼルが指摘するような
別のBew（カットのない証明）を利用している点を問題だと指摘している。
ただし、この場合にはカットのある証明から、それ抜きの証明への
変換を用いており、その手順の停止性の証明は体系内ではできない
ので、ゲーデルの第二不完全性定理に抵触するわけではない。
111:１０２とか
04/12/24 17:14:23
帰ってきました。ちなみに１０７はぼくじゃないです。
＞そもそも、無矛盾性を体系内で表現できると単純素朴に
＞考えることができません。
そういえば、前原さんも「数値別に正確に表現しているわけではない」と書いておられました。
林さんの本も読んでみます。いろいろとありがとうございました。
どなたとどなたが同一なのか分かりませんが、レスをくれた方にはすべて感謝したいです。
（なんかもう110さんみたいな賢者がでてくるなんて、2chはすごすぎる・・・）
112:１３２人目の素数さん
04/12/24 17:25:27
>>107
＞どう書くか? を問題としなければ、
そう。まさにそこが問題であると林晋は言っている。
しかし、それはもはや”数学”の問題ではない。
はっきりいえば、数学よりももっと根本的な
言語とそれを用いる自分にかかわる”哲学”
の問題である。
113:１３２人目の素数さん
04/12/29 05:50:41
どなたか、わかる方、お教えください。
114:１３２人目の素数さん
05/01/02 23:36:49
651
115:１３２人目の素数さん
05/01/05 13:15:52
自然数の和と積に関する理論（いわゆる、ロビンソン算術）を作りたい、と考えて、
まず、語彙、項、論理式の定義を設定する、と、
これで、論理式はつくることができる、と、
で、その論理式が、自然数の和と積に関する一連の内容を表現できるように、と、モデルを設定する、と、
これで、十分なんじゃないか、と、
なんで、公理系をつくるんだろう？、と、
具体的に、論理式の集まりを把握したい、という目的とか、
その理論の意味論的完全性を示せば、その理論の公理系で証明できることを示すことによって、
すなわち、（意味論的に）真である、が言える（別にいらんなぁ）、とか、
そこらへんの目的からっすかね？
誰か詳しい人、教えてください
116:１３２人目の素数さん
05/01/05 13:25:25
>>115
意味不明。公理系も無いのに、モデルが作られるか。
117:１３２人目の素数さん
05/01/05 15:15:51
>>116
確かに、115のいうモデルは、数理論理学でいう
それとは異なるようだね。
115は漫然とモデルという言葉を使わずに
全く別の言葉で説明するように。
118:１３２人目の素数さん
05/01/05 15:20:25
ところで115は、ロビンソン算術の命題が
どんなものか知っているのかな？
119:１３２人目の素数さん
05/01/05 15:29:38
１１５はのいうモデルはモーデルのことだな。
120:１３２人目の素数さん
05/01/05 16:08:38
>>116
なんといったらいいのか、意味論的な諸設定とでも、いいましょうか、
115で言いたかった内容を、もう一度繰り返すと、
まず、語彙、項、論理式の定義を設定する、と、
これで、
#a＋##a＝###a
# 後続者関数、
項、論理式の定義は、ロビンソン算術とよばれているもののそれと同じいうことで
という論理式がつくれる、と、
で、
これに
一足す二は三
という内容をもたせるべくして、意味論的な諸設定（論議領域に自然数を設定したり、個体定項aに自然数0割り当てたり、関数に付値したり、・・ ここんところを、115では、モデルという語を用いてあらわしました）、を設定する、と、
これで、いいじゃん、と、（他の命題の表現についても、同様。で、これをもって、自然数の和と積に関する理論、ということでいいじゃん、と）
以下、115の内容へと続く
121:１３２人目の素数さん
05/01/05 17:10:36
＞論議領域に自然数を設定したり
簡単にいうけど、そもそも自然数全体が
無限個あるってことが問題なわけなんだけど。
単純に列挙なんかできないよ。どうするの？
122:１３２人目の素数さん
05/01/05 20:51:33
つーか、だって、それが、一階の理論の意味論なんやねんもん、
そんなところ批判されたって、言葉につまるというか、
最初に言い出した奴に言ってくれというか、
違うねん、そういうところにひっかかると、話が遠ざかってしまう。
そうじゃなくて、
ロビンソン算術の意味論は、上でも言ってるように、論理式に、意味みたいなもん、与えてくれてる。
これは、この理論が、自然数の和と積というものを表現しようとしているかぎり必要、ということはわかる。
俺が聞いてるのは、じゃあ、構文論とか、形式的体系（公理系）は、自然数の和と積を表現しようとしたやつに、
いったい、何を与えてくれてんねん、ということ、
123:115とか
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:１３２人目の素数さん
05/01/07 18:24:07
>>125さんの言うとおりです
Nは公理を勝手に増やしたり増やしたりしたらN'≠Nになってしまいます。
つまり、証明能力が変わってしまうと言うことです。当たり前ですね。
でもN'にも（一気に無限種類の公理を考えたりする荒業をしなければ）
閉論理式でN'から独立なものは存在します。（NにN'を代入するだけ）
127:１３２人目の素数さん
05/01/07 19:08:16
>>125
>>126
ある「その肯定形も否定形もNで証明できないようなNの閉じた式」を、形式的体系に加えようとも、
まだ、他に、その形式的体系にとって、「その肯定形も否定形もNで証明できないようなNの閉じた式」はある、ということでしょうか？
128:１３２人目の素数さん
05/01/07 19:51:01
うん。
N'で証明できない式はNでも証明できないからね。
ちなみに、
公理の集合Σからφが証明できない
⇔Σ∪{￢φ}は無矛盾な公理系
だけどこういうことはご存知ですよね？
129:１３２人目の素数さん
05/01/07 20:09:15
Σの無矛盾性を仮定するのを忘れておったわ
ハァッハッハハハ
130:１３２人目の素数さん
05/01/08 00:30:53
はい。
ところで、
＞（一気に無限種類の公理を考えたりする荒業をしなければ）
一気に、すべての「その肯定形も否定形もNで証明できないようなNの閉じた式」を考える、ということですか？
131:１３２人目の素数さん
05/01/08 00:39:51
まあ大体そういうことですー
より正確に知りたい場合はrecursively enumerableとか
そういう言葉をキーワードに件の定理を勉強してくださいですー
132:１３２人目の素数さん
05/01/08 02:29:38
もうちょっと、集合論とか証明論とか、勉強してみます。
ありがとうございました。
133:１３２人目の素数さん
05/01/10 20:11:30
ググった、先のサイトで、こんなのを見つけました。
＞ある数学的構造に対して完全な公理系が見つかれば，その構造における命題の真偽は決定可能である．
＞ゲーデルが１９３０年に発見した第一不完全定理は，自然数論を含むどんな公理系も完全でなく，また決定可能でないというものである．
＞命題の真偽は決定可能である．
というのは、、命題の、真である・真でない（意味論的な真理値）を決定できる、ということですか？
134:１３２人目の素数さん
05/01/10 20:20:34
>>133
決定可能というのはあるアルゴリズムによって有限回の計算で求められるということ。
135:伊丹公理 ◆EniJeTU7ko
05/01/10 23:36:57
>>133
＞ある数学的構造に対して完全な公理系が見つかれば，その構造における命題の真偽は決定可能である．
完全な公理系では、公理が有限個なら、全ての論証を列挙する事によって、
真理値が有限回の計算で求められるが無限個なら一般には分からない。
しかし多くの場合帰納的可算であるから、決定可能。
136:１３２人目の素数さん
05/01/11 00:25:36
だから一言で言えばYesだね。
もちろん誰も貴方の家のPCとか東大工学部にあるスパコンとかで
1000万年内に求まる、とかそういう保証はしてないですからね。
137:１３２人目の素数さん
05/01/11 00:36:36
>>135
本物？だとしたら勇み足だよー
第一不完全性定理はチョー厳密に言えば、
r.e.（c.f. >>131 再帰的枚挙可能とか帰納的可算と訳す）
公理化可能な無矛盾な公理系でPeano算術（本当はそれより弱いRobinson算術QでOK）
を含むものは（「含む」の意味もきちんと定義できます。）不完全、とか言う定理
です。で、普通数学の理論は自然数論を含みますしr.e.axiomatizableですから、
不完全、かつ決定不可能です。
というわけで、参考文献二つだけ。
Computability and Unsolvability (Mcgraw-Hill Series in Information Processing and Computers.)
Martin Davis (著) ペーパーバック (1982/11/01) Dover Pubns
Aspects of Incompleteness (Lecture Notes in Logic, 10)
Per Lindstrom (著) ペーパーバック (2003/11) A K Peters Ltd
Godel's Incompleteness Theorems (Oxford Logic Guides, No 19)
by Raymond M. Smullyan
一番上のほうの本は和訳もあります。計算可能性理論の古典。
一番下は和訳は訳語が酷いので、英語でベンキョーした方がむしろわかりやすいでしょう。
138:１３２人目の素数さん
05/01/11 00:40:10
と思ったが、「完全な公理系」は多くの場合、r.e.だといってるのかな？
それなら正しいですね。
実際に人間が扱う理論（代数トポロジーとか無限次元Hilbert空間論とか
概均質ベクトル空間論とか、まあ何でも）は全てr.e.ですよ。
r.e.じゃない理論なんて、集合論を使って無限個の公理を一気に付け加えて、
とかそうやって作ったよう分からん理論です。
139:１３２人目の素数さん
05/01/11 09:16:41
>>138
ところで
人間が扱い得る＝r.e.(recursively enumerable)
かどうかは、未だ解決されていない。
140:１３２人目の素数さん
05/01/11 13:48:54
ところで、
Robinson算術Q（構文論的不完全な公理系の例として）は、 再帰的枚挙可能.（recursively enumerable）だが、再帰的 (recursive)ではない、ということであってますか？
141:１３２人目の素数さん
05/01/11 21:10:26
>>140
そんな質問をするのは再帰的を理解していない証拠。よぉくかんがえてみろ、自明だぞ。
142:１３２人目の素数さん
05/01/12 00:00:08
学んでる途中の者が、質問というよりは、確認の目的で書き込んだことなので、
あんまり気にせずに、
さくっと、もしくは、さらっと、流してください
＞自然数もしく有限の記号列の集合が r.e.（recursively enumerable, 再帰的に枚挙可能）であるというのは，その要素をすべて並べあげる機械的な手続きがあることをいう．
＞r.e.集合で，その補集合もr.e.になるものを，再帰的 (recursive)という．
というのを、上のググッた先で見ました。
例えば、構文論的完全な公理系の要素の集合、その補集合（全体集合は任意の論理式の集合）もr.e.になるので，再帰的 (recursive)、
ということか？という感じで読んでいましたが、
いまひとつ、確証が持てなかったので、上のように、書き込んでみました。
143:１３２人目の素数さん
05/01/12 00:12:25
>>141
Q の「公理」全体の集合は有限集合なので、もちろん再帰的だけれど、
Q の「定理」全体の集合が再帰的かどうかも自明？
144:伊丹公理 ◆EniJeTU7ko
05/01/12 00:13:50
>>137
公理系が完全と言う前提での話し。
145:１３２人目の素数さん
05/01/12 00:46:41
>>142
ちゃんと本読んで勉強したほうが速いよ
>>143
定理の集合をTh_Qとでも置けば、φ∈Th_{Q}かどうかは、
計算機を使って証明をゲーデル数の少ない順に虱潰しに調べていって
証明B_g（gはゲーデル数）がφの証明になっているかどうか確かめればよいから
明らかに再帰的でしょ
>>144
そうなのか、ｽﾏｿ。
モデル理論にあまり詳しくないが、実体の理論とかのことでしょうね。
146:143
05/01/12 00:57:00
>>145
それは、再帰的に枚挙可能なことの証明。
147:１３２人目の素数さん
05/01/12 01:00:34
だったっけ……
ホントだ、recursiveな函数の定義域ですからね。
いや、『数学基礎論講義』で勉強したことはあるんですが、
どうもよく一章のその部分は分からなかったんですよ。
『帰納的関数と述語』も去年の春休み頃だいぶ読んだんですが、
もう忘れてしまっていて……
欝出し脳orz
148:１３２人目の素数さん
05/01/12 01:15:48
公理が「有限個」と言うときは、公理シェーマは一つとして数えるのが普通ですか？
149:１３２人目の素数さん
05/01/12 01:19:17
知らんがなｗｗｗ
ただ、実質的に公理図式と言うのは、無限個の公理と言っても
一つの規則で、普通人間は、無限個の公理がある、という意識はあまり持たないですよね。
そういったことにきちんと数学的な説明を与えるために
axiom schemeとかrecursiveとか、そういう用語があるわけです。
150:１３２人目の素数さん
05/01/12 01:26:57
すんません
誰か
＞自然数もしく有限の記号列の集合が r.e.（recursively enumerable, 再帰的に枚挙可能）であるというのは，その要素をすべて並べあげる機械的な手続きがあることをいう．
＞r.e.集合で，その補集合もr.e.になるものを，再帰的 (recursive)という．
について、コメントお願いします。
レスの流れを、見ていましたが、いっそう、
再帰的(recursive)というものが、どういうものか、わからなくなってきました。
Qは再帰的なんですか？
ちなみに、おおもとはここからです。
URLﾘﾝｸ(members.at.infoseek.co.jp)
151:１３２人目の素数さん
05/01/12 01:27:12
ありがとうｗｗｗ
152:１３２人目の素数さん
05/01/12 01:28:35
>>150
再帰的は決定可能と同じだよ。
153:１３２人目の素数さん
05/01/12 01:32:16
Qは決定不可能ですよね、
じゃあ、Qは再帰的ではない、ということですか？
154:１３２人目の素数さん
05/01/12 01:35:59
女の子はうんこをしないように Ｑは再帰的ではない
155:143
05/01/12 01:39:07
>>153
不完全性定理の文脈での決定不能命題の定義と、
公理系 T が決定可能であることの定義を復習しましょう。
これらは全く別の概念です。
156:１３２人目の素数さん
05/01/12 01:40:45
学んでいないものを復習することはできない。
157:１３２人目の素数さん
05/01/12 01:51:46
>>143で言ってる再帰的と
>>150で言ってる再帰的とは、別の内容ですかね？
158:１３２人目の素数さん
05/01/12 01:54:06
>>157
１４３は帰納的の意味ですね。
159:１３２人目の素数さん
05/01/12 01:58:04
帰納的の意味というのは、
再帰的に枚挙可能というやつですか？
160:１３２人目の素数さん
05/01/12 02:05:34
recursive＝帰納的＝再帰的
ただ、最初（一般帰納関数の概念が出てくる前）は
primitive recursiveのことを単にrecursiveといっていたので注意。
161:１３２人目の素数さん
05/01/12 02:09:19
公理から、ある命題もその否定も導かれないならば
どっちが正しいか決めることは出来ませんね。
たとえば連続体仮説のように。
というか、マジで自分で勉強しろって。
河合文化教育研究所の数学基礎論シリーズの
0巻か1巻が、丁寧に書いてあってお勧め。
（もちろん0巻は1,2巻の内容の概説なので
途中の議論は一部飛ばされています。）
162:１３２人目の素数さん
05/01/12 02:15:12
>>161
そんな誤植だらけの絶版本を薦めるなよ。
163:１３２人目の素数さん
05/01/12 06:17:50
いや、良く読んでないから誤植と言われても良く分からんのだが、
（0巻は集合論以外は読んだ。1巻は読んでない。持ってるだけ）
0巻『数学基礎論へのいざない』は寝転んで読む分には
最適だと思うのだがどうよ？内容は古いけどさ。
ってか絶版になってたっけ？
>>162さんは代わりとしては何を薦めるんですか？
164:１３２人目の素数さん
05/01/12 11:57:08
>>155
ズバリ言ったら？
定理の全体がr.e.というのと、
公理の全体がr.e.というのとは違う、ってさ。
r.e.公理化可能って後者のことでしょ？
165:１３２人目の素数さん
05/01/12 17:13:13
チョー要約すると
公理かどうかはごく簡単に判定できるし、定理は公理から
帰納的に（段階的に）定義されるものだけど、定理かどうかの
判定は非常に難しい、ということね。
166:１３２人目の素数さん
05/01/12 17:31:22
>>165
＞公理かどうかはごく簡単に判定できる
r.e.公理化可能といっても、
一般に公理かどうかの判定は
不可能だと思うぞ。
recursiveじゃないからな。
167:１３２人目の素数さん
05/01/12 21:44:31
>>166
そういう体系（公理がreでnon-recursive）の例はどんなものがあるんですか？
168:１３２人目の素数さん
05/01/13 02:39:24
>>167
多くの体系では、定理全体が r.e. で recursive でないのだから、
いくらでも作ることができる。
こういう話での基本的なトリックに、r.e. な公理系を持つ体系は、
recursive な公理系が存在するという結果がある。
169:１３２人目の素数さん
05/01/13 18:17:04
>>168
ありがとうございます。定理全体を公理にすればよいんですね。
170:１３２人目の素数さん
05/01/14 02:14:04
もっとくだらない例。
トートロジー A をひとつ固定し、An = A∧A∧...∧A (n個) と定める。
r.e. だが recursive でない自然数の集合 S に対し、
{ An | n∈S } は r.e. だが recursive でない公理系。
171:１３２人目の素数さん
05/01/14 19:20:56
>>170
は、明らかに recursive
172:１３２人目の素数さん
05/01/17 03:32:37
なぁなぁみんな
cot(x)
ってなんだ？
173:１３２人目の素数さん
05/01/17 03:44:59
>>172
市ね
174:１３２人目の素数さん
05/01/17 03:45:29
>>172
いやマジで聞いてるんだが
175:１３２人目の素数さん
05/01/17 23:55:52
高校生スレにGO！
176:伊丹公理 ◆EniJeTU7ko
05/01/21 17:54:51
以前
＞ロビンソン算術ってなぁに？
と言う質問をしたことがあるが、
本日、田中一之、数の体系と超準モデル、裳華房
を購入して大体読んだので理解した。
177:１３２人目の素数さん
05/01/21 23:34:22
一日で全部読んだの！？
まあそれは兎も角、その本は悪い本じゃないけど
かなり特殊な章立ての本ですね。
どうも筆者が学んだ順になっているらしいけど。
178:伊丹公理 ◆EniJeTU7ko
05/01/23 11:22:37
どこかに誤爆したようなのでもう一度。
>>176-177
大して深いことは書いてなかったな。
以前読んだ
G. E. Sacks, Degrees of Unsolvability,
同じく
G. E. Sacks, Saturated Model Theory
等々のほうが余程面白かった。
勿論、A. Robinson, Non-standard Analysis
も。
179:伊丹公理 ◆EniJeTU7ko
05/01/25 14:01:08
G を具体的な有限個の生成元と有限個の関係式で定義された群：有限表示群とする。
（有限表示可能群を単に有限表示群と云うこともあるが、ここでは上記の意味に取る。）
H も有限表示群とする。
G において語の問題が解け、 H が抽象群として G に同型なら、
H も語の問題が解けることを示せ。
180:１３２人目の素数さん
05/01/25 15:44:40
ﾜﾗ
181:１３２人目の素数さん
05/01/25 19:08:31
基礎論初心者です。どちらの本がお勧めですか。
Shoenfield/Mathematical Logic
Ebbinghaus, Flum, & Thomas/Mathematical Logic
182:１３２人目の素数さん
05/01/25 20:11:17
>>181
だんぜんうえ したはうんこちゃん
183:１３２人目の素数さん
05/01/25 21:30:28
>>182
良く知ってるな。
logic の本なんで読んだこと無い。
一度お勧め本でKleeneの本少し読んだが、すぐやめた。
>>181
logic は止めとけ。
Cohn, Universal Algebra は logic も含んでいて面白い。
184:１３２人目の素数さん
05/01/26 02:01:31
>>181
上は何十年か前にLogicの素養の無い院生のために
書かれた基礎論の概論、下はLogicに興味を持った
学部生のためのUTMの本。下の本はpartAは大分簡単だと
思いますが、paｒtBでは、無限論理、Fraisse の定理、
Lindostromの定理なんかも扱っています。
と言うわけで、本格的に勉強するつもりなら上がお勧めです。
一寸齧ってみよう、ということなら下でもよいでしょう。
185:１３２人目の素数さん
05/01/30 23:19:04
いまさらShoenfield、ツー気もしないでもないな。
186:181
05/01/31 10:53:40
>>185
Shoenfieldの他にお勧めがあれば教えて下さい。
187:１３２人目の素数さん
05/01/31 17:12:24
Shoenfield といえば、中途半端で汚ない formal system, Goedel interpretation
の変な改良、近藤--Addison の定理の泥臭い証明など文句をたらたら言った後で、
「でも良い本だよね」でしめるのが標準的な評価だったけど、今はどうなんでしょ。
章末の演習問題はたくさんあるけれど、初学者が少しづつ手探りで進むための問題が
ないので、>>185 の言うようにある程度数学の本の読み方を知っていないとつらいかも。
188:１３２人目の素数さん
05/02/05 13:04:20
『「知」の欺瞞』関連情報
●ｂｋ１の『「知」の欺瞞』のページ
* 佐々木力、ポストモダン思想の軽薄さを完膚なきまでに暴露した、知的刺激溢れる書物、2000/07/10
URLﾘﾝｸ(www.math.tohoku.ac.jp)
このページは黒木玄個人の責任で維持しております。
クレームその他は黒木個人におよせください。
★2002年新学習指導要領の中止を［上野、戸瀬、黒木］→NAEE2002で署名を！★
URLﾘﾝｸ(www.math.tohoku.ac.jp)
189:１３２人目の素数さん
05/02/05 15:25:58
afo
190:１３２人目の素数さん
05/02/05 15:40:09
>>187
「近藤--Addison の定理の泥臭い証明」なんて、誰がいったんだ。
近藤基吉のもとの証明、見てみい。
191:１３２人目の素数さん
05/02/05 16:10:47
こんど見てみる。
192:１３２人目の素数さん
05/02/05 16:28:27
面白いと思ってるの？
193:１３２人目の素数さん
05/02/08 12:31:46
しゃれが分からん香具師
194:１３２人目の素数さん
05/02/08 12:53:05
ぬるぽ？
195:１３２人目の素数さん
05/02/08 14:38:00
(ﾟдﾟ)ﾎﾟｶｰﾝ
196:１３２人目の素数さん
05/02/08 17:54:21
LKの基本定理とか無矛盾性証明を学びたいのですが、分かりやすめの本を紹介してもらえませんか。
竹内さんのはきつそうなので勘弁。すると自分ではあとは共立の赤い本（数理論理学）しか知りません。
洋書でも構わないので、お願いします。
書き方は無味乾燥でも大丈夫ですが、証明のギャップが大きいと逝きますので、
その辺を考慮していただければ、たいへんありがたいのですが。
197:１３２人目の素数さん
05/02/08 18:27:18
竹内さんのってGTMのProof Theoryのこと？
それとも証明論入門の事？
あまり知らないのだけど、一応レスしとくと
前者の事を言っているのなら、後者がより易しい。
で、後者でも難しすぎるなら、最近書かれた
松本先生ので勉強するのが一番賢いと思うけど、
他には『数学基礎論入門』とかか。あと、
"Basic proof theory" by A.S. Troelstra & H. Schwichtenberg
なんてのもあるようです。Smullyanの"First-Order Logic"にも
カット除去定理の証明はあったような感じです。
まあ自分で現物を見て判断してください。
198:１３２人目の素数さん
05/02/08 18:28:30
PrawitzとかでOPACってみてもいいかもね。
199:１３２人目の素数さん
05/02/08 18:42:20
>>197
GTMじゃないYO!
Studies in Logic and the Foundations of Mathematics だYO!
200:１３２人目の素数さん
05/02/08 21:05:04
>>196
今はもう絶版になったり品切再版未定のものですが、
図書館などで長期の貸し出しをしてもらえる環境にあるならば、
次の二冊を薦めます。
・前原昭二「数理論理学 数学的理論の論理的構造」培風館
無矛盾性証明の前に、カット除去定理とその簡単な応用までを
まず身につけたいのならば、この本のε定理の前のところまで
読んでください。
・竹内外史、八杉満利子「証明論入門」共立出版
Peano Arithmetic の無矛盾性証明まで一気に読む力があれば、
これを通読するのが一番です。(「数学基礎論(増補版)」でもよい)
>>197 でちょっと触れている、松本和夫「数理論理学」共立出版 は
該当部分は、竹内-八杉に完全に含まれているので、上記の本が手に
入らない場合の次善の策と思います。
201:１３２人目の素数さん
05/02/08 22:19:40
『証明論入門』って易しめですかね
数学基礎論（増補版）だと、最後の章の
二階論理が無くなっちゃう気がする
書いてるのは竹内さんじゃなくて八杉さんだけど
202:197
05/02/08 22:22:19
今更だが一寸書き間違いが
【誤】最近書かれた⇒【正】最近復刊された
203:１３２人目の素数さん
05/02/08 23:16:15
>>197-202
たくさんのレスに激しく感謝します。
ＯＰＡＣると、プラヴィッツさんのは一冊だけ無関係ぽいのがあるのみでした。
数学基礎論入門はグッドステインというひとの著書ですか？
以前少し見たときはコンパクトでつらそうでしたが、
証明論入門が最良ということですので、もう一度じっくりと見極めてこよう・・。
204:１３２人目の素数さん
05/02/10 00:35:38
パラメータをもつ関数同士の合成について質問します。
例えばa, b, c（全て正）をパラメータとし、3つの関数
y=a/x， y=b/x， y=c/x
を合成して、これらに共通したグラフ形状（ある意味、平均約な形状）を示す
新たな関数y=A/x を作り出す理論・手法というのは存在するのでしょうか？
関数の合成といえば三角関数の合成と、フーリエ展開における指数関数の
合成くらいしか知りませんので、よろしくお願い致します。
205:204
05/02/10 00:42:09
すみません
× 平均約な
〇 平均的な
206:１３２人目の素数さん
05/02/10 13:23:12
ageました
207:１３２人目の素数さん
05/02/12 06:06:06
スレ違い
208:１３２人目の素数さん
05/02/13 06:35:15
別に数学が好きでもないし、ちょっとした疑問が出来たけどスレ立てるまでも無いのでここで聞いてみる
360角形と円は同じ物だと考えれますかね
209:１３２人目の素数さん
05/02/13 10:11:07
円と多角形は違う図形です
210:１３２人目の素数さん
05/02/13 11:00:12
全然違うじゃん
というか普通の質問スレで質問してください
基礎論というのは、一つの数学の分野
（証明可能性とかを扱う）なので。
211:１３２人目の素数さん
05/02/13 13:02:00
数学板を｢質問｣で検索して一番まともそうなスレタイがここだったんですが
もしかして高校生のための～が数学板での標準質問スレですか
212:１３２人目の素数さん
05/02/13 13:48:44
>>211
質問スレは目的に応じていくつかあるので、どれが「標準」かは決まって
ないけど、その質問がここではスレ違いになることだけは確か。
とりあえず雑談スレで聞いてみるのがいいと思います。
雑談はここに書け！【２１】
ｽﾚﾘﾝｸ(math板)
ただ、質問する際は「同じ」ということの意味をもっと精確に規定
したほうがいいと思うよ。それによって答えがかわってくるから。
213:１３２人目の素数さん
05/02/13 15:16:51
どうも、とりあえずそっちのスレで聞いてみますね。ありがとうございました
214:１３２人目の素数さん
05/02/14 02:17:14
っていうか数学ってなんなん？
215:１３２人目の素数さん
05/02/14 13:46:55
>>214
スレ違い。
216:１３２人目の素数さん
05/02/15 17:05:15
等号を含む一階述語論理の等号って、あれは、述語記号ですか？
217:１３２人目の素数さん
05/02/15 18:34:50
二変数の述語記号ですよ。
ただ、等号に関する公理はやたら沢山ありますけど
218:１３２人目の素数さん
05/02/15 19:45:02
モデルにおける付置の処理は、どんなことになってんでしょうか？
219:１３２人目の素数さん
05/02/16 16:56:43
ああいうことになってます。
としか答えようないんですけどね。
どんなことになってんでしょうか、とか意味不明なこと言われても。
220:１３２人目の素数さん
05/02/17 10:30:43
昔、ブラウアーとか言う人が「直観主義」とかいうことを言い出して
ヒルベルト（だったかな）と論争したと思うんですけど、結局あれは決着
ついたのでしょうか。それともまだ解析学のような普通の数学をするのに
2重否定の除去はいつもできるとは限らないなどと言いながら数学してる
数学者も今現在いるのでしょうか。
221:１３２人目の素数さん
05/02/17 11:02:31
>>220
1927年 ヒルベルトのハンブルクでの講演「数学の基礎について」で自分の視点から論争を総括
同年 ブロウウェルの論文「形式主義についての直感主義的反省」で４つの妥協案を提案→実質的和解
1931年 ゲーデルが不完全性定理を発表
222:１３２人目の素数さん
05/02/17 11:44:14
直観主義 -> 位相や層
223:１３２人目の素数さん
05/02/17 12:19:47
> 等号に関する公理はやたら沢山ありますけど
沢山って？？？
224:１３２人目の素数さん
05/02/17 13:13:37
>>221
＞同年 ブロウウェルの論文「形式主義についての直感主義的反省」で４つの妥協案を提案→実質的和解
へーーーすごいや。そんなことがあったんですね。その「４つの妥協案」と
言うのはどのようなものなんでしょう。もし嫌でなかったら教えていただけ
ないでしょうか。あるいはどこか参照先をお教えいただけるとうれしいです。
当方、一般ピープルなので、論文の調べ方なんて知らないもので。(;_;)
それともその論文はネットで調べられるのかな。英語なら根性で読むけど
他の外国語だとちょっと．．．
225:220
05/02/17 14:22:40
よく調べもしないで質問するなと怒られそうですが。もしやと思って
「直観主義 和解」でググって見たら
URLﾘﾝｸ(www.shayashi.jp)
を見つけることができました。このページの
「ゲーデル、不完全性定理」と題した文章の「たとえば、１９２７年ころに」
から始まるあたりを読んで見ますと
「和解ではなく、ヒルベルトがブラウワーを政治的にねじ伏せた」
と書いてあります。さてさて．．．今現在の数学者の皆さんはどうなのでしょう？
例えば普通の解析学はどのように教えられているのでしょう？
あるいは
「フェルマーの最終定理」の証明は排中律や2重否定の除去はまったく用いられて
いないのでしょうか？普通に用いられているとするならそれに文句をつける数学者は
いないのでしょうか？
なんか教えて訓になっちゃいましたが、同じように疑問に思っている人
他にもいるんでないかなあ。
226:１３２人目の素数さん
05/02/17 14:48:12
現在、二重否定除去を無条件に認めない数学は確かにあって、
構成主義解析とかはそれを認めません。
ただ、二重否定は兎に角認めちゃいけないんだ、
とただ宗教のように二重否定除去を拒絶するんじゃなくて、
本人の人たちは、それなりの理由があってそうしています。
ただ、今の数学においては明らかに異端で、
数学者が1000人いたら、999人は普通の論理を普通に使う数学者です。
多分直観主義で数学やるのなんて、直観主義自体の研究を
除いたら構成主義解析くらいしか無いんじゃないかと思います
「数学の基礎をめぐる論争―21世紀の数学と数学基礎論のあるべき姿を考える」
「リーディングス 数学の哲学―ゲーデル以後」
なんかが参考になるかと。
227:１３２人目の素数さん
05/02/17 14:49:30
>>223
任意の論理式～に関して、～が公理、
という形で沢山ある、というだけですね
228:１３２人目の素数さん
05/02/17 14:55:49
どちらが正しいか？などという不毛な争いをする時代はとっくに過ぎ去った。
今は、通常の数学は従来通り進められ、同時に、数理論理学や
基礎論の一部では、使える論理を制限した場合にどのような
体系ができるかという研究が行われている。
229:１３２人目の素数さん
05/02/17 16:08:29
URLﾘﾝｸ(www.mec.gr.jp)
ところが直観主義は、ある程度昔からわかっていたことなのですが、位相的な
数学と非常に密接な関係になるのです。(中略) 位相、トポロジーなどと妙な
具合に結びつき、具体的なものとして急速に用いられるようになってきたので
す。それは、ここ10年かあるいは15年ぐらいでの大きな発展の一つではないで
しょうか。また、例えばカテゴリーの方でのトポスのような話も、トポロジー、
位相と直感論理の関係とは同様なものなのです。
URLﾘﾝｸ(kurt.scitec.kobe-u.ac.jp)
層の概念で、これは集合が時間に沿って連続的に変化して行くものをモデル化
したものであると考えることも出来ます。そして層の世界を支配する論理は古
典論理ではなく直観主義論理であり、「すべての実数上の函数は連続である」
など、古典論理に従う数学では到底成り立ち得ない直観主義の様々な考え方が、
層の世界では非常に自然になります。
230:１３２人目の素数さん
05/02/17 16:18:06
>>229のリンク先の話は
「直観主義数学のよいモデルが存在する」
ということ。
非ユークリッド幾何学のモデルが存在するからといって
ユークリッド幾何学が否定されたわけではないように
直観主義数学のモデルが存在するからといって、
古典論理による数学が否定されたわけではない。
231:１３２人目の素数さん
05/02/17 16:29:18
>>220
ところで君は、二重否定が矛盾をもたらすと思っているのかな？
ブラウアーの発言を「二重否定が矛盾をもたらす」ととらえるなら
それは何の根拠もない言いがかりである。
普通なら「矛盾するというなら証拠を出せ」で終わりなのだが、
ヒルベルトは、数学における二重否定使用の矛盾性を証明しようとした。
しかし、このもくろみはゲーデルによって「無理」であることが示された。
232:１３２人目の素数さん
05/02/17 16:39:46
>>231のつづき
もっとも、ゲーデルの結果は、二重否定の矛盾を示すものではない。
ゲーデル自身、そんなことは信じていなかった。
彼は、単にヒルベルトのもくろみに無理があるといったまでである。
少なくとも「古典論理は矛盾する」と主張するのは
確たる根拠を示しえない点で、㌧デモである。
直観主義数学の研究は、古典論理による数学を
否定するものではなく、その意味では上記のような
㌧デモ的態度とはまったく異なるものである。
233:１３２人目の素数さん
05/02/17 16:46:38
>>226
＞今の数学においては明らかに異端で、
＞数学者が1000人いたら、999人は
＞普通の論理を普通に使う数学者です。
通常の数学では、見た目上非構成的な対象や論法を
使っていても、議論の本質とは無関係な場合が多い。
しかしながら、通常の数学者は、精密な検討を
なしえない為、漠然と自分の数学が直観主義に
反するものだと思い込んでいるに過ぎない。
234:１３２人目の素数さん
05/02/17 17:14:11
＞直観主義で数学やるのなんて、
＞構成主義解析くらいしか無いんじゃないか
林晋氏は、ヒルベルトの形式主義の源として
不変式論の有限基底定理をあげていたが･･･
不変式論に着目すれば、その後、ワイルが
古典群の不変式を具体的に構成している。
このことと、ワイルがヒルベルトの形式主義に
異を唱えたこととは関係があるのかどうか･･･
235:220
05/02/17 17:30:26
いやあ、たくさんの情報ありがとうございます。おもしろいですねえ。
>>231
＞ところで君は、二重否定が矛盾をもたらすと思っているのかな？
いえいえ。それどころか、二重否定の除去や、排中律が使えないなんて
いわれたら不自由で嫌だなあ、と思っています。
＞ヒルベルトは、数学における二重否定使用の矛盾性を証明しようとした。
＞しかし、このもくろみはゲーデルによって「無理」であることが示された。
へーーー。具体的にはゲーデルは何を示したんでしょう？もしかして
第2不完全性のことですか？（この言葉って一般的なんでしょうか？私は
前原昭二の「数学基礎論入門」で読んだだけです。その本の第2不完全性
のあたりは、はしょってある証明があまりにも多くて〔帰納的関係が算術
的論理式で表現可能とかいうところだったかな〕あきらめました。
だから、第2不完全性についてはよくわかってないかも。）
>>229
ありがとうございます。これからそのリンク先を読んで見ます。
236:１３２人目の素数さん
05/02/17 18:12:45
＞具体的にはゲーデルは何を示したんでしょう？
＞もしかして第2不完全性のことですか？
Yes．
237:１３２人目の素数さん
05/02/17 23:09:02
＞ 現在、二重否定除去を無条件に認めない数学は確かにあって、
＞ 構成主義解析とかはそれを認めません。
すでに古典になっちゃったとは思いますが、構成主義数学といえば、Bishopが
有名ですね。
URLﾘﾝｸ(plato.stanford.edu)
この数学を一言で言えば、排中律と外延性公理を仮定せず、しかし選択公理は
仮定するというものです。選択公理を仮定していると非構成的になると思うかも
知れませんが、排中律を仮定していないため、そのような非構成的な現象は生じ
ないのです（ただし外延性公理を仮定すると排中律が導かれてしまいます）。
Bishopのすごいところは、今まで非構成的にしか議論できないだろうと思われ
ていたいくつかの理論を排中律なしで構築できることを示したことで、既にBishop
以前にも代数学の基本定理が排中律なしで証明できることは知られていたのです
が、Bishopは、抽象空間におけるルベーグ積分論や、一般の局所コンパクトアー
ベル距離群におけるハール測度の構成とか、一変数複素解析におけるリーマンの
開写像定理とか、少し弱い形ではあるが、局所凸空間のハーン・バナッハの定理
とかを証明して見せたのです。
現在でも例えばシュワルツの超関数の空間の完備性とかを調べている人が日本
にもいます。
238:１３２人目の素数さん
05/02/18 13:15:33
>>237
＞外延性公理
集合論ではそういう建前はあるけど、実際には
群の元の異なる表示が、同じ元を表すかどうか
判定するアルゴリズムが存在しないなんていう
結果もあるわけだから。
もっともこの話は排中律には関係ないか。
239:１３２人目の素数さん
05/02/20 17:43:41
超ひも理論なんか研究してる奴は馬鹿
ｽﾚﾘﾝｸ(rikei板)l50
240:１３２人目の素数さん
05/03/01 14:07:11
321
241:１３２人目の素数さん
05/03/01 21:19:09
>>239
オマエモナー
242:１３２人目の素数さん
05/03/11 15:05:45
モデル論の入門書として適当な本ってありますか？
243:１３２人目の素数さん
05/03/11 22:56:07
>>242
最近の本だとこのあたり。
David Marker, Model Theory: An Introduction, GTM, Springer, 2002.
URLﾘﾝｸ(www.amazon.co.jp)
Bruno Poizat, A Course in Model Theory: An Introduction to Contemporary
Mathematical Logic, Universitext, Springer, 2000.
URLﾘﾝｸ(www.amazon.co.jp)
244:１３２人目の素数さん
05/03/13 22:30:30
一階述語の証明の集合が原始帰納的であることは完全性定理と実質的に等しい。
というような文章を読んだのですが、なぜだか分かりません。
前者にはモデルの概念も何もないと思うのですが・・。
正確には下のように書かれていました。なぜか教えてください。
Putative proofs of universal validity of first-order formulas can be checked for validity, algorithmically.
In technical language, the set of proofs is primitive recursive.
Essentially, this is Godel's completeness theorem,
although that theorem is usually stated in a way that does not make it obvious that it has anything to do with algorithms.
245:１３２人目の素数さん
05/03/14 19:59:47
ランダム性の概念を数学的に追求した書物はありますか？
246:１３２人目の素数さん
05/03/14 21:42:30
クレタ人はみんな頭がいいとクレタ人が言った
247:１３２人目の素数さん
05/03/15 01:31:50
坪井明人 モデルの理論 河合出版
248:１３２人目の素数さん
05/03/15 02:12:08
へー、坪井先生 本書いてたんだー。（by元ゼミ生）
249:１３２人目の素数さん
05/03/15 02:37:37
高１です。すれ違いかもしれませんが質問がスレタイだったので質問させて下さい
因数分解なのですが、これって公式全部覚えないとダメなんでしょうか？
確か中学校の時、因数分解は
－2a / －b±√－b^2－4ac で解くと言ってたのですが。
複雑になってくると応用が利きません。
250:１３２人目の素数さん
05/03/15 02:55:14
>>249
オマイさんは激しく勘違いしていると思われ。
数学基礎論ってのは大学くらいから専攻の対象になる数学の一分野のことで基礎の数学のことでは
ない。
URLﾘﾝｸ(messages.yahoo.co.jp)
Yahoo数学板の「高校生の為の数学質問コーナー」あたりで聞いてきなさいな。
251:１３２人目の素数さん
05/03/15 19:47:27
ちょっとなごんだw
252:１３２人目の素数さん
05/03/16 00:24:52
>>243
>>247
レスｻﾝｸｽｺ
>>247
のが手に入りそうなんで、とりあえず、それから読んでみます。
253:１３２人目の素数さん
05/03/16 11:21:22
あのーみなさんは自由変数と束縛変数で文字の使い分けしてますか？
例えば自由変数にはa,b,cなどのアルファベットの最初の方を使い、
束縛変数にはx,y,zなどのアルファベットの後ろの方を使う、というような。
私はどうせ本質は変わらないのだからいちいち区別すんのやめよーー、
と思っていました。
最近GentzenのCut除去定理の証明をなぜかもう一度フォローしたくなって
読んでるんですが、この証明見ると自由変数と束縛変数を区別しなかったら
ちょっとやりにくいなあ、としきりに思えてくるわけです。そこでいろいろ
疑問がわいてきたのですが、私はもう社会人？？年生。いまさら近くにこんな
話題にのってくれる人もなし、文献もなし。どなたかご教示ください。
・そもそもGentzenのLKの形式って自由変数と束縛変数の区別をするのが普通な
のでしょうか？
・もし、GentzenのLKで自由変数と束縛変数を区別しない場合、例えば（∀右）
の推論規則は
Γ⇒Θ、A
－－－－－－－
Γ⇒Θ、∀xA
のように∀xを付け加えるだけなのでしょうか。それとも
Γ⇒Θ、A(x)
－－－－－－－－－
Γ⇒Θ、∀yA(y)
のように変数を換えてしまう（上記ではxをyに換えている）のも推論規則の
なかに含めてしまうのでしょうか。
＊そもそも自由変数と束縛変数を区別しないGentzenの流儀なんてなかったりして。
＊こんな細かいことってどこ探しても説明なんてないんだよなあ。
＊ほんと、誰かたすけてちょ。
254:１３２人目の素数さん
05/03/16 14:11:26
>>253
自由変数と束縛変数を区別しない Hilbert 流の体系の本はたくさんあるので、
それを参考にすれば自然に作れるはずですが。
255:253
05/03/16 16:31:22
>>254
どうも舌足らずですみません。自由変数と束縛変数を区別しないだけなら
もちろん何の問題もないのですが、Cut除去定理の証明をどのように工夫する
のかなあ、と思いまして。
もしかして、その区別をしない場合は
「終式（証明図の最後のSequent）を変えず」にCut除去するの
ではなくて、「束縛変数の違いを無視して、終式を変えずに」Cut除去
するのかなあ、と思ったわけです。
256:１３２人目の素数さん
05/03/16 17:08:49
（∀右）と（∃左）の推論規則には、それの適用により
束縛されることになる変数に関する条件が付いているはず。
いつでもどこでも無制限に適用できるわけではないので、
本を読み返してみよう。
257:253
05/03/16 17:59:48
>>256
私が今読んでる証明は、数学的帰納法を2重に使用する方法でCutを除去する
のですが、その場合、今着目している証明図の固有変数(eigen variable)
が各々の（∀右）と（∃左）で”固有”なものとなるように書き換えを行う
んです。とすれば、
Γ⇒Θ、A(x)
－－－－－－－－－
Γ⇒Θ、∀yA(y)
のように変数を換えてしまうのも推論規則の中に含めていないと考えづらい
ですよね。そこで上記のような話になるんです。
「下式に固有変数がないこと」という条件を無視して推論すると言うこと
を言っているのではありません。
258:１３２人目の素数さん
05/03/16 22:21:38
Bourbakiみたいに束縛変数のところを□に置き換えて、頭の quantifier と□を鎖
で結んじゃう流儀を使えば何にも問題なくなる。
259:253
05/03/16 22:42:01
>>258
それはそうですけど、私がひっかかってるのは、どちらかと言うと
Γ⇒Θ、A
－－－－－－－
Γ⇒Θ、∀xA
のように∀xを付け加えるだけの流儀も捨てがたいなあと言う気持ち
があるからなんです。
話は違いますが、鎖で結ぶってところが抵抗あるんですよねえ。
ワープロ（というよりTeXですが）で書きづらいし。
260:１３２人目の素数さん
05/03/17 00:08:47
＞ 話は違いますが、鎖で結ぶってところが抵抗あるんですよねえ。
□ が出てくるときは、いつも □ とそれより左にある quantifier とただ一本の
鎖で結ばれているから、□ とその quantifier の間にある記号の個数だけ □ に
ダッシュを付けた記号 □''…' を □ と鎖のかわりに使えばいい。
261:253
05/03/17 10:54:43
>>260
＞□ とその quantifier の間にある記号の個数だけ □ に
＞ダッシュを付けた記号 □''…' を □ と鎖のかわりに使えばいい。
なるほどねえ。簡単に工夫できるんですねえ。
>>255に誰か偉い人のコメントあるといいなあ。
262:偉い人
05/03/17 14:06:41
>>261
自分で考えろ
263:253
05/03/17 15:00:25
残念(;_;)
264:１３２人目の素数さん
05/03/17 15:49:18
>>244
にレスしてあげたいが気力がでない。
>>263
カット消去の証明を書き換えるのはまんどくさいので、区別無しの
システムを作って、区別ありのシステムとの間で証明図の相互書き換えが
可能であること示せば？
265:253
05/03/17 18:02:42
>>264
レスありがとうございます。
＞区別無しの
＞システムを作って、区別ありのシステムとの間で証明図の相互書き換えが
＞可能であること示せば？
とのことですが、証明図の終式（証明図最後のSequent）で、同じ変数が
自由変数としても束縛変数としても使用されている場合を考えると、あまり
うまくいかない気がします。やはり「終式（証明図の最後のSequent）を変えず」
にCut除去するのではなくて、「束縛変数の違いを無視して、終式を変えずに」
Cut除去すると言う風になるような気がしてきました。
266:253
05/03/17 18:12:22
あ、私も勘違いしてた。Cut除去の証明においては、自由変数と束縛変数を区別する
というよりも、もし区別しない流儀を選んだ場合、
>>253の
＞例えば（∀右）
＞ の推論規則は
＞ Γ⇒Θ、A
＞－－－－－－－
＞ Γ⇒Θ、∀xA
＞ のように∀xを付け加えるだけなのでしょうか。それとも
＞ Γ⇒Θ、A(x)
＞－－－－－－－－－
＞ Γ⇒Θ、∀yA(y)
＞ のように変数を換えてしまう（上記ではxをyに換えている）のも推論規則の
＞ なかに含めてしまうのでしょうか。
のところが良く分からないのです。
267:１３２人目の素数さん
05/03/17 22:18:54
集合論の基礎から高度な内容までを含んだ優れた書籍はありませんか？
洋書でも結構です。
268:１３２人目の素数さん
05/03/18 00:36:10
>>267
Jech or Kunnen
269:１３２人目の素数さん
05/03/18 03:25:01
>>257
束縛変数と自由変数の区別をするかどうかの問題ではなく、
eigen-variable が固有であるという条件が保証されていない
場合に Gentzen の証明をどのように修正すればいいかという
問題を考えるべきでしょう。
270:253
05/03/18 08:18:46
>>269
その通りです。（>>266）
271:１３２人目の素数さん
05/03/19 03:43:43
>>265
＞とのことですが、証明図の終式（証明図最後のSequent）で、同じ変数が
＞自由変数としても束縛変数としても使用されている場合を考えると、あまり
そんな終式での照明図ではそもそもcutは除去できないと思われ。
例えば「情報科学における論理」p.78でも読んでみれ。
272:253
05/03/19 11:01:16
>>271
情報提供ありがとうございます。早速取り寄せてみます。（品切れ？）
ところで、自由変数と束縛変数を区別しない場合、
（∀右）の推論規則として
Γ⇒Θ、A
－－－－－－－
Γ⇒Θ、∀xA
のように∀xを付け加えるだけのものしか許さない場合、もしかしてCutなしでは
証明できない簡単なSequentがあるのではないかと思って考えてみたら、
∀(x=y∧x∈z)⇒∀y(y∈z)・・・(1)
はもしかしてCutなしでは証明できないのではないでしょうか。もちろん
∀(x=y∧x∈z)⇒∀x(x∈z)・・・(2)
は簡単に証明できますから、
∀x(x∈z)⇒∀y(y∈z)・・・・・(3)
とのCutを使えば(1)は証明できますが、推論規則として上記の（∀右）しか
許さない場合は(1)はCutなしでは証明できないのではないでしょうか。
273:偉い人
05/03/19 11:32:10
＞∀(x=y∧x∈z)⇒∀y(y∈z)・・・(1)
＞はもしかしてCutなしでは証明できないのではないでしょうか。
そもそも∀の後ろに何の変数もない式は証明できないだろう。
＞もちろん
＞ ∀(x=y∧x∈z)⇒∀x(x∈z)・・・(2)
＞は簡単に証明できますから、
それは、君が論理法則を誤解してるということ。
274:253
05/03/19 16:40:57
>>273
その通りですね。xが抜けていました。正しくは
∀x(x=y∧x∈z)⇒∀y(y∈z)・・・(1)
∀x(x=y∧x∈z)⇒∀x(x∈z)・・・(2)
です。失敬、失敬、(^^;)
275:１３２人目の素数さん
05/03/19 18:15:54
>>274
∀x(x=y∧x∈z)⇒∀y(y∈z)
cut があろうとなかろうと、正しくない式が証明されてはいかん。
276:253
05/03/19 23:54:32
>>275
>>274の(2)は示せますか？
なんか、ガックシorz
277:１３２人目の素数さん
05/03/20 02:07:38
>>275
>>274 の(1)や(2)は普通に正しい様だが。
278:１３２人目の素数さん
05/03/20 02:19:19
私は>>275じゃないですけど、(1)は何か
yのboundが少々おかしくないですか？
279:１３２人目の素数さん
05/03/20 11:51:38
>>278
気持ちが悪いけど別に問題はないと思われ。free の y と、bound されてる
y は無関係なわけで。
だけど、こんな変数がある時は cut を消去できなかったような気が。
280:１３２人目の素数さん
05/03/30 13:50:46
あのーー。GentzenのLKやNKの形式的論理計算を支援してくれるようなソフト
探しているんですが、どなたかご存じないですか。まあ、日本語でHelpが読めるに
越したことはないですが、英語でもがんばってみたいと思うのですが。
（Hilbert式のでもいいかな。）
281:280
05/03/30 21:03:32
あ、すいません。当方MS-Windowsなので、MS-Windowsで使用できるものを
おながいします。
282:１３２人目の素数さん
05/03/30 21:18:11
>>280
Lisp かなんかで自分で作ったほうがいいんでは。
勉強になるし、拡張性も思いのままだし。
283:280
05/03/30 21:51:15
>>282
Lispってそういう文字列処理得意なんですか？
284:１３２人目の素数さん
05/03/30 23:20:42
>>283
MLとかOCaml使うべし。
再帰的データ型使えるしパーサとかも普通にライブラリに入ってるはず。
285:280
05/03/30 23:41:20
>>284
ちょっと検索してみましたが、MS-Winで使用するにはMeadowとかやんないと
いけないんでしょうか？
やっぱ、xyzzyじゃ無理？
（つっても、xyzzyもKaTeX使ってる程度だけど）
286:１３２人目の素数さん
05/03/31 01:11:15
>>280
別にMeadow入れる必要はないよ。
↓ここから辿って適当なコンパイラ落としてくればよろし。
URLﾘﾝｸ(www.jaist.ac.jp)
287:280
05/03/31 11:55:46
>>286
をを！おありがとうござりあんす！
288:１３２人目の素数さん
05/03/31 20:12:27
>>283
> Lispってそういう文字列処理得意なんですか？
もちろん。
文字列処理じゃなくて記号処理っていうべきだけど。
Windows では PLT-Scheme がお勧め。
289:280
05/03/31 21:00:26
>>288
をを！ありがとうございます。
するってえと、MLとLispとどっちにするか迷いますなあ。
290:１３２人目の素数さん
05/04/08 21:43:50
モデル理論の超フィルタを使用した超積構造の作り方って、
ルベーグ積分の almost everywhere と似ていないか？
何か関係あるのかな。
291:１３２人目の素数さん
05/04/09 00:30:02
基礎論の入門書の良書ってどんなのがありますか？
基礎論は全くわからないので、なんとなく流派とか色々ありそうで、
どんな本から読めばよいか分かりません。
（できれば、和書がよいのですが）どなたか教えてください。
292:１３２人目の素数さん
05/04/09 01:39:45
>>291
数学基礎論シリーズ
URLﾘﾝｸ(www.kawai-juku.ac.jp)
293:１３２人目の素数さん
05/04/09 01:46:52
>>292
どうもです。参考にしてみます。
294:１３２人目の素数さん
05/04/09 02:38:36
クロスリーとかも入門書としてはよいような。
295:１３２人目の素数さん
05/04/09 11:12:17
291ですが、因みに、基礎論に流派とかってありますか？
（なんかG.B.流（ゲーテル・ベルヌーイだったかな）とか聞いたことがあるんだけど。）
あったら、どんなのがあるのか教えてもらえませんか？
296:１３２人目の素数さん
05/04/09 14:02:43
学派だったら無いこともないけど、
あまり数学で学派なんか気にしないですよ。
GBというのは多分ゲーデル、ベルナイスの事だと思うんですが、
単に公理的集合論の定式化に、BG式のものがあるだけで、
これも本質的にはZF式のものと同じものです。
297:１３２人目の素数さん
05/04/09 17:49:04
>>296
返答ありがとうございます。
じつは位相の本で、このＢＧ流を使われていたので
できれば、この体系から勉強したいと考えていて。
上に挙げていただいた本はどうなんでしょうか？
298:１３２人目の素数さん
05/04/09 22:11:41
数学基礎論の研究って盛んなの?
外国でも?
299:１３２人目の素数さん
05/04/11 00:02:51
age
300:１３２人目の素数さん
05/04/11 15:31:04
>>298
日本は盛んではない国だったと思うが？
301:１３２人目の素数さん
05/04/12 21:29:33
アメリカじゃナウい学問
302:１３２人目の素数さん
05/04/12 23:43:20
>300
何故だろうか？
303:１３２人目の素数さん
05/04/12 23:45:48
隈部正博って知ってる？
304:１３２人目の素数さん
05/04/13 00:24:53
竹内外史ゆかりの人か？
305:１３２人目の素数さん
05/04/13 17:26:33
誤差を含めた割り算ってどうやるんですか？
誤差のある重さと誤差のある体積を使って密度を求める問題がわからない…orz
306:１３２人目の素数さん
05/04/13 20:04:48
>>303
出身が早稲田、専門が帰納的関数論だから廣瀬健先生の門下かな？
307:１３２人目の素数さん
05/04/13 21:41:49
写像ｆ：Ｘ→Ｙが単射であるとは一体何を示せばいいのですか？
308:１３２人目の素数さん
05/04/13 22:38:06
微分係数と導関数って何を求めてるの？
309:１３２人目の素数さん
05/04/13 23:43:51
>303
放送大学助教授。
310:１３２人目の素数さん
05/04/17 12:14:24
>>305 >>307 >>308
スレ違いです。
数学基礎論は「数学の基礎」ではありません。
311:１３２人目の素数さん
05/04/19 21:54:59
理論の公理がr.e.なら、定理もr.e. 、というのが書いてあったのですが、
論理式の集合（定理）がr.e.なら、それは、r.e.公理化可能である、という逆の方向も言えますか？
312:１３２人目の素数さん
05/04/20 01:58:28
>>311
言える。定理がr.e.なら、その定理の集合は公理化可能。証明はクレイグによる。
313:１３２人目の素数さん
05/04/20 16:37:24
ありがﾄﾝ
314:４９００１２８
05/04/21 04:54:14
2^nで表されるゼロ以外の自然数の集合をA、その冪集合をBとする。
Bをωー１を含んでる集合Cと含まない集合Dにわける。
Dの各要素が含んでいるAの元をそれぞれ足し合わせる。
Φ＝０、（１）＝１、（２）＝２、（１、２）＝３、（４）＝４
（１、４）＝５、・・・・・（１、２、４、８）＝１５、・・・・・・・
（１、２、４、８、・・・・ωー１/4、ωー１/２）＝ωー１
｜
１+１/2+１/４+１/８+・・・・・１/ωー１/2+１/ωー１＝２
＝１＋２＋４＋８＋・・・・・・ωー１/ωー１＝２
従って、１＋２＋４+８＋・・・・ωー１/２＝ωー１
Cを下のように無限順序数に対応させる。
（ωー１）＝ω、（ωー１、１）＝ω＋１、（ω－１、２）＝ω＋２・・・
（ωー１、１、２、４、８、・・・・ωー１/２）＝ω＋ωー１
よって、AとBは対等。
４９００１２８てついそううつそうき
315:４９００１２８
05/04/21 06:00:06
誰かかまって
316:１３２人目の素数さん
05/04/21 10:27:34
ωー１?
317:１３２人目の素数さん
05/04/21 12:41:54
>>314
君が順序数を全く理解していないことはわかったから
とりあえず日本語と、式の書き方のマナーを1から勉強して出直してくれ。
318:１３２人目の素数さん
05/04/21 17:32:58
順序数を理解してないのに１からといわれても。。。
319:１３２人目の素数さん
05/04/22 00:24:26
>>318
ウマい。座布団一枚！
320:１３２人目の素数さん
05/04/22 05:16:51
最後の有限順序数はなんて表現すんの？
321:４９００１２８
05/04/22 05:44:21
最後の有限順序数を抜いたAの総和は発散しないべ。
つーか最後の有限順序数とかいう概念てないのかい？
ないと僕は対角線論法が理解できないんだけど。
誰か丁寧におしえれ。百円やるから。
322:４９００１２８
05/04/22 05:52:12
今からうんこするからやっぱいいや。
323:１３２人目の素数さん
05/04/22 07:33:33
始めがあっても終わりがない(場合もある)のが整列集合。
324:１３２人目の素数さん
05/04/22 19:47:01
いわゆる“フェルマーの無限降下法”ですね(^-^;)
ω-1
ω-2
ω-3
ω-4
ω-5
：
：
325:１３２人目の素数さん
05/04/22 23:33:58
あまり関係ないかと
326:１３２人目の素数さん
05/04/23 01:35:26
>>321
αが有限順序数ならばα+1も有限順序数だから
最後の有限順序数なんてものは存在しない。
わかったか？ほら百円よこせ。
327:４９００１２８
05/04/23 02:37:05
まあそんなことはわかるんだけどさ、
ωが最初の超限順序数なら、その一つ前が、
最後の有限だべ。具体的な値が存在しないのは
当たり前だけど。そう考えないと、
２＾ｎの総和（ｎは自然数全てを動く）は発散しなくなるべ。
無限に足しても自然数になることになるべ。
328:１３２人目の素数さん
05/04/23 12:02:59
>>327
だからね、仮にω-1って順序数があったとしてもそれは有限では有り得ないの。
下4行は完全に電波でしかないし。
329:１３２人目の素数さん
05/04/24 01:35:56
公理的集合論の基礎を勉強し終わって、より深く勉強したいんだけど、
どんな本がいいかな？
「巨大基数の集合論」ってどんな感じ？
URLﾘﾝｸ(www.springer-tokyo.co.jp)
「Set Theory」これは？
URLﾘﾝｸ(www.amazon.co.jp)
読んだことある人いたら、感想を聞きたいです。
330:１３２人目の素数さん
05/04/24 02:23:57
>仮にω-1って順序数があったとしても
ねーだろｗｗｗ
>>329
ｽﾚﾘﾝｸ(math板)
の上のほうを参照すればよいと思う
331:１３２人目の素数さん
05/04/24 02:50:28
(log6 2)2 ログ６の２の二乗っていくつになるの？
332:１３２人目の素数さん
05/04/24 03:49:40
>>310
333:４９００１２８
05/04/25 17:50:47
有限の次が有限なのはわかるけどね、それを常に
適用させると有限である自然数を
並べ終わったあとに余る実数なり部分集合なりから、
一対一の矛盾を導く対角線論法がおかしくなるべ。
余った要素に対応する新しい有限である自然数を、
順次作ってけばよくなるから。あれは有限の自然数を無限に
並べる手順が完了したと仮定して導く背理法だからね。
仮に自然数を並べ終えたなら、そのときの最後を考えるべきだしょ。
で、２＾n（nは自然数のすべてを動く）の集合を
Aとした場合、Aの部分集合を自然数の２進法表示と同一視すれば、
Aはすべて自然数だから、最後の自然数を抜いたAの総和は
最後の自然数をこえない。だから最後の自然数を抜いたAは
自然数と一対一の対応がつくべ。そうすると最後の自然数を
含んでいるAの部分集合も自然数に対応しるから、Aの冪集合は
可算濃度だべ。
最後の自然数を考えないとしると、２進法と同一視したAの部分集合を
小さい順に並べてったとき、２＾Nが自然数であるかぎり
それより小さい要素でできている部分集合はすべて自然数に
対応する。よって、この操作が完了したと仮定すると
この列は全て自然数になる。
でも無限の要素をもつ部分集合は自然数に対応しないので、
背理。
334:１３２人目の素数さん
05/04/25 19:13:52
順序数には、一つ前がある後続順序数（successor ordinal）と
一つ前がない極限順序数（limit ordinal）があるんだよ（０は除く）。
極限順序数が存在するというのは無限公理から導かれて、
最初の極限順序数がωなわけ。
だから、ωの一つ前というのは存在しないの。
集合論は独学だと電波方面に行きやすいから注意が必要。
迷ったら教科書を開いて、定義や公理に立ち返った方がいいよ。
335:１３２人目の素数さん
05/04/26 03:32:41
>>333
>>ｽﾚﾘﾝｸ(math板:626番)にレスしました
336:４９００１２８
05/04/26 04:28:31
＞＞有限である自然数を並べ終わったあと
有限の値である自然数を無限個並べ終わったあとね、かきまちがった。
最大の自然数が存在しないのもわざわざおせーてもらわなくても
わかるんだけどね、おれがつくった集合Aの部分集合を自然数の二進法表示と
同一視して考えると、ある自然数２＾ｎがあった場合、それ以下の要素のみで
できてる部分集合は要素が無限個あっても自然数２＾ｎより小さいから、
全部自然数になるだろ。
２＾ｎの２乗もその２乗も無限に自然数だから、
自然数からなる集合Aの部分集合はすべて自然数に対応して、
Aの冪集合は可算濃度になるべ。
337:１３２人目の素数さん
05/04/26 04:57:09
こっちのスレは少々スレ違い、ということなんだけどなあ
ま、高校の数学の質問がくるより良いか
>集合Aの部分集合を自然数の二進法表示と
>同一視して考えると
A={m ; m=2^n , nは自然数}という意味だと思うんだが
Aの冪集合P(A)とNは一対一に対応しません。
対応するのはAの「有限」部分集合
338:４９００１２８
05/04/26 05:34:52
朝早いのに応えてくれてありがと。
有限の部分だけ対応するね。
２＾ｎが有限だとすると、それ以下でできてる
部分集合も有限でしょ。Aの中には有限しかないんだから、
Aのどの要素をとっても、それ以下の要素のみでできてる部分集合は
全部有限でしょ。とするとある２＾ｎが最大の自然数で、２＾ｎの次から
無限というへんてこなこと考えないと「無限」部分集合はつくれなく
なりません？
339:１３２人目の素数さん
05/04/26 05:41:22
ならないですよ
2^nはnを大きくするといくらでも大きくなるから。
有限個しかないのと、有限のnしかない
（無限大の自然数なんて無いんだから、言い方がおかしいけど）
というのは区別しないといけない
340:４９００１２８
05/04/26 05:53:56
自然数の無限列が自然数じゃないないんだから、無限の元をもつ部分集合を
有限とするか、自然数におわりをつくるかしないと、
、論理的におかしくなりません？
341:１３２人目の素数さん
05/04/26 06:00:46
2^nという形では有限部分集合しか対応させられないよ。
無限部分集合に対応させるには、2^ωにしないとダメ。
342:１３２人目の素数さん
05/04/26 06:20:39
4900128さん
次の論法のおかしさを見抜いてください。
"各自然数nについて、
S_[n] ={0,1,...,n}
は有限集合である。
集合
S_[0]={0}
は有限集合である。
ゆえに集合
S={0,1,2,...} (自然数全体)
は有限集合である(!)."
343:339
05/04/26 06:46:53
>>340
なりません
どうしてなるのか分からない
有限、無限はきちんと定義できます。
それと用語は正しく使いましょう。
344:１３２人目の素数さん
05/04/26 08:40:46
2^nはどれも有限なのに2^ωまで行くと
可算無限なんて飛び越して
一足飛びに連続の濃度に行ってしまうのが
気持ち悪くて仕方がなかった5年前の俺
345:１３２人目の素数さん
05/04/26 15:24:28
>>344
全てのnに対する2^nの直和なら可算無限なんだけどね。
346:１３２人目の素数さん
05/04/26 21:11:39
>>342
4900128ではないですが，自然数全体の集合はinductiveに定義できない（F(n+1) = {n+1} ∪ F(n)のlfpではない）
のにinductionを適用しているということでしょうか？
347:１３２人目の素数さん
05/04/26 21:53:58
>>346
4900128さんに考えていただきたいのは、ω-1なるものが仮に存在するとして、帰納法の
適用により (ω-1)+1 = ω は有限集合ということになるわけだから、ωの定義に反するわけ
だということだったのですが。
348:１３２人目の素数さん
05/04/26 21:58:22
その例だと帰納法を適用できるかどうかの方が問題になってしまうと思う。
使うとしたら余帰納法だろう。
349:１３２人目の素数さん
05/04/26 22:50:02
>>348
有限順序数は帰納的順序数として定義されているのではなかったか。
350:１３２人目の素数さん
05/04/27 00:12:26
可算、非可算てのは個数というより位相的な性質なのであって、
「濃度」という訳はけっこう名訳のような気がする。
351:１３２人目の素数さん
05/04/28 00:41:45
不完全性定理の補助定理で
Aが公理系Nで証明可能であるなら、AからPr（g（A））を導き出してよい
公理系Nがｗ無矛盾であるなら、Pr（g（A））からAを導き出してよい
というのがありますが、
これは、「Aが証明可能である」から、（そういう意味のようなものを持ってる）Pr（g（A））を使ってもいいよ、
ということなのか、
そんなことではなくて、
ただ、形式的体系上の２つの記号列の関係として、（推論規則のような形で）
Aという論理式からPr（g（A））という論理式を導き出してもいい、（意味のようなものは関係なくて）
ということなのか、
ちょっと、わからないでいます。
誰か教えてください。