数学基礎論・数理論理学のスレッド その7
■ このスレッドは過去ログ倉庫に格納されています
0001132人目の素数さん
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/
0386368
2011/02/24(木) 00:21:42.85ああそうだよ、内容なんてわかってないよ。
俺の論理学歴といえば先日小野の現代数理路理学序説を読了し、
最近shoenfieldを読み始めたばかりだよ。
low basis theorem についてはある人のブログで知ったんだよ、問題あるか?
0387132人目の素数さん
2011/02/24(木) 00:26:29.370388132人目の素数さん
2011/02/24(木) 00:26:46.53¬∀x〜〜という論理式がそもそも出て来ない。
だから¬∀x¬が出て来ないからその略記としての∃xもそもそも出て来ない。
あるのは、任意にとった x に対して …x… が成り立つ、という …x… という式だけ。
0389132人目の素数さん
2011/02/24(木) 00:28:01.310390132人目の素数さん
2011/02/24(木) 16:44:00.270391132人目の素数さん
2011/02/24(木) 20:11:19.86話の展開をわかりやすくするためだろ。
0392132人目の素数さん
2011/02/24(木) 20:28:22.40往々にしてトンデモだったりするから困る
0393132人目の素数さん
2011/02/24(木) 21:04:17.78www 本当杉て困る。
0394368
2011/02/24(木) 22:45:14.870395368
2011/02/24(木) 23:12:50.35論理学をやったことない人がいる。
0396132人目の素数さん
2011/02/25(金) 12:41:58.62寝言は寝てから言え
0397132人目の素数さん
2011/02/25(金) 12:44:27.440398132人目の素数さん
2011/02/25(金) 13:40:21.63>>395-396の流れを読め。
0400132人目の素数さん
2011/02/25(金) 20:18:53.14あと記述集合論とかとの関係で再帰函数論も或る程度知ってる人が大半なはず。
非古典論理とか部分構造論理とかには疎いだろうけどそれだけがロジックじゃないし。
0401368
2011/02/25(金) 22:19:27.88キューネンとかウッディンとかの本読んでるけど、
論理学のテキストまったく読んだことない人間でも
読めると思うけど?
実際に自分が読めてる。
論理学の知識はすべて共通前提だと考えれば大丈夫だと思う。
実際に直感的に明らかな論理学の結果しか使わないし。
何だかんだで代数、位相、測度、基数の方がメインな道具に見える。
0402132人目の素数さん
2011/02/25(金) 23:35:13.210403368
2011/02/25(金) 23:57:02.29forcing axiom, and the non-stationary ideal
0404132人目の素数さん
2011/02/27(日) 01:20:35.00> 公理的集合論(略)の研究者で
実際に何やってる人?
組合せ論的な構成可能集合の研究とか?
0405132人目の素数さん
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が成立し得るというふうにとれます。
その意味で正しいのでしょうか?
普通に考えると、「→」のところで、「⇔」の間違いじゃないのかと、
思えるんですが。
0406132人目の素数さん
2011/02/27(日) 21:42:08.97∀ξ_{n+1}(s∈ξ_{n+1}→t∈ξ_{n+1}) から
∀ξ_{n+1}(t∈ξ_{n+1}→s∈ξ_{n+1}) が導ける。
ちょっと読み進めばそのことが書いてあるはず。
0407132人目の素数さん
2011/02/27(日) 21:43:42.25"集合" ξ_{n+1} の補集合を考えれば、
s∈ξ_{n+1}→t∈ξ_{n+1} の逆向きもO.K.
0408132人目の素数さん
2011/02/27(日) 21:53:53.94>>407
ありがとうございます。
ちゃんとした理屈があることが分かり、安心しました。
内包公理や補集合をヒントに理解してみます。
0409132人目の素数さん
2011/03/03(木) 15:09:48.69何の役にもたたないのにw
0410132人目の素数さん
2011/03/03(木) 16:30:05.360411368
2011/03/03(木) 21:57:25.77点集合トポロジーだったかなんだったか。
>>409
俺もそうだけど、別にいいじゃん知ったか。
知ったかでも博士とれちゃう国あるんだよ、世界には^^
0412132人目の素数さん
2011/03/03(木) 22:08:12.18邪魔なんで
0413368
2011/03/03(木) 22:34:23.08こんな俺でも
ここじゃちょっとは役に立つと思って助言してる。
なんつーか隣人愛ってやつかな、論理の入り口で彷徨ってる
人間みるとつい助けたくなっちゃう。
0414132人目の素数さん
2011/03/03(木) 22:55:43.28じゃ助けてよ。シエラハの理論、pcf理論を理解したいんだけど、オススメのショートコースある?
0416368
2011/03/05(土) 23:12:13.84知らなかった定理が結構ある。
0417132人目の素数さん
2011/03/06(日) 06:14:59.410418368
2011/03/07(月) 21:37:05.07まぁ本来啓蒙書なんで。
その割には証明がある丁寧な本程度と考えた方が。
0419132人目の素数さん
2011/03/16(水) 18:44:12.04まあ仕方ないかな。
0420132人目の素数さん
2011/03/16(水) 18:46:10.160421132人目の素数さん
2011/03/16(水) 19:09:28.700422132人目の素数さん
2011/03/17(木) 13:19:17.800423132人目の素数さん
2011/03/17(木) 13:24:44.900424132人目の素数さん
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なんて初めて聞いた。
0426132人目の素数さん
2011/03/18(金) 22:22:50.440427368
2011/03/18(金) 22:45:13.30そんなら425をサクッと説明しちゃってくださいよ。
0428132人目の素数さん
2011/03/18(金) 22:50:59.580429132人目の素数さん
2011/03/18(金) 22:56:57.07だけど、逆は一般には成り立たないことに
なぞらえてるのでは?
0430132人目の素数さん
2011/03/18(金) 23:05:57.04なんでstrongなのかわからん
0431132人目の素数さん
2011/03/19(土) 00:31:55.49wff、置換、論理的同値、トートロジー
の定義を書いてみよう。
書いているうちにわかる場合が多いよ。
0432132人目の素数さん
2011/03/19(土) 00:33:29.970433132人目の素数さん
2011/03/19(土) 00:44:12.360434431
2011/03/19(土) 00:50:10.470435368
2011/03/19(土) 08:09:26.45頭が整理されるってことは結構あると思う。
0436132人目の素数さん
2011/03/19(土) 09:44:19.26別の名前が付いている訳でもないけど。
AならばBというのとA→Bはトートロジーだというのでは
後者の方が強い気はするよね。
トートロジーに関するいくつかの性質を使えば前者から後者も証明できるだろうけど。
0437132人目の素数さん
2011/03/19(土) 11:07:58.09多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える(たとえば、関数記号+を和の関係を表す述語に置き換える)結果、それが言えるという意味ですか?
それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語(=11は定理だが、(自由な表れの述語Aに関して)A11が定理は言えない)は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
どなたか、お教えください
よろしくおねがいします
0438368
2011/03/19(土) 11:58:48.45> ジェフリー『形式論理学』の決定可能、決定不可能のくだりで
> 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える(たとえば、関数記号+を和の関係を表す述語に置き換える)結果、それが言えるという意味ですか?
> それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語(=11は定理だが、(自由な表れの述語Aに関して)A11が定理は言えない)は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
> どなたか、お教えください
> よろしくおねがいします
言葉の定義とかも書かないとわからないと思いますよ。
普通の数理論理学のテキストにない用語が多いですから。
0439132人目の素数さん
2011/03/19(土) 12:00:34.250440368
2011/03/19(土) 12:07:59.68> ジェフリー『形式論理学』の決定可能、決定不可能のくだりで
> 多項関係の述語を含む関数記号を含まない理論が決定不可能というのは関数記号を多項関係の述語に置き換える(たとえば、関数記号+を和の関係を表す述語に置き換える)結果、それが言えるという意味ですか?
> それとも、同一性記号や和の関係を表す述語のような特別な付値を持つ述語(=11は定理だが、(自由な表れの述語Aに関して)A11が定理は言えない)は関係なくて、自由な表れの多項関係の述語を持てば理論は決定不能になるという意味ですか
> どなたか、お教えください
> よろしくおねがいします
付値は命題への真偽値の与え方と考えてよろしいでしょうか?
それから「自由な表れ」とはなんでしょうか?
0441368
2011/03/19(土) 12:09:39.27> なにこの糞数字コテ
どうも!
0442132人目の素数さん
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 が論理的同値でない場合でも成り立つので、明らかに強いですね。
0449132人目の素数さん
2011/03/19(土) 14:41:00.370450132人目の素数さん
2011/03/19(土) 14:41:41.100451368
2011/03/19(土) 14:44:01.60それじゃあ深い意味はなく、
使いやすい程度の直感的な命名の可能性が高い。
0452132人目の素数さん
2011/03/19(土) 14:45:21.500453132人目の素数さん
2011/03/19(土) 14:46:54.490454368
2011/03/19(土) 14:48:57.61私の間違えですね。訂正します。
:
A→B B
------------
A
:
のとき、A→BはAよりも強いと言いますから、
同値の場合は強いとは言わないかもしれないですね。
0455132人目の素数さん
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でいうような定義での「強い」ではないですね。
まぁその本読んだことないんで知りませんが。
0457132人目の素数さん
2011/03/19(土) 14:59:31.770458132人目の素数さん
2011/03/19(土) 15:03:58.550459132人目の素数さん
2011/03/19(土) 15:09:35.95>>424
証明するために、内包公理が必要かどうか。
>>430
「同値」の階層を混同している。
「論理式が同値」と「命題が同値」は全く異なる概念。
「A←→Bならば、その時に限って、A≡B」が証明できるというだけ。
←→、≡は共に略記だけど、常識の範囲だから定義は略。
完全性定理をきちんと理解するには、この辺の区別は重要。
0460132人目の素数さん
2011/03/19(土) 15:11:11.86よいです。
=が自由な表れでないと言っているのは、∀x(x=x)のような公理があるために、=を他の述語と置き換えることは必ずしも自由でないということを言っています
0461132人目の素数さん
2011/03/19(土) 15:11:24.830462132人目の素数さん
2011/03/19(土) 15:12:31.060463132人目の素数さん
2011/03/19(土) 15:16:38.80valuation function: wff→truth value
0464132人目の素数さん
2011/03/19(土) 20:46:20.72∀x∃y(P(x)→Q(y))→∃x∀y(P(x)→Q(y))
が成立しないんじゃないかと思います。
反例として、
箱が二個(箱1、箱2)と玉が一個だけの世界を考えて、
P(x)、Q(x)がともに、玉が箱xに入っているという命題を表すものとします。
このとき、各xに対してy=xと考えてやれば「∀x∃y(P(x)→Q(y))」は真になりますよね。
ところがy=1のときはx=2を、y=2のときはx=1の場合を考えてやればいずれも「P(x)→Q(y)」が成立しないため、「∃x∀y(P(x)→Q(y))」が偽になりますよね??
と考えたのですが、間違いがあれば教えてくださいm(_ _)m
0465368
2011/03/19(土) 20:58:24.75散歩ついでに読んでみたけど
71ページの辺りの文脈読んでなんとなく推測。
replacement theorem は
A←→B がトートロジーならば C[A]←→C[B] もトートロジーと書ける。
|= C ⇔ C はトートロジー -----------(1)
(1)の書き方に従えば、
|= A←→B ⇒ |= C[A]←→C[B] -----------(2)
また、
strong replacement theorem は、
|= (A←→B)→(C[A]←→C[B]) -----------(3)
(3)からCuttingによって(2)が証明できるが逆は成り立たない。
だからstrongと読んでいるのではないだろうか?
>>459の言うとおりだとしても、
置き換えの定理が出てくるこの時点で、内包公理どころか
集合論の気配は一切ない。
本来のstrong replacement theoremの意味はどうだから知らないが、
少なくともこの本を読んでも、
「強い」が内包公理の要不要に依存しているようには思えない。
0466132人目の素数さん
2011/03/19(土) 21:15:27.00>>429は一般に言えることなの?
0467368
2011/03/19(土) 22:19:40.96定理1 T,A |= B ⇔ T |= A→B
のTを空集合とすれば、
A |= B ⇔ |= A→B
定理2(Cutting) T |= A 、A, K |= B ⇒ T, K |= B
のような定理で、TとKを空集合とすれば、
|= A 、A |= B ⇒ |= B
となり、replacement theorem が証明される。
|=という記号はこの本の定義(2重ターンスタイルとか書かれてた)に従ったが、
上の定理1と2が常に成り立つかは恐らく証明体系に依存する。
>>429はこの|=のことを証明を表す記号として言っているのでは?
0468132人目の素数さん
2011/03/19(土) 22:38:17.87もうちょっとわかりやすくたのむ・・・
strongとそうでないのは、結局、どっちからどっちをも証明できると考えておいてOK?
0469368
2011/03/19(土) 22:40:11.88∀x∃y(P(x)→Q(y))→∃x∀y(P(x)→Q(y))
が「成立しない」の意味によりますね。
論理式としては成立しますが、これだけでは常に真ではないですね。
最後の方の文章がいまいち理解できませんが、
一応確認しておきたいのですが、
論理式の前半の∀x∃y(P(x)→Q(y))に出てくる変数xとyは、
後半の∃x∀y(P(x)→Q(y))の変数xとyとは違うということは
分かっていますか?
0470368
2011/03/19(土) 22:46:39.88strong replacement theorem と replacement theorem という定理は、
メタ理論において定理とみなされていて、
メタ理論において必要十分条件(同値)になっています。
しかし形式体系の中で、論理式として取り扱う際には、
strong replacement theorem から replacement theorem への
論理式の変形は可能ですが、逆への変形は不可能なのです。
つまり形式体系の中で strong だと主張しているのです。
0471132人目の素数さん
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ありがとうございます。
すみません、「成立」は述語論理でトートロジーになるという意味です。
僕の読んでいる教科書で、「∀x∃y(P(x)→Q(y))→∃x∀y(P(x)→Q(y)) 」をNKで証明せよという課題が載っていて、解答がなかったもので。。。
>論理式の前半の∀x∃y(P(x)→Q(y))に出てくる変数xとyは、
>後半の∃x∀y(P(x)→Q(y))の変数xとyとは違うということは
それは分かっています。
「∀x∃y(P(x)→Q(y))→∃x∀y(P(x)→Q(y)) 」の反例(偽になる場合)があれば教えていただけませんか?
0474132人目の素数さん
2011/03/20(日) 00:09:54.48P,Q ともに1変数述語として、対応する部分集合をそれぞれ整数全体、偶数全体
x,y を異なる変数
とすれば、このフレームはモデルとならない。
0475132人目の素数さん
2011/03/20(日) 00:13:56.99多項関係の述語記号を持ち関数記号を持たない理論は決定不可能とあったのですが、その理論で算術の定理(例えば、任意の数項に関して、数項と0の積と0と数項の積は同一という算術の定理)は真ですか?
というのが聞きたかった内容です
>>473
あってると思いますよ
∀x∃y(P(x)→Q(y))→∃x∀y(P(x)→Q(y))は妥当ではないですから
例えば、任意のドメインの要素がPに含まれあるドメインの要素がQに含まれ(∀x∃y(Px→Qy)が真)、あるドメインの要素が¬Qに含まれる(∃x∀y(Px→Qy)が偽)世界を考えれば、∀x∃y(Px→Qy)→∃x∀y(Px→Qy)の妥当性の反例になると思います
もっとも、教科書が妥当でない式の証明を求めるということはないので、誤植か読み違いが起きてるのでしょう
xとyの順序をyとxと読み違えたりすることで式の内容はかわってきますよ
0476132人目の素数さん
2011/03/20(日) 02:02:42.880477464
2011/03/20(日) 17:46:21.59ありがとうございます。どうも誤植だった模様です。
正確には∀x∃y(P(x)→Q(y))→∃y∀x(P(x)→Q(y))だったようです。
0478132人目の素数さん
2011/03/20(日) 18:21:08.09戸田じゃなくて戸田山ね。
あの人は(学部の素朴な)集合論の普通の定理に関しても
この定理は哲学的には問題があるとか良く分かんないこと書いてた気がする。
ゲーデルと20世紀の論理学の彼が書いた記事は面白かったけどね。
0479368 ◆jkwVJMjC32
2011/03/21(月) 10:54:28.93「多項関係の述語記号を持ち関数記号を持たない理論は決定不可能」
というのBoolosによって示された定理のことでしょうか。
算術の定理に必要な関数記号を論理学の述語で代用するということは、
数学を二階述語論理で直接展開するということでしょうか。
これが真になるというのは、どのような場合なのでしょうか。
私は知りませんが、興味はありますね!
0480132人目の素数さん
2011/03/22(火) 18:59:09.84>429は一般に言えることなの?
p を命題変数とする。勝手な論理式 A に対し、
p が証明可能ならば A も証明可能
しかし、p→A は一般にはトートロジーではない。
証明可能の条件をもうちょっと強めると、古典命題論理の範囲では
Mints による定理があって、逆にあたることが成立する。
0481132人目の素数さん
2011/03/23(水) 00:53:46.06>数学を二階述語論理で直接展開するということでしょうか。
は、私がそういうことかなと推測した内容で、本が言っている内容かはわかりません
数理論理の内容なので、関数記号を除いたからといって数学の定理が扱えないわけはない
じゃあどうやって?
述語でやろうというのか?しかし・・
という感じで質問に来ました
0482132人目の素数さん
2011/03/23(水) 23:44:06.57Modal logic
Classical modal logic
Regular modal logic
Normal modal logic
Modern modal logic
Temporal logic
Propositional dynamic logic
Linear temporal logic
Interval temporal logic
Graphical interval logic
Signed interval logic
Future interval logic
Kinetic logic
Dynamic logic
Propositional dynamic logic
Multimodal logic
Hennessy-Milner logic
Epistemic modal logic
Public announcement logic
Product update logic
Deontic logic
Dyadic deontic logic
Imperative logic
0483132人目の素数さん
2011/03/23(水) 23:44:42.49Algorithmic logic
Branching-time logic
CTL*
Computational tree logic
Tense logic
Computational verb logic
Hybrid logic
Quantum logic
Many-valued logic
Fuzzy logic
T-norm fuzzy logics
Monoidal t-norm based logic
Product fuzzy logic
Nilpotent minimum logic
Lukasiewicz logic
Godel-Dummett logic
Basic fuzzy logic
Post logic
Kleene logic
Provability logic
Interpretability logic
0484132人目の素数さん
2011/03/23(水) 23:45:10.90Bayesian logic
Probabilistic logic
Subjective logic
Combinations logic
Substructural logic
Relevant logic
Linear logic
Strict logic
Full linear logic
Modern Lambek calculus
Non-commutative logic
Cyclic linear logic
Pomset logic
BV
NEL
Bunched logic
Affine logic
Direct logic
Full affine logic
■ このスレッドは過去ログ倉庫に格納されています