- 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/
- 2 名前：１３２人目の素数さん [2011/10/29(土) 22:58:12.73 ]
- king.
- 3 名前：１３２人目の素数さん [2011/10/29(土) 23:07:02.01 ]
- king.
- 4 名前：１３２人目の素数さん mailto:sage [2011/10/29(土) 23:08:15.09 ]
- やっちまったな
- 5 名前：１３２人目の素数さん mailto:sage [2011/10/29(土) 23:27:39.24 ]
- iup.2ch-library.com/i/i0461635-1319883402.jpg
- 6 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 03:40:17.06 ]
- このスレタイが基地外の色がなくて常識的。このままでよい。
- 7 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 05:56:52.63 ]
- つーか、いくら議論しても反論になってない反論（しかも毎回同じ内容）ばかりで
この先いつまで議論しても噛み合うようには思えない。
このスレタイで嫌だって奴だけで別のスレッドに移行すればいいんでない？
板の分割とかもあるわけだから、スレッドを二つに分けても問題ないでしょ。
新しいスレッドは基地外だらけになりそうだがなｗ
- 8 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 08:18:03.13 ]
- ＞997 名前：１３２人目の素数さん[sage] 投稿日：2011/10/29(土) 11:23:35.35
＞完全性定理の内容って
＞「理論が無矛盾ならモデルが存在する」（ただしこのモデルは超越的方法で作られる）
＞で、これから
＞ Aがどんなモデルでも真
＞ → ￢Aを満たすモデルは存在しない ①
＞ → もし超越的な方法を許したとしても￢Aのモデルは存在しない ②
＞ → ￢Aを仮定すると理論が矛盾する //定理の対偶
＞ → Aは証明可能
＞が成り立つってことだけど、
＞超越的な方法を認めない場合でも②は有効と言えるんだろうか？
超越的だか何だかは関係ない。
極大無矛盾集合の証明で論理式を並べているので
完全性定理の証明を形式化したとき論理式に選択公理が入ってるってこと。
- 9 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 09:46:50.40 ]
- 数学基礎論、数理論理学は数学ではなく、
論理学なのだから、哲学板か、情報学板へ
言った方が良いよ。
- 10 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 10:04:58.75 ]
- >>8
「論理式に選択公理が入ってる」って日本語がわからん。
完全性定理だけは1階述語論理一般で普遍的に成り立ってくれなければ
困るので、弱ケーニヒだかの超越的な手法を使えない。
- 11 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 10:13:59.80 ]
- >>9
数学基礎論、数理論理学が数学か否かについては
本スレッドではなく別途、スレッドを立てて
そこで議論していただくことを強く勧める。
- 12 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 10:19:33.13 ]
- >>10
一階述語論理の完全性定理は、一階述語論理上の定理ではなく
集合論（もしくは二階算術）の定理である。
逆数学においては弱いケーニヒの補題が成立するＷＫＬという
２階算術の体系で成立することが知られている、ということ。
とはいえ、本来はモデルを考えるのに、集合論を前提している。
- 13 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 10:35:18.10 ]
- 「任意のモデルでAが成り立つ。よってAは定理(証明が存在する)」
という証明の手法は い つ で も 使える。これが完全性定理じゃないの？
項、論理式、証明といった再帰的に定義された具体物の存在について言っているので、
「実は集合論の上の定理でした」じゃ困る。
- 14 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 10:37:15.31 ]
- 新スレがたったので、改めてこちらで質問させてもらいます。
「ゲーデル数xは、PAの項である」を再帰的に表す算術上の述語
はどのようにして定義すればよいのでしょうか。
- 15 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 10:41:31.14 ]
- >>12
とはいえモデルってものはそのユニバースを集合としているわけで、
決して「集合論なんて知りません」というスタンスではない。
集合論という理論の中で成立している特定の定理を、どうすれば具体物に適用できるのか、
正当化できるのか、という質問です。
- 16 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 11:01:53.49 ]
- 弱ケーニッヒ補題と1階論理の完全性定理の同値性はRCA0だけで書ける。
これは見かけ上の記述がRCA0でOKということ。
実際にこれらの同値性を証明する議論に
どういう体系(最低でも公理的集合論？)が必要かは
明確に述べられないと思う。
1階論理とその完全性定理をすべて公理的集合論(例えばZFC)で書いたとき、
完全性定理を意味する長大な論理式の中に、
選択公理から推論される何らかの論理式を使わなければ、
論理式を整列することはできないことは簡単に想像できる。
ところが論理式をゲーデル数化することで、この選択公理が不要になることもわかっている。
事実不完全性定理の対角定理で選択公理が不要なのはこの議論による。
- 17 名前：16 mailto:sage [2011/10/30(日) 11:04:25.55 ]
- ちなみに>>12とは別人（一応
- 18 名前：１３２人目の素数さん [2011/10/30(日) 11:32:19.55 ]
- 初等ダイアグラム使えばモデルなんて必要ないよ。
PA上での完全性定理は田中さんの本で多少触れられている。
- 19 名前：１３２人目の素数さん [2011/10/30(日) 12:03:48.40 ]
- >>14
例えば、
ゲーデル数xがPAの項に該当することをIsTerm(x)とすれば、
IsTerm(x)：xが0∨xが無限個の変数∨xが項を引数に持つ関数
で定義される。
- 20 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 12:08:31.63 ]
- 一般に、数学の定理は集合論の定理でも、自然数論の定理でもない。
当然、完全性定理も同じ。12 も 13 もおかしい。
完全性定理は、普通はモデルという集合概念を使って述べられている。
そのまま、PA の定理にはならない。大体、普通の完全性定理は集合論
の形式言語で書かれてさえいない。
- 21 名前：１３２人目の素数さん [2011/10/30(日) 12:26:27.48 ]
- あほめ
モデルも言語も両方形式化するんだよ
- 22 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 12:30:07.65 ]
- バカだね。
形式化というのは色々な選択しがある、そのことが不完全性定理のもと
であるのに、何のことわりもなく、そのようなことができると思って
いるのは、数理論理学をよくわかっていない証拠だ。
- 23 名前：１３２人目の素数さん [2011/10/30(日) 13:32:17.92 ]
- >>15
1階論理とかってのはコンセンサスなのでは？
現時点で代替的な手段がまったくないから。
数学に必要な論理的構造は1階論理でOK、というのは前提としてよいと思う。
数学の中には1階論理で記述不可能な命題もあるけれど、
それらは同値の命題に置き換えることで記述可能になっている。
また普通数学をやるときには素朴集合論の命題をミニマムな前提としてやるから、
素朴集合論の命題がすべて正当化できる論理なら間違いないと思う。
- 24 名前：12 mailto:sage [2011/10/30(日) 13:39:01.69 ]
- >>13
＞「任意のモデルでAが成り立つ。よってAは定理(証明が存在する)」
＞という証明の手法は い つ で も 使える。
＞これが完全性定理じゃないの？
２行目がおかしい。
理論Tにおいて、Aという命題を証明するのに
「理論Tの任意のモデルでAが成り立つ」
という方法は使えない。
例えばTがPAの場合とか。
- 25 名前：12 mailto:sage [2011/10/30(日) 13:45:22.21 ]
- >>16
＞弱ケーニッヒ補題と1階論理の完全性定理の同値性はRCA0だけで書ける。
＞これは見かけ上の記述がRCA0でOKということ。
RCA0は二階算術。つまり自然数の集合について記述できる。
「弱い集合論」と思えばいい。
一階算術では、自然数については記述できるが、
その集まりについては記述できない。
＞実際にこれらの同値性を証明する議論に
＞どういう体系(最低でも公理的集合論？)が必要かは
＞明確に述べられないと思う。
集合を扱える必要はある。ZFCである必要はないが。
- 26 名前：１３２人目の素数さん mailto:sage [2011/10/30(日) 13:48:56.22 ]
- 今のところ分かっていることは、
・PAでは組合せ論の命題ではみ出るのが結構ある。
・Z2では実解析や関数解析周辺ではみ出るのが結構ある。
・ZFCではゲイル・スチュワートの定理など無限ゲーム系命題がはみ出る。
・1階述語論理では書けず、しかも同値命題が発見されていないものあり。
・シェラーはZFC＝数学説指示。
・ZFCに様々な公理を付けると2^ω＝ω2となることが多い。
- 27 名前：12 mailto:sage [2011/10/30(日) 13:50:24.04 ]
- >>20
＞一般に、数学の定理は集合論の定理でも、
＞自然数論の定理でもない。
＞当然、完全性定理も同じ。
一般の数学者が、集合論を意識しないのは随意だが
大抵のものは集合論の定理となる。
完全性定理を記述する際には集合の概念が必要。
＞完全性定理は、普通はモデルという集合概念を
＞使って述べられている。
＞そのまま、PA の定理にはならない。
その通り。>>10は、ある理論Tの完全性定理は
Tもしくはそれより弱い理論の定理だと誤解
している。
- 28 名前：12 mailto:sage [2011/10/30(日) 13:56:59.90 ]
- >>15 >>23
モデルは、一階論理上では直接扱えないが。
少なくとも、集合を扱える理論が必要。
そのような理論を、一階論理上の公理系として
実現することはできるが。
- 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 □
|
 |
