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

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


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

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

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

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

前スレ
数学基礎論・数理論理学　その10
uni.2ch.net/test/read.cgi/math/1319895756/
2 名前：１３２人目の素数さん mailto:sage [2012/01/02(月) 23:31:59.88 ]: ここは「哲学排除！」のアスペは来ない（はず）ので、
スレタイスレ446氏をはじめとした哲学的論理学の話題も歓迎！
平和に行きましょう。
3 名前：１３２人目の素数さん [2012/01/02(月) 23:33:33.23 ]: おつ
4 名前：前スレ969 [2012/01/02(月) 23:52:17.59 ]: 申し訳ありません。前スレが埋まってしまいそうなので、前スレ980からのコメントを
ここでもう一度貼らせて頂きます。
5 名前：前スレ969 [2012/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 [2012/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 名前：１３２人目の素数さん [2012/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 [2012/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 [2012/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 [2012/01/02(月) 23:54:38.57 ]: ４、PA|- x・y=z→□[x・y=z]
３と同様なので省略。

とりあえず、ここまでで何かありましたら、御意見よろしくお願いいたします。

参考にしたのは、
Wolfgang RautenbergのA Concise Introductionto Mathematical Logic
www.scribd.com/doc/32314723/A-Concise-Introduction-to-Mathematical-Logic
の第６章、７章です。
11 名前：前スレ969 [2012/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 名前：１３２人目の素数さん [2012/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 [2012/01/02(月) 23:56:29.51 ]: 引っ越し終了

スレ汚しすみません。
14 名前：スレタイスレ446 [2012/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 名前：１３２人目の素数さん mailto:sage [2012/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 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 00:28:26.98 ]: そのうち、記述論理が一階述語論理にとって替わるのかな？
昔、様相論理を使って集合論を記述してどうの、という話があったけど、下火になったしね。
様相論理を記述論理に直して再チャレンジってことかな？
17 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 01:20:30.22 ]: Zermelo の集合論で出来ることと出来ないことがまとめてある文献ってありますか？
18 名前：１３２人目の素数さん mailto:age [2012/01/03(火) 02:19:48.96 ]: 前スレ942の
>記述論理ってかなり便利じゃないだろうか？決定可能だし...。
>量化記号が一般化されているし、
ってところは、ハッタリだったという理解でおk？
19 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 05:28:29.98 ]: 昨夜、あっという間に新スレへの移行が完了してしまっとるなあ。実に見事だ。
勝手に「自称次スレ」を立ててたアスペは、指を咥えとるしかなかったんだろな。
この新スレには、アスペみたいな奴が現れないことを祈ろう。
自分で立てた隔離スレで騒いだまま、ずっと出てくるなよ。
20 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 07:09:53.37 ]: >>17
纏まっている文献は知らないけど、
ZF では成り立つが Zermelo の集合論で成り立たないことが有名な結果は幾つかある。
一番有名なのはω＋ωがフォンノイマン順序数として存在すること。
ただ、順序型としてのω＋ωは滅茶苦茶弱い算術でも扱えるので、実際の数学には影響はない。
本当に数学的な命題での例となるとそんなにないかな。
選択公理スレにも書いてある通り、ボレルゲームの決定性はその一例。
他に、「二つの一階の構造が、初等同値であることと、あるウルトラフィルタによる超冪が同型であることは同値」
っていうシェラハによるモデル理論の金字塔的結果は、
置換公理なしでは無理だって聞いたことがあるような。
21 名前：スレタイスレ446 [2012/01/03(火) 07:38:10.89 ]: >>18
量化記号が一般化されているかは言葉の使い方次第だが、
推論のタブローは必ず停止するかクラッシュするので決定可能。
だからこそ計算クラスで表現力が調べられる。
22 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 08:17:51.03 ]: >>16
>昔、様相論理を使って集合論を記述してどうの、という話があった
詳細きぼん。それって、様相論理は決定可能だから、決定可能な集合論を作ろうってこと？
23 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 08:40:34.37 ]: どうやらアスペはマツシンだったっぽい。
議論の仕方から脱線する話題まで、マツシンそのものと言える。
自分の隔離スレで、「直観主義は直観主義論理を採用すること」等々、
素人っぷり丸出しのこと喚いているぜ。
24 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 08:43:15.18 ]: 803 ：１３２人目の素数さん：2011/12/26(月) 02:31:25.06
　　直観主義で提唱された論理が直観主義論理っていうだけで、
　　直観主義の研究＝直観主義論理の研究、ではないんだがな。
　　直観主義っていうのは、論理の部分だけではなく、非論理的公理の部分や、
　　その他数学のあるべき姿全般に対する哲学的主張（例えば形式主義に反対するなど）までひっくるめた
　　文字通り一つの「主義」なんだけどな。
　　直観主義論理はその一部分に過ぎないし、その部分だけならば形式主義とは矛盾しないわけだ。
25 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 08:56:44.28 ]: アスペとの基礎論論争は、隔離スレでやってくれ
26 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 09:11:00.68 ]: 折角マツシンは自分で隔離されているわけだし、放っておけば害はないだろ。
相手しないと、こっちの本スレに出張してくるの？
27 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 09:25:17.08 ]: >>20
>他に、「二つの一階の構造が、初等同値であることと、あるウルトラフィルタによる超冪が同型であることは同値」
>っていうシェラハによるモデル理論の金字塔的結果
その証明が書いてある文献、教えてもらえますか？
28 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 09:34:12.01 ]: >>20
すみません、もう一つ。"フォンノイマン順序数" って何ですか？
29 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 10:07:44.30 ]: ググるべし。ググるとこんなんが出てきた：

フォン・ノイマンに由来する順序数の定義を仮定しているからで、
その中で個々の順序数は先行する全ての順序数の集合になっている。このような定義はブラリ＝フォルティがパラドックスを考案した当時はまだ知られていなかった。
(ja.wikipedia.org/wiki/%E3%83%96%E3%83%A9%E3%83%AA%EF%BC%9D%E3%83%95%E3%82%A9%E3%83%AB%E3%83%86%E3%82%A3%E3%81%AE%E3%83%91%E3%83%A9%E3%83%89%E3%83%83%E3%82%AF%E3%82%B9)

つまり順序数を「先行する全ての順序数の集合」として表現した場合の順序数のこと。
置換公理の自然さの解説に「ω＋ωというあるべきものの存在が示せなくなる」なんてのを見かけるが、
それはフォン・ノイマンに由来する順序数の定義を仮定しているからで、
この表現方法にこだわらなければ理由にも何にもなってないのさ。
30 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 10:24:30.64 ]: お聞きしたいことがあります。
一階述語論理の公理系Tが帰納的に記述可能であることの厳密な定義は何でしょうか？
公理系がデタラメに構成されていないことというニュアンスは分かるのですが…
31 名前：スレタイスレ446 [2012/01/03(火) 10:30:37.67 ]: >>16
＞そのうち、記述論理が一階述語論理にとって替わるのかな？
今の計算機の原理が変わらない限り一階論理がなくなることはない。

＞昔、様相論理を使って集合論を記述してどうの、という話があったけど、下火になったしね。
様相論理は可能世界を用いて内包を使う意図があって導入された。
様相論理が扱う文は一階論理で透明性（代入法則が成り立たない）を持たない文なので、
数学や一階論理の様な神の視点の立場に合致しなかった。

＞様相論理を記述論理に直して再チャレンジってことかな？
既にはじまっている。
人工知能では概念を扱うためオントロジーが導入された。
オントロジーは最上位の概念としてメタなオントロジーを持つとされるが、
とりわけSUMOという体系はサブシステムとして集合やクラスを扱うことができる。
このオントロジーの記述の手段として次の3つが考えられたわけだ。
・パースらが研究していた存在グラフをsowaらが発展させた概念グラフ、また意味ネットワーク。
・記述論理。
・Guarinoの形式的オントロジー。
そして記述論理が最も有望とされている。
32 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 10:37:30.87 ]: >>30
読んで字の如くそのまんま。
自然数が与えられたとき、それが公理系Tの公理のゲーデル数であるか否かが
帰納的に決定可能（つまり計算機で判定可能）ということ。
33 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 10:44:29.64 ]: >>31
訂正：
様相論理は可能世界を用いて内包を使う意図があって導入された。
↓
可能世界を用いて内包を使う意図があって様相論理へ導入された。
34 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 11:45:06.48 ]: >>32
ありがとうございます。
もうひとつ質問ですが、Uは公理系Tの再帰的拡大であると言われたとき、TとUのゲーデル数の定め方は異なっていても
よいのですか？
35 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 17:50:48.78 ]: >>34
Uは公理系Tの再帰的拡大であると言われたとき、ゲーデル数での表現はまだ定めてないような。
だから32も正確ではなくて「自然数が与えられたとき、それが公理系Tの公理のゲーデル数であるか否かが帰納的に決定可能」
なようにゲーデル数化できる公理系、というべきだね。
36 名前：１３２人目の素数さん mailto:age [2012/01/03(火) 18:00:02.51 ]: >>31
>様相論理は可能世界を用いて内包を使う意図があって導入された。
クリプケが可能世界意味論を提案するずっと前から、様相論理はあるわけなんだが。
37 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 18:07:31.10 ]: >>35
なるほど。ありがとうございます。
38 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 18:50:46.99 ]: >>36
>>33
39 名前：１３２人目の素数さん mailto:age [2012/01/03(火) 19:03:29.31 ]: >可能世界を用いて内包を使う意図があって様相論理へ導入された。
何が導入されたん？
40 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 19:13:06.29 ]: >>24（＝前スレ803？）
直観主義の非論理的公理ってどういうものがあるんですか？
41 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 19:32:45.00 ]: >>39
なんだか文章がおかしくなったのでもう一度。
「クリプキが可能世界を導入して内包を含む文を解釈することに成功した。」

>>31
訂正：
＞透明性（代入法則が成り立たない）を持たない文
↓
　透明性（代入規則による外延交換が成り立つ）を持たない文
42 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 19:40:50.28 ]: >>41
透明性といっているってことは、一階術語様相論理の話をしている？
それなら通常の一階述語論理を断片として持つのだから、
数学や集合論を記述することなんて訳ないのでは？
43 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 19:56:26.21 ]: 誤字訂正：
一階術語様相論理
↓
一階述語様相論理
44 名前：１３２人目の素数さん [2012/01/03(火) 20:13:11.86 ]: 16が言っているのは、以前ちょっと流行った STS (Structural Theory of Sets) のことだと思う。

www.blutner.de/AFA/baltag.pdf

様相言語は量記号を持たない（量記号の有無は議論には影響しない）ようだから、
命題様相論理で集合論を記述していると考えていい。
45 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 20:20:55.15 ]: >>31
＞今の計算機の原理が変わらない限り一階論理がなくなることはない。
今の計算機の原理と一階論理にはどんな関係があるの？
量子計算機とかDNA計算機とかだと、一階論理ではなくなる？
46 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 20:41:38.99 ]: >>42
透明性はエレクトラのパラドクスの発生や宵の明星・明けの明星の問題の話です。
論理へクリプキ意味論を導入すると、
文は一般に内包で、意味論側で可能世界が与えられると外延と解釈できるようになります。
このような不透明な体系、例えば様相論理は数学の記述は難しいとクワインが指摘したのです。
数学は2つの対象が等しいならば、両者で同じことが成り立つという客観（神の視点）を持つからです。
一方で普段通りに、モデル理論を意味論、1階論理を構文論とすれば、
自然言語の透明性が保存され外延交換が成り立ちます。
（実はその後、クワインは透明性を持つ体系での厳密科学の形式化を断念していますが...）
勿論自明なやり方でなら一階論理を含む様相論理で数学を書くことは可能ですが。
47 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 20:59:09.91 ]: >>46
内包と外延の分析に有益というのは、様相論理の利点の一つだろうが、
それだけが様相論理を評価する場合の唯一の視点というわけではない。
Baltag のSTSでは、また別の視点が強調されている。
そこで「数学や一階論理の様な神の視点の立場に合致しなかった」と評価するのは
ちとずれているんではあるまいか？
48 名前：１３２人目の素数さん [2012/01/03(火) 21:19:02.83 ]: >>16
>そのうち、記述論理が一階述語論理にとって替わるのかな？
>様相論理を記述論理に直して再チャレンジってことかな？
えー？記述論理って述語論理のちゃちなサブセットだろ？
49 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 21:23:21.74 ]: あちゃー、隔離スレではトンデモ学者に矢田部さんが味方認定されちゃってる。可哀想に。
50 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 21:29:49.63 ]: AMC（空でない集合たちの族に対して、それらの各々の非空有限部分集合の族が取れる、という公理）から
選択公理をどうやって証明したらいいのか分かりません。
外延性公理と正則性公理が必要なのだそうですが、誰か分かる方いますか？
51 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 21:51:52.07 ]: >>49
俺も何度か経験あるけど、お前のトンデモ理論を俺が支持しているかのように書くのはやめてくれ、と思う。
ツワモノになると、自分のトンデモ理論が正しいと公式に表明してくれ、とかメール送ってくるし。
52 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 22:01:09.38 ]: >>44 >>47
STSは全く知りませんでしたね。だとすると誤読でしたね。
確かにクリプキの指示とかの話は内包論理に関する様相論理の話でしかない。
>>45
＞今の計算機の原理と一階論理にはどんな関係があるの？
一階論理程度の表現能力があれば十分だというところですね。
ホーン節はじめ分解原理・SLD導出・失敗による否定・エルブランモデル。
論理プログラムは部分帰納関数の表現まで使える...。
＞量子計算機とかDNA計算機とかだと、一階論理ではなくなる？
拡張する必要はあるでしょうね。
53 名前：１３２人目の素数さん mailto:age [2012/01/03(火) 22:35:03.01 ]: >>40
直観主義ブラウワーと形式主義ヒルベルトの論争があったように、
直観主義は本来は形式化に反対するものなので、
その論理の部分とか非論理的公理とかいうのはおかしいと言えばおかしいのだけど、
現代的視点で形式化した場合に、と断りを付けておくけど：

有名どころは、

扇定理(Fan Theorem) と
連続選択公理(実数の選択関数で連続なものが取れる)

かな。これだけでブラウワーの数学が形式化できるのか、
もっと公理が必要なのかはよく知らない。
54 名前：１３２人目の素数さん mailto:age [2012/01/03(火) 22:40:31.56 ]: 補足すると、連続選択公理からは「実数値関数はすべて連続である」という定理が出る。
この定理は勿論、古典論理（とそんなに強くない数学的公理）上では矛盾するけれど。
だから、直観主義は、排中律を拒否して論理を弱めているので、古典論理より定理が少なくなる、というのはある意味嘘。
弱めているのは論理の部分だけで、非論理的公理の部分は一方が他方より強いとか弱いとかって関係にはない。
55 名前：ただのバカ [2012/01/03(火) 22:47:42.05 ]: これからの論理は直観にいくよりも矛盾許容論理。
定理ごっそり増える
56 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 22:51:18.72 ]: >>52
>＞今の計算機の原理と一階論理にはどんな関係があるの？
>一階論理程度の表現能力があれば十分だというところですね。
十分というだけで、必要でないのなら、
一階論理の断片となる論理がとって替わる可能性があるってことでは？

>今の計算機の原理が変わらない限り一階論理がなくなることはない。
と辻褄があっていない。
57 名前：１３２人目の素数さん mailto:sage [2012/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

www.springerlink.com/content/j67206441630333u/
58 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 23:11:44.90 ]: >>56
もちろんここで言う一階論理はある程度の断片や拡張も含めた意味で。
ホーン節の分解システムも一階論理の断片だったりするし。
逆に一階論理に推移閉包や述語定数を添加する場合もある。
ペアノ算術の関数や述語をダイレクトに添加した例もよく見る。
ソフト側では、それ以上のファジーや適切論理なんかまで使うけど。
59 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 23:12:31.51 ]: >>57
>>57さんへの文句ではないが、
なんでリンク先は出版年を明記してないんだろう？
60 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 23:14:32.92 ]: >もちろんここで言う一階論理はある程度の断片や拡張も含めた意味で。
それ言ったら様相論理も含まれるやん。一階論理はある程度の断片だし。
一階論理の代替になれなかった様相論理の次の候補、という話してるのに。
61 名前：１３２人目の素数さん [2012/01/03(火) 23:19:43.61 ]: 低次元な議論は

　も　う　や　め　て　く　れ
62 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 23:22:25.47 ]: >>59
確かに不思議ですね。出版は1971年だそうです。

最初のページを見てみると、
この手の話は一般連続体仮説G.C.H.を仮定した結果が多いみたいですね。
概要でもGCHを使わずに、と強調していますし。
これなら置換公理を使っていても全然不思議ではありませんね。
63 名前：スレタイスレ446 mailto:sage [2012/01/03(火) 23:27:25.77 ]: >>60
様相論理が一階論理の断片と考えられるといえばそうだけど、
わざわざ様相論理といったときは、大抵モーダルオペレータや
関係構造やらフレームやらを使用する意図があるという前提で。
（計算機で一階論理の述語や関数の引数を制限するのは別の理由。）
64 名前：１３２人目の素数さん mailto:sage [2012/01/03(火) 23:55:11.91 ]: >>62
選択公理や正則性公理も当然使われているだろうな。
65 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 00:17:53.20 ]: 第二不完全性の証明は結局分かったんだろうか？
実際のところ、証明に必要な帰納法はΣ_1帰納法で十分だったの？
66 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 00:22:44.64 ]: >>55
ネタにマジレスかも知らんが、矛盾許容論理というと古典論理より弱い。
従って非論理的公理をいじらないのなら定理が増えるなんてことはあり得ない。
67 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 01:10:08.95 ]: こっちに現れるんだろうからコピペしとこ

999 ：１３２人目の素数さん：2012/01/03(火) 00:46:52.02
　　数理学厨は >>917, >>923 で皮肉られて言い返せなくなったと見えて、姿を消したな。
　　前回は、伝統を良しとして歴史的偶然を批判するっていう自己矛盾を指摘されて言い返せず、
　　暫く消えていたがそのうち何事もなかったように現れた。
　　今後もまたほとぼりがさめたと判断した頃に現れるのだろう、新スレに。
68 名前：１３２人目の素数さん mailto:sage [2012/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 名前：１３２人目の素数さん [2012/01/04(水) 02:14:16.13 ]: >>36
天才と言われるクリプケが可能世界意味論を提案する前の様相論理は何を研究していたのか？
70 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 02:28:24.73 ]: >>54
ビショップの直観主義数学は、古典論理上の数学より弱いって聞いたけど
71 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 04:21:21.24 ]: ああ、僧正と橋々の構成的解析ね。
72 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 05:08:22.74 ]: 橋々？僧正は Bishop のことだな。
73 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 07:34:38.51 ]: >>69
最初期はルイスやゲーデルやタルスキやマッキンゼーらが
シンタックスのみで研究していた。
ただし関係構造が必要なのは知られていて、
カルナップの意味論なんかが考案された。
既にプライアーの時相論理が開発されていて、
自然数をドメインとして＜を関係として持つモデルがあった。
50年代の終わりにようやくクリプキ構造の完全性定理が出来る。
74 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 08:33:11.69 ]: >>69
様相論理の体系で S4 とか S5 とかはあるのに、S1, S2, S3 がないのは不思議だよね？
これはクリプキ意味論以前から様相論理が研究されていた名残り。
S1, S2, S3 は通常の可能世界意味論を持たない。
少し変更を加えれば（非正則世界を許す）S2 と S3 は完全な意味論が可能世界意味論で作れる。
しかし S1 はどうやってもその手の意味論は与えられなかったはず、詳しくは知らない。
あと、S6 以降の体系も世の中にはある。
75 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 09:05:15.50 ]: >>74
S1 から始まる体系の系列は、Lewis が厳密内意（論理学スレで話題になってた）の研究で提案したもので、
様相論理の研究と言ってしまっていいのかは疑問。
もっとも A ⊰ B を □(A→B) と、逆に □A を ⊥⊰ A と理解することで、
厳密内意と様相は同じものとみなしていいんだけどね。
（少なくとも S2 以上は。S1 はどうだったか忘れた。）
ある意味、適切論理の先行研究ともいえる。
76 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 09:25:30.07 ]: 俺は>>68はいいこと言ったと思う。こういうものの見方が必要だと思うんだ。
だからこそ、哲学はこのスレから出て行けとか、哲学的論理学はスレから分けるべきだとか、
そういう「排除の論理」には賛成しかねる。数学系の論理学と哲学系のそれが、
近いことをやっていて、スレが一緒で問題がないのなら、そのまま一緒にやっていくのがいい。
「排除の論理」の人々は、分類フリークっていうか分類することが目的になってると思うんだよね。
77 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 09:37:31.81 ]: >>75
>逆に □A を ⊥⊰ A と理解することで
T ⊰ A じゃなくて？

>>76
禿堂。数学系の論理学と哲学系の論理学だけじゃなくて、計算機系の論理学もな。
78 名前：１３２人目の素数さん mailto:age [2012/01/04(水) 10:00:03.96 ]: おっと、ここで「数学じゃない」厨が現れて、
哲学なんかと仲良くしようというなら哲学板へスレごと移動しる！
とか言い出すに一票。
79 名前：１３２人目の素数さん mailto:age [2012/01/04(水) 10:01:48.99 ]: >>77
>T ⊰ A じゃなくて？
仰るとおりでございます。
80 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 11:26:40.86 ]: >>74
またS6以降はどう決まるのでしょうか？
81 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 14:07:47.35 ]: 我々エイリアンからすれば、
おまいら地球人のやってるコトは全て児戯。
82 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 14:36:24.27 ]: 今時のプログラミング言語の型理論の基礎はSystem F、
要するに二階λ計算、大体二階直観論理相当。
一階述語論理で十分なんて馬鹿げてる。

動作原理としてはノイマン型でロジックとは関係ないし。
83 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 15:05:06.21 ]: >>80

S6:
home.utah.edu/~nahaj/logic/structures/systems/s6.html

S7:
home.utah.edu/~nahaj/logic/structures/systems/s7.html

S8:
home.utah.edu/~nahaj/logic/structures/systems/s8.html

S9:
home.utah.edu/~nahaj/logic/structures/systems/s9.html
84 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 16:02:50.44 ]: >>82
つまりこれまでの論理プログラムなどのハード計算が使い物にならないので、
非古典論理や型の理論などのソフト計算が導入されている。ということでしょうか？

＞動作原理としてはノイマン型でロジックとは関係ないし。
チューリング機械であるという見方の一方でブール代数を扱うという見方もあるのではないでしょうか？
人の推論と計算機の間にロジックが必要なのではないでしょうか？

>>83
非常に便利です。
これらはどの様相論理の本にも載っていませんでした。
85 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 16:05:56.20 ]: 訂正：
型理論はソフト計算とは無関係でしょうが...。
86 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 19:03:32.23 ]: 命題論理とスイッチ回路の初等的過ぎる疑問::
ラッセル方式でNORだけの公理は割とみじかく書き下しできるのに
NANDだけだといやになるほど長くなる
一方
回路設計をNAND素子オンリーで組むのはラクチンなのに
NOR素子オンリーで組むのはなぜか苦労する（手間が時間が）

・・・トンデモ本「数理示申學序説の前書き」より自分で引用

これ数学SFに使おうと思いますが玄人の眼からみると幼すぎますか
できれば評価レスキボンヌ
87 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 19:15:18.41 ]: >>84
ハード計算、ソフト計算ってのが何を意味してるかわからん。
論理プログラムとの関係もわからん。
88 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 21:45:22.34 ]: >>87
ハード計算が計算機の立場の情報処理技術、
ソフト計算が人間の立場の情報処理技術。
論理について考えると、
命題論理・一階述語論理はハード計算。
様相論理・時相論理・多値論理・関係論理・ﾊﾟﾗｺﾝｼｽﾃﾝﾄ論理・曖昧論理・
ファジー論理はソフト計算。
だから命題論理や一階述語論理の応用である論理プログラムもハード計算になる。
89 名前：１３２人目の素数さん [2012/01/04(水) 22:20:43.07 ]: >>88
あんたはやっぱり少し見えてる。
>人と計算機の間にロジック
について差し支えない範囲で語ってくれんか？
90 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 23:35:52.71 ]: >>89
そんなに詳しく考えているのではないですが、
計算機の内部でブール代数に基くビット演算が起こっていると考えられますが、
（実際のハードウェアがどうなっているかは知りませんが、）
これを厳密かつ人が扱いやすく定義し理論的保障を与えるために、
形式的言語として命題論理のような論理演算システムが必要と考えています。
（もちろん状態遷移系でもチューリング機械でもレジスター機械でも何を駆使してもよいのですが。）
とりわけ一階論理は人の推論に比較的合っているうえにそこそこの表現力も持っているのではないでしょうか？
もちろんプログラムなどの側で有用なのは言うまでもないでしょう。
91 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 23:37:10.93 ]: ばかだろ
92 名前：１３２人目の素数さん mailto:sage [2012/01/04(水) 23:43:09.11 ]: >>31
>今の計算機の原理が変わらない限り一階論理がなくなることはない。
これは一階論理の代わりにチューリングマシンやλ演算でも良いのですよね？

>>88
ハード計算とソフト計算はあなたが考えた独自用語ですよね？
ソフト計算とはヒューリスティクスという意味でしょうか？

>だから命題論理や一階述語論理の応用である論理プログラムもハード計算になる。
チューリング等価なプログラミング言語であるprologで
あなたが示したすべての論理をソフトウェアとして実現できます。
だから一階述語論理の応用はハード計算とは言えません。
ソフト計算に分類した論理を使えばヒューリスティクスを自然に表現できる、
という主張なら納得できるのですが。
93 名前：スレタイスレ446 mailto:sage [2012/01/04(水) 23:55:11.56 ]: >>92
＞これは一階論理の代わりにチューリングマシンやλ演算でも良いのですよね？
大抵は組み合わせて使います。

＞ハード計算とソフト計算はあなたが考えた独自用語ですよね？
＞ソフト計算とはヒューリスティクスという意味でしょうか？
Soft computingとHard computingのことですね。

＞チューリング等価なプログラミング言語であるprologで
＞あなたが示したすべての論理をソフトウェアとして実現できます。
例えばそのProlog自体の基礎となっているのが論理プログラムなどという話しですね。
94 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 08:51:28.00 ]: >>83
番号が大きいほうだけではなくて、S1 より弱い S0 なんてのもあるのか。
そのサイトは便利だ、㌧クス
95 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 09:06:25.42 ]: >>74
非正則世界ってなんですか？
96 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 14:57:03.04 ]: Sπ
97 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 19:02:59.82 ]: >>95
非正規世界(non-normal world)のことだろ。
数学用語ではnormalは普通「正規」と訳される。「正則」はregularね。
非正規世界では、□Aという形の論理式は問答無用で偽とする。
それ以外のconnectiveの意味論は通常通りとする。
正規世界では通常のクリプキ意味論。
S2やS3はこんな意味論で完全になるそうだ。
98 名前：１３２人目の素数さん mailto:sage [2012/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 名前：１３２人目の素数さん mailto:sage [2012/01/05(木) 19:23:55.92 ]: 誰も「すべてを網羅している」なんて言ってないよーな
100 名前：１３２人目の素数さん [2012/01/05(木) 19:34:21.83 ]: Vopěnka cardinal ってなんでしょうか？
Vopěnka principle (VP) は前スレで話題になっていましたが。

[ 続きを読む ] / [ 携帯版 ]

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