12/01/02 23:04:29.50
数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
URLﾘﾝｸ(www.math.tohoku.ac.jp)
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
前スレ
数学基礎論・数理論理学 その10
ｽﾚﾘﾝｸ(math板)
2:１３２人目の素数さん
12/01/02 23:31:59.88
ここは「哲学排除！」のアスペは来ない（はず）ので、
スレタイスレ446氏をはじめとした哲学的論理学の話題も歓迎！
平和に行きましょう。
3:１３２人目の素数さん
12/01/02 23:33:33.23
おつ
4:前スレ969
12/01/02 23:52:17.59
申し訳ありません。前スレが埋まってしまいそうなので、前スレ980からのコメントを
ここでもう一度貼らせて頂きます。
5:前スレ969
12/01/02 23:52:46.99
LoebのDerivability ConditionsのD3の証明を自分なりに書いてみました。
間違い等あったらご指摘頂けないでしょうか。よろしくお願いいたします。
------------------------------------------------------------------------------------
LoebのDerivability ConditionsのD3を証明するためには、任意のΣ_1文Fに対して、
PA|- F→Pr([F])
が証明できればよく、そのためにはFの構成に関する帰納法で証明すればよい。
つまり、以下の１から４の順番で証明すればよい。
１、F ⇔ x=y, Sx=y, x+y=z, x・y=z のとき、
PA|- F→□[F]
２、PA|- α∧β→□[α∧β]
３、PA|- ∃xα→□[∃xα]
４、PA|- ∀x<yα→□[∀x<yα]
ただし、
PA|- α→□[α]
PA|- β→□[β]
とする。
6:前スレ969
12/01/02 23:53:05.11
F[t/x]
Fの自由変数xにtを代入した論理式を表す
１、PA|- x=y→□[x=y]
証明
PA,x=y|- □[x=y] を示せばよい。すなわち
PA,x=y|- □[x=y][x/y]
|- □[x=y [x/y]]
|- □[x=x]
を示せばよい。
公理より、PA|-x=x
これにD1を適用すると、
PA|- □[x=x]
したがって、
PA,x=y|- □[x=y]
すなわち、
PA|- x=y→□[x=y]
証明終わり
7:１３２人目の素数さん
12/01/02 23:53:21.78
２、PA|- Sx=y→□[Sx=y]
証明
PA,Sx=y|- □[Sx=y] を示せばよい。すなわち
PA,Sx=y|- □[Sx=y][Sx/y]
|- □[Sx=y [Sx/y]]
|- □[Sx=Sx]
を示せばよい。
PA|- Sx=Sx
これにD1を適用すると、
PA|- □[Sx=Sx]
したがって、
PA|- Sx=y→□[Sx=y]
証明終わり
8:前スレ969
12/01/02 23:53:38.64
３、PA|- x+y=z→□[x+y=z]
証明
xについての（PAの公理での）数学的帰納法で示す。
（ⅰ）PA|- (x+y=z→□[x+y=z])[0/x] を示す
(x+y=z)[0/x] |- y=z
|- □[y=z]
|- □[(x+y=z)[0/x]]
|- □[(x+y=z)][0/x]
よって、
|-(x+y=z)[0/x]→□[(x+y=z)][0/x]
⇔|-(x+y=z→□[x+y=z])[0/x]
9:前スレ969
12/01/02 23:54:02.47
（ⅱ）PA|- ∀x〔(x+y=z→□[x+y=z])→(x+y=z→□[x+y=z])[Sx/x] 〕を示す
まず、以下のことに注意する。
/////////////////////////////////////////////
(x+y=z)[Sy/y] ≡ (x+y=z)[Sx/x]
よって、
□[x+y=z][Sy/y] ≡ □[x+y=z][Sx/x]
/////////////////////////////////////////////
これを踏まえた上で、
∀y∀z(x+y=z→□[x+y=z])|- ∀y∀z(x+y=z→□[x+y=z])[Sx/x] を示す
∀y∀z(x+y=z→□[x+y=z])|- (x+y=z)[Sy/y]→□[x+y=z][Sy/y]
|- (x+y=z)[Sx/x]→□[x+y=z][Sx/x]
≡ (x+y=z → □[x+y=z])[Sx/x]
したがって、（ⅰ）（ⅱ）と帰納法の公理より
PA|- x+y=z→□[x+y=z]
証明終わり
10:前スレ969
12/01/02 23:54:38.57
４、PA|- x・y=z→□[x・y=z]
３と同様なので省略。
とりあえず、ここまでで何かありましたら、御意見よろしくお願いいたします。
参考にしたのは、
Wolfgang RautenbergのA Concise Introductionto Mathematical Logic
URLﾘﾝｸ(www.scribd.com)
の第６章、７章です。
11:前スレ969
12/01/02 23:55:29.26
989 ：１３２人目の素数さん：2012/01/02(月) 23:36:45.49
まずΣ1論理式って否定を持つものもあるのだから、
１から４の他に少なくとも原子論理の否定についても同じことを示さないといけない。
990 ：１３２人目の素数さん：2012/01/02(月) 23:39:36.25
＞PA,x=y|- □[x=y] を示せばよい。すなわち
＞PA,x=y|- □[x=y][x/y]
ここがまずい、□[x=y] は x,y を自由変数に持つ論理式じゃない。
x,y という変数記号のゲーデル数が現れる論理式ではあるけど。
よって y に x を代入とかって意味をなさない。
12:１３２人目の素数さん
12/01/02 23:55:55.25
992 ：969：2012/01/02(月) 23:48:31.36
>>989
リンク先のA Concise Introductionto Mathematical Logicには原論理式の否定についての
証明が書かれていなかった（ように思われる）ので、見落としてました。ありがとうございます。
（なんで、書かれてなかったのだろうか・・・）
>>990
すいません、定義を書くのが面倒でそのへんのことを端折っていました。
正確には、以下のように定義されているものとしてよろしくお願いいたします。
sub(t,i,x)
"ゲーデル数がxである論理式のi番目の自由変数に、ゲーデル数がtである項を代入してできる論理式"のゲーデル数の数項を返す関数
var(x) = 2・x+17
※PAの原始記号にはそれぞれ奇数の数項を当てており、変数x_1,x_2,…には19以上の奇数の数項が割り当てられているものとします。
num(x)
x番目の数項を返す関数。たとえば、num(3)=SSS0
su(x,y,z) = sub(num(x),var(y),z)
□A ≡ Pr([A])
□[A] ≡ □(su(x_m,k_m,…,su(x_2,k_2,su(x_1,k_1,[A]))…))
したがって、
□[x=y] は x,y を自由変数に持つ論理式を表しているものとします。
13:前スレ969
12/01/02 23:56:29.51
引っ越し終了
スレ汚しすみません。
14:スレタイスレ446
12/01/03 00:10:14.11
>>6
＞PA,x=y|- □[x=y] を示せばよい。すなわち
＞PA,x=y|- □[x=y][x/y]
＞|- □[x=y [x/y]]
＞|- □[x=x]
ここが理解できないのですが、
PA,x=y|- □[x=y]（この□はPr([])の略と解釈します。）から、
PA,x=y|- □[x=y][x/y]が出てくるのはどういった条件によるのでしょうか？
また次の
|- □[x=y [x/y]]
が出てくる理由も分からないのですが、これは例のリンク先に書いてあるのでしょうか？
（とは言え、例のリンク先の本は私がこの掲示板で以前誰かに推奨したものですが...。）
15:１３２人目の素数さん
12/01/03 00:11:55.78
>>前スレ969
大きな流れとしては間違っていないと思うけど、細かい点で幾つか気になる。
＞(x+y=z)[0/x] |- y=z
＞|- □[y=z]
＞|- □[(x+y=z)[0/x]]
＞|- □[(x+y=z)][0/x]
最初に |- はどういう意味？ PA の元での implication と理解していい？
二行目の |- は１を使っているんだよね？
三行目の |- はそんなに自明じゃなくて>>9の注意みたいなのが必要な気がする。
で、その注意だけど
＞(x+y=z)[Sy/y] ≡ (x+y=z)[Sx/x]
＞よって、
＞□[x+y=z][Sy/y] ≡ □[x+y=z][Sx/x]
これは D1 と D2 を使った推論かな？
16:１３２人目の素数さん
12/01/03 00:28:26.98
そのうち、記述論理が一階述語論理にとって替わるのかな？
昔、様相論理を使って集合論を記述してどうの、という話があったけど、下火になったしね。
様相論理を記述論理に直して再チャレンジってことかな？
17:１３２人目の素数さん
12/01/03 01:20:30.22
Zermelo の集合論で出来ることと出来ないことがまとめてある文献ってありますか？
18:１３２人目の素数さん
12/01/03 02:19:48.96
前スレ942の
>記述論理ってかなり便利じゃないだろうか？決定可能だし...。
>量化記号が一般化されているし、
ってところは、ハッタリだったという理解でおk？
19:１３２人目の素数さん
12/01/03 05:28:29.98
昨夜、あっという間に新スレへの移行が完了してしまっとるなあ。実に見事だ。
勝手に「自称次スレ」を立ててたアスペは、指を咥えとるしかなかったんだろな。
この新スレには、アスペみたいな奴が現れないことを祈ろう。
自分で立てた隔離スレで騒いだまま、ずっと出てくるなよ。
20:１３２人目の素数さん
12/01/03 07:09:53.37
>>17
纏まっている文献は知らないけど、
ZF では成り立つが Zermelo の集合論で成り立たないことが有名な結果は幾つかある。
一番有名なのはω＋ωがフォンノイマン順序数として存在すること。
ただ、順序型としてのω＋ωは滅茶苦茶弱い算術でも扱えるので、実際の数学には影響はない。
本当に数学的な命題での例となるとそんなにないかな。
選択公理スレにも書いてある通り、ボレルゲームの決定性はその一例。
他に、「二つの一階の構造が、初等同値であることと、あるウルトラフィルタによる超冪が同型であることは同値」
っていうシェラハによるモデル理論の金字塔的結果は、
置換公理なしでは無理だって聞いたことがあるような。
21:スレタイスレ446
12/01/03 07:38:10.89
>>18
量化記号が一般化されているかは言葉の使い方次第だが、
推論のタブローは必ず停止するかクラッシュするので決定可能。
だからこそ計算クラスで表現力が調べられる。
22:１３２人目の素数さん
12/01/03 08:17:51.03
>>16
>昔、様相論理を使って集合論を記述してどうの、という話があった
詳細きぼん。それって、様相論理は決定可能だから、決定可能な集合論を作ろうってこと？
23:１３２人目の素数さん
12/01/03 08:40:34.37
どうやらアスペはマツシンだったっぽい。
議論の仕方から脱線する話題まで、マツシンそのものと言える。
自分の隔離スレで、「直観主義は直観主義論理を採用すること」等々、
素人っぷり丸出しのこと喚いているぜ。
24:１３２人目の素数さん
12/01/03 08:43:15.18
803 ：１３２人目の素数さん：2011/12/26(月) 02:31:25.06
直観主義で提唱された論理が直観主義論理っていうだけで、
直観主義の研究＝直観主義論理の研究、ではないんだがな。
直観主義っていうのは、論理の部分だけではなく、非論理的公理の部分や、
その他数学のあるべき姿全般に対する哲学的主張（例えば形式主義に反対するなど）までひっくるめた
文字通り一つの「主義」なんだけどな。
直観主義論理はその一部分に過ぎないし、その部分だけならば形式主義とは矛盾しないわけだ。
25:１３２人目の素数さん
12/01/03 08:56:44.28
アスペとの基礎論論争は、隔離スレでやってくれ
26:１３２人目の素数さん
12/01/03 09:11:00.68
折角マツシンは自分で隔離されているわけだし、放っておけば害はないだろ。
相手しないと、こっちの本スレに出張してくるの？
27:１３２人目の素数さん
12/01/03 09:25:17.08
>>20
>他に、「二つの一階の構造が、初等同値であることと、あるウルトラフィルタによる超冪が同型であることは同値」
>っていうシェラハによるモデル理論の金字塔的結果
その証明が書いてある文献、教えてもらえますか？
28:１３２人目の素数さん
12/01/03 09:34:12.01
>>20
すみません、もう一つ。"フォンノイマン順序数" って何ですか？
29:１３２人目の素数さん
12/01/03 10:07:44.30
ググるべし。ググるとこんなんが出てきた：
フォン・ノイマンに由来する順序数の定義を仮定しているからで、
その中で個々の順序数は先行する全ての順序数の集合になっている。このような定義はブラリ＝フォルティがパラドックスを考案した当時はまだ知られていなかった。
(URLﾘﾝｸ(ja.wikipedia.org))
つまり順序数を「先行する全ての順序数の集合」として表現した場合の順序数のこと。
置換公理の自然さの解説に「ω＋ωというあるべきものの存在が示せなくなる」なんてのを見かけるが、
それはフォン・ノイマンに由来する順序数の定義を仮定しているからで、
この表現方法にこだわらなければ理由にも何にもなってないのさ。
30:１３２人目の素数さん
12/01/03 10:24:30.64
お聞きしたいことがあります。
一階述語論理の公理系Tが帰納的に記述可能であることの厳密な定義は何でしょうか？
公理系がデタラメに構成されていないことというニュアンスは分かるのですが…
31:スレタイスレ446
12/01/03 10:30:37.67
>>16
＞そのうち、記述論理が一階述語論理にとって替わるのかな？
今の計算機の原理が変わらない限り一階論理がなくなることはない。
＞昔、様相論理を使って集合論を記述してどうの、という話があったけど、下火になったしね。
様相論理は可能世界を用いて内包を使う意図があって導入された。
様相論理が扱う文は一階論理で透明性（代入法則が成り立たない）を持たない文なので、
数学や一階論理の様な神の視点の立場に合致しなかった。
＞様相論理を記述論理に直して再チャレンジってことかな？
既にはじまっている。
人工知能では概念を扱うためオントロジーが導入された。
オントロジーは最上位の概念としてメタなオントロジーを持つとされるが、
とりわけSUMOという体系はサブシステムとして集合やクラスを扱うことができる。
このオントロジーの記述の手段として次の3つが考えられたわけだ。
・パースらが研究していた存在グラフをsowaらが発展させた概念グラフ、また意味ネットワーク。
・記述論理。
・Guarinoの形式的オントロジー。
そして記述論理が最も有望とされている。
32:１３２人目の素数さん
12/01/03 10:37:30.87
>>30
読んで字の如くそのまんま。
自然数が与えられたとき、それが公理系Tの公理のゲーデル数であるか否かが
帰納的に決定可能（つまり計算機で判定可能）ということ。
33:スレタイスレ446
12/01/03 10:44:29.64
>>31
訂正：
様相論理は可能世界を用いて内包を使う意図があって導入された。
↓
可能世界を用いて内包を使う意図があって様相論理へ導入された。
34:１３２人目の素数さん
12/01/03 11:45:06.48
>>32
ありがとうございます。
もうひとつ質問ですが、Uは公理系Tの再帰的拡大であると言われたとき、TとUのゲーデル数の定め方は異なっていても
よいのですか？
35:１３２人目の素数さん
12/01/03 17:50:48.78
>>34
Uは公理系Tの再帰的拡大であると言われたとき、ゲーデル数での表現はまだ定めてないような。
だから32も正確ではなくて「自然数が与えられたとき、それが公理系Tの公理のゲーデル数であるか否かが帰納的に決定可能」
なようにゲーデル数化できる公理系、というべきだね。
36:１３２人目の素数さん
12/01/03 18:00:02.51
>>31
>様相論理は可能世界を用いて内包を使う意図があって導入された。
クリプケが可能世界意味論を提案するずっと前から、様相論理はあるわけなんだが。
37:１３２人目の素数さん
12/01/03 18:07:31.10
>>35
なるほど。ありがとうございます。
38:スレタイスレ446
12/01/03 18:50:46.99
>>36
>>33
39:１３２人目の素数さん
12/01/03 19:03:29.31
>可能世界を用いて内包を使う意図があって様相論理へ導入された。
何が導入されたん？
40:１３２人目の素数さん
12/01/03 19:13:06.29
>>24（＝前スレ803？）
直観主義の非論理的公理ってどういうものがあるんですか？
41:スレタイスレ446
12/01/03 19:32:45.00
>>39
なんだか文章がおかしくなったのでもう一度。
「クリプキが可能世界を導入して内包を含む文を解釈することに成功した。」
>>31
訂正：
＞透明性（代入法則が成り立たない）を持たない文
↓
透明性（代入規則による外延交換が成り立つ）を持たない文
42:１３２人目の素数さん
12/01/03 19:40:50.28
>>41
透明性といっているってことは、一階術語様相論理の話をしている？
それなら通常の一階述語論理を断片として持つのだから、
数学や集合論を記述することなんて訳ないのでは？
43:１３２人目の素数さん
12/01/03 19:56:26.21
誤字訂正：
一階術語様相論理
↓
一階述語様相論理
44:１３２人目の素数さん
12/01/03 20:13:11.86
16が言っているのは、以前ちょっと流行った STS (Structural Theory of Sets) のことだと思う。
URLﾘﾝｸ(www.blutner.de)
様相言語は量記号を持たない（量記号の有無は議論には影響しない）ようだから、
命題様相論理で集合論を記述していると考えていい。
45:１３２人目の素数さん
12/01/03 20:20:55.15
>>31
＞今の計算機の原理が変わらない限り一階論理がなくなることはない。
今の計算機の原理と一階論理にはどんな関係があるの？
量子計算機とかDNA計算機とかだと、一階論理ではなくなる？
46:スレタイスレ446
12/01/03 20:41:38.99
>>42
透明性はエレクトラのパラドクスの発生や宵の明星・明けの明星の問題の話です。
論理へクリプキ意味論を導入すると、
文は一般に内包で、意味論側で可能世界が与えられると外延と解釈できるようになります。
このような不透明な体系、例えば様相論理は数学の記述は難しいとクワインが指摘したのです。
数学は2つの対象が等しいならば、両者で同じことが成り立つという客観（神の視点）を持つからです。
一方で普段通りに、モデル理論を意味論、1階論理を構文論とすれば、
自然言語の透明性が保存され外延交換が成り立ちます。
（実はその後、クワインは透明性を持つ体系での厳密科学の形式化を断念していますが...）
勿論自明なやり方でなら一階論理を含む様相論理で数学を書くことは可能ですが。
47:１３２人目の素数さん
12/01/03 20:59:09.91
>>46
内包と外延の分析に有益というのは、様相論理の利点の一つだろうが、
それだけが様相論理を評価する場合の唯一の視点というわけではない。
Baltag のSTSでは、また別の視点が強調されている。
そこで「数学や一階論理の様な神の視点の立場に合致しなかった」と評価するのは
ちとずれているんではあるまいか？
48:１３２人目の素数さん
12/01/03 21:19:02.83
>>16
>そのうち、記述論理が一階述語論理にとって替わるのかな？
>様相論理を記述論理に直して再チャレンジってことかな？
えー？記述論理って述語論理のちゃちなサブセットだろ？
49:１３２人目の素数さん
12/01/03 21:23:21.74
あちゃー、隔離スレではトンデモ学者に矢田部さんが味方認定されちゃってる。可哀想に。
50:１３２人目の素数さん
12/01/03 21:29:49.63
AMC（空でない集合たちの族に対して、それらの各々の非空有限部分集合の族が取れる、という公理）から
選択公理をどうやって証明したらいいのか分かりません。
外延性公理と正則性公理が必要なのだそうですが、誰か分かる方いますか？
51:１３２人目の素数さん
12/01/03 21:51:52.07
>>49
俺も何度か経験あるけど、お前のトンデモ理論を俺が支持しているかのように書くのはやめてくれ、と思う。
ツワモノになると、自分のトンデモ理論が正しいと公式に表明してくれ、とかメール送ってくるし。
52:スレタイスレ446
12/01/03 22:01:09.38
>>44>>47
STSは全く知りませんでしたね。だとすると誤読でしたね。
確かにクリプキの指示とかの話は内包論理に関する様相論理の話でしかない。
>>45
＞今の計算機の原理と一階論理にはどんな関係があるの？
一階論理程度の表現能力があれば十分だというところですね。
ホーン節はじめ分解原理・SLD導出・失敗による否定・エルブランモデル。
論理プログラムは部分帰納関数の表現まで使える...。
＞量子計算機とかDNA計算機とかだと、一階論理ではなくなる？
拡張する必要はあるでしょうね。
53:１３２人目の素数さん
12/01/03 22:35:03.01
>>40
直観主義ブラウワーと形式主義ヒルベルトの論争があったように、
直観主義は本来は形式化に反対するものなので、
その論理の部分とか非論理的公理とかいうのはおかしいと言えばおかしいのだけど、
現代的視点で形式化した場合に、と断りを付けておくけど：
有名どころは、
扇定理(Fan Theorem) と
連続選択公理(実数の選択関数で連続なものが取れる)
かな。これだけでブラウワーの数学が形式化できるのか、
もっと公理が必要なのかはよく知らない。
54:１３２人目の素数さん
12/01/03 22:40:31.56
補足すると、連続選択公理からは「実数値関数はすべて連続である」という定理が出る。
この定理は勿論、古典論理（とそんなに強くない数学的公理）上では矛盾するけれど。
だから、直観主義は、排中律を拒否して論理を弱めているので、古典論理より定理が少なくなる、というのはある意味嘘。
弱めているのは論理の部分だけで、非論理的公理の部分は一方が他方より強いとか弱いとかって関係にはない。
55:ただのバカ
12/01/03 22:47:42.05
これからの論理は直観にいくよりも矛盾許容論理。
定理ごっそり増える
56:１３２人目の素数さん
12/01/03 22:51:18.72
>>52
>＞今の計算機の原理と一階論理にはどんな関係があるの？
>一階論理程度の表現能力があれば十分だというところですね。
十分というだけで、必要でないのなら、
一階論理の断片となる論理がとって替わる可能性があるってことでは？
>今の計算機の原理が変わらない限り一階論理がなくなることはない。
と辻褄があっていない。
57:１３２人目の素数さん
12/01/03 23:00:43.67
>>27
Every two elementarily equivalent models have isomorphic ultrapowers
Saharon Shelah
Israel Journal of Mathematics
Volume 10, Number 2, 224-233, DOI: 10.1007/BF02771574
URLﾘﾝｸ(www.springerlink.com)
58:スレタイスレ446
12/01/03 23:11:44.90
>>56
もちろんここで言う一階論理はある程度の断片や拡張も含めた意味で。
ホーン節の分解システムも一階論理の断片だったりするし。
逆に一階論理に推移閉包や述語定数を添加する場合もある。
ペアノ算術の関数や述語をダイレクトに添加した例もよく見る。
ソフト側では、それ以上のファジーや適切論理なんかまで使うけど。
59:１３２人目の素数さん
12/01/03 23:12:31.51
>>57
>>57さんへの文句ではないが、
なんでリンク先は出版年を明記してないんだろう？
60:１３２人目の素数さん
12/01/03 23:14:32.92
>もちろんここで言う一階論理はある程度の断片や拡張も含めた意味で。
それ言ったら様相論理も含まれるやん。一階論理はある程度の断片だし。
一階論理の代替になれなかった様相論理の次の候補、という話してるのに。
61:１３２人目の素数さん
12/01/03 23:19:43.61
低次元な議論は
も う や め て く れ
62:１３２人目の素数さん
12/01/03 23:22:25.47
>>59
確かに不思議ですね。出版は1971年だそうです。
最初のページを見てみると、
この手の話は一般連続体仮説G.C.H.を仮定した結果が多いみたいですね。
概要でもGCHを使わずに、と強調していますし。
これなら置換公理を使っていても全然不思議ではありませんね。
63:スレタイスレ446
12/01/03 23:27:25.77
>>60
様相論理が一階論理の断片と考えられるといえばそうだけど、
わざわざ様相論理といったときは、大抵モーダルオペレータや
関係構造やらフレームやらを使用する意図があるという前提で。
（計算機で一階論理の述語や関数の引数を制限するのは別の理由。）
64:１３２人目の素数さん
12/01/03 23:55:11.91
>>62
選択公理や正則性公理も当然使われているだろうな。
65:１３２人目の素数さん
12/01/04 00:17:53.20
第二不完全性の証明は結局分かったんだろうか？
実際のところ、証明に必要な帰納法はΣ_1帰納法で十分だったの？
66:１３２人目の素数さん
12/01/04 00:22:44.64
>>55
ネタにマジレスかも知らんが、矛盾許容論理というと古典論理より弱い。
従って非論理的公理をいじらないのなら定理が増えるなんてことはあり得ない。
67:１３２人目の素数さん
12/01/04 01:10:08.95
こっちに現れるんだろうからコピペしとこ
999 ：１３２人目の素数さん：2012/01/03(火) 00:46:52.02
数理学厨は >>917, >>923 で皮肉られて言い返せなくなったと見えて、姿を消したな。
前回は、伝統を良しとして歴史的偶然を批判するっていう自己矛盾を指摘されて言い返せず、
暫く消えていたがそのうち何事もなかったように現れた。
今後もまたほとぼりがさめたと判断した頃に現れるのだろう、新スレに。
68:１３２人目の素数さん
12/01/04 01:44:23.59
>>57
その結果面白いね。
前スレで話題になっていた van Benthem's characterization theorem って、
ふたつの pointed model が modal equivalence であることと、
ultrafilter extension で bisimular であることが同値ってことだったけど、
一階述語論理にすると
ultrafilter extension → ultraproduct
bisimular → isomorphic
という類推ができる。それなのに様相論理では普通に証明できるのに、
一階述語論理については集合論的な公理が必要だとすると、不思議だねえ。
69:１３２人目の素数さん
12/01/04 02:14:16.13
>>36
天才と言われるクリプケが可能世界意味論を提案する前の様相論理は何を研究していたのか？
70:１３２人目の素数さん
12/01/04 02:28:24.73
>>54
ビショップの直観主義数学は、古典論理上の数学より弱いって聞いたけど
71:１３２人目の素数さん
12/01/04 04:21:21.24
ああ、僧正と橋々の構成的解析ね。
72:１３２人目の素数さん
12/01/04 05:08:22.74
橋々？僧正は Bishop のことだな。
73:スレタイスレ446
12/01/04 07:34:38.51
>>69
最初期はルイスやゲーデルやタルスキやマッキンゼーらが
シンタックスのみで研究していた。
ただし関係構造が必要なのは知られていて、
カルナップの意味論なんかが考案された。
既にプライアーの時相論理が開発されていて、
自然数をドメインとして＜を関係として持つモデルがあった。
50年代の終わりにようやくクリプキ構造の完全性定理が出来る。
74:１３２人目の素数さん
12/01/04 08:33:11.69
>>69
様相論理の体系で S4 とか S5 とかはあるのに、S1, S2, S3 がないのは不思議だよね？
これはクリプキ意味論以前から様相論理が研究されていた名残り。
S1, S2, S3 は通常の可能世界意味論を持たない。
少し変更を加えれば（非正則世界を許す）S2 と S3 は完全な意味論が可能世界意味論で作れる。
しかし S1 はどうやってもその手の意味論は与えられなかったはず、詳しくは知らない。
あと、S6 以降の体系も世の中にはある。
75:１３２人目の素数さん
12/01/04 09:05:15.50
>>74
S1 から始まる体系の系列は、Lewis が厳密内意（論理学スレで話題になってた）の研究で提案したもので、
様相論理の研究と言ってしまっていいのかは疑問。
もっとも A ⊰ B を □(A→B) と、逆に □A を ⊥⊰ A と理解することで、
厳密内意と様相は同じものとみなしていいんだけどね。
（少なくとも S2 以上は。S1 はどうだったか忘れた。）
ある意味、適切論理の先行研究ともいえる。
76:１３２人目の素数さん
12/01/04 09:25:30.07
俺は>>68はいいこと言ったと思う。こういうものの見方が必要だと思うんだ。
だからこそ、哲学はこのスレから出て行けとか、哲学的論理学はスレから分けるべきだとか、
そういう「排除の論理」には賛成しかねる。数学系の論理学と哲学系のそれが、
近いことをやっていて、スレが一緒で問題がないのなら、そのまま一緒にやっていくのがいい。
「排除の論理」の人々は、分類フリークっていうか分類することが目的になってると思うんだよね。
77:１３２人目の素数さん
12/01/04 09:37:31.81
>>75
>逆に □A を ⊥⊰ A と理解することで
T ⊰ A じゃなくて？
>>76
禿堂。数学系の論理学と哲学系の論理学だけじゃなくて、計算機系の論理学もな。
78:１３２人目の素数さん
12/01/04 10:00:03.96
おっと、ここで「数学じゃない」厨が現れて、
哲学なんかと仲良くしようというなら哲学板へスレごと移動しる！
とか言い出すに一票。
79:１３２人目の素数さん
12/01/04 10:01:48.99
>>77
>T ⊰ A じゃなくて？
仰るとおりでございます。
80:スレタイスレ446
12/01/04 11:26:40.86
>>74
またS6以降はどう決まるのでしょうか？
81:１３２人目の素数さん
12/01/04 14:07:47.35
我々エイリアンからすれば、
おまいら地球人のやってるコトは全て児戯。
82:１３２人目の素数さん
12/01/04 14:36:24.27
今時のプログラミング言語の型理論の基礎はSystem F、
要するに二階λ計算、大体二階直観論理相当。
一階述語論理で十分なんて馬鹿げてる。
動作原理としてはノイマン型でロジックとは関係ないし。
83:１３２人目の素数さん
12/01/04 15:05:06.21
>>80
S6:
URLﾘﾝｸ(home.utah.edu)
S7:
URLﾘﾝｸ(home.utah.edu)
S8:
URLﾘﾝｸ(home.utah.edu)
S9:
URLﾘﾝｸ(home.utah.edu)
84:スレタイスレ446
12/01/04 16:02:50.44
>>82
つまりこれまでの論理プログラムなどのハード計算が使い物にならないので、
非古典論理や型の理論などのソフト計算が導入されている。ということでしょうか？
＞動作原理としてはノイマン型でロジックとは関係ないし。
チューリング機械であるという見方の一方でブール代数を扱うという見方もあるのではないでしょうか？
人の推論と計算機の間にロジックが必要なのではないでしょうか？
>>83
非常に便利です。
これらはどの様相論理の本にも載っていませんでした。
85:スレタイスレ446
12/01/04 16:05:56.20
訂正：
型理論はソフト計算とは無関係でしょうが...。
86:１３２人目の素数さん
12/01/04 19:03:32.23
命題論理とスイッチ回路の初等的過ぎる疑問::
ラッセル方式でNORだけの公理は割とみじかく書き下しできるのに
NANDだけだといやになるほど長くなる
一方
回路設計をNAND素子オンリーで組むのはラクチンなのに
NOR素子オンリーで組むのはなぜか苦労する（手間が時間が）
・・・トンデモ本「数理示申學序説の前書き」より自分で引用
これ数学SFに使おうと思いますが玄人の眼からみると幼すぎますか
できれば評価レスキボンヌ
87:１３２人目の素数さん
12/01/04 19:15:18.41
>>84
ハード計算、ソフト計算ってのが何を意味してるかわからん。
論理プログラムとの関係もわからん。
88:スレタイスレ446
12/01/04 21:45:22.34
>>87
ハード計算が計算機の立場の情報処理技術、
ソフト計算が人間の立場の情報処理技術。
論理について考えると、
命題論理・一階述語論理はハード計算。
様相論理・時相論理・多値論理・関係論理・ﾊﾟﾗｺﾝｼｽﾃﾝﾄ論理・曖昧論理・
ファジー論理はソフト計算。
だから命題論理や一階述語論理の応用である論理プログラムもハード計算になる。
89:１３２人目の素数さん
12/01/04 22:20:43.07
>>88
あんたはやっぱり少し見えてる。
>人と計算機の間にロジック
について差し支えない範囲で語ってくれんか？
90:スレタイスレ446
12/01/04 23:35:52.71
>>89
そんなに詳しく考えているのではないですが、
計算機の内部でブール代数に基くビット演算が起こっていると考えられますが、
（実際のハードウェアがどうなっているかは知りませんが、）
これを厳密かつ人が扱いやすく定義し理論的保障を与えるために、
形式的言語として命題論理のような論理演算システムが必要と考えています。
（もちろん状態遷移系でもチューリング機械でもレジスター機械でも何を駆使してもよいのですが。）
とりわけ一階論理は人の推論に比較的合っているうえにそこそこの表現力も持っているのではないでしょうか？
もちろんプログラムなどの側で有用なのは言うまでもないでしょう。
91:１３２人目の素数さん
12/01/04 23:37:10.93
ばかだろ
92:１３２人目の素数さん
12/01/04 23:43:09.11
>>31
>今の計算機の原理が変わらない限り一階論理がなくなることはない。
これは一階論理の代わりにチューリングマシンやλ演算でも良いのですよね？
>>88
ハード計算とソフト計算はあなたが考えた独自用語ですよね？
ソフト計算とはヒューリスティクスという意味でしょうか？
>だから命題論理や一階述語論理の応用である論理プログラムもハード計算になる。
チューリング等価なプログラミング言語であるprologで
あなたが示したすべての論理をソフトウェアとして実現できます。
だから一階述語論理の応用はハード計算とは言えません。
ソフト計算に分類した論理を使えばヒューリスティクスを自然に表現できる、
という主張なら納得できるのですが。
93:スレタイスレ446
12/01/04 23:55:11.56
>>92
＞これは一階論理の代わりにチューリングマシンやλ演算でも良いのですよね？
大抵は組み合わせて使います。
＞ハード計算とソフト計算はあなたが考えた独自用語ですよね？
＞ソフト計算とはヒューリスティクスという意味でしょうか？
Soft computingとHard computingのことですね。
＞チューリング等価なプログラミング言語であるprologで
＞あなたが示したすべての論理をソフトウェアとして実現できます。
例えばそのProlog自体の基礎となっているのが論理プログラムなどという話しですね。
94:１３２人目の素数さん
12/01/05 08:51:28.00
>>83
番号が大きいほうだけではなくて、S1 より弱い S0 なんてのもあるのか。
そのサイトは便利だ、㌧クス
95:１３２人目の素数さん
12/01/05 09:06:25.42
>>74
非正則世界ってなんですか？
96:１３２人目の素数さん
12/01/05 14:57:03.04
Sπ
97:１３２人目の素数さん
12/01/05 19:02:59.82
>>95
非正規世界(non-normal world)のことだろ。
数学用語ではnormalは普通「正規」と訳される。「正則」はregularね。
非正規世界では、□Aという形の論理式は問答無用で偽とする。
それ以外のconnectiveの意味論は通常通りとする。
正規世界では通常のクリプキ意味論。
S2やS3はこんな意味論で完全になるそうだ。
98:１３２人目の素数さん
12/01/05 19:18:28.07
>>83
とりあえず、このリストは命題論理だけでもかなり漏れている。
有名なのを列挙してみると
Alt_n、Grz、Triv、Verum、A*、Dum、K4BW_n、K4BD_n、K4_n,m
、Ord_t、E_t、O_n、RD、LD、Z_t、Ds_n、Q_t、R_t、Rd_t、Lin
、CSM0、CSM1、CSM2、CSM3、NB1、NB2、Int(＝ρS4)
、For、Cl(＝ρS5)、SmL、KC(＝ρS4.2)、LC(＝ρS4.3)、SL、KP、BD_n
、BW_n、BTW_n、T_n、B_n、NL_n、FS、MIPC、IntK...。
さらに様相システムは、先頭にρ、τ、σが付くし、
後ろには-や、添加したオペレータが付き得る。
また各システムで、S4ｘS4や(Grz)^nのように
2つ以上のシステム内のオペレータが干渉し合う体系も起こり得る。
99:１３２人目の素数さん
12/01/05 19:23:55.92
誰も「すべてを網羅している」なんて言ってないよーな
100:１３２人目の素数さん
12/01/05 19:34:21.83
Vopěnka cardinal ってなんでしょうか？
Vopěnka principle (VP) は前スレで話題になっていましたが。
101:１３２人目の素数さん
12/01/05 19:40:15.42
様相論理も部分構造論理も、幾らでも新たな体系を作ろうと思えば作れる。
研究と称して、そういった体系のお決まりの性質（完全性、有限モデル性、決定可能性、カット除去等々）を
これまたお決まりの方法で証明する、というオリジナリティのかけらもない論文が多すぎる。
よってそれらをすべて網羅する必要があるとは思われない。
102:１３２人目の素数さん
12/01/05 20:20:30.73
>>76
分類フリークといえば、少し前に一人で樹形図書きまくってたアホがいたな。
同一人物かね。
103:１３２人目の素数さん
12/01/05 21:17:22.87
何それｗｗｗ
ちょっと見てみたいｗ
104:スレタイスレ446
12/01/05 21:17:32.98
>>99>>101
＞幾らでも新たな体系を作ろうと思えば作れる。
その通りです。
ただし、>>98に掲載されている体系は、
（恐らくHandbook Of Philosophical Logicの３巻からの引用。）
ほとんどがK4やS4の拡張で、
複雑なペトリネット・公理的集合論・線形時相論理などに関する
統一的な研究に由来するようですね。
105:１３２人目の素数さん
12/01/05 21:18:41.38
数セミの渕野先生の文章読んだけど、何か苫米地英人っぽい偏狭さを感じる。
106:１３２人目の素数さん
12/01/05 21:19:47.51
>>70
通常「直観主義数学」と言えばブラウワーの数学（を形式化したもの）を指すでしょ。
ビショップとかマルティンレーフとか、それ以外の直観主義論理上の理論は構成主義と呼ぶと思う。
論理を直観主義にしたものすべてを直観主義数学と呼ぶのは、浅学の窮みｗｗ
107:１３２人目の素数さん
12/01/05 21:37:14.88
F先生が偏狭なのはいまさら(ry
108:１３２人目の素数さん
12/01/05 22:00:50.90
>>103
こんなの↓
980 : 半角混ぜるとずれるので、 : 2011/06/28(火) 21:22:21.01
数理論理学━┳━逆数学━━┳━高階逆数学
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━無限ゲーム決定理論
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━構成的逆数学
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━計算論的逆数学
＿＿＿＿＿＿┣━非古典論理━┳━様相論理
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━部分構造論理
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━代数的論理
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━高階述語論理
＿＿＿＿＿＿┣━公理的集合論━┳━連続体仮説━━強制法・反復強制法
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━SH・◇・CH・ADなど
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━内部モデル・決定性公理
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━巨大基数・超巨大基数・Rの基数不変量
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━無限集合組合せ理論
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━PCF理論
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━Generic Multiverses・Ω-論理
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━集合論その他(GB,NF,KP)
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━推移的クラスの微細構造論
109:１３２人目の素数さん
12/01/05 22:01:10.29
＿＿＿＿＿＿┣━モデル理論━┳━幾何学的モデル論
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━超準的数学
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━ダイアレクティカ圏・HyperDoctrine
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━真の算術など
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━有限モデル理論
＿＿＿＿＿＿┣━再帰理論━━┳━計算量理論━┳━記述計算量理論
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┃＿＿＿＿＿＿＿┗━次数理論━━非可解性次数
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━型付ラムダ計算
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━順序数上の再帰理論・高階再帰論
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━解析的階層
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━コルモロゴフ複雑性・チャイティン数
＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━抽象機械
＿＿＿＿＿＿┗━証明論━━┳━定理自動証明
＿＿＿＿＿＿＿＿＿＿＿＿＿＿＿┣━新井先生とかRathjenの業績
＿＿＿＿＿＿＿＿＿＿＿＿＿＿＿┗━構成的数学━━構成的型理論━━直観主義型理論
110:１３２人目の素数さん
12/01/05 22:08:14.80
>>105
どこらへんで偏狭さを感じたんだい？
111:１３２人目の素数さん
12/01/05 22:31:12.35
>>104
>ほとんどがK4やS4の拡張で、
>複雑なペトリネット・公理的集合論・線形時相論理などに関する
>統一的な研究に由来するようですね。
統一的な研究に由来する体系なのに、
名称に体系だった趣がまるで感じられないのはなぜ？
112:１３２人目の素数さん
12/01/05 22:41:31.65
人の名前から付いてたり
公理を表す文字だったり
体系の性質に注目して居たりするからでは
113:１３２人目の素数さん
12/01/05 22:50:44.20
「新井先生とかRathjenの業績」って分野の名称だったんだｗ
114:１３２人目の素数さん
12/01/05 22:53:21.20
>>113
定義上、二人しか結果の出せない分野だな。
つーかそういう瑣末な問題以前の問題が多すぎる、その樹形図は。
115:１３２人目の素数さん
12/01/05 22:57:54.23
>>112
自分で幾つもの体系を提案するのに、異なる名付け方法を採用するか？
一人（一グループ）の人間が、一つの研究の中で、いくつものの体系の名称を付けるのなら、
統一的な名前の付け方を採用するのが普通ではないんだろうか？
116:１３２人目の素数さん
12/01/06 00:53:27.05
>>104
> （恐らくHandbook Of Philosophical Logicの３巻からの引用。）
全４巻の旧版の方？ それとも未だ未完結で全１８？巻の新版の方？
117:１３２人目の素数さん
12/01/06 02:11:00.43
>>114
逆に言えばその二人はその分野以外では業績が出せない。
なぜならどんな業績を出しても「新井先生とかRathjenの業績」という分類になるから。
118:１３２人目の素数さん
12/01/06 03:15:34.28
アホのしかもだいぶ昔のレスを肴に、よーもまーそこまで下らん話ができるもんだな。
119:１３２人目の素数さん
12/01/06 04:40:22.16
またF先生祭になる伊予柑
120:スレタイスレ446
12/01/06 07:09:34.47
>>116
新版の方。
２章の様相論理の発展。
121:１３２人目の素数さん
12/01/06 07:17:36.41
そこには非正規世界のある可能世界意味論とか書いてありますか？
122:スレタイスレ446
12/01/06 08:01:41.06
>>121
載っている。
非正規世界(non-normal world)って名称ではないけど。
あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、
記述されている。
このシステムのクラスNExt(L)自体の順序構造も調べられているよう。
123:１３２人目の素数さん
12/01/06 08:02:05.66
ファジー論理のハンドブックも進行中みたいだね。
URLﾘﾝｸ(www.mathfuzzlog.org)
124:１３２人目の素数さん
12/01/06 08:30:55.97
>あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、
>記述されている。
記述する、の主語はなんでしょう？
125:１３２人目の素数さん
12/01/06 08:50:41.10
>非正規世界(non-normal world)って名称ではないけど。
>あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、
>記述されている。
あのう、非正規世界というのは、正規でない体系(S2, S3など)を扱う為に導入したから
名称も非正規世界ということになったわけでして。
126:１３２人目の素数さん
12/01/06 09:17:59.72
>>100
Vopěnka 関連は最近流行っているみたい。
Archive for Mathematical Logic では、
2011年だけで2本も（少ない？）関連論文が出ている。
no access
Indestructibility of Vopěnka’s Principle
Andrew D. Brooke-Taylor
2011, Volume 50, Numbers 5-6, Pages 515-529
URLﾘﾝｸ(www.springerlink.com)
C^{(n)}-cardinals
Joan Bagaria
Online First, 22 December 2011
URLﾘﾝｸ(www.springerlink.com)
127:１３２人目の素数さん
12/01/06 10:28:49.07
Vopenka とか膨大基数とか拡張可能とか C^{(n)}-基数とか、色々な基数が出てくるけど、
その間の関係ってどうなっているの？
誰か関係を表にした奴へのリンクとか貼ってくれないかな？
128:１３２人目の素数さん
12/01/06 12:41:03.21
前スレの
935 ：１３２人目の素数さん
Vopěnka's principle（VP）:="Cが言語のモデルの宇宙としてのプロパークラスとしたとき、
Cの2つの要素を任意にとると、片方がもう片方に初等埋め込み可能"
「VP⇒拡張可能基数」が成り立つからかなり強い仮定。
また膨大基数kを仮定すると、V_k（累積的階層）がVPのモデルになる。
が累積的階層であるとき、この階層のランクの添え字の基数がVopěnka基数。
に対して
958 ：１３２人目の素数さん：2012/01/02(月) 13:24:57.89
>>931
>Vopěnka's principle
でググっていたら
URLﾘﾝｸ(www.imub.ub.es)
が出て来た。 VP に同値な命題がいくつか書いてあり、
さらに WVP なる物もあった。このなかで一つ分からないのが
accessible category の定義だ。
accessible ordinal (cardinal) と似たような感じだとは思うが
解説希望
と質問したのだが、未だに回答が無い。
129:１３２人目の素数さん
12/01/06 18:48:10.19
970 ：958：2012/01/02(月) 22:32:22.66
こに質問に誰も答えられないと云う事は・・・
975 ：１３２人目の素数さん：2012/01/02(月) 22:43:55.95
>>970
そんなローカルな研究解説できる人間などほとんどいない。
あなたが調べられる以上の情報は期待できないだろう。
Jech本にもVPまでしかのっとらんしな
130:スレタイスレ446
12/01/06 19:02:30.54
>>124
主語は集合論だと思いますよ、明文化されてはいませんが。
NExt(L)は様相システムLの正規に拡張したシステム全体の集合族。
公理に関して順序関係を定義していくと、完備分配束が出来たりする。
>>125
いえ、Handbook Of Philosophical Logicの３巻でnon-normal worldって名称が使われていないという意味です。
131:１３２人目の素数さん
12/01/06 20:07:47.44
>>130
122のレスは
>載っている。
>非正規世界(non-normal world)って名称ではないけど。
という部分と、
>あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、
>記述されている。
>このシステムのクラスNExt(L)自体の順序構造も調べられているよう。
の部分は完全に別の話をしているという理解でいいの？
同じ話題だとすると、正規でない L について「正規なまま拡張」なんてできない訳で、
何言っているかやっぱり分からんのだ。
132:１３２人目の素数さん
12/01/06 20:16:52.31
>主語は集合論だと思いますよ、明文化されてはいませんが。
自分の発言について「思いますよ」とは恐れ入るな。
133:１３２人目の素数さん
12/01/06 20:51:57.69
>>132
NExt(L)で記述したのは別人だから別におかしくないのでは？
134:１３２人目の素数さん
12/01/06 20:57:57.94
「あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、
記述されている。」と書いたのはスレタイスレ446氏だろ？偽者なのか？
自分で「記述されている」と言っておいてその主語が何かについて
「集合論だと思いますよ」と書いたのも彼／彼女だろう。
135:スレタイスレ446
12/01/06 21:19:27.32
>>131
＞の部分は完全に別の話をしているという理解でいいの？
そう。改行していないだけ。
>>132
件の本に記述されているのは確か。
しかし、どういった理論（少なくとも集合が扱える）に基いているか不明だということ。
136:１３２人目の素数さん
12/01/06 21:33:31.67
>>128
すべての質問に回答が付くと思うな。
スルーされたくなければスルーされないような書き方を研究するんだな。
137:１３２人目の素数さん
12/01/06 21:59:17.28
１階述語論理の証明体系について皆さんにお聞きしたいことがあります。
全称化：「A→Bから∀ｘA→Bが出てくる（ただしｘはBに自由に現れない）」という推論規則がありますが、
これから理論Tについて「T|-AならばT|-∀xA」を示すにはどうすればいいのでしょう。
命題論理のトートロジーや∀xA(x)→A(t)（tは代入可能な項）、等号の公理は論理公理に入っているものとしてください。
三段論法も推論規則に入っています。
138:１３２人目の素数さん
12/01/06 22:28:15.65
>>128
accessible ordinal (cardinal) の解説希望。
139:１３２人目の素数さん
12/01/06 23:29:10.95
>>135
そういう解説がないと全く読解不能の文章を書く能力ってどうやって身につけられるの？
前スレの「考える人」と同じ臭いを感じる。
結局、何が記述されていると言っていたワケ？
140:１３２人目の素数さん
12/01/06 23:55:13.51
知識も話題も豊富なスレタイスレ446氏は、こまめにレスを返したりする性格も相俟って
このスレの主になりつつあるわけだけど、
>>139が指摘しているようなささっと書いたレスが意味不明な場合があって
（単なるタイポだろうけど、それがときとして致命的に読みにくくなる）
そこを直さないと主としての風格というか権威は得られないと思う。
141:１３２人目の素数さん
12/01/07 04:36:23.17
アスペ＝マツシンについて詳しく知りたい方へ
URLﾘﾝｸ(logsoku.com)
142:１３２人目の素数さん
12/01/07 06:21:44.06
たかが２ｃｈのスレで権威ねえ。
言いたいことは分からんでもないがｗ
143:１３２人目の素数さん
12/01/07 08:38:42.87
>>137
少なくとも書かれている規則からだけでは無理。
何故なら ∀ｘA という形の論理式を問答無用で偽と解釈する
（それ以外は通常の解釈をする）意味論を考えると、
それら規則はすべて真であることを保存するが、
証明しようとしているのは真を保存しない。
何か忘れている規則があるはず。
144:１３２人目の素数さん
12/01/07 09:05:13.62
>>137
全称化は向きが逆だろ。
「A→BからA→∀ｘBが出る（ただしｘはAに自由に現れない）」
T|-AならT|-￢∀ｘA→A
全称化よりT|-￢∀ｘA→∀ｘA
よってT|-∀ｘA
145:１３２人目の素数さん
12/01/07 09:48:30.24
>>143
すみません、「A→BからA→∀ｘ」の間違いでした。
>>144
>T|-AならT|-￢∀ｘA→A
この部分と
>よってT|-∀ｘA
この部分がよく分かりません。もしよろしければ詳しく教えて下さいませんか？
146:１３２人目の素数さん
12/01/07 16:33:08.81
本スレッド>>1の
「数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ」
は全くの誤りとして論破されました。
本スレッドは反数学的トンデモスレッドとして閉鎖されますので
以下のスレッドに移動願います。
数理論理学（数学基礎論） その11
ｽﾚﾘﾝｸ(math板)
147:１３２人目の素数さん
12/01/07 16:54:44.05
隔離スレから出てきちゃダメでしょ
148:１３２人目の素数さん
12/01/07 17:33:30.28
このスレ自身が数学板の中では 哲ヲタやキチガイ専用の隔離スレだったりしてな
149:１３２人目の素数さん
12/01/07 20:06:39.51
劣等感をはき散らすのはみっともない。
150:１３２人目の素数さん
12/01/07 20:08:39.18
>>148
わかっていても言っちゃいけないことがある
151:１３２人目の素数さん
12/01/07 20:13:00.92
>>150
大学の教員はそれをやる非常識人が多いんだよ。
そんな連中が学生相手に社会人としての常識を説いたりするから笑える。
152:１３２人目の素数さん
12/01/07 20:32:52.31
>>141のレス見て発狂したんだろ。
153:１３２人目の素数さん
12/01/07 20:58:34.99
閉鎖されますので、って閉鎖する権限持っているの？
こういう妄想してしまうのは、やっぱり人格障害なんだろうな。
154:１３２人目の素数さん
12/01/07 21:11:03.25
>>153
何をいまさらｗｗｗ
155:スレタイスレ446
12/01/07 22:20:46.89
>>139
＞そういう解説がないと全く読解不能の文章を書く能力ってどうやって身につけられるの？
掲示板を読んでいる人間が、隣に座って同じ本を一緒に読んでいる様を想像して書きます。
また、投稿欄に書いた文章を決して読み返さないこと。
（レス数を減らしてじっくり書き込む時間をとるのがベストなのかもしれない。）
＞前スレの「考える人」と同じ臭いを感じる。
確かに文体が似ていますね。
考える人（＝考えない人）というコテハンは、このスレのその5辺りから時折出没していますよ。
>>140
以後、レスの数は減らします。
156:１３２人目の素数さん
12/01/07 23:18:50.20
>>155
本を読んだけど理解できない人に解説するつもりで書いていて、
まだ読んでない人に自分のレスが理解できるか考えてなかったという事ですね。
その本をまだ読んでいないから内容を聞いている、と気がつくべきだと思います。
157:１３２人目の素数さん
12/01/07 23:46:45.99
>>156
お前さんも文章を推敲した方がいい
158:横
12/01/07 23:49:02.64
>>156
> 156 名前：１３２人目の素数さん [sage]： 2012/01/07(土) 23:18:50.20
> >>155
あなたは
> 本を読んだけど理解できない人に解説するつもりで書いていて、
> まだ読んでない人に自分のレスが理解できるか考えてなかったという事ですね。
と私は思います。
あなたは、わたしが
> その本をまだ読んでいないから内容を聞いている、と気がつくべきだと思います。
159:１３２人目の素数さん
12/01/08 02:20:00.10
>>153
削除依頼が通ると思っているんだろ。
503 ：数学板住人：2012/01/03(火) 08:04:24.00 HOST:36-2-122-83.saitama.ap.gmo-isp.jp<8080><3128><8000><1080>[36.2.122.83]
削除対象アドレス：
ｽﾚﾘﾝｸ(math板)
削除理由・詳細・その他：
数理論理学（数学基礎論） その11
ｽﾚﾘﾝｸ(math板)
と重複しているため削除願います。
ちなみに同じく埼玉のマツシンと思われる人物が
498 ：数理論理学者：2011/10/30(日) 09:40:31.00 HOST:d180.GsaitamaFL22.vectant.ne.jp<8080><3128><8000><1080>[116.91.89.180]
削除対象アドレス：
ｽﾚﾘﾝｸ(math板)
削除理由・詳細・その他：
スレッドのタイトルについて審議中、
合意案を無視して勝手に立てられた為。
タイトル審議スレ
数学基礎論スレのスレタイを決めるスレ
ｽﾚﾘﾝｸ(math板)
という削除依頼も出している。
自分で削除を依頼したスレの次スレを自称するのに勤しんでいるという矛盾に
本人は気づいていないようだな。
160:１３２人目の素数さん
12/01/08 04:37:01.40
２ちゃんのテンプレの"間違い"を正すより、
スタンフォード哲学事典(SEP)の"間違い"を正すほうが
よっぽど価値があることなんではないのか、マツシンよ。
SEPに特攻した武勇伝を期待しているよ。
161:１３２人目の素数さん
12/01/08 06:09:56.90
>>148は、>>67に反論できなくなって、捨て台詞ってこと？
気の利いたことが言えなくなった奴って痛々しいな。
162:１３２人目の素数さん
12/01/08 07:39:28.89
そうだな、ここのスレの間違いが訂正されてもここの住人くらいにしか恩恵はない。
スタンフォードの事典の誤りが訂正されたら、世界中に恩恵がある。
あの記事の誤りを訂正させたら世界中から賞賛の嵐だぜ、マツシンよ。
こんなスレのテンプレなんて下らんことにこだわらないで、世界に羽ばたこうぜ、世界のマツシン！
163:１３２人目の素数さん
12/01/08 08:26:44.00
マツシンあるいはアスペと呼ばれている人は、本気であんなこと言っているの？それともネタ？
基礎論の最初の目的（の一つ）がパラドックスの解決だったかということと、
基礎論の研究の結果実際にパラドックスを解決できたかという、
全く別の問題（一方は歴史の問題、もう一方は数学または哲学の問題）を混同していて、
自分でそれに気づかないって普通の感覚では理解不能なんですが。
やっぱりネタで言っているんではないのかと。
164:１３２人目の素数さん
12/01/08 08:41:00.87
ネタだと思ってるんなら、火傷しないようにスルーしとけ。
奴には関わらんでいた方が幸せ。
と、何度か奴と関わったことのある俺がいっとく。
165:１３２人目の素数さん
12/01/08 09:47:16.07
そのマツシンって奴、素人が！素人が！って言ってるけど、
自分はどんな論文出版しているんだ？誰かデータ持ってないかな？
区体論の人と同じく、自分も素人なのに虚勢張って言っているだけか？
166:１３２人目の素数さん
12/01/08 09:57:35.73
>>127
C^{(n)}-基数というのは、一種類の基数ではないようだよ。
可測、超強、超コンパクト、膨大、超膨大等々、
様々な巨大基数公理のC^{(n)}-版が考えられるということらしい。
167:１３２人目の素数さん
12/01/08 18:21:24.54
>>145
>>T|-AならT|-￢∀ｘA→A
>この部分と
T|-AならT∪{￢∀ｘA}|-Aで、演繹定理より。
>>よってT|-∀ｘA
>この部分がよく分かりません。もしよろしければ詳しく教えて下さいませんか？
排中律より∀ｘA∨￢∀ｘAだが、￢∀ｘAから∀ｘAがでるので、
どちらにしても∀ｘA。
168:１３２人目の素数さん
12/01/08 18:35:31.85
質問です。基礎論の大学院生は博士号取得までにいくつくらい論文を書くのが普通ですか？
169:１３２人目の素数さん
12/01/08 18:38:20.46
頭の悪そうな質問だな．
170:１３２人目の素数さん
12/01/08 18:49:00.93
数理論理学・数学基礎論というのが、もはや一つの分野とは言いがたくて、複数の分野の総称という感じ。
だから基礎論では一概にはいえなくて、分野ごとに論文の書きやすさは大きく異なる。
よく言われるのは、非古典論理や計算機科学寄りだと論文数が多くなる。
171:１３２人目の素数さん
12/01/08 19:11:56.59
>>155
また面白い話題を提供してくれることを期待しています。
172:１３２人目の素数さん
12/01/08 19:32:49.90
446氏が哲学板の論理学スレに出現してる
173:１３２人目の素数さん
12/01/08 19:43:41.45
スレタイスレ446氏にはこっちのスレで
「レシュニフスキーやネルソン・グッドマンなどの形式的オントロジーによるアプローチ」
の数学的側面を語ってもらいたいな。
174:１３２人目の素数さん
12/01/08 20:02:24.92
>>170
勝手な印象だけど、非古典論理と順序数解析とでは、
偏微分方程式と代数幾何くらい論文の多寡が違う気がするな。
175:137
12/01/08 20:04:19.57
>>167
>T|-AならT∪{￢∀ｘA}|-Aで、演繹定理より。
￢∀ｘAが閉論理式でない場合はT∪{￢∀ｘA}が閉論理式の集合で無くなってしまいますが、
それはよいのでしょうか？
176:１３２人目の素数さん
12/01/08 20:19:18.49
どんな公理系を考えているのか知らないけれど、
普通のシステムなら演繹定理に閉論理式という条件は要らないと思う。
177:137
12/01/08 20:34:26.18
そもそもT∪{￢∀ｘA}を公理系と考えることが出来ないのではないでしょうか？
公理系の定義は閉論理式の集合なので。
178:１３２人目の素数さん
12/01/08 21:07:09.40
公理系と考えることが出来なくとも |- は同様に定義できる。
179:１３２人目の素数さん
12/01/08 21:28:19.98
>>170
論文が量産される分野だと、引用される機会も多くなるから、
被引用回数とか G-index, H-index など各種指数も高くなる。
ただ基礎論系の雑誌は、その中でどこかの分野に特化したものは少ないので、
IF は分野の間で格差はそんなにないね。
一番 IF が高い基礎論系の雑誌は Annals of Pure and Applied Logic かね？
180:１３２人目の素数さん
12/01/08 21:47:34.48
>>170 "もはや"ではなくて、当初からそう。
それが数学ではないと言われるゆえん。
181:137
12/01/08 21:50:26.40
>>178
よく分かりました。閉論理式でないといけないと思い込んでいましたが、
意味論と関連付けて考えない限りは
閉論理式に縛られる必要はありませんでしたね。
182:１３２人目の素数さん
12/01/08 21:51:19.38
例えば、岩沢理論。基礎論よりも新しいのに
ずっと深くて重要な進歩がある分野。
これは複数の雑多な分野の総称ではない。
183:１３２人目の素数さん
12/01/08 21:51:50.31
>>67に反論できなくなった奴がまた現れたな。
「一つの分野とは言いがたい」から「数学ではない」って、
さすが追い込まれた奴の発想というか論理展開は独創性溢れてるなｗｗ
184:１３２人目の素数さん
12/01/08 21:54:14.52
>>180 いや、それでも最初期は大きな野望もあって
一つの分野ではあった。しかし、ゲーデル以後、そういった
大きな野望はなくなって、堕落してしまった。
185:１３２人目の素数さん
12/01/08 21:54:37.82
はいはい、また岩澤理論ね、えーとなんだっけ？暗号に応用できるんだっけ？
よくわからないなー。なんにしても>>67に言い返せないのかなあ？
186:１３２人目の素数さん
12/01/08 21:59:12.38
>>183
67って、全然基礎論擁護になっていないじゃん。引用が引用されてて
わけわからん
ちゃんと書きなよ
187:１３２人目の素数さん
12/01/08 22:01:30.82
言い返せってw
あのね、そういうセリフはディフェンディングチャンピオンのセリフよ。
傍流なんだから、打って出ないでいたら、そのまま負けの立場よ
188:１３２人目の素数さん
12/01/08 22:02:15.97
岩沢理論の大きな野望ってなんですか？
この理論だけで一つの分野だとすると、
整数論は「複数の分野の総称」ってことになりますが？
189:１３２人目の素数さん
12/01/08 22:03:30.16
以上、言い返せないバカの負け惜しみでした。
190:１３２人目の素数さん
12/01/08 22:06:57.52
>>188
数学自体が一つの分野であって、本来は切り分けられないけど、
便宜上分けた一部。
身体に対する右腕のような用語。
基礎論屋と話していると、
反論の仕方が負け犬そのもの。
基礎論はこれこれこういう理由で駄目だ、
というと、
いいや、それは違う、こういういいところがある、
という形で反論を期待しているのに、
数学なんて、所詮どの分野もそんなもんでしょ
といった厭世的な答しかかえってこない。
真の数学を知らないんだよな。
191:１３２人目の素数さん
12/01/08 22:10:26.13
このバカは、一つの目標に向かってすべてが進んでいる、
ファシズム的な分野が理想だと思っているらしいな。
ま、若気の至りってやつだろうな。多様性の重要さがわかっちゃいない。
192:１３２人目の素数さん
12/01/08 22:12:27.71
＞真の数学を知らないんだよな。
とか言って逃げないで、その一つの分野である数学の「大きな野望」を解説してくれよ。
いつもごまかして逃げて行くだけじゃないか？
193:１３２人目の素数さん
12/01/08 22:13:47.35
個々の研究者レベルでは、いくつかの方向を向いていて良い。
しかし学問たるもの発展の過程で必ず中心と傍流ができる。これは避けられ無い。
その中心が無数にあったら、それは学問とは呼べない。
194:１３２人目の素数さん
12/01/08 22:15:37.99
基礎論は一つのパラダイムを形成していないんだな。
195:１３２人目の素数さん
12/01/08 22:18:11.70
>>193
ハッタリ乙
196:１３２人目の素数さん
12/01/08 22:21:05.02
>>190
>数学なんて、所詮どの分野もそんなもんでしょ
基礎論屋って皆そんなふうに考えてるの？
だとしたらかなり可哀想な人達
197:１３２人目の素数さん
12/01/08 22:22:43.32
シミュレーションスレのシミュレーションを基礎論に置き換えるとよく分かる
198:１３２人目の素数さん
12/01/08 22:22:45.70
>>196
自演乙
199:１３２人目の素数さん
12/01/08 22:24:38.43
「その中心が無数にあったら、それは学問とは呼べない」とか
「基礎論は一つのパラダイムを形成していないといけない」とか
自分の主観的な仮定に基づく批判をしているようだが、
その仮定は殆どの人間にとって「はあ？」なんだな。
だから別に反論する気も反論する必要も感じない。
200:１３２人目の素数さん
12/01/08 22:29:51.95
基礎論は数理科学で数学じゃない、とか言い張ってたのはどうしたのかなー？
前スレで皮肉られて、言い返せなくなってやめちゃったのー？
201:１３２人目の素数さん
12/01/08 22:31:04.72
>>199
では、>>170
の前半について反論してくれ。
そして基礎論の中心テーマは何？一番大きいものひとつ。
202:１３２人目の素数さん
12/01/08 22:33:00.02
おま、アホか？何が「では」なんだか、サッパリ分からんな。
203:１３２人目の素数さん
12/01/08 22:35:50.18
>>199
ごめん、読み間違えた。読み返してみたら、
やはり、そういったこと全て基礎論では認めちゃっているんだよね。
数学では違うんだよ。
そこにハァ？といってしまうあたりが数学者じゃない。
数学はひとつ。
この理念があるかないかが数学者かそうで無いかを分ける。
204:１３２人目の素数さん
12/01/08 22:37:09.68
数学は一つの有機体なのだが、
そこに基礎論は入っていないということを
認めてしまっているので、
基礎論は数学では無い。
もう合意事項な。
205:１３２人目の素数さん
12/01/08 22:37:17.69
＞真の数学を知らないんだよな。
言ってる本人も知らないだろ、勉強不足で。
いつも抽象的な数学理念ばかり。
206:１３２人目の素数さん
12/01/08 22:39:30.02
たった一度でもいいから具体的な理念を語れば疑念が晴れるのにねえ…
207:１３２人目の素数さん
12/01/08 22:40:42.53
「中心が複数ある一つの有機体」とか「複数のパラダイムが共存する一つの有機体」とか
そういう想像が出来ない時点で視野の狭さを感じるな。
>>191の言うとおり、若気の至りなんだろうから、生暖かく見てるのが一番かね。
208:１３２人目の素数さん
12/01/08 22:42:23.88
いや、こういった合意事項が出来るのは残念なことだが、
それなら俺はもうここでは何も言わない。
言わない理由はシミュレーションスレに書いてあることと基本は同じ。
じゃ、俺は数学して寝る。さいなら。
209:１３２人目の素数さん
12/01/08 22:43:36.05
>>208
具体的に語ってくれれば、すぐにもその合意事項というのを撤回しますよ
210:１３２人目の素数さん
12/01/08 22:45:47.93
逃げちゃったねー。もう来るなよー。
211:１３２人目の素数さん
12/01/08 22:47:04.05
ぐーぐるで「具体的な理念」を探して寝るそうだ。おやすみ。
見つかったらこのスレにコピペしてね。
212:１３２人目の素数さん
12/01/08 22:49:15.89
「基礎論の中でも論文が書きやすい分野と書きにくい分野がある」ということを認めると
「数学はひとつ」という理念を持っていないということになるのなら、
「数学の中で論文が書きやすい分野と書きにくい分野がある」というのもその理念を否定している。
数学の研究現場を知らないアマチュア数学者の臭いがぷんぷんだなｗ
213:１３２人目の素数さん
12/01/08 23:05:02.97
例えば、といいながら出てくるのは岩沢理論だけ。文字通り馬鹿の一つ覚えだな。
工房か？学部生ならもう一つや二つレパートリーがあっても良さそうだし。
214:１３２人目の素数さん
12/01/08 23:10:21.53
>>181
>よく分かりました。閉論理式でないといけないと思い込んでいましたが、
>意味論と関連付けて考えない限りは
>閉論理式に縛られる必要はありませんでしたね。
全称化の規則、気を付けて。
|- の左側に現れる変数を全称化することを禁止しないと、健全でなくなるよ。
215:１３２人目の素数さん
12/01/08 23:25:07.20
>>177
|- は本当は |-_X などの添え字が付く。
このXは推論規則と公理型の集まり。
A |-_X B と書いたとき、
AからXの推論規則と公理型を使ってBを証明できる、を意味する。
このとき、Aは論理式の集合、Bは論理式。
だから別にAの中身が公理でなければならないのではない。
通常の古典論理では、XにHKやLKが入る。
そしてペアノ算術などではXにPAが入る。
だから右側がPAの公理なら、 |-_PA ∀x￢(sx=0) と書いてよい。
しかし |-_PA ￢(0x=0) などは無条件に書けない。
（エルブランの定理が関与する。言語内に定数がない場合がある。）
だから PA |-_PA φ とする必要がある。
ここで左側のPAはPAが定義されている言語上のすべての論理式になる。
もちろんモデルを持たせるには閉論理式である必要がある。
数学書では大抵 PA |- ∀x￢(sx=0) と書かれる。
これは |-_PA を略しているのだが、次のような事例の識別ができなくなる。
PA |-_HK φ ⇔ PA |=_HK φ は成り立つ。
PA |-_PA φ ⇔ PA |=_PA φ は成り立たない。
これは計算機や非古典論理や証明論では致命傷になり得る。
216:１３２人目の素数さん
12/01/08 23:40:17.04
批判されてるうちが華だと思うな。
無視されて消えていくより。
最近見た学部生向け現代数学案内では、いろんな分野を
紹介しているのに、基礎論だけごっそり無かった。
217:１３２人目の素数さん
12/01/08 23:44:27.73
おお、学部生向け案内とかマジでリア工だったのか
218:１３２人目の素数さん
12/01/08 23:48:47.28
>基礎論だけごっそり無かった。
基礎論以外の数学のすべての分野が全部あっただと？そんなわけあるまい。
世の中には無数に分野があるんだ。
そのうち「学部生向け現代数学案内」の類で必ず紹介される分野、
大学によって紹介されたりされなかったりする分野、
まず紹介されない分野とあるわけだが、
日本では基礎論は二つ目に分類される、っていうだけ。
アメリカではまともな大学なら確実に第一分類だろう。
219:１３２人目の素数さん
12/01/09 00:04:37.33
>>218
つまり、日本では無視できるほど格下だと思っていた基礎論が、
アメリカに行って世界を見てみると結構認められていて、
焦った連中がここで憂さ晴らしをしているわけね。
220:１３２人目の素数さん
12/01/09 00:24:04.74
>>218-219
呑気だなー。
221:１３２人目の素数さん
12/01/09 00:31:25.36
>>218
無数にある分野の一個にすぎないの？基礎論って。
222:１３２人目の素数さん
12/01/09 00:34:17.67
もしかして基礎論を擁護する振りして
実はおとしめるという高等技術か？
223:137
12/01/09 01:00:30.34
>>214
はい。
ともかくモデルによる充足関係T|=AとT|-Aの関係を見るときは
Tとして閉論理式の集合のみを考えるようにすれば問題ない、
しかし演繹定理などの構文論の定理は閉論理式という制約のない形で述べておいた方が
使い勝手が良いという理解でよろしいでしょうか？
>>215
Xに当たるものはいわゆる論理公理・推論規則で|-の左側にくるものは非論理公理と呼ばれるものであっていますか？
224:１３２人目の素数さん
12/01/09 03:09:20.13
数学のすべての分野は無数にある分野の一つなわけだが。
それが貶めているという風にしか読めないなら小学校から国語をやり直してきな。
>>218、無数にある分野の一個「にすぎない」なんて一言も言っていないわけで、
苦し紛れに相手の発言を捏造するのは見苦しいよ。
225:１３２人目の素数さん
12/01/09 06:18:21.24
>>216
君も相手されている内が華だよ。
馬鹿の一つ覚えやっていると誰も相手しなくなるぜ。
226:215
12/01/09 07:44:56.92
>>223
＞Xに当たるものはいわゆる論理公理・推論規則で|-の左側にくるものは非論理公理と呼ばれるものであっていますか？
Xには論理も非論理も両方入ると考えてください。
HKやLKは一般的な一階論理の公理や推論のまとまり。
これにいくつか公理を付け加えたものがPAとなります。
はじめに、言語という使用可能な記号を設定するのですが、
その言語を適当に並べて、「論理式」の条件を満たすような記号列が、
（集合という形で）左側に入ります。
もちろんXに入る公理や推論、右側の論理式でも、言語で設定した記号以外は使用できません。
227:215
12/01/09 07:57:03.84
もう少し直感的に考えると、
ある言語を設定して、その言語を使って作られる論理式がある。
PA |-_PA φ の左側が定義域、右側が値、|-_PA が写像の定義と考えると、
定義域も値もその言語の論理式全体を動くといったイメージ。
228:215
12/01/09 07:59:35.85
訂正：
この説明はよくない。
同じ定義域から複数の値が出現するだろうから。
229:１３２人目の素数さん
12/01/09 12:17:11.15
>>225
え？初めてだよここ書くの。
230:１３２人目の素数さん
12/01/09 15:50:12.96
このスレの
138 ：１３２人目の素数さん：2012/01/06(金) 22:28:15.65
>>128
accessible ordinal (cardinal) の解説希望。
と質問したのだが、未だに回答が無い。
231:１３２人目の素数さん
12/01/09 15:57:22.42
あきらめてググったら？
232:１３２人目の素数さん
12/01/09 17:56:53.11
>>231
もうググったよ。それでも分からん。
ただし、 >>230 を投稿したのは私では無い。
233:１３２人目の素数さん
12/01/09 19:52:48.35
日本人は韓国に来るな
234:１３２人目の素数さん
12/01/09 19:55:21.11
韓国人は日本にくるな
235:１３２人目の素数さん
12/01/09 20:34:25.35
ゆとり民族、ゴミジャップ
236:１３２人目の素数さん
12/01/09 20:57:36.69
関数f(x)がx=aで微分可能なとき、{Af}'(a)=Af'=(a)を証明せよ
できる人いる？
237:１３２人目の素数さん
12/01/10 01:11:47.07
>>230
accessible ordinal (cardinal) = not inaccessible ordinal (cardinal)
なんじゃね？二重否定の除去！
238:１３２人目の素数さん
12/01/10 05:38:37.97
>>232
ぐぐればふつうに出てくるぞ：
URLﾘﾝｸ(en.wikipedia.org)
239:１３２人目の素数さん
12/01/10 10:06:39.78
>>238
いかにも巨大基数と関係が出て来そうな定義だな。
240:１３２人目の素数さん
12/01/10 15:34:56.39
巨大基数と膨大基数の違いをおしえれ
241:１３２人目の素数さん
12/01/10 16:14:01.75
>>235
キムチ野郎
242:１３２人目の素数さん
12/01/11 01:15:54.22
コピペ
75 ：１３２人目の素数さん：2012/01/10(火) 16:38:44.94
ｽﾚﾘﾝｸ(math板:89-94番)
ということなんで選択公理廃止！
以後、決定性公理を採用します。
243:１３２人目の素数さん
12/01/11 02:12:16.17
決定性公理：すべての数学体系は決定可能である。
244:１３２人目の素数さん
12/01/11 02:39:26.08
確かに今の日本はゆとり国家
245:１３２人目の素数さん
12/01/11 04:00:59.17
これが古代史に伝わる数百年に一度、
彼の地に誕生するというスーパーゆとり民族か。
246:１３２人目の素数さん
12/01/11 06:54:52.94
>>54
直観主義数学ではすべての実数値関数が連続ということですが、
ということは実数の集合はすべて可測ということですか？
247:１３２人目の素数さん
12/01/11 16:35:14.91
>>240
字義的には huge cardinal が巨大基数と訳されるべきだろうな。
ま、定着しちまったものは仕方がない。
定訳をおかしいおかしい言っているとマツシンになっちまうしな。
248:１３２人目の素数さん
12/01/11 16:42:57.80
>>247
> 定訳をおかしいおかしい言っているとマツシンになっちまうしな。
で、常識的な公理をおかしいおかしい言ってるとエムシラになるってかｗｗｗ
249:１３２人目の素数さん
12/01/12 01:45:57.67
このスレを見ると、住人に人気があるのは
・様相論理
・証明可能性述語
・巨大基数
みたいだな。選択公理関係もはやってる？
250:１３２人目の素数さん
12/01/12 06:37:25.16
>>246
可測というにはルベーグ測度が定義できないと話にならない。
何かそれっぽいものは直観主義でも定義できるらしいが、
どこまでできればそれをルベーグ測度と呼んでいいのか、という問題になる。
251:１３２人目の素数さん
12/01/12 07:14:54.37
>>238
232はググりもしなかったことが明らかになったな
252:１３２人目の素数さん
12/01/12 07:56:39.56
12 ：１３２人目の素数さん ：2012/01/12(木) 01:18:39.79
数学基礎論・数理論理学 その11
(p)ｽﾚﾘﾝｸ(math板)
の奴らは
(p)URLﾘﾝｸ(www.imub.ub.es)
のような研究集会があった事すら知らん奴が多いようだな
可哀想な数学を知らない人達・・・
253:１３２人目の素数さん
12/01/12 08:01:08.02
すいません、
私は現在統合失調症で職を持たない身なのですが、
明日の論理学の世界に貢献したいと考えております。
そこで以下のように公理系のデータベースの構築をはじめようと考えております。
URLﾘﾝｸ(www4.atwiki.jp)
すべての公理系をクリックすればアウトプットできるような
巨大なデータベースの構築を目指します。
もちろんリンクなどでの立体的なデータ構造を考えております。
データの保管はOracleサーバを考えております。
よろしこお願いします。
254:１３２人目の素数さん
12/01/12 08:06:19.15
また、個々の体系が何を意味しているのかは分かりません。
一アマチュアプログラマーとして皆様に貢献したいです。
上のリストは以前紹介された様相論理のデータベースをもとにしています。
私はマジ基地ですが、よろしこお願いします。
255:１３２人目の素数さん
12/01/12 17:14:23.11
>>252
そいつ（巨大基数スレ12）は232か？
だとすると自分の怠慢を棚にあげてよくもまーｗｗ
256:１３２人目の素数さん
12/01/12 20:06:42.71
>>250
すべての関数が連続ならば、積分を考えるには開集合に測度を持たせられれば十分だろ。
ルベーグ測度なんてのはルベーグ積分の為にあるものなんだから。
直観主義でも開集合には測度を定義できるんですよね？
257:１３２人目の素数さん
12/01/12 21:13:52.74
こんなんあるよ
us.metamath.org/index.html
これの部分構造論理とか線型論理とか様相論理とかのver.があれば
勉強・研究する人には便利だろうな
258:１３２人目の素数さん
12/01/12 21:30:54.87
いちおうE. BishopのConstructive Analysisとか
Foundations of Constructive Analysisとかには
Lebesgue measureが定義してあるみたいだよ
ただ「直観主義数学ではすべての実数値関数が連続」
とかいうときの「実数値関数」とか「連続」という言葉の意味は
普通の数学でいうときのそれとは違うと考えるべきだと思うけどね
A が B より強いというのは A → B が成立して A と B が両立する場合に言うのが
普通なのでそういう意味では片方が他方より強いという関係にはないけど、
数学的公理の部分で、形式的には古典的数学と互いに背反するような
公理ないし定義を採用していることにはなると思う
259:１３２人目の素数さん
12/01/13 00:01:25.37
>>257
なんでそんなめんどくさい貼り方するの？
URLﾘﾝｸ(us.metamath.org)
260:１３２人目の素数さん
12/01/13 01:49:59.23
>>258
>ただ「直観主義数学ではすべての実数値関数が連続」
>とかいうときの「実数値関数」とか「連続」という言葉の意味は
>普通の数学でいうときのそれとは違うと考えるべきだと思うけどね
もっともだとは思うが、
それを言い出すと A → B の意味も直観主義と古典論理では違うし、
何から何まですべて違うことになる。
確かに公理系Tに公理を一つ加えただけで
Tに元々含まれる公理の意味は変わるともいえる、背景が違うのだから。
しかし、ある程度の差異は捨象して同一視してしまって比較するってのが
学問というものじゃないかい？
261:１３２人目の素数さん
12/01/13 02:25:16.86
部分構造論理では最近は何が流行っているのでしょう？
詳しい方、解説をお願いします。
262:１３２人目の素数さん
12/01/13 02:40:34.56
421 ：「名無しわざとか？」とかイヤミを言われた：2012/01/12(木) 08:03:41.44 ID:3+R7T9ps
誰も解答を書かないので>>360の解答を。
連立方程式
{ x-4=y+4
{ x+4=2(y-4)
これを解いてy=20,x=28
Aさんが28個。Bさんが20個。
つーことで、アイジャグの320番台と328番台が高設定だ！
朝から全ツッパしろ！！！
爆死覚悟でやってみてーけど、ヲレ明日は忍者屋敷イカネーといけないので凹
P.S つるかめ算とかやってたような頭の柔らかい小学生とかはもっと簡単に解けちゃうのか？
ｽﾚﾘﾝｸ(slotj板:310-312番)
263:１３２人目の素数さん
12/01/13 06:16:18.84
線型論理も部分構造論理の一つと考えれば、部分構造論理の中で線型論理は断然はやってるね。
264:GMG ◆.5wljPk1.c
12/01/13 08:29:02.49
180=nα+B=B+(n-1)α＋α
265:１３２人目の素数さん
12/01/13 18:24:27.23
Lukasiewicz 論理をよく聞くかな。部分構造論理の中では直観主義論理に次いで綺麗な構造らしい。
URLﾘﾝｸ(en.wikipedia.org)
266:１３２人目の素数さん
12/01/13 18:29:14.69
古典命題論理をストローク一本、公理一本で展開することに何かメリットある？
267:１３２人目の素数さん
12/01/13 18:40:40.82
そら時と場合によるだろう。かなり特殊だけど役に立つ場面はあるだろうね。
268:１３２人目の素数さん
12/01/13 20:34:54.20
次の性質を持つ集合 x は一般に何と呼ばれているのですか?
∀y∀z [ [x ∋ y ∋ z ] ⇒ [ x ∋ z ] ]
269:あのこうちやんは始皇帝だった
12/01/13 20:38:02.94
>>268
ニートの、ゴミ・クズ・カスの、クソガキ！！！！！！！！！
270:スレタイ446
12/01/13 21:24:28.35
遺伝的集合とか推移的集合じゃないの？
271:１３２人目の素数さん
12/01/13 22:15:53.14
メンバーのメンバーはメンバーなり。
272:１３２人目の素数さん
12/01/13 22:16:38.49
昔懐かし稲垣メンバー。
273:１３２人目の素数さん
12/01/13 22:28:49.43
>>270
ググってもそれらしき物は出て来なかったが。
274:１３２人目の素数さん
12/01/13 23:31:01.63
>>273
英語てググりなさい
275:１３２人目の素数さん
12/01/13 23:59:55.45
hereditary set, transitive set でググったら、
URLﾘﾝｸ(en.wikipedia.org)
が有った。
しかしその意味合い (定義では無くて背景などの関連事項) が良く分からない。
276:１３２人目の素数さん
12/01/14 04:18:22.31
>>127
巨大基数の表なんざ、ぐぐればすぐに出てくるぞ：
URLﾘﾝｸ(en.wikipedia.org)
277:１３２人目の素数さん
12/01/14 04:40:42.26
>>276
29 種類どころか僅かしか無かった。
278:１３２人目の素数さん
12/01/14 05:12:44.76
どう見ても29種類以上、書いてあるけどな
279:１３２人目の素数さん
12/01/14 06:05:32.06
>>275
関係Rが推移的とは
∀y∀z [ [x R y R z ] ⇒ [ x R z ] ]
280:１３２人目の素数さん
12/01/14 06:57:56.92
お、スレタイスレ446氏が降臨している！リクエストをコピペしとく。
173 ：１３２人目の素数さん：2012/01/08(日) 19:43:41.45
スレタイスレ446氏にはこっちのスレで
「レシュニフスキーやネルソン・グッドマンなどの形式的オントロジーによるアプローチ」
の数学的側面を語ってもらいたいな。
281:１３２人目の素数さん
12/01/14 07:20:03.82
>>279
＞関係Rが推移的とは ∀y∀z [ [x R y R z ] ⇒ [ x R z ] ]
∀x∀y∀z [ [ [x R y ] & [ y R z ] ] ⇒ [ x R z ] ]
ぢゃないのか？
282:１３２人目の素数さん
12/01/14 07:26:00.16
∀xがあるかないかの違いしか見つけられんが
283:１３２人目の素数さん
12/01/14 07:55:28.45
1. inaccessible
2. alpha-inaccessible
3. hyper-inaccessible
4. Mahlo
5. alpha-Mahlo
6. hyper-Mahlo
7. reflecting
8. weakly compact
9. Pi^n_m-indescribable
10. totally indescribable
11. lambda-unfoldable
12. unfoldable
13. v-indescribable
14. lambda-shrewd
15. shrewd
16. ethereal
17. subtle
18. almost ineffable
19. ineffable
20. n-ineffable
21. totally ineffable
22. remarkable
23. omega-Erdos
24. 0-sharp
25. omega_1-Erdos
26. almost Ramsey
27. Jonsson
28. Rowbottom
29. Ramsey
30. ineffably Ramsey
31. measurable
284:１３２人目の素数さん
12/01/14 08:01:54.67
32. 0-dagger
33. lambda-strong
34. strong
35. tall
36. Woodin
37. weakly hyper-Woodin
38. Shelah
39. hyper-Woodin
40. superstrong
41. subcompact
42. strongly compact
43. supercompact
44. eta-extendible
45. extendible
46. Vopenka
47. almost huge
48. super almost huge
49. huge
50. superhuge
51. n-superstrong
52. n-almost huge
53. n-super almost huge
54. n-huge
55. n-superhuge
56. I3
57. I2
58. I1
59. I0
60. Reinhardt
285:１３２人目の素数さん
12/01/14 08:09:56.67
>>283-284
乙。大体のは聞いたことあったけど、数えてみると60もあるんだ。
他に俺の知ってるのは hypermeasurable とかかな。
286:１３２人目の素数さん
12/01/14 08:25:15.60
weakly inaccessible とか strongly inaccessible とかは？
287:１３２人目の素数さん
12/01/14 08:34:30.11
どうしてこうもググりもしない教えてクンが多いのか
288:１３２人目の素数さん
12/01/14 10:33:29.38
>>284
dagger が無いんだが・・・と書こうとしたら次に出て来た。
289:１３２人目の素数さん
12/01/14 16:42:22.90
>>252
巨大基数厨の諸君に告ぐ。
巨大基数の集合論とその応用 そのアレフ 0
ｽﾚﾘﾝｸ(math板)
290:１３２人目の素数さん
12/01/14 20:12:09.02
>>275
公理的集合論では与えられた集合が推移的じゃないと
困る場面が山のようにある
順序数は普通、∈で整列順序付けされる推移的集合として定義される
与えられた集合と同型な推移的集合を作るテクニックとかもある
291:１３２人目の素数さん
12/01/14 20:13:31.75
巨大基数スレも乱立かよ。
マツシンといい、やっぱり基礎論はトンデモ多発分野なだけある。
292:１３２人目の素数さん
12/01/14 21:47:13.19
>>291
マツシンて誰？
293:１３２人目の素数さん
12/01/14 21:51:36.40
>>292
>>141あたりを参照
294:１３２人目の素数さん
12/01/14 23:08:59.21
>>101
巨大基数公理も、幾らでも新たな公理を作ろうと思えば作れる。
研究と称して、そういった公理のお決まりの性質（○○基数から導けて△△基数を導く等々）を
これまたお決まりの方法で証明する、というオリジナリティのかけらもない論文が多すぎる。
よってそれらをすべて網羅する必要があるとは思われない。
295:１３２人目の素数さん
12/01/14 23:09:39.74
>>293
2003年ってもう9年前じゃん。バカじゃね？
296:１３２人目の素数さん
12/01/14 23:13:08.90
8年ぶりにマツシンが活動期に入ったんだろ
297:１３２人目の素数さん
12/01/14 23:21:45.54
>>290
テクニックって一階？二階？三階？
298:１３２人目の素数さん
12/01/14 23:44:02.56
>>294
ネタにマジレスですまんが、
そういう研究で論文が通ったのは精々80年代まで。
いまどきそれだけじゃ、査読を通らん。
非古典論理に比べてかなり健全だろ？
299:スレタイ446
12/01/15 00:05:24.66
>>280
レシュネフスキーの数学理論は現在の記述論理にかなり近い。
プロトセティックは型理論のようなもので、
オントロジーは真偽ではなく存在の有無を実現するためのε記号を扱う論理学。
aεb（aはbである。）。
この上にメレオロジーを定義してクラスClを実現する。
（「クラス－真のクラス」は集合とならない、実際にはGBの断片＋α）
グッドマンの方はこのメレオロジーの変種の個体計算などを形式化してる。
300:１３２人目の素数さん
12/01/15 01:13:40.04
いくつかシツモソ
＞この上にメレオロジーを定義してクラスClを実現する
クラスCIってなんですか？
＞実際にはGBの断片＋α
どういう断片ですか？αは具体的には？
301:１３２人目の素数さん
12/01/15 02:22:08.13
>>296
マツシンは8年間活動自粛してたわけではないぞ。
その間も他人のブログのコメント欄なんかを中心に精力的に活動してた。
302:１３２人目の素数さん
12/01/15 03:13:55.87
>>298
巨大基数の健全性ｗ
303:１３２人目の素数さん
12/01/15 04:02:33.74
マツシンタンとかエムシラとかsikiとか人生とか長生きしてるよな。今井は生きてる？鑑定団に出たあたりまでは確認したけど。
304:１３２人目の素数さん
12/01/15 05:52:42.90
このスレが巨大基数について一番専門的な話をしているようなので、質問です。
large large cardinal (大巨大基数?)とか
small large cardinal (小巨大基数?)とか
middle large cardinal (中巨大基数?)とか
ってそれぞれどの基数ですか？
305:１３２人目の素数さん
12/01/15 06:22:31.35
large small cardinal とか small small cardinal とかってなんですかｗｗ
306:１３２人目の素数さん
12/01/15 07:37:38.92
>>294
前半部分は全くその通りだが
「...というオリジナリティのかけらもない論文が多すぎる」というのは
現状をまるっきり分かっていない奴の言うこと。
そんな論文見かけたことすらないね。
307:１３２人目の素数さん
12/01/15 08:15:59.80
ネタにマジレスかこわるい
308:１３２人目の素数さん
12/01/15 08:48:03.56
>>304
URLﾘﾝｸ(ncatlab.org)
ここ見ると31の measurable cardinal が境界だそうだ。
だから 1-30 が small large cardinal で
32-60 が large large cardinal なんじゃないの？
middle large cardinal って聞いたことないけど、measurable のこと？
309:１３２人目の素数さん
12/01/15 13:57:59.29
>>296 >>301 >>303
何年間も同じ奴を追っかけて・・・ヒマだなおまえら。
310:１３２人目の素数さん
12/01/15 14:04:05.75
logic systemのリスト化...ソフトウェアにするか動的ウェブで実現するか...
311:１３２人目の素数さん
12/01/15 16:17:21.91
追っかけなくても勝手に現れに来るからｗ
312:１３２人目の素数さん
12/01/15 20:05:32.35
>>308
Stanford Encyclopedia of Philophy の Koellner の記事
(URLﾘﾝｸ(plato.stanford.edu))から引用：
A large cardinal is small if the associated large cardinal axiom can hold in Gödel's constructible universe L,
that is, if “V ⊨ κ is a φ-cardinal” is consistent, then “L ⊨ κ is a φ-cardinal” is consistent.
Otherwise the large cardinal is large.
この定義によると24のゼロシャープはもう large large cardinal のはずだが。
313:スレタイ446
12/01/15 20:29:39.02
>>300
クラスClは
(a,b)(a＝b≡C(a)＝C(b))
cl(a)≡(Ex)(a＝C(x))
で、定義される。このEは1階論理の量化記号みたいなもの。
Clは何らかの個体の集まりなんだけど、
その集まりの集まりは元の集まりと変わらない。というのが彼のクラスの特徴。
こうすると最上位概念の存在によって循環がなくなる。
1項述語Cl,Ob,二項述語∈,＝が存在して、
・等号＝に関する公理
・外延性公理 (a,b)(cl(a)(cl(b))→(x)(x∈a≡x∈b)→a＝b)
・(a,b)(a∈b→ob(a)(cl(b))
・内包性公理 (Ea)(cl(a)((x)(x∈a N≡ob(Y).ψ(x))))
GodelとBernaysの公理的集合論の断片になる。
あとはクラスclとobに関する操作が多少加わる。
とはいえ、集合論いらない数学は
Feferman・Aczelの構成的数学などもある。
それらをオントロジーの枠組みで実現しているものだろう。
314:１３２人目の素数さん
12/01/15 20:58:47.50
>>312
0^\sharp は cardinal ではないからその定義は意味をなさない罠ｗｗ
315:１３２人目の素数さん
12/01/16 01:16:26.67
>>304
俺は>>308の流儀と>>312の流儀、どちらも聞いたことがあるけど、
きんちんとした定義はないんじゃないかな？
だから23までが small large cardinal
32以降が large large cardinal でいいんじゃない？
ついでにその間の24-31が middle large cardinal とか新説を唱えてみる。
316:１３２人目の素数さん
12/01/16 06:53:15.92
>>313
その理論の強さはどれくらい？ZFC より弱いの強いの？
317:１３２人目の素数さん
12/01/16 08:14:12.21
>とはいえ、集合論いらない数学は
>Feferman・Aczelの構成的数学などもある。
>それらをオントロジーの枠組みで実現しているものだろう。
「それら」は何を指していますか？「実現している」の主語はなんですか？
スレタイスレ446氏のレスは相変わらず読みにくいんですが。
318:１３２人目の素数さん
12/01/16 08:38:47.03
コアモデルがあるような巨大基数は小さいとか言ってみるテスト
319:１３２人目の素数さん
12/01/16 09:34:52.00
?してみるテストって久しぶりに見たw
320:１３２人目の素数さん
12/01/17 02:32:53.13
>>314
κ is a 0-sharp cardinal if there is a non-trivial elementary embedding j: L → L whose critical point is κ
と定義すれば>>312の定義が適用できる！
321:１３２人目の素数さん
12/01/17 06:40:24.56
つまり、0-sharp cardinal は cardinal でないこともあるってことだね。
322:１３２人目の素数さん
12/01/17 17:16:10.88
312の定義に意味を持たせるには
if“V ⊨ κ is a φ-cardinal”then“κ is in L”
であればいいので、“κ is cardinal”である必要はないのね。
323:１３２人目の素数さん
12/01/18 01:46:48.73
>>321, >>322
普通に>>320は、最初に「For a cardinalκ, 」を補えばいいだろうが！
324:１３２人目の素数さん
12/01/18 04:32:03.92
基礎論最大の未解決問題ってなんなのでしょうか？
325:１３２人目の素数さん
12/01/18 05:51:34.40
>>323
では 0-sharp cardinal の存在と（通常の意味の）0-sharp の存在は同値？
326:１３２人目の素数さん
12/01/18 08:50:07.59
>>324
間違いなく「P対NP問題」でしょう。
基礎論の各分野での最大の未解決問題となると、分かりませんが。
327:１３２人目の素数さん
12/01/18 17:46:55.71
>>325
Silver indiscernible は順序さえ保てば自由に動かせて
非可算基数はすべて Silver indiscernible なのだから、
critical point を特定の非可算基数になるような
L から L への elementary embedding なんて
(0^\sharp の存在から)簡単に作れる。
328:１３２人目の素数さん
12/01/18 18:30:36.14
自動定理証明系で
証明仮定（証明図）がすべて出力できるソフトウェアはありますか？
329:１３２人目の素数さん
12/01/18 19:17:07.58
>>328
自分で作れば良い。全ての図を少しずつ列挙し、
同時に一方ではそれらが証明図になって居るかどうか少しずつ判定すれば良い。
330:１３２人目の素数さん
12/01/18 19:39:04.24
>>329
それって普通の対話型証明ソフトと変わらないですよね？
私は公理からの論理式のシーケント列を見たいのです。
331:１３２人目の素数さん
12/01/18 23:53:47.48
３２８の件 スルー お願いします
332:１３２人目の素数さん
12/01/19 01:45:57.11
>>327の言う通りなので、
κ is a real-sharp cardinal if for any a⊂ω, there is a non-trivial elementary embedding j: L[a] → L[a] whose critical point is κ
と定義すれば、“∀a⊂ω(a-sharp exists)”も real-sharp cardinal の存在と同値になって>>312の定義が適用できる！
dagger についても同様。