数学基礎論・数理論理学のスレッド その7
■ このスレッドは過去ログ倉庫に格納されています
0001１３２人目の素数さん
2010/11/11(木) 22:13:5719世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
前スレ
数学基礎論・数理論理学のスレッド その6
http://kamome.2ch.net/test/read.cgi/math/1265884076/
0375368
2011/02/23(水) 21:10:09.87ジャクソンとショーアのlow basic theoremより
recursive degreeを下げることで不完全性定理は成り立たないようにできる！
0376１３２人目の素数さん
2011/02/23(水) 21:15:08.730377１３２人目の素数さん
2011/02/23(水) 21:27:56.540380１３２人目の素数さん
2011/02/23(水) 22:21:36.12It was first proposed by Skolem[1] as a formalization of his finitist conception of the foundations of arithmetic, and it is widely agreed that all reasoning of PRA is finitist.
0382１３２人目の素数さん
2011/02/23(水) 23:43:01.36いやlow basis theoremのはずなのにスペル間違ってたから
きっと内容分かってないんだろなと思ってからかっただけだよ
というかジャクソンってもしかしてJockuschのことじゃないだろうな？
0383１３２人目の素数さん
2011/02/23(水) 23:52:38.94ヒルベルト達の言う有限の立場で示せる命題と言うのは、
或る特定の自然数に対する命題（Δ0式）とか、
或いは変数 x を使って x に対して成り立つ命題を証明することで
「任意の x に対して〜〜」を示す、とか、つまりかなり直截的に証明できるものなので、
∀x P(x)を仮定して∃x P(x)を示すとか、或いはその逆とか、
そういう凝った証明は出て来ないんじゃないかと思います。
従って、別に背理法を使っちゃいけないとはほとんど言っていませんが、
背理法を何度も重ねた超越的な存在証明みたいなものは実際上出て来ないはずです。
だからヒルベルトの計画が上手くいったなら当時の直観主義者達に対する反撃になってた訳で。
0384１３２人目の素数さん
2011/02/24(木) 00:02:15.70∀x P(x)を仮定して背理法によって∃x ¬P(x)を示すとか
0386368
2011/02/24(木) 00:21:42.85ああそうだよ、内容なんてわかってないよ。
俺の論理学歴といえば先日小野の現代数理路理学序説を読了し、
最近shoenfieldを読み始めたばかりだよ。
low basis theorem についてはある人のブログで知ったんだよ、問題あるか？
0387１３２人目の素数さん
2011/02/24(木) 00:26:29.370388１３２人目の素数さん
2011/02/24(木) 00:26:46.53¬∀x〜〜という論理式がそもそも出て来ない。
だから¬∀x¬が出て来ないからその略記としての∃xもそもそも出て来ない。
あるのは、任意にとった x に対して …x… が成り立つ、という …x… という式だけ。
0389１３２人目の素数さん
2011/02/24(木) 00:28:01.310390１３２人目の素数さん
2011/02/24(木) 16:44:00.270391１３２人目の素数さん
2011/02/24(木) 20:11:19.86話の展開をわかりやすくするためだろ。
0392１３２人目の素数さん
2011/02/24(木) 20:28:22.40往々にしてトンデモだったりするから困る
0393１３２人目の素数さん
2011/02/24(木) 21:04:17.78www 本当杉て困る。
0394368
2011/02/24(木) 22:45:14.870395368
2011/02/24(木) 23:12:50.35論理学をやったことない人がいる。
0396１３２人目の素数さん
2011/02/25(金) 12:41:58.62寝言は寝てから言え
0397１３２人目の素数さん
2011/02/25(金) 12:44:27.440398１３２人目の素数さん
2011/02/25(金) 13:40:21.63>>395-396の流れを読め。
0400１３２人目の素数さん
2011/02/25(金) 20:18:53.14あと記述集合論とかとの関係で再帰函数論も或る程度知ってる人が大半なはず。
非古典論理とか部分構造論理とかには疎いだろうけどそれだけがロジックじゃないし。
0401368
2011/02/25(金) 22:19:27.88キューネンとかウッディンとかの本読んでるけど、
論理学のテキストまったく読んだことない人間でも
読めると思うけど？
実際に自分が読めてる。
論理学の知識はすべて共通前提だと考えれば大丈夫だと思う。
実際に直感的に明らかな論理学の結果しか使わないし。
何だかんだで代数、位相、測度、基数の方がメインな道具に見える。
0402１３２人目の素数さん
2011/02/25(金) 23:35:13.210403368
2011/02/25(金) 23:57:02.29forcing axiom, and the non-stationary ideal
0404１３２人目の素数さん
2011/02/27(日) 01:20:35.00> 公理的集合論(略)の研究者で
実際に何やってる人?
組合せ論的な構成可能集合の研究とか?
0405１３２人目の素数さん
2011/02/27(日) 21:35:27.99前原「数学基礎論入門」で、「等号の基本性質」の節の冒頭にある、
次の記述意味が分かりません。
>sとtがn階の対象式である場合には、s=tは、
>∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1})
>という論理式の略記法であった。
ここで、_{n+1}により下付き文字をあらわしました。
この定義ですと、t∈ξ_{n+1}でかつ、¬(s∈ξ_{n+1})となるξ_{n+1}が
存在した場合でも、論理式s=tが成立し得るというふうにとれます。
その意味で正しいのでしょうか？
普通に考えると、「→」のところで、「⇔」の間違いじゃないのかと、
思えるんですが。
0406１３２人目の素数さん
2011/02/27(日) 21:42:08.97∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1}) から
∀ξ_{n+1}(t∈ξ_{n+1}→s∈ξ_{n+1}) が導ける。
ちょっと読み進めばそのことが書いてあるはず。
0407１３２人目の素数さん
2011/02/27(日) 21:43:42.25"集合" ξ_{n+1} の補集合を考えれば、
s∈ξ_{n+1}→t∈ξ_{n+1} の逆向きもO.K.
0408１３２人目の素数さん
2011/02/27(日) 21:53:53.94>>407
ありがとうございます。
ちゃんとした理屈があることが分かり、安心しました。
内包公理や補集合をヒントに理解してみます。
0409１３２人目の素数さん
2011/03/03(木) 15:09:48.69何の役にもたたないのにｗ
0410１３２人目の素数さん
2011/03/03(木) 16:30:05.360411368
2011/03/03(木) 21:57:25.77点集合トポロジーだったかなんだったか。
>>409
俺もそうだけど、別にいいじゃん知ったか。
知ったかでも博士とれちゃう国あるんだよ、世界には＾＾
0412１３２人目の素数さん
2011/03/03(木) 22:08:12.18邪魔なんで
0413368
2011/03/03(木) 22:34:23.08こんな俺でも
ここじゃちょっとは役に立つと思って助言してる。
なんつーか隣人愛ってやつかな、論理の入り口で彷徨ってる
人間みるとつい助けたくなっちゃう。
0414１３２人目の素数さん
2011/03/03(木) 22:55:43.28じゃ助けてよ。シエラハの理論、pcf理論を理解したいんだけど、オススメのショートコースある？
0416368
2011/03/05(土) 23:12:13.84知らなかった定理が結構ある。
0417１３２人目の素数さん
2011/03/06(日) 06:14:59.410418368
2011/03/07(月) 21:37:05.07まぁ本来啓蒙書なんで。
その割には証明がある丁寧な本程度と考えた方が。
0419１３２人目の素数さん
2011/03/16(水) 18:44:12.04まあ仕方ないかな。
0420１３２人目の素数さん
2011/03/16(水) 18:46:10.160421１３２人目の素数さん
2011/03/16(水) 19:09:28.700422１３２人目の素数さん
2011/03/17(木) 13:19:17.800423１３２人目の素数さん
2011/03/17(木) 13:24:44.900424１３２人目の素数さん
2011/03/18(金) 22:11:10.98命題論理のごく初歩的なところをやっているんですが、
replacement theoremとstrong replacement theoremの違いがわかりません。
wff Aを何回か含むwffをC[A]とし、C[A]の中のいくつかのAをwff Bで置き換えた結果をC[B]とする。このとき、
replacement theorem：AとBが論理的同値ならばC[A]とC[B]も論理的同値
strong replacement theorem：(A←→B)→(C[A]←→C[B])はトートロジー
なぜ、後者のほうが「強い」のでしょうか？
0425368
2011/03/18(金) 22:19:34.59なんて初めて聞いた。
0426１３２人目の素数さん
2011/03/18(金) 22:22:50.440427368
2011/03/18(金) 22:45:13.30そんなら425をサクッと説明しちゃってくださいよ。
0428１３２人目の素数さん
2011/03/18(金) 22:50:59.580429１３２人目の素数さん
2011/03/18(金) 22:56:57.07だけど、逆は一般には成り立たないことに
なぞらえてるのでは？
0430１３２人目の素数さん
2011/03/18(金) 23:05:57.04なんでstrongなのかわからん
0431１３２人目の素数さん
2011/03/19(土) 00:31:55.49wff、置換、論理的同値、トートロジー
の定義を書いてみよう。
書いているうちにわかる場合が多いよ。
0432１３２人目の素数さん
2011/03/19(土) 00:33:29.970433１３２人目の素数さん
2011/03/19(土) 00:44:12.360434431
2011/03/19(土) 00:50:10.470435368
2011/03/19(土) 08:09:26.45頭が整理されるってことは結構あると思う。
0436１３２人目の素数さん
2011/03/19(土) 09:44:19.26別の名前が付いている訳でもないけど。
AならばBというのとA→Bはトートロジーだというのでは
後者の方が強い気はするよね。
トートロジーに関するいくつかの性質を使えば前者から後者も証明できるだろうけど。
0437１３２人目の素数さん
2011/03/19(土) 11:07:58.09多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？
それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
どなたか、お教えください
よろしくおねがいします
0438368
2011/03/19(土) 11:58:48.45> ジェフリー『形式論理学』の決定可能、決定不可能のくだりで
> 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？
> それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
> どなたか、お教えください
> よろしくおねがいします
言葉の定義とかも書かないとわからないと思いますよ。
普通の数理論理学のテキストにない用語が多いですから。
0439１３２人目の素数さん
2011/03/19(土) 12:00:34.250440368
2011/03/19(土) 12:07:59.68> ジェフリー『形式論理学』の決定可能、決定不可能のくだりで
> 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える（たとえば、関数記号+を和の関係を表す述語に置き換える）結果、それが言えるという意味ですか？
> それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語（＝11は定理だが、（自由な表れの述語Ａに関して）A11が定理は言えない）は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
> どなたか、お教えください
> よろしくおねがいします
付値は命題への真偽値の与え方と考えてよろしいでしょうか？
それから「自由な表れ」とはなんでしょうか？
0441368
2011/03/19(土) 12:09:39.27> なにこの糞数字コテ
どうも！
0442１３２人目の素数さん
2011/03/19(土) 12:34:39.610443368
2011/03/19(土) 13:42:36.350444368
2011/03/19(土) 13:58:43.76strong replacement theorem から
replacement theorem が証明できる。逆は一般に成り立たないね。
fを付値とすれば
strong replacement theorem より
(A←→B)→(C[A]←→C[B])がトートロジーだから、
f((A←→B)→(C[A]←→C[B]))＝Т
一般に
f(⊥→X)＝f(⊥)→f(X)＝Т
f(X→Т)＝f(X)→f(Т)＝Т
が成り立つから、
f(A←→B)＝⊥ ∨ f(C[A]←→C[B])＝Т
replacement theorem の仮定から、
A と B は論理的同値なので、
f(A)＝(B)＝Т ∨ f(A)＝(B)＝⊥
このとき f(A←→B)＝f(A)←→f(B)＝Т であるので、
f(C[A]←→C[B])＝f(C[A])←→f(C[B])＝Т
よって、
f(C[A])←→f(C[B])＝Т ∨ f(C[A])←→f(C[B])＝⊥
なので C[A] と C[B] は論理的同値。
0445368
2011/03/19(土) 14:09:13.52誤：f(C[A])←→f(C[B])＝Т ∨ f(C[A])←→f(C[B])＝⊥
正：f(C[A])＝f(C[B])＝Т ∨ f(C[A])＝f(C[B])＝⊥
0446368
2011/03/19(土) 14:17:43.260447424
2011/03/19(土) 14:23:56.03なんでstrongなのか・・・
ちなみに戸田山和久の『論理学をつくる』ってテキストです
0448368
2011/03/19(土) 14:26:13.99C[A] と C[B] が論理的同値ならば、
A と B が論理的同値でない場合でも成り立つので、明らかに強いですね。
0449１３２人目の素数さん
2011/03/19(土) 14:41:00.370450１３２人目の素数さん
2011/03/19(土) 14:41:41.100451368
2011/03/19(土) 14:44:01.60それじゃあ深い意味はなく、
使いやすい程度の直感的な命名の可能性が高い。
0452１３２人目の素数さん
2011/03/19(土) 14:45:21.500453１３２人目の素数さん
2011/03/19(土) 14:46:54.490454368
2011/03/19(土) 14:48:57.61私の間違えですね。訂正します。
：
A→B B
------------
A
：
のとき、A→BはAよりも強いと言いますから、
同値の場合は強いとは言わないかもしれないですね。
0455１３２人目の素数さん
2011/03/19(土) 14:52:51.440456368
2011/03/19(土) 14:56:16.92strong replacement theorem は replacement theorem と同値だが、
C[A] と C[B] が論理的同値 という別の命題があった場合、
strong replacement theorem は 「A と B が論理的同値でない」
場合にも成り立ちますが、
このとき replacement theorem が成立している必要はないという意味で、
「強い」と命名したんじゃないんでしょうか。
ですから>>454でいうような定義での「強い」ではないですね。
まぁその本読んだことないんで知りませんが。
0457１３２人目の素数さん
2011/03/19(土) 14:59:31.770458１３２人目の素数さん
2011/03/19(土) 15:03:58.550459１３２人目の素数さん
2011/03/19(土) 15:09:35.95>>424
証明するために、内包公理が必要かどうか。
>>430
「同値」の階層を混同している。
「論理式が同値」と「命題が同値」は全く異なる概念。
「A←→Bならば、その時に限って、A≡B」が証明できるというだけ。
←→、≡は共に略記だけど、常識の範囲だから定義は略。
完全性定理をきちんと理解するには、この辺の区別は重要。
0460１３２人目の素数さん
2011/03/19(土) 15:11:11.86よいです。
＝が自由な表れでないと言っているのは、∀ｘ（ｘ＝ｘ）のような公理があるために、＝を他の述語と置き換えることは必ずしも自由でないということを言っています
0461１３２人目の素数さん
2011/03/19(土) 15:11:24.830462１３２人目の素数さん
2011/03/19(土) 15:12:31.060463１３２人目の素数さん
2011/03/19(土) 15:16:38.80valuation function: wff→truth value
0464１３２人目の素数さん
2011/03/19(土) 20:46:20.72∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))
が成立しないんじゃないかと思います。
反例として、
箱が二個(箱１、箱２)と玉が一個だけの世界を考えて、
Ｐ(ｘ)、Ｑ(ｘ)がともに、玉が箱ｘに入っているという命題を表すものとします。
このとき、各ｘに対してｙ＝ｘと考えてやれば「∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))」は真になりますよね。
ところがｙ＝１のときはｘ＝２を、ｙ＝２のときはｘ＝１の場合を考えてやればいずれも「Ｐ(ｘ)→Ｑ(ｙ)」が成立しないため、「∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))」が偽になりますよね？？
と考えたのですが、間違いがあれば教えてくださいｍ(＿ ＿)ｍ
0465368
2011/03/19(土) 20:58:24.75散歩ついでに読んでみたけど
71ページの辺りの文脈読んでなんとなく推測。
replacement theorem は
A←→B がトートロジーならば C[A]←→C[B] もトートロジーと書ける。
|= C ⇔ C はトートロジー -----------（１）
（１）の書き方に従えば、
|= A←→B ⇒ |= C[A]←→C[B] -----------（２）
また、
strong replacement theorem は、
|= (A←→B)→(C[A]←→C[B]) -----------（３）
（３）からCuttingによって（２）が証明できるが逆は成り立たない。
だからstrongと読んでいるのではないだろうか？
>>459の言うとおりだとしても、
置き換えの定理が出てくるこの時点で、内包公理どころか
集合論の気配は一切ない。
本来のstrong replacement theoremの意味はどうだから知らないが、
少なくともこの本を読んでも、
「強い」が内包公理の要不要に依存しているようには思えない。
0466１３２人目の素数さん
2011/03/19(土) 21:15:27.00>>429は一般に言えることなの？
0467368
2011/03/19(土) 22:19:40.96定理１ T，A |= B ⇔ T |= A→B
のTを空集合とすれば、
A |= B ⇔ |= A→B
定理２（Cutting） T |= A 、A, K |= B ⇒ T, K |= B
のような定理で、TとKを空集合とすれば、
|= A 、A |= B ⇒ |= B
となり、replacement theorem が証明される。
|=という記号はこの本の定義（2重ターンスタイルとか書かれてた）に従ったが、
上の定理１と２が常に成り立つかは恐らく証明体系に依存する。
>>429はこの|=のことを証明を表す記号として言っているのでは？
0468１３２人目の素数さん
2011/03/19(土) 22:38:17.87もうちょっとわかりやすくたのむ・・・
strongとそうでないのは、結局、どっちからどっちをも証明できると考えておいてＯＫ？
0469368
2011/03/19(土) 22:40:11.88∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))
が「成立しない」の意味によりますね。
論理式としては成立しますが、これだけでは常に真ではないですね。
最後の方の文章がいまいち理解できませんが、
一応確認しておきたいのですが、
論理式の前半の∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))に出てくる変数ｘとｙは、
後半の∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))の変数ｘとｙとは違うということは
分かっていますか？
0470368
2011/03/19(土) 22:46:39.88strong replacement theorem と replacement theorem という定理は、
メタ理論において定理とみなされていて、
メタ理論において必要十分条件（同値）になっています。
しかし形式体系の中で、論理式として取り扱う際には、
strong replacement theorem から replacement theorem への
論理式の変形は可能ですが、逆への変形は不可能なのです。
つまり形式体系の中で strong だと主張しているのです。
0471１３２人目の素数さん
2011/03/19(土) 22:48:50.08おお、よくわかった。
また質問したいです。よろしければお名前を教えていただけませんか
0472368 ◆jkwVJMjC32
2011/03/19(土) 23:01:35.98仮に368としておきます。
論理学をつくるをざっと眺めたところ、
無駄に冗長なうえに、
今回の意味論とシンタックスの混同のように、
さまざまな罠が張り巡らされているようなので気を付けてください。
0473464
2011/03/19(土) 23:04:43.49ありがとうございます。
すみません、「成立」は述語論理でトートロジーになるという意味です。
僕の読んでいる教科書で、「∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ)) 」をＮＫで証明せよという課題が載っていて、解答がなかったもので。。。
>論理式の前半の∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))に出てくる変数ｘとｙは、
>後半の∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ))の変数ｘとｙとは違うということは
それは分かっています。
「∀ｘ∃ｙ(Ｐ(ｘ)→Ｑ(ｙ))→∃ｘ∀ｙ(Ｐ(ｘ)→Ｑ(ｙ)) 」の反例(偽になる場合)があれば教えていただけませんか？
■ このスレッドは過去ログ倉庫に格納されています