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

1 ：12/01/02 〜 最終レス ：12/01/19

数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
19世紀末から20世紀半ばにかけて生まれ、発展した数学の一分野です。
現在では、証明論、再帰的関数論、構成的数学、モデル理論、公理的集合論など、
多くの分野に分かれ、極めて高度な純粋数学として発展を続けています。
（「数学基礎論」という言葉の使い方には、専門家でも若干の個人差があるようです。）
応用、ないし交流のある分野は、計算機科学の諸分野や、代数幾何学、
英米系哲学の一部などを含み、多岐にわたります。
（数学セミナー98年6月号、「数学基礎論の学び方」
ttp://www.math.tohoku.ac.jp/~tanaka/intro.html
或いは 岩波文庫「不完全性定理」 6.4 数学基礎論の数学化 などを参照）
従ってこのスレでは、基礎的な数学の質問はスレ違いとなります。
他のスレで御質問なさるようにお願いします。
前スレ
数学基礎論・数理論理学　その10
http://uni.2ch.net/test/read.cgi/math/1319895756/

2 ：

ここは「哲学排除！」のアスペは来ない（はず）ので、
スレタイスレ446氏をはじめとした哲学的論理学の話題も歓迎！
平和に行きましょう。

3 ：

おつ

4 ：

申し訳ありません。前スレが埋まってしまいそうなので、前スレ980からのコメントを
ここでもう一度貼らせて頂きます。

5 ：

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 ：

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 ：

２、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 ：

３、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 ：

（�A）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]
したがって、（�@）（�A）と帰納法の公理より
PA|- x+y=z→□[x+y=z]
証明終わり

10 ：

４、PA|- x・y=z→□[x・y=z]
３と同様なので省略。
とりあえず、ここまでで何かありましたら、御意見よろしくお願いいたします。
参考にしたのは、
Wolfgang RautenbergのA Concise Introductionto Mathematical Logic
http://www.scribd.com/doc/32314723/A-Concise-Introduction-to-Mathematical-Logic
の第６章、７章です。

11 ：

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 ：

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 ：

引っ越し終了
スレ汚しすみません。

14 ：

>>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 ：

>>前スレ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 ：

そのうち、記述論理が一階述語論理にとって替わるのかな？
昔、様相論理を使って集合論を記述してどうの、という話があったけど、下火になったしね。
様相論理を記述論理に直して再チャレンジってことかな？

17 ：

Zermelo の集合論で出来ることと出来ないことがまとめてある文献ってありますか？

18 ：

前スレ942の
>記述論理ってかなり便利じゃないだろうか？決定可能だし...。
>量化記号が一般化されているし、
ってところは、ハッタリだったという理解でおk？

19 ：

昨夜、あっという間に新スレへの移行が完了してしまっとるなあ。実に見事だ。
勝手に「自称次スレ」を立ててたアスペは、指を咥えとるしかなかったんだろな。
この新スレには、アスペみたいな奴が現れないことを祈ろう。
自分で立てた隔離スレで騒いだまま、ずっと出てくるなよ。

20 ：

>>17
纏まっている文献は知らないけど、
ZF では成り立つが Zermelo の集合論で成り立たないことが有名な結果は幾つかある。
一番有名なのはω＋ωがフォンノイマン順序数として存在すること。
ただ、順序型としてのω＋ωは滅茶苦茶弱い算術でも扱えるので、実際の数学には影響はない。
本当に数学的な命題での例となるとそんなにないかな。
選択公理スレにも書いてある通り、ボレルゲームの決定性はその一例。
他に、「二つの一階の構造が、初等同値であることと、あるウルトラフィルタによる超冪が同型であることは同値」
っていうシェラハによるモデル理論の金字塔的結果は、
置換公理なしでは無理だって聞いたことがあるような。

21 ：

>>18
量化記号が一般化されているかは言葉の使い方次第だが、
推論のタブローは必ず停止するかクラッシュするので決定可能。
だからこそ計算クラスで表現力が調べられる。

22 ：

>>16
>昔、様相論理を使って集合論を記述してどうの、という話があった
詳細きぼん。それって、様相論理は決定可能だから、決定可能な集合論を作ろうってこと？

23 ：

どうやらアスペはマツシンだったっぽい。
議論の仕方から脱線する話題まで、マツシンそのものと言える。
自分の隔離スレで、「直観主義は直観主義論理を採用すること」等々、
素人っぷり丸出しのこと喚いているぜ。

24 ：

803 ：１３２人目の素数さん：2011/12/26(月) 02:31:25.06
　　直観主義で提唱された論理が直観主義論理っていうだけで、
　　直観主義の研究＝直観主義論理の研究、ではないんだがな。
　　直観主義っていうのは、論理の部分だけではなく、非論理的公理の部分や、
　　その他数学のあるべき姿全般に対する哲学的主張（例えば形式主義に反対するなど）までひっくるめた
　　文字通り一つの「主義」なんだけどな。
　　直観主義論理はその一部分に過ぎないし、その部分だけならば形式主義とは矛盾しないわけだ。

25 ：

アスペとの基礎論論争は、隔離スレでやってくれ

26 ：

折角マツシンは自分で隔離されているわけだし、放っておけば害はないだろ。
相手しないと、こっちの本スレに出張してくるの？

27 ：

>>20
>他に、「二つの一階の構造が、初等同値であることと、あるウルトラフィルタによる超冪が同型であることは同値」
>っていうシェラハによるモデル理論の金字塔的結果
その証明が書いてある文献、教えてもらえますか？

28 ：

>>20
すみません、もう一つ。"フォンノイマン順序数" って何ですか？

29 ：

ググるべし。ググるとこんなんが出てきた：
フォン・ノイマンに由来する順序数の定義を仮定しているからで、
その中で個々の順序数は先行する全ての順序数の集合になっている。このような定義はブラリ＝フォルティがパラドックスを考案した当時はまだ知られていなかった。
(http://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 ：

お聞きしたいことがあります。
一階述語論理の公理系Tが帰納的に記述可能であることの厳密な定義は何でしょうか？
公理系がデタラメに構成されていないことというニュアンスは分かるのですが…

31 ：

>>16
＞そのうち、記述論理が一階述語論理にとって替わるのかな？
今の計算機の原理が変わらない限り一階論理がなくなることはない。
＞昔、様相論理を使って集合論を記述してどうの、という話があったけど、下火になったしね。
様相論理は可能世界を用いて内包を使う意図があって導入された。
様相論理が扱う文は一階論理で透明性（代入法則が成り立たない）を持たない文なので、
数学や一階論理の様な神の視点の立場に合致しなかった。
＞様相論理を記述論理に直して再チャレンジってことかな？
既にはじまっている。
人工知能では概念を扱うためオントロジーが導入された。
オントロジーは最上位の概念としてメタなオントロジーを持つとされるが、
とりわけSUMOという体系はサブシステムとして集合やクラスを扱うことができる。
このオントロジーの記述の手段として次の3つが考えられたわけだ。
・パースらが研究していた存在グラフをsowaらが発展させた概念グラフ、また意味ネットワーク。
・記述論理。
・Guarinoの形式的オントロジー。
そして記述論理が最も有望とされている。

32 ：

>>30
読んで字の如くそのまんま。
自然数が与えられたとき、それが公理系Tの公理のゲーデル数であるか否かが
帰納的に決定可能（つまり計算機で判定可能）ということ。

33 ：

>>31
訂正：
様相論理は可能世界を用いて内包を使う意図があって導入された。
↓
可能世界を用いて内包を使う意図があって様相論理へ導入された。

34 ：

>>32
ありがとうございます。
もうひとつ質問ですが、Uは公理系Tの再帰的拡大であると言われたとき、TとUのゲーデル数の定め方は異なっていても
よいのですか？

35 ：

>>34
Uは公理系Tの再帰的拡大であると言われたとき、ゲーデル数での表現はまだ定めてないような。
だから32も正確ではなくて「自然数が与えられたとき、それが公理系Tの公理のゲーデル数であるか否かが帰納的に決定可能」
なようにゲーデル数化できる公理系、というべきだね。

36 ：

>>31
>様相論理は可能世界を用いて内包を使う意図があって導入された。
クリプケが可能世界意味論を提案するずっと前から、様相論理はあるわけなんだが。

37 ：

>>35
なるほど。ありがとうございます。

38 ：

>>36
>>33

39 ：

>可能世界を用いて内包を使う意図があって様相論理へ導入された。
何が導入されたん？

40 ：

>>24（＝前スレ803？）
直観主義の非論理的公理ってどういうものがあるんですか？

41 ：

>>39
なんだか文章がおかしくなったのでもう一度。
「クリプキが可能世界を導入して内包を含む文を解釈することに成功した。」
>>31
訂正：
＞透明性（代入法則が成り立たない）を持たない文
↓
　透明性（代入規則による外延交換が成り立つ）を持たない文

42 ：

>>41
透明性といっているってことは、一階術語様相論理の話をしている？
それなら通常の一階述語論理を断片として持つのだから、
数学や集合論を記述することなんて訳ないのでは？

43 ：

誤字訂正：
一階術語様相論理
↓
一階述語様相論理

44 ：

16が言っているのは、以前ちょっと流行った STS (Structural Theory of Sets) のことだと思う。
http://www.blutner.de/AFA/baltag.pdf
様相言語は量記号を持たない（量記号の有無は議論には影響しない）ようだから、
命題様相論理で集合論を記述していると考えていい。

45 ：

>>31
＞今の計算機の原理が変わらない限り一階論理がなくなることはない。
今の計算機の原理と一階論理にはどんな関係があるの？
量子計算機とかDNA計算機とかだと、一階論理ではなくなる？

46 ：

>>42
透明性はエレクトラのパラドクスの発生や宵の明星・明けの明星の問題の話です。
論理へクリプキ意味論を導入すると、
文は一般に内包で、意味論側で可能世界が与えられると外延と解釈できるようになります。
このような不透明な体系、例えば様相論理は数学の記述は難しいとクワインが指摘したのです。
数学は2つの対象が等しいならば、両者で同じことが成り立つという客観（神の視点）を持つからです。
一方で普段通りに、モデル理論を意味論、1階論理を構文論とすれば、
自然言語の透明性が保存され外延交換が成り立ちます。
（実はその後、クワインは透明性を持つ体系での厳密科学の形式化を断念していますが...）
勿論自明なやり方でなら一階論理を含む様相論理で数学を書くことは可能ですが。

47 ：

>>46
内包と外延の分析に有益というのは、様相論理の利点の一つだろうが、
それだけが様相論理を評価する場合の唯一の視点というわけではない。
Baltag のSTSでは、また別の視点が強調されている。
そこで「数学や一階論理の様な神の視点の立場に合致しなかった」と評価するのは
ちとずれているんではあるまいか？

48 ：

>>16
>そのうち、記述論理が一階述語論理にとって替わるのかな？
>様相論理を記述論理に直して再チャレンジってことかな？
えー？記述論理って述語論理のちゃちなサブセットだろ？

49 ：

あちゃー、隔離スレではトンデモ学者に矢田部さんが味方認定されちゃってる。可哀想に。

50 ：

AMC（空でない集合たちの族に対して、それらの各々の非空有限部分集合の族が取れる、という公理）から
選択公理をどうやって証明したらいいのか分かりません。
外延性公理と正則性公理が必要なのだそうですが、誰か分かる方いますか？

51 ：

>>49
俺も何度か経験あるけど、お前のトンデモ理論を俺が支持しているかのように書くのはやめてくれ、と思う。
ツワモノになると、自分のトンデモ理論が正しいと公式に表明してくれ、とかメール送ってくるし。

52 ：

>>44>>47
STSは全く知りませんでしたね。だとすると誤読でしたね。
確かにクリプキの指示とかの話は内包論理に関する様相論理の話でしかない。
>>45
＞今の計算機の原理と一階論理にはどんな関係があるの？
一階論理程度の表現能力があれば十分だというところですね。
ホーン節はじめ分解原理・SLD導出・失敗による否定・エルブランモデル。
論理プログラムは部分帰納関数の表現まで使える...。
＞量子計算機とかDNA計算機とかだと、一階論理ではなくなる？
拡張する必要はあるでしょうね。

53 ：

>>40
直観主義ブラウワーと形式主義ヒルベルトの論争があったように、
直観主義は本来は形式化に反対するものなので、
その論理の部分とか非論理的公理とかいうのはおかしいと言えばおかしいのだけど、
現代的視点で形式化した場合に、と断りを付けておくけど：
有名どころは、
扇定理(Fan Theorem) と
連続選択公理(実数の選択関数で連続なものが取れる)
かな。これだけでブラウワーの数学が形式化できるのか、
もっと公理が必要なのかはよく知らない。

54 ：

補足すると、連続選択公理からは「実数値関数はすべて連続である」という定理が出る。
この定理は勿論、古典論理（とそんなに強くない数学的公理）上では矛盾するけれど。
だから、直観主義は、排中律を拒否して論理を弱めているので、古典論理より定理が少なくなる、というのはある意味嘘。
弱めているのは論理の部分だけで、非論理的公理の部分は一方が他方より強いとか弱いとかって関係にはない。

55 ：

これからの論理は直観にいくよりも矛盾許容論理。
定理ごっそり増える

56 ：

>>52
>＞今の計算機の原理と一階論理にはどんな関係があるの？
>一階論理程度の表現能力があれば十分だというところですね。
十分というだけで、必要でないのなら、
一階論理の断片となる論理がとって替わる可能性があるってことでは？
>今の計算機の原理が変わらない限り一階論理がなくなることはない。
と辻褄があっていない。

57 ：

>>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
http://www.springerlink.com/content/j67206441630333u/

58 ：

>>56
もちろんここで言う一階論理はある程度の断片や拡張も含めた意味で。
ホーン節の分解システムも一階論理の断片だったりするし。
逆に一階論理に推移閉包や述語定数を添加する場合もある。
ペアノ算術の関数や述語をダイレクトに添加した例もよく見る。
ソフト側では、それ以上のファジーや適切論理なんかまで使うけど。

59 ：

>>57
>>57さんへの文句ではないが、
なんでリンク先は出版年を明記してないんだろう？

60 ：

>もちろんここで言う一階論理はある程度の断片や拡張も含めた意味で。
それ言ったら様相論理も含まれるやん。一階論理はある程度の断片だし。
一階論理の代替になれなかった様相論理の次の候補、という話してるのに。

61 ：

低次元な議論は
　も　う　や　め　て　く　れ

62 ：

>>59
確かに不思議ですね。出版は1971年だそうです。
最初のページを見てみると、
この手の話は一般連続体仮説G.C.H.を仮定した結果が多いみたいですね。
概要でもGCHを使わずに、と強調していますし。
これなら置換公理を使っていても全然不思議ではありませんね。

63 ：

>>60
様相論理が一階論理の断片と考えられるといえばそうだけど、
わざわざ様相論理といったときは、大抵モーダルオペレータや
関係構造やらフレームやらを使用する意図があるという前提で。
（計算機で一階論理の述語や関数の引数を制限するのは別の理由。）

64 ：

>>62
選択公理や正則性公理も当然使われているだろうな。

65 ：

第二不完全性の証明は結局分かったんだろうか？
実際のところ、証明に必要な帰納法はΣ_1帰納法で十分だったの？

66 ：

>>55
ネタにマジレスかも知らんが、矛盾許容論理というと古典論理より弱い。
従って非論理的公理をいじらないのなら定理が増えるなんてことはあり得ない。

67 ：

こっちに現れるんだろうからコピペしとこ
999 ：１３２人目の素数さん：2012/01/03(火) 00:46:52.02
　　数理学厨は >>917, >>923 で皮肉られて言い返せなくなったと見えて、姿を消したな。
　　前回は、伝統を良しとして歴史的偶然を批判するっていう自己矛盾を指摘されて言い返せず、
　　暫く消えていたがそのうち何事もなかったように現れた。
　　今後もまたほとぼりがさめたと判断した頃に現れるのだろう、新スレに。

68 ：

>>57
その結果面白いね。
前スレで話題になっていた van Benthem's characterization theorem って、
ふたつの pointed model が modal equivalence であることと、
ultrafilter extension で bisimular であることが同値ってことだったけど、
一階述語論理にすると
ultrafilter extension → ultraproduct
bisimular → isomorphic
という類推ができる。それなのに様相論理では普通に証明できるのに、
一階述語論理については集合論的な公理が必要だとすると、不思議だねえ。

69 ：

>>36
天才と言われるクリプケが可能世界意味論を提案する前の様相論理は何を研究していたのか？

70 ：

>>54
ビショップの直観主義数学は、古典論理上の数学より弱いって聞いたけど

71 ：

ああ、僧正と橋々の構成的解析ね。

72 ：

橋々？僧正は Bishop のことだな。

73 ：

>>69
最初期はルイスやゲーデルやタルスキやマッキンゼーらが
シンタックスのみで研究していた。
ただし関係構造が必要なのは知られていて、
カルナップの意味論なんかが考案された。
既にプライアーの時相論理が開発されていて、
自然数をドメインとして＜を関係として持つモデルがあった。
50年代の終わりにようやくクリプキ構造の完全性定理が出来る。

74 ：

>>69
様相論理の体系で S4 とか S5 とかはあるのに、S1, S2, S3 がないのは不思議だよね？
これはクリプキ意味論以前から様相論理が研究されていた名残り。
S1, S2, S3 は通常の可能世界意味論を持たない。
少し変更を加えれば（非正則世界を許す）S2 と S3 は完全な意味論が可能世界意味論で作れる。
しかし S1 はどうやってもその手の意味論は与えられなかったはず、詳しくは知らない。
あと、S6 以降の体系も世の中にはある。

75 ：

>>74
S1 から始まる体系の系列は、Lewis が厳密内意（論理学スレで話題になってた）の研究で提案したもので、
様相論理の研究と言ってしまっていいのかは疑問。
もっとも A ⊰ B を □(A→B) と、逆に □A を ⊥⊰ A と理解することで、
厳密内意と様相は同じものとみなしていいんだけどね。
（少なくとも S2 以上は。S1 はどうだったか忘れた。）
ある意味、適切論理の先行研究ともいえる。

76 ：

俺は>>68はいいこと言ったと思う。こういうものの見方が必要だと思うんだ。
だからこそ、哲学はこのスレから出て行けとか、哲学的論理学はスレから分けるべきだとか、
そういう「排除の論理」には賛成しかねる。数学系の論理学と哲学系のそれが、
近いことをやっていて、スレが一緒で問題がないのなら、そのまま一緒にやっていくのがいい。
「排除の論理」の人々は、分類フリークっていうか分類することが目的になってると思うんだよね。

77 ：

>>75
>逆に □A を ⊥⊰ A と理解することで
T ⊰ A じゃなくて？
>>76
禿堂。数学系の論理学と哲学系の論理学だけじゃなくて、計算機系の論理学もな。

78 ：

おっと、ここで「数学じゃない」厨が現れて、
哲学なんかと仲良くしようというなら哲学板へスレごと移動しる！
とか言い出すに一票。

79 ：

>>77
>T ⊰ A じゃなくて？
仰るとおりでございます。

80 ：

>>74
またS6以降はどう決まるのでしょうか？

81 ：

我々エイリアンからすれば、
おまいら地球人のやってるコトは全て児戯。

82 ：

今時のプログラミング言語の型理論の基礎はSystem F、
要するに二階λ計算、大体二階直観論理相当。
一階述語論理で十分なんて馬鹿げてる。
動作原理としてはノイマン型でロジックとは関係ないし。

83 ：

>>80
S6:
http://home.utah.edu/~nahaj/logic/structures/systems/s6.html
S7:
http://home.utah.edu/~nahaj/logic/structures/systems/s7.html
S8:
http://home.utah.edu/~nahaj/logic/structures/systems/s8.html
S9:
http://home.utah.edu/~nahaj/logic/structures/systems/s9.html

84 ：

>>82
つまりこれまでの論理プログラムなどのハード計算が使い物にならないので、
非古典論理や型の理論などのソフト計算が導入されている。ということでしょうか？
＞動作原理としてはノイマン型でロジックとは関係ないし。
チューリング機械であるという見方の一方でブール代数を扱うという見方もあるのではないでしょうか？
人の推論と計算機の間にロジックが必要なのではないでしょうか？
>>83
非常に便利です。
これらはどの様相論理の本にも載っていませんでした。

85 ：

訂正：
型理論はソフト計算とは無関係でしょうが...。

86 ：

命題論理とスイッチ回路の初等的過ぎる疑問::
ラッセル方式でNORだけの公理は割とみじかく書き下しできるのに
NANDだけだといやになるほど長くなる
一方
回路設計をNAND素子オンリーで組むのはラクチンなのに
NOR素子オンリーで組むのはなぜか苦労する（手間が時間が）
・・・トンデモ本「数理示申學序説の前書き」より自分で引用
これ数学SFに使おうと思いますが玄人の眼からみると幼すぎますか
できれば評価レスキボンヌ

87 ：

>>84
ハード計算、ソフト計算ってのが何を意味してるかわからん。
論理プログラムとの関係もわからん。

88 ：

>>87
ハード計算が計算機の立場の情報処理技術、
ソフト計算が人間の立場の情報処理技術。
論理について考えると、
命題論理・一階述語論理はハード計算。
様相論理・時相論理・多値論理・関係論理・ﾊﾟﾗｺﾝｼｽﾃﾝﾄ論理・曖昧論理・
ファジー論理はソフト計算。
だから命題論理や一階述語論理の応用である論理プログラムもハード計算になる。

89 ：

>>88
あんたはやっぱり少し見えてる。
>人と計算機の間にロジック
について差し支えない範囲で語ってくれんか？

90 ：

>>89
そんなに詳しく考えているのではないですが、
計算機の内部でブール代数に基くビット演算が起こっていると考えられますが、
（実際のハードウェアがどうなっているかは知りませんが、）
これを厳密かつ人が扱いやすく定義し理論的保障を与えるために、
形式的言語として命題論理のような論理演算システムが必要と考えています。
（もちろん状態遷移系でもチューリング機械でもレジスター機械でも何を駆使してもよいのですが。）
とりわけ一階論理は人の推論に比較的合っているうえにそこそこの表現力も持っているのではないでしょうか？
もちろんプログラムなどの側で有用なのは言うまでもないでしょう。

91 ：

ばかだろ

92 ：

>>31
>今の計算機の原理が変わらない限り一階論理がなくなることはない。
これは一階論理の代わりにチューリングマシンやλ演算でも良いのですよね？
>>88
ハード計算とソフト計算はあなたが考えた独自用語ですよね？
ソフト計算とはヒューリスティクスという意味でしょうか？
>だから命題論理や一階述語論理の応用である論理プログラムもハード計算になる。
チューリング等価なプログラミング言語であるprologで
あなたが示したすべての論理をソフトウェアとして実現できます。
だから一階述語論理の応用はハード計算とは言えません。
ソフト計算に分類した論理を使えばヒューリスティクスを自然に表現できる、
という主張なら納得できるのですが。

93 ：

>>92
＞これは一階論理の代わりにチューリングマシンやλ演算でも良いのですよね？
大抵は組み合わせて使います。
＞ハード計算とソフト計算はあなたが考えた独自用語ですよね？
＞ソフト計算とはヒューリスティクスという意味でしょうか？
Soft computingとHard computingのことですね。
＞チューリング等価なプログラミング言語であるprologで
＞あなたが示したすべての論理をソフトウェアとして実現できます。
例えばそのProlog自体の基礎となっているのが論理プログラムなどという話しですね。

94 ：

>>83
番号が大きいほうだけではなくて、S1 より弱い S0 なんてのもあるのか。
そのサイトは便利だ、�dクス

95 ：

>>74
非正則世界ってなんですか？

96 ：

Sπ

97 ：

>>95
非正規世界(non-normal world)のことだろ。
数学用語ではnormalは普通「正規」と訳される。「正則」はregularね。
非正規世界では、□Aという形の論理式は問答無用で偽とする。
それ以外のconnectiveの意味論は通常通りとする。
正規世界では通常のクリプキ意味論。
S2やS3はこんな意味論で完全になるそうだ。

98 ：

>>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 ：

誰も「すべてを網羅している」なんて言ってないよーな

100read 1read

1read 100read

TOP カテ一覧 スレ一覧 2ch元 削除依頼 ▲
・　次のスレ
28: 大数学者Edward Wittenを語るスレ (82)
29: 複素幾何学★２ (200)
31: ¶ 放送大学の数学科目 5講目 § (367)
32: 一般人と数学オタの違い (99)