数学基礎論・数理論理学　その10

[表示 : 全て最新50 1-99 101- 201- 301- 401- 501- 601- 701- 2chのread.cgiへ]
Update time : 12/17 02:14 / Filesize : 227 KB / Number-of Response : 713
[このスレッドの書き込みを削除する]
[＋板最近立ったスレ＆熱いスレ一覧 : ＋板最近立ったスレ／記者別一覧] [類似スレッド一覧]


↑キャッシュ検索、類似スレ動作を修正しました、ご迷惑をお掛けしました

数学基礎論・数理論理学　その10

1 名前：１３２人目の素数さん [2011/10/29(土) 22:42:36.86 ]: 数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは岩波文庫「不完全性定理」 6.4 数学基礎論の数学化などを参照）

従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。

前スレ
数学基礎論・数理論理学　その9
kamome.2ch.net/test/read.cgi/math/1317639944/
29 名前：12 mailto:sage [2011/10/30(日) 14:08:37.52 ]: >>16
＞完全性定理を意味する長大な論理式の中に、
＞選択公理から推論される何らかの論理式を使わなければ、
＞論理式を整列することはできないことは簡単に想像できる。

日本語の文章になっていないと思われる。
完全性定理の証明において、論理式の整列が必要であり、
そのために、選択公理が必要という意味か？

＞ところが論理式をゲーデル数化することで、
＞この選択公理が不要になることもわかっている。
＞事実不完全性定理の対角定理で
＞選択公理が不要なのはこの議論による。

これまた意味不明。
ゲーデル数化によって選択公理なしに完全性定理が証明できる
といっているのか？それは初耳だ。あなたが証明したのなら
ぜひ論文を書いて、専門誌に発表したほうがいい。
30 名前：12 mailto:sage [2011/10/30(日) 14:11:40.14 ]: >>15
＞集合論という理論の中で成立している特定の定理を、
＞どうすれば具体物に適用できるのか、正当化できるのか

もし15=13で、
「理論Tの任意のモデルでAが成り立つ」
という手法を理論Tで使うことが正当化できるのか
という意味なら、そもそもそういう目的で考えられた
ものではないというしかない。
31 名前：12 mailto:sage [2011/10/30(日) 14:16:41.51 ]: >>14
>「ゲーデル数xは、PAの項である」を再帰的に表す算術上の述語
>はどのようにして定義すればよいのでしょうか。

それは、PAの項をいかなる形で数に翻訳するかによる。
もちろんやり方は一つではない。
32 名前：12 mailto:sage [2011/10/30(日) 14:22:50.24 ]: >>23
>普通数学をやるときには素朴集合論の命題を
>ミニマムな前提としてやるから、素朴集合論の命題が
>すべて正当化できる論理なら間違いないと思う。

「素朴集合論」という言葉が指し示す理論が明確でない。
おそらくラッセルのパラドックスが起きるようなものではない
だろうが、その場合の公理系が明確ではない。
例えば、フレンケルの置換公理を採用せず、そのかわりに
分出公理を採用するというようなものだろうか？。
33 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 14:29:17.25 ]: >>19
レスありがとうございます。

xが項を引数に持つ関数

具体的には、どのように表すのですか？
34 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 14:33:09.27 ]: >>31
PAの各記号に一対一で自然数を対応させて、それを素数の指数に当ててやる方法で考えた場合は、どうなるんでしょうか？
35 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 14:33:34.82 ]: >>27
> 一般の数学者が、集合論を意識しないのは随意だが
> 大抵のものは集合論の定理となる。
> 完全性定理を記述する際には集合の概念が必要。

これらには、形式化とは何かということの考察が抜けている。何をどう表現
するかを考察すれば、最後の「集合の概念」というのは形式化された集合論
のことではないことに気がつくはずだ。
36 名前：１３２人目の素数さん [2011/10/30(日) 14:42:41.82 ]: メタ理論のこと？
それ言ったらロジックなんて何もはじまんないと思うけど。
37 名前：12 mailto:sage [2011/10/30(日) 14:44:11.80 ]: >>35
＞これらには、形式化とは何かということの考察が抜けている。

ええ、形式化については言及していませんから。
（終）
38 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 14:52:05.30 ]: 参考にしている本には、IsTerm(x)を以下のように定義するとありました。

:= x=/0/
またはヨn<x (IsTerm(n)かつ/S/*par(n))
またはヨm<x ヨn<x ［IsTerm(m)かつIsTerm(n)かつ(par(m)*/+/*par(n)または par(m)*/・/*par(n) )］
とありました。
ただし、/x/はxのゲーデル数、x*yはxとyを連結させたゲーデル数を、par(x)は/(/ * x * /)/とします。

これは正しい定義になってるのでしょうか？
・再帰的な定義になっている
・" )(+-0S(0) "などというPAの項にはならないテキトーな記号列のゲーデル数は、IsTermでも真にならない。
この二点がよくわかりません。
39 名前：12 mailto:sage [2011/10/30(日) 14:54:31.74 ]: >>8
＞完全性定理の証明を形式化したとき
＞論理式に選択公理が入ってるってこと。

この人の「形式化」という言葉の使用法は独特ですね。

どうも、数学の命題を必要な前提条件をつけた上で
一階述語論理の論理式で書き表す行為を「形式化」
とよんでいるようです。

それはともかく、この言葉、実際は不要ですね。
なぜなら単純に
「完全性定理を証明するのに選択公理が必要」
と書けばいいだけなので。
40 名前：12 mailto:sage [2011/10/30(日) 14:56:33.92 ]: >>38
まず再帰的という言葉の意味は御存知ですか？
41 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 15:03:22.33 ]: よく知られたことだが、完全性定理を証明するのに選択公理が必要なのは
公理系あるいは、論理式が整列されていない場合で、PA, ZFC など自然な公理
系に関する完全性定理には不必要だ。形式化したときという意味が不明。
>> 37
形式化を考えないなら、18 にあるような PA での完全性定理という表現は
ナンセンスになる。
42 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 15:05:48.23 ]: >>40
ある関数fが再帰的
⇔初期関数であるか、または再帰的関数から関数合成で得られた、または再帰的関数から原始帰納法でえられた、または再帰的関数から最小化でえられた関数

ある述語が再帰的
⇔特性関数が再帰的関数である。

と理解してます。
43 名前：１３２人目の素数さん [2011/10/30(日) 15:10:32.52 ]: >>38
・IsTermの定義にIsTermが出てくるから
・意味をなさない記号列はゲーデル数化していないから
44 名前：12 mailto:sage [2011/10/30(日) 15:12:48.17 ]: >>41
＞よく知られたことだが、（中略）
＞PA, ZFC など自然な公理系に関する
＞完全性定理には（選択公理は）不必要だ。

いつ、どこでお知りになられましたか？
この件に関して「よく知っている」のは
あなた一人である可能性が高いので。
45 名前：１３２人目の素数さん [2011/10/30(日) 15:14:06.58 ]: >>41
上の議論の完全性って1階論理の話じゃないだろうか。
46 名前：12 mailto:sage [2011/10/30(日) 15:14:47.94 ]: >>42
ではｆの定義が、再帰の定義に沿っているかどうか
確認していただけますか？
>>43
＞・意味をなさない記号列はゲーデル数化していないから
間違ってますね。
47 名前：１３２人目の素数さん [2011/10/30(日) 15:15:59.23 ]: >>41
それらの体系には無限個の公理が存在しますがどうやって整列させますか？
48 名前：43 [2011/10/30(日) 15:19:47.81 ]: そうですね。
再帰的定義で項が閉じてるから
項じゃないものは当然入ってきませんね
49 名前：12 mailto:sage [2011/10/30(日) 15:21:32.34 ]: >>41
＞形式化を考えないなら、

41＝35＝8　でしょうか？

>>8のいわれる「形式化」は「公理の明示」の意味ですね。
もちろん、いかなる公理に基づいているかは明示する必要があります。
（もっとも、これを「形式化」という人はあなただけですが）

>>18のいわれる証明は知らないので、なんともいえません。
50 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 15:28:42.80 ]: >>47
>>44
よく知られていることは、初めに与えられた述語、関数記号が整列されて
いる場合、論理式は有限列であるから、長さ n に関する帰納法で、おのおの
の n についての整列を定義することができ、これらの和が、論理式全体の整列
を与える。
51 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 15:31:16.68 ]: >>49
当り前だが、8 は別人だよ。それより 50 をよく勉強しなさい。
52 名前：12 mailto:sage [2011/10/30(日) 15:40:07.63 ]: >>50
＞初めに与えられた述語、関数記号が整列されている場合、

で、PAやZFCでは、述語、関数記号が整列されていることは
「よく知られている」のですか？

よく御存知とはおもいますが、関数記号の中には定数記号も含まれます。
定数記号も整列可能である、と断言できるのですね？
53 名前：12 mailto:sage [2011/10/30(日) 15:42:06.10 ]: >>51
＞当り前だが、8 は別人だよ。
書いている当人にとっては当り前でしょうが
それ以外の人にとってはそうではないんですよ。

このことが、アスペルガー症候群の人には
理解しがたいといわれていますが。
54 名前：12 mailto:sage [2011/10/30(日) 15:45:32.98 ]: >>51
＞50 をよく勉強しなさい。

>>50の前提条件である
「初めに与えられた述語、関数記号が整列されている場合」
にはその通りでしょう。重要なのは上記の前提条件は
PAやZFCにおいて成立するのか？という点です。

>>52にも書きましたが、関数記号の中には定数記号も含まれます。
定数記号も整列可能である、と断言できるのですね？
55 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 15:55:24.82 ]: ZFC には定数記号はない。ε と = (述語記号か論理記号かは流儀による）
以外は変数記号と論理記号だけ。
PA の定数記号は　0 だけ。PA の関数記号は S だけ。

当たり前というのは、50 のようにすっきり書ける人と 8 のようにごてごて
書いている人の違いはわかるだろうという意味だが、52 のようなことを書いて
いる人にはわからないかもしれないね。
56 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 16:03:46.11 ]: 54 のようなことを書いてあるので、変数記号についても書いておこう。
変数記号は、自然数によって番号付けられているから、整列されている。

もう少しついでに書いておこう。ゲーデル数を対応させて、有限列を自然数
に対応させることがわかれば、すべての文字列に自然数が対応し、これは単射
だから整列されていることは明らか。50に書いてあるのは、可算でなくても
整列されていればよいということ。
57 名前：12 [2011/10/30(日) 16:33:12.46 ]: >>55
なるほど。定数記号に関しては明らかでした。

ところで>>8も引用は長いですが、
文章は三行なので「ごてごて」とは思えません。
したがってやはり自明とはいえません。
58 名前：12 [2011/10/30(日) 16:46:44.25 ]: >>55-56
とはいえ、モデルの各元に対して、元々の理論の中に存在しない
定数記号を付加することが可能であるので、その場合、モデルの
濃度によっては、整列するために選択公理が必要でしょう。
59 名前：12 [2011/10/30(日) 16:54:58.46 ]: >>58
＞ゲーデル数を対応させて、有限列を自然数に対応させることがわかれば、
＞すべての文字列に自然数が対応し、これは単射だから整列されていることは
＞明らか。
＞50に書いてあるのは、可算でなくても整列されていればよいということ。

自然数だから整列可能、といいたいようですが、それは自明ですか？

一階述語論理上で公理化された自然数論のモデルは範疇的ではありません。
当然、非標準的なモデルもありますよ。
60 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 17:02:39.81 ]: >>58 >>59
いい加減にしたらよい。44のようなことを書いたことが恥ずかしい
と思ったらどうかね。
自然数論のモデルというのなら、もちろん、整列できないモデルさえ
つくれる。しかし、今、完全性定理を証明しようとしているので、
そんなものが問題にならないのは明らかだ。要するに偉そうに、答え
たり、しているが、ちっともわかっていなかったということだ。
恥ずかしいと思うことを、初めにしたらよい。
61 名前：１３２人目の素数さん [2011/10/30(日) 17:11:13.56 ]: >>60
＞44のようなことを書いたことが恥ずかしいと思ったらどうかね。

あなたが41で「可算（濃度）モデルにおける完全性定理」
と書いていれば、そういうこともいえたであろうが・・・

＞自然数論のモデルというのなら、もちろん、
＞整列できないモデルさえつくれる。
＞しかし、今、完全性定理を証明しようとしているので、
＞そんなものが問題にならないのは明らかだ。

完全性定理には、モデルの濃度の制限はない。

＞要するに偉そうに、答えたり、しているが、
＞ちっともわかっていなかったということだ。

「偉そうに」と思ったのは貴方の勝手。
あなたもモデルの濃度を全く考慮していなかった。
つまりわかっていなかった。
あなたは、わからないことは恥と思うのであれば
まず自分自身を恥じたらよい。

もっとも、そういう考え方は狂っている、と私は思うが。
62 名前：１３２人目の素数さん [2011/10/30(日) 17:15:13.99 ]: ところで、私には、41が完全性定理の前提から
選択公理を除こうとする理由が理解できない。
63 名前：１３２人目の素数さん [2011/10/30(日) 17:30:18.48 ]: ところで全くの脱線だが

>>60
＞いい加減にしたらよい。
＞恥ずかしいと思うことを、初めにしたらよい。

こんなおかしな喋り方をする
アニメのキャラクターでも
いるのかね？
64 名前：42 mailto:sage [2011/10/30(日) 17:48:15.19 ]: >>46

>ではｆの定義が、再帰の定義に沿っているかどうか
>確認していただけますか？

IsTermの特性関数が再帰的関数になるか考えてましたが、やっぱりまだ分かりません。(直感では、IsTermが再帰的であること、計算可能であることは分かります。)

IsTerm(x)の定義の中に、m<xなるmに対して再びIsTerm(m)が出てきてるので、特性関数は原始帰納法によって一部定義されであろうことまでは分かるのですが、、、。
もしかして、IsTermの特性関数は累積帰納法で表しますか？
65 名前：8 [2011/10/30(日) 18:07:39.86 ]: しばらく見ない間に議論が起きましたが
足りない部分について補足しますね＾＾；

>>29
ゲーデル数は全順序になるので、
整列可能定理が不要になるのです。
>>39 >>49
私は形式化という言葉をかなり広い意味で使っています。
確かに誤解が多い書き方だったと思いますね。
>>64
再帰的関数と再帰的述語だけでできた論理式は再帰的と考えて良いですよ。
定義からやり直すと煩雑すぎます。
66 名前：15 mailto:sage [2011/10/30(日) 18:22:01.69 ]: >>41
論理式が整列されてるってことでなぜ救えるのかわかりませんね。

>>50
> これらの和が、論理式全体の整列を与える。
証明というものを具体的な対象物として見る場合、これはちょっと受け入れられない論法ですね。

>>60
> しかし、今、完全性定理を証明しようとしているので、そんなものが問題にならないのは明らかだ。
これは了解

>>61
> 完全性定理には、モデルの濃度の制限はない。
これは誤解していると思う。
67 名前：8 [2011/10/30(日) 18:49:24.69 ]: >>66
だよな、そもそも1階論理の完全性の話してんのにな。
それにはじめてに論理式に識別番号つけて整列させてんなら
言語定義すんのに整列可能定理が必要ｗ
しわを伸ばしてみたら、しわの位置が変わっただけｗ
68 名前：42 mailto:sage [2011/10/30(日) 19:41:37.61 ]: >>65

>再帰的関数と再帰的述語だけでできた論理式は再帰的と考えて良いですよ。

定義しようとしている述語が、別の述語を使って定義されていれよいのですか、今考えているIsTerm は定義中に再びIsTermが現れているのが問題なのです。もっといえば、そうである以上原始帰納法を使って定義できるはずなのですが、それがなかなか分からないのです。

ちなみに今、考えているのは論理式ではなく形式化されていない算術の述語なのですが。
69 名前：15 mailto:sage [2011/10/30(日) 20:15:11.07 ]: 別に数理論理学が数学の基礎付けに関わらなくても全然構わないんだけど、
完全性定理に限っては普遍的に成り立ってくれなきゃ困るんだよ。

「超越的な方法を認めなくても結果的に有効」であって欲しいのです。
70 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:20:18.99 ]: ところで42は
Proof(x,y):=yはゲーデル数xの論理式の証明である
が再帰的述語であることは理解していますか？
71 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:21:54.46 ]: 訂正：証明である→証明のゲーデル数である
72 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:37:40.00 ]: >>69
よく分かりませんが、あなたのその願いがいつか叶うことを祈っておきます
73 名前：42 mailto:sage [2011/10/30(日) 20:43:22.86 ]: >>70
再帰的になるということは、各文献で目にしていますが、確認はしていません。
なので、現在はproof(x,y)が本当に再帰的な述語であるかどうかを確認するため、これを構成する際に必要な諸々の述語を再帰的かどうか確認しています。
とまぁ、この過程で今「ゲーデル数xはPAの項である。」でどんづまっています。
74 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:43:44.52 ]: 「超越的な方法」というのがWKLのことなら、
WKL が PRA 上の保存拡大だから「結果的に有効」なんじゃない？
75 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:53:29.84 ]: >>72
>>74
「超越的な方法」とはPRAそのものだろ。
76 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 20:59:37.82 ]: >>67 >>69
チミたちには難しすぎるようだが、選択公理が必要なのは、一般的な
設定の場合で、具体的なもの、例えば、PA, ZFC では論理式は、自然な
方法で整列できるのだよ。
77 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 21:03:46.06 ]: >>73
論理式Aが証明可能であるということの定義は
Aに至る論理式の有限列が存在して、その列の各項が公理か、以前の論理式から導かれること
というのは理解していますか？

もし、理解していればそれと同じような感じで
有限記号列Tが項である⇔
Tに至る有限記号列の有限列が存在して、……
と表せるのは理解できますか？
78 名前：69 mailto:sage [2011/10/30(日) 21:06:17.15 ]: >>76
オレは別に「整列」とは言ってないが、お前ほんとに具体的なものについて語ってるか？
項、式、証明ってほんとに具体的なものなんだぞ？
79 名前：１３２人目の素数さん [2011/10/30(日) 21:20:37.41 ]: そもそも1階述語論理が
もろに対数学用述語論理だかんね
命題論理の完全性定理だけ考えりゃええんやないの？
それに論理体系を集合論で記述せにゃあかんこともないやろ
そもそも初期の頃は高階述語論理がスタンダードやて
その後に1階論理にしぼらな決定可能な完全性こしらえた証明体系つくれへんし
LS定理やらも意味もたへんさかい現状の1階論理さ注目されたんど
わいはエルブラン領域でスコーレム＝エルブランの完全性定理使っちくりゃ
-----エルブランは有限主義で選択公理嫌いでさかい信頼できんど------
ヘンキンさにペコペコ頭下げといて極大集合こしらえる必要もあらへんやろ
まぁ論理プログラミングさまさまやないけ
80 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 21:31:31.69 ]: まあもうちょっと真面目に書いていただければ助かるのですが・・・
81 名前：１３２人目の素数さん [2011/10/30(日) 23:16:26.46 ]: 電線やハブや変圧器が電気メーカーにより製造される。
各家庭には様々な種類の電化製品が設置されている。
そしていくつかの発電施設が存在している。
例えば、あなたは今部屋の電灯を点けたとする。
このとき発電施設からいくつかの電線やハブや変圧器を
辿って行けばあなたの電灯に到達することは確実だ。
電灯が点けば真、発電施設が公理、ハブや変圧器が推論規則、
発電施設から電灯までの電線が証明だ。

電灯が点くなら、発電施設から電灯まで辿る電線がある。
これが完全性定理の内実である。
82 名前：42 mailto:sage [2011/10/30(日) 23:25:54.39 ]: >>77
もととなるものと、それをもとにして生成する規則の二つがあればよいということでしょうか？
形式的体系でいえば、もととなるのは公理で、生成規則は推論規則になります。
項でいえば、0と変数がもとなるもので、Sと+と・が生成規則になると。
83 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 23:36:10.57 ]: >>82
はい、そういうことです

今、ビデオ見てるんで一旦落ちます
84 名前：42 mailto:sage [2011/10/30(日) 23:44:06.37 ]: 見当違いのことを言ってたら訂正をお願いします。

私が理解できないのは、
1. 形式的体系PAの各記号を自然数に一対一対応させる。
2. PAの記号からなる有限列(項や論理式)を、ある自然数に一対一対応させる。(エンコードの方法は、素因数分解を利用した関数とする。)
3. PAの記号からなる有限列(項や論理式)の有限列(証明のこと)を、上と同じ方法で自然数に一対一に対応させる。

4. 以上の考えをベースにして、形式的体系に関する概念を、算術上の述語として表現する。

5. 述語 IsTerm (x)「xは形式的体系PAの項である。」
⇔ x=/0/
またはヨn<x (IsTerm(n)かつx=/S/*par(n))
またはヨm<x ヨn<x ［IsTerm(m)かつIsTerm(n)かつ(x=par(m)*/+/*par(n)または x=par(m)*/・/*par(n) )］

このように考えた上で、私がわからないのは、
・5の定義は正しいのか
・正しいとしたら、5におけるIsTerm の特性関数はどのようになものになるのか
の二点です。
どうか教えてください。
85 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 00:46:40.15 ]: >>84
今戻りました

項Tに対して、Tに至るまでの記号列の列T1,T2,...,Tn=Tを考える
これを項Tを生成する列と呼ぶことにして、この列にゲーデル数を対応させる
yはゲーデル数xの項を生成する列のゲーデル数であることを表す述語をMakeTerm(x,y)とでもしておく
項の生成の仕方より列に現れるT1,T2,...,Tnのゲーデル数はTのゲーデル数以下なので
xに対してyはある関数g(x)で上から抑えられるはず
そのときIsTerm(x) :=∃y<g(x) (MakeTerm(x,y)) と表される

これでわかりますか？
86 名前：42 mailto:sage [2011/10/31(月) 01:03:17.00 ]: >>85
レスありがとうございます。

仰ってることは(たぶん)分かっております。
私が知りたいのは、ではそれを具体的にどうやって再帰的関数(および述語)の形で表すのか、ということです。85さんの説明でいえば、MakeTermは、ではどうやって定義されるのでしょうか。おそらくMakeTerm の特性関数は原始帰納法の形、つまり
f(0)=g(x)
f(x+1)=h(x,f(x))
という形になると思うのですが、その具体的構成方法を知りたいのです。
これを定義するには、準備としていくつかの関数と述語を定義しないとだめだということは分かってますが。。。
87 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 01:22:01.06 ]: >>86
特性関数考えるより具体的にMakeTermがどう表現されるか考えた方が早いですよ

T1,T2,...,Tn=TがTを生成する列である⇔∀p=1,2,...,n [Tp=0∨∃q<p {Tp=S(Tq)} ∨∃r<p ∃s<p {Tp=(Tr)+(Ts) ∨ Tp=(Tr)*(Ts)}]
あとはこれをゲーデル数に書き換えればOK
88 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 01:26:58.78 ]: >>87
すまん最後に　∧ Tn=T が抜けてた
89 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 01:32:21.66 ]: あと気になったが変数記号は定義に無かったか？
90 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 01:52:22.65 ]: あした早いんでもう寝ますzzzzz
91 名前：42 mailto:sage [2011/10/31(月) 02:08:52.15 ]: それだと、Prove(x) (⇔ヨyproof(x,y) )が再帰的でないのと同様に、IsTerm (x)も再帰的でなくなってしまうような気がするのですが。

理解力がなく申し訳ないです。
身近に教えてくれる人がいればいいのですが、なにぶん独学なもので。。。
また明日しっかり考えてみようと思います。今日はご丁寧にありがとうございました。
92 名前：42 mailto:sage [2011/10/31(月) 03:50:15.46 ]: 結局まだうだうだ考えてたのですが、

累積帰納法で得られた関数は、再帰的関数である。

ということを証明できれば、私の疑問点は解決できることがわかりました。
93 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 04:52:16.35 ]: Foundations of Mathematics への入会ってどうすればいいのか誰かご存知ですか？
94 名前：12 mailto:sage [2011/10/31(月) 07:02:50.15 ]: >>69
>別に数理論理学が数学の基礎付けに関わらなくても全然構わないんだけど、
>完全性定理に限っては普遍的に成り立ってくれなきゃ困るんだよ。

「普遍的に成り立つ」という言葉で、
どういうことを期待しているのか不明。

>「超越的な方法を認めなくても結果的に有効」であって欲しいのです。

モデル理論は超越的であると私は思いますが、
あなたは、なぜ、違うと思うのでしょうか？
95 名前：12 mailto:sage [2011/10/31(月) 07:05:41.79 ]: >>76

>>58　の
＞モデルの各元に対して、元々の理論の中に存在しない定数記号を
＞付加することが可能であるので、その場合、モデルの濃度によっては、
＞整列するために選択公理が必要でしょう。

を理解できなかったようですが、付加はできないと思ってますか？
そう思う理由はなんですか？付加できるとは聞いていないからですか？
96 名前：12 mailto:sage [2011/10/31(月) 07:09:34.70 ]: >>67
＞そもそも1階論理の完全性の話してんのにな。

だから「対象の個数は可算個でいい」と？なぜ？
97 名前：8 [2011/10/31(月) 08:12:47.78 ]: >>96
＞> しかし、今、完全性定理を証明しようとしているので、そんなものが問題にならないのは明らかだ。
＞これは了解
いえここへのレスです。
98 名前：１３２人目の素数さん mailto:sage [2011/10/31(月) 08:33:10.20 ]: >>91
g(x)が再帰的関数、P(x,y)が再帰的述語のとき、∃y<g(x) P(x,y) も再帰的述語になるということはご存知ですか？

Prove(x) (⇔ヨyproof(x,y) ) の場合、yを上から抑えるg(x)が存在しません
例えば、論理式Aを証明する過程でむちゃくちゃ長い論理式を経由しなければならない場合もあるかもしれないのです

一方、項の定義では、生成規則は必ず生成前のより生成後の方が記号列の長さが大きくなるように作られています
したがって、項Tを生成する列T1,T2,...,Tnで n≦(Tの長さ)、かつ∀p=1,2,...,n Tp≦Tとなるようなものを具体的に作ることが可能です
よって、yを上から抑えるg(x)が存在することになり、結果IsTerm(x)も再帰的になるのです
99 名前：42 mailto:sage [2011/10/31(月) 22:06:24.97 ]: >>98
よくわかりました！！

今日一日中考えてやっと理解できました。
ありがとうございます。
100 名前：１３２人目の素数さん [2011/10/31(月) 22:49:21.54 ]: g(x),f(x,y),f(x,g(x)),P(x,y)∊PR

∃y<g(x) P(x,y)
⇔ Π_[y<g(x)] f(x,y)＝0
　≡ f(x,g(x))・Π_[y<g(x)-1] f(x,y)＝0
　≡ f(x,g(x))・f(x,g(x)-1)・Π_[y<g(x)-2] f(x,y)＝0
　：
　：
　≡ f(x,g(x))・f(x,g(x)-1)・...・f(x,g(x)-g(x))＝0

∃y<g(x) P(x,y)∊PR　　　　　　　　　　　　　　　　　　□
101 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 00:04:23.72 ]: >>94-96
どうもまわりくどい書き方だな。
モデル理論は超越的だとオレも思うし、違うなんて言ってないよ。
「普遍的に成り立つ」という言葉は普通の意味にとってくれ。

完全性定理が普遍的には成り立たないとしたら何がおこるんだろうか。
AがTで妥当であり、T[￢A]もT[A]も矛盾していない、
実例を作れたらな。
102 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 01:46:19.25 ]: 論理学の根本的な部分について質問させてください。
論理学では論理を形式化して考察していきますが、
メタな論理としてどこまでのレベルのものを許すのかということは考慮されるんでしょうか？
たとえば述語論理の体系では集合の概念を用いて理論が展開されますが、
より初等的な概念で展開することは可能でしょうか？
103 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 03:21:57.74 ]: >>102
考慮するときもある。
が、しかし、入門的な教科書ではそれは一旦脇に置いておく書き方をするのが普通。
もっと高度なことをやるときには考慮しないといけなくなるけれど、
そういうことをやる為にはまず脇に置いた議論をきちんと理解していることが前提となる。
104 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 06:12:25.61 ]: 12,8 あるいは 15 という方たちは、ある程度の知識はお持ちのようだが、どう
もよくわかっていないようなので書いておこう。
述語論理の完全性という場合、述語論理をどう述べるかということがある。
述語記号、関数記号、定数記号が自然数で番号が付けられているかどうか？
あるいは順序数で番号付けられているかどうか？
次に完全性定理をどのように述べているかを調べる。例えば、無矛盾な公理
系に対してと書いてあるような場合、一般には、述語論理は、この公理系の
言語を含むものに拡大されていることになる。
これらのことが、完全性定理が選択公理と関係するかどうかの鍵である。
最初に書いた自然数で番号付けられた言語からはみ出なければ、選択公理
は不要なのだ。
105 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 06:37:38.03 ]: >>104
>一般には、述語論理は、この公理系の言語を含むものに拡大されていることになる。

それはその通りだし、可算な言語からはみ出ないと限定してもいいけど、
その場合でも、自明で基礎的な算術だけで証明できるわけじゃないでしょ？
106 名前：12 mailto:sage [2011/11/01(火) 07:19:22.56 ]: >>69 >完全性定理に限っては普遍的に成り立ってくれなきゃ困るんだよ。
>>94 >「普遍的に成り立つ」という言葉で、どういうことを期待しているのか不明。
>>101 >「普遍的に成り立つ」という言葉は普通の意味にとってくれ。

「普遍的に成り立つ」という言い方は普通しませんので
”普通の意味”というのは意味不明です。
107 名前：12 mailto:sage [2011/11/01(火) 07:21:40.31 ]: >>101
＞完全性定理が普遍的には成り立たないとしたら何がおこるんだろうか。
＞AがTで妥当であり、T[￢A]もT[A]も矛盾していない、実例を作れたらな。

「妥当」という言葉の定義は御存知ですか？

AがTで妥当であって、￢AもTで妥当である、という場合も存在しますよ。
108 名前：12 mailto:sage [2011/11/01(火) 07:27:06.40 ]: >>104
>一般には、述語論理は、この公理系の言語を含むものに拡大されていることになる。
>>105
>それはその通りだし、可算な言語からはみ出ないと限定してもいいけど、
>その場合でも、自明で基礎的な算術だけで証明できるわけじゃないでしょ？

104は、論理式の整列と選択公理の関係しか見ていないようだが、
別の点にも注目する必要がある。

モデルを構築する際に、無矛盾性（妥当性、充足可能性を
チェックしているが、述語論理の決定不能性定理からいえば、
無矛盾（妥当、充足可能）か否かを判定できるアルゴリズム
は存在しない。
109 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 08:01:07.64 ]: >>107

101ではないが、
T|=A⇔Tの任意のモデルにおいて、Aは真ということだよな？
もし、T|=�Aだとしたら、Tの任意のモデルで�Aも真ということ。
ということは、Tの任意のモデルで、Aも�Aも真。こんなのってないよ、ありえないよ。
110 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 13:00:33.75 ]: >>98
定義の仕方、およびそれが再帰的になっていることはしっかり確認できました。ありがとうございます。

上から抑えるためのg(x)って具体的にはどんなものになりますか？
参考書には、g (x)=(p_len(x)＾2)＾x・len (x)＾2
とありましたが、どうしてこれが抑えるために十分なのかがわかりません。
111 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 14:10:23.41 ]: >>110
それはゲーデル数の定義によるから何ともいえんよ……
112 名前：１３２人目の素数さん [2011/11/01(火) 21:39:34.80 ]: 普通の1階論理なら完全性は成り立つよ。
普遍的にね。
113 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 22:09:33.16 ]: >>110から多分推測するに
Tをゲーデル数xの項として、Tを生成する列をT1,T2,...,Tnとする。Tの長さはlen(x)で表される
例えばT=(S1)+(S2)の形であれば、Tを生成する列の中にS1とS2があるはず。そうすると列の長さnは2^len(x)以下である
（>>98で n≦(Tの長さ)と書いたが間違いでした。すみません）また、T1,T2,...,Tnのゲーデル数はx以下である
よって列のゲーデル数は(p_1)^x・(p_2)^x…(p_len(x)^2)^x≦(p_len(x)^2)^x・len (x)＾2で抑えられる
114 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 22:16:15.70 ]: >>113
ミス
×そうすると列の長さnは2^len(x)以下である
○そうすると列の長さnはlen(x)^2以下である
115 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 23:20:51.62 ]: >>112
普通の1階論理ってなに？
関数や述語などが有限個であれば普通？

普遍的に成り立つって、追加の前提や仮定がまるっきり無用なの？
116 名前：１３２人目の素数さん [2011/11/01(火) 23:42:31.83 ]: >>69
普遍的において何を仮定しているのか不明ですけど、
そもそも述語論理での完全性定理は、
「ほとんどの証明体系で成り立たない」です。
例えば普通の真偽値では |＝￢A→(A→B) です。
証明体系を以下で定義します。
公理型 A→A
推論規則　MP
このとき |＝￢A→(A→B) ⇒ |-/-￢A→(A→B) です、何もできません。
つまり述語論理の中で完全な証明体系を探しているのであって、
述語論理は完全じゃないです。
本によってはLKの完全性定理とかNJの完全性とかちゃんと書いています。
117 名前：１３２人目の素数さん mailto:sage [2011/11/01(火) 23:52:04.97 ]: そういう話じゃないみたい
118 名前：１３２人目の素数さん mailto:sage [2011/11/02(水) 00:01:10.42 ]: HJは真偽値が3つないと完全にならなかったな。
119 名前：12 mailto:sage [2011/11/02(水) 07:08:29.92 ]: >>109
>T|=A⇔Tの任意のモデルにおいて、Aは真ということだよな？

ああ、妥当を充足可能と同義だと思っていたが、誤解だった。

その場合
「AがTで無矛盾」というのは
「AがTで充足可能」という意味で、
「AがTで妥当」とは違う。
120 名前：12 mailto:sage [2011/11/02(水) 07:12:22.84 ]: >>112
>普通の1階論理なら完全性は成り立つよ。
>普遍的にね。

その場合の完全性は
「1階論理のどのモデルでも真な命題
　（つまり1階論理で妥当な命題)なら
　1階論理で証明可能」
という意味。
121 名前：12 mailto:sage [2011/11/02(水) 07:17:43.40 ]: よく述語論理の完全性定理を
「述語論理の命題Pは、かならず
　P自身かその否定￢Pのいずれか
　が証明可能」
と思っている人がいるが誤り。

論理の完全性は、理論の完全性とは意味が異なる。

ところで
「無矛盾で完全な理論T、つまり、理論Tが、
　命題Pかその否定￢Pのいずれかを必ず証明出来る
　場合には、モデルが存在する」、
という命題はWKL0ではなくRCA0で証明可能。
122 名前：８ [2011/11/02(水) 08:13:31.03 ]: >>117
>>69が訊きたいのはかなり原理的なレベルの話だと思うのです。
完全性定理は「数学に使える位まともな論理」だけで成り立つということです。
例の述語論理の決定不能定理も、Qが展開できる程度の証明体系に限定されますから。

ところでWKL0⇒リンデンバウムの補題⇒完全性定理ですが、
>>69が問題にしているのは可算な述語論理の言語の完全性定理の
RCA0への翻訳だと思いますよ、つまりチャーチの提唱レベルの話でしょう。
123 名前：１３２人目の素数さん mailto:sage [2011/11/02(水) 09:34:34.03 ]: やはり逆数学という、基本的に後ろ向きの数学の一派の話なわけだ。
原理的というには、話をせまくしすぎている。
124 名前：１３２人目の素数さん mailto:sage [2011/11/02(水) 09:38:20.21 ]: >>123 ですね。
こういうものは、基本的に
公理の数をいくら減らせるか、という話なので、
大きな目標なり企みなりがあってこそのもので、
そうでなければ、スケールの小さなテーマに終わってしまう。
125 名前：１３２人目の素数さん [2011/11/02(水) 13:20:55.22 ]: 比較的新刊のフランセーン『ゲーデルの定理』を中身見ないで注文しようかどうしようか
迷っているんだが、もう読んだ人どうよ？
126 名前：１３２人目の素数さん mailto:sage [2011/11/02(水) 13:30:58.77 ]: 逆噴射数学
127 名前：１３２人目の素数さん [2011/11/02(水) 19:16:02.80 ]: >>125
基本的に読み物ね。
具体的な数学的内容は全くないです。
不完全性定理の社会的視点ですね。
新書のゲーデルの哲学とかのもう少し詳細なものですかね。
128 名前：１３２人目の素数さん [2011/11/02(水) 19:22:46.29 ]: >> 127
ありがとう。数学的内容がないということなのでやめときます。
（さっき訳者あとがきPDFを見たらそうでもないように見えたが）
129 名前：あのこうちやんは始皇帝だった mailto:shikoutei@chine [2011/11/02(水) 19:29:37.64 ]: ＞＞１２８
　お前、早く、社会人にならないと、取り返しがつかないことになるぞ！
130 名前：１３２人目の素数さん mailto:sage [2011/11/02(水) 19:55:42.02 ]: 彼女にフェラチオさせてから寝るか・・
131 名前：１３２人目の素数さん [2011/11/02(水) 20:03:02.10 ]: >>128
数学的内容というのは語弊があった。
定義・定理・証明みたいな流れがないってこと。
不完全性定理の解説については岩波文庫の例の本の解説と同じレベル。
132 名前：１３２人目の素数さん [2011/11/02(水) 20:51:55.88 ]: >> 131
了解。ありがとう。
133 名前：8 [2011/11/02(水) 22:34:43.03 ]: >>123
1派ではない、Simpsonの本しか読んだことない。
>>132
ただしゲーデルの定理とかいう本はまともな本。
「どんな体系で不完全が成り立つんだろ」
「決定不能とかって不完全性とどう関係してるんだろ」
「自己言及ってどんな種類があるんだろ」
みたいな疑問があったら読んでみるといいのでは？
既に不完全性定理を知っている人は
立ち読みか図書館で興味あるとこに目を通すだけで充分。
134 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 00:25:00.08 ]: 逆数学が仮に分類だから狭いとしても、代数多様体の分類とおなじく、
分類を証明する手段が数学をゆたかにするっていうこともあるよね。
135 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 01:52:39.31 ]: 逆数学が狭いといわれるのは、分類だからではなく、研究対象が二次的
であることにある。
136 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 04:24:21.82 ]: 研究対象が二次的だと何故狭くなる？その二つがどう結びつくのか皆目見当が付かない。
137 名前：8 [2011/11/03(木) 06:36:37.24 ]: 逆数学は数学を計算クラスの視点から階層化している気がする。
例の2階算術の部分体系も様々なチューリングマシンで置き換えられるし。
純粋に好奇心をそそられる研究だと思うけど。
138 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 08:44:09.19 ]: >>137 重箱の隅とも言う。
139 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 08:51:45.25 ]: 二次的であれば重要度が減る。
三次、４次、とつづく研究をするか？

ある定理を証明するのに、ある公理系が必要十分であることを証明できたら、
次に、そのメタ証明を証明するのに、必要十分な公理系を証明する、
そのメタメタ証明を、、、

あ、私は135とは別人ね
140 名前：１３２人目の素数さん [2011/11/03(木) 08:52:33.58 ]: >>122
>完全性定理は
>「数学に使える位まともな論理」
>だけで成り立つということです。

ん？集合論は数学には使えないトンデモ論理だといいたがってる？
もしかして8は有限主義者？クロネッカーの生まれ変わり？
141 名前：１３２人目の素数さん [2011/11/03(木) 08:57:37.20 ]: >>122
>　ところでWKL0⇒リンデンバウムの補題⇒完全性定理ですが、
>　>>69が問題にしているのは可算な述語論理の言語の完全性定理の
>　RCA0への翻訳だと思いますよ、つまりチャーチの提唱レベルの話でしょう。

言語を可算に制限しても、理論が完全でない場合、
RCA0ではダメだよ。
142 名前：１３２人目の素数さん [2011/11/03(木) 09:08:24.32 ]: >>135
>逆数学が狭いといわれるのは、
>･･･研究対象が二次的であることにある。

そもそも「二次的」という言葉を
どういう意味で用いているのか不明。

数学の成果を「一次的」として、
その数学の前提をどれほど弱められるかが
「二次的」だということか？

もしそうなら、別に狭いともつまらんとも思わんが。
143 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 09:52:04.05 ]: （フランセーン『ゲーデルの定理』は）
>定義・定理・証明みたいな流れがない

それ、「流れ」じゃなく「スタイル」だろ。

フランセーンの本は数学書ではないよ。
読者層は数学科の学生ではなく数学に興味をもつ一般人だから。

とはいえ、いい加減なものかといえば全然違うけどね。
むしろ、数学科を出た人間も目からウロコが落ちる話が沢山書いてある。

岩波文庫「不完全性定理」とはまた違った意味で読み応えがある。
144 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 11:20:08.84 ]: 重箱の隅をつつくようなマイナーな研究は、私費でやるべき
145 名前：8 [2011/11/03(木) 12:41:34.25 ]: >>140
いいたがっていない。
集合論がどういった証明体系の述語論理の上にあるのか
普通は明示されないが、おそらく完全な述語論理の上で
つくられているので問題なし。
>>141
理論の完全の所を詳しくお願いします。
146 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 13:17:56.41 ]: >>145
>>141は完全の意を取り違えてるだけだから質問しても無駄だろう
147 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 14:23:15.33 ]: >>145
＞集合論がどういった証明体系の述語論理の上にあるのか
＞普通は明示されないが、おそらく完全な述語論理の上で
＞つくられているので問題なし。

8のいう「完全」の定義とは？
148 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 15:27:59.99 ]: どんな図形が描画可能か、という問題がある。
使っていいのは定規とコンパスだけか？
それとも２次曲線は描けるとするか？

使える道具はいろいろ仮定できるが、それらを組み合わせて「実際に」描画するのは
具体的で有限なプロセスでなければならぬ。
149 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:20:22.38 ]: >>148
なにやら唐突な書き込みだが、
過去の書き込みへの返答なのか？
150 名前：１３２人目の素数さん [2011/11/03(木) 16:26:05.53 ]: fdg
151 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:27:03.44 ]: 代数学の基本定理ですべての代数方程式に解があることが分かっているのに、
わざわざそれが代数的な解法を持つかどうか考えるのも二次的だな。
角の三等分は存在することが分かっているのに、作図できないことを示すのも二次的だ。
つまりガロア理論の金字塔的といわれる結果は重要度が低いのね。
152 名前：150 [2011/11/03(木) 16:31:17.57 ]: 間違えて書き込んでしまった...

ところで命題論理で￢、→、∧、∨だけでは
2値論理をすべて網羅することはできないみたいですね。
＝を付け加えてようやく16パターンが完成する。
153 名前：１３２人目の素数さん [2011/11/03(木) 16:42:28.85 ]: >>151
PAが不完全にもかかわらず、偽命題がPAで証明可能を意味する文を
PAの中で証明しようとしている。に対してはその理屈は成り立つ。
しかし逆数学が研究しているのは計算可能性の次数や算術や再起関数の階層であって、
今証明されている数学の定理をどれだけ少ない公理で証明できるかを研究しているわけではない。
154 名前：１３２人目の素数さん [2011/11/03(木) 16:43:36.63 ]: >>151
＞代数学の基本定理ですべての代数方程式に解があることが分かっているのに、
＞わざわざそれが代数的な解法を持つかどうか考えるのも二次的だな。

逆数学の話なら、「代数的な解法を持つかどうか考える」
という理解が間違ってる。

代数的な解の存在が、いかなる前提によって証明されるのか
を考えている。
155 名前：１３２人目の素数さん [2011/11/03(木) 16:49:48.77 ]: ああ、151は
解の存在証明が一次的
解法の存在が二次的
といいたいわけね。

そういう意味でいうと、
無矛盾性の証明不能性は一次的
命題の決定不可能性は二次的
ってことかい？
156 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:49:51.40 ]: >>154 で、その代数解の存在を証明するのに必要な前提が証明できたら、
その次には、その証明のためにはどんな前提が必要なのか、考えるのですね。
わかりまつ
157 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:51:13.61 ]: それは逆数学が二次的だから重要でないのではなくて、
逆数学が逆数学だから重要でない、と言っているに等しいが。
二次的だから重要でないのなら同じく二次的な代数的解法の不存在も重要ではないことになる。
158 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:51:33.32 ]: 数学では無く論理学ですね。
159 名前：１３２人目の素数さん [2011/11/03(木) 16:53:44.43 ]: >>156
ん？「代数解の存在を証明するのに必要な前提」は証明しないよ。

ミュンヒハウゼン（あるいはアグリッパ）のトリレンマって知ってる？
全ての命題に証明を求めるなら無限背進か循環論法に陥る。
独断は排除できないよ。
160 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 16:57:21.32 ]: ガロア理論にとって、代数解の存在云々は
理論のごく一部です。数の演算に関する本質的洞察を
含み、数学全土に応用があります。
本当にガロア理論勉強した事あります？
161 名前：１３２人目の素数さん [2011/11/03(木) 17:00:11.57 ]: >>157
「それ」とは>>153のコメント？

「計算可能性の次数や算術や再帰関数の階層」は一つの尺度に過ぎない。
例えばRCA0とWKL0の違いは何なのか、理解しないのなら意味がない。

二次的かどうかが問題なわけではないだろう。
代数的解法の存在も、代数的解法による解の意味が重要。
162 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 17:00:32.02 ]: >>159 そういう意味じゃ無い
163 名前：１３２人目の素数さん [2011/11/03(木) 17:04:21.38 ]: >>160
＞数の演算に関する本質的洞察

では、ガロア理論によって明らかになった、
「数の演算の本質」とはズバリ何？

あなた本当にガロア理論理解できてます？
教科書の記述を丸ごと記憶するのは勉強と違うよ。
164 名前：１３２人目の素数さん [2011/11/03(木) 17:05:03.23 ]: >>162　ではどういう意味？
165 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 17:07:07.82 ]: >>163 あなたはガロア理論理解してますか？Yes or No?
166 名前：153 [2011/11/03(木) 17:14:05.37 ]: RCA0とWKL0の違いはチューリングマシンの違いですね。
確かに次数やクラスは1つの視点ですね。
167 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 17:22:16.38 ]: >>166
具体的に説明されたい。
168 名前：8 [2011/11/03(木) 19:15:30.11 ]: >>152
複雑だけど￢と→だけできる。
￢(A→￢B)
￢(A→B)
￢(￢A→￢B)
￢(￢A→B)
の4つで1パターンで真になる命題が網羅できるので、
これの否定で3パターン真で命題が網羅できて、
4つの内2つを組み合わせて2パターンで真になる命題を網羅する。
4つ全部を組み合わせて恒真、その否定で偽をつくる。
これで16パターンが網羅できる。
169 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 19:49:36.91 ]: >>148
証明可能性を描画可能性になぞらえているのか？
コッホ曲線をどうやって描画する？
170 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 20:22:00.87 ]: >>163 まぁ、簡単にいうと、ガロア理論の
本質とは、
ある集合の構造を調べるときに、その集合を直接調べるのではなく、
その集合からその集合への写像の族を考え、
その族の構造を調べることが有効である。
ということ。それ以降の数学のあらゆる所で出てくる重要な考え。
171 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:16:48.67 ]: >>170
わざわざガロア理論とか数の演算の本質とかいうから
実に高尚極まりない整数論の奥義を語るかと思えば
数学のどこでもでてくるヌルい一般論じゃんｗ
172 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:22:30.85 ]: >>171
>>151が、ガロア理論を誤解して過小評価していたので、
ガロア理論の本質論が出たまで。
そう、今ではいたるところに普及した
重要な考え。
173 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:36:59.04 ]: >>172
ガロア理論の本質でもなんでもない。

例えば、ガロア理論→幾何学、集合→空間、写像→変換と置き換え
「幾何学の本質とは
　空間の構造を調べるのに、空間を直接調べるのではなく
　空間から空間への変換の族を考え、
　その族の構造を調べることが有効だということ」
といっても通じてしまう。

こんなヌルイ一般論を重要というのは・・・馬鹿ｗ
174 名前：１３２人目の素数さん [2011/11/03(木) 21:37:49.72 ]: >>168
その4つの式の最初に￢をつける意味は？
175 名前：１３２人目の素数さん [2011/11/03(木) 21:46:35.36 ]: >>174
￢(A→￢B)＝A&B
￢(A→B)＝A＆￢B
￢(￢A→￢B)＝￢A&B
￢(￢A→B)＝￢A&￢B
と思われ。
176 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:50:53.37 ]: 以前ツイッターで
「複素数は本来、数じゃ無い！」
とわめいていた数学者(？)がいた。

実数ではなく複素数、というところが素人っぽくて面白い。
どうも、全順序集合でないと、本来の数ではないらしいｗ
177 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 21:55:30.41 ]: 角度の値は、実数ではなく円周群の要素と考えたほうがいい。
円周群の要素を数と呼ばないのは、どう言い訳しても手抜かりである。
178 名前：8 mailto:sage [2011/11/03(木) 22:03:22.17 ]: >>174ない。
179 名前：１３２人目の素数さん [2011/11/03(木) 22:04:44.77 ]: 辞書的順序入れれば複素数も全順序になるよ
180 名前：８ [2011/11/03(木) 23:21:16.14 ]: ￢と∧∨は1つの述語にまとめられる。
A○Bを￢(A∧B)、
A◎Bを￢(A∨B)で定義すれば
どちらも2項述語1つだけで真理値表をすべて満たす。
A○Bの否定が(A○B)○(A○B)になったりする。
代数の演算を考えれば自明だが。
181 名前：１３２人目の素数さん mailto:sage [2011/11/03(木) 23:21:35.62 ]: >173
ガロア理論の重要なところの一つはその一般化できる構造なんじゃないの？
ガロア理論の説明で良く幾何学の証明不可能性の話が出てくるから
そうなんだと思ってたけど。
182 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 04:35:29.49 ]: >>160
ほんじゃガロア理論のごく一部であるところの
代数解の不存在云々（アーベルの定理？）は
二次的なので重要でないってことでおk?

つーか、ガロア理論の一部とか思ってるの？
一部ではなくて、単に金字塔的な応用例ってだけだろｗ
君こそ勉強しなおしてきたらどうだい？
183 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 05:04:11.68 ]: >>176
実数ってのがそもそも「数」ではない。実数で表されるものは「量」だ。
従って「数学」という名称は名が体を表していない。「量学」と改称すべきである。
184 名前：１３２人目の素数さん [2011/11/04(金) 06:36:50.32 ]: >>183
量と数と実数の関係をはっきり述べないと議論にならない
185 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 07:13:03.86 ]: >>184
こんな定義だそうだ：
kamome.2ch.net/test/read.cgi/math/1317089920/21
186 名前：１３２人目の素数さん [2011/11/04(金) 08:02:31.27 ]: >>185
要するに
離散量＝自然数＝真の数
連続量＝実数＝数でない
といいたいわけか。

なんか窮屈だな。
窮屈を好むのはやっぱ精神異常？
187 名前：１３２人目の素数さん [2011/11/04(金) 08:04:26.33 ]: なんでもかんでも数と呼んだらええんちゃうｗ

自然数も有理数も実数も複素数も四元数も数。
それどころかベクトル空間の元も数。だから関数も数。
ええい、もう、集合も数とよんだらええがなｗ
188 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 08:13:49.78 ]: 人数とか個数とはいうけど、水数とは言わないだろ、水量だ。
つまり日本語の「数」は、本来連続量には使われない。
連続量である実数に「数」とつけるのはテクニカルタームでだけだ。
189 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 08:14:59.70 ]: いま思ったが、数学で扱うものはみな集合だから
数学は集合論だってことだなｗ。

ということで、数学板を集合論板に改名すべしｗ
190 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 08:18:33.42 ]: >>188
もうええよ、数学も量学もせますぎ。
今の数学は全て集合論だからｗ

♪これも集合、あれも集合
　たぶん集合、きっと集合
191 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 08:23:09.84 ]: >>190
というと、圏論ヲタから
「圏の重要性を全く無視している！」
といわれそうだな。

それなら、まあ、圏論の立場も立てて
数学板を集合論・圏論板に変えるのはどうだ？ｗ
192 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 09:27:38.04 ]: >>181 ガロア理論の胆は、
集合(体)の構造を調べたい時に、
その集合上の写像の族(変換群)の
族としての構造(群構造)を調べるという所。

個々の写像が具体的にどの元をどの元に
移すかどうかは忘れて、写像の族が織り成す
性質(群としての性質)を調べるという所。
ここに既に圏論の考えがある。
193 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 09:59:33.66 ]: 上がガロア理論の本質だけど、
代数方程式に絡めて、もう少し詳しく書く。

有理数係数代数方程式に代数解があるということは、
有理数体に解を付加した体が、
有理数体に1の冪根を付加した体の
部分体になっていること。(本当は嘘だが遠くない)
だから、ある体はある体を部分体をもつか？
という問題になる。

体上の(自然な)変換群を考えると、
部分体と部分変換群との間に自然な対応がつく。
(ここがガロア理論の胆。以下は代数的な話)

有理数体に冪根を添加したという特別な体に対し、その体の変換群は、冪根の性質からある制約をうける。その制約は、部分変換群へも伝播し、対応する部分体へも伝播する。
この部分体が、有理数体に代数方程式の解を添加した体なら、その制約は、
その代数方程式へも伝播する。
五次以上の代数方程式では、この制約を外れるものが出る。
こういうシナリオです。
194 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 20:05:57.67 ]: 逆数学が二次的って言われるのは、
ある定理や理論にどの公理がどの程度本質的に効いてくるのか
ってことが分かるってのがメインで、基本的にはそれ自体から
数学のレベルで新しい定理が出てくるってわけじゃない
（メタレベルで数学がより分かるようになるだけ）って意味じゃねーの？
195 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 21:07:21.61 ]: でも、再帰的に逆数学の定理も素材になるじゃん。
196 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 21:48:52.44 ]: >>195
逆数学が逆数学自体を研究対象にしたところで、それが数学からみて
二次的な存在であることは変わらない（というかむしろ三次的存在になってしまう）
のではないの？
197 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 21:53:55.21 ]: >>194
そういうことを言いたいのであれば、最初からそう言えばいい。
例のアホは、そんな詳しいことは言ってない。
「逆数学は二次的だ」としか言ってない。だから

A：じゃあガロア理論も二次的だな。
B：何を言うか。お前はガロア理論を分かってない。

とかいうワケの分からない方向に進むのだ。Aが言っていることは

「お前の言ういい加減な "二次的" に従えば、ガロア理論だって
　二次的になってしまうぞ。それでいいのか？」

ということである。すなわち、Aの発言の本質は

「 "二次的" とは何なのか詳しく説明しろ」

ということであり、Aが問題にしているのは "二次的" の定義である。
従って、A自身はガロア理論のことを "二次的" だとは思ってない。
Aは、"二次的" という内容を皮肉っているだけである。
実際、>>151の書き方は明らかにこのような意図に読める。
よって、Bのような返答は見当違いであり、正しい返答の仕方は

「いや、二次的とはこういう意味だ。ガロア理論はこの意味で二次的では無い」

というものでなければならない。"二次的" の定義に触れない返答は意味が無く、
話がこじれるだけである。
198 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 21:57:25.73 ]: 要するに>>197は話にならんレベルのアホってことか。了解した。
199 名前：１３２人目の素数さん [2011/11/04(金) 21:59:57.78 ]: 答えられないから逃げるね

まで読んだ
200 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 22:02:01.64 ]: >>198
いくら煽っても、例のアホが何も言ってないことには変わらない。
今の段階で分かっていることは

・例のアホ本人による、「逆数学は二次的だ」の説明が未だに無い。何も言ってないのと同じ。
・別人である>>194による、「二次的だ」の見解は登場している。

ということにすぎない。
201 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 22:06:55.85 ]: まあいくら誤魔化したところで、そんなつまらないことをいつまでも愚痴愚痴ネチョネチョやってるアホが
一人居るってことはずっと変わらんということにすぎない。
202 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 22:24:51.74 ]: まあ、いくらつぶやいたところで、例のアホが何も言ってないことには変わらない。
圏論スレのころから内容が全く無い。
203 名前：１３２人目の素数さん [2011/11/04(金) 22:29:58.48 ]: ガロア理論に先行する圏論の萌芽はないの？
204 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 22:47:08.09 ]: >>197 他人に日常用語の定義定義とうるさくて、
当の本人は何も定義しないし、何も主張しない。
他人の話にケチつけてれば自分の立場が
崩れないと考えている。完全なアホ。
自分がアホ出ないことを主張してみな。
205 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 22:52:44.88 ]: アホ本人を納得させるつもりで書いてないから。
第三者(特に若者)がみてこっちに分がありそうだと
思ってくれればそれでじゅうぶん。
206 名前：１３２人目の素数さん [2011/11/04(金) 23:08:22.36 ]: >>205
君には分がないよ。
よく考えればわかるので説明はしない。
207 名前：１３２人目の素数さん mailto:sage [2011/11/04(金) 23:29:45.39 ]: あ、言っとくが、二次的という言葉で
逆数学を最初に批判したのは私じゃない。
でも充分私には言いたいことは伝わった。
私は彼に分があると思った
208 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 01:19:12.75 ]: >>194
代数的解法があるかどうかはメタレベルではなく数学の問題だと？
ある定理や理論にどの公理がどの程度本質的に効いてくるのかは二次的で
ある解を求めるのにどういう手法（代数的か超越的か）が本質的に必要かは一次的なのか？
随分と恣意的な境界線だこと。というか逆数学を二次的にするための定義だな。
「二次的とは逆数学のようであること」と言っているのと大差ない。
209 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 02:09:51.06 ]: 二次的だと狭いってのも意味不明だな
210 名前：１３２人目の素数さん [2011/11/05(土) 02:16:07.40 ]: ﾁｮｲｽしてはいけない公理をﾁｮｲｽするから球分割の矛盾が生じるのだ
211 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:16:55.47 ]: ちゅうか、「方程式を代数的に解く」ってのは数学の話で、
連続体仮説を公理に入れるか入れないかはメタ数学の話で、
重力を含む超統一理論があるかどうかってのは物理学の話で、
……etc.
って中で、数学のレベルでの話以外は数学にとっては二次的三次的なもんだろ。
どんだけ頭沸いてるんだか。
212 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:23:28.11 ]: で、その「数学のレベル」ってのはなんなんですかね。
213 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:35:16.66 ]: >>211
それって「逆数学は重要でないから重要でない」とか言っているのと同じだから。
真面目に議論する気がないなら出て行ってね。
214 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:38:54.08 ]: >>213
逆数学は逆数学で、
逆数学からすれば数学も物理も国文学も等しく二次的三次的だ
と言っているのに、君こそまじめに話する気がはじめからないんだろ？
215 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:41:12.51 ]: つか、>>214は二次的＝重要でないとか、言ってるも同然なんだが、
んなわけないだろ、ドンだけ頭悪いんだこの阿呆は
216 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 03:42:03.55 ]: おっと、滑った。

つか、>>213は二次的＝重要でないとか、言ってるも同然なんだが、
んなわけないだろ、ドンだけ頭悪いんだこの阿呆は
217 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 04:13:40.16 ]: dictionary.goo.ne.jp/leaf/jn2/166890/m0u/%E4%BA%8C%E6%AC%A1%E7%9A%84/

にじ‐てき【二次的】
［形動］主となる物事に対して、それに付随する関係にあるさま。また、ある物事から派生したもので、それほど重要でないさま。副次的。「―な災害」「―な問題」
218 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 04:18:53.04 ]: １．主となる物事に対して、それに付随する関係にあるさま。
２．また、ある物事から派生したもので、それほど重要でないさま。
３、副次的。

ってのは意味が並立なわけだが。
219 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 04:19:44.54 ]: 辞書も読めないとか、やっぱり幼稚園児並の脳みその持ち主だったｗ
220 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 04:21:54.87 ]: 逆数学は二次的　と最初に言ったのは>>135
二次的＝狭い　と最初に言ったのも>>135
二次的＝重要度が減る　と最初に言ったのは>>139

>>135にとっては、逆数学は二次的で、狭い
>>139にとっては、逆数学は二次的で、重要度が減る

二次的だとなぜ重要度が減るのか、あるいは、
二次的だとなぜ重要でないのか、そのことに答えたレスはまだない

二次的だとなぜ狭いのか、そのことに答えたレスもまだない

とりあえず、スレを見渡す限りは、二次的だと重要でないという考え方は
マイナーのようである
221 名前：１３２人目の素数さん mailto:age [2011/11/05(土) 04:24:29.24 ]: 並列なら「二次的＝重要でない」も正しい解釈の一つ。
従ってそれを「んなわけないだろ」と言っている奴こそ辞書が読めないんだな
222 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 04:26:00.30 ]: いや、>>217で答えは出ていたか

そうか、最初から重要でない意味が含まれているのか
223 名前：１３２人目の素数さん mailto:age [2011/11/05(土) 04:27:53.94 ]: ワロタ藁ｗ
224 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 05:05:00.64 ]: >>221
並立なんだから、他の意味で言っている場合を完全無視して
「二次的＝重要でない」と言ってると主張するのは、
幼稚園児にも笑われるレベルの阿呆だ。
225 名前：１３２人目の素数さん mailto:age [2011/11/05(土) 05:09:13.82 ]: 正しい解釈の一つである可能性を無視して
「んなわけないだろ」だろと全面否定した人間は
幼稚園児に笑われるレベルだろ
226 名前：１３２人目の素数さん mailto:age [2011/11/05(土) 05:14:54.56 ]: 並列に複数の意味がある言葉は、文脈によって最も適切な意味で解釈するべきであろう。
しかるに139が「二次的であれば重要度が減る。」と述べている。
更に逆数学批判派は同語反復的な主張が多数であった。
かような文脈において、二次的＝重要でない、という解釈は
139の発言をまさに同語反復とするものであり、
この文脈において最も適切な「二次的」の解釈であると考えられるのである。
227 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 05:17:26.03 ]: というか、俺も逆数学は数学にとって二次的だというレスをしているが、
全く逆数学批判派ではないぞ。そこまで興味を持っても居ないが。
228 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 05:18:16.08 ]: 重要度が減ると重要でないをイコールで結ぶのはさすがに赤ん坊以下だよ。
229 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 05:32:12.01 ]: 逆数学が副次的なものでないという主張の意味が分からん。
230 名前：１３２人目の素数さん mailto:age [2011/11/05(土) 05:47:21.72 ]: >>228
お、辞書の読み方では勝ち目がないと悟って論点のすり替え？
しかし残念だが>>226の主張は「重要度が減る」と「重要でない」の同値は必要ない。
後者から前者への implication さえあればいい。
231 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 08:01:47.04 ]: 俺は逆数学は、二次的だとは思わんな。寧ろ根本的だろう。

例えばRCA0とWKL0の違いが明らかになったのは面白い。
前者は明らかに構成的だが、後者は何らかの超越的な仮定がある。

こういうことに対して何の面白みも感じない人は
数学的感覚が鈍磨しているといっていい。
232 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 09:09:38.10 ]: >>231 それって単なる盆栽趣味。ないしはスケールが小さい。
ないしはスケールの大きな数学を知らない
233 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 10:21:18.06 ]: >>232　スケールの大きいことをやりたがる人は
数学なんかやらないｗ

微細構造を好む人がやるのが数学。
234 名前：１３２人目の素数さん [2011/11/05(土) 10:28:58.83 ]: 計算理論の壮大さを知らんようだな。
全数学を包括しかき回すほどの規模。
21世紀の主流は計算論＋理論計算機＋集合論
235 名前：１３２人目の素数さん [2011/11/05(土) 10:35:20.73 ]: >>234
別に壮大だとは思わない。
そもそも壮大だからスゲーとはおもわんし。
なにかといえば大きさを求める奴は
きっと●ん●んが小さいんだろうｗ
いっとくけど、♀の＊＊＊は鈍感だから
入れたって正確な大きさなんかわかりゃ
せんってｗ
236 名前：１３２人目の素数さん [2011/11/05(土) 12:13:54.61 ]: 逆数学が2次的ってｗ
本来逆数学のような計算論の視点が1次的で、
これまでの数学が2次的なものなのだが。
ユークリド言論が1次的で非ユークリッドが2次とか言っているようなものw
237 名前：１３２人目の素数さん [2011/11/05(土) 12:18:44.87 ]: >> 234
これ興味あるからもうすこし聞かせて。
オレは、本当にそうであればよいと思う者だが、今の計算論や理論計算機にそんな兆候があるか？
何あるいは何処がその兆候だと思うんだ？
238 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 12:23:15.54 ]: >232
無限と同じぐらいの深淵じゃないの？
可算数と非可算数の境界の話だよね？
239 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 13:58:14.73 ]: >>236
逆数学にとって数学が二次的な対象でしかないことは誰も否定して無いと思うが。
240 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 14:49:37.41 ]: >>239
逆数学は、直接、数学の成果を得る活動ではないが
その結果が、数学でないかといえば、そんなことはないから
結局、フツウの数学と変わるところはない。
241 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 17:17:43.15 ]: 逆数学の井の中の「数学」を大海の数学と称する腹か。
自分で「フツウの数学」と区別しておいてそれは詭弁ではあるまいか。
242 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 17:25:08.36 ]: >>241
要は対象の選び方の違いにすぎない。
こんなことに難癖をつける奴は●違いだろう。
243 名前：１３２人目の素数さん [2011/11/05(土) 19:00:04.00 ]: >>243
述語論理ですが、
言語Lってのは
論理的述語記号∧、∨、￢、→、∀、∃
変数記号x1、x2、x3、...
関数変数記号F1、F2、F3、...
述語変数記号R1、R2、R3、...
の記号の組合せの事ですよね。
この記号の組合せの総数、つまり2^Lの中で、
変数記号、引数に項をとる関数の形をしたものが項ですよね。
項の集まりをTermとすればTerm⊆2^Lになりますよね。
引数に項をとる述語と、述語を引数にとる論理的述語が論理式ですよね。
論理式の集まりをFlmとすればFlm⊆2^L。
244 名前：１３２人目の素数さん [2011/11/05(土) 20:50:08.36 ]: LによってTermやFlmが規定されることから、
これらをTerm(L)やFlm(L)と書き換えよう。
M(L)という対が＜M,Pri,Fnc,m,v＞と定義される。
Mは集合。
Priは定義域がMを動く述語の集合。
Fncは定義域・値域がMを動く関数の集合。
mは定義域が定数記号ならば値域がM、
定義域が述語定数記号ならば値域がPri、
定義域が関数定数記号ならば値域がFnc、
となる全単射関数。
vはFlm(L)から{0,1}への関数。

さてここまで来れば私の主張したい内容が想像つくだろう。
つまり、「論理的述語記号だけ特別扱いするのは卑怯ではないだろうか？」
245 名前：１３２人目の素数さん [2011/11/05(土) 21:23:51.57 ]: >>244
＞「論理的述語記号だけ特別扱いするのは卑怯ではないだろうか？」
上記の文章は理解できない。

もし、
「論理記号によって書かれた述語だけを
　述語として認めるのはおかしいだろう？」
といいたいのであれば、全くその通りである。

実は一階述語論理と二階述語論理の違いはそこにある。
一階述語論理では、論理式として書けるものしか拘束できない。
しかしながら、二階述語論理では、述語全体を束縛する演算子
として∀、∃を用いることができる。
246 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 21:33:28.20 ]: >>241 ははは。
基礎論って、妖怪人間ならぬ妖怪数学みたいなものか？
普通の人間や数学は、日夜、立派な人間や立派な数学になりたいと
切磋琢磨しているのに、
普通の人間か数学になりたい、それで充分だからならせてくれと。
247 名前：１３２人目の素数さん [2011/11/05(土) 22:09:00.71 ]: さて、途中まで書いていたのだが以下続き。

論理的述語記号は通常、
A　B　A∧B
------------
1　1　1
1　0　0
0　1　0
0　0　0
のような真理値が定義されているのだが、
これはいささか早計ではないだろうか。
これが前提となるのは非常に不快である。
そこで論理的述語記号を関数や述語と同様に、
論理的述語変数と論理的述語定数に分離して考えてはどうだろうか。
つまり論理的述語記号∧、∨、￢、→、∀、∃ を
論理的述語変数L1、L2、L3、...
にすげ替えてしまうのである。
同時に論理式の定義を以下のように拡張する。
・引数に項をとる述語。
・引数に引数に述語か論理的述語をとる論理的述語。
248 名前：１３２人目の素数さん mailto:sage [2011/11/05(土) 22:27:27.03 ]: >>211
同意。
逆数学や基礎論と数学は別物。
別物なんだから、価値観が違う。

基礎論にとっては、代数方程式論より逆数学のほうが重要かもしれないが、
数学にとっては、代数方程式論の方がはるかに大事。

価値観が違うんだから、はっきり分けるべき。

数学は数学。論理学は論理学。

刃物をつかっているという点では同じでも、
サムライと板前くらい違う。目的も価値観も違う。
249 名前：１３２人目の素数さん [2011/11/05(土) 22:32:31.65 ]: >>245
まったくそのとおりである、私はさらにその考えを推し進めようとしている。

注意すべきは論理的述語は引数に直接項をとることができない。
これは既存の1階述語論理と同様である。
（いや、∀と∃の存在保証が失われた今、1階というのは意味をなさない言い方か。）

さて、今述語論理の言語は以下の述語を持つ。
論理的述語変数 L0、L1、L2、...
論理的述語定数 -
非論理的述語変数 R1、R2、R3...
非論理的述語定数 -
ここで論理式の定義と比較したとき、ある事実に気が付くだろう。
論理式の非論理的述語は引数に項をとる。
論理式の論理的述語は引数に非論理的述語と論理的述語をとる。
つまり項で非論理的述語の真偽が決まり、非論理的述語で論理的述語の真偽が決定する。
250 名前：１３２人目の素数さん [2011/11/05(土) 22:54:57.82 ]: 非論理的述語を1階の述語、
論理的述語を2階の述語と考えると、
当然3階4階...n階と階層化をすすめたくなる。
重要なのは、n階の述語は引数にn階以下の述語をとるということ。
そして1階だけが極小の述語となり、引数に項しかとれない。
述語はどの階層でも真偽が決定するが、項は単独では真偽決定できない。
251 名前：１３２人目の素数さん [2011/11/05(土) 23:29:23.60 ]: さて、構造の側はどうするかというと、
{Pri_n(L)}n∊N とでもして述語を階層ごとに分けとけばよいだけだ。
さて言語Lの論理式は今や以下の定義となる。
・項を引数に持つ1階述語。
・n階以下の述語を引数に持つn階述語。ただしn≧2。

こうすると構造の側はどのように真偽を判定するのか。
なおn階の述語すべてのアリティの個数制限をなくす。
252 名前：１３２人目の素数さん [2011/11/05(土) 23:45:50.00 ]: なお真偽値をいくつにしても構わないし、
どういった場合においてもここまで一般化された
言語では任意の証明体系で完全性定理が成り立つ。
というより論理記号がないため恒真が意味をなさない。

こう考えると1階述語論理とは、
述語が2階までで、
2階の述語定数記号が各アリティ2の∧、∨、￢、→、∀、∃ である。
ここで通常の1階論理と同じような真理値を2階の述語に与えれば良い。
（勿論構造の側の解釈を与える全単射の関数mもn階分に対応している。）
また、高階述語論理や様相論理も自由に展開できることを確かめたれたい。

了
253 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 02:12:56.62 ]: 話をバッサリ切ってごめんけど、なんでこんなに難しい文章で説明しようとするの？
254 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 02:14:56.35 ]: バカだから
255 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 02:18:17.96 ]: ロボットに説明するわけじゃあるまいし。

何で数学の証明とか解説ってやたら難しい事書くんだろう。人間が人間に説明するんだから(ry
256 名前：１３２人目の素数さん [2011/11/06(日) 03:51:17.42 ]: >>255
解釈の方法を限定するためじゃね。
自然言語で意味が一意になるように書くと、更に長くなるよ。

試しに選択公理を論理式と自然言語で書いて見比べてみたら。
257 名前：１３２人目の素数さん [2011/11/06(日) 07:15:28.38 ]: 難しいと言うか
普通の教科書の書き方をパロッてるんだろう
258 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 08:11:19.75 ]: >>248
何がいいたいのか意味不明。

そもそも代数方程式でも解の存在が大事だという人と
解の性質が大事だという人がいるだろう。

数学の中で分野わけすればいいだけのこと。
整数論至上主義者は、整数論のために
関数解析を「数学ではない」といって
切るつもりか？
259 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 08:18:45.68 ]: >>249-252
ゲーデルのLを知らんのか？
あれはまさに無限階論理といってもいいわけだが。

しかし、全ての階をいっしょくたにできるような
最上階というものは存在しない。
260 名前：１３２人目の素数さん [2011/11/06(日) 08:53:31.44 ]: さて、いよいよ本論に入ろう。

前回、真偽の決定可能な論理式は1階以上の述語とした。
一方でn階の述語はそれ以下の階層の述語を引数にとるとした。
ここで項も論理式に加えてしまうのが合理的だと思わないだろうか。
また2階以上の階層の真偽が同様に決定するのも不自然だ。
はじめてに論理式の定義を以下のように書き換える。
・従来の変数は0階の論理式である。
・従来の関数は1階の論理式である。
・従来の述語は2階の論理式である。
・従来の論理的述語は3階の論理式である。
さらに
・n階の論理式はそれ以下の論理式を引数に持つ。

ここで問題が発生する。f(x)∧y、a＜(b＜c) のようなものが発生する。
これは容易に解決する。
261 名前：１３２人目の素数さん [2011/11/06(日) 09:41:26.91 ]: >>259
ある段階で導入する可能性もある。

かつて関数vは論理式と真理値を関連付けていた。
これは解釈という考え方で一般化することが可能である。
例えば、従来のx＜y∧y＜zという論理式を考える。
x＜y∧y＜zの真理値は、x＜yとy＜zの真理値によって決定する。
ここでx＜y∧y＜zの真理値とx＜yとy＜zの真理値は実は違うものだと考える。
そして真理値というよりは、例えば集合{t0,t1}を値が動くと考える。
一方f(x)やg(y)は構造の領域Mを動いている。
3階以上の述語も同様にふるまう。
ここで各階の論理式は解釈により集合へ対応付けられる。
各階の論理式に対応する集合は、M0、M1、M2、...とでも定義しておけばよい。
例えばPAの標準モデルは、
M0＝N、M1＝N、M2＝{0,1}、M3＝{0,1}となるだろう。

ここで先ほどのf(x)∧y、a＜(b＜c)。
f(x)∧yだが、f(x)はM1、yはM0に対応付けられる。
∧は{t0,t1}に対応付けられている。
ここで∧を解釈する関数の定義域が{t0,t1}だけならば、
それ以外の不正な値を定義不能としてはじくことが出来る。
つまり、f(x)∧y、a＜(b＜c)などは決定不能になる。
もちろんM0＝M1＝M2＝...と定義することで
意図的に関数値や定義域を混同させることも可能だ。
つまり完全性定理での論理式が、決定可能な論理式に制限されるだけだ。
262 名前：１３２人目の素数さん [2011/11/06(日) 09:55:54.14 ]: ところで真理が真偽2択から解放された今、
モデルの定義も変えねばなるまい。
矛盾許容論理などを考えればモデルとは、
ある言語のすべての論理式を定義可能な領域を持つ構造。
これにより先ほどの完全性定理は再び従来通りの論理式に対するものとなる。
263 名前：１３２人目の素数さん [2011/11/06(日) 10:06:41.41 ]: >>260、261
お前アホか。全部既知のことを今頃お勉強が終わったということ。
それからn階なんて言っている時点で古過ぎ。循環だってあるんだから。
264 名前：１３２人目の素数さん [2011/11/06(日) 10:34:01.28 ]: >>263
ご立腹かね？ワトソンくん！
265 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 16:26:20.00 ]: 流れをぶった切って。
物理なんかの測定から理論を抽出するところに逆数学的なものを感じるんだけど、
逆数学にそういった応用例とかないのかしらん？
266 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 16:43:51.03 ]: >>243-244　>>247　>>249-252　>>260-261

トンデモ？
267 名前：１３２人目の素数さん [2011/11/06(日) 17:16:49.63 ]: >>266
すでに知られていることを独自の発想のように書いてるスレ潰し
268 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 17:19:39.30 ]: >>267
既知？全く荒唐無稽の既知外だろｗ
269 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 17:32:12.02 ]: >>258 わかってないなぁ。
数学はひとつなの。

関数解析にとっても代数方程式は重要なの。
整数論と関数解析は分けることができないの。
向かう方向はおなじだから。

だが、逆数学はわけることができる。
価値観が違うんだから、どうどうと違う学問だと
なのって、数学の外で一国をつくればよい。

関数解析と整数論が違う学問だと思うのは、
きっと、現在の教育を途中で投げ出すと、
そういう感覚を覚えるようになってしまっているのが
原因。
270 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 17:43:37.04 ]: ロジックだって、完全性定理のレベルでさえ、
束、位相、代数が基盤だろ。
271 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 17:48:05.83 ]: >>270 いや、高校数学で充分足りる
272 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 18:02:19.72 ]: ロジックって、一体何を目的にして何に向かって
研究してるの？
273 名前：１３２人目の素数さん [2011/11/06(日) 18:20:57.12 ]: 証明論とかって計算機畑の方が主流？
ここ最近の研究事情がどうなってるのかわからん。
274 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 18:23:49.45 ]: >>269
＞数学の外で一国をつくればよい。

ずいぶん壮大なことをのたまっているようだが、今の体制で
本当にそのようなことを実現するなら、政治的な力が必要だな。
内部から変化することはありえないから。

こんなところで愚痴ってないで、お前が先頭に立って
排斥運動の1つでもやってみたらどうだねｗ
275 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 18:28:10.07 ]: ロジックというのは、ロジックに関係しているというだけの
雑学の総称？
276 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 18:48:03.53 ]: 「AはAに関係してるものの総称」
277 名前：１３２人目の素数さん [2011/11/06(日) 19:35:09.95 ]: >>276
アニメやゲームはそういう感じで使われているね
278 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 21:24:26.00 ]: >>271
基礎的な定理には初等的な証明、理解の仕方があるのは、
代数だって変わらんでしょ。けどそれじゃ数学的構造理解しているとは言えない。
279 名前：１３２人目の素数さん [2011/11/06(日) 21:38:02.64 ]: >>243-244　>>247　>>249-252　>>260-261
あなたのスタイルがちょっと古かったりおおげさだったりするのが皆の癇にさわって
いるだけかも。既知かも知れんが、学生だとすればなかなか力ある。
しつこくがんばれば将来性あるよ。めげるな。
280 名前：１３２人目の素数さん mailto:sage [2011/11/06(日) 22:05:42.78 ]: 基礎論による理論の構造分析を、通常数学の学習や理論の創造に役立てたい。
オススメの基礎論学習コースある？
学習者は代数専攻の数学修士として。
281 名前：１３２人目の素数さん [2011/11/07(月) 05:44:38.12 ]: >>279
人を駄目にする褒め方をしてはいけない
282 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 05:50:42.76 ]: むしろボロクソにけなしまくる方が駄目にするんじゃねえの？？
283 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 07:16:52.39 ]: >>279
全然見当違い。
そもそも論理式の値が真偽値でないとする発想が既知外。
てゆーか自画自賛だろ。トンデモがよくやる手だｗ
284 名前：１３２人目の素数さん [2011/11/07(月) 07:52:43.55 ]: ファジー論理
285 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 08:00:25.69 ]: 過去にもいたよね、方程式の解が実数でないものを認めようとしたり
小さい数から大きな数を減じてみようとしたり。
286 名前：１３２人目の素数さん [2011/11/07(月) 10:17:53.15 ]: >>285
それを今やって大発見だと思う人がいたら可哀相な人だよね。
287 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 10:28:23.70 ]: >>272 とか、
>>280 とか、
真面目な質問に答える能力のある人はいないの？
288 名前：１３２人目の素数さん [2011/11/07(月) 11:13:58.64 ]: じゃあ俺が、
といっても俺も素人なんであんまり真に受けないでね。

さしあたり完全性定理とか不完全性定理を知りたいなら、
朝倉現代基礎数学 15 数理論理学鹿島亮著
を読んで、証明とか説明に不足を感じたら
J.R.Shoenfied著のMathematical Logic
を読めばいいと思う。

モデル理論の代数幾何への応用とかは知らないんで。
289 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 11:50:14.30 ]: 完全性定理、不完全性定理は、エンダートンで
勉強しました。その次にくるのは何がよいでしょうか？
290 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 17:31:06.56 ]: >>289
エンダートンを読了したのならば数理論理学に関して一通りの基礎は身に付いたはずなので
次は自分が特に興味のあるテーマのモノグラフやサーベイに進むのが良いでしょう。
291 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 18:52:20.60 ]: 代数方面の人なら幾何的モデル理論とかが良いんじゃないかな
別にモデル論の知識は無くても読めるように書いてあるよ

基礎論全般の勉強なら新井敏康の数学基礎論が良いよ
包括的な入門書の中では一番レベルが高いんじゃないかな
292 名前：１３２人目の素数さん [2011/11/07(月) 20:37:37.55 ]: Endertonたけぇｗ
仕方ないからこれにしよう・・・
Lectures in Logic and Set Theory: Volume 1, Mathematical Logic (Cambridge Studies in Advanced Mathematics) [ペーパーバック]
George Tourlakis (著)
293 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 20:49:01.48 ]: >>291
へえ、モデル理論仕込まなくても読めるんですか。
アリ。
294 名前：１３２人目の素数さん [2011/11/07(月) 21:15:27.88 ]: モデル理論の代数幾何への応用なら
江田の数理論理学、これは絶対おススメ。
295 名前：１３２人目の素数さん [2011/11/07(月) 22:10:14.58 ]: 証明論で良い本ある？
296 名前：１３２人目の素数さん [2011/11/07(月) 22:48:43.42 ]: Umm
APPLIED LOGIC SERIESとかCambridge University Pressのコンピュータサイエンスの
論理シリーズは良書が多いねぇ
297 名前：１３２人目の素数さん mailto:sage [2011/11/07(月) 23:32:17.19 ]: >>294
生協で見たことあるが、そんな特徴ある本なの？
読んでみないと分からんもんだね。
298 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 17:18:48.13 ]: ウィトゲンシュタインの論考ってどうなの？
基礎論的には。
299 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 18:05:45.72 ]: 数学としての基礎論にとっては無価値だろ。
300 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 18:10:42.83 ]: 数学として基礎論は無価値だろ。
301 名前：１３２人目の素数さん [2011/11/08(火) 18:54:12.25 ]: ウィトゲンシュタインの像とかいう概念を
直観主義で再現するみたいなパワポ見たことあるよ
302 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 20:17:17.36 ]: 論理学なんかやって何の意味があるんだ？
303 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 21:46:59.04 ]: もちろん数学の基礎付けですよ！
304 名前：１３２人目の素数さん [2011/11/08(火) 21:53:03.38 ]: 論理学は木の研究
目標は新たな計算機の創造
うひ
305 名前：１３２人目の素数さん mailto:age [2011/11/08(火) 22:39:11.92 ]: 論理学なんかで数学の基礎付けができるのか？
306 名前：１３２人目の素数さん mailto:sage [2011/11/08(火) 22:49:07.15 ]: 量化の代入的解釈(substitutional quantification )って何ですか？ぐぐってもよくわからなかったのですが。。。
307 名前：１３２人目の素数さん [2011/11/08(火) 23:36:34.25 ]: 例えば述語論理で言語の定数が0,1,2のとき、
「∀xP(x)が真」を、「P(0)が真＆P(1)が真＆P(2)が真」
と置き換えて解釈をする流儀。
モデルの側の領域と無関係と考えるような意味論。
ただ強完全性とコンパクト定理が成り立たない。
308 名前：１３２人目の素数さん mailto:sage [2011/11/09(水) 00:09:01.98 ]: >>307
なるほど。解説ありがとうございます。

>モデルの側の領域と無関係と考えるような意味論。

領域と無関係というのは、領域自体考えに入れないということですか？
たとえば、普通ならP(0)が真 iff V(0)∈V(P)と考えると思うのですが、上の意味論ではP(0)の真理値はどうやって決まるのでしょうか？
309 名前：１３２人目の素数さん [2011/11/09(水) 08:14:34.34 ]: 例えば
P(x)のモデルMでの解釈が{2,3}で、
言語の定数記号がa,b、
そのMでの解釈がそれぞれ2と3だとする。
このとき代入したもの
P(a/x)とP(b/x)を解釈すると両方真。
つまり∀xP(x)が真。
ところがモデルMの領域全体がどうなっているかは不明！
310 名前：１３２人目の素数さん mailto:sage [2011/11/09(水) 13:40:46.76 ]: >>309
そういうことでしたか、よく分かりました。
311 名前：１３２人目の素数さん [2011/11/10(木) 15:23:53.16 ]: 論理学なんかで数学の基礎付けができるのか？
312 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 15:25:57.13 ]: それは未来人に訊いてください
313 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 16:50:53.13 ]: ロジック抜きでどうやって数学を構築するのかと…
314 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 18:28:52.13 ]: トポスとか圏論とか
315 名前：１３２人目の素数さん [2011/11/10(木) 18:47:35.69 ]: >>314
そりゃ集合論抜きでロジック構築する方法だろ＾＾；
316 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 19:42:13.85 ]: 数学の基礎付けがどうとかいうのは
今時（ロジックの中でも）時代遅れで、
研究者はほとんどそんなこと気にしちゃいない
317 名前：１３２人目の素数さん [2011/11/10(木) 19:55:31.55 ]: きさまら同じ話題を難解ループしてんだよｗ
318 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 20:20:19.96 ]: お前もいつまでこのスレ読んでるつもりだ？
319 名前：１３２人目の素数さん [2011/11/10(木) 20:33:33.69 ]: 命ある限り読むつもりだよｗ
その5辺りから読んでるんだから
320 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 20:34:33.65 ]: その１からのログを保持してる俺はそろそろ飽きてきた
321 名前：１３２人目の素数さん [2011/11/10(木) 20:39:10.71 ]: なぜなにスレッドの
洗濯小売はどうなったのか？
322 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 22:44:01.56 ]: >>316 では、今のロジシャンは何をやりたいの？
323 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 22:47:13.21 ]: ただのパズラー？
324 名前：１３２人目の素数さん [2011/11/10(木) 22:58:40.05 ]: 従来の論理学は
コンピュータサイエンスに移ったよ。
洋書のCSシリーズのが充実している。
325 名前：１３２人目の素数さん mailto:sage [2011/11/10(木) 22:59:07.72 ]: パズラーに失礼の無いように
326 名前：１３２人目の素数さん mailto:sage [2011/11/11(金) 09:49:01.53 ]: 第二不完全性定理の証明がわかりません。具体的には、
PA|- Pr(【φ】)→Pr(Pr(【φ】))
をどうやって証明するのかがわかりません。
不完全性定理ってなかなか難しいですね。
327 名前：１３２人目の素数さん [2011/11/11(金) 19:49:22.09 ]: 補題
Σ1文φについてPA|-φ→Pr(【φ】)
328 名前：１３２人目の素数さん mailto:sage [2011/11/11(金) 21:57:15.05 ]: >>327
定義に関する帰納法で証明すればいいんですかね？
φが原子論理式のとき
φが�Ψのとき
φが、、、、

んーいまいちまだ分からないんですが。
329 名前：１３２人目の素数さん mailto:sage [2011/11/11(金) 22:14:05.71 ]: たとえば
PA|- ∀x∀y(x=y→Pr(【x=y】))
はどうやって証明するんでしょうか？
330 名前：１３２人目の素数さん [2011/11/11(金) 22:56:20.05 ]: >>329
PAの定義や証明体系に依存する。
331 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 01:49:07.93 ]: >>330
たしかにそうですね、、、定義も書かずすみませんでした。

ところで、第二不完全性定理を証明する際に使われる導出性条件(derivability conditions)というのが３つありますよね。

D1 PA|- φ→Pr(【φ】)
D2 略
D3 PA|- Pr(【φ】)→ Pr(【 Pr(【φ】) 】)

このうちのD1とD3は何が異なるのでしょうか？ Pr(【ψ】)をD1のφとして考えれば、 D3はD1に含まれる気がするのですが。
332 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 03:39:12.71 ]: D1が間違っているように見えるが、君の参考にしている本には本当にそう書いてあるかい？
333 名前：１３２人目の素数さん [2011/11/12(土) 06:54:09.56 ]: >>331
D1はPA|-φならばPA|-Pr(【φ】) だと思いますよ。
334 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 09:05:16.20 ]: D1が間違っていました、失礼しました。
335 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 09:38:08.20 ]: 次の論理法則を証明せよ：－

「前提が偽であることは帰結も偽であることを何ら保証するものではない。」
336 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 12:01:57.63 ]: やばい数学オリンピック辞典見てみたけどさっぱり内容がわからない・・
337 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 12:37:56.98 ]: １ |-A←→B
２ |-A ⇔ |-B
1と2って同値でしょうか？
338 名前：１３２人目の素数さん [2011/11/12(土) 13:28:48.48 ]: １から２を示す。
|-A←→B
|-A→B∧B→A
|-A→B------(1)
|-B→A------(2)
もし|-Aなら(1)とMPで|-B、|-A⇒|-B
もし|-Bなら(2)とMPで|-A、|-B⇒|-A
よって |-A ⇔ |-B。
逆に２から１は一般に出ない。
339 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 16:46:34.16 ]: >>338
助かりました、ありがとうございます。
340 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 17:06:01.89 ]: >>269
＞関数解析にとっても代数方程式は重要なの。
＞整数論と関数解析は分けることができないの。

この屁理屈だと、数学と物理学も分けることができない、となる。
物理学にとっても、数学は重要であるからだｗ
もちろん、他の学問でも同じことだが。

＞向かう方向はおなじだから。

具体的に、どこだいｗｗｗｗｗｗｗ
341 名前：１３２人目の素数さん [2011/11/12(土) 21:19:30.75 ]: >>340
どこが屁理屈なのかわからない
342 名前：１３２人目の素数さん [2011/11/12(土) 21:22:49.41 ]: >>341
つまり、数学と物理学は分けることができない、と
343 名前：１３２人目の素数さん [2011/11/12(土) 22:55:45.50 ]: 猫は？
344 名前：１３２人目の素数さん mailto:sage [2011/11/12(土) 22:58:56.97 ]: なにかと忙しいらしい

54: 11/09(水)21:06 AAS
猫がカンボジア国籍取得。五輪に前進。

57: 11/12(土)09:51 AAS
猫五輪確定？カンボジア3選手が選考レース辞退

来年のロンドン五輪男子マラソンを目指し、カンボジア国籍を取得した猫が出場する五輪選考レース「東南アジア競技大会」(16日、ｲﾝﾄﾞﾈｼｱ)を出走予定の同国代表3選手が辞退｡同レースに出走する同国選手は猫のみになった｡
345 名前：１３２人目の素数さん [2011/11/13(日) 05:08:28.07 ]: >>342
数理物理学抜きの数学は考えられないな
346 名前：１３２人目の素数さん [2011/11/13(日) 10:25:14.55 ]: >>345
数理論理学抜きの数学も考えられんよ
347 名前：345 [2011/11/13(日) 11:21:31.05 ]: >>346
全く同意する。
数理論理学は数学の重要な分野だと思う。
348 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 11:54:52.99 ]: ベン図さえあれば論理学いらん
349 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 12:00:45.38 ]: 全く同意する。
アダルトビデオは映像芸術の欠くべからざるジャンルだ。
350 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 12:06:48.71 ]: >>342 数学と物理の一部は分けられない。
でも、数学と論理学は分けられる。
数学と物理を僧侶と牧師に例えるなら
基礎論はただの禿げてる人。
見かけは僧侶に近いが考えていることは違う
僧侶と牧師は見かけは違うしスタイルも違うが
考えている方向性は同じ
351 名前：官軍（一兵卒）(＾o＾) mailto:sage [2011/11/13(日) 12:42:52.49 ]: (Ｐ⊃Ｑ)⊃(￢Ｑ⊃￢Ｐ) は tautology であり。

“(ＰならばＱである)ならば、(ＱでないならばＰではない)”が成立する。

しかし、[Ｐ⊃(ＱＶＲ)]⊃[(Ｐ⊃Ｑ)Ｖ(Ｐ⊃Ｒ)] は tautology であるのに

“ＰならばＱかＲであるならば、ＰならばＱかまたはＰならばＲである”は

成立しない。
352 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 12:44:46.23 ]: ことがらＡ，Ｂ，Ｃ，Ｄが在り、これらについて次の２つの関係が成り立って
いるものとする。

　　(ｲ) Ａであれば、Ｂか又はＣである。

　　(ﾛ) Ｄであれば、ＢでもＣでもない。

このとき、以下の主張 (1) ～ (8) のうち正しいものを列挙せよ。尚、解法も述べよ。

　　(1) Ｄでなければ、Ａではない。

(2) Ｃであれば、Ｄではない。

(3) Ａでなければ、Ｄでないか又はＢではない。

(4) Ａでなければ、Ｄではない。

(5) Ｂでなければ、Ａでないか又はＤである。

(6) Ｂでなければ、Ａでないか又はＣである。

(7) Ｂであれば、Ｃではなく、Ｄでもない。　

(8) ［Ｂでなければ、Ｄではない］か又は［Ｄでなければ、Ｂではない］
353 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 14:58:00.91 ]: 結局、導出性条件(derivability conditions)の証明がわからず、第二不完全性定理もしっかり理解できなかった。
354 名前：１３２人目の素数さん [2011/11/13(日) 15:32:57.93 ]: >>350
＞数学と物理の一部は分けられない。

一部とは具体的に何を指すか？

もし「理論物理学」を指すならあなたが間違っている。

理論物理学は、物理であって数学ではない。
なぜなら理論物理学も物理現象を扱うからである。
理論物理学は数学のように証明によって
その真偽が決まるわけではない。
355 名前：１３２人目の素数さん [2011/11/13(日) 15:37:15.51 ]: >>350
＞でも、数学と論理学は分けられる。

物理において数学が使われているように
数学において論理が使われているだけだ
というのであれば、もちろん分けられる。

し・か・し、論理の数学的研究は、道具の使い方の研究ではない。
論理そのものの数学的構造を調べることにある。
したがって、数学の証明には全く役に立たないことは多々ある。

証明に役立たない論理の研究は無意味だというのは
物理に役立たない数学の研究は無意味だというのと
同程度に見識が狭い。
356 名前：１３２人目の素数さん [2011/11/13(日) 15:43:41.36 ]: >>350
>（数学と物理は）
>見かけは違うしスタイルも違うが
>考えている方向性は同じ

と思ってるなら数学も物理も分かってない。

数学では、ユークリッド幾何も非ユークリッド幾何も意味がある。
しかし物理学では、ニュートン力学と相対論の両方が意味がある、
ということはない。意味があるのは物理現象と整合する理論だけだ。

ちなみに、ニュートン力学の速度の合成はユークリッド的
相対論の速度の合成はクラインの円盤の変換として
実現できるので非ユークリッド的である。
357 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 15:53:35.40 ]: >>356
物理学でも、
ニュートン力学と相対論は、両方意味があるよ。
状況に応じて使い分けられている。
358 名前：１３２人目の素数さん [2011/11/13(日) 15:56:21.05 ]: >>350
>（基礎論は見かけは数学に近いが)考えていることは違う

まず基礎論という言葉は論理学を指すものではないから
論理学という意味で言っているのならば、明確に間違っている。

さて、>>356で、「物理的世界」のように
「数学的世界」があるわけではないことを
ユークリッド幾何と非ユークリッド幾何の
例で示した。

数理論理学の研究から、多種多様な数学の存在が示される。
もし、数学と物理は「唯一無二の世界」を探求する点で似ており、
論理学は「多種多様な可能世界」を想定する点で異なるというなら
その人は、数学を誤解している。数学は「多種多様」なのであって
数理論理学はその事実を示しているに過ぎない。
359 名前：１３２人目の素数さん [2011/11/13(日) 15:58:14.42 ]: >>357
ニュートン力学は単に「方便」として用いられているにすぎない。
非ユークリッド幾何もごく小さい箇所では、ユークリッド的であると
みなせるのと同様な意味で、だ。

しかし、そのことは、ニュートン力学が
物理的に「正しい」ことを意味しない。
360 名前：１３２人目の素数さん [2011/11/13(日) 16:05:43.86 ]: >>359
物理に正しいも間違いもないよ。
全てはモデルなんだから。
真実があるとしたら、それは神のみが知りうる。
それが物理学のとる立場だ。

大学生になったら、そういうことを意識してくださいね！
361 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 16:35:17.23 ]: >>359
ニュートン力学は、正しいよ。
通常の状態では、相対論と一致するとてもよい近似理論。
精度の高さと計算効率の良さから、今でも使われている。
というより、ほとんどニュートン力学だよ。
相対論が必要になるのは、かなり特殊な状況だ。
362 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 16:52:36.52 ]: >>361
GPSで使うぞい
363 名前：猫 ◆MuKUnGPXAY mailto:age [2011/11/13(日) 18:28:46.96 ]: 通常の場合、（どんな）物理理論にも適応限界が存在すると考えるのが
自然ですね。ソレは取りも直さず物理理論の正当性は（数学的な厳密性
ではなくて）実験結果との整合性に依って担保されるからであり、また
実験から得られる数値データには必ず誤差が含まれるという事実にも注
意が必要ですね。でも数学に於ける主張には如何なる適応限界も存在し
ません。ソレは『その命題が成立する条件が全て明確にされてる』から
ですね。

猫
364 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 18:33:16.64 ]: >>361
相対論は電磁気学の一部だろ。電磁気学は認めない立場とかそういう特殊な方？
365 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 18:34:41.32 ]: 特殊相対性理論の方な
366 名前：１３２人目の素数さん [2011/11/13(日) 18:36:26.66 ]: >>353
まずはΣ1完全性定理を
ゲーデル数で算術化するところから考えよう。
367 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 18:46:39.06 ]: >>364
電磁気学は、相対論の前に出来ていると思いますよ？
相対論なしでも電磁気学はなりたつと思います。
もちろん相対論とも矛盾しないですが。
368 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 19:11:30.37 ]: 数学わからない人は、マクスウェルの方程式と
特殊相対性理論の関係もわからないんですねえ。
369 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 20:09:28.34 ]: 例えば磁場は相対論効果によるものだし、特殊相対論の原題は
「動いている物体の電気力学」で、電磁気学のうち取り扱いがいい加減だった
相対運動をする場合の理論なんだよ。
実は伸び縮みするとか結構どうでもいい話。
ウケがいいからクローズアップされるだけで。
370 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 21:38:20.80 ]: 前の話を蒸し返すけど、物理なんかの測定から理論を抽出するところは逆数学じゃないの？
逆数学にそういった応用例とかないのかしらん？
371 名前：１３２人目の素数さん [2011/11/13(日) 21:57:42.68 ]: そもそも逆数学じゃないそれ。
そーゆーのは「抽象」っていう。
372 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 22:01:47.42 ]: ガウス？
373 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 22:07:48.80 ]: 逆数学とやらは知らんが、そんなガチガチにやっても絶対流行らん。
374 名前：１３２人目の素数さん [2011/11/13(日) 22:12:27.72 ]: ここでまともに逆数学なんて語られていないから
参考にしないほうが良いよ。
375 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 22:35:30.31 ]: >>366
形式化されていない∑1完全性定理なら証明できました。が、形式化されたそれを証明する方法がよくわかりません。

ところで、私は前原先生の本をベースに勉強しています。
以下のページでは、前原先生の証明を土台にして第二不完全性定理を証明しているみたいなんですが、これって正しいですか？

miuse.mie-u.ac.jp/bitstream/10076/6295/1/AN100450900050008.PDF
376 名前：１３２人目の素数さん mailto:sage [2011/11/13(日) 22:38:53.70 ]: >>375の追記

とくに定理12以降の部分についてです。これなら私にも理解できそうなんですが、
他の文献と比べて記述があっさりしている気がして本当に正しいのか不安に思ってしまいました。
377 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 00:39:36.38 ]: 第二不完全性条件に関して質問をしている者です。
自分なりに考えてみたのですが、以下の証明って正しいでしょうか。

表現定理より、再帰的述語ならばPAで数値別に表現可能である。
r is recursive ⇒ PA|-R
また、
PA|-R ⇒ PA|-Pr(【R】)
は証明できる。
したがって、
r is recursive ⇒ PA|-Pr(【R】)
また、証明できる論理式に対して仮定を増やしても、その論理式は証明できるので、
PA|-R→Pr(【R】)
は証明できる。
ゆえに、
r is recursive ⇒ PA|-R→Pr(【R】)
378 名前：１３２人目の素数さん [2011/11/14(月) 01:18:05.53 ]: >>377
間違えがある。
rが再帰的、つまり表現可能とは、
r⇒PA|-R
￢r⇒PA|-￢R
の2つが満たされること。
rが再帰的⇒PA|-Rにならない。
そしてそのPDFは証明の誤りや脱字や
定義の足らない部分が多数含まれている、
読まないほうが良い。
379 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 05:08:59.80 ]: ことがらＡ，Ｂ，Ｃ，Ｄが在り、これらについて次の２つの関係が成り立って
いるものとする。

　　(ｲ) Ａであれば、Ｂか又はＣである。

　　(ﾛ) Ｄであれば、ＢでもＣでもない。

このとき、以下の主張 (1) ～ (8) のうち正しいものを列挙せよ。尚、解法も述べよ。

(1) Ｄでなければ、Ａではない。

(2) Ｃであれば、Ｄではない。

(3) Ａでなければ、Ｄでないか又はＢではない。

(4) Ａでなければ、Ｄではない。

(5) Ｂでなければ、Ａでないか又はＤである。

(6) Ｂでなければ、Ａでないか又はＣである。

(7) Ｂであれば、Ｃではなく、Ｄでもない。　

(8) ［Ｂでなければ、Ｄではない］か又は［Ｄでなければ、Ｂではない］
380 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 05:10:34.13 ]: 論理法則とはそも何ぞや？
381 名前：１３２人目の素数さん [2011/11/14(月) 08:52:14.54 ]: >>380
そういうのは数理論理学ではなくて論理学がやることだね
382 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 09:15:32.61 ]: >>384
数理論理学（＝記号論理学）と論理学とはどう違うのさ？　ヽ(^。^)ノ
383 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 10:16:00.81 ]: 記号を使うかどうか
384 名前：１３２人目の素数さん [2011/11/14(月) 10:21:26.09 ]: 「記号論理学」には「(アリストテレス流の)伝統的論理学」は含まれない。
385 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 14:53:23.90 ]: >>380 ：１３２人目の素数さん：2011/11/14(月) 05:10:34.13
　　＞
＞論理法則とはそも何ぞや？

　　　論理法則＝トートロジー
386 名前：１３２人目の素数さん [2011/11/14(月) 18:44:59.32 ]: ゲーデルオリの証明で不完全性定理アプローチしとんか
モデル論使えば一発なんやけどな
387 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 19:42:18.19 ]: ゲー・デルオリって誰
388 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 19:43:51.28 ]: ゲロ出る俺
389 名前：１３２人目の素数さん [2011/11/14(月) 20:28:44.06 ]: ゲーデルオリジナルの略にきまっちょるがな
390 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 21:55:34.44 ]: 超素人なんだけど、ゲーデルの不完全性定理と対角線論法の関係を教えてくれ
何と何が対応しているんだ？
対角線論法じたいは、数学ガールで分かった。しかし不完全性定理はあの本でもイミフだった。
391 名前：１３２人目の素数さん [2011/11/14(月) 22:14:05.98 ]: 第1不完全性定理はPAの中の論理式で、
￢を付けても付けなくても証明不可能なものが存在すると主張する定理。
この論理式はゲーデル文と言われ、対角線論法はゲーデル文をつくる際に必要。
対角化定理(不動点定理)自体は数学のあらゆる場所に登場する。
チューリング機械の停止判定問題が否定的に解ける件などもこれが原因。
392 名前：１３２人目の素数さん mailto:sage [2011/11/14(月) 23:01:20.98 ]: >>389
ヴェルタース・オリジナルみたいなもん？
393 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 00:22:52.63 ]: >390
「不完全性定理と対角線論法の関係」という話だと、もうちょっと突っ込んだ考えが必要。
Webだとこれが良くまとまっていると思う。
(pdf)自己言及の論理と計算
ttp://www.kurims.kyoto-u.ac.jp/~hassei/selfref2006.pdf
394 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 01:46:48.53 ]: >>378

>間違えがある。
>rが再帰的、つまり表現可能とは、
>r⇒PA|-R
>￢r⇒PA|-￢R
>の2つが満たされること。
>rが再帰的⇒PA|-Rにならない。

仰る通りです。私が間違ってました。

>そしてそのPDFは証明の誤りや脱字や
>定義の足らない部分が多数含まれている、
>読まないほうが良い。

たしかに、題からしてすごい間違いを犯してますね。
ただ、私の気になる第二不完全性定理の箇所に関しては、私には誤りが見つかりませんでした。そして、非常に分かりやすい証明でした。
具体的にどこが誤っているか教えていただけませんか？
よろしくお願いします。
395 名前：１３２人目の素数さん [2011/11/15(火) 07:24:03.09 ]: >>392
知りません///
>>393
良くかけてるとおもう
>>394
誤りがあるか否かが問題ではない
誤りがると信じるか否かが問題である
396 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 14:45:36.71 ]: 言及されてる論文も貼っとく。
www.springerlink.com/content/h881p406u0378850/fulltext.pdf
397 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 21:28:16.27 ]: >>390
www.age.ne.jp/x/eurms/GDL.html#00
398 名前：１３２人目の素数さん [2011/11/15(火) 22:03:40.15 ]: >>338
>逆に２から１は一般に出ない。
具体的な反例は？
399 名前：394 mailto:sage [2011/11/15(火) 22:57:44.24 ]: >>395
そうですか、残念です。

もう少し考えてみます。
400 名前：１３２人目の素数さん [2011/11/15(火) 22:58:52.36 ]: 演繹定理から逆も成り立つ＾＾；
401 名前：１３２人目の素数さん [2011/11/15(火) 23:01:53.16 ]: >>363
数学についてはもちろんおっしゃるとおりですが，物理理論にとって実験結果
との整合は実は単なる結果であって，その理論の単純さや美しさこそが正当性
の根拠なのではないでしょうか（たとえば特殊相対論）．
そろそろ２１世紀の科学哲学が必要なのでは？
402 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 23:07:07.64 ]: 実験との整合性は物理理論の目的
特殊相対性理論では、マイケルソン・モーリーの実験の意味を考えるのが、
アインシュタインの研究の動機。
403 名前：１３２人目の素数さん [2011/11/15(火) 23:17:36.97 ]: >>402
知ってのとおり天動説だって観測との整合性はあった．
アインシュタインはマイケルソンモーリーの実験を知らなかったという
説もある（それは十分あり得ることだろう）．
このあたりはこの板のみなさんにはいうまでもないだろうが．
404 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 23:21:18.86 ]: 俺が彼氏にフェラチオしてるときはもっと激しくジュパジュパ音を出してあげてるよ
405 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 23:22:45.71 ]: 理論が美しい、とか誰が判定するんだ？
406 名前：１３２人目の素数さん [2011/11/15(火) 23:27:08.83 ]: >>405
単純さなら，相当程度客観的に評価できるんでないかい．
407 名前：１３２人目の素数さん [2011/11/15(火) 23:37:59.91 ]: >>399
本当に間違っているか不明。
余り信じないほうが良い。
ゲーデルの証明は複雑で、粗探しは大変そう。
そのPDF書いた人もself-containedじゃないと
ことわりを入れてるのでなおさら難しい...。

不完全性定理は有限の立場、つまり2項述語∊を使ってよいなら、
集合論を経由してかなりシンプルに証明できる。
408 名前：１３２人目の素数さん [2011/11/15(火) 23:38:50.87 ]: 訂正：
不完全性定理は有限の立場、
↓
不完全性定理は有限の立場を出て、
409 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 23:43:22.09 ]: >>400
演繹定理って、
Γ,A|-B ⇒ Γ|-A→B
のことだよね？

Γ|-A ⇒ Γ|-B
とは、違うのでは？
410 名前：１３２人目の素数さん [2011/11/15(火) 23:54:38.09 ]: >>409
|-A⇔|-B を仮定。
|-A⇒|-B について考えると、
|-A より {B}|-A
演繹定理を使って
|-B→A-------(1)
逆に|-B⇒|-A について考えると、
|-A→B-------(2)
(1),(2)から |-A←→B　　　　　　　　　　□
411 名前：１３２人目の素数さん mailto:sage [2011/11/15(火) 23:58:26.37 ]: >>407

真摯なコメントありがとうございます。

>不完全性定理は有限の立場、つまり2項述語�を使ってよいなら、
>集合論を経由してかなりシンプルに証明できる。

様相論理を使う証明のことですか？

もう導出性条件の有限な証明を理解するのは諦めようかな、、、。
412 名前：１３２人目の素数さん [2011/11/16(水) 00:06:41.74 ]: >>410
まちがっとるやろ．
それは，|-Aかつ|-Bから|-A←→Bを出しとるんや．
413 名前：１３２人目の素数さん mailto:sage [2011/11/16(水) 00:07:10.52 ]: >>410

>|-A より {B}|-A

ここは、
|-A⇒|-B より、 {B}|-A⇒|-B
としか、言えないのでは？なので、以下も

>演繹定理を使って
>|-B→A-------(1)

|-B→A⇒|-B
としか言えないと思いますが。
414 名前：410 mailto:sage [2011/11/16(水) 07:10:46.56 ]: >>412-413
完全に間違っていた
415 名前：１３２人目の素数さん [2011/11/16(水) 07:50:18.61 ]: >>411
公理的集合論を使った証明ですね。
補題：集合論は集合モデルの存在を証明できない、
を使ってPAの第2不完全性を証明。

第1はRE集合での証明がシンプルで見通しが良い。
詳細な論理式についての議論を省ける。
ただし集合が胡散臭いなら無理...。
416 名前：１３２人目の素数さん mailto:sage [2011/11/16(水) 19:33:17.57 ]: 確かに今じゃ数理論理学は、哲学方面のほうが盛んだよな。
クリプキの定理とか数学史を塗り替えるものだし。
417 名前：１３２人目の素数さん [2011/11/16(水) 20:22:30.89 ]: 394さんの質問にお答えします。

まず関係というからには「何に関する何項関係か」を明示する必要があります。

　例：「nは素数である」は数nに関する１項関係である。n+3<m は数n,mに関する２項関係である。

そしてたとえば「数 n,m に関する２項関係が論理式Aによって表現される」という場合には、
A中に n,m に対応する自由変数記号 x,y があって、x,y に「数n,mを表す項」を代入した論理式のことを
論じる必要があります。
そこで件の悲惨なPDFですが、たとえば89ページの下から4～3行目の

　定理11より、関係 Bew(「r」) は論理式 bew(『r』) によって表現される。

という部分に次の質問をすれば簡単に終わりかと思います。

関係 Bew(「r」) は何に関する何項関係ですか？
論理式 bew(『r』) 中の対応する自由変数記号はどれですか？
（注意：83～84ページにあるように『r』は定数を表す項であって自由変数記号を含みません）
418 名前：１３２人目の素数さん mailto:sage [2011/11/16(水) 22:19:31.52 ]: >>417
解説ありがとうございます。

納得しました。たしかに、皆様の仰る通り、このpdfは間違いがけっこうありました。たとえば、他にも、pp91の(15.6)から(15.7)にかけての箇所も誤りですよね？

417さんのおかげで、より深い理解が得られました。ありがとうございます。
419 名前：１３２人目の素数さん mailto:sage [2011/11/16(水) 22:31:12.25 ]: >>417
追記

もし、第二不完全性定理の証明について解説しているネット上の資料をご存知でしたら、教えていただけませんか？
言語は英語でも構いません。それと、証明の方法は、様相論理等によるものではなく、第一不完全性定理の証明を形式化してする証明によるものでお願い致します。

、、、なんかものすごい厚かましいですね、すみません。
420 名前：１３２人目の素数さん [2011/11/17(木) 00:13:52.72 ]: ttp://www.scribd.com/doc/51607996/An-Introduction-to-Godel-s-Theorems
ttp://phil.gu.se/logic/uppsatser/blanck_logd.pdf

余談だが可証性述語を様相演算子に置き換えることで、
第2不完全性定理は証明できない。
そもそもの3つの可導性条件を満たすことを示すのが
この証明の最大の難所なわけで、これは第1不完全性定理の
算術化を避けては通れない。
しかしこの算術化を厳密に行うテキストはほとんど皆無で、
大抵は3つの条件を事実として認めるか、アウトラインを述べるにとどまる。
かつてNatarajan Shankarは定理自動証明機械を用いて完全な証明を試みたが、
そのプログラム中にはエラーが発見された...。
またBoolosははじめから様相論理で算術を展開したが、
これは強い体系のため、第2不完全性定理よりも弱い定理になることが指摘されてしまう...。
421 名前：１３２人目の素数さん mailto:sage [2011/11/17(木) 04:41:25.90 ]: 次の問題にこたえよ。　解答のみならず、解法も記せ。

【問題】ことがらＡ，Ｂ，Ｃ，Ｄがあり、これらについて次の２つの
　　　　関係が成り立っているものとする。

　　　　　（ｲi Ａであれば、Ｂか又はＣである
　　　　　（ﾛ）Ｄであれば、ＢでもＣでもない
　　　　　　　　　
　　　　　このとき、以下の主張（１）～（７）のうち正しいものを列挙せよ。

　　　　　　（１）Ｄでなければ、Ａではない
　　　　　　（２）Ｃでなければ、Ｄではない
　　　　　　（３）Ａでなければ、Ｄでないか又はＢではない
　　　　　　（４）Ａでなければ、Ｄではない
　　　　　　（５）Ｂでなければ、Ａでないか又はＤである
　　　　　　（６）Ｂでなければ、Ａでないか又はＣである
　　　　　　（７）Ｂであれば、Ｃではなく、Ｄでもない

、
422 名前：１３２人目の素数さん [2011/11/17(木) 11:19:21.45 ]: スレチ
論理学スレか質問スレでやれ
423 名前：１３２人目の素数さん mailto:sage [2011/11/17(木) 15:35:49.54 ]: いちいちコピペに反応するな
424 名前：１３２人目の素数さん mailto:sage [2011/11/17(木) 16:31:46.49 ]: >>420
参考資料と解説ありがとうございます。資料は後ほどじっくり読んでみたいと思います。
やはりderivability conditions の証明は相当に難しいのですね。

すみません、まだ疑問があります。以下の推論はどこがおかしいでしょうか。以下を認めるとD1からD3がでてきてしまうのですが。

D1より
PA|- A ならば PA|-Pr(【A】)
また、
PA,A|- A
ゆえに、
PA,A|- Pr(【A】)
演繹定理より、
PA|- A→ Pr(【A】)
425 名前：１３２人目の素数さん [2011/11/17(木) 18:39:44.83 ]: >>424
＞PA|- A ならば PA|-Pr(【A】)
＞また、
＞PA,A|- A
＞ゆえに、
＞PA,A|- Pr(【A】)

ここがおかしい。
PA,A|-A のとき、
A|-A かつ PA|-/-A があり得る。
426 名前：１３２人目の素数さん mailto:sage [2011/11/17(木) 19:38:25.07 ]: >>425

>PA,A|-A のとき、
>A|-A かつ PA|-/-A があり得る。

すみません、、まだよく分からないのですが、
PA|-/-Aのときは、Prの定義より、PA,Aから Pr(【A】)は証明できないということでしょうか。
427 名前：１３２人目の素数さん [2011/11/17(木) 19:58:19.69 ]: >>426
証明の前にわかっていること。
PA|-A が成り立つとき、PA|-Pr(【A】) を結論してよい。

証明の仮定。
PA,A|-A

例えばAがPAから独立とする。
するとPA|-/-A。
このとき、PA|-Pr(【A】)もしくはPA|-/-Pr(【A】)。
ここで、PA|-/-Pr(【A】)の場合を考える。
すると、A|-Pr(【A】)もしくはA|-/-Pr(【A】)。
さらに、A|-/-Pr(【A】)の場合を考えると、
PA,A|-/-Pr(【A】)
428 名前：１３２人目の素数さん mailto:sage [2011/11/17(木) 21:36:37.32 ]: >>427
よくわかりました。丁寧な解説ありがとうございます。
429 名前：１３２人目の素数さん [2011/11/17(木) 23:01:37.14 ]: >>428
ほんとにわかった？

Pr述語が途中ですり替わっているだけでしょ？
424はきちんと書けば、つぎのようになるでしょ。

D1より
PA|- A ならば PA|-Pr( PA,【A】)
また、
PA,A|- A
ゆえに、
PA,A|- Pr( PA+A,【A】)
演繹定理より、
PA|- A→ Pr( PA+A,【A】)

つまり、この最後が　Pr( PA,【A】)　でなければD3は出てこないでしょ？
Pr( PA+A,【A】)　はまあ自明だよね。
430 名前：官軍（一兵卒）(＾o＾) mailto:sage [2011/11/18(金) 02:03:43.06 ]: >>424
＞演繹定理より

ﾜﾛﾀYO
431 名前：１３２人目の素数さん [2011/11/18(金) 14:31:35.38 ]: 電波テロ装置の戦争(始)
エンジニアと参加願います公安はサリンオウム信者の子供を40歳まで社会から隔離している
オウム信者が地方で現在も潜伏している
それは新興宗教を配下としている公安の仕事だ
発案で盗聴器を開発したら霊魂が寄って呼ぶ来た
<電波憑依>
スピリチャル全否定なら江原三輪氏、高橋佳子大川隆法氏は、幻聴で強制入院矛盾する日本宗教と精神科
<コードレス盗聴>
2004既に国民20%被害250～700台数中国工作員3～7000万円2005ソウルコピー2010ソウルイン医者アカギ絡む<盗聴証拠>
今年５月に日本の警視庁防課は被害者SDカード15分を保持した有る国民に出せ!!<創価幹部>
キタオカ1962年東北生は二十代で2人の女性をレイプ殺害して入信した創価本尊はこれだけで潰せる<<<韓国工作員鸛<<<創価公明党 <テロ装置>>東芝部品)>>ヤクザ<宗教<同和<<公安<<魂複<<官憲>日本終Googl検索
432 名前：１３２人目の素数さん [2011/11/18(金) 16:17:35.18 ]: 魂は幾何学

誰か(アメリカ)気づいた
ソウルコピー機器

テロ装置の再読願います
433 名前：１３２人目の素数さん [2011/11/18(金) 22:31:02.80 ]: 数学、特にその中核となる数論は、
古代の人、未来の人、遠い外国の人、もしかしたら
宇宙人とさえも交信可能な、コミュニケーション素材。

でも基礎論は今の限定された人々のあいだだけだな。
434 名前：１３２人目の素数さん mailto:sage [2011/11/18(金) 22:33:47.42 ]: 虎の威を借る狐

って言葉知ってるか？ｗ
435 名前：１３２人目の素数さん mailto:sage [2011/11/22(火) 02:57:04.13 ]: 通常の整数ではなく、代数的整数でも宇宙人と交信可能だというわけか。
代数的整数の定義は、必然的に選ばれたものだとでも？
436 名前：１３２人目の素数さん mailto:sage [2011/11/22(火) 19:12:38.48 ]: RのQ-線形空間としての基底は存在するが、それを「具体的に構成して見ることは出来無い。」を証明するにはどんな枠組、手法が要るの？
437 名前：１３２人目の素数さん mailto:sage [2011/11/22(火) 20:30:32.85 ]: 選択公理とパラレルになってる
438 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 02:47:31.19 ]: 選択公理の成り立たないモデルを作る必要がある罠
439 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 09:46:17.55 ]: >>433
自然数も実数と同様に人の作ったウソである
440 名前：１３２人目の素数さん [2011/11/23(水) 10:13:50.48 ]: >>439
ウソという言葉に否定的なニュアンスを勝手に感じてはならないわけですね。
441 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 11:09:09.69 ]: イヌやサルにとって自然数も実数もまったく必要がないものである．
442 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 12:34:43.78 ]: イヌヤサルは物を数えるのに自然数は用いていないちう主張？
443 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 12:44:02.85 ]: 1,2,3,∞
444 名前：１３２人目の素数さん [2011/11/23(水) 13:35:33.45 ]: 数学はつまるところ数量の科学でしょ？といったら笑われたｗ
構造・作用・空間の科学だと。
でもそういう概念も数量記号化不可能なものなら数学ではないんじゃ・・・
445 名前：１３２人目の素数さん [2011/11/23(水) 13:37:34.74 ]: 数量的概念のはいらない数学なんてありうるのでしょうか？
あったとしてもそれはある公理系をもった記号論理学にすぎなくなるのでは。
446 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 14:18:31.81 ]: >439
そうすると類別も対応も嘘になるから何にもできなくなると思う。
447 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 14:55:53.34 ]: 嘘、というか、都合のよいフィクション
448 名前：１３２人目の素数さん [2011/11/23(水) 15:12:46.43 ]: 自然数全体の集合というのは、便宜的なものにすぎないが、
自然数に対する興味は知性的な頭脳集団の存続する限り
残るだろう。
素数はどれくらいあるか？(リーマン予想)
不定方程式に整数解はあるか？(フェルマー予想)

そして素晴らしいことには、この二つの問いには
19世紀以来、継続的に散発的でない進展があるということ。
449 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 15:17:52.53 ]: ただし、数論と比較して、幾何学は、
もともとの意味の幾何学(クライン以前)は、継続的な進展は途絶え、
数学としての深みのある問題はなくなってしまったので、
数論の進展も永久に残るかどうかは分からない。しかし、
それは数学ないし知性自体の死を意味するかもしれない。
450 名前：１３２人目の素数さん [2011/11/23(水) 15:49:07.89 ]: 最近集合論を勉強しているけど
座標を前にしてRの直積、写像、ベキ乗について考えてるとなんだか
わけがわからなくなってくる。それぞれが原子、運動、空間の範囲
みたいに見えてくる。しかしそうするとそもそも集合って何って思え
てきて頭が死ぬ！
451 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 16:13:15.63 ]: その程度で死ぬ頭ならそのまま死んだ方がいい
452 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 17:29:15.38 ]: >>449
「クライン以前の幾何学」（初等幾何）というのは
「ガロア以前の代数学」（初等代数）というのと
同程度の意味しかない。

クライン以降、幾何学はリー群論に進化してしまった。
453 名前：１３２人目の素数さん [2011/11/23(水) 17:34:03.03 ]: >>450
ある人に、集合とは何か？と聞かれたので、
「｛｝と，だけで表わせるもの」
と答えてやった。

{},{{}},{{},{{}}},･･･

上記の最初の３つの集合は、それぞれ
自然数の０，１，２に対応する。
454 名前：１３２人目の素数さん [2011/11/23(水) 17:37:59.01 ]: >>446
＞そうすると類別も対応も嘘になるから

どうも私の発言を誤解しているようだが、
私は０とか１とか２とかいう数がウソ（つまりフィクション）
だといったのではない。

それらをひっくるめた概念としての自然数というものが
ウソ（つまりフィクション）だといったのである。

例えば数学的帰納法というのは、あくまで願望にすぎない。
455 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 17:39:28.89 ]: 数学は小説と同じ
人間の思考パターンの表現
数学が研究しているのは、脳という神経組織の振る舞い。
456 名前：１３２人目の素数さん [2011/11/23(水) 18:03:22.65 ]: >>453
可視化へ進みすぎじゃあないか

前に少しグラフを習ったので、それだと考えると「見える」んだけどなあと思った。
つまり座標成分を点、写像は線と考えればいい。（完全）二部グラフならそれぞれの数が
そのまま一致する。特に意味が無いけど、、
457 名前：１３２人目の素数さん [2011/11/23(水) 18:08:30.09 ]: >>453
それは余り説明になっていない。
それにその書き方は一部の集合論の流儀にすぎない。
458 名前：１３２人目の素数さん [2011/11/23(水) 18:38:53.26 ]: >>456
点と線で視覚化できる集合写像はごく一部にすぎないけど。
459 名前：１３２人目の素数さん [2011/11/23(水) 18:59:57.61 ]: >>457
まあいいじゃん、聞いてきた相手もちゃんとした説明が欲しいんじゃないだろうし。
460 名前：１３２人目の素数さん [2011/11/23(水) 20:44:22.77 ]: >>452 まぁ、ある意味そう言うこと。
しかし数論の場合は、ガロア以前の問題を
ガロア以後の研究が解決し続けているのに対し、

幾何学は、問題自体を捨て去った。
捨てずに追いかけ続けたのが、和算。
日本人の性質を表しているようだ。
因みに幾何学という語が日本で使われ出したのは
明治以降。
461 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 21:05:08.00 ]: 初等幾何学が研究されなくなったのは、
難しい問題がなくなったからではない。
難しい問題の全てが解決されないか、
解決されても散発的な解法しか発見されなくなったから。
462 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 21:07:40.13 ]: 最近解かれたケプラー予想は初等幾何の問題。
そういう意味では進展は無いわけではないし
研究も全くなくなったわけではない。
しかし、発見された解法はどれも美しくない。
463 名前：１３２人目の素数さん mailto:sage [2011/11/23(水) 23:27:01.85 ]: 現実と虚構をわざと混同させる意図のもと構成されたフィクション。
464 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 06:33:55.54 ]: >>460
＞幾何学は、問題自体を捨て去った。

とは思わんね。幾何学を合同変換群における不変式論と
定義しなおしてしまった時点で、不変式かどうか判定
すればすむ問題は、もはや問題ではない。
465 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 06:39:59.15 ]: >>457
残念だが、ZFCでは集合論に集合以外のものは出てこない。
つまり{}と,以外で書き表さねばならないようなものは出てこない。

もちろん、内包的な定義は存在する。
しかし、これを外延的に表わせたとするなら
やはり{}と,しか出てこない。

自然数であれ実数であれ複素数であれ、集合である。
すべて{}と,で表わせる。面倒だから省略記法で誤魔化してるだけだ。
466 名前：１３２人目の素数さん [2011/11/24(木) 07:01:01.81 ]: >>465
一部の集合論がZFCだって言ってるんだけど。
467 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 07:07:32.62 ]: >>466
一部というには、大きすぎるような。Axiom of Foundation が特殊
といいたいということでも、ちょっとなぁ。
468 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 07:43:18.26 ]: 内包公理さえうまく定義すれば集合なんてブラックボックスでも形式化できる。
しかし{}と,だけで書けるってのおかしい。
非可算無限個の集合を紙の上にかけるなら元々ZFCなんていらないし。
469 名前：１３２人目の素数さん [2011/11/24(木) 10:43:13.01 ]: >>464
初等幾何の全ての問題が捨て去られたわけではないね。
ケプラー予想などを除く最も主要だった問題群は、
今や代数幾何学という分野名で数論と密接に関連して
研究され続けていると。
470 名前：１３２人目の素数さん [2011/11/24(木) 11:00:32.48 ]: しかし数論の問題と違って、幾何学は、
問題を昇華する過程で、結局古典的問題は
原型をとどめたままでも面白いものは無くなり、
結局捨て去られてしまったのだと思う。

円を有限分割して同体積の正方形に
できないことは、まだ証明されてから
一世期たっていないはずだが、
ケプラー予想ほどではないけど、あまり評価されてないと思う。
471 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 11:34:46.08 ]: 19世紀クラインは、幾何学の問題を不変式論に
還元したというより、群や不変式という
代数学の言葉を使って、幾何学の意味の
拡大を行ったというほうが正しいだろう。
それまで幾何学と思われなかったことまで
幾何学という言葉で綺麗にくくれると。

16世紀にデカルトがすでにユークリッド幾何学を
方程式論に還元できることは言っていた。
しかし、それでも和算家は、
幾何は幾何として研究していたわけで。
472 名前：１３２人目の素数さん [2011/11/24(木) 13:37:31.72 ]: つまんねぇの。
473 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:26:00.68 ]: 第一不完全性定理の仮定はω無矛盾でなく無矛盾でよいと聞きますが、
その場合は証明の定義を変更する必要があると
474 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:27:11.10 ]: >>473
ミスしました。

第一不完全性定理の仮定はω無矛盾でなく無矛盾でよいと聞きますが、
その場合は証明の定義を変更する必要があるとwikipediaにはあります。
しかしそれでは定理の一般化とは言えないのではないでしょうか？
475 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:35:59.28 ]: wikipediaじゃ数学の勉強にはならん。
証明読め。
476 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:38:22.54 ]: >>475
新井敏康の本では証明の定義を変えているという訳ではないようです。
wikipediaの記述が間違いなのでしょうか？
477 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 18:50:53.34 ]: なぜわざわざω無矛盾にしたのだろうかという考察が岩波文庫の不完全性定理本にある。
478 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 20:26:01.91 ]: >>474
証明の定義というより可証性述語の定義。
今新井の本をちらっと見たけど
第一不完全性定理の証明の前に
算術化を行ってProv(a,b)を定義していて、
第一不完全性定理でロッサー述語を一気に導入して証明してた。
ロッサー述語は定理の条件のω無矛盾が無矛盾に広げられる。
ゲーデルも論文出したときは無矛盾にしたかったらしいよ。
479 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 20:30:45.57 ]: >>478
ということは、純粋な一般化ということでいいのでしょうか？
証明の中でPrの定義を変更していますが、証明する事柄にPrは現れないので。
480 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:13:54.22 ]: ゲーデルとロッサーの原論文を読めばすぐに済むことをわざわざ質問する意図がわからない。
481 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:15:53.77 ]: ゆとり世代なめるなよ
482 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:37:03.43 ]: >>479
純粋な一般化とは何だろうか？
483 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:41:54.66 ]: >>482
「ω無矛盾な公理系には証明も反証も不可能な論理式が存在する」という定理を
「無矛盾な公理系には証明も反証も不可能な論理式が存在する」という形に一般化されますが、
この時の「証明」の定義は前者と後者で別物なのでしょうか？
新井敏康「数学基礎論」を読む限りでは両者における「証明」の定義は同じ物のようですが、
484 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:43:16.48 ]: というかそういう疑問を抱く時点で両者の証明を理解してない。
485 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:51:41.38 ]: 対角線論法と不完全性定理は何と何が対応しているんだ？
486 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:56:15.96 ]: ゲーデルの完全性定理、不完全性定理の証明は面倒ではあるけど難解ではないからちゃんと読めよ。
それが解れば周辺論文もそんなに難しくないことがわかる。
広中やワイルズやペレルマンの論文よりずっと読みやすいぞ、内容も平易だし。
487 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 21:57:58.47 ]: >>485
証明を読めば解る
488 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:06:24.94 ]: >>483
同じ。
>>485
対角定理で証明も反証もできない論理式をつくる。
489 名前：483 mailto:sage [2011/11/24(木) 22:08:54.76 ]: >>488
ありがとうございます!
490 名前：483 mailto:sage [2011/11/24(木) 22:18:31.37 ]: 何度も申し訳ありません。
もうひとつわからない部分があります。
新井敏康「数学基礎論」においてderivability conditionsのうちの
(D2)Pr(【A→B】)∧Pr(【A】)→Pr(【B】)
を証明してありますがよく分かりません。
考えている公理系をPAというものとして、PAの標準モデルが存在することを用いて
原始再帰的関数の問題に帰着させて証明するのではいけないのでしょうか？
491 名前：483 mailto:sage [2011/11/24(木) 22:25:25.50 ]: >>490
(D2)PA|-Pr(【A→B】)∧Pr(【A】)→Pr(【B】)です。すみませんでした。
492 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:31:42.84 ]: ここまでくると何で理解できないのかが理解できない

教科書を燃やして数学を勉強するのを諦めた方がいい
493 名前：１３２人目の素数さん [2011/11/24(木) 22:41:44.91 ]: >>490
よく言っていることが理解できないけど
それで証明できるなら別に良いと思う。
494 名前：１３２人目の素数さん [2011/11/24(木) 22:44:30.60 ]: >>486 比べるんじゃない。
価値が全然違う。
495 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:44:33.77 ]: 内容をキチンと吟味せず結果だけ質問しても何にもならないよ。
496 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 22:45:45.54 ]: >>494
価値なんぞ較べてないだろ
難易度が違うと言っている。
497 名前：１３２人目の素数さん [2011/11/24(木) 22:49:20.70 ]: そんなかじゃペレルマンのが圧倒的に難解だろうな
498 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 23:00:28.77 ]: 予備知識のあるなしによるが内容の前提が一般数学の知識内におさまらない分
ペレルマンのが一番難解かもね。

それに較べたら予備知識ほぼゼロでも理解できるんだからゲーデルの論文なんて
有り難すぎて涙が出るくらいだ。
499 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 23:19:46.19 ]: ゲーデルの論文ひいては数理論理学は数学ではない（から素人でも理解しやすい）、という可能性は？
500 名前：１３２人目の素数さん mailto:sage [2011/11/24(木) 23:24:52.14 ]: 理解しやすくはない、ゲーデルは証明は厳密詳細にやってるから、全て理解するのは面倒くさい。
でもあれが数学の証明でないなら、俺は数学の証明を読んだことがないな。

あれくらい諄い数学の証明はそうそうないぞ。
501 名前：猫にコネは不必要 ◆MuKUnGPXAY mailto:age [2011/11/25(金) 00:20:49.81 ]: 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。

猫
502 名前：１３２人目の素数さん [2011/11/25(金) 00:22:29.22 ]: 猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。
猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。猫は痴漢をしました。痴漢をしました。痴漢をしました。痴漢をしました。

芳雄
503 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 07:12:33.12 ]: >>474
wikipediaにちゃんと
「命題の証明より小さな、否定命題の証明が存在しないという性質を追加」
って書いてあるじゃん。これが(ロッサーの方法の)全てだよ。

ところで、「矛盾の証明が存在しない」はPAで証明できないが
「すべての矛盾の証明について、
　これより小さな矛盾の否定の証明が存在する」
はPAで証明できる。もし「矛盾の証明が存在しない」ならば確かに
「すべての矛盾の証明について、
　これより小さな矛盾の否定の証明が存在する」
が、逆は真ではない。したがって、このことは、第二不完全性定理に
何ら疑念を生じさせるものではない。
504 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 08:37:39.57 ]: >>500 それは君の数学の経験が浅いだけ。
505 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 08:43:33.93 ]: >>499
そうだね。
高校数学すらほとんど使っていない。
帰納法くらいか。
数学というよりパズル。
506 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 09:21:51.82 ]: >>503
しかし僕の持っている本では証明の定義は変えてありません。
あくまで定理を示す中で証明可能性述語を変形したものを
用いるのみで、定理のステートメントにおける「証明」の定義は
ゲーデルのものとロッサーのもので変わっていません。
507 名前：１３２人目の素数さん [2011/11/25(金) 10:02:59.16 ]: >>506
その「持ってる本」を明示しなよ。伏せる必要ないだろ？
508 名前：483 mailto:sage [2011/11/25(金) 11:00:01.17 ]: >>507
新井敏康「数学基礎論」です。
509 名前：１３２人目の素数さん [2011/11/25(金) 22:01:31.69 ]: >>465
それは通常ｎ番目の自然数と解釈されるような
推移的集合しか記述しない。
510 名前：１３２人目の素数さん mailto:sage [2011/11/25(金) 22:15:17.39 ]: \
511 名前：１３２人目の素数さん [2011/11/25(金) 22:51:17.77 ]: >>506
定理で示される証明と
可証性述語が表現する証明はちげーよ
512 名前：483 mailto:sage [2011/11/26(土) 00:51:08.93 ]: >>511
それでは>>483において両者の「証明」の定義は同じということで良いのですか？
513 名前：１３２人目の素数さん [2011/11/26(土) 01:04:28.23 ]: たりめー
可証性述語はその証明も反証もできない論理式探すためのどーぐ
何を意味してるかなんてかんけーねー
514 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 02:50:11.55 ]: >>504
車種・車メーカー板に居る人？
515 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 16:29:29.28 ]: >>506
＞あくまで定理を示す中で証明可能性述語を変形したものを用いる

「その変形を、新しい証明の定義とする」と読めない奴は池沼。
516 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 18:33:06.39 ]: ゲーデルの第二不完全性定理の証明は、何をもって、証明されているか
ということが問題なのだ。いかなる本にも、証明は書いてないのだ。
このような、方法で、証明ができるということが書いてあるのだ。
この違いは専門家とよく話さないとわからないもので、このような
ところで説明されてわかることではない。
517 名前：１３２人目の素数さん [2011/11/26(土) 20:07:34.59 ]: ゲーデルの第二不完全性定理の証明ごときで
専門家と話す事なんかない。
数学としてはエレメンタリーな組み合わせ論の証明にすぎない
518 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 20:09:09.83 ]: 哲学や論理学としてみたら一流の結果かもしれないが、
数学としてみたら二流以下の結果
519 名前：１３２人目の素数さん [2011/11/26(土) 20:21:06.16 ]: 平方剰余の相互法則のような、いつまでも高いレベルでの一般化があるようなよい定理だと思うが。
520 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 20:51:50.70 ]: 平方剰余の相互法則の一般化の様に豊かな応用が無い。
521 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 20:55:04.45 ]: 平方剰余の相互法則は、フェルマー予想界隈の
研究からの要請があって、一般化されてきたのであって、
単にいじくりまわしていたわけじゃ無い。
522 名前：１３２人目の素数さん [2011/11/26(土) 21:04:32.09 ]: >>515
証明の定義自体は何もかわってないはず。
523 名前：１３２人目の素数さん [2011/11/26(土) 21:07:30.84 ]: >>516
一応新井の本には証明が全部入ってる。
ただし冪関数ありのPAだけど。
524 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 21:39:39.54 ]: >>523
３章を読み終わっているなら聞きたいんだが、
P101の補題3.3.2は証明になっていないと思うんだが、どう？
525 名前：１３２人目の素数さん [2011/11/26(土) 21:54:48.30 ]: >>521
それは出鱈目が過ぎる
526 名前：１３２人目の素数さん [2011/11/26(土) 22:01:08.85 ]: >>521 どう？
527 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 22:02:04.34 ]: 訂正
>>525 どう出鱈目？
528 名前：１３２人目の素数さん [2011/11/26(土) 22:54:15.96 ]: >>527
フェルマー予想界隈の「要請」から一般化されたとか歴史的におかしいだろ。
529 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 23:14:52.57 ]: 第二不完全性定理をどこまで弱い算術で
証明できるかという方面の研究はあるよ
まあ割と些事だけどね

でも518はどうせP=?NP問題とかも
数学としてはエレメンタリーな二流の問題とか言って
切って捨てるんだろうな
530 名前：１３２人目の素数さん [2011/11/26(土) 23:25:41.21 ]: >>524
確かに何をやっているのか理解できない。
「でよい。　　■」って何だよｗ
531 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 23:37:03.89 ]: >>528 平方剰余の相互法則の重要な応用として、
全ての整数が四つの平方数の和で表されるという定理がある。
この種の問題(フェルマー予想はp乗数の和の問題)を初めとして
重要な応用を目指して一般化されてきた。
無目的に一般化してきたわけでは無い。
532 名前：１３２人目の素数さん mailto:sage [2011/11/26(土) 23:39:27.44 ]: >>529
前半。些事、そうですね。

後半。それは解けてみてからでなくては
わからないけれど、今までの状況からすると
その可能性はかなり高いですね。
533 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 00:02:56.01 ]: >>530
やっぱりそうだよね。
どうも破綻していると思えてならない
534 名前：１３２人目の素数さん [2011/11/27(日) 00:42:06.34 ]: >>531
ルジャンドルによる四平方定理の証明は1770年。
平方剰余の相互法則を証明したガウスが生まれる前のこと。
535 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 01:18:37.60 ]: >>534 それって証明に不備があったやつでしょ？
19世紀にディリクレが埋めたけど。
536 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 01:21:34.41 ]: とにかく平方剰余の相互法則の応用でそのルジャンドルの定理も
証明出来るし、相互法則の一般化でより深い整数論の定理がいろいろ証明できるのよ。
537 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 01:44:25.69 ]: もひとつ補足しておくと、
平方剰余の相互法則は、何も無いところから
いきなりガウスが見つけたものじゃなくて、
ルジャンドルの平方和の研究の中に
その芽があるんです。相互法則のステートメントで
使うカッコをルジャンドル記号と言うでしょ。
538 名前：１３２人目の素数さん [2011/11/27(日) 04:00:55.62 ]: >>537
相互法則を発見したのはオイラーじゃなかったっけ？
539 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 05:41:22.25 ]: >>523
普通の数学の定理と異なっている内容であることに気がついていない
証拠なのだ。
第一不完全性定理とは、全く性質が異なっていることに気がつくべき
なのだが、普通気がつかない。
540 名前：１３２人目の素数さん [2011/11/27(日) 06:17:01.75 ]: >>539=>>516かい？
思わせぶりなことを書いても、2chじゃただのハッタリとしか思われないよ
541 名前：１３２人目の素数さん [2011/11/27(日) 07:18:09.67 ]: suimasenga
圏論と論理学の関係について教えてください
清水によれば圏は普遍論理だそうですが
542 名前：１３２人目の素数さん [2011/11/27(日) 08:31:32.56 ]: >>540
ぶっちゃけ、第一より第二が大事！と発狂する奴は
「無矛盾厨」なる人格障害の可能性が大。

>>529の研究の中には、以前、紹介があった自己検証体系も
含まれると思われるが、あれはあれでちょと面白い。

どうでもいいが平方剰余の相互法則のような
エレメンタリーな「算数」をありがたがる
小学生は無限を扱うこのスレッドには
立ち入らないでいただきたい。
543 名前：１３２人目の素数さん [2011/11/27(日) 08:37:22.48 ]: 論理推論を算術計算でシミュレートする、というアイデアを
数学として認めたくない人はいる。大抵は爺ィだが。
544 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 09:59:03.95 ]: >>540
483 にこんなところで訊くなといっているだけ。
545 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 12:40:59.08 ]: >>542 平方剰余の相互法則はエレメンタリーな
ままでは終わらない、とても深い理論。
代数屋はもちろん、幾何でも解析でも
こんなことは常識なのに、基礎論屋とはやっぱり
感覚が違うなと感じる。
常識をわきまえたうえであえて傍流に入ると言うなら
まだわかるが、常識を最初から認識してない。
数学で無い別の価値観をもった非数学分野だと
いうなら、それでいいんだけど。
546 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 14:03:31.53 ]: >>545
自演乙
547 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 15:37:47.45 ]: >>545
平方剰余の相互法則は、幾何や解析どころか
代数でも自分の研究とは無関係と思う人は数多い。
これこそ常識であって、545の考えは他の数学者には
通用しない「俺様常識」に過ぎない。
548 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:26:01.98 ]: >>547
そんな事はない。
そんな事言ってるのは、せいぜい、数学の流れを見る余裕も無く、
学位や就職の為だけの論文作成作業におわれている
底辺院生か底辺ポスドクぐらいだろ。
549 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:32:04.61 ]: >>547 たぶんあなたの言っている数学者は、
かなり広義の意味であって、志の低い人たち。
歴史に名を残す様な数学者は一人もはいっていないと思う。
550 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:33:17.10 ]: コイツどんだけ数論を過大評価してるんだｗｗｗ
551 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:39:40.24 ]: っていうか、まともな数学者の多くは、
代数とか幾何とか解析とか数論とか、分けてなんかいないよ。
何でも使うから。
552 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 16:51:54.56 ]: んだ。必要ならメタ数学の定理も使う。
553 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 17:04:33.97 ]: >>552 少しね。でも、基礎論のアイデアを
使うだけで、基礎論の研究は使わ無い。
というか、基礎論の重要な成果のほとんどは
もともと普通の数学者が作った。彼らを後世が
どう呼ぶかは後世の人が決めたのであって、
やってる数学者本人は、自分の専門分野なんて
気にしてない。
基礎論からキャリアをはじめて基礎論屋を
名乗っている人のやってる研究はみんな役に立たない。
(一部の役に立てようとして研究しているものは除いて)
554 名前：１３２人目の素数さん [2011/11/27(日) 18:55:45.54 ]: 今のロジックの主流はモノイダル論理ですね。
これは∧と∨を同一視したものです。
またリテラルはAと￢Aを同一視します。
これは圏論との関連もあって非常に重要な位置を
数学基礎論において担っていますね。
数論はモノイダル論理で書き換えることができます。
例の平方剰余の相互法則もモノイダル論理の一推論規則にすぎないです。
555 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 19:51:33.51 ]: >>554 何の狙いがあって、そんな事をやっているのですか？
556 名前：１３２人目の素数さん [2011/11/27(日) 19:58:40.23 ]: 「すぎない」を使う奴の文章は信用しないことにしている
557 名前：１３２人目の素数さん [2011/11/27(日) 20:23:24.33 ]: >>555
まずモノダイル論理はすべての計算モデルで解釈可能です。
次に非常にシンプルでコンパクト閉圏と対応しており、
数学全体の記述をすることも可能です。
おそらくモノダイル論理が導入されたのは
ジラールによる線形論理の研究がはじめてでしょうが、
今では言語哲学、分析哲学、計算機科学、公理的集合論といった
あらゆる世界で運用されるようになっています。
クミルの竪琴とよばれる推論規則などは
修正クリプキ構造T1-Stepを張ったデントライトの海で
展開される特殊なモノダイル論理で、ジュークの宇宙を再現することができますね。
特にフィッシャーのSSS_ΩやF0-代数との関連で注目されています。
558 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:18:49.35 ]: ＞基礎論の重要な成果のほとんどはもともと普通の数学者が作った。

まず、基礎論の重要かつ基本的な成果はゲーデルによって挙げられた。
述語論理の完全性定理、自然数論の不完全性定理、選択公理の相対無矛盾性etc．

「普通の数学者」が基礎論以外の数学でも成果を挙げている、という意味なら
ゲーデルが基礎論以外の数学で挙げた重要な成果を一つでいいから教えてほしい。
559 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:20:42.82 ]: >>558
ゲーデル解
560 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:22:52.18 ]: >>559
残念ながら、その成果は、ゲーデルが論理学においてあげた
華々しい成果に比べると大したことがない。
561 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 21:26:19.72 ]: ゲーデルはロジシャン中のロジシャンだろ
数学者ではない、と思う
562 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:05:06.09 ]: ゲーデルは相対性理論もやった
563 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:06:38.16 ]: >>557 ですから、そうする事によって、何を目指しているのですか？
564 名前：１３２人目の素数さん [2011/11/27(日) 22:16:57.58 ]: >>563
理論物理や数論幾何で頻出するユニポテント群の
構造解析にマスセル-ドーソンの創造なんていう
解釈可能世界を導入する際にユニ楽園という
議論領域の全体を動くような広義圏論のステンレステンソル代数の
一つのアイディアとなるってことですね。
パースのアイディアは存在の海なんて煩雑なものだから。
565 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:22:34.16 ]: 無茶苦茶やなぁ
566 名前：１３２人目の素数さん [2011/11/27(日) 22:24:23.93 ]: それからブラウンが提唱した形式の法則なんかはCalculusに基く
ブール代数の構成を可能にした「区別」という、
マトゥラーナ＝ヴァレラ図式による拡大可能な
システムの自己観察機能による再循環になってる。
例えば「横断」による算法、これは自己同型写像による対象aの分布関数
R：Spec(∑_N0)；B(a,ε)→Vll(-<>r)
を意味するもので、primary algebra の公理からアイオーンの時間の固体化、
即ちリンデンバウム補数の位相が閉であること(ArrX/R)、
また複素散乱ウカシェベッチ型ベクトルの縮減対応から得られる
「埋め込み」が線型写像であること⇔Θ：ξ(Asc(3))ΛΓ(A_0)→Γ(A_0)の作用が存在する。
直線的被覆が「シミュラークルの質料」というXの規定なんかが有名。
567 名前：１３２人目の素数さん [2011/11/27(日) 22:28:12.64 ]: さらにはヒルデガルド対応ってのがる。
一般Tate仮説の∃￢%がKe(C*)の底鎖列として定義される場合に、
任意カントール空間の実効的閉集合世界のMedvedev次数構造が
immunityは以下の可換図式と同値。
s → bl → bel → I
　　　　　↓　↓
　　　　　b → tl → w
つまりVintage代数がストーン双対ってこと。

あとは、identification in the limit をベール空間の集合へ一般化した
学習還元可能性。学習は以下のようなもの。

心象自制有界学習(P ≦bl Q)：
(∃ψ)(∃c)(8g 2 Q) [limn(gn)(g) 2 P
& #fn :(g n) , (g n + 1)g < c]:

誤謬有界学習(P ≦bel Q)：
(∃ψ)(∃c)(8g 2 Q) [limn(gn)(g) 2 P
& #f(g n) : n 2 !g < c]:

剰余類学習(P ≦tl Q)：
(∃ψ,;;;;,ψ_k )(∀g∈ Q)(∃m ≦ k) limnψm(gn)(g) ∈ P:

あるいは、ジュリア閉集合が、
(∀m) P ∧ Im ≠∮となるような
有理区間の計算可能な枚挙fImg が存在しないとき。
568 名前：１３２人目の素数さん [2011/11/27(日) 22:29:33.79 ]: さらに、中間休止RC0が論理のイマージュとなった「差異」、
セリーの合弁写像Fmin：など、アームストロングの公理系による裏付け、
ドゥルーズのindetermineとideeの分裂など・・・。
最近では以下のようなボニファスの記述(無限還元公理)がある。

Tc1：aを中心とした推論可能域をｒをa；ｒと記述する
Tc2：消滅を∃￢%とする
Tc3：∃￢%のヒルデガルド対応は∃%である
Tc4：∃%の次は0；ｒとする
Tc5：0；ｒ→1；ｒの対応でModanponetが一階無効
569 名前：１３２人目の素数さん [2011/11/27(日) 22:30:40.26 ]: ちなみにセリーの合弁写像の根拠を与える。
ギヨーム理論が数詞と内部空間をゼロ複数、S単数などの空間的配置で
形態論に内在する意味の精神過程を捉えるエルチュードだとは自明。

P; Q 2 ω＾ω だから、P がQ にculervent還元(P s Q) とは、
ある双対アルゴリズムが存在して，任意のg 2 Q に対して
(g) 2 P となるときを指すから、T の定理とL反駁の
分離関数全体の集合Sep(T) はr.e.separating class
と呼ばれる特殊な実効埋蔵閉集合になる。

つまり完備側芽のTerr分解X_0[－，]：が以下のように変形される。

Ps j= (8x; y)(9z)(x < y ! x < z < y).
(9e0; : : : ; ek )(8g 2 Q)(9m k) em(g) 2 P

これがセリーの合弁写像と同型である。
570 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:38:25.64 ]: つまらない
571 名前：１３２人目の素数さん mailto:sage [2011/11/27(日) 22:43:35.02 ]: 知の欺瞞、ﾁｮｰひもカルト、圏論カルト
572 名前：１３２人目の素数さん [2011/11/27(日) 22:49:54.30 ]: 具体的な内容についていけない場合は
カルトと批判すればOKとｗ
573 名前：１３２人目の素数さん [2011/11/27(日) 23:21:58.96 ]: >>566-569
止めろ。アホ！
574 名前：１３２人目の素数さん [2011/11/28(月) 00:05:28.92 ]: >>572
ｗをつければ高みに立てると思っているのだろうか
575 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 02:29:48.13 ]: >554
ついていけなくて悪いが……モノダイル論理ってもしかして双対を扱えるの？
もしそうならちょっと興味があるなぁ。
576 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 03:20:01.88 ]: >>575
知の欺瞞
577 名前：１３２人目の素数さん [2011/11/28(月) 10:26:41.08 ]: >>566-569
もっと書け！
578 名前：１３２人目の素数さん [2011/11/28(月) 10:37:03.52 ]: 情報板ではダメそうなのでここにきました．教えて下さい．
プログラムの表示意味論って何のためにあるのですか？
分かり切ったことをあらためて書き下しているようで狙いがわかりません．
おまけに継続やエラーや入出力などつまらない所（論理の範囲外である
所）で当然のようにツギハギを重ねているようにみえます．
そのツギハギが表示的意味論の生き甲斐なのでしょうか？
579 名前：１３２人目の素数さん [2011/11/28(月) 18:16:29.65 ]: 質問です。

不完全性定理を証明するために、形式的体系を算術化しますよね。
その算術化の方法について、どうしてβ関数によるものを考えるのでしょうか。

田中「数学基礎論講義」には

「形式的算術では指数関数が最初から与えられているわけではないので、それとは異なるコード化技法が必要になる」pp.57

とあります。
しかし形式的体系（たとえばPA）に指数関数記号がなくても、
原始再帰関数（つまり指数関数）は表現可能なのだから、実質的には指数関数記号があると考えてもよい気がするのですが。
どうなのでしょうか。
580 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 18:46:48.46 ]: 掛け算がないだけで第一不完全性定理も成立しませんので。
581 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 18:50:25.58 ]: その表現可能性を示すためにβ関数を使うんじゃなかったっけ？
582 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 18:58:31.98 ]: 東大のゲーデルと20世紀のやつの三巻にそのあたり詳しく書いてある
583 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 19:06:59.11 ]: あれは駄本個人的に
584 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 20:34:05.86 ]: 理由書かないと駄レス
585 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 21:13:44.36 ]: あれは良本個人的に
586 名前：１３２人目の素数さん mailto:sage [2011/11/28(月) 22:34:14.39 ]: >>578
妙に的確で変な質問だな。自分からは言いたくないもんだから誰かに言わせたいみたいな。
理由自分でちゃんとわかってるだろ。
587 名前：スレタイスレ446 [2011/11/28(月) 23:54:27.03 ]: >>578
表示的意味論・操作的意味論・公理的意味論ってのは単なる意味論の分類。
大雑把に言って、
表示的意味論≡数学的意味、
操作的意味論≡抽象機械、
公理的意味論≡論理学的意味。
プログラミングの文脈で述べられるが、
見方によっては数学のモデル理論なんかも表示的意味の領域理論の一種と呼べる。
公理的意味論は普通の数理論理学だけあって
決定不能な命題が他の意味論より発生しやすい。
たとえば並列性の概念をもった理論などは、
数理論理学では一般に記述不能。
これは並列性特有の非束縛決定不能性(Unbounded nondeterminism)命題などが原因。
例えばデッドロックみたいなイメージ。
ただし時相論理なんかで計算状況の断片だけ切り取ったりするくらいは可能。
その一方でKowalskiが計算可能性よりも推論規則の方が
多くの命題を生成可能であると証明しているから、
単純に包含関係があるわけでもない。
以前向うのスレで紹介したゲーム論的意味論で不完全性定理が成り立たない自然数論の構成も、
単純な表示的意味論による解釈を2つのプレイヤーの戦略に置き換えると、
並行的な現象であるクラスの決定不能性が破れてしまうという原理によるものだろう。
ちなみにエラー補足や継続などもプログラム言語の内部。
>>579
コードとデコードの保証。算術化って素数の冪乗でもできるけど、
PAに指数関数なかったら例えば論理式なんかがゲーデル数化できない。
>>582
田中の本をまとめたのがその本だよ。
588 名前：スレタイスレ446 mailto:sage [2011/11/29(火) 00:04:16.60 ]: >>579
追記：詳しくはその本の9章参照。
589 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 01:30:11.43 ]: >>578は何を読んで次の様に感じたのだろうか？
> おまけに継続やエラーや入出力などつまらない所（論理の範囲外である
> 所）で当然のようにツギハギを重ねているようにみえます．

表示的意味論でもcontinuation semanticsのスタイルで最初から記述すればツギハギにはならない。
ただ初学者向けにdirect semanticsのスタイルで定式化してからエラーや入出力を扱うとなるとcontinuationスタイルに変える必要がそこで生ずるので
知らない人にはツギハギみたいに見えるかも。

因みにcpoやそれに関する再帰方程式に関する領域論は別にして、トイ言語でないプログラミング言語に対する表示的意味論については
日本語ではロクな教科書はないので、英語の教科書で勉強するしかない。日本語の教科書によっては「表示的意味定義とはインタプリタを書く事である」
なんて大きな勘違いをしているとしか思えないのが岩波の某有名教科書シリーズにあったりするからね。

>>587
> >>578
> 表示的意味論・操作的意味論・公理的意味論ってのは単なる意味論の分類。
> 大雑把に言って、
> 表示的意味論≡数学的意味、
> 操作的意味論≡抽象機械、
> 公理的意味論≡論理学的意味。

公理的意味論は、論理的意味というよりも証明の為の形式的体系で、それに対する解釈を与え、公理的意味論の健全性の基準を与えるのが
表示的意味論と考えれば良い。公理的意味論を与えただけでは矛盾していたりする可能性があるが、同一のプログラミング言語に
表示的意味論も与えて、その表示的意味という解釈に対して公理的意味論の体系が健全である事を示せば、公理的意味論で与えた
証明体系を安心して使用できる事になる。

これが>>578が質問していた表示的意味論を与える意義は何か？という問いへの答え。
590 名前：１３２人目の素数さん [2011/11/29(火) 01:34:42.22 ]: >>588
その本のpp80の注意.には

PAにはすべての原始再帰関数に対する関数記号とそれらに関する公理が入っていると考えてもよい

とあるので、原始再帰関数である指数関数の記号と公理もPAには入ってると考えてもよいのですよね？
となると、β関数の意義って何なのかがよく分からなくなるのですが、いかがでしょうか。
591 名前：１３２人目の素数さん [2011/11/29(火) 02:46:09.24 ]: representable functor
592 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 07:12:51.67 ]: こんなところで訊くなといっているのだが、わからないやつだね。
原始帰納関数が何故、表現可能となるか、とくに帰納法のところを
どう書くか考えないで、結果が成り立つことばかりいっているから
わからないのだ。
593 名前：スレタイスレ446 mailto:sage [2011/11/29(火) 07:45:34.33 ]: >>575
コンパクト論理のことだろう。
>>589
それが正しい回答だろう。
>>590
スコーレム関数として考えると、
理論から関数記号をとっても、
その関数に関係する論理式をユニークにとって保存拡大できるので、
はじめから原始再帰的関数をすべて入れてても結果は同じ。
しかし今回は指数関数が入っていないとして話を始めるので
β関数を導入しますよ、ということ。
594 名前：１３２人目の素数さん [2011/11/29(火) 18:25:42.28 ]: >>592
周りに聞ける人がいないもので。
今質問しているのは、形式的体系の算術化に関することなので、表現定理云々はあまり関係ないように思うのですが。

>>593
コメントありがとうございます。少し考えをまとめます。

第二不完全性定理を証明する際にPAの証明をPA内部で証明しますよね。
そのとき、形式的体系を指数関数を使ってコーディングするかβ関数を使ってするかで、その方法は異なってきますよね
指数関数によるコーンディングを選んだ場合、PAの証明をPA内部で証明するにはPAに予め
指数関数記号とその公理が予め含まれていないといけないように思われます。
これに対して、β関数によるコーディングを選んだ場合なら、予め指数関数記号とその公理がPAに含まれていなくても、
PAの証明をPA内部で証明することができます。これがβ関数を導入する意義であります。

しかし、>>590,593にあるように実質的にはPAには指数関数記号とその公理が備わっていると考えてもよいので、
実は指数関数でコーディングをしても、PAの証明をPA内部で証明するには何ら不都合はない。　　　　　　　□

以上の考え方でおかしいところはあるでしょうか？
よろしくお願いします。
595 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 19:08:35.84 ]: いや指数関数が入ってない場合は
β関数はもっと前に第一不完全性定理を証明するときに
既に導入されるでしょ
596 名前：スレタイスレ446 [2011/11/29(火) 20:50:01.89 ]: >>594
そんな感じですね。
カントール対関数でユニークにエンコード、
β関数でユニークにデコード、
両方とも可証性述語の定義に必要。
指数関数というか原始再帰的関数とそれに関する公理を
すべてぶっこんだPAの保存拡大はPRAとかよく言われます。

余談：ところで不完全性定理はT|-/-Con(T)でしたが、
Π1^0文に関してはWKL0|-φ⇒PRA|-φとなり、
ヒルベルト・プログラムの断片的実現と呼ばれます。
ですからケーニッヒ補題が超越的とかいう書き込みが上の方にありますが、
ケーニッヒ補題を使った文は有限の立場の文に置き換えれますね。
597 名前：１３２人目の素数さん mailto:sage [2011/11/29(火) 20:54:48.16 ]: 全くわからないやつだね。
有限列をどうやって表すかってことなんだよ。これができなければ、
なにも表現できないんだよ！
598 名前：１３２人目の素数さん [2011/11/29(火) 22:07:07.10 ]: >>595
β関数を導入しなくても、第一不完全性定理は、
PAに指数関数の記号と公理がない状態で指数関数によるコーディングで証明できると思うのですが。

>>596
よかった、>>594の考え方であってたのですね。安心しました。
PRAなるものがあるのですね、知りませんでした。勉強になります。余談に関しては知識が追い付かずよく理解できませんが、
いずれ分かるようになれたら良いと思います。

>>597
私の読解力がないせいだとは思うのですが、言っていることがよくわかりません。
「有限列をどうやって表すか」というのは形式的体系を自然数に
エンコードする方法のことですよね？いろいろ種類はあると思いますが、
私は素数のべき乗によるものと対関数によるものぐらいしか思いつきません。
599 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 07:19:13.98 ]: 要するに、論理式で書くというkとがわかっていないんだね。
600 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 07:27:47.20 ]: >>596
PRAはPAの保守拡大どころか、それより弱い体系なんだけど……

＞PAに指数関数の記号と公理がない状態で指数関数によるコーディングで証明できる
要は E(x,y,n) : y = x^n とか P(x,y) : 「y は x の証明である」とかを
加法と乗法だけを用いた論理式で表現しないといけないわけだけど、
どうやって実行するつもりなんですか？
601 名前：スレタイスレ446 mailto:sage [2011/11/30(水) 07:48:04.07 ]: >>600
＞PRAはPAの保守拡大どころか、それより弱い体系なんだけど……
確かにそうでしたね・・・。
量化付きの文の帰納法が制限されていたのを忘れていました。
だから有限の立場というんだった。
602 名前：１３２人目の素数さん [2011/11/30(水) 09:33:43.93 ]: >>600

表現定理により、原始再帰的関数および原始再帰的述語はPAにおいて数値別に表現できますよね。
となれば、たとえば8=2^3はPAにおいて、PA|-8=2・2・2・1　と表現できるのではないのでしょうか。

・・・と思いましたが、なんか怪しいですね。
表現定理は一応一通り自分で証明したつもりだったんですが、改めて各文献に目を通したらきちんと理解してなかったみたいです。
とくに今になって>>592さんの言う原始帰納法の箇所が実はめちゃくちゃ大事だったことに気が付きました。
今日もう一度しっかり勉強してから、質問させていただきます。
ありがとうございました。
603 名前：１３２人目の素数さん [2011/11/30(水) 09:44:15.71 ]: 追記：
＞PAに指数関数の記号と公理がない状態で指数関数によるコーディングで証明できる

この発言に関して、完全に私が誤ってました。
604 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 10:10:00.35 ]: cs2011_terui.pdfがピンポイントかも。
605 名前：１３２人目の素数さん [2011/11/30(水) 11:36:54.26 ]: >>586 >>587 >>589
ありがとうございます．参考になりました．
でもやはり表示的意味論の爽快感がどこにあるか不明です．
（健全性の根拠というのも内向きの意義のようですし）
λ計算の意味論は自明なほどに簡潔です．
プログラミング言語と表示的意味論とは本来似合わないのでは？
表示的，操作的，公理的の３分類もいまいちですね．
意味論といえば表示的に決まっているでしょう？
公理的意味論はむしろ証明論ですね．
606 名前：１３２人目の素数さん mailto:sage [2011/11/30(水) 20:26:05.47 ]: >>605
横からスマン、
個人的な意見だけれど、表示されるものがなんなのか明確なコンセンサスが
あるわけじゃないからいろんな理論が出てくるんだろうと思っている。
表示されたものがなんであるかによってその３分類が出てくると考えると
そこそこしっくりくる。
607 名前：589 mailto:sage [2011/12/01(木) 02:32:26.27 ]: >>605
> でもやはり表示的意味論の爽快感がどこにあるか不明です．
> （健全性の根拠というのも内向きの意義のようですし）
しかし、プログラミング言語に対して定義したホーア論理の体系に対して健全性が保証されていなければ、そのホーア論理の体系で検証しても
全くの徒労となる可能性があるのだから、公理的意味論に対して健全性を示す事は最低限必要不可欠な事ですよ。

> λ計算の意味論は自明なほどに簡潔です．
それはλ計算はプログラミング言語として見れば極めて単純なトイ言語だからに過ぎない。
それと、意味定義に用いるメタ言語がλ記法という、対象言語のλ計算とそっくりのを用いるから更に簡潔に見えるだけ。

> プログラミング言語と表示的意味論とは本来似合わないのでは？
プログラミング言語の意味を実装と独立に与えるには表示的意味論を定義してやるしかない。
プログラミング言語を設計する人間は、本来は、その言語の表示的意味を定義するべきなのだ。
それが余りにも複雑怪奇な代物になれば、それは設計している言語の構成に問題がある証拠であり、
表示的意味がより分かりやすいように言語設計を改める必要がある事を示している。
プログラミング言語に対して定義された表示的意味は、その言語の利用者（ソフトウェア技術者）が知る必要はない代物なのは確か。

> 表示的，操作的，公理的の３分類もいまいちですね．
> 意味論といえば表示的に決まっているでしょう？
それは数理論理学屋の立場からすればその通りだが、プログラミング言語に対する形式的意味論の研究は、
数理論理学屋がプログラミング言語の研究に流れ込んで来るようになる前の1960年代後半～1970年代初頭に既に始まっているから、
コンピュータ・サイエンスの歴史からすれば、君のその主張は全く正しくない。
自然言語の意味論にしても、数理論理学の立場からは「意味論」という名前が相応しくないと感じる様々な意味論がある様にね。

> 公理的意味論はむしろ証明論ですね．
これも数理論理学の立場からすればその通りだし、589に書いた通り個人的には同じ意見だが、
587の人が書いている通り、プログラムの論理的な側面を「知る」為の「意味論」というのがコンピュータサイエンスの立場。
608 名前：１３２人目の素数さん [2011/12/01(木) 05:54:50.23 ]: >プログラミング言語の意味を実装と独立に与えるには表示的意味論を定義してやるしかない。
了解です．
>プログラミング言語を設計する人間は、本来は、その言語の表示的意味を定義するべきなのだ。
了解です．
>それが余りにも複雑怪奇な代物になれば、それは設計している言語の構成に問題がある証拠であり、
>表示的意味がより分かりやすいように言語設計を改める必要がある事を示している。
それが表示的意味論の具体的なメリットの一つですね．
>プログラミング言語に対して定義された表示的意味は、その言語の利用者（ソフトウェア技術者）が知る必要はない代物なのは確か。
そういう意味では，今のプログラミング言語は改める必要があることが既に示唆されているということでしょうか？
609 名前：１３２人目の素数さん mailto:sage [2011/12/01(木) 08:38:45.01 ]: >>605
>λ計算の意味論は自明なほどに簡潔です．

操作的意味論のこと？
λ計算だって表示的意味論、
というかスコット理論がが理論的根拠だよ？
610 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 15:27:19.05 ]: D無限大モデルが自明とは恐れ入るな。
611 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 15:28:56.89 ]: 天才現る
612 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 15:40:45.48 ]: >>393とか、ちょっとでも理解できていたら、
表示的意味論が無意味とかλ計算の意味論が自明なんて思わないだろう。
613 名前：１３２人目の素数さん mailto:sage [2011/12/02(金) 22:25:41.47 ]: 写像を学んでて思ったただの感想なんだけど、一般項とか自然数てなんだろうな。数列が
2,4,6,8,10,,n,,と並んでる場合一般項は2＋2(n-1)だ。
しかしこの並びを集合と考えると、この集合はmap(N,N)に含まれる
写像の一つに過ぎない。つまり｛f(1)=2、f(2)=4、、ｎ、、｝という写像。
そう思うとmap(Ｍ、Ｎ）の一般項てなんだろう。んで別に一般項て
わけじゃないけど、全単射というのがある。
そうすると自然数というかa<b<c...というように規則を持つ無際限な並びと
いうのは、map(Ｍ、Ｎ）に含まれる写像のうちで、ＭからＮへの全単射を持つ
写像という様に考えたほうがいいのかもしれないと思った。まああくまで集合
ありきの考え方であって、自然数は集合から定義されるものではないのかもしれ
ないけど。
614 名前：613 mailto:sage [2011/12/02(金) 22:26:55.37 ]: 間違えた。｛f(1)=2、f(2)=4、、ｎ、、｝の｛は（だわ。
615 名前：１３２人目の素数さん mailto:sage [2011/12/03(土) 01:19:17.26 ]: 間違えてるのは書き込むスレッド
616 名前：１３２人目の素数さん [2011/12/03(土) 01:26:34.73 ]: 知的財産・受験生ブロガーの一覧

士業名鑑
www.samrai-index.com/04benrishi/benrishi_blogJ.htm

弁理士試験ストリート
benrishi-street.com/
617 名前：１３２人目の素数さん mailto:sage [2011/12/03(土) 02:06:54.44 ]: >613
余代数ネタ？
ペアノの公理からして後続関数による定義だしな。
618 名前：613 mailto:sage [2011/12/05(月) 13:14:10.95 ]: >>617
すまん勉強不足なもんで言ってる事がわからん、、
集合論を学んでると数に対する自明な感覚が失われてきて、もっと上手く定義
しなおせられれば気持ち良いんだが、わからないとものすご気持ち悪いまま終
わると言う感じ。が続く

順序数、とか、同型でない、とかなあ。
自然数は全然自然な無限でもなんでもないという事はよくわかったし、そういう横並びにかつ規則を
持って並んでる無限だけが無限じゃない、という事もわかった。でもそれは濃度と、写像（全単射）の
概念があれば十分なんじゃなかろうか。順序型ωと濃度アレフ０って区別のアプローチが違うだけで
どっちかがあればどっちかが要らないような気がする。
619 名前：１３２人目の素数さん [2011/12/05(月) 14:46:58.37 ]: >>617
0と後者関数から自然数全体を生成するのは
自由代数の最も基本的な例だから
余代数ではなくて代数。
余代数ならばωから下ってくる形の定義法になる筈。
620 名前：613 mailto:sage [2011/12/05(月) 16:41:32.92 ]: ちょっと理解に苦しむまま集合への３０講を読んだ。６１３から感想を
乗せてしまって申し訳ないんですが、最後に１つ質問。
選択公理によって議論が巻き起こったと言う話があるようですが、そもそも
対角線論法は選択公理なしで行えますか？大まかな最低限の段階として

１自然数の集合が持つ元から、実数の集合が持つ元をただ一つ指定する。
２自然数の集合が持つ全ての元から、実数の集合の元をただ一つ指定する。
３自然数の集合が持つ全ての元から指定された実数の集合の元が、実数の集合
の元全てであるとすると、実数の集合が元として持たない実数が存在する事になり、
矛盾が生ずる。
４自然数の集合が持つ全ての元の個数（濃度）と、実数の集合が持つ全ての元の
個数（濃度）は異なる。

１の「実数の集合が持つ元をただ一つ指定する」、は選択公理なしで行えますか？
また
１の「自然数の集合が持つ元から」、という部分は、つまり自然数の集合が持つ
ただ一つの元からという事でしょうか（もし自然数の二つの元から指定していたら、
そのうちの一つによって実数の集合が持たない実数も指定できてしまうから）。
この場合、これは選択公理なしで行えますか？
621 名前：１３２人目の素数さん mailto:sage [2011/12/05(月) 18:30:24.42 ]: 自然数と実数に1対1対応できないと言う証明、
>>620 証明を見直してもらうといいが、
選択公理なしに具体的な関数がつくれればいいわけ。
自然数の対角線論法なら選択関数はいらない。
ついでに、
集合とそのべき集合の濃度がちがうことは選択公理なしに証明できる。
（カントールベルンシュタインの定理）
基数にしてもきちんと公理的集合論の教科書のほうがやさしく書いてあるのに。
622 名前：613 mailto:sage [2011/12/05(月) 18:53:32.78 ]: >>621
回答ありがとうございます。
＞具体的な関数がつくれればいい
ふむ、、自然数と実数なら単純にf(x)=xと考えられるからと言う事でしょうか？
あんまり多分野の数学を知らないので　（a,b)　←関数によってこの形に（一意に）
出来ない集合同士というのがいまいちピンと来ないのですが、集合にも色々あるん
ですね。

＞きちんと公理的集合論の教科書
教科書選びは難しいですね。。
623 名前：１３２人目の素数さん mailto:sage [2011/12/05(月) 19:04:59.68 ]: >>620
613もそうなんだけど、ちょっと何言ってるか分かんない

あと「集合への30講」はちょっと古い本で、
集合論の入門書として必ずしもいい本ではないので注意した方が良い。
というかそれ以前に数学の文章のまともな書き方を勉強した方が良い。
624 名前：１３２人目の素数さん [2011/12/05(月) 23:23:39.39 ]: たびたび質問してすみません。
Boolosの『THE LOGIC OF PROVABILITY』をお持ちの方に質問です。

pp.37のFinSeqという論理式の定義

: ヨa<s ヨb<s ヨk<s (s = pair(pair(a,b),k)) ∧ ∀c<s ∀d<s (pair(c,d)<pair(a,b)→ヨi<k β(c,d,i)≠β(a,b,i))

において、∧以降の定義の意味がよくわかりません。
場合によっては、(pair(c,d)<pair(a,b) かつ ¬ヨi<k β(c,d,i)≠β(a,b,i)) もありうるため、このような定義をしているのでしょうか？
よろしくお願いいたします。
625 名前：１３２人目の素数さん [2011/12/05(月) 23:59:57.03 ]: >>624
しょうもないツッコミを入れるが、お前p.とpp.の使い分けの意味わかってないだろ
626 名前：１３２人目の素数さん [2011/12/06(火) 00:09:09.82 ]: >>625
わかってません・・・
ちょっとかっこつけて書きたかったんです。
627 名前：１３２人目の素数さん [2011/12/06(火) 00:17:05.39 ]: ページをまたがるときは、pp. なんですね。
628 名前：１３２人目の素数さん [2011/12/06(火) 00:24:54.73 ]: https://svn.kwarc.info/repos/kwarc/doc/macros/fromCTAN/cv/currvita/currvita.sty
629 名前：１３２人目の素数さん mailto:sage [2011/12/06(火) 23:04:28.35 ]: ～広めてください。

▼スイス政府国民保護庁　著「民間防衛」(civil defense)

武力を使わずに他国を侵略する段階を説明しています。
マスコミは乗っ取りがほぼ完了しており機能していません。。クチコミでも身近な人に広めましょう。
日本は今、侵略されつつあります。平和ボケから目覚め、行動を起こしましょう！

現在第五段階です。

ＴＰＰ・日中韓ＦＴＡ・人権擁護法・外国人参政権　などが実現してしまえば最終段階が始ってしまいます。
猶予がありません。声を挙げて下さい！

第一段階「工作員を送り込み、政府上層部の掌握と洗脳」
第二段階「宣伝。メディアの掌握。大衆の扇動。無意識の誘導」
第三段階「教育の掌握。国家意識の破壊」
第四段階「抵抗意識の破壊。平和や人類愛をプロパガンダとして利用」
第五段階「教育やメディアを利用して、自分で考える力を奪う」

最終段階「国民が無抵抗で腑抜けになった時、大量移住で侵略完了」
630 名前：１３２人目の素数さん mailto:sage [2011/12/06(火) 23:11:52.60 ]: ↑
他はともかく、ＴＰＰが何でそこに入っているの？ｗ
オマエも何らかの利害関係者じゃん
631 名前：１３２人目の素数さん [2011/12/06(火) 23:30:58.11 ]: >>602
ゲーデル数のデコード関数定義にどうしても冪関数が必要になります。
>>605
コーディング上の爽快感と意味論は無関係だと思いますよ。
表示的意味論はドメインに重視した考えですし、
意味関数でユニークに決定するという安定さがあります。
しかしλ計算ならまだそれでいいとしても、
π計算やλμ計算だとか高階χ計算みたいな
逐次から並列や分散へ進んだ体系では操作的であるほうが見通しても良くなるでしょうね。
一方公理的意味論(ホア論理)はプログラムで検証する意図があったみたいですが...。
>>624
例えば有限列ってのがアルファベットの
A,B,C,...Zだとして、(A,0)の対をBなどと考えてみる。
Z＝(((...(A,0)...),21),22)　のように22ステップでZに到達するイメージ。
ここで(a,b)がZより小さい、例えば((...(A,0)...),21)なんかだとすると、
(c,d)がそれより小さい、例えば((...(A,0)...),20)だとする。
このとき、β(x,y,i)でxとyで決まる列のiステップ目のアルファベットがユニークにでる。
β((...(A,0)...),21,0)＝A
β((...(A,0)...),20,0)＝A
のように、A,B,C,...とやっていける。しかし途中で、
β((...(A,0)...),21,21)＝Y
β((...(A,0)...),20,21)＝？
のように存在しないステップが出現するはずですよね...。
632 名前：スレタイスレ446 mailto:sage [2011/12/06(火) 23:33:57.85 ]: >>631
補足：ちなみに(A,0)はpair(A,0)の略記なだけなので。
そして実際はβ関数で出てくるのはゲーデル数です。
633 名前：１３２人目の素数さん [2011/12/07(水) 10:27:38.77 ]: >>631
>コーディング上の爽快感と意味論は無関係だと思いますよ。
あそこの「爽快感」とは，表示的意味論によってどのような「目からウロコ
感」があるかというような意味でした．
>逐次から並列や分散へ進んだ体系では操作的であるほうが見通しても良くなるでしょうね。
その方がやりやすいだけ（あるいは単なる退却）なのではないですか？
むしろ並列＆分散体系に対してこそ表示的意味論の意義が鮮明になると思います．
なお「操作的」や「公理的」に「意味論」は似合わないです．
（最後の３行は分かりにくいでしょうか？）
634 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 12:19:12.81 ]: 操作的意味論は、他の機械への写像を考えて、相対的に意味を検討する意味論。
ヒルベルトが幾何学の無矛盾性を算術の無矛盾性に還元したのと同じ手法。
だからモデル理論的手法を使うことが出来る。
こういうものに意味がないと思う人は数学は向いてない。
直感でしか理解したくないのなら数学は必要ない。
635 名前：１３２人目の素数さん [2011/12/07(水) 13:10:46.45 ]: >>634
>操作的意味論は、他の機械への写像を考えて、相対的に意味を検討する意味論。
機械が出てくる時点で数学（ヒルベルトの手法）からは遠い。
>だからモデル理論的手法を使うことが出来る。
だからって？操作的意味論はそういうものだから、ってこと？
>こういうものに意味がないと思う人は数学は向いてない。
こういうものって？けっこう特定したうえでその意味が不明と言って
いるのだが。それに今は「数学」はどうでもよいし。
636 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 14:31:00.45 ]: 抽象機械のことでしょ。
状態遷移マシンとかラムダ式とか。
637 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 14:37:24.44 ]: >>631
ベキ関数無しのコーディングは可能だそうだ
代わりにBussの#関数を使う（Edward Nelsonの本で知った）
638 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 15:24:11.98 ]: 元の質問者の読んでる新井さんの本も使ってないんじゃない？
639 名前：１３２人目の素数さん [2011/12/07(水) 17:57:45.02 ]: >>636
ラムダ式まで抽象機械とは言わんだろ
640 名前：１３２人目の素数さん [2011/12/07(水) 19:35:21.68 ]: >>637
> Edward Nelsonの本で知った

彼の何というタイトルの本ですか？
Edward Nelsonの本で数理論理学関連と言えばPredicative Arithmeticぐらいしか思い付かないのですが（不勉強なもので、それも読んでいません）。
641 名前：スレタイスレ446 [2011/12/07(水) 21:06:19.80 ]: >>633
> >逐次から並列や分散へ進んだ体系では操作的であるほうが見通しても良くなるでしょうね。
> その方がやりやすいだけ（あるいは単なる退却）なのではないですか？
やりやすいということですね。
>>587のUnbounded nondeterminism に関連して、
表示的意味論は並列性などの解釈とするのが困難だという趣旨の定理もあります。
とはいえ、表示的が不可能なわけでないので退却というほどでも。
> むしろ並列＆分散体系に対してこそ表示的意味論の意義が鮮明になると思います．
これは詳しくききたいですね。
> なお「操作的」や「公理的」に「意味論」は似合わないです．
これはどういったことなのか分かりませんでした。

>>634
モデル論的手法が何かはわかりませんが、
シェラとかのモデル理論が使えるのは表示的意味論の方だと思いますが。
数学は形式的には時間の流れがまったく考慮されない逐次的処理という特徴があって、
計算機とは時間の流れが議論に混入するという理解が一般的だと思っていましたが。

>>635
機械で計算するかは余り関係ないと思いますけどね。
ま、チャーチの提唱次第ですかね。

>>637
全く知りませんでした、書名が知りたいですね。

>>638
exp関数なんかの定義に使われていると思います、計算理論入門の章ですね。
642 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 21:07:02.49 ]: BussのBounded Arithmeticにも.
x#y = 2^(|x|・|y|)
643 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 21:09:01.79 ]: ちなみに竹内さんの日本語の書籍にも出てきたはず。
644 名前：スレタイスレ446 [2011/12/07(水) 21:48:57.88 ]: 限定算術周辺は盲点だった。
しかし定義上冪と似たような性質が用いられている気もするけど。
実際エンコード方法はいくつもあるんだろうな...。
645 名前：１３２人目の素数さん mailto:sage [2011/12/07(水) 22:52:37.72 ]: 最低x^log(y)くらいの演算がないとgodel numberingがうまくいかない。
冪相当のものがないとまずいのは40年くらい前から分かってきていた。
Bounded Arith.の人たちはこんな事ばっかり考えてるから。
646 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 05:22:04.87 ]: スマッシュ関数の定義可能性を保証する公理は \Omega_1 と呼ばれるが、
I\Delta_0 + \Omega_1 は Robinson's Q で解釈可能（Hajek-Pudlak などを参照）。
つまりこの解釈を通せば、ゲーデル数化は Robinson's Q においても可能、ということ。
647 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 14:12:12.58 ]: もし自己言及のパラドクス、嘘つきのパラドクスがパラドクスじゃなかったら

それでも不完全性定理は証明されるの？

これ、どなたか教えてください。お願いします。もしスレ違いならすいません（´；ω；`)
648 名前：１３２人目の素数さん [2011/12/08(木) 14:50:29.19 ]: >>647
おもしろそうな質問だが，これだけでは意味不明と思う．
形式的に答えるなら，少なくとも，不完全性定理の証明には，そういうパラド
クスの存在はまったく前提とされていない，ということになるからね．
他の人のコメントも見てみて．
649 名前：647 mailto:sage [2011/12/08(木) 15:06:27.52 ]: ありがとうございます。。

＞もし自己言及のパラドクス、嘘つきのパラドクスがパラドクスじゃなかったら

やっぱり、ここの部分がしっかり定義されていないというコトですか？

ちょっと調べてきます。。
650 名前：スレタイスレ446 [2011/12/08(木) 20:58:21.54 ]: >>646
その考えでいくと他にもいろいろな関数ができそうですね...。
>>647
自己言及のパラドクスは不完全性定理の証明でよく見られますね。
自己言及のパラドクスは定義されているわけでなく、
それに類似した現象を指示する慣用句です。
第1不完全性定理は自己言及パラドクスのようなものとは無縁にも証明可能です。
実は最近、マルチエージェントについて考えていた際に、
不完全性定理の証明について自己言及のパラドクスなどの特定の解釈をすると
不自然なことに気が付きました...これは哲学的な問題ですが。
651 名前：１３２人目の素数さん [2011/12/08(木) 21:48:07.98 ]: >>650
>不完全性定理の証明について自己言及のパラドクスなどの特定の解釈をすると不自然
これもうすこし聞かせてほしいな。もし可能なら
652 名前：１３２人目の素数さん [2011/12/08(木) 23:06:21.79 ]: >>647
648、650が言うのでよいと思うが、647が言いたかったのが
「嘘つきのパラドクスと不完全性定理（第一）とは同一内容である；
後者は前者を厳密に形式化したものに相当する」ということであれば
（とてもそうは読めないが）、それはその通りだと思う。
フランセーンがどう言うか知らんが。
653 名前：１３２人目の素数さん [2011/12/08(木) 23:11:41.26 ]: クレタ人のパラドックスもベリーのパラドックスも死刑囚のパラドックスも不完全性定理の証明に使えるなら、禿頭のパラドックスも使えないかな。
654 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 23:21:11.51 ]: 確かに嘘つきパラドクスと不完全性定理は確かに似ているけど、
通俗的解説書しか読んだことない人にとっては
類似点よりも相違点を理解する方がずっと大切だと思ってください。

嘘つきパラドクスも不完全性も同じなんだ！
とアナロジーで物事を語る入門者の大半はとんでもないことを言ってます。
655 名前：１３２人目の素数さん [2011/12/08(木) 23:22:46.69 ]: >>653
くどいのだが、そうしたなんとかパラドックスが「不完全性定理の証明
に使われている」ということはないよね。
656 名前：647 mailto:sage [2011/12/08(木) 23:23:07.06 ]: 答えて下さった方々、ありがとうございます。。
>>652
＞「嘘つきのパラドクスと不完全性定理（第一）とは同一内容である；
＞後者は前者を厳密に形式化したものに相当する」ということであれば

ようするに聞きたかったのは、このとうりです。
もし哲学の現場で「嘘つきのパラドクス」がパラドクスでも何でもない、勘違いだったとなれば、
不完全性定理は、それでも証明されるのか、という事です。

僕も>>650さんの哲学的な問題…という所、聞いてみたいです。。
657 名前：１３２人目の素数さん mailto:sage [2011/12/08(木) 23:30:13.21 ]: まあdiagramはほとんど同じ形だけどな。
658 名前：１３２人目の素数さん [2011/12/09(金) 01:01:21.60 ]: >>655
フナクイムシがシールド工法の開発に果たした役割くらいはあると思う
659 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 06:37:08.51 ]: >>650
例えばタワー関数は出てこない。
I\Delta_0 にタワー関数の定義可能性を加えた体系では
Robinson's Q の無矛盾性が証明できてしまうので、
不完全性定理により、その体系を Q で解釈することは出来ない。
冪も出てこないということは Hajek-Pudlak に書いてある。
この方法ではスマッシュ関数の入れ子くらいが限界。
それでもゲーデル数化に充分ってところが味噌。
660 名前：１３２人目の素数さん [2011/12/09(金) 09:18:27.66 ]: >>656
不完全性定理は、そんな勘違いがあろうがなかろうが、成立します。
それから、そのような考察をするなら、「パラドックス」という言葉
を極力形式的に定義しておくべきと思います（既知の定義もありますし）。
661 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 22:11:37.02 ]: ゲーデルが論文で挙げてるのはどっちかというと
嘘つきパラドックスじゃなくてリシャールのパラドックスじゃなかったっけ。

嘘つきパラドックスと不完全性定理にはいくつか大きな違いがあって、
まず前者では命題の真偽そのものについて述べているのに対し、
後者は命題の証明可能性についての話です。
前者を形式化したタルスキーの定理では、
「そのような述語は存在できない」という結論になるのに対し、
後者ではそのような命題があっても矛盾せず、それは証明できない命題となります。
但し存在しても矛盾しないというだけで、実際に
証明可能性述語が存在するかどうかは別問題なので、
不完全性定理を勉強するときはかなり手間をかけて
実際にそのような述語を作ることになります。
662 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 22:11:58.22 ]: 次に嘘つきパラドックスは直接に自分自身の真偽について言及していますが、
不完全性定理で出てくる文章は、直接的には
自然数を足したり掛けたりしたら等しくなるというような命題です。
それが結果的に自分自身が証明できないということと同値になります。

最後に、哲学で出て来るこの種のパラドックスでは
「この文は」というような意味のはっきりしない指示語などが使われているので、
数学者に言わせれば、
日常言語のような曖昧な言葉を使うのが悪いんだよ、ということになります。
不完全性定理では上で見たように自然数の足し算掛け算について
述べているだけの命題なのでそういうことはありません。
663 名前：１３２人目の素数さん mailto:sage [2011/12/09(金) 22:30:39.29 ]: いやいや哲学方面も厳密な議論してるよ。
Strong Lier Paradoxってのが、
カントールの定理やTuringマシンの停止問題と同型。
圏論の図式レベルまで単純化すると第一不完全性定理も同型。
664 名前：１３２人目の素数さん [2011/12/09(金) 23:41:57.72 ]: おまいら頭悪いなｗ
kamome.2ch.net/test/read.cgi/psycho/1284396792/364-370
665 名前：１３２人目の素数さん [2011/12/10(土) 02:54:55.58 ]: いまだに第二不完全性定理の証明に必要な導出性条件の証明ができない。
ここの住人はどうやって理解したんだろうか。
666 名前：１３２人目の素数さん mailto:sage [2011/12/10(土) 08:44:44.06 ]: 論文読め
667 名前：スレタイスレ446 [2011/12/10(土) 09:38:44.80 ]: >>651 >>656
不自然な点とは第2不完全性定理なんですが、
大雑把にいえば、モデルを持つ理論が、自らのモデルについては言及できないという言明について、
その条件がモデルを持つことであるために、自己言及できていないのでは？という趣旨です。
当初は単一の世界での不完全性定理を考えていて気が付かないかったのですが、
複数の世界でエージェントの信念や知識を考慮すると不自然なんです。
自己言及のパラドクス的なモノをまだ知らない状況、というものが考えられるなど...。
この考えはまだまとまっていませんが。
>>659
どうも、無料なうえに良書ですね。
>>661
それらをまとめると、タルスキの定理は、
すべての論理式φで、N|=φ←→R(【φ】)なので、
⇔すべての論理式φで、PA∪{φ←→R(【φ】)}|-φ←→R(【φ】)
だからゲーデル文ψでPA∪{ψ←→R(【ψ】)}|-ψ←→￢R(【ψ】)となり、
真偽判定は第1不完全性定理の証明判定の別モードと解釈もできますよね。
つまりそれぞれ自己言及パラドクス（ゲーデル文）が源泉。
ま、実は第1は自己言及も可証性述語も一切必要なしに証明できるんですが。
>>663
同型とは何でしょうか。
668 名前：１３２人目の素数さん [2011/12/10(土) 10:46:36.38 ]: >>667
>不自然な点とは第2不完全性定理なんですが、
ここのパラグラフまだよくわからないのですが，なんとなくおもしろそうですね．
まとまったら解説をよろしく．
以下は私の中での不明点．もちろんコメントいただく必要はありません．
>理論が、自らのモデルについては言及できない
直感的には，これは理論の宿命ではないのだろうか？
>その条件がモデルを持つことであるために、自己言及できていないのでは？
これを文字通りに解釈すると｢その理論が無矛盾であるために自己言及できて
いない｣という意味になるが，それはナンセンスではないか
だが，こう考えることがそもそも「単一の世界」に捉われているということなのか？
669 名前：１３２人目の素数さん [2011/12/10(土) 10:50:28.68 ]: 世界とかエージェントとかは様相論理の話だと思われる
670 名前：１３２人目の素数さん [2011/12/10(土) 12:14:47.43 ]: >>669
それはそうなのだが
671 名前：スレタイスレ446 [2011/12/10(土) 17:08:19.79 ]: >>667
訂正：
タルスキの定理は正確には、
すべての論理式φで、N|=φ←→R(【φ】)となる述語Rが存在しない。ですね。
>>668
基本的には理論自体のモデルと、その理論から証明される言明中の支持するモデルが同一かどうか考えていますね。
あくまで哲学的な意味でですが。
672 名前：１３２人目の素数さん [2011/12/10(土) 18:43:34.43 ]: >>671
ここでいう「モデル」って、たとえば完全性（無矛盾<->モデルの存在）
などの文脈で使われる「モデル」と思っていいのですよね？（それとも別の意味？）
673 名前：スレタイスレ446 mailto:sage [2011/12/10(土) 23:33:12.77 ]: そのモデルです。
674 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:29:22.34 ]: ツォルンの補題を用いて
「Aが無矛盾→Aはモデルを持つ」の証明を教えてください
お願いします
675 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:36:12.67 ]: 教科書嫁
676 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:40:42.60 ]: 教科書ないんです
調べてやれって言われました・・・
677 名前：１３２人目の素数さん mailto:sage [2011/12/11(日) 23:46:50.90 ]: 図書館池
678 名前：１３２人目の素数さん [2011/12/11(日) 23:50:48.14 ]: フランセーンが「ＰＡの超準モデルの存在は不完全性とまったく無関係」と
書いているのだが、これはちょっと言い過ぎでないかい？
679 名前：１３２人目の素数さん [2011/12/12(月) 04:18:24.46 ]: 「任意の自然数 i,j について、i+j=k のとき、PAで ”i+j=k” が証明可
能である」
これはjに関する数学的帰納法で証明できる。

とあるのですが、どうしてjだけでよくて、iやkについては考慮しないで良いのでしょうか？
1変数の述語に関しての数学的帰納法はよく分かるのですが、複数変数の述語に関しての
数学的帰納法がよく分かりません。

初歩的な質問ですみません。
680 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 04:53:38.89 ]: >>679
jについて、任意の自然数iに対して或る自然数kが存在してi+j=k
を仮定し、自然数iを任意に固定して1を右から足すだけ。
あとはiを動かして終わり。
681 名前：１３２人目の素数さん [2011/12/12(月) 06:03:53.48 ]: jに関する数学的帰納法で証明できるというだけで、iやkを考慮しなくていいなんて書いてないだろ？
やりたければiやkに関する帰納法でも出来るんじゃない？どういう公理を採用しているのか知らないけど。
682 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 06:40:24.97 ]: >>681
任意の自然数i、jについて、i、jを固定したならペアノの公理からi+j=kも自然数であることが示せるから、jやkは考えなくてよい訳で
「任意の自然数 i,j について、i+j=k のとき、PAで ”i+j=k” が証明可能である」
の「任意の自然数 i,j について、i+j=k」は「任意の自然数 i,j に対してある自然数が存在してi+j=k」と解釈した訳だが。
>>679の文についてこの解釈が間違っているのか？
683 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 06:42:49.32 ]: 間違ってる
684 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 06:53:51.33 ]: >>683
>>679の文章をどう解釈すればよかったのか分からない。
685 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 07:00:32.23 ]: 「任意の自然数 i,j,k について、i+j=k のとき、PAで ”i+j=k” が証明可能である」の間違いだろ。
もしくは「任意の自然数 i,j について、自然数 k が存在して、PAで ”i+j=k” が証明可能である」でも同じことだが。
i,j に対して i+j=k となる k が存在することは小学生でも知っている自明な話。
686 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 07:49:04.82 ]: >>685
i+j=kを満たす任意の自然数i、jについて、PAで ”i+j=k” が証明可能である
を示すのか。
ペアノの公理を公理として認める限り、これはトートロジーだろう。
687 名前：１３２人目の素数さん [2011/12/12(月) 10:45:55.80 ]: 「任意の自然数 ,j について、1+j=k のとき、PAで ”1+j=k” が証明可
能である」
「任意の自然数 ,j について、2+j=k のとき、PAで ”2+j=k” が証明可
能である」
「任意の自然数 j について、3+j=k のとき、PAで ”3+j=k” が証明可
能である」
…

この無限個の命題を数学的帰納法で証明できる、ということでしょ
688 名前：１３２人目の素数さん mailto:sage [2011/12/12(月) 11:16:16.25 ]: i+0=kに帰結させて、次はi=kであることを示す。
これには数学的帰納法は必要ない。ただし、
S(i')=S(k')と帰納的に0=0に帰結させる。
jを選ぶかどうかは証明したい人の勝手。
689 名前：検便のナウシカ ◆UVkh7uHFoI [2011/12/12(月) 19:21:09.48 ]: てｓｔ
690 名前：スレタイスレ446 [2011/12/13(火) 00:37:14.98 ]: >>674
それは完全性定理。
ツォルン使うところだけ言うと、
無矛盾な文の集合の族に、包含関係で順序を入れる。
任意に整列した部分集合をとれば有界になってるから、
この族は極大元をもつ。
こいつにAと共に無矛盾性を保つ文がすべて入ってるから、
こいつの解釈を定義すると...。
>>678
どういった文脈でしょうか...。
>>679
仮定の方のi+j=kは、経験的な意味での足し算。
＞PAで ”i+j=k” が証明可能である
こっちはS(S(...S(0)...))のような形をしているが、
i,j,kは数項と呼ばれるメタ変数による略記だと思う。
普通はiかjの片方を任意固定して帰納法を使う。
片方固定しているから、もう片方の選び方で
ユニークにkが決まるということがi+j=k という仮定から出る。
この帰納法が第二不完全性定理がPA以上であることとつながる。
691 名前：624 [2011/12/13(火) 02:26:39.96 ]: >>631
レス遅くなりましたが、解説ありがとうございます。おかげで疑問点は解消できました。

もう1つ質問させて下さい。（何度もすみません）
このスレでも何度か書いていますが、私はどうしてもLoebの可導性条件、特に
D3　PA|- Pr([A])→Pr([Pr([A])])
の証明が理解できません。

以下、私がどこまで理解しているかを簡単に書きます。
D3を証明するためには、任意のΣ1文Fに対して、
PA|- F→Pr([F])
が証明できればよく、そのためにはFの構成に関する帰納法で証明すればよいわけですよね。
つまり、以下の１から４の順番で証明すればよいと。

１、F ⇔ x=y, 0=x, Sx=y, x+y=z, x・y=z　のとき、PA|- F→Pr([F])
２、F ⇔ G∧Hのとき、PA|- F→Pr([F])
３、F ⇔ ∃xG(x)のとき、PA|- F→Pr([F])
４、F ⇔ ∀x<y G(x)のとき、PA|- F→Pr([F])

以上の１以降が理解できなく困っています。たとえば、
PA|- x+y=z→Pr([x+y→z])
はどのようにして証明すればよいのでしょうか。
文献[1]には、これの証明が載っているのですが私にはよく理解できませんでした。

使用している文献は
[1]　Boolos「THE LOGIC OF PROVABILITY」
[2]　田中他「数学基礎論講義」
の2冊です。

長くなりましたが、どうぞよろしくお願いします。
692 名前：624 [2011/12/13(火) 02:31:02.51 ]: 追記

文献[2]には、D3の証明は膨大な量になるので、これを書き下すのは実際にはかなり困難な作業とあります。
一方、文献[1]には（多少の省略はあるものの）D3の証明を最後まで書いているように思われます。
やはり私がしっかり読めていないだけで、文献[1]も大幅に証明を省略しているのでしょうか？
693 名前：624 [2011/12/13(火) 02:34:07.71 ]: >>691の
PA|- x+y=z→Pr([x+y→z])
は
PA|- x+y=z→Pr([x+y=z])
の間違いです。失礼しました。
694 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 03:14:10.12 ]: >>690
＞この帰納法が第二不完全性定理がPA以上であることとつながる。
少し前で、第二不完全性定理はPAより遥かに弱い体系でも成り立つ、って話が出ているのにもかかわらずこの発言ｗ
695 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 06:15:56.94 ]: >>691
当り前だが、２は帰納法の条件が抜けている。693 では x+y=z
から y=0 の場合、z=x そうでない場合 x+(y-1) = z-1 が導かれる
といったことに気づくことが必要。
696 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 06:21:31.04 ]: >>646 で述べられているやり方により、
冪もスマッシュ関数もないロビンソンのQでも第二不完全性定理は成り立つ。
しかし積は必要で、積もないプレスバーガー算術では第二不完全性定理が成り立たないのは有名な話。
697 名前：スレタイスレ446 [2011/12/13(火) 08:13:28.50 ]: >>694 >>696
例の文脈で言ってたのはゲーデル数化ですよね。
ところでQでは零元との加算の交換法則さえ成り立たないですよね。
PAよりもQの方がはるかに証明可能な論理式が少ないと予想できます。
ところで第一の証明の際に結構数学的帰納法を多用しますよね？
その証明を形式化した第二の可証性述語を証明するのに、
帰納法の公理が一切不要であるということは証明されているのでしょうか？
プレスバーガーにも帰納法は入ってますし。
それとも別の方法があるということでしょうか？
698 名前：１３２人目の素数さん mailto:sage [2011/12/13(火) 17:01:02.16 ]: >>697
帰納法もゲーデル数化も扱いは同じだよ。
Qは直接は帰納法を持っていないけど、>>646でいうように
「解釈された帰納法」は持っているので、それで充分。
699 名前：１３２人目の素数さん [2011/12/14(水) 00:18:55.11 ]: >>647 >>650 >>651 >>656 >>667
不完全性定理と自己言及のパラドクスはかなり異なる。
まず第一不完全性定理の証明にゲーデル文などは必須ではないことに注意。
1階述語論理の充足不能判定性問題の決定不可能性が容易に証明可能だが、
このときロビンソン算術の不完全性は、
後続者関数の単射性と0の非後続者性と前者の存在性に関する3つの公理だけで証明可能。
3つを∧でつなげて存在例化したのをAとする。
するとAの任意モデルは標準モデルと同型になる。
さらに文φをある一項述語に相対化してすべての関数述語定数を存在例化したものをφ*とすると、
φ*は一項述語をドメインとするモデルであるかに依存して真偽が決定する。
このテクニックで任意のφについて、
φが決定不能⇔”Aが真ならばφ*が真である”ことが決定不能。
として第一不完全性定理が成り立つ。
また第二不完全性定理については、自らの無矛盾性証明ができないだが、
T|-⊥→φなので、T|-Pr(⊥)→Pr(φ)とT|-/-￢Pr(⊥)からT|-/-￢Pr(φ)がでて、
そもそも任意の論理式が証明できないことが証明できない、
第二不完全性定理はこれの系と言える。
さらにこれらが解を持たないある種の不定方程式と同値であることと、
ほとんどの次数と変数の不定方程式が決定不能なことを考えると、
真でありながら証明可能な論理式は、ほんのわずかしかない。
700 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 04:05:35.73 ]: >後続者関数の単射性と0の非後続者性と前者の存在性に関する3つの公理だけで証明可能。
>3つを∧でつなげて存在例化したのをAとする。
>するとAの任意モデルは標準モデルと同型になる。
ほほぅ、それは世紀の大発見ですな。
701 名前：１３２人目の素数さん [2011/12/14(水) 04:33:52.08 ]: 集合論は完成された学問ですか？
まだ進化し続けているのでしょうか？
日本人で集合論を専門にしている方はいますか？
702 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 04:57:56.30 ]: Mitchellのアーベル圏充満埋め込み定理の読みやすい証明の有る本教えれ。
703 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 05:26:12.73 ]: >>701
一般人が「集合論」という名称から想像する学問内容と、
研究現場で「集合論」と呼ばれる研究内容は必ずしも一致しないことも多い。
どのような研究内容を想像しているのか？
704 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 06:44:06.79 ]: スレタイスレ446君は偉そうなこと言う割に、不完全性定理っていう基本的な事実については余りに無知なんだね。
不完全性定理の為の条件である「ある程度の算術を含み、かくかくしかじかの性質を満たす公理系」の内、
「かくかくしかじか」の部分は得意気に解説しているブログはよく目にするが、
最初の「ある程度の算術を含み」がどういうことなのか理解が浅い連中が多い。
PAほど強い必要は全然ないし、それよりも「含む」という部分が曲者。
狭い意味で考えてしまうと、ZFC 集合論と算術は言語が違うのだから算術を含んでいないことになってしまい、
ZFC 集合論には不完全性定理が適用できないことになってしまう。
705 名前：１３２人目の素数さん [2011/12/14(水) 08:06:23.57 ]: >>700
前者の存在性に関する公理から任意の論理式φについて、
φ(z)∧∀x(φ(x)→φ(f(x)))→∀xφ(x)
の形の文が出現、これを2階述語論理で量化した
∀φ(φ(z)∧∀x(φ(x)→φ(f(x)))→∀xφ(x))
と「後続者関数の単射性」と「0の非後続者性」は範疇的で
何れもω_0のドメインを持つ。このことから、
”1階の文φ”が決定不能⇔”2階の文Aが真ならばφ*が真である”が決定不能。
706 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 12:41:59.00 ]: >>705
2階述語論理で量化...?
707 名前：スレタイスレ446 [2011/12/14(水) 18:53:08.34 ]: >>704
>>690でPA以上といったことについてならば、
私は>>679のレスポンスを見て、第一不完全性定理の証明を形式化して
第二不完全性定理を証明しようとしていると予想したんですね。
だから第一の条件がQになるのに対し第二がPAになっている理由を述べたわけです。
PAよりも単純な体系でも証明できるのでしょうが、
例の限定算術についてはほとんど知らないので、
数学的帰納法位は必要なんじゃないだろうか、と考えた末のレスポンスが>>697なわけです。
708 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 20:23:27.08 ]: ただ、普通の数学者にとってみれば、
Peano算術をどれだけ弱く出来るかとかそういうことは
専門家のみが興味を持つどうでもいいことなので、
だからこそ指数関数を最初から加えて証明を簡略化したりする
709 名前：１３２人目の素数さん [2011/12/14(水) 20:52:04.65 ]: さらに言えば、
再帰的クラスの決定問題については、
去年、Rendellによって構築されたライフゲームの万能チューリング機械により、
ttp://uncomp.uwe.ac.uk/CAAA2011/Program_files/764-772.pdf
すべてエデンの園に帰着できることが証明されているので、
ttp://arxiv.org/PS_cache/arxiv/pdf/0709/0709.4280v1.pdf
これからは不完全性定理含め、Σ_1・Π_1階層の決定問題はすべて
セルオートマトン上で実行されながら研究が進む流れとなるだろう。
710 名前：１３２人目の素数さん mailto:sage [2011/12/14(水) 21:48:34.40 ]: >>706
正確にはあらゆる論理式に対して
述語定数を定義してから、その述語を量化する。
711 名前：１３２人目の素数さん [2011/12/16(金) 07:26:41.52 ]: >>702

Peter Freyd 著 abelian categories
712 名前：１３２人目の素数さん [2011/12/17(土) 01:52:21.32 ]: 記号論理学ってここに入りますか？

[ 新着レスの取得/表示 (agate) ] / [ 携帯版 ]

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