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

数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
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/

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

おつ

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

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|- β→□[β]
とする。

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]

証明終わり

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

証明終わり

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

（�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]

証明終わり

４、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
の第６章、７章です。

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 を代入とかって意味をなさない。

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 を自由変数に持つ論理式を表しているものとします。

引っ越し終了

スレ汚しすみません。

>>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]]
が出てくる理由も分からないのですが、これは例のリンク先に書いてあるのでしょうか？
（とは言え、例のリンク先の本は私がこの掲示板で以前誰かに推奨したものですが...。）

>>前スレ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 を使った推論かな？

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

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

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

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

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

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

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

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

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

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

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

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

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

ググるべし。ググるとこんなんが出てきた：

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

つまり順序数を「先行する全ての順序数の集合」として表現した場合の順序数のこと。
置換公理の自然さの解説に「ω＋ωというあるべきものの存在が示せなくなる」なんてのを見かけるが、
それはフォン・ノイマンに由来する順序数の定義を仮定しているからで、
この表現方法にこだわらなければ理由にも何にもなってないのさ。

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

>>16
＞そのうち、記述論理が一階述語論理にとって替わるのかな？
今の計算機の原理が変わらない限り一階論理がなくなることはない。

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

＞様相論理を記述論理に直して再チャレンジってことかな？
既にはじまっている。
人工知能では概念を扱うためオントロジーが導入された。
オントロジーは最上位の概念としてメタなオントロジーを持つとされるが、
とりわけSUMOという体系はサブシステムとして集合やクラスを扱うことができる。
このオントロジーの記述の手段として次の3つが考えられたわけだ。
・パースらが研究していた存在グラフをsowaらが発展させた概念グラフ、また意味ネットワーク。
・記述論理。
・Guarinoの形式的オントロジー。
そして記述論理が最も有望とされている。

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

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

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

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

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

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

>>36
>>33

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

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

>>39
なんだか文章がおかしくなったのでもう一度。
「クリプキが可能世界を導入して内包を含む文を解釈することに成功した。」

>>31
訂正：
＞透明性（代入法則が成り立たない）を持たない文
↓
　透明性（代入規則による外延交換が成り立つ）を持たない文

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

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

16が言っているのは、以前ちょっと流行った STS (Structural Theory of Sets) のことだと思う。

http://www.blutner.de/AFA/baltag.pdf

様相言語は量記号を持たない（量記号の有無は議論には影響しない）ようだから、
命題様相論理で集合論を記述していると考えていい。

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

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

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

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

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

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

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

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

>>40
直観主義ブラウワーと形式主義ヒルベルトの論争があったように、
直観主義は本来は形式化に反対するものなので、
その論理の部分とか非論理的公理とかいうのはおかしいと言えばおかしいのだけど、
現代的視点で形式化した場合に、と断りを付けておくけど：

有名どころは、

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

かな。これだけでブラウワーの数学が形式化できるのか、
もっと公理が必要なのかはよく知らない。

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

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

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

>今の計算機の原理が変わらない限り一階論理がなくなることはない。
と辻褄があっていない。

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

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

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

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

低次元な議論は

　も　う　や　め　て　く　れ

>>59
確かに不思議ですね。出版は1971年だそうです。

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

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

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

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

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

こっちに現れるんだろうからコピペしとこ

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

>>57
その結果面白いね。
前スレで話題になっていた van Benthem's characterization theorem って、
ふたつの pointed model が modal equivalence であることと、
ultrafilter extension で bisimular であることが同値ってことだったけど、
一階述語論理にすると

ultrafilter extension → ultraproduct
bisimular → isomorphic

という類推ができる。それなのに様相論理では普通に証明できるのに、
一階述語論理については集合論的な公理が必要だとすると、不思議だねえ。

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

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

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

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

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

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

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

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

>>75
>逆に □A を ⊥⊰ A と理解することで
T ⊰ A じゃなくて？

>>76
禿堂。数学系の論理学と哲学系の論理学だけじゃなくて、計算機系の論理学もな。

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

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

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

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

今時のプログラミング言語の型理論の基礎はSystem F、
要するに二階λ計算、大体二階直観論理相当。
一階述語論理で十分なんて馬鹿げてる。

動作原理としてはノイマン型でロジックとは関係ないし。

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

>>82
つまりこれまでの論理プログラムなどのハード計算が使い物にならないので、
非古典論理や型の理論などのソフト計算が導入されている。ということでしょうか？

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

>>83
非常に便利です。
これらはどの様相論理の本にも載っていませんでした。

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

命題論理とスイッチ回路の初等的過ぎる疑問::
ラッセル方式でNORだけの公理は割とみじかく書き下しできるのに
NANDだけだといやになるほど長くなる
一方
回路設計をNAND素子オンリーで組むのはラクチンなのに
NOR素子オンリーで組むのはなぜか苦労する（手間が時間が）

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

これ数学SFに使おうと思いますが玄人の眼からみると幼すぎますか
できれば評価レスキボンヌ

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

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

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

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

ばかだろ

>>31
>今の計算機の原理が変わらない限り一階論理がなくなることはない。
これは一階論理の代わりにチューリングマシンやλ演算でも良いのですよね？

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

>だから命題論理や一階述語論理の応用である論理プログラムもハード計算になる。
チューリング等価なプログラミング言語であるprologで
あなたが示したすべての論理をソフトウェアとして実現できます。
だから一階述語論理の応用はハード計算とは言えません。
ソフト計算に分類した論理を使えばヒューリスティクスを自然に表現できる、
という主張なら納得できるのですが。

>>92
＞これは一階論理の代わりにチューリングマシンやλ演算でも良いのですよね？
大抵は組み合わせて使います。

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

＞チューリング等価なプログラミング言語であるprologで
＞あなたが示したすべての論理をソフトウェアとして実現できます。
例えばそのProlog自体の基礎となっているのが論理プログラムなどという話しですね。

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

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

Sπ

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

>>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つ以上のシステム内のオペレータが干渉し合う体系も起こり得る。

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

Vopěnka cardinal ってなんでしょうか？
Vopěnka principle (VP) は前スレで話題になっていましたが。

様相論理も部分構造論理も、幾らでも新たな体系を作ろうと思えば作れる。
研究と称して、そういった体系のお決まりの性質（完全性、有限モデル性、決定可能性、カット除去等々）を
これまたお決まりの方法で証明する、というオリジナリティのかけらもない論文が多すぎる。
よってそれらをすべて網羅する必要があるとは思われない。

>>76
分類フリークといえば、少し前に一人で樹形図書きまくってたアホがいたな。
同一人物かね。

何それｗｗｗ
ちょっと見てみたいｗ

>>99>>101
＞幾らでも新たな体系を作ろうと思えば作れる。
その通りです。
ただし、>>98に掲載されている体系は、
（恐らくHandbook Of Philosophical Logicの３巻からの引用。）
ほとんどがK4やS4の拡張で、
複雑なペトリネット・公理的集合論・線形時相論理などに関する
統一的な研究に由来するようですね。

数セミの渕野先生の文章読んだけど、何か苫米地英人っぽい偏狭さを感じる。

>>70
通常「直観主義数学」と言えばブラウワーの数学（を形式化したもの）を指すでしょ。
ビショップとかマルティンレーフとか、それ以外の直観主義論理上の理論は構成主義と呼ぶと思う。
論理を直観主義にしたものすべてを直観主義数学と呼ぶのは、浅学の窮みｗｗ

F先生が偏狭なのはいまさら(ry

>>103
こんなの↓

980 : 半角混ぜるとずれるので、 : 2011/06/28(火) 21:22:21.01
　　数理論理学━┳━逆数学━━━━┳━高階逆数学
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━無限ゲーム決定理論
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━構成的逆数学
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━計算論的逆数学
　　＿＿＿＿＿＿┣━非古典論理━━┳━様相論理
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━部分構造論理
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━代数的論理
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━高階述語論理
　　＿＿＿＿＿＿┣━公理的集合論━┳━連続体仮説━━━強制法・反復強制法
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━SH・◇・CH・ADなど
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━内部モデル・決定性公理
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━巨大基数・超巨大基数・Rの基数不変量
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━無限集合組合せ理論
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━PCF理論
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━Generic Multiverses・Ω-論理
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━集合論その他(GB,NF,KP)
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━推移的クラスの微細構造論

　　＿＿＿＿＿＿┣━モデル理論━━┳━幾何学的モデル論
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━超準的数学
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━ダイアレクティカ圏・HyperDoctrine
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━真の算術など
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━有限モデル理論
　　＿＿＿＿＿＿┣━再帰理論━━━┳━計算量理論━┳━記述計算量理論
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┃＿＿＿＿＿＿＿┗━次数理論━━━非可解性次数
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━型付ラムダ計算
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━順序数上の再帰理論・高階再帰論
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━解析的階層
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┣━コルモロゴフ複雑性・チャイティン数
　　＿＿＿＿＿＿┃＿＿＿＿＿＿＿＿┗━抽象機械
　　＿＿＿＿＿＿┗━証明論━━━━┳━定理自動証明
　　＿＿＿＿＿＿＿＿＿＿＿＿＿＿＿┣━新井先生とかRathjenの業績
　　＿＿＿＿＿＿＿＿＿＿＿＿＿＿＿┗━構成的数学━━━構成的型理論━━━直観主義型理論

>>105
どこらへんで偏狭さを感じたんだい？

>>104
>ほとんどがK4やS4の拡張で、
>複雑なペトリネット・公理的集合論・線形時相論理などに関する
>統一的な研究に由来するようですね。
統一的な研究に由来する体系なのに、
名称に体系だった趣がまるで感じられないのはなぜ？

人の名前から付いてたり
公理を表す文字だったり
体系の性質に注目して居たりするからでは

「新井先生とかRathjenの業績」って分野の名称だったんだｗ

>>113
定義上、二人しか結果の出せない分野だな。
つーかそういう瑣末な問題以前の問題が多すぎる、その樹形図は。

>>112
自分で幾つもの体系を提案するのに、異なる名付け方法を採用するか？
一人（一グループ）の人間が、一つの研究の中で、いくつものの体系の名称を付けるのなら、
統一的な名前の付け方を採用するのが普通ではないんだろうか？

>>104
> （恐らくHandbook Of Philosophical Logicの３巻からの引用。）

全４巻の旧版の方？　それとも未だ未完結で全１８？巻の新版の方？

>>114
逆に言えばその二人はその分野以外では業績が出せない。
なぜならどんな業績を出しても「新井先生とかRathjenの業績」という分類になるから。

アホのしかもだいぶ昔のレスを肴に、よーもまーそこまで下らん話ができるもんだな。

またF先生祭になる伊予柑

>>116
新版の方。
２章の様相論理の発展。

そこには非正規世界のある可能世界意味論とか書いてありますか？

>>121
載っている。
非正規世界(non-normal world)って名称ではないけど。
あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、
記述されている。
このシステムのクラスNExt(L)自体の順序構造も調べられているよう。

ファジー論理のハンドブックも進行中みたいだね。

http://www.mathfuzzlog.org/index.php/Handbook_of_Mathematical_Fuzzy_Logic

>あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、
>記述されている。
記述する、の主語はなんでしょう？

>非正規世界(non-normal world)って名称ではないけど。
>あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、
>記述されている。
あのう、非正規世界というのは、正規でない体系(S2, S3など)を扱う為に導入したから
名称も非正規世界ということになったわけでして。

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

C^{(n)}-cardinals
Joan Bagaria
Online First, 22 December 2011
http://www.springerlink.com/content/n6330090pxr6832n/

Vopenka とか膨大基数とか拡張可能とか C^{(n)}-基数とか、色々な基数が出てくるけど、
その間の関係ってどうなっているの？
誰か関係を表にした奴へのリンクとか貼ってくれないかな？

前スレの
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
でググっていたら
http://www.imub.ub.es/hocard11/Problems.pdf
が出て来た。 VP に同値な命題がいくつか書いてあり、
さらに WVP なる物もあった。このなかで一つ分からないのが
accessible category の定義だ。
accessible ordinal (cardinal) と似たような感じだとは思うが
解説希望
と質問したのだが、未だに回答が無い。

970 ：958：2012/01/02(月) 22:32:22.66
　　こに質問に誰も答えられないと云う事は・・・

975 ：１３２人目の素数さん：2012/01/02(月) 22:43:55.95
　　>>970
　　そんなローカルな研究解説できる人間などほとんどいない。
　　あなたが調べられる以上の情報は期待できないだろう。
　　Jech本にもVPまでしかのっとらんしな

>>124
主語は集合論だと思いますよ、明文化されてはいませんが。
NExt(L)は様相システムLの正規に拡張したシステム全体の集合族。
公理に関して順序関係を定義していくと、完備分配束が出来たりする。
>>125
いえ、Handbook Of Philosophical Logicの３巻でnon-normal worldって名称が使われていないという意味です。

>>130
122のレスは

>載っている。
>非正規世界(non-normal world)って名称ではないけど。

という部分と、

>あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、
>記述されている。
>このシステムのクラスNExt(L)自体の順序構造も調べられているよう。

の部分は完全に別の話をしているという理解でいいの？
同じ話題だとすると、正規でない L について「正規なまま拡張」なんてできない訳で、
何言っているかやっぱり分からんのだ。

>主語は集合論だと思いますよ、明文化されてはいませんが。
自分の発言について「思いますよ」とは恐れ入るな。

>>132
NExt(L)で記述したのは別人だから別におかしくないのでは？

「あるシステムLを正規なまま拡張したシステム全体のクラスがNExt(L)で、
記述されている。」と書いたのはスレタイスレ446氏だろ？偽者なのか？
自分で「記述されている」と言っておいてその主語が何かについて
「集合論だと思いますよ」と書いたのも彼／彼女だろう。

>>131
＞の部分は完全に別の話をしているという理解でいいの？
そう。改行していないだけ。

>>132
件の本に記述されているのは確か。
しかし、どういった理論（少なくとも集合が扱える）に基いているか不明だということ。

>>128
すべての質問に回答が付くと思うな。
スルーされたくなければスルーされないような書き方を研究するんだな。

１階述語論理の証明体系について皆さんにお聞きしたいことがあります。
全称化：「A→Bから∀ｘA→Bが出てくる（ただしｘはBに自由に現れない）」という推論規則がありますが、
これから理論Tについて「T|-AならばT|-∀xA」を示すにはどうすればいいのでしょう。
命題論理のトートロジーや∀xA(x)→A(t)（tは代入可能な項）、等号の公理は論理公理に入っているものとしてください。
三段論法も推論規則に入っています。

>>128
accessible ordinal (cardinal) の解説希望。

>>135
そういう解説がないと全く読解不能の文章を書く能力ってどうやって身につけられるの？
前スレの「考える人」と同じ臭いを感じる。

結局、何が記述されていると言っていたワケ？

知識も話題も豊富なスレタイスレ446氏は、こまめにレスを返したりする性格も相俟って
このスレの主になりつつあるわけだけど、
>>139が指摘しているようなささっと書いたレスが意味不明な場合があって
（単なるタイポだろうけど、それがときとして致命的に読みにくくなる）
そこを直さないと主としての風格というか権威は得られないと思う。

アスペ＝マツシンについて詳しく知りたい方へ

http://logsoku.com/thread/science.2ch.net/math/1057850128/

たかが２ｃｈのスレで権威ねえ。
言いたいことは分からんでもないがｗ

>>137
少なくとも書かれている規則からだけでは無理。
何故なら ∀ｘA という形の論理式を問答無用で偽と解釈する
（それ以外は通常の解釈をする）意味論を考えると、
それら規則はすべて真であることを保存するが、
証明しようとしているのは真を保存しない。
何か忘れている規則があるはず。

>>137
全称化は向きが逆だろ。
「A→BからA→∀ｘBが出る（ただしｘはAに自由に現れない）」
T|-AならT|-¬∀ｘA→A
全称化よりT|-¬∀ｘA→∀ｘA
よってT|-∀ｘA

>>143
すみません、「A→BからA→∀ｘ」の間違いでした。
>>144

>T|-AならT|-¬∀ｘA→A
この部分と

>よってT|-∀ｘA
この部分がよく分かりません。もしよろしければ詳しく教えて下さいませんか？

本スレッド>>1の
「数学基礎論は、素朴集合論における逆理の解消などを一つの動機として、
　19世紀末から20世紀半ばにかけて生まれ」
は全くの誤りとして論破されました。

本スレッドは反数学的トンデモスレッドとして閉鎖されますので
以下のスレッドに移動願います。

数理論理学（数学基礎論）　その11
http://uni.2ch.net/test/read.cgi/math/1325247440/

隔離スレから出てきちゃダメでしょ

このスレ自身が数学板の中では 哲ヲタやキチガイ専用の隔離スレだったりしてな

劣等感をはき散らすのはみっともない。

>>148
わかっていても言っちゃいけないことがある

>>150
大学の教員はそれをやる非常識人が多いんだよ。
そんな連中が学生相手に社会人としての常識を説いたりするから笑える。

>>141のレス見て発狂したんだろ。

閉鎖されますので、って閉鎖する権限持っているの？
こういう妄想してしまうのは、やっぱり人格障害なんだろうな。

>>153
何をいまさらｗｗｗ

>>139
＞そういう解説がないと全く読解不能の文章を書く能力ってどうやって身につけられるの？
掲示板を読んでいる人間が、隣に座って同じ本を一緒に読んでいる様を想像して書きます。
また、投稿欄に書いた文章を決して読み返さないこと。
（レス数を減らしてじっくり書き込む時間をとるのがベストなのかもしれない。）

＞前スレの「考える人」と同じ臭いを感じる。
確かに文体が似ていますね。
考える人（＝考えない人）というコテハンは、このスレのその5辺りから時折出没していますよ。

>>140
以後、レスの数は減らします。

>>155
本を読んだけど理解できない人に解説するつもりで書いていて、
まだ読んでない人に自分のレスが理解できるか考えてなかったという事ですね。
その本をまだ読んでいないから内容を聞いている、と気がつくべきだと思います。

>>156
お前さんも文章を推敲した方がいい

>>156
> 156 名前：１３２人目の素数さん [sage]： 2012/01/07(土) 23:18:50.20
> >>155
あなたは
> 本を読んだけど理解できない人に解説するつもりで書いていて、
> まだ読んでない人に自分のレスが理解できるか考えてなかったという事ですね。
と私は思います。
あなたは、わたしが
> その本をまだ読んでいないから内容を聞いている、と気がつくべきだと思います。

>>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]
　　削除対象アドレス：
　　　　http://uni.2ch.net/test/read.cgi/math/1325513069/
　　削除理由・詳細・その他：
　　　　数理論理学（数学基礎論）　その11
　　　　http://uni.2ch.net/test/read.cgi/math/1325247440/
　　　　と重複しているため削除願います。

ちなみに同じく埼玉のマツシンと思われる人物が

498 ：数理論理学者：2011/10/30(日) 09:40:31.00 HOST:d180.GsaitamaFL22.vectant.ne.jp<8080><3128><8000><1080>[116.91.89.180]
　　削除対象アドレス：
　　　　http://kamome.2ch.net/test/read.cgi/math/1319895756/
　　削除理由・詳細・その他：
　　　　スレッドのタイトルについて審議中、
　　　　合意案を無視して勝手に立てられた為。

　　　　タイトル審議スレ
　　　　数学基礎論スレのスレタイを決めるスレ
　　　　http://kamome.2ch.net/test/read.cgi/math/1319788429/

という削除依頼も出している。
自分で削除を依頼したスレの次スレを自称するのに勤しんでいるという矛盾に
本人は気づいていないようだな。

２ちゃんのテンプレの"間違い"を正すより、
スタンフォード哲学事典(SEP)の"間違い"を正すほうが
よっぽど価値があることなんではないのか、マツシンよ。
SEPに特攻した武勇伝を期待しているよ。

>>148は、>>67に反論できなくなって、捨て台詞ってこと？
気の利いたことが言えなくなった奴って痛々しいな。

そうだな、ここのスレの間違いが訂正されてもここの住人くらいにしか恩恵はない。
スタンフォードの事典の誤りが訂正されたら、世界中に恩恵がある。
あの記事の誤りを訂正させたら世界中から賞賛の嵐だぜ、マツシンよ。
こんなスレのテンプレなんて下らんことにこだわらないで、世界に羽ばたこうぜ、世界のマツシン！

マツシンあるいはアスペと呼ばれている人は、本気であんなこと言っているの？それともネタ？
基礎論の最初の目的（の一つ）がパラドックスの解決だったかということと、
基礎論の研究の結果実際にパラドックスを解決できたかという、
全く別の問題（一方は歴史の問題、もう一方は数学または哲学の問題）を混同していて、
自分でそれに気づかないって普通の感覚では理解不能なんですが。
やっぱりネタで言っているんではないのかと。

ネタだと思ってるんなら、火傷しないようにスルーしとけ。
奴には関わらんでいた方が幸せ。
と、何度か奴と関わったことのある俺がいっとく。

そのマツシンって奴、素人が！素人が！って言ってるけど、
自分はどんな論文出版しているんだ？誰かデータ持ってないかな？
区体論の人と同じく、自分も素人なのに虚勢張って言っているだけか？

>>127
C^{(n)}-基数というのは、一種類の基数ではないようだよ。
可測、超強、超コンパクト、膨大、超膨大等々、
様々な巨大基数公理のC^{(n)}-版が考えられるということらしい。

>>145

>>T|-AならT|-¬∀ｘA→A
>この部分と
T|-AならT∪{¬∀ｘA}|-Aで、演繹定理より。

>>よってT|-∀ｘA
>この部分がよく分かりません。もしよろしければ詳しく教えて下さいませんか？
排中律より∀ｘA∨¬∀ｘAだが、¬∀ｘAから∀ｘAがでるので、
どちらにしても∀ｘA。

質問です。基礎論の大学院生は博士号取得までにいくつくらい論文を書くのが普通ですか？

頭の悪そうな質問だな．

数理論理学・数学基礎論というのが、もはや一つの分野とは言いがたくて、複数の分野の総称という感じ。
だから基礎論では一概にはいえなくて、分野ごとに論文の書きやすさは大きく異なる。
よく言われるのは、非古典論理や計算機科学寄りだと論文数が多くなる。

>>155
また面白い話題を提供してくれることを期待しています。

446氏が哲学板の論理学スレに出現してる

スレタイスレ446氏にはこっちのスレで
「レシュニフスキーやネルソン・グッドマンなどの形式的オントロジーによるアプローチ」
の数学的側面を語ってもらいたいな。

>>170
勝手な印象だけど、非古典論理と順序数解析とでは、
偏微分方程式と代数幾何くらい論文の多寡が違う気がするな。

>>167
>T|-AならT∪{¬∀ｘA}|-Aで、演繹定理より。
¬∀ｘAが閉論理式でない場合はT∪{¬∀ｘA}が閉論理式の集合で無くなってしまいますが、
それはよいのでしょうか？

どんな公理系を考えているのか知らないけれど、
普通のシステムなら演繹定理に閉論理式という条件は要らないと思う。

そもそもT∪{¬∀ｘA}を公理系と考えることが出来ないのではないでしょうか？
公理系の定義は閉論理式の集合なので。

公理系と考えることが出来なくとも |- は同様に定義できる。

>>170
論文が量産される分野だと、引用される機会も多くなるから、
被引用回数とか G-index, H-index など各種指数も高くなる。
ただ基礎論系の雑誌は、その中でどこかの分野に特化したものは少ないので、
IF は分野の間で格差はそんなにないね。
一番 IF が高い基礎論系の雑誌は Annals of Pure and Applied Logic かね？

>>170 "もはや"ではなくて、当初からそう。
それが数学ではないと言われるゆえん。

>>178
よく分かりました。閉論理式でないといけないと思い込んでいましたが、
意味論と関連付けて考えない限りは
閉論理式に縛られる必要はありませんでしたね。

例えば、岩沢理論。基礎論よりも新しいのに
ずっと深くて重要な進歩がある分野。
これは複数の雑多な分野の総称ではない。

>>67に反論できなくなった奴がまた現れたな。
「一つの分野とは言いがたい」から「数学ではない」って、
さすが追い込まれた奴の発想というか論理展開は独創性溢れてるなｗｗ

>>180 いや、それでも最初期は大きな野望もあって
一つの分野ではあった。しかし、ゲーデル以後、そういった
大きな野望はなくなって、堕落してしまった。

はいはい、また岩澤理論ね、えーとなんだっけ？暗号に応用できるんだっけ？
よくわからないなー。なんにしても>>67に言い返せないのかなあ？

>>183
67って、全然基礎論擁護になっていないじゃん。引用が引用されてて
わけわからん
ちゃんと書きなよ

言い返せってw
あのね、そういうセリフはディフェンディングチャンピオンのセリフよ。

傍流なんだから、打って出ないでいたら、そのまま負けの立場よ

岩沢理論の大きな野望ってなんですか？
この理論だけで一つの分野だとすると、
整数論は「複数の分野の総称」ってことになりますが？

以上、言い返せないバカの負け惜しみでした。

>>188
数学自体が一つの分野であって、本来は切り分けられないけど、
便宜上分けた一部。
身体に対する右腕のような用語。

基礎論屋と話していると、
反論の仕方が負け犬そのもの。

基礎論はこれこれこういう理由で駄目だ、
というと、
いいや、それは違う、こういういいところがある、
という形で反論を期待しているのに、

数学なんて、所詮どの分野もそんなもんでしょ

といった厭世的な答しかかえってこない。

真の数学を知らないんだよな。

このバカは、一つの目標に向かってすべてが進んでいる、
ファシズム的な分野が理想だと思っているらしいな。
ま、若気の至りってやつだろうな。多様性の重要さがわかっちゃいない。

＞真の数学を知らないんだよな。
とか言って逃げないで、その一つの分野である数学の「大きな野望」を解説してくれよ。
いつもごまかして逃げて行くだけじゃないか？

個々の研究者レベルでは、いくつかの方向を向いていて良い。
しかし学問たるもの発展の過程で必ず中心と傍流ができる。これは避けられ無い。
その中心が無数にあったら、それは学問とは呼べない。

基礎論は一つのパラダイムを形成していないんだな。

>>193
ハッタリ乙

>>190
>数学なんて、所詮どの分野もそんなもんでしょ

基礎論屋って皆そんなふうに考えてるの？
だとしたらかなり可哀想な人達

シミュレーションスレのシミュレーションを基礎論に置き換えるとよく分かる

>>196
自演乙

「その中心が無数にあったら、それは学問とは呼べない」とか
「基礎論は一つのパラダイムを形成していないといけない」とか
自分の主観的な仮定に基づく批判をしているようだが、
その仮定は殆どの人間にとって「はあ？」なんだな。
だから別に反論する気も反論する必要も感じない。

基礎論は数理科学で数学じゃない、とか言い張ってたのはどうしたのかなー？
前スレで皮肉られて、言い返せなくなってやめちゃったのー？

>>199
では、>>170
の前半について反論してくれ。
そして基礎論の中心テーマは何？一番大きいものひとつ。

おま、アホか？何が「では」なんだか、サッパリ分からんな。

>>199
ごめん、読み間違えた。読み返してみたら、
やはり、そういったこと全て基礎論では認めちゃっているんだよね。

数学では違うんだよ。
そこにハァ？といってしまうあたりが数学者じゃない。

数学はひとつ。

この理念があるかないかが数学者かそうで無いかを分ける。

数学は一つの有機体なのだが、
そこに基礎論は入っていないということを
認めてしまっているので、

基礎論は数学では無い。

もう合意事項な。

＞真の数学を知らないんだよな。
言ってる本人も知らないだろ、勉強不足で。
いつも抽象的な数学理念ばかり。

たった一度でもいいから具体的な理念を語れば疑念が晴れるのにねえ…

「中心が複数ある一つの有機体」とか「複数のパラダイムが共存する一つの有機体」とか
そういう想像が出来ない時点で視野の狭さを感じるな。
>>191の言うとおり、若気の至りなんだろうから、生暖かく見てるのが一番かね。

いや、こういった合意事項が出来るのは残念なことだが、
それなら俺はもうここでは何も言わない。
言わない理由はシミュレーションスレに書いてあることと基本は同じ。
じゃ、俺は数学して寝る。さいなら。

>>208
具体的に語ってくれれば、すぐにもその合意事項というのを撤回しますよ

逃げちゃったねー。もう来るなよー。

ぐーぐるで「具体的な理念」を探して寝るそうだ。おやすみ。
見つかったらこのスレにコピペしてね。

「基礎論の中でも論文が書きやすい分野と書きにくい分野がある」ということを認めると
「数学はひとつ」という理念を持っていないということになるのなら、
「数学の中で論文が書きやすい分野と書きにくい分野がある」というのもその理念を否定している。
数学の研究現場を知らないアマチュア数学者の臭いがぷんぷんだなｗ

例えば、といいながら出てくるのは岩沢理論だけ。文字通り馬鹿の一つ覚えだな。
工房か？学部生ならもう一つや二つレパートリーがあっても良さそうだし。

>>181
>よく分かりました。閉論理式でないといけないと思い込んでいましたが、
>意味論と関連付けて考えない限りは
>閉論理式に縛られる必要はありませんでしたね。
全称化の規則、気を付けて。
|- の左側に現れる変数を全称化することを禁止しないと、健全でなくなるよ。

>>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 φ　は成り立たない。

これは計算機や非古典論理や証明論では致命傷になり得る。

批判されてるうちが華だと思うな。
無視されて消えていくより。

最近見た学部生向け現代数学案内では、いろんな分野を
紹介しているのに、基礎論だけごっそり無かった。

おお、学部生向け案内とかマジでリア工だったのか

>基礎論だけごっそり無かった。
基礎論以外の数学のすべての分野が全部あっただと？そんなわけあるまい。
世の中には無数に分野があるんだ。
そのうち「学部生向け現代数学案内」の類で必ず紹介される分野、
大学によって紹介されたりされなかったりする分野、
まず紹介されない分野とあるわけだが、
日本では基礎論は二つ目に分類される、っていうだけ。
アメリカではまともな大学なら確実に第一分類だろう。

>>218
つまり、日本では無視できるほど格下だと思っていた基礎論が、
アメリカに行って世界を見てみると結構認められていて、
焦った連中がここで憂さ晴らしをしているわけね。

>>218-219
呑気だなー。

>>218
無数にある分野の一個にすぎないの？基礎論って。

もしかして基礎論を擁護する振りして
実はおとしめるという高等技術か？

>>214
はい。
ともかくモデルによる充足関係T|=AとT|-Aの関係を見るときは
Tとして閉論理式の集合のみを考えるようにすれば問題ない、
しかし演繹定理などの構文論の定理は閉論理式という制約のない形で述べておいた方が
使い勝手が良いという理解でよろしいでしょうか？
>>215
Xに当たるものはいわゆる論理公理・推論規則で|-の左側にくるものは非論理公理と呼ばれるものであっていますか？

数学のすべての分野は無数にある分野の一つなわけだが。
それが貶めているという風にしか読めないなら小学校から国語をやり直してきな。
>>218、無数にある分野の一個「にすぎない」なんて一言も言っていないわけで、
苦し紛れに相手の発言を捏造するのは見苦しいよ。

>>216
君も相手されている内が華だよ。
馬鹿の一つ覚えやっていると誰も相手しなくなるぜ。

>>223
＞Xに当たるものはいわゆる論理公理・推論規則で|-の左側にくるものは非論理公理と呼ばれるものであっていますか？
Xには論理も非論理も両方入ると考えてください。
HKやLKは一般的な一階論理の公理や推論のまとまり。
これにいくつか公理を付け加えたものがPAとなります。

はじめに、言語という使用可能な記号を設定するのですが、
その言語を適当に並べて、「論理式」の条件を満たすような記号列が、
（集合という形で）左側に入ります。
もちろんXに入る公理や推論、右側の論理式でも、言語で設定した記号以外は使用できません。

もう少し直感的に考えると、
ある言語を設定して、その言語を使って作られる論理式がある。
PA |-_PA φ の左側が定義域、右側が値、|-_PA が写像の定義と考えると、
定義域も値もその言語の論理式全体を動くといったイメージ。

訂正：
この説明はよくない。
同じ定義域から複数の値が出現するだろうから。

>>225
え？初めてだよここ書くの。

このスレの
138 ：１３２人目の素数さん：2012/01/06(金) 22:28:15.65
>>128
accessible ordinal (cardinal) の解説希望。
と質問したのだが、未だに回答が無い。

あきらめてググったら？

>>231
もうググったよ。それでも分からん。
ただし、 >>230 を投稿したのは私では無い。

日本人は韓国に来るな

韓国人は日本にくるな

ゆとり民族、ゴミジャップ

関数f(x)がx=aで微分可能なとき、{Af}'(a)=Af'=(a)を証明せよ

できる人いる？

>>230
accessible ordinal (cardinal) = not inaccessible ordinal (cardinal)
なんじゃね？二重否定の除去！

>>232
ぐぐればふつうに出てくるぞ：
http://en.wikipedia.org/wiki/Accessible_category

>>238
いかにも巨大基数と関係が出て来そうな定義だな。

巨大基数と膨大基数の違いをおしえれ

>>235
キムチ野郎

コピペ

75 ：１３２人目の素数さん：2012/01/10(火) 16:38:44.94
　　http://uni.2ch.net/test/read.cgi/math/1317556554/89-94

　　ということなんで選択公理廃止！
　　以後、決定性公理を採用します。

決定性公理：すべての数学体系は決定可能である。

確かに今の日本はゆとり国家

これが古代史に伝わる数百年に一度、
彼の地に誕生するというスーパーゆとり民族か。

>>54
直観主義数学ではすべての実数値関数が連続ということですが、
ということは実数の集合はすべて可測ということですか？

>>240
字義的には huge cardinal が巨大基数と訳されるべきだろうな。
ま、定着しちまったものは仕方がない。
定訳をおかしいおかしい言っているとマツシンになっちまうしな。

>>247
> 定訳をおかしいおかしい言っているとマツシンになっちまうしな。

で、常識的な公理をおかしいおかしい言ってるとエムシラになるってかｗｗｗ

このスレを見ると、住人に人気があるのは
・様相論理
・証明可能性述語
・巨大基数
みたいだな。選択公理関係もはやってる？

>>246
可測というにはルベーグ測度が定義できないと話にならない。
何かそれっぽいものは直観主義でも定義できるらしいが、
どこまでできればそれをルベーグ測度と呼んでいいのか、という問題になる。

>>238
232はググりもしなかったことが明らかになったな

12 ：１３２人目の素数さん ：2012/01/12(木) 01:18:39.79
数学基礎論・数理論理学　その11
(p)http://uni.2ch.net/test/read.cgi/math/1325513069/
の奴らは
(p)http://www.imub.ub.es/hocard11/
のような研究集会があった事すら知らん奴が多いようだな
可哀想な数学を知らない人達・・・

すいません、
私は現在統合失調症で職を持たない身なのですが、
明日の論理学の世界に貢献したいと考えております。
そこで以下のように公理系のデータベースの構築をはじめようと考えております。
http://www4.atwiki.jp/mathe_logic/pages/14.html
すべての公理系をクリックすればアウトプットできるような
巨大なデータベースの構築を目指します。
もちろんリンクなどでの立体的なデータ構造を考えております。
データの保管はOracleサーバを考えております。
よろしこお願いします。

また、個々の体系が何を意味しているのかは分かりません。
一アマチュアプログラマーとして皆様に貢献したいです。
上のリストは以前紹介された様相論理のデータベースをもとにしています。
私はマジ基地ですが、よろしこお願いします。

>>252
そいつ（巨大基数スレ12）は232か？
だとすると自分の怠慢を棚にあげてよくもまーｗｗ

>>250
すべての関数が連続ならば、積分を考えるには開集合に測度を持たせられれば十分だろ。
ルベーグ測度なんてのはルベーグ積分の為にあるものなんだから。
直観主義でも開集合には測度を定義できるんですよね？

こんなんあるよ
us.metamath.org/index.html

これの部分構造論理とか線型論理とか様相論理とかのver.があれば
勉強・研究する人には便利だろうな

いちおうE. BishopのConstructive Analysisとか
Foundations of Constructive Analysisとかには
Lebesgue measureが定義してあるみたいだよ

ただ「直観主義数学ではすべての実数値関数が連続」
とかいうときの「実数値関数」とか「連続」という言葉の意味は
普通の数学でいうときのそれとは違うと考えるべきだと思うけどね

A が B より強いというのは A → B が成立して A と B が両立する場合に言うのが
普通なのでそういう意味では片方が他方より強いという関係にはないけど、
数学的公理の部分で、形式的には古典的数学と互いに背反するような
公理ないし定義を採用していることにはなると思う

>>257
なんでそんなめんどくさい貼り方するの？
http://us.metamath.org/index.html

>>258
>ただ「直観主義数学ではすべての実数値関数が連続」
>とかいうときの「実数値関数」とか「連続」という言葉の意味は
>普通の数学でいうときのそれとは違うと考えるべきだと思うけどね
もっともだとは思うが、
それを言い出すと A → B の意味も直観主義と古典論理では違うし、
何から何まですべて違うことになる。
確かに公理系Tに公理を一つ加えただけで
Tに元々含まれる公理の意味は変わるともいえる、背景が違うのだから。
しかし、ある程度の差異は捨象して同一視してしまって比較するってのが
学問というものじゃないかい？

部分構造論理では最近は何が流行っているのでしょう？
詳しい方、解説をお願いします。

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 つるかめ算とかやってたような頭の柔らかい小学生とかはもっと簡単に解けちゃうのか？


http://kohada.2ch.net/test/read.cgi/slotj/1321424162/310-312

線型論理も部分構造論理の一つと考えれば、部分構造論理の中で線型論理は断然はやってるね。

180=nα+B=B+(n-1)α＋α

Lukasiewicz 論理をよく聞くかな。部分構造論理の中では直観主義論理に次いで綺麗な構造らしい。

http://en.wikipedia.org/wiki/%C5%81ukasiewicz_logic

古典命題論理をストローク一本、公理一本で展開することに何かメリットある？

そら時と場合によるだろう。かなり特殊だけど役に立つ場面はあるだろうね。

次の性質を持つ集合 x は一般に何と呼ばれているのですか?

∀y∀z [ [x ∋ y ∋ z ] ⇒ [ x ∋ z ] ]

>>268

　ニートの、ゴミ・クズ・カスの、クソガキ！！！！！！！！！

遺伝的集合とか推移的集合じゃないの？

メンバーのメンバーはメンバーなり。

昔懐かし稲垣メンバー。

>>270
ググってもそれらしき物は出て来なかったが。

>>273
英語てググりなさい

hereditary set, transitive set でググったら、
http://en.wikipedia.org/wiki/Transitive_set
が有った。

しかしその意味合い (定義では無くて背景などの関連事項) が良く分からない。

>>127
巨大基数の表なんざ、ぐぐればすぐに出てくるぞ：
http://en.wikipedia.org/wiki/List_of_large_cardinal_properties

>>276
29 種類どころか僅かしか無かった。

どう見ても29種類以上、書いてあるけどな

>>275
関係Rが推移的とは
∀y∀z [ [x R y R z ] ⇒ [ x R z ] ]

お、スレタイスレ446氏が降臨している！リクエストをコピペしとく。

173 ：１３２人目の素数さん：2012/01/08(日) 19:43:41.45
　　スレタイスレ446氏にはこっちのスレで
　　「レシュニフスキーやネルソン・グッドマンなどの形式的オントロジーによるアプローチ」
　　の数学的側面を語ってもらいたいな。

>>279
＞関係Rが推移的とは ∀y∀z [ [x R y R z ] ⇒ [ x R z ] ]
∀x∀y∀z [ [ [x R y ] & [ y R z ] ] ⇒ [ x R z ] ]
ぢゃないのか？

∀xがあるかないかの違いしか見つけられんが

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

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

>>283-284
乙。大体のは聞いたことあったけど、数えてみると60もあるんだ。
他に俺の知ってるのは hypermeasurable とかかな。

weakly inaccessible とか strongly inaccessible とかは？

どうしてこうもググりもしない教えてクンが多いのか

>>284
dagger が無いんだが・・・と書こうとしたら次に出て来た。

>>252
巨大基数厨の諸君に告ぐ。

巨大基数の集合論とその応用　そのアレフ 0
http://uni.2ch.net/test/read.cgi/math/1326526644/

>>275
公理的集合論では与えられた集合が推移的じゃないと
困る場面が山のようにある

順序数は普通、∈で整列順序付けされる推移的集合として定義される
与えられた集合と同型な推移的集合を作るテクニックとかもある

巨大基数スレも乱立かよ。
マツシンといい、やっぱり基礎論はトンデモ多発分野なだけある。

>>291
マツシンて誰？

>>292
>>141あたりを参照

>>101
巨大基数公理も、幾らでも新たな公理を作ろうと思えば作れる。
研究と称して、そういった公理のお決まりの性質（○○基数から導けて△△基数を導く等々）を
これまたお決まりの方法で証明する、というオリジナリティのかけらもない論文が多すぎる。
よってそれらをすべて網羅する必要があるとは思われない。

>>293
2003年ってもう9年前じゃん。バカじゃね？

8年ぶりにマツシンが活動期に入ったんだろ

>>290
テクニックって一階？二階？三階？

>>294
ネタにマジレスですまんが、
そういう研究で論文が通ったのは精々80年代まで。
いまどきそれだけじゃ、査読を通らん。
非古典論理に比べてかなり健全だろ？

>>280
レシュネフスキーの数学理論は現在の記述論理にかなり近い。
プロトセティックは型理論のようなもので、
オントロジーは真偽ではなく存在の有無を実現するためのε記号を扱う論理学。
aεb（aはbである。）。
この上にメレオロジーを定義してクラスClを実現する。
（「クラス−真のクラス」は集合とならない、実際にはGBの断片＋α）
グッドマンの方はこのメレオロジーの変種の個体計算などを形式化してる。

いくつかシツモソ
＞この上にメレオロジーを定義してクラスClを実現する
クラスCIってなんですか？
＞実際にはGBの断片＋α
どういう断片ですか？αは具体的には？

>>296
マツシンは8年間活動自粛してたわけではないぞ。
その間も他人のブログのコメント欄なんかを中心に精力的に活動してた。

>>298
巨大基数の健全性ｗ

マツシンタンとかエムシラとかsikiとか人生とか長生きしてるよな。今井は生きてる？鑑定団に出たあたりまでは確認したけど。

このスレが巨大基数について一番専門的な話をしているようなので、質問です。
large large cardinal (大巨大基数?)とか
small large cardinal (小巨大基数?)とか
middle large cardinal (中巨大基数?)とか
ってそれぞれどの基数ですか？

large small cardinal とか small small cardinal とかってなんですかｗｗ

>>294
前半部分は全くその通りだが
「...というオリジナリティのかけらもない論文が多すぎる」というのは
現状をまるっきり分かっていない奴の言うこと。
そんな論文見かけたことすらないね。

ネタにマジレスかこわるい

>>304

http://ncatlab.org/nlab/show/large+cardinal

ここ見ると31の measurable cardinal が境界だそうだ。
だから 1-30 が small large cardinal で
32-60 が large large cardinal なんじゃないの？
middle large cardinal って聞いたことないけど、measurable のこと？

>>296　>>301　>>303
何年間も同じ奴を追っかけて・・・ヒマだなおまえら。

logic systemのリスト化...ソフトウェアにするか動的ウェブで実現するか...

追っかけなくても勝手に現れに来るからｗ

>>308
Stanford Encyclopedia of Philophy の Koellner の記事
(http://plato.stanford.edu/entries/independence-large-cardinals/)から引用：

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 のはずだが。

>>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の構成的数学などもある。
それらをオントロジーの枠組みで実現しているものだろう。

>>312
0^\sharp は cardinal ではないからその定義は意味をなさない罠ｗｗ

>>304
俺は>>308の流儀と>>312の流儀、どちらも聞いたことがあるけど、
きんちんとした定義はないんじゃないかな？
だから23までが small large cardinal
32以降が large large cardinal でいいんじゃない？
ついでにその間の24-31が middle large cardinal とか新説を唱えてみる。

>>313
その理論の強さはどれくらい？ZFC より弱いの強いの？

>とはいえ、集合論いらない数学は
>Feferman・Aczelの構成的数学などもある。
>それらをオントロジーの枠組みで実現しているものだろう。
「それら」は何を指していますか？「実現している」の主語はなんですか？
スレタイスレ446氏のレスは相変わらず読みにくいんですが。

コアモデルがあるような巨大基数は小さいとか言ってみるテスト

?してみるテストって久しぶりに見たw

>>314
κ is a 0-sharp cardinal if there is a non-trivial elementary embedding j: L → L whose critical point is κ
と定義すれば>>312の定義が適用できる！

つまり、0-sharp cardinal は cardinal でないこともあるってことだね。

312の定義に意味を持たせるには
if“V ⊨ κ is a φ-cardinal”then“κ is in L”
であればいいので、“κ is cardinal”である必要はないのね。

>>321, >>322
普通に>>320は、最初に「For a cardinalκ, 」を補えばいいだろうが！

基礎論最大の未解決問題ってなんなのでしょうか？

>>323
では 0-sharp cardinal の存在と（通常の意味の）0-sharp の存在は同値？

>>324
間違いなく「P対NP問題」でしょう。
基礎論の各分野での最大の未解決問題となると、分かりませんが。

>>325
Silver indiscernible は順序さえ保てば自由に動かせて
非可算基数はすべて Silver indiscernible なのだから、
critical point を特定の非可算基数になるような
L から L への elementary embedding なんて
(0^\sharp の存在から)簡単に作れる。

自動定理証明系で
証明仮定（証明図）がすべて出力できるソフトウェアはありますか？

>>328
自分で作れば良い。全ての図を少しずつ列挙し、
同時に一方ではそれらが証明図になって居るかどうか少しずつ判定すれば良い。

>>329
それって普通の対話型証明ソフトと変わらないですよね？
私は公理からの論理式のシーケント列を見たいのです。

　３２８の件　スルー　お願いします

>>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 についても同様。

>>326
> >>324
> 間違いなく「P対NP問題」でしょう。

P≠NP?問題は計算機科学の問題で基礎論の問題じゃないだろが。
そいつを基礎論の問題なんて言ったら「問題を横取りするな」って計算機屋が怒るぞ。
そもそも数学の基礎付けとは全く無関係な問題だ。
そのうち、代数屋あたりが解きそうだな。
結局、ロジシャン自慢のBounded Arithmeticでは歯が立たなかったし。

また「基礎論＝数学の基礎付け」とか言う香具師がでてきなすった。
隔離スレが過疎っちまって構って欲しいのか？

>>312の定義を適用するために、
通常では何らかの性質を持つ基数の存在として記述されない巨大基数公理を
そういう形に書き換えてたいようだけど、
そもそも>>312の定義がおかしくないかい？
“is consistent”というメタレベルの言明を挟んでいるのだから、
“V ⊨ κ is a φ-cardinal”と“L ⊨ κ is a φ-cardinal”で出てくる
二つのκが同じもの、というのが意味をなさないよ。正しくは

if “V ⊨ ∃κ(κ is a φ-cardinal)”then“L ⊨ ∃κ(κ is a φ-cardinal)”

ではないかな？

間違えた、正しくは

if “V ⊨ ∃κ(κ is a φ-cardinal)” is consistent, then so is “L ⊨ ∃κ(κ is a φ-cardinal)”

ではないかと。

大学入ったら基礎論やりたいんですがまず何を勉強したらいいですか？
細かい分野としては逆数学とか証明論などに興味があります、よろしくお願いします

>>337
まず君がいまどのレベルなのか教えてくれないと、アドバイスしようがないだろ。

>>333
Bounded Arithmetic で歯が立っていないのは事実だが、
かと言って計算機屋や代数屋の他の技術だって歯が立っていないだろ。
そもそも、どの未解決問題だってその分野の既存の技術で歯が立たないから未解決なんだし、
常に他分野の技術によって解決される可能性は開けている。

よって、未解決問題がどの分野に属しているかは、
その問題自体がどの分野の言葉で記述されているかで決めるべき。
ゆえに、P≠NP?問題は数学基礎論・数理論理学の一分野で(も)ある
理論計算機科学の問題。

巨大基数スレが二つも乱立しているというのに、
巨大基数ネタで一番盛り上がっているのは結局このスレというのは、
なぜなのだろう？

結局みんなアスペが嫌いなのよ。
巨大基数スレは、アスペが独立スレ立てろと言い出したから、
なんとなくみんなそっちに書きたがらないｗ

>>339
チンコに歯立てるなよ

一般向けの本で、高校レベルの知識で理解可能と書いてあるのに、
実際読んだら？の嵐だったよ。
いきなり「標準形」って出てきてどんどん展開していく。
そこに「標準形」の説明はない。俺には理解できなかった。
やさしい入門書あったら、教えてね。

入門書で金をどぶにすてることから「がくもん」がはじまるのかな
自分で失敗したほうが身につくと思われます　んちって

>>343
齋藤正彦 数学の基礎―集合・数・位相 (基礎数学)
で肩慣らししてみたら？（基礎論やらなくても必要な部分）

>>341
アスペだけじゃなく、スレ立てた主も、
教えてもらおうって相手を見下してる偉そうな香具師だったからな。
あっちのスレでアホ丸出しのタワゴトをのたまっているが、
誰も好き好んであのスレ主の相手したいとは思わんだろ。

>>333>>339
ゲーデルがテューリングがでてきたころ、そのような問題がふれている
ということが書いてあるのを読んだことがある。だから、古い問題では
あるのだけれど、計算機科学ができてから特に大きな問題になったと
いうことだろう。

>>339
> >>333
> Bounded Arithmetic で歯が立っていないのは事実だが、
> かと言って計算機屋や代数屋の他の技術だって歯が立っていないだろ。
> そもそも、どの未解決問題だってその分野の既存の技術で歯が立たないから未解決なんだし、
> 常に他分野の技術によって解決される可能性は開けている。
>
> よって、未解決問題がどの分野に属しているかは、
> その問題自体がどの分野の言葉で記述されているかで決めるべき。

P≠NP?問題は別に数理論理学の言葉で書く必要などないのだが。
計算機科学が数理論理学と関係なく生み出して来た言葉で書けるぞ。
Boolean Circuitなんて考え方は基礎論とは全く独立な発想だからな。Razvorovも代数屋だし。

> ゆえに、P≠NP?問題は数学基礎論・数理論理学の一分野で(も)ある
> 理論計算機科学の問題。

理論計算機科学が数理論理学の一分野という認識はお前みたいな基礎論屋の勘違い。
夜郎自大の基礎論屋らしい勘違いというか誇大妄想ではある。

理論計算機科学にはむしろ代数の辺境分野とでも呼ぶべき言語理論なども重要なコアパートとして含まれるし
普遍代数や圏論の応用分野でもあるのだから、理論計算機科学は数理論理学の一分野なんかじゃない。

むしろロクな問題もなくロクにポストもなかった基礎論屋が「計算機がらみなら問題も色々あるしメシも食えそう」って
理論計算機科学でやってた問題をつまみ食いするようになったのが９０年頃からの傾向。

基礎論屋のほとんどは見向きもしていなかったMartin-L\"ofの型理論とかが
計算機言語の型システムの高度化にも使えるという計算機屋の仕事が計算機科学側で流行り出してから、
慌てて基礎論屋が飛び付いてつまみ食いして計算機科学的には何の使い物にもならない瑣末な視点の論文を基礎論屋が粗製乱造して来たのが実態じゃないか。
型理論の論文は基礎論屋が乱入して来てからロクなのが出ていない。ずっと昔からやっていたMartin-L\"ofとかには当然ながら俺も敬意を表するが。

>P≠NP?問題は別に数理論理学の言葉で書く必要などないのだが。
>計算機科学が数理論理学と関係なく生み出して来た言葉で書ける
頑張れば書けるよね、それがどうした？
代数の問題だって頑張って幾何の言葉や解析の言葉で書きなおせる場合が多い。
だからその問題が幾何や解析の問題だと言い出せばのはこじつけ。

>理論計算機科学でやってた問題をつまみ食いするようになったのが９０年頃からの傾向。
>基礎論屋のほとんどは見向きもしていなかったMartin-L\"ofの型理論とか
君の「俺様歴史観」によるとそういうことになるわけね。
あほらしくてわざわざ反論する気もしないな。

>>335-336
κを定数記号だと理解すれば、>>312はそのままで>>336の意味になると思うがの

>>346
>あっちのスレでアホ丸出しのタワゴトをのたまっている
いや全く。
巨大基数（的）性質なのに、名前付けるのに「存在すれば」という仮定つけてる、
なんてのは巨大基数のなんたるかがまるっきり分かっていない証拠。
巨大基数に手を出す前にもっと勉強すべきことがあるだろう、って話。

>>345
ポチらせていただきました。どうもです。

>>350, >>336
俺は>>312の記述が間違っていて、
ZF(C) |- (∀κ:cardinal)[κ is a φ-cardinal → L ⊨ (κ is a φ-cardinal)]
が small large cardinal の定義だと思っていた。
これだと０♯とか、そのままでは適用できなくなるでしょ？

結局、small large cardinal とか large large cardinal とかってなんなの？どの定義が正しいワケ？

スレタイスレ446氏はその後出てこないの？
また新たなネタをもたらしてくれることを期待しているんだが。

自演乙

BBQ が止まっています
BBX が止まっています
ほんとに？

>>353
実際にいままでに提案された巨大基数公理については、どっちの定義でも同じこと。
確かにゼロシャープとかの場合は、ちょっと定義をいじらないといけないけどね。

スレタイスレ446氏まだー？

数学基礎論は、哲学的問題に数学を持ち込んだという意味で「数理哲学」と呼ぶべきものだと思う。
「数学に関する哲学」という意味での「数理哲学」は、一般的な「数理○○学」の用法から逸脱していて適切ではない。

生命とか国家について考えてるわけじゃないから哲学とまではいかないだろう。
論理学のうち数理的にやれる部分を数理論理学と呼び、研究の発展とともに「数理的」の内容が変わっていく、って感じじゃないの？

はっきり言って哲学とは関係ない。
皆、やりたいことをやっているだけ。

世界 50 億人誰にでも分かる表現が可能なのが数学。
そうで無いのが哲学。

>>363
それはハッタリ的アフォリズムでしかない

阿保リズム

>>361,363
現代哲学には大陸哲学と分析哲学があります。
生命や国家について語り人類に共通な真理とは限らないのは大陸哲学です。
擬似問題を切り捨て明晰さを重視し自然科学と親和性が高いのが分析哲学です。
数学の哲学は分析哲学の一分野です。

大陸哲学
http://ja.wikipedia.org/wiki/%E5%A4%A7%E9%99%B8%E5%93%B2%E5%AD%A6
分析哲学
http://ja.wikipedia.org/wiki/%E5%88%86%E6%9E%90%E5%93%B2%E5%AD%A6
数学の哲学
http://ja.wikipedia.org/wiki/%E6%95%B0%E5%AD%A6%E3%81%AE%E5%93%B2%E5%AD%A6

>>366
ならなんでやたらドイツ語の基礎文献が多いんだ？

ごめん、ちゃんと読んでなかった。
撤回する。

哲学なら現代と限定するのはそもそもおかしくね

そのへんは、数学を現代数学と限定するのが本来おかしいのと一緒でしょ

最近有名になったサンデルとかの政治哲学とかも分析哲学よりだし
国家や生命についての問題は疑似問題に過ぎないというと語弊があるけどね

>>361
そうやって数学の扱える範囲を拡げたのが基礎論の大きな功績の一つ。

>>363
仮に「哲学」と「数学」の違いをそう定義するのなら、
基礎論以前には「哲学」でしか扱えなかったものが
基礎論によって「数学」として扱えるようになった、ということ。

-P(e(x,y)) | -P(x) | P(y) # label(condensed_detachment).
P(e(x,e(e(e(x,y),e(z,y)),z))) # label(XCB).
から
P(e(x,x)) # label(Reflexivity).
を証明。
============================== PROOF =================================
% -------- Comments from original proof --------
% Proof 1 at 3.04 (+ 0.20) seconds: Reflexivity.
% Length of proof is 19.
% Level of proof is 8.
% Maximum clause weight is 48.
% Given clauses 588.

1 P(e(x,x)) # label(Reflexivity) # label(non_clause) # label(goal). [goal].
2 -P(e(x,y)) | -P(x) | P(y) # label(condensed_detachment). [assumption].
3 P(e(x,e(e(e(x,y),e(z,y)),z))) # label(XCB). [assumption].
4 -P(e(c1,c1)) # label(Reflexivity) # answer(Reflexivity). [deny(1)].
5A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)].
5 P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w)). [resolve(5A,a,3,a)].
6A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)].
6 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),e(v6,v5)),v6)). [resolve(6A,a,5,a)].
7A -P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u))) | P(w). [resolve(2,a,5,a)].
7 P(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w))). [resolve(7A,a,3,a)].
9A -P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),e(v6,v5))) | P(v6). [resolve(2,a,6,a)].
9 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),v6),e(v5,v6))). [resolve(9A,a,3,a)].
10A -P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w)) | P(e(u,w)). [resolve(2,a,7,a)].
10 P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),w),e(v5,w)),v5),x))). [resolve(10A,a,7,a)].

11A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)].
11 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w)),v5),e(v6,v5)),v6)). [resolve(11A,a,7,a)].
14A -P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w)) | P(e(u,w)). [resolve(2,a,7,a)].
14 P(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5))). [resolve(14A,a,3,a)].
28A -P(x) | P(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),w),e(v5,w)),v5),x)). [resolve(2,a,10,a)].
28 P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),e(e(e(e(v5,e(e(e(v5,v6),e(v7,v6)),v7)),v8),v9),e(v8,v9)))). [resolve(28A,a,7,a)].
35A -P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w)),v5),e(v6,v5))) | P(v6). [resolve(2,a,11,a)].
35 P(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),w),e(u,w)),v5),v6),e(v5,v6))). [resolve(35A,a,3,a)].
57A -P(x) | P(e(e(e(x,y),e(z,y)),z)). [resolve(2,a,3,a)].
57 P(e(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5)),v6),e(v7,v6)),v7)). [resolve(57A,a,14,a)].

141A -P(x) | P(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5)). [resolve(2,a,14,a)].
141 P(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(e(e(e(e(u,e(e(e(u,w),e(v5,w)),v5)),v6),v7),e(v6,v7)),v8),v9),e(v8,v9))),v10),e(v11,v10)),v11)). [resolve(141A,a,35,a)].
262A -P(e(e(e(x,e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),x),w),e(v5,w)),v5)),v6),e(v7,v6))) | P(v7). [resolve(2,a,57,a)].
262 P(e(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,w),e(v5,w)),v5)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9)),v10)),e(v9,v10))). [resolve(262A,a,28,a)].
589A -P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),e(w,u)),w),v5),v6)) | P(e(v5,v6)). [resolve(2,a,9,a)].
589 P(e(e(x,e(e(e(e(e(e(y,e(e(e(y,z),e(u,z)),u)),w),v5),e(w,v5)),e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),e(v10,v9))),v10)),x)). [resolve(589A,a,141,a)].
1754A -P(e(e(x,e(e(e(x,y),e(z,y)),z)),e(e(e(u,e(e(e(u,w),e(v5,w)),v5)),e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9)),v10))) | P(e(v9,v10)). [resolve(2,a,262,a)].
1754 P(e(x,x)). [resolve(1754A,a,589,a)].
1755 $F # answer(Reflexivity). [resolve(1754,a,4,a)].
============================== end of proof ==========================
1階論理の証明は省略してもここまでの分量になる。

できたら正誤表もヨロ
・・・ともかくGJ・・・感謝

巨大基数の数理哲学的な説明ってどうなってるの？

　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_
　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、
　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ
　　　　　/　　　／:::::／　　　　　　　　　　　＼
　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 |
　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 |
　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ|
　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　
　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。
.　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。
　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。
　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて
　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。
　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は?
　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？
　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼
.　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼
　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 |
　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､
　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣|
　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/

誰もお前みたいなブスとは付き合いたくねえ。

>>375
何に感謝したの？？

ざっくり言って、第二不完全性定理は、もちろん第一不完全性定理の系で、
第一不完全性定理は不動点定理の単なる系なのだが、その不動点定理も、さらに
なにかメタな洞察があって、そこからみれば自明な定理である、なんていう話は
聞いたことあるかな？

証明の仕方によっては
系になり得るけど
第二は第一と無関係に証明できるし
第一も不動点定理と無関係に証明できるからなぁー

>>381
たしかにそりゃそうなので前段は余計なことを言ったかもしれん。
ただ、オリジナル（ゲーデル）では380で書いた順番だったから
それが一番自然な順序と言えなくもないだろう？
まあそれはよいとして、後段の、不動点定理が成り立つのはそりゃ当然だ、
と見えるようなメタな定理ってあるんかな？しつこくてすまんが。

対角線論法や自己参照のイメージで良い。
似たような論法は計算論全般でよく出てくる。

>>383
それは分かるのだが、たとえば、ブラウワの不動点定理とラムダ計算における不動点定理に
共通する成立条件は何なのだろうか？あるいはこうした不動点定理を最も抽象化した定理って
どんな形をしているんだろうか？という疑問なのだが。おかしいか？

λ計算は数学の関数の性質をすべて抜き出せるからなぁ。
共通する性質はある程度の算術が作れるってところか。

>>384 >>385
圏論ではそういう抽象化をやってないか？

やってます。
過去スレでも話題になってます。

>>387
スマン。どのあたり？

圏論好き集まれスレで話題になってるよ。

>379
萌え材につかいましたが・・・やはり問題あり?

>>386
>>387
>>389
Lawvereの定理のことを言ってるんだとしたら、あれはゲーデルや通常の不動点定理を
それほど抽象化したものにはみえない。記法を換えただけにみえるのだが。

おほほ猫

ケケケ猫

>>391
同感。
結局は対角線論法が根源的な説明に思える。

>>393
あんた全てのスレッドを監視しとんのか？
あんたとは無縁じゃろう、この話題は。

>>395
何処を監視するのかは私の勝手なのでね。

猫

こんばんは。初めて書き込むのですが、論理学の質問をしたいと思って
ネット上を探していたらここにたどりつきました。ご助力願います。

質問　Ｌｐの論理式でないのはどれか。

(1)∀w∀x∃zＲ(x,z)
(2)∀xＰx⊃∀xＲ(x,c)
(3)∀xＰx⊃∀cＲ(x,c)
(4)∀z∀x(∀xＰx⊃∀zＲ(zz))

です。出題の意図がわかりかねまして質問しました。
どうぞよろしくお願いします。

「Ｌｐの論理式」という表現は、貴方の持っている本特有の言葉遣いだと思われます。意味がわかりません。

すみません。
どうやらLpというのは「初等論理の言語」を表しているようで、
⊃、¬、∧、∨、∀、∃を表すようです。

>>397
本？それとも講義？
本なら書名を教えてくれない？

講義です。
その先生が独特に使うのでしょうか…。
もう途中から何言ってるのか、って感じで困ってたんです。
最後に課題を出されまして…。
専門ではなく教養なので、おそらくそこまで難しいことは言ってないとは
思うですが…。

>>397
素直に考えると
4番が量化記号がダブって束縛しているのでおかしいけど、
論理式の定義によるからなぁ

397です。レスありがとうございます。

もうすこし追記します。その先生によると

Lpの論理式（Ｆ）とは、次の(1)〜(4)を繰り返し適用して構成される
有限の記号列のことである。
(1)各atomic formula　αはＦである。
(2)αはすでにＦであるとわかっている⇒（¬α）もＦである。
(3)α,β∈Ｆ⇒(α⊃β）,(α∧β）,（α∨β）∈Ｆ
(4)α∈Ｆ⇒（∀xα）∈Ｆ

というのが定義のようです。

素人にゆっくり教えてやろうという講義ではなく、先生の独り言的な講義
だったため、素人のこちらは全くわかりませんでした…。

>>403
わきからごめん。
>もう途中から何言ってるのか
こういう状態でこの宿題だけやっても、という気はするが、参考までにコメントするよ。
｢Ｌｐの論理式である｣というのは、直感的には，｢文法に合った式である｣という意味だよね。
ここに貴方が書いた定義に照らすとすれば、(1)-(4)はどれも文法に合っていると思う。
しかし、ふつうの定義では，(1)(2)は（かろうじて）文法に合っているが、(3)(4)は文法に
合っていない（Lpの論理式でない）と思われる。というのは、，(3)は定数cが限量変数に
使われているし、(4)は（402も言うように）zとxが限量変数としてダブって使われている
から。どうかな？

>>403
その定義だと1が論理式じゃないね。
∃記号が¬∀¬と交換できないなら。

皆さん、ありがとうございます。
404さんもおっしゃる通り、この状態では…ということはわかっていますが、
どうしてもこの単位が必要という現状です。
頼りにするのがこの板だけというまわりもあてにならない状況で申し訳あり
ませんが、お付き合いいただけると幸いです。

先ほどの質問につきましては、いただいたアドバイスを元に選びます。

もうひとつだけお願いします。

質問　yは∀xＰx⊃∀yＲ(x,y)の中で、xに代入可能であるか。yes,noで答えよ。

という質問です。
「代入」というテーマで授業した内容からだと思いますが、もう途中から
何言ってるのかわかりませんでした…。

すみませんが、よろしくお願いいたします。

>>406
とりあえず言えることは、
>>397のような問題は通常、
「論理式の定義から作れるものはどれか？」ということが問うているので、
>>403のような定義から作れるか試してみろってことです。

＞質問　yは∀xＰx⊃∀yＲ(x,y)の中で、xに代入可能であるか。yes,noで答えよ。
NOです。
束縛された変数には代入できないです。
※直感的理解
∃yP(y,a)：yは束縛されている、aは束縛されていない。

407さん、ありがとうございます。
ちょっとわかったような気がします。

とすると、

∀xＰx⊃∀yＲ(x,y)において、freeに現れているxにzを
代入した論理式を書きなさい。

という問いに対しては、∀xＰx⊃∀yＲ(z,y)

と答えればよろしいのでしょうか。
もはやこんな感じ、という理解しかできませんが…。

>>397
通常の形成規則にしたがえば、論理式(wff)である記号列は(2)だけで、(1),(3),(4)はwffsではない。

うぇるふぉーむどふぉーみゅら

圏論による数学の基礎について語ろう！

上のほうで圏論と集合論（巨大基数）の関係が話題になってたけど、
圏論を他の代数構造同様に（クラスサイズっていう違いはあるが）集合論の中で実現して
っていう話だから数学の基礎としての圏論というのとはなんか違うな。

>403だけ？∀に関する他のルールは無いの？
普通に考えれば∀zが入れ子になっている(4)が怪しいけど、
仲間外れというなら束縛したwの出て来ない(1)も怪しい。

量化記号がダブるとか、∀zが入れ子になるとか、束縛したwが出て来ないとか
そんな理由で論理式にしないなんてことよくするの？

>>414
とにかくあれは問題のための問題（悪問）と思う。
実際に使うために論理式を書く場合は、変数はダブらないように書くし、
中に出てこない変数を束縛するなんてこともしないだろ。

そうだな。あんなことをやってるから教養は要らないってことになる。あれは文系かな？どうせ論理を教えるならもっと違うやりかたがあるがな。

圏論上の形式的議論を圏論だけでできるんですか？
述語論理は当然のように使っているようにみえるんですが、これでは圏論は自立していないと
いうことにはならないのですか？

集合論だって述語論理は使っている。
述語論理の上のレベル（というか非論理的公理）として、
集合論などのほかの「数学の基礎」から自立できているかが問題。
述語論理から独立させようなんて誰も考えてないよ。

そうだけど、集合論におけるメタ数学的議論は集合論で形式的に扱う事が出来るけど
圏論におけるメタ数学的議論は圏論で形式的に扱うのはかなりの困難があるし、
その全ての側面を扱うのは難しいと思う

>圏論におけるメタ数学的議論は圏論で形式的に扱うのはかなりの困難がある
慣れの問題でしかない、という説もある。そしてその説には一理ある。

前にちらっと話題に出てきた STS (Structural Theory of Sets) は、
述語論理から独立させて、様相命題論理で集合論を記述しようという話。

つまり比喩的に左側が機械語側、右側がユーザー側として階層をまとめると、

>>412が圏論と巨大基数の話に関して言ったこと：
一階述語論理　−　集合論　−　各数学（圏論もこの一つ）

数学の基礎として圏論
一階述語論理　−　圏論　　−　各数学

STSの目指すもの
様相命題論理　ー　集合論　−　各数学

>>418
>述語論理から独立させようなんて誰も考えてないよ。
だったら圏論は述語論理の単なるマクロ集であって、共通の基盤言語だなんて言い方は
しないほうがよいのではないですか？

>>412
こんなんあるでよ

http://www.math.ucla.edu/~asl/bsl/1303/1303-002.ps
RELATING FIRST-ORDER SET THEORIES AND ELEMENTARY TOPOSES

>>422
なんか色々なことをごっちゃに理解しているように見受けられるな。
「圏論が数学の共通の基盤言語」というのは、
数学の色々な構造から共通の性質を抜き出すのに便利というプラグマティックな話であって
「圏論は数学の基礎として数学と述語論理の橋渡しとなる」というのとは
また別の話だと俺は理解しているのだが。

いや、巷で「数学の基礎」と言われていることの中身を突き詰めれば
>>422の言うとおりマクロ集ということでしかないのでは？
もちろん、それは集合論が数学の基礎というときも同様だけど。

＞なんて言い方はしないほうがよいのではないですか？
「集合論が数学の基礎だ」とか「圏論が集合論に代わる基礎となり得る」とかというのは、
ある意味使い古された言い回し。ここの住人が言い出したことではないので、
こんなところで「その言い方はおかしい」と言っても始まらない。

>>425
「数学の基礎」と「数学の共通の基盤言語」は同じ意味内容だと主張したいの？

数学の共通言語はTEXだよ

圏論は所詮モデル論なんだよ。しかし言語の本質はシンタックスだ。
だから圏論は、共通も何もそもそも言語ですらないんだよ。
同じことは集合論にも言える。
わかるかな。

↑あふぉ

シンタックスだのセマンティクスというのは
メタレベルからオブジェクトレベルをいじる場合の手段の区分。

一階述語論理 − 集合論or圏論 − 数学各論

という階層は、
オブジェクトレベル、メタレベル、メタメタレベルなどの
一つのレベルの中での話。
（オブジェクトレベルの一階述語論理は、
セマンティクスだろうとシンタクスだろうとメタレベルの数学各論の一つになる。）
一つのレベルの中でセマンティクスだのシンタクスだの言うのは無意味。

>>430　ややこしいな

基礎付けの話になると、最終的にどっかで循環にならざるをえないからな。
それを尤もらしい美辞麗句で隠したのが、メタレベルと対象レベルの分離、ともいえるわけだｗ

>>430
なるほど。数理論理学を学ぶために最低限必要なセンスとして

＊シンタックスとセマンティクスが区別できること
＊オブジェクトレベルとメタレベルが区別できること
＊シンタックスとセマンティクスの区別と、オブジェクトレベルとメタレベルの区別が、区別できること

の３つを伺っていましたが、最後の区別がよく分かりました。

＞＊シンタックスとセマンティクスが区別できること
＞＊オブジェクトレベルとメタレベルが区別できること
＞＊シンタックスとセマンティクスの区別と、オブジェクトレベルとメタレベルの区別が、区別できること

これ至言だな

シンタックスとセマンティックがはじめに理解すれば良い
メタな視点は後から考えれば良いし、ロジック学習の基礎において必須でもない。

ソースは誰？ぐぐったら鴨さんのはてなが出てきたけど、これが初出？

俺様勉強法を語って自分の無理解をひけらかしちまう馬鹿＝435、哀れだなｗｗ

>>430で言われているように、
シンタックス（構文論）もセマンティクス（モデル論）もどちらもメタ的な視点の話なので、
良い子の皆さんは435のいうことを真に受けてはいけませんよ

そんなことより、圏論による基礎の話はどうなった？
>>423のリンク先の論文の評価を聞きたい。

>>432
ともいえる、なんて控えめである必要はなく、そう断言してしまってもいいと思う
というか「メタレベルとオブジェクトレベルは、避けられない循環を飾る美辞麗句」なんて
基礎付けの本質を突いた至言だと思う、鴨さんの３つの区別と並んで。

はじめはメタな視点を意識する必要がないという話しだが。
>>438の考えを認めるとすべての数学はメタな視点に基いている。
メタを意識する必要が出てくるのは不完全性定理や内部モデルから。

435=441 のいうことが正しい。
430 に書いてあることは、形式論理の研究者のなかにさえ、そのように
思っている人がありが、無限連鎖に陥るだけで、意味を考えることができ
ない。

学部教養レベルの確認が一段落したら、圏論によってシンタックスとセマンティックスの
区別がなくなるという話もしようぜ。

ちょうど話題が出たんで、甲鳥さんのページで質問です。
ttp://taurus.ics.nara-wu.ac.jp/staff/kamo/shohyo/logic-2.html
＞著者は、また、自然数論は完全性定理が成り立つには強すぎる体系である旨の
＞主張もしている。それも大違いである（こちらは、かなり広まっている誤解だ
＞が、どんなに広まっていようと、専門家に一言相談すれば「それは間違ってい
＞る」と言ってもらえるのだから、言い訳にはならない）。一階ペアノ算術（自
＞然数の加減乗除と大小比較ができて数学的帰納法が自由に使えるが、関数一般
＞や集合一般を自由に扱うことはできない世界と思って、ほぼ間違いない）は一
＞階述語論理上の公理系なので、完全性定理が適用できる。したがって、一階ペ
＞アノ算術の公理系から証明可能な式全体と、一階ペアノ算術の公理系が真とな
＞るすべての解釈で真となる式全体は、一致する。これを、「一階ペアノ算術は、
＞一階ペアノ算術のすべてのモデルに対して、健全かつ完全である」という。

という部分ですが、
「一階ペアノ算術は、一階ペアノ算術のすべてのモデルに対して、健全かつ完全である」
というのは本当に成り立つんでしょうか？今一書いてあることが理解できないのですが。

>>444
もちろん本当だと思うが、どう理解できないの？

あぁ勘違いしていた。
完全性定理は論理だけに関する定理だった。

>>443
こういう人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場

林さんの数理論理学では
述語論理の完全性と古典算術の完全性を別の定理として区別していますね。（独言

>>447 駆け出しだな

＞圏論によってシンタックスとセマンティックスの区別がなくなる
別にそんなこと無いですけど……

と書こうと思ったら既出だった

専門家をバカにできるとは 441=442 はアスペか？隔離スレからでてくんな。

どうでもいいことだが、>>442は別人。

>397　Ｌｐの論理式でないのはどれか。

(1)∀w∀x∃zＲ(x,z)
(2)∀xＰx⊃∀xＲ(x,c)
(3)∀xＰx⊃∀cＲ(x,c)
(4)∀z∀x(∀xＰx⊃∀zＲ(zz))

コピペなら明瞭に(4) R(zz) はwww
誤植でR(z,z)にしても「R(z)三R(z,z)」は未だ証明されてない
よーするに　ここでの単位は　とらぬのが正解
あふぉ　が伝染って　後遺症で困るとおも晴れri

どうも本当にアスペが隔離スレから出てきたようだな

>>441
通常の数学（特に代数構造など）の話でも、
★そういう見方をすれば★メタ的な視点に立っているものが多い、
ということに気づけないようでは数理論理学のお先真っ暗。

とりあえず宣言しとくけど
今夜0時までに
田中の数学基礎論講義の5章までの定理をすべて
Coqで証明するよ＾＾

すげえ！

Definition P1(a b:Prop):Prop:=
a->(b->a).
Definition P2(a b c:Prop):Prop:=
(a->(b->c))->((a->b)->(a->c)).
Definition P3(a b:Prop):Prop:=
(~b->~a)->(a->b).

今日はここらへんまでかな。

スレの勢いからして
もうそろそろ次スレの季節だな

Record L_PA:Type:=
language
(Func:Set)
(Rela:Set)
(arity:Func+Rela->nat).

今夜はここまで

＞430 に書いてあることは、形式論理の研究者のなかにさえ、そのように
＞思っている人がありが、無限連鎖に陥るだけで、意味を考えることができない。
馬の耳に念仏だな、こりゃ。念仏の「こころ」がまるで分かっちゃない。

馬＝442
念仏＝「メタレベルとオブジェクトレベルは、避けられない循環を飾る美辞麗句」

圏論話は終了か？

┌∩┐(◣_◢)┌∩┐
上の方にある、
一階述語論理　−　集合論　−　各数学
の図式は古典的で、考えているのは数学屋だけ。
実際には一階述語論理　−　集合論の間の区別は曖昧。

参考文献を上げて下さい

┌∩┐(◣_◢)┌∩┐
この本にZFCを一階論理で厳密に展開しているので参考にすること。
Axiomatic Set Theory (Graduate Texts in Mathematics) [Paperback]
Gaisi Takeuti (Author), Wilson M. Zaring (Author)
http://www.amazon.com/Axiomatic-Theory-Graduate-Texts-Mathematics/dp/0387900500

>>423
（圏論的意味での）イデアル全体とか取っているのは、
そのトポスが集合論の世界に含まれている前提での話。
「一階述語論理と数学をつなぐ」という意味での
「基礎としての圏論」の研究とは言いがたい。

463が言ってる集合論ってまさか
「集合と位相」で習うようなことじゃないだろうか

>>467 だから言っただろ。駆け出しがうようよしてんだよ

┌∩┐(◣_◢)┌∩┐
一階述語論理の言語にZFCの公理系を添加したものと∈-モデルからなる数学は、
厳密に分離することが出来ない、これは実際に展開してみないと気付きにくい。
例えばキューネンなどの本では述語論理の箇所が省略されているので気付けない。
>>465の本の冒頭が参考になる。

「∈-モデルからなる数学」って何のこと言ってるの？

そもそも>>469では述語論理＋ZFCとその上の数学とを
厳密に区別できないと言っているのに対して
>>463では述語論理と集合論（ZFC）とは区別できないと
少し別のことを言っているように思うんだが

集合論は数学をやる上での基本的な言葉みたいなものだから
基本的な論理と一体だとか言うのは普通の数学やってる人達で、
却って情報系・哲学系の人とか数学でもロジックやってる人は
集合論（ZFC）の公理と述語論理の公理は別のレベルのものだとして明確に区別すると思う
（一部の新論理主義の立場に立つ哲学者等を除く）

他人には意味不明な用語法を断りなしにするのは、トンデモか駆け出しの証拠ｗ

>>463
等号公理は、一階述語論理の公理なのか、集合論の公理なのかはっきりしない、
とかそういう意味で区別が曖昧と言っているのかな？
それはイエメンとサウジアラビアの国境が未画定（つまり曖昧）だから
国家としてのイエメンとサウジアラビアの区別が厳密に区別できない
と言っているようなもので的外れ。

>>466
確かにイデヤールの部分はそうなんだけど、
かなりの部分は一階述語論理の直上のものとして理解できるでしょ、
elementary topos というのは正にそれ故に意義のある概念。
集合論に依存していいのなら Grothendieck topos で十分だった。
その論文では「canonical injection である」という述語が、
集合論と同じ表現力を持たせる為に圏論側で必要な「述語記号」だと言ってる。

とはいえ、集合論に依存している部分とそうでない部分をごちゃ混ぜにしているのは確かに問題。
圏論による基礎を標榜している指導的な研究者である著者達がこんな書き方をするから、
「圏論は集合論に変わる基礎」と言っても

一階述語論理　−　集合論　−　圏論　−　各数学

みたいに「屋上屋を重ねる」ような無駄なこと、っていう印象を持たれてしまう。

┌∩┐(◣_◢)┌∩┐
Oh,Motherfucker!（＾＾；
等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれるので問題なし。

問、等号なし一階述語論理でZFC外延公理から以下を導け：
∀x(x∈a ⇔ x∈b) ⇒ (a∈c ⇔ b∈c)

＞等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれるので問題なし。

こういう人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場

>>473
>みたいに「屋上屋を重ねる」ような無駄なこと
それ以前に、圏論が述語論理（λhol含む）や集合論のような共通言語には到底なりえんのじゃないかな。
言語（道具）にしては難しすぎるし奇妙すぎる。

>述語論理（λhol含む）や集合論のような共通言語
述語論理上の理論である集合論と述語論理を並列な言語としてる時点でアウト！

>等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれる
「等号なし」とは、等号記号が言語に入っていないのか、記号はあるが等号公理が入っていないのか。

中身以前に、自分の発言に必要な情報が欠けていて多義的であることに気づかないってのは、やっぱり駆け出しの証拠だ。
謙虚に勉強しなおすがよろしかろう。

ちなみに、前者だとすると、標準的な外延性公理がそもそも記述できない。
後者ならば>>475の言う通り。どちらにしてもおかしい。

>>478 あんたもそういう区別がやっとできるようになった駆け出しだな。
もっと大事なことを言えよ。

欠けた情報は集合論という言葉に対してもそう。
一階述語論理上のZFC⇒集合論だが逆は成り立たん。

┌∩┐(◣_◢)┌∩┐
Suck me!
等号公理を抜いた一階述語論理。
こいつさんに2項述語＝をぶち込むさかい。

Require Import Classical_Pred_Type.
Section Generic.
Variable U:Set.
Require Export Le.
Require Export Lt.
Require Export Plus.
Require Export Gt.
Require Export Minus.
Require Export Mult.
Require Export Between.
Require Export Peano_dec.
Require Export Compare_dec.
Require Export Factorial.
Require Export EqNat.
Require Export Wf_nat.
Require Import Decidable.
Goal forall n, n<=n.
Goal forall n, n<=n->n<=n.
Goal forall n m, n<=m->m<=n.
Goal forall n m, n<m->m<n.
Goal U=U.
Goal exists n,n<n.
Theorem A0:forall(a b c:nat),a=b->a=c.
Proof.
intros.
先ずは準備っと。

>>473
「数学の基礎としての○○論」の研究なんてのはきょうび流行らない。
元祖の集合論でも、数学の基礎としての集合論の研究なんて久しく聞かないね。

482を恥の上塗りというのだなｗｗｗ

>>485
同感。
ところでmother fuckerの┌∩┐(◣_◢)┌∩┐って
馬鹿さ加減というか無知さ加減が以前の「考える人」と良く似てると思うのだが。

>>484
確かに。部外者が想像する集合論と、実際に集合論で研究されている内容には差異があるかも。
数学の基礎として集合論を志すと、研究の現場に行ってみると
「こういうことをやりたかったのではない！」と思うだろうな。

　　たしかに専門分野としての集合論は「集合というものの性質を定める規約集」ではなく「累積階層という対象の構造を探求する研究」になっていますね。

とはキューネン本の訳者の言。

>>486
禿堂

(*鶏慣れのために算術命題をチェック。*)
Goal forall (n m : nat)(f : nat -> nat), (S n = S m) -> n = m->f n = n -> S (f (f n)) = S m -> n = m.
intros.
rewrite H1 in H2.
rewrite H1 in H2.
apply H0.
Qed.

スレチですまんのだけど、Coqだと
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : eq A x x.
という風に等号を定義するだけで（ちなみに上記の意味は、「Type Aの変数xに対して
x=x（eq A x xのこと）の証明が存在することを仮定し、その証明をeq_reflと名づける」といった感じ。）
eq_rect : forall (A : Type) (x : A) (P : A -> Type), P x -> forall y : A, eq A x y -> P y
というような等号公理が導かれてしまうけど、これってどういう原理なの？
わかりやすい説明とか文献あったら教えてくだされ。エラいひと！

>>481
欠けた情報：⇒の意味
怪しげな記号の使い方をするのもトンデモや駆け出しの証拠ｗ

>>473
>かなりの部分は一階述語論理の直上のものとして理解できる
とすると、ZFC その他一階述語理論としての集合論と同じく、
一階述語理論としての圏論がある筈だけど、そんなん聞いたことないぞ

>>491
それはつまらん言い掛かりにしか見えない

>>491
いや、言いがかりではなく481は何を言いたいのか分からん。
自分で読み返してみてそれに気づけないのなら真性駆け出し。
玄人に質問の意図を伝えられない素人の図、だなｗｗ

Awodeyの教科書に
集合論は数学の基礎だというのと
圏論は数学の基礎だというのは意味合いが違うよ的な話が書いてあるよ

こういうのこそ2chらしくていい
俺は「真性」は大歓迎よ
もっと自己主張してほしい

「集合論の公理系」と「ZFC（＋追加公理）」は
イコールじゃないよというようなことを言いたいんだろうけど、
handbook of set theoryとかJechとかは
事実上ZFCかその保守拡大のBGのことしか書いてないよ
良くてMKにちょっと言及するくらい

結局、「⇒」で何を言おうとしているのかが分からないことが原因。

多分
一階述語論理にZFCの公理を加えることだけが
集合を展開する唯一の手段ではない、という趣旨かと。

>>495
定着した古典的な言葉に新しい意味を付与するってのは、研究を宣伝する際の古典的な定石。
他にも逆数学の Simpson がホームページで「数学の基礎」の彼流の意味を解説している。
「集合論は数学の基礎」というのも、Simpson 的な意味で言われる場合もあって、
Awodey が彼の本で言及しているような意味とは必ずしもならない。
結局のところ、言われている文脈を考慮しなければ、どういう意味かは分からない。
しかし「ひねっていない」言葉の意味、というか伝統的なオーソドックスな意味というのがあって、
特に断り書きがないような場合には暗黙の了解的にその意味で理解すべき、というのがある。
それが「数学各論と一階述語論理を繋ぐ」という意味だし、
これがオーソドックスだからこと Awodey が対比の為に言及している。
（オーソドックスでなければわざわざ対比に使わない。）
このオーソドックスな意味での「圏論による基礎」は、
オーソドックスなだけにかなり長いこと研究されている。
いまどき流行らないというのは認めざるを得ないところだが。

>>492
Elementary topos は、確かにモデルに関して記述される場合が多いけれど、
object と morphism の２つの sort を持つ一階述語論理
（お好みなら identity を使って morphism だけの方法でもいいが）を考え、
identity と composition を関数記号として入れれば、
elementary topos であることを一階述語論理で記述できる。

元々 "elementary" という言葉は、
elementary extension, elementary submodel 等々、
一階述語論理の観点という意味合いを持つ。
トポスの重要な性質をすべて
（上述の言語による）一階述語論理で記述できた、
というのが elementary topos の意義。

公理系に関する研究がないじゃないか、というかも知れないが：
完全性があるのだから、
そうやって記述された elementary topos の公理系で何が証明できるか調べることと、
elementary topos に共通する("elementary" な)性質を調べることは同値。

誤字訂正：
×これがオーソドックスだからこと Awodey が対比の為に言及している。
○これがオーソドックスだからこそ Awodey が対比の為に言及している。

>>501
勉強になる
>トポスの重要な性質をすべて（上述の言語による）一階述語論理で記述できた
これはFOLの記述力から自明じゃないかと思うんだが？

>>503
FOLの記述力に関するどういう定理から自明なんだい？
Lawvere が elementary topos の概念を出す前には、
トポスというのは「層全体のなす構造」って定義しかなかったんだよ？

＞定着した古典的な言葉に新しい意味を付与するってのは、研究を宣伝する際の古典的な定石。
＞他にも逆数学の Simpson がホームページで「数学の基礎」の彼流の意味を解説している。
基礎と言ったらヒルベルトプログラムでの意味しか考えられない単細胞なアスペに聞かしてやりたい。
と思ったらいま自分の隔離スレで活動始めやがったとこだった。
ということはこのレスも読んでいるに違いない。

500だけど、>>505に補足：
「数学の基礎」の一番オーソドックスな伝統的な意味は、
Hilbert Programme の意味での基礎付けね。
でも、アスペに言われるまでもなく、
それが数学的に不可能なのことは既に分かっているので、
それ以降は（数学史の文脈などを除けば）
オーソドックスな意味は500で言った通りってこと。

＊＊論数学では虚数 i=√-1 はある質（表現）からそれと異なった質（表現）
に移る演算単位である。すると空間の距離Ｘとそれと直角な距離Ｙは
異なった質の関係にあります。からｒ＝Ｘ＋Ｙｉです。ＹiやＸの表現を
消すと当然存在量が残ります。消滅表現をＡ＾*と表すとＸ・Ｘ＾2＝Ｘ＾２
（Ｙｉ）・（Ｙｉ）＾*＝Ｙ＾２でありｒ＾２＝Ｘ＾２＋Ｙ＾で
ピタゴラスの定理です。


9 ：?　＊＊論研究報告：2012/02/01(水) 01:09:12.22 ID:2eW/+tej
おっと間違えた。Ｘ・Ｘ＾2＝Ｘ＾２　ではなくて
Ｘ・Ｘ＾*＝Ｘ＾２です。



10 ：?　＊＊論研究報告：2012/02/01(水) 01:15:30.41 ID:2eW/+tej
虚数の意味は前から言っているんだが
未だに数学会では遅れた考えを外国でもやっていて
未だ＊＊論には追い付いていない。これは人類の
知的衰退と思われる。我が新人類右脳同盟の啓蒙が
必要と思われる。長年の物質欲ボケがたたってると
思われる。身を引き締めよ。

>>497
確かに「専門分野としての集合論」では、ZFC に公理を加えたものばかりしか考えませんね。
仰る通り、たまにBGとかMKとか出てきますけど。
古典的な数学は殆ど展開できると言われている KP (kripke-Platek 集合論)や
圏論と関係が深い MacLane 集合論や Lawvere 集合論、
直観主義論理の数学は殆ど展開できると言われる CZF (Constructiv ZF)、
某所で話題沸騰中の Quine の NF (New Foundation)などなどの
「その他の集合論」は、集合論というより証明論で研究されているって印象。
「集合というものの性質を定める規約集」を志す人は、集合論じゃなくて証明論に行くべきだな。

>>490
スレチじゃないと思いますね。
Coqはバージョンによって多少違うようですが、
シンタックスはCIC（帰納的構成計算）という型言語で出来ています。
Coqは帰納的な定理から型理論の導出規則に基づいて、
自動的に新たな定理を作る機能があります、等号公理以外についても。
ttp://www3.di.uminho.pt/~jno/mfes/0809/SFV-CIC.pdf
の23ページ位からですね。

お、スレ主がお帰りになられたか

C.C. Chang , H. Jerome Keisler
Model Theory: Third Edition がDoverで出るか。

「駆け出し」って煽り文句が流行ってるようだな。

>>501
そうやって一階述語論理上の理論としての圏論は考えられるのは事実だけど、
そういうのがあまり出てこないのは別の理由からじゃないか？
圏論と型理論（高階算術ともいう）との間にかなり密接な関係があることは
かなり早い段階で分かっていた。
(Lambek & Scott の Introduction to Higher Order Categorical Logic など参照。)
型理論は、圏論云々よりはるか前からある「数学の基礎」候補だった。
だから圏論に合わせた一階述語理論をわざわざ作るまでもなく、
型理論を「圏論による基礎のための一階述語理論」として研究されてきたのだと
俺は理解しているがどうか。

いつものことながら圏論基礎ネタは盛り上がるのう
駆け出しから玄人まで一言いいたくなるテーマなんだろうな

>>514
というか、裸の王様のニオイがするからじゃないかな？

集合論は数学の基礎だと言い出したのは
HilbertじゃなくてBourbakiだと思うけど。
集合論はとても超越性の高い理論だから
Hilbertとかは、とても数学全体の基礎にはなりにくいという感覚をまだ持ってたんじゃないかな

>>516
集合論が数学の基礎だというのはまあ違和感はない。
述語論理上の最小限の言語だろう。
その点圏論はまったく違う。いろんな怪しげな概念を強制してくる。

圏論の概念が怪しげだと思うのは、メタな思考に慣れてないからでは？

>>517
圏論が各数学と一階述語論理と繋げるという意味で基礎となりうるかかどうかは既に技術的な問題になっている。
違和感があろうがなかろうがそういう主観的なものはもはや関係ない。
ま、流行るかどうかは主観的な問題も込みなので、知らんけどな。

>集合論が数学の基礎だというのはまあ違和感はない。
>述語論理上の最小限の言語だろう。
どういう意味で最小限と言っているの？
集合論より大きくない述語論理の言語は存在するのだから最小ではないと思うけど？

言語の大小なんて、公理の数を数えるのと同じでナンセンスだろ。
（二つの公理も連言で繋げば一つになるように）
ちょっとした小細工で本質的に変わらないのに大きくも小さくもできる。

>>518
メタなのはむしろ望ましいが、そのメタレベルの概念が怪しげに見えると言っている。
圏論の独自性（の一つ）は、まさにそういう理論の怪しさや不格好のようなことを見抜ける
ところにあるのかなと思っていたんだ。
>>519
言葉はちょっと違うが、流行るかどうかがやっぱり最も大事じゃないの？
技術的に詰めているものが望遠鏡なのか単なるガラスなのか

なんか「ユークリッド幾何は違和感はない、射影幾何は違和感がある」と同レベルに見えるんだよね。
確かに非ユークリッド幾何は、ユークリッド幾何ほどは流行らない。
しかし非ユークリッド幾何には非ユークリッド幾何にしかない意義がある。
両者の比較や、目的による使い分けなどをすることによる相乗効果で幾何学がより深化することになった。
集合論による数学の基礎と圏論による数学の基礎も同じではないのかな？
両方あることで、数学の形式化の理解を深化させてくれる。

優等生の模範解答ですな

射影幾何は非ユークリッド幾何ではないけどね

>>523
紳士的な議論だが、
集合論もあるけどこれもある。流行らないかもしれないが、あったらあったで
いいじゃないか、なんていう圏論は嫌でしょ。
>>520
∈だけ追加だよね？たしか
極小といえばよかったかな
>>521
そんなことはない

>...なんていう圏論は嫌でしょ。
いや、君が嫌ならそれでいいんじゃない？
でも他人に嫌がるように強制できないことも分かるでしょ。
つーか、議論のレベルを女子高生みたいな好き嫌いレベルまで落とすんなら
っこでは誰も君との議論に付き合わなくなると思うけどね。

＞>>521
＞そんなことはない
それだけだと>>527で批判されている「嫌でしょ」と同じく全く説得力ないんだが？
どう「そんなことはない」のか説明してくれないと反論のしようがない。

どんな言語でも、述語記号・関数記号・定数記号が全部有限なら、
小細工することで極小な言語にすることが出来ますね。
公理が極小というのが無意味なのと一緒。最小は勿論無理ですが。

>>509
情報ありがとうございます。参考になりました。他にもなにか文献等
ご紹介いただけないでしょうか。

何を言っているのかさっぱり分かんない…
ちょっと気まぐれで覗いてみたが、まるで地獄だ…

>>522
>流行るかどうかがやっぱり最も大事じゃないの？
そもそも基礎論自体が流行っていないｗｗ
集合論が圏論より流行ってると言っても団栗の背比べｗｗｗ

>>527
へたに柔らかく言い過ぎたか？
そんな圏論ならそんなふうにニッチにやっていけばいい。
だが圏論にはもっと大きな意味があると聞こえているので、もしそうなら衆人にそれが分かるように
言ってくれと言った。
>>528
だって公理の数の件は数えるものが悪いだけだね？
それくらいあなたにも分かっているだろと思うから。
>>529
528とも同じくいまは本質的なことじゃないと思うのでごめん。

>>530
ttp://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.32.5387&rep=rep1&type=pdf
私に探せるものであなたに探せないものはない。

＞圏論にはもっと大きな意味があると聞こえているので
こういう誤解をする人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場

http://www.springerlink.com/content/j971335218m52258/
>>530
申し訳ないが読んだことがない本で・・・。

>>533
>そんな圏論ならそんなふうにニッチにやっていけばいい。
そんなふうがニッチと思うかどうかは結局主観の問題だからね。
「集合論の問題はニッチなものだけじゃない」と何人かの専門家が解説しているのを見てきたけど、
ほとんどの部外者には「なんだ、やっぱりニッチな話じゃん」としか思わないだろうし。
ニッチかどうかなんてそんなもんよ。

>535　これは必ずしも誤解ではなく、たしかに昔からよく耳にするな

>>537
客観性のない主観的な罵り言葉なんて、負け惜しみの捨て台詞なんだから生暖かくスルーしてやればよろし。

>>538
「もっと大きな意味」とか曖昧な言葉を含んでいるものに
「誤解ではなく」とか断言できる神経が全く理解できないな。

>>540
まさか圏論の近くにはこんな人が多いんじゃないだろなｗ

低俗な煽り合いはもう終了でいい？
もっと生産的な話がしたくてさっきから待ってるんだけど。

>>513
圏論に対応させる形式体系として型理論の方がよく出てくるのは確かにそおの通り。
だけど、圏論をそのまま一階述語論理にのっける公理系も Lwavere を始め研究されている。
最近でも以下のような論文が出ている。最近つっても10年以上前だけど。

http://www.cwru.edu/artsci/phil/AxiomatizingCategoryCategories.pdf

>538,541
そこまで言うのなら「よく耳にする」で済ませないで、
出典を明らかにするなりリンク貼るなりすれば？
そうすれば「低俗な煽り合い」と言われないで済むと思うけど。

>>529
A∧BよりAの方が短い、という意味では公理系の極小性は定義できない？
もちろん、Aと全然違うCとどちらが小さいとも言えないから
集合論と圏論の比較には役に立たないだろうけどさ。

>>526,>>533
数学の基礎付け・形式化に、集合論は必須のものなのか、
それとも別の方法も可能だけど歴史的経緯や使いやすさで集合論が選ばれているだけなのか、
という問題は重要な問題だと思う。
だから「集合論もあるけどこれもある」っていう圏論の研究は意味があるし、全くニッチな研究だとは思わない。
数学の基礎付け・形式化そのものがニッチだという人には「興味が違うのね」としか言えないけど。

哲オタ乙。研究にどんな意味があるかどうかなんて言い方次第って実例だなｗ

538が言っているのは
「独立した個を重視する西洋近代の終焉が...、これからは関係性を重視した圏論が...」
っていうポモな人たち（いや本当にポモなのかも知らないけど）の発言なんじゃない？
そんなのに踊らされてるなんて...

>>544
＞数学の基礎付け・形式化に、集合論は必須のものなのか、
＞それとも別の方法も可能だけど歴史的経緯や使いやすさで集合論が選ばれているだけなのか
その大事な大事な研究の結果、どっちだと分かったの？少なくとも結論には興味ある。

>>548
横レスかもしらんが、型理論型理論と言ってるように、
型理論で形式化できるものは圏論を使って形式化できる。
「通常の数学」はこの範囲。しかし「通常ではない数学」が問題。
集合論でも圏論が形式化できるかが色々微妙なように、
逆に圏論での形式化では集合論的な数学が問題になる。
特に置換公理が型理論（よって圏論）とは相性が悪いので、
このスレか関連スレでも何度か話題になっているように
置換公理を使った数学（要するに集合論的な数学）をどう評価するべきかという問題になる。

集合論派は「群全体のなす圏、環全体のなす圏などは集合論で記述できないがそんなのは数学の中でごく例外的」と言い、
圏論派は「置換公理を使うような数学は圏論では記述できないがそんなのは数学の中でごく例外的」と言うわけですね。
お互い自分に都合がいいように「数学」というものを設定していると。

>>531
何が地獄なの？？

>>550
そうやって党派的な図式にするのは楽しいのだろうが
>>549は「どう評価するべきかという問題になる」と至って中立的なことしか言っていないぞ

どんな定理に置換公理が必要化はこのスレの上のほうで話題になっていたけど、
そういう背景があったわけね。

亀レスだが>>532が絶妙に本質を突いている件

>>549
型理論に埋め込めるCZFは置換公理を含むんだが？

>>551
文系の俺には全くついていけない別世界、とでも言うかな…

集合論と圏論って、互いに直交していたりしないの？

なんだよ直交って

>>557
そりゃ点（要素）対　矢（射）に象徴されるように直交してるさ。
だがこのスレの大勢的論調では、２つはx軸メインかy軸メインかくらいの
違いしかないらしいんでがっかりしたところだ。
>>558
話が遅いな。少しは推察してやれよ。

>>559
そんじゃおまえがその「直交している」ことの偉大な意義を解説してくれや

トンデモ出現のようだな。基礎論スレの恒例行事。

直交しているという表現を使う>>557は多分プログラマの人なんだろ。
処理系作っていた人がそんな表現使ってた。独立しているぐらいの意味だったはず。
プログラマの人は勝手に変な言葉をあやふやに定義して、形式的に定義された言葉で
みんな知っている、という意味不明な前提を持ち出すから話が成立しない。

>562
そうそう、そんな感じ。
関数空間の基底みたいな話がメタ数学にもあったりしないのかな、と思って。

538=559って要するに、
どこかの哲オタの話を真に受けてゲーデルの不完全性定理には深遠な意味があると勝手に期待したものの、
専門家一同の「ハァ？」を買ってしまって逆ギレ、
という構図だね。

>>563
関数空間に、内積を定義しておかないと、直交も何もないってことは理解できてる？

>>557は
直交しているという言葉にきちんとした意味があるのが
前提になっている書き方だろ

せめて「直交しているみたいな概念がメタ数学にも無いのかな」と言わないと
意味分からん

>565
そういわれてみればそうだね。
プログラムコードなら位相を入れられるけど、集合論と圏論といった概念だとムリなのかなぁ。

>>564
不完全性定理以外にそういうネタがあるってのは新たな発見だったｗ

>>562
＞プログラマの人は勝手に変な言葉をあやふやに定義して、形式的に定義された言葉で
＞みんな知っている、という意味不明な前提を持ち出すから話が成立しない。

変な言葉といえば、ポインタで使われる「指す」という用語の
明示的な定義を未だに見たことが無い。

int a = 0;
int *p = &a;

この場合、「pはaを指す」のか「pはaのアドレスを指す」のか？

ネットを徘徊すると、どっちの使われ方も見かける。
だが、前者の方がより多く使われているように見える。
また、経験上、前者の方がより "正しい" ように思える。
しかし、結局のところ、「指す」の明示的な定義は知らない。

一方で、「代入する」という用語には明示的な定義が用意されていることが多い。
この差は何なのか？

>>569
アドレスを指すというのはもともとは誤用であろう（意味は伝わるが）
アドレスそのものはどこにも無いので指せない。（アドレスが示すメモリはある）
ポインタが指すのはメモリであってアドレスではない。

しかしアドレスというのは住所である。
住所は、実際には土地（場所）を指しているのだが
その土地を住所で代表し、「住所」宛の手紙と言うのと同じ。

つまり、「aを指す」と「aのアドレスを指す」は同じ意味であり
どちらが正しいというものではない。

そもそも 「指す」てのはスラングだわな、だから定義なんかされてない
ポインタがアドレスを保持することを「指す」と言ってるだけで
cそのものの動作に「指す」なんてないわな。

>>570
＞ポインタが指すのはメモリであってアドレスではない。
ところがどっこい、どこかのポインタスレにおいて、

「ポインタが指すのはメモリではなくオブジェクトである。これが分からん奴は半人前だ(ｷﾘｯ」

などと主張する輩がいた。あなたとは正反対の主張だ。
また、>>571によれば「ただのスラング」だそうだ。
これは、あなたの主張とも上記の輩とも違う主張だ。


やはり「指す」は変な用語である。人によって全く見解が違う。
プログラミング業界は、なぜ、「代入する」のように明示的な定義を
早い段階で用意しておかなかったのか？この差は何なのか？
仮に「スラング」が正しいにしても、それならそれで

「指すという用語はスラングである」

という "明示的な定義" が必要である。しかし、このような
定義は広く一般に普及しているとは言い難い。

連投失礼。ちょっと訂正する。

× などと主張する輩がいた。あなたとは正反対の主張だ。
○ などと主張する輩がいた。あなたとは異なる主張だ。

世の中にはソフトリンクもハードリンクもあるのだが

>>572
そういうのを人の褌で相撲を取る、というのだ。
誰かの主張を引用するのなら引用元を明示するべきだろう、
でなければ本当にそういう主張がなされたのか、単なる君の誤解なのか確認するすべがない。
そもそも他人の主張を根拠に何かを批判するのならば、
自分もその主張に賛同する旨を明言するべき。
さもなくば、相手が反論しても「それ、俺の主張じゃないし」と言うのと同じ。
学問的な議論をする際の最低限のルールすら身につけていなかったようだから、
以後気をつけるよーに！

>>572
オブジェクトを指すってのはまたずいぶん抽象的な話だな。
オブジェクトはメモリにのっている。なにも異なる主張ではない。
でなけりゃ void * は何を指しているんだ？ 
そして「指す」はスラングだと言うのにも矛盾しない。

＞ 「指すという用語はスラングである」 
＞ という "明示的な定義" が必要である。

なんで？ そんなもんいらんだろ。
「指す」という語は日本語であるという明示的な定義がなくても
みなが問題なく使用しているように。

>>555
その埋め込みは排中律に適用できない。
つまり直観主義論理でないと成り立たない。
「通常の数学」が排中律を使っていないというのなら、
それに加えて置換公理も含めて圏論で扱える、ということ。

圏論による基礎に関して誰かまとめて下さいませんか？
ぱっと見ただけでも色々な流儀（？）があって、私なりにまとめると以下の通りですが
互いの関係がよく分かりません。

・「集合論が数学の基礎」というのと「基礎」の意味は同じなのか異なるのか、
・述語論理と数学を繋ぐのかそうではないのか、
・型理論と「圏論をそのまま一階述語論理にのっける公理系」、
・古典論理を採用して置換公理がないのと、直観主義論理で置換公理があるもの

ただの言葉遊び

>>557-568 >>569-576
しょうもない話だな

>>579
プログラムってのは言葉だからな、日常では「言葉遊び」と軽んずるようなことが、
致命的な問題を起こすことがあるのよ。値呼出しと名前呼出しの違いとかな。
もっとも、嘘つきの逆理とかラッセルの逆理とかだって、日常では「言葉遊び」と軽んじられる。
プログラムと違って現実に問題になることもない、本当のお遊びｗ

>>578
HANDBOOK OF PHILOSOPHICAL LOGICの12巻に大体載ってる。

>HANDBOOK OF PHILOSOPHICAL LOGICの12巻に大体載ってる
どなたか要点だけでも書いていただけないでしょうか？この本がすぐ見えないので
特に、型理論と「圏論をそのまま一階述語論理にのっける公理系」をなぜ考えるのか
ということだけでもいいのですが。

>>534,536
レス遅れてすみません。すばらしい文献を紹介していただいて感謝しております。
夢中で読んでました。勘違いも見つかったり、まあ、とりあえず自分の疑問を治めることが
できました。ただ、ショックなのは、以前ネットをあさって集めた文書の中に、紹介いた
だいた文献が、既にあったことです。なんとも愚かですなあ。

とにかく感謝感激です。ありがとうございました。

>>582
目次見た感じ、圏論っぽい話はないけど、本当にその巻に書いてある？

>>583
Categorical Logicについて勉強したいならばBart Jacobsの大作"Categorical Logic and Type Theory"を読めばいいんじゃないの？
今はペーパバック版が出て安く買えるようになってるはずだし

>>583
以前こんな書き込みがありました。

623 ：１３２人目の素数さん：2011/11/23(水) 15:34:26.24

＞哲学ではうん十年前から圏論（カテゴリー論）を扱っており、これと数学基礎論を関連付けせず語るのは片手落ちだ。

哲学（論理学？）と圏論の関係って
証明図の代わりにダイアグラムで書こうってもの。
そのために高階直観主義論理⇔トポス
の対応を考えているだけ。
初等トポス⇔ハイティングモデル
選択公理付きトポス⇔ブールモデル
グロタンディークトポス⇔一階無限論理
また逆にトポスを与えたら
Mitchel Benabou Languageという言語がつくれる。
上のような圏論的解釈の完全性定理に該当するものも証明されている。
そして圏論が数学の基礎となるのは初等トポスに自然数、
1→N→N
｜　｜　｜
｜　↓　↓
└→X→X
を加えて1→0をとったものが集合論に該当しますというだけのことだろう。

656 ：446：2011/11/26(土) 10:57:45.95
いや、なんでもできるわけではない。
例えばベクトル空間の圏は、cartesian closed にならない。
cartesian closed categoryの上位にmonoidal categoryがある。
cartesian closed は任意オブジェクトA,Bに対して
AｘB→A
↓
B
さらにB^AｘA→Bのユニーク性、また→1をもつもので、
B^AってのはAからBへの射だから、
a→b∧aならばbっていう三段論法が出てくるのすぐわかる、
これでハイティング代数がcartesian closed になることがわかる。
ハイティング代数⇔直観主義論理。選択公理入れれば古典論理完成。
さらにB^AｘA→Bのユニーク性はλ計算の関数適応にも対応。
関数のカリー化からきた考えだから当たり前だけど。
トポスは集合論を解釈する具体的な真偽値を与えるために
subobject classier（これは大抵真と偽の2元集合）を導入したもの。
函手の表現可能性⇔ universal elementの存在なので、
トポスに出てくるΩってのはこれのこと。
例えば集合の圏Setの簡単な例。
2＝{0,1}、Fは函手、集合S'⊆Sのとき、
F(x)＝1(x∊S')
F(x)＝0(¬x∊S')
これがトポスだと以下のようになる...。
S'⇒S
↓　↓F
1→2(subobject classier)

>>586 >>587 >>588
レスありがとう。今読ませてもらっています。
Jacobsはちょっと高いのでどうしようか．．．

＜コメ作付け制限＞新基準に福島１１市町村が否定的　福島県の１１年産米
緊急調査で放射性セシウムが４月適用予定の新基準値（１キロ当たり１００
ベクレル）を超えた地区があった１２市町村のうち、１１市町村が「１００
ベクレル超５００ベクレル以下」の地区での今春の作付け制限に否定的なこ
とが毎日新聞の取材で分かった。うち４市町は現行の暫定規制値（同５００
ベクレル）を超えた地区でも作付けを認めてほしいとした。農林水産省は自
治体の意向を踏まえた上で２月中にも作付け制限計画をまとめる方針だが、
調整は難航しそうだ。(毎日新聞)

>を加えて1→0をとったものが集合論に該当します
「とった」ってどういう意味だろう？
「公理から取り除く」という意味だとすると、トポスの公理に1→0なんてないし。
「公理として付け加える」という意味だと、1点集合から空集合に射があったら矛盾するし。
同じ言葉が正反対の意味に解釈できるって日本語難しい。

>>589
圏論的論理学のテキストが無料公開されているのを忘れてました。
http://www.cs.unibo.it/~asperti/PAPERS/book.pdf

ところで以下は型理論学習のための大雑把な予備知識ですが・・・。
λ計算は関数の抽象にλ記号を使った型システムとなります。
型なしλ計算は単一の型を持つシステムとして、やはり型システムに組み込まれます。
究極の型理論として強正規化不能（停止しない式変形がある程度のイメージ、
ただし決定不可能性とは別）ないくつかの型システムがあり、
このシステムの循環する型や、不動点コンビネータを制限することで、
断片としてλ-Cubeと呼ばれる8つの単純型システムからなる構造が得られます。
このCubeのある辺を切り取ると、ゲーデルのDialectica解釈内でのSystem T
（自然数論の無矛盾性証明に導入されました。）が抽出され、
またある辺からはGirardのSystem FやF_ωが抽出され、
CoqやLFなどの自動推論器の原型なども取り出せます。
またCubeのある面は命題論理に、反対側の面は述語論理に対応しています。
こうして取り出された様々な型システムはカリー＝ハワード同型対応によって、
通常の様々な数理論理学の証明規則に各々対応しています。
一方型システムは公理的集合論などの数学の基礎の代替ともなり、
ZFやZFCなどの代わりにQuineのNFやPotterのZU/ZFU、AndrewsのQ_0などが考案されました。
また論理はLTT（通常の論理）とLPT（真偽値を持たない命題を作れる）に分類され、
例えばLPTであるBessonのPT_ω（AczelのFrege構造の形式化）によると、
循環によるパラドクスR∈R<-->~R∈Rの構成さえも許してしまう型システム系の数学が作れます。

>>583
とりあえず>>513の言及している本と>>542のリンク先をそれぞれ見てみたらどうでしょう？

毎度です。>557と関係のあるような関係の無いような話ですが、
CNFに距離空間を突っ込んでHornCNF!=CNFにチャレンジしてみました。
＃数理論理学というよりも計算複雑性の話ですね。

どこか間違っているような気がするのですが、素人なので追いきれず……
どなたかコメント頂けませんでしょうか？

まとめた資料はttp://arxiv.org/e-print/1202.1194にあります。
.tar.gzを付ける必要があるみたいです。

突っ込まなかったけど、>>567について言っておくと、
位相を入れたからって直交は定義できないんですけど。
内積から位相は決まるが、位相から内積は決まらない。
区別は出来ている？

>595
大丈夫です。区別できています。
>567はベクトル空間の間違いですね。

73 ：１３２人目の素数さん：2012/02/09(木) 21:15:32.88
決定性公理 AD って二階算術の命題として定式化出来ますか？
定式化出来るとして、 ADの否定は
ATR0やΠ11-CA0などの体系で証明できますか？

なぜADはATR0やΠ11-CA0などの体系で証明できますか？ではなく
ADの否定は証明できますか、なのだろうか。

選択公理と矛盾する公理じゃなかったっけ

二階算術で定式化できる範囲では選択公理と矛盾しないし（ただし consistency strength は巨大基数レベル）。
つーか、二階算術で定式化できる選択公理もかなり狭い範囲でADと矛盾しないし。

巨大基数レベルってのは巨大基数の帰納的類似物であるような可算順序数レベルってこと？

もちょっと易しい話題にしてくれんかな？

再帰型Tから、T_rectを作るアルゴリズムがご紹介いただいた文献>>534,536 でわかり、
大変感激している最中です。∧、∨、＝や∃までもが再帰型で定義できるというのは
すごい。しかもその定義から作られるT_rectがまさに論理にぴったりとあてはまるのは
不思議としか言いようがない。さて、「再帰型Tから、T_rectを作るアルゴリズム」
というのは、もしかして天下り的に受け取るしかしょうがないのかもしれませんが、
もう少し「再帰型Tから、T_rectを作るアルゴリズム」を深く理解できるような解説
がしてある文献を紹介していただけないでしょうか。あわよくば、「再帰型Tから、
T_rectを作るアルゴリズム」が、当たり前のように思えるようになるといいのですが。

とりあえず今は、圏を知らなければならない気がして予習してます。
どうか偉い方、神様、よろしくお願いします。

http://ci.nii.ac.jp/nrid/1000080216994
有名なので既知かもしれませんが
滝田氏の型理論１〜４のPDFを参照してください。
Lofの構成的型理論やλ-CubeやL-Cubeの話題まで一通り解説があります。
私はこのPDFで、論理が型理論に埋め込まれる理由が大分理解できました。

※以下、私的メモでレスとは※
http://www.shayashi.jp/freePXbook.pdf
LET-quantifier　condition formula

下記の本に様々な非古典論理を紹介してあるようなのですが、それぞれの意味論についても解説されているのでしょうか？

Priest "An Introduction to Non-Classical Logic: From If to Is"

amazonのなかみ検索とか使うと良いよ。

>>606
盲点でした。ありがとうございます。

スレタイスレ446＝林晋氏、という理解でおk?

それはあなたの妄想
さすがに林さんはPRAの証明能力について初歩的勘違いはしないと思う
ロジックもいろいろ分野があるから畑違いなら勘違いしても良いんだが
林さんはそうじゃない

林晋さんは結構あちこちに出没してそう
アマゾンでも他人のゲーデル本を批判してたよ

あの人はそういうビョーキだから
他人のゲーデル本を批判して一生を終えるんだろう

そんな批判的な事は書いてなかったような
普通の好意的な書評だと思ったけど。
どの本の事？

>PRAの証明能力について初歩的勘違いはしないと思う
どこで勘違いしてた？哲学板の方？

http://uni.2ch.net/test/read.cgi/math/1319895756/601

>>611
それは別の人でしょw

>612
林晋さんはアマゾンで吉永良正さんの本を批判している
数学ガールは誉めてるけど自分の本を一般人にレビューされて噛み付いてる

林さんくらいの書き方なら仕方ないんじゃないかな

数学ガールを批判している人がいないのが逆に怖いんだが。

数学ガールって読む価値ある？
最短経路の本ぐらいの出来だったら読んでみようかと思うけど。

確かに吉永の本は初学者向けにしても細かな間違いが多かったが
そんなに目くじらをたてるほどのもんでもないな

ブルーバックスなんざ雰囲気だけ味わえればいいんだよ

もう一度あの頃のブルースクリーン（BSoD）の雰囲気を味わいたい

啓蒙書では厳密でなくていいけど間違いは許さないってのは、考え方として悪くない。
少なくとも大学教授ならその程度の基準は満たすべき。

>>620
いや、完全性定理の意味での「完全性」と不完全性定理の意味での「完全性」とをごっちゃにするのは
素人向けの啓蒙書と言えども完全にNGでしょ。根本的間違いなんだから。
そんな根本的な間違いのある本は素人にとっても読まない方が遥かに良い。
数学だと根本的な間違いの恐ろしさは分かりにくいけど、物理だったらトンデモ本とされる間違いですよ。

高橋昌一郎のゲーデル本もひどいよね
ああいうのを読んで一般の人がわかったとか言ってるのはかわいそう

関係ないけど、昔たまたまネットサーフィンしてたら、
女子高生がドラッガーを読んだら云々とかいう本の著者が、
数学ガール不完全性定理のアドヴァイザーでも有名な
アメリカの某日系集合論研究者にブログで論争しかけられていた。
これも女子ドラの著者がゲーデルエッシャー何とかとかいう本に騙されたのが原因。
ゲーデル本の著者は自著の内容に責任をもつべき。

>>625
そのアドバイザーって誰？

くるるゲーデル

高橋昌一郎の名前が出た途端に関係ない話題が書き込まれるのは何故

「理性の限界」を読んだけど、どう読んでも不完全性定理の説明はおかしいと思った。
ネットの書評ではほとんど間違いの指摘がされてないのは不思議だね。

> 少なくとも大学教授ならその程度の基準は満たすべき。

って書いた俺が言うのも何だけど、現代哲学系の人は仕方ない。
そんな本、真に受けないくらいのリテラシーは必要。
こういうスレ読む人間が読む本じゃない。

>629
探すと酷評もあるよ
”高橋昌一郎　バカ”でぐぐれ

数学ガールへの批判ってないの？

>>632
ミルカさんが偉そうでウザかわいい

>>633
誉めてんじゃねーよ

　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_
　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、
　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ
　　　　　/　　　／:::::／　　　　　　　　　　　＼
　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 |
　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 |
　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ|
　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　
　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。
.　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。
　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。
　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて
　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。
　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は?
　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？
　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼
.　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼
　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 |
　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､
　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣|
　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/

あー、くるるさんね。最近二重におめでたいらしいな。

いいよなー
嫁さん怖そうだけど

>>632
人を椅子ごと蹴り倒してはいけない。

嫁さん怖そうなのは照れ隠しなのでは？
なんだかんだ言って仲良く暮らしているようだし。

Hさんて林晋先生？

888 名前：考える名無しさん 投稿日：2012/02/19(日) 19:55:29.41 0
高橋の『理性の限界』
は計算機科学者で数学史家のＨさんにコキおろされてたような…
啓蒙書だからこそ、きちんと専門家が書いた本を選ぶべきと思う

>>627
見てる限りでは、あの人数学の見識かなり狭い。

狭くても深ければいいんじゃないの？
重要なのは掘った容積だから狭い分は深さでカバーできるさ。

>>537の
＞「集合論の問題はニッチなものだけじゃない」と何人かの専門家が解説している
にその人も含まれているわけですね。

上の方で不完全性定理の証明を鶏でやろうとしていたものだけど
http://r6.ca/Goedel/Goedel20050512.tar.gz
まったくもって途方もない作業。
これを見れば高橋氏が不完全性定理を誤解するのも頷けよう。

細い穴ほど崩落しやすいわけだが

>>642
見当違いなところを深くほってもダメ

>>645
同意

掘った穴に閉じこもっていなさい

集合論って、なんか具体性の無いあの世の話をしている感覚なんだよね。
代数幾何学みたいに目に見える具体的な問題を対象にしていない。

不完全性定理ってそんなにすごいもんなのか
あの証明を思い付いたのはすごいけど
フォローするだけなら大したことないじゃん

理系崩れや文系上がりの科学哲学者や科学史学者
そういうのが一般人相手にすごいすごいって布教して回ってるだけじゃん
本書けばそこそこ売れるから

きっちり追うと意外と骨折れるよ。
第二の方は端折った証明しかこの世に存在しないし。

代数幾何のやってることが目に見えるって648は天才のようだな。
もしかして次のフィールズ賞候補者？

>>651
途中の手法は抽象度高いけど、目的とする問題は
具体的で目に見えるでしょ？小学生にすら伝えられるものも多い。

ロッサーの不完全性定理について

>>651
森重文氏のフィールズ賞の理由となった業績の目的とする問題を
小学生に分かるように解説してくれ。

また極端なｗ

>>601
二階算術で記述可能な決定性は射影決定性(PD)まで。
ZF+DC+PD は ZFC + Woodin 基数無限個と無矛盾等価。
逆に二階算術で記述可能な選択公理はすべてDCのfragmentなので、
ZFC + Woodin 基数無限個が無矛盾ならば ZF+DC+AD も無矛盾、
よって ZF + AD + 二階算術の選択公理も無矛盾。

ZFC+PD が ZFC + Woodin 基数無限個と無矛盾等価の間違いではなくて？

┌∩┐(◣_◢)┌∩┐
集合論の内部で論理体系や計算機を展開するか、
構成的型理論や計算機の内部に数学を構築するか、
それが問題だ。

また恥の上塗り野郎が現れたか

┌∩┐(◣_◢)┌∩┐
上に書き込みにあるように
鶏のようなlofさんの型理論の断片の中で数学も論理も動きます＾＾；
もち実数論も巨大基数でも遊べます。
logさんの理論はλ-Cubeの中に埋め込まれ、
λ-CubeはHyper-λ-Cubeの中に埋め込まれます。
Hyper-λ-Cubeは型理論に総括され、
バベルの図書館に保管されています。
これが世界の実体です。

面白すぎ　スルーできねーwww

┌∩┐(◣_◢)┌∩┐
Fuck Off！！
な〜んもわかっちょらん。
λ-Cubeはカリーハワード対応でL-Cubeとかいう
論理学のサイコロと同値になる。
一方CL対応でSKI-Cubeとサイコロ同値になるんやで。
つまり神はサイコロ振ってこの世界を創ったわけなんや。
ほぉ〜Yeah、Fuck、Fuck、Fuckin、Baby!!

>>645,>>646
断面積の大きい隧道ほど技術的に難しいのは土木のジョーシキ。
山の高さは裾野の広さで決まる、っていうのなら賛成だが、穴では比喩にならん。

ロッサーの不完全性定理と来れば次はクライゼルの注意。

無矛盾性を違う方法で定義すれば、
Con' Tが証明できるとかいうけど、
そういう方法はφが既に証明されていれば
¬φは証明しないことにする、みたいな感じで
例外なく体系の整合性の問題を迂回して
全然違うところから「無矛盾性」を導いてるよね

数学ガールはクライゼルの注意にはメンションしているの？

ウォリーウィズ数学ガールならリードしちゃいなよ。

意味不明なカタカナ語使うなよ

ユーザー、憂鬱、イニシアチブ。

今まで見た中で一番奇妙な言語は
WhiteSpaceだな。
バイナリ列のまんま。
タブとスペースのクリーネスター

┌∩┐(◣_◢)┌∩┐
Fuckin Baby?
Babyloon!
Prover9は停止しないし
Coqは人に劣るし、
俺のブレインがナンバーワン
Oh!Brack"!

巨大基数と不完全性定理って何か関係あるの？

「俺のブレイン」は必ず停止するのか？

停止コード発行する機能のところが微妙にバグっておられる
ようにみうけられますなあ

┌∩┐(◣_◢)┌∩┐
Hey!Fuckin!!
俺のブレインは常に停止してるよcomin!
TrururururuYeah!
型理論、これ世界の謎解く道の概念
◎珍レーフも論理記号の謎解くために
構成的型理論つくったBabyぉおｎ！！FuckinMyBabｙ
SuckSuckSuckMineふぉおおおおYahhhhh!!!
暗いぜるの注意の謎も解けるYO！いけるYO!!
WhiteSpaceも形式化できるYO!いけるYO!!
MultiFucinAllOfTheWorld！！Laier!!!!

　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_
　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、
　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ
　　　　　/　　　／:::::／　　　　　　　　　　　＼
　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 |
　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 |
　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ|
　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　
　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。
.　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。
　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。
　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて
　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。
　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は?
　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？
　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼
.　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼
　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 |
　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､
　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣|
　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/

数日前にAPALから出たPalmgrenの論文で、
「圏論をそのまま一階述語論理にのっける公理系」に関して言及があるね。

http://www.sciencedirect.com/science/article/pii/S0168007212000309

┌∩┐(◣_◢)┌∩┐
Yes...Yes..Yes.YesYeYe,GoodMaaaaaaaaannn!!!!!!
圏論のせたら五分で数学！
Rally,Fuckin！
Rally,Fuckin！
Fuckin IN IN!！
Lawvareがのせたら五年で主流！
Rally,Fuckin！
Rally,Fuckin！
Fuckin IN IN!！
Coooooooool！！！！！
け・ん・ろ・ん〜〜〜〜〜〜！！！
Scarish!!!!!!!!

Erik Palmgren
いいんですけどできれば即pdfで読めるものがありませんか？
書誌をGccgっても有料なのばっかしで（汗）

これならどうだい？著者のページをぐぐればすぐに見つけられるよ。
http://arxiv.org/abs/1201.6272

なんじゃそら

「圏論をそのまま一階述語論理にのっけ」たら何がおいしいの？
無知でスマンが教えてくれ。

>>680
感謝します　Gccgり方が足らなくて恥ずかしい
>>682
何がおいしいのか現物確認しようと・・・
ちなみに興味あったのは
(i)::カテゴリー論界隈ではまだ順序対の規定を「インチキ」しておられるのか？
(ii)::一階述語論理はゲンツェン方式のまんまか？
（個体定数が可算個を超えるのはどうも納得いかんのです（汗））
嗤ってやってください　これで萌える性格ですので
外史竹内の時代からの数理ヲタクなのですよお

Aの上にBのっけると、
BではunusualなAのtoolでBをhack出来るのが魅力。飛び道具的威力を発揮することがある。
不完全性定理は数論の上に証明論のせたとみなすことも可能。実際には自己言及的だが。

>>683
>(i)::カテゴリー論界隈ではまだ順序対の規定を「インチキ」しておられるのか？
インチキってどういうことですか？
>個体定数が可算個を超えるのはどうも納得いかんのです
これはどういうこだわり？

>>684
ありがとう。
圏論をhackか。いいな。
・証明論を数論にのせる
これは分かるが、
・圏論を述語論理にのせる
これは、元々のっていたじゃないか、と思っちゃうので分からん

>>685
直積のダイアグラムではAxB＝BxAにしかならん気がします
「濃度が同じだし同じobjectとみなす」でかまわない？
巾のダイアグラムから直積を"C のop"で導くのは見たことないし
あ　それから　[個体定数x　個体記号○]でした
可算個を超えると「有限でない長さの記号列のセンテンスやフォーミュラ」
まで考えんと話にギャップができませんか？
素人の単なる勘違いでせうか
いろいろ説明不足で申し訳ない

　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_
　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、
　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ
　　　　　/　　　／:::::／　　　　　　　　　　　＼
　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 |
　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 |
　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ|
　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　
　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。
.　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。
　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。
　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて
　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。
　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は?
　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？
　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼
.　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼
　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 |
　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､
　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣|
　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/

話半分で圏論はどうとか言わずに
ちゃんと勉強してから発言しなさいよ

┌∩┐(◣_◢)┌∩┐
http://www.journalarchive.jst.go.jp//jnlpdf.php?cdjournal=sugaku1947&cdvol=35&noissue=1&startpage=50&lang=ja&from=jnlabstract
たまには俺も役立つFackin!!!

懐かしい！
月刊マセマティクス（1980.2.1）だあ

┌∩┐(◣_◢)┌∩┐
高齢者
バカ乙筆記―
トンデモ中〜
ふひ
FucingAnarkingThanksBoolan！！Fukinkin!!!

MIKAMIのインターネット　　　でググれ


このブログ痛すぎｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗ
ｸｿﾜﾗﾀｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗ

>>679
その著者のいうpredicativeなtoposというのは一体どういうもの？

>>694
?ttp://igitur-archive.library.uu.nl/dissertations/2006-0522-200026/full.pdf
たぶんこのことだと・・・

Mendelson "Introduction to Mathematical Logic" のスコーレム標準形の話でわからないことがあります。
定数と関数記号を持たない述語論理の論理式は、どの∃も、どの∀より左にある冠頭標準形（スコーレム標準形）を持つ。
という定理（PROPOSITION 2.31）なのですが、「定数と関数記号を持たない」という条件はどこで使われているのでしょうか？

┌∩┐(◣_◢)┌∩┐
Fuck!
純粋述語計算（定数・関数記号を持たない述語計算）でも
充分にSNFが実現できるって話やろ？Yahhhhh!
Bud Luck,men！！

　お前たちは、定職に就くのが先決だろがああああああ！！！！！！

　ニート・無職の、ゴミ・クズ・カスのクソガキどもがあああああ！！！！！！

スコーレム関数の関数記号を導入するのだから、
標準形は関数記号なしの言語の論理式ではないだろ

┌∩┐(◣_◢)┌∩┐
Auti!!!
ｗ(((●ｍ◎；)))ｗ~~~
OhMyFuck!!!!!
つまるところ、
・「定数と関数記号を持たない述語論理」の論理式
ではなく、
・定数と関数記号を持たない「述語論理の論理式」
がTruthってPoemかFacki'n！！！！
アッシェ〜〜〜〜〜〜〜〜〜〜〜ム！！
くるっくるっくるっ、CokeKokkoooooooooooooo!!!!!!!!

Mendelsonを手元に持ってる人じゃないと分からんなあ
結果自体は定数記号や函数記号があっても成り立つから、
簡略化のためか、または、証明がその条件に依存しているかだと思う。

Mendelsonのはスコーレム関数ではなく述語を使っていますね。
変数がすべて束縛された論理式をPNFに変形して、
これを新しい述語で置き換え、新しい束縛変数を追加して
∀を右にどんどん追いやってSNFにしています。
定数と関数は証明に必要ないので省いただけだと思いますね。

最近、スレが盛り上がらんな。
ロジックでいまホットな話題ってないの？

>>703
ホットな話題があったらもう盛り上がってるさｗ

>>703
ゲーデルでおわってるんだろ

>>703
数理論理学分野のトップジャーナルと言われる Annals of Pure and Applied Logic の
most cited articles のランキングがある：

http://www.journals.elsevier.com/annals-of-pure-and-applied-logic/most-cited-articles/

これを見ると、トップ10はすべて非古典論理っぽいな。
11位にやっとモデル理論の論文が現れる。
それ以下でも非古典論理の論文が大部分のようだ。

　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_
　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、
　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ
　　　　　/　　　／:::::／　　　　　　　　　　　＼
　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 |
　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 |
　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ|
　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　
　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。
.　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。
　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。
　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて
　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。
　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は?
　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？
　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼
.　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼
　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 |
　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､
　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣|
　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/

>>706
非古典論理の中でもファジー論理が
1位、3位、5位、6位と上のほうを独占しているね。
日本語のネットコミュニティでもかのytbさんが目立っているし
ファジー論理が最近のホットな話題ってのは事実だろうね。

>>708
ザデーか

>>708
「日本語のネットコミュニティ」ではロジックの中心みたいに見える集合論の論文は
>>706のランキングんは全然出てこないな。
やっぱり日本は島国なんだろうな、世界の流行から隔絶ｗ

>>710
笑う事ではないよ

「マンガでわかるZFC（仮）」
http://togetter.com/li/264548

762：１３２人目の素数さん：2011/12/24(土) 05:01:26.65 downup
日本は世界中で鉄道が斜陽産業と言われていた最中に鉄道技術に投資し新幹線を開発して鉄道の新たな時代を切り開いた。
世界中で見捨てられたから日本も見捨てる、では中韓と何も変わらない。

>>710
だいぶ上の方の>>170-179で言われていることだが、
非古典論理は論文量産型の分野なので当然引用回数も多くなる。

被引用回数よりも、昨年一年APALで「最もホットな論文」のランキングの方がまだ信用できる。
1位と5位こそ非古典論理だが、2位にちゃんと集合論の論文がある。
その他、3位は再帰理論、4位は証明論で6位がモデル理論だ。

Top 25 Hottest Articles
Mathematics > Annals of Pure and Applied Logic
January to December 2011 full year
http://top25.sciencedirect.com/subject/mathematics/16/journal/annals-of-pure-and-applied-logic/01680072/archive/36/

>>704
話題があることと、掲示板が盛り上がることはそれほど関係しないと思いますね。
この掲示板では非古典論理の話題はほとんど出ませんが、
研究が多岐に細分化されすぎているから議論にならないんだと思います。
>>705
ゲーデルからはじまった。
>>708
その被引用数からホットな話題が分かるかは不明です。
私の印象ですが、ファジー論理は恐らくコンピュータサイエンスの影響ですね。
人工知能ブームとか工学の制御系ソフトウェアの研究がきっかけです。
例えばオントロジー工学で記述論理を発展させようとしたとき、
大抵、様相論理（とりわけ時相論理）やファジー論理の方に拡張するんで。
そのせいで、ファジー論理は分厚いハンドブックのシリーズも出ています。

ttp://d.hatena.ne.jp/lkozima/20100806/1281098179
（一応貼っときます

※とりあえずまだ書き込まれてなさそうなロジックネタ

・MontagueのUGという体系がきっかけではじまった、
チョムスキー階層n＋1階部分がシンタックスになり、
n階部分がそのモデルになる自己反映型言語。
・同じくMontagueが内包論理内部で展開した
自然言語Englishの定量的断片である型付理論ME_a。
・Thorndykeから始まった物語を生成文法ベースで記述する体系SGが、
ホーン節に基くKowalski Logic上で展開しStory Treeで任意の物語を生成する。
・Goodmanから始まるメレオロジー系の音譜言語。
・生成文法を一般化した、非線形現象の記述に便利なL-systems。
（抽象的書換えシステムARSの断片PRSに該当。）
・Spencer-BrownのLaws of FormからはじまるBoundary Logic
（2値ブール代数の簡易表示、binary logicとも同値）をPA（初等算術）に発展させ、
計算機言語上のネスト構造そのものに算術を埋め込む。
・Brownian formでの不動点束を使った自己言及系パラドクスの視覚化。
・真理値を文字列とするWave Logicで、真理値をバイナリ―列に限定したDiamond Logicに、
無限に長い論理式とその極限や余極限の概念を導入したLimit Logicにおける不動点定理と、
チャイティンによるシステムSの不完全性定理の証明との関係。
・囚人のDilemmaの異種、Gedel GameやLob Gameなどからはじまるパラドクス的Dilemma Game理論。
・PTなど集合論じゃないフレーゲ構造（循環許容システム）。
・新フレーゲ主義者Crispin Wrightの2階述語論理＋ヒュームの原理で算術の形式化。

見出しだけ並べて内容は把握してないと見た

　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_
　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、
　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ
　　　　　/　　　／:::::／　　　　　　　　　　　＼
　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 |
　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 |
　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ|
　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　
　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。
.　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。
　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。
　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて
　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。
　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は?
　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？
　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼
.　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼
　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 |
　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､
　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣|
　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/

>>707
それ面白いと思ってやってんのか
友達だったら恥ずかしいからやめろという
生まれてから一度もセックスしたことないだろ

>>714
その２位は集合論の論文ではない。
形式集合論の論文というべきものだ。Fuzzy Logic にしろ、他の分野のもの
にしろ深い結果の論文よりも、易しく数多くの人のわかる論文がホットになる。

>>717
そんな難しい話題でもないです。
チョムスキーの生成普遍文法を統語論的に
扱ったのがMontagueのUG（Universal grammar）です。
これは内包論理とよばれる様相論理の一種です。
チョムスキー階層は下がるにつれ一般化されるんで
低階層がモデルになるのは結構自然なイメージだと思います。
これで同じ言語の内部でシンタックスとモデルを分けるのがプログラミング言語で話題になります。
自然言語NLみたいな自然言語の形式化で関数言語で使われているんですが、
様々な自然言語に使われてもいるんですよね。
Thorndykeも同じ生成文法系の統語論系の言語ですね。
L-systemは生物学系の体系で項書換え系システムの一種ですが、
ソフトウェアも出ていて、フラクタル集合とかも実行できますよ。
Wrightの2階述語論理＋ヒュームの原理は、
SOLで集合の外延交換の公理からペアノの公理が全部出るって話です。
一方Goodmanのはオントロジー系の研究です。
フレーゲ構造はアクゼルのイメージを実現した話で型理論の数学です。
これらはググればＰＤＦがすぐ出てきます。
残りはN S HellersteinのDiamond って本を参照してください。
ネット上には余り出ていませんが、スペンサーブラウン自体は批判されています。
しかし私にはもう時間がない

>日本は世界中で鉄道が斜陽産業と言われていた最中に鉄道技術に投資し
>新幹線を開発して鉄道の新たな時代を切り開いた。

ロンドンもパリもニューヨークも大抵高架か地下鉄で
踏切なんてロクにありゃしないが、東京には今でも山ほど踏切がある。

>世界中で見捨てられたから日本も見捨てる、では中韓と何も変わらない。

日本の都市交通は、いまだに鉄路と道路が平面交差してる点で
ぶっちゃけ中韓、東南アジアと大して変わらん。
立体交差が当然の、ヨーロッパや北アメリカとは全然違う。

>>717
＞見出しだけ並べて内容は把握してないと見た
ネットでは珍しくないだろｗ

STS446は、ほら、イタイ奴だからさｗ

数学基礎論って旧帝系の大学でもやってんの？

今の日本の無知な若者が嘲笑する中国、韓国の状況は
過去の日本の状況そのものだったりする。

「なんでもかんでも○○が一番」というのは
別に韓国の専売特許でもなくその昔は日本にも
こんなイタイことを平気でほざく奴が沢山いた。

>>724
旧帝大は、大日本帝国滅亡後、沈没の一途だからｗ

東大は秋入学で浮上したいらしいが、あれで完全に滅亡だな。

まあ、諸悪の根源は法学部と医学部だから。
理工系はダニどもから独立したほうがマシだろう。

なんでわざわざ自滅の方向に進むのか？
もっとましな政策があっても良いと思う。

>>727
政策で解決できることじゃないな。
文明の発展は自爆行為。
おそらく、数千年後も生き残るのは
今も狩猟採集生活を送っている人々だけ。
文明に毒された連中の子孫は滅亡してるな。

そしてその民族もたまに来るメテオで
くたばるのか。。。

>>715
コンピュータサイエンス→コンピュータエンジニアリング

>>722
>ロンドンもパリもニューヨークも大抵高架か地下鉄で
>踏切なんてロクにありゃしないが、東京には今でも山ほど踏切がある。
ロンドンもパリもニューヨークも、中心部しか行ったことがないと見た。
郊外に行けば踏切が結構沢山あるぞ。
東京だって中心部は殆ど高架か地下鉄だろ。
旅行者としてしか行ったことないくせに偉そうなこと語るなよ。

フランスの新幹線、TGVは踏切すごくたくさんある。
新幹線は山形とかごく一部の地域に限られるけど。

>>714
2位って、佐藤さんのあの論文、あれが集合論の論文とはねえ...
3位も再帰論の論文とは言いがたい。
タイトルに "set theory" とか "recursion-theoretic" と付けば
集合論や再帰論の論文になるとか思っているおバカだな。
ま、4位の新井先生の論文はお前の言うとおり証明論だがな。

新幹線を成功させた頃の日本は確かに輝いていた。しかしいまの日本はどうか？
世界の流行から外れたものに目をつけて、新たな時代を切り開いた例があるだろううか？
いまの日本は世界で流行っているものを取り入れるだけで、正に中韓と同じではなかろうか？

>>706
そのランキングで1位の6人共著の論文、19回引用されて1位になっているようですけれど、
引用している論文を調べてみると14本は6人の著者の誰かが著者になっています。
つまり自著引用を除けば5回しか引用されていない、ということです。
ランキングはあくまで目安、とは言いますが、これでは目安にすらならないのではないでしょうか？

2位と4位の論文が日本人によるものなら、別に世界から隔絶されてないじゃん

さて、時間が出来たので残りの部分を解説。
Diamond Logicは4つの真理値をとる。
tttttt…（＝“t/t”）⇔真
tftftf…（＝“t/f”）⇔真でも偽でもある
ftftft…（＝“f/t”）⇔真でも偽でもない
ffffff…（＝“f/f”）⇔偽
これに順序構造を入れると、
t/t（＝true）
t/f f/t
f/f（＝false）
みたいな形になる、だからDiamond。
“/”の定義は
a/b＝( a ∧ (t/f) ) ∨ ( b ∧ (f/t) )
＝( a ∨ (f/t) ) ∧ ( b ∨ (t/f) ).
この記号は“だが”のような意味で解釈する。
例えば“t/f”は“真だが偽”。
これはtとfだけのバイナリだけど一般にn個のものはWave Logicと呼ばれる。

次にBrownian form。
基本はMarkで“￣|”で表す。

￣| ￣| ＝ ￣|

￣|
￣| ＝ ・

が成り立つ。

X￣| :＝ not X

XY :＝ X ∧ Y

なんかで定義、古典ブール代数と同じ。
このとき不動点は、
￣￣￣￣|
￣￣￣| |
| |
￣￣

ブラウンの定義は幅をとるので、Boundary Logicを定義。
[] = true;
[[]] = false;
[ A ] =¬A;
AB = A ∨ B;
[[ A ][ B ]] = A ∧ B;
[ A ] B = if A then B;
[[ A ] B ][[ B ] A ] = A xor B;
見ての通りプログラムのネスト構造。
()()＝() :＝ 0×0＝0
なんかで算術が定義される。
ネスト内部に何も書かなければ動作しないんで問題なくプログラムで実装可。
後の細かい話は適当なPDFを。
http://ir.canterbury.ac.nz/bitstream/10092/2491/1/12614995_Meguire.pdf

Limit Logicは極限不動点による停止定理がチャイティン不完全性定理の
停止不可能なビット列であることを意味している。
まず導入される論理式は、
Inf(x_n) ＝ (All N ≧ 0 )(Exists n ≧ N)(x_n)
＝(x1 ∨ x2 ∨ x3 ∨ x4 ∨ ...)
∧(x2 ∨ x3 ∨ x4 ∨ ...)
∧(x3 ∨ x4 ∨ ...)
∧(x4 ∨ ...)
∧ ....
Cof(x_n) ＝ (Exists N ≧ 0 )(All n ≧ N)(x_n)
＝(x1 ∧ x2 ∧ x3 ∧ x4 ∧ ...)
∨(x2 ∧ x3 ∧ x4 ∧ ...)
∨(x3 ∧ x4 ∧ ...)
∨(x4 ∧ ...)
∨ ....
の2つで、きょｋ

この数学フォーラムに書き込むのはこれで最後にします。
以降プログラム技術などのフォーラムに移る予定ですが、
恐らくこれからは匿名で活動したりメーリングリストで内輪の活動になると考えています。
これまで多くの書き込みを行ったのは、
順序構造の研究などに専念されている数学サイドの方々に、
計算機・哲学サイドの大局的な視野や物語というものを紹介したかったからでした。
それはある意味では成功したし、別の意味では不快感を与えるだけに終わったのかもしれません。
しかし現在私が数学サイドの述べる非古典論理（例えば部分構造論理や直観主義論理）
の話を耳にするたびに、一般性のない不自然な形式化の仕方に疑問を感じます。
しかしそれは皆さんの興味の対象があくまで数学だからなのかもしれません。
私には非可算濃度だとか巨大基数だとかは内実のないシンボリック操作としての興味しかありません。
やはり論理というよりCoqのような構成的な型体系の中ですべての言語を展開するのが自然に思えます。
以上。

大物逝く...

>>735
禿同。被引用回数なんてのは、
自己引用で稼げる数が大勢に影響しない程度の数にならないと指標として意味をなさない。
ネイチャーとかサイエンス級の論文の比較にしか使えない。基礎論の論文の比較に使うのは無意味。
もう一つの hottest article のランキングも、ダウンロード数で比較しているみたいだが
著者が自分でダウンロードする回数が影響するような回数ならまず意味がない。
具体的な数字が出てないので、どれくらいの回数なのか分からないけど。

食べログのスレはここですか？

ランキングの信頼性にケチつけるのはいいが、
>>714のランキング2位が集合論でないとすると15位のMoschovakisの論文まで集合論の論文はなくて、
>>706のランキングでは全くなし。>>714と類似の過去のランキング(2009年10月からの1年間)でも
集合論の論文での最高位は21位の池上さんのだ。
ランキングに意味がないと言うのも一理あるとは思うが、
どのランキングを見ても集合論の論文がない（かかなり低順位）となると、
負け惜しみ見えるのもまた事実だな。

このスレの流れは、日本は「世界の流行から外れた」集合論「に目をつけて、新たな時代を切り開」くべきだということですか？

>>733
それじゃどうやって分野を判断するの？

異なる分野の被引用数比べて何の意味があるのか

そう、その魔法の呪文があれば無敵だな。
指標がどんなに低く出たとえしても「分野が異なる」と呪文を唱えれば、どんな批判からでも逃れられるｗ

どんな論文でもオリジナルな結果である限り、分野を細分化していけば「その分野で一番」になる罠ｗｗ

>>747
MSCでも見てみろ

異なる分野で、色々な指標を比較しても意味がないのは確か。問題はそういうときの「分野」の分け方。
数学の被引用数を化学や生物のそれと比較しても意味がない、というのは説得力がある。数学は化学や生物と異なる分野と認識されているから。
基礎論が他の数学と違うというのも、リスペクトされているかは別として基礎論が異なる分野だという認識は数学の中では普通だろう。
問題は、同じ基礎論なのに「異なる分野だから比べても意味がない」と言って説得力があるのか、>>750が言うように思われないか、ということだ。
集合論とファジーが異なる分野だというのは、基礎論の内部では通用しても、外部では>>750のような「イタイ言い訳」にしか聞こえないのかも知れない。
ファジーの世界の外にいるあなたが、どちらもファジーの論文なのに「異なる分野の指標を比べても」と言われても「イタイ言い訳」としか思えないでしょ？

数学や基礎論関係ならいかなる分野でも、
被引用数が少ないからといって必ずしも価値が無い訳じゃないと言われたら
（その理由に関する限り）素直に納得するけどなあ。
生物学とか工学とかじゃないんだから。

俺は生物学や工学にだって、被引用数が少なくても価値のある研究はあると思うが。

引用数には、引用の多少以外の意味などないことに気づくべき

>>741
それは大変残念です。
この場を貴重な勉強の場にしている者にとって打撃ですらあります。
特に、
>計算機・哲学サイドの大局的な視野や物語
>一般性のない不自然な形式化の仕方に疑問を感じます。
>論理というよりCoqのような構成的な型体系の中ですべての言語を展開するのが自然に思えます。
などの観点でのお話をもっと聞きたかったと思います。
Coqはともかく全体におおいに同感ですし。
>以降プログラム技術などのフォーラムに移る
とのことですが、できればSTS446の筆名で書いていただけるとよいと思います。
匿名にしてもその筆致からいずれ特定されるでしょうから。

age

[Ｐ⊃Ｑ] ⊃ [〜Ｑ⊃〜Ｐ]　恒真式（tautology）であり、
[ＰならばＱ] ならば [ＱでないならばＰでないが成立するが、

しかし、[Ｐ⊃(Ｑ∨Ｒ)] ⊃[(Ｐ⊃Ｑ)∨(Ｐ⊃R)] はtautologyである
にも拘わらず、[Ｐならば(ＱかＲ)] ならば、[(ＰならばＱ)であるか
または(ＰならばRである)] は成立しない。

なんつーか、引用数だのほにゃららファクターだのの話のお決まりのパターンだな。
そういうのを振り翳してアレは駄目だコレは駄目だ騒いでいる奴も痛々しいが、
別の客観的な根拠も示さないで「ほにゃららファクターなんて無意味」とか否定しか出来ない連中も哀れｗｗ
お受験の偏差値談義と基本的な構図は一緒。

>>759-760
数学の知識が全くなくても書けるレス

>>721
スペンサーブラウン批判をネットで読みたい人はこちらをどうぞ。

スペンサー・ブラウンなんていらない
http://www.math.tohoku.ac.jp/~kuroki/SB/
危ないスペンサー・ブラウンに関するリンク集
http://www.math.tohoku.ac.jp/~kuroki/SB/links.html

>>760
自虐ネタ？ワロてあげよう。

分野として価値があるかどうかとは関係ない話として聞いて欲しいのだが、
most-cited のランキングはともかく、hottest のランキングで集合論の論文が2010年でも2011年でも上位に来ないのは確かに不可思議ですね。
論理学の会議があれば集合論は一大勢力なのだし、こんなダウンロードさえされれば順位が上がるランキングなのに。
おいらが勝手に想像する原因は以下のとおり。

・集合論では、みんなが興味を持つような論文は APAL 以外の雑誌に投稿される。
・集合論の内部で興味が分散してしまっていて共通に興味を持たれる論文がない。
・集合論では雑誌掲載前に論文が出回り、誰もエルゼビアのページから落とさない。

いや、どれも「それって集合論だけなのか？」って疑問に答えられんな、スマソ。

>>763
数理論理学の関係では、計算機関係の人の数が断然多い。
だから、そのような人の興味の対象がランキングに反映される。
Fuzzy logic, Fuzzy set もそうだし、上の２位、４位も彼ら
の興味によっている。

>>764
知ったかはカッコ悪いよ。
Hajek の弟子筋がやってる Fuzzy logic を「計算機関係の人の興味」だなんて、
どんだけ無知なんだか。

>>765
ハイェック達って、CS系への応用研究と思われるのが嫌で、
mathematical fuzzy logic という名前付けて、
応用系の fuzzy logic とは差別化しようとしているんでしたっけ。
人口が多い計算機系の人を取り込んだ方が色々有利だと思うんですけど、
偉い人は政治的な打算より数学者としてのプライドが優先するんですかね。

>>766
それは諸刃の剣よ。下手すると、庇を貸して母屋を云々、になるから。
彼らの場合、実際に、計算機系応用系を排除しながら
上で話題になった各種ランキングなどあれだけ高い各種指標を叩き出しているわけで、
（学問的中身はともかく）政治的に相当うまくやってるな、という印象。

>>763
集合論と言うのは、あるまとまったパラダイムを指す用語で無くて、
パラダイムの存在していない複数の論文をさしている用語だからね。
集合に関する解答付き問題集に近い。
文系では、このような分野は多い。

しかし政治的には、外部者には、あたかも
一つのパラダイムが存在していて、そこで自分たちの研究が
中心をなしているように振る舞うことが、政治的には得。
だから、時代とともに中心は政治的意図によって変わり、
長い生命力を持つ研究はほとんど無い。

中国と同じ。
中国数千年の歴史といいつつも、各政権は
断続的で短命。
その時代を支配している政権が、直前の政権の歴史を
抹殺する。

歴史を時の政府の都合の良いようにねつ造して恥じない例が
南京事件。

>>752
集合論もファジー理論も、理論としては存在していなくて、
個々の興味深いが別々の問題とその発見的解法が点在していて、
それらを無理やり分割したり集めたりして分野名を(その時々の
政治的意図によって)なづけているだけだから。

論理式：［(Ｐ⊃Ｑ)⊃(〜Ｑ⊃〜Ｐ)］はトートロジーであり、
論理法則：［(ＰならばＱである)ならば、(ＱでなければＰではない)］
が成立する。　

しかるに、〔〔Ｐ⊃(Ｑ∨Ｒ)〕⊃〔(Ｐ⊃Ｑ)∨(Ｐ⊃Ｒ)〕 は
トートロジーであるにもかかわらず、〔〔Ｐならば(Ｑ∨Ｒ)〕ならば〔(ＰならばＱ)か(ＰならばＲ)〕は成立しない。

>>773
明らかに成立するよ
嘘だと思ったら反例上げてみな？

>>766
「計算機科学に近い」と言うのを侮辱だと思っている数学者は結構多い。
実際、侮辱の意味で言われることもあるしね。
764も、ロジックで流行っているのは計算機科学に近いからで、
自分の大好きな集合論だけは計算機科学に汚されていない高貴な分野、とか思ってそう。
モデル理論の論文が集合論に比べてかなり上位に出てくる理由も
「計算機関係の人の数が断然多い」からなんだろうｗ

>761
圏論は、より長くもってはいるが、結局スペンサーブラウン（形式の法則）と同じ
評価がくだることになると思うにだがどう？どちらもかつて京都の人たちが入れ込んで
いた。

>>776
にだが

>>773
は、Ｐ： x は整数である
Ｑ：x は奇数である
Ｒ：x は偶数である

等を考えているのかも知れないが、
これは x の値によって真理値が違うのでダメ

幾何とか解析とか数論とかに比べて
一般に研究されている集合論が特に場当たり的だとは思わないけどな。

集合論は、数理論理学の研究者にロジックと言うより数学だと思われているし、
集合論の研究者自身もそう思っているし、
集合も論理も似たようなものだ、と思っている人の多くは
集合論を学部低学年の履修科目だとしか思っていないし。

学者としてのプライドがどうのとか侮蔑がどうとかじゃなくて
数学的な興味と計算機科学的な重要性は、
重なる部分も或る程度あるかも知れないけど
基本的に別物でしょ。有機化学と分子生物学とどっちが偉いか、
みたいなもんで答えなんて無い。

このスレで話題になったような計算機科学は数学以外の何者でもない。

計算機科学は非可算無限を嫌う数学。

┌∩┐(◣_◢)┌∩┐
Fuck!
おいおいｗ形式の法則と圏論を一緒にすない！
形式の法則はBinary Logicと完全に同値。
古典論理に論理記号が2つしかいらないという話し。
シェーファ棒とかも同じ発想。
しかし圏論は全く別世界。
圏論はこの世界の原理であり宇宙そのものを支配する言語。

分野甲の研究しているのに、ろくに理解もしていない人間に「分野乙の研究だ」と知ったか顔で言われたら、
不愉快に感じるのは当然だろうし、侮辱だと感じるのも不思議ではないのではないか？
分野乙を見下しているとか優劣がどうとかそういう問題ではない。

タイトルに set theories と付けば集合論の論文だと言ったり
fuzzy と付けば計算機関係だと言ったり
キーワードと断片的な知識だけで知ったかする駆け出しがウロウロしとる

>>783
Cause Stone Cold Said So!!

集合論と関係ない論文にset theoriesとタイトルをつけるセンスもなんとかしてほしい

>>773
＞明らかに成立するよ
＞嘘だと思ったら反例上げてみな？

Ｐ：[あるは正整数である］Ｑ：[xは有理正数であるある]
Ｒ：[xは正実数である]　とおく。

[Ｐならば(ＱかＲ)] は 真。しかるに [(ＰならばＱ)か(ＰならばＲ)] は 偽。

しかるに、[ＰならばＱ]かまたは[ＰならばＲ]　は偽。

>>788 は、反例になってないな。　(^o^)

これ↓ならどうだ。

〔〔Ｐ⊃(Ｑ∨Ｒ)〕⊃〔(Ｐ⊃Ｑ)∨(Ｐ⊃Ｒ)〕 は
トートロジーであるにもかかわらず、〔〔Ｐならば(Ｑ∨Ｒ)〕ならば〔(ＰならばＱ)か(ＰならばＲ)〕は成立しない。

Ｐ：男である
Ｑ：女である
Ｒ；動物である

どういう人がどういう論文をダウンロードしているかは、神様でもなければ分からない。
通常の人間には推測しかできないのに、>>764が断定してしまうのは、妄想癖など何らかの人格障害がある証拠。
まともな人間なら>>763くらいの書き方しか出来ない。

「764＝アスペ」説か。
名前にこだわる787もアスペくさいけどな。

>>783
>形式の法則はBinary Logicと完全に同値。
圏論もλcalcやλholと同値だろ？
Fuck!!

これ↓ならどうだ。

〔〔Ｐ⊃(Ｑ∨Ｒ)〕⊃〔(Ｐ⊃Ｑ)∨(Ｐ⊃Ｒ)〕 は
トートロジーであるにもかかわらず、〔〔Ｐならば(Ｑ∨Ｒ)〕ならば〔(ＰならばＱ)か(ＰならばＲ)〕は成立しない。

Ｐ：ｘは 2<x<6 であるような実数である。
Ｑ：ｘは 4<x<12 であるような実数である。
Ｒ；ｘは 1<x<8 であるような実数である。

何故そこで決定不能命題をとってくるという発想にならないんだ

古典論理か直観主義論理かはっきりさせずに議論しても無益。
直観主義論理ではエムシラ派>>773の言うことは正しい。

なこといえば部分構造論理では正しいとか、何でも言えるがな

>>792
┌∩┐(◣_◢)┌∩┐
Mother Fuck!
λcalcやλhol⇒圏論（CCC）
だが逆は一般に成り立たん、Fuckin!!

Fuckin!! kin!! kin!! kin!!
λcalcやλhol⇔CCC
λcalcやλhol⇒圏論
kin!! kin!! kin!!

エムシラ御大は古典論理を捨てて直観主義論理を採用しろと言っている現代版ブラウワー
という理解でおk？

偉そうなことは、不動点定理みたいな画期的な業績をあげてから語ることだな

>>798
で結局、圏論の方が弱いということか？
Fuckin!!

>>799
白石の白は白痴の白
白痴なぞ大数学者と比較する以前の存在
それどころか白痴とは世にそもそも存在しないにすら等しい

>>802 は、松芯痰。ｗ

>>799
御大は『記号論理学の根本的改革』で直観主義を否定している。（^A^;）ﾊｧﾊｧ

突然ですが、
フィードバックを含む順序論理回路のブール代数での扱い方について
記した本で良い本は無いでしょうか。
いま、コッペルベルグの本を読んでいますが、
ふと情報処理試験を受けてみて気になったもので。

アスペ＝松芯痰は、隔離スレでは誰も相手してくれなくなったんで、こっちに出張してきたのか。
やっぱり隔離スレの看守が必要だな。

エムシラは知ってるが、松芯痰なんてのもいるのか

アインシュタインがジェラシぃ人達がたくさんいる物理ほどではないが
数学にもトンデモは少なからずいるんだよ

「不完全性定理」でtwitterを検索すると、プチトンデモな書き込みがいっぱい出てきて頭がクラクラするなｗ

>>801
┌∩┐(◣_◢)┌∩┐
Fool＆Mother Fuck In!
λcalcやλholを圏論に組み込めるが
逆はできんということだYeah！MoKin!!

>>805
数学の本のスレで聞いたら
ここは文系の人らの巣窟だから分からないと思うよ
自分もそっちは疎いから答えられない

数学は文系だしな

>>807 松芯痰なんてのもいるのか

マツシンとも言う。　本名；松本真吾＠鉄道総合研究所。かずかずの掲示板を荒らして、
顰蹙をかってきたデムパで、エムシラ御大によって fj.sci. math で叩き潰されたの
は有名。ｗｗｗｗ

>>811
なるほど違和感の理由がわかった

www.math.tohoku.ac.jp/~y-keita/friday-seminar/friday-seminar/sanders1112.pdf

↑の文書の27ページ目に

(#2) CZF proves "Each total function from R to R is continous"

とありますが、本当でしょうか？
これが正しいとすると ZF は CZF に排中律を加えたものらしいので、
ZF でも "Each total function from R to R is continous" が
証明できることになってしまうと思うのですが。

「正則性公理がないとZFCは矛盾する」以来の大ネタになりそうなヨカン

>>815
超準（Non-standard analysis)での話だと思われますが?

>>815
なんでそんなリンクの貼り方するの
http://www.math.tohoku.ac.jp/~y-keita/friday-seminar/friday-seminar/sanders1112.pdf

敢えて2chからリファラを送らない形でURL書いてるのに
なんで改悪するんだよ
そのくらい察しろよ

>>815
CZF proves "Each total function from R to R is continous"
これは次のようなことではないでしょうか？

「『実数上の全域関数』として構成的数学において認められるモノ」はすべて連続である。

『実数上の全域関数』と通常認められても構成的数学ではそうでない、
というモノがきっとたくさんあるので、
ZFが変な事を証明するということにはならないと思います。
素人なので間違っていたら恐縮です。

>>813
「鉄道総合研究所」という名前の研究所はないが

EURMSは「ユルムス」と読むらしい。
島根県 西伯郡大山町 下市75
電話: 0858 58 2601

>>822
誤　島根県
正　鳥取県

大した違いじゃないが。

>>819
なんでそんなことわざわざするんだよ
馬鹿馬鹿しい

厨だからでしょ

>>820
公理が増えれば定理が増えるのは当然。
もし "Each total function from R to R is continous" が CZF の定理なら
CZF + PEM = ZF の定理にもなる。この点は>>815が正しい。

>「『実数上の全域関数』として構成的数学において認められるモノ」はすべて連続である。
これは正しいが、この事実を
>(#2) CZF proves "Each total function from R to R is continous"
と表現するのは、論理学の初歩が身についていない「駆け出し」の典型的な誤り。
そのページの(#4)も同様に間違い。

ニュー速とかVIPとかにサイトのURLが載っちゃったらしたら
一時的なブロックくらい普通にされることはあるよ
そうでなくても向こうのサーバ管理者が不快感を抱く事はあると思う

Fuckin!
こんな狭い世界でURLが掲載されても何にもならんーーー〜〜〜！！
FooYaahhhhhhhh!!!!!!!
と・こ・ろ・で、
最近「駆け出し」、
Let's OnceMore,
「KAKEDASHI」
というTermがはやっとんのかぁ？？？
YesBaby!!

>>815
その文書は他にも嘘多数なので、参考にしないように。
トンデモ愛好家の方に「是非」と勧めるレベル。
著者は、駆け出しの学生さんかと思ったら、博士号をお持ちだそうだ。

BHK interpretation の定義も、∀の解釈は通常と同じと書いてあるが真っ赤な嘘。
これでは直観主義論理 IL ではなく、中間論理のCDになってしまう。
27ページの (#1) IL rejects AC というのも、
"reject" の意味が不明瞭なので断定出来ないが、かなり濃い灰色。
何故なら Bishop 流の数学では、ある種のACを認めている。

その他、細かい間違いが多数あるが、書くのが面倒なのでやめとく。
「その文書は信用すべきでない」を示すのにはこれだけ間違いを指摘しておけば十分だろうから。

>>826は、「古典論理で不連続関数となるような対象 "f" は本当は不連続な関数なのだが、
構成主義では公理が弱いからその存在が証明できないのだ」と考えるんだろうけど
「或る対象は構成されて初めて存在する」と考える構成主義者はそもそもそう考えない。

だからこそ、排中律も
「本当は成り立っているかも知れないのだが公理系が弱いから証明できない」
じゃなくて単に
「排中律は成立しない（つねに"反例"が存在する）」
という風に表現されるわけで。
「本当は〜〜なのだが」という類の言い方は構成主義に真っ向から反する言い方だと思う。

敢えて二重引用符"で挟んであるのは、二重括弧の中が構成主義的な言明で
外がメタな立場での言明だからでしょ。
こういう言い方は構成主義の話をするときには多くの人がするので
>「駆け出し」の典型的な誤り。
などというのは如何なものか

>>831は著者本人か？日本語が達者だなｗ
って思うくらいに著者と同レベルのレスだな。

>敢えて二重引用符"で挟んであるのは、二重括弧の中が構成主義的な言明で
>外がメタな立場での言明だからでしょ。
問題になっているのは

>CZF proves "Each total function from R to R is continous"

なんだが。CZF ってのは形式体系でしかない。
構成主義というのは CZF の「可能な解釈の一つ」でしかない。
CZF は ZF の部分体系であるのだから、古典数学も CZF の「可能な解釈の一つ」。
命題 A が形式体系 T で証明可能だということは、
その命題は T のどんな解釈でも正しいことを意味する。
こんなことは論理学の初歩。

よって CZF proves "Each total function from R to R is continous" と書いてあれば
CZF の可能な解釈の一つである古典数学でも
"Each total function from R to R is continous" が正しいということ。
Sanders本人も>>381も、論理学の初歩が全く身についていない駆け出しだということだ。

んんｗｗｗｗｗ

831は、
「排中律が証明できない」と
「排中律の否定が証明できる」
の違いから勉強してくるべきだなｗ

だからその構成主義的な解釈の仕方で或る命題を読むと
そういう表現になるというだけだろ。
その前にブラウワーの話とかをわざわざしているのだから
文脈上そのくらいの補間をすることは求められているんじゃないか？
普通のロジックの分野だとprovably continuousとか言うのかも知れないけど
直観主義者は大抵そういう言い方を嫌う。

>>826みたいな事言うのなら今度から
　実数上の全域関数には不連続なものがある。
じゃなくて
　「「実数上の全域関数」として古典論理上の数学において認められるモノ」」には不連続なものがある、
と言うようにしてくれよ。CZFをZFCや普通の数学と両立しないやり方で拡張することだって出来るんだから。

アホだな。

>CZFをZFCや普通の数学と両立しないやり方で拡張することだって出来るんだから
どんな拡張しても定理は増える一方で、
定理であったものが定理でなくなることはありえない。
つまり CZF で定理だという以上、
「どんなやり方で拡張しても」定理でなければいけない。
「ZFCや普通の数学と両立しないやり方」があったとしても
「ZFCや普通の数学になる拡張」がある以上言い訳になっていない。

>「「実数上の全域関数」として古典論理上の数学において認められるモノ」」には不連続なものがある
メタレベルとオブジェクトレベルの区別を付けてから出直してくるんだな。

なんか>>836は覚えたての言葉を披露したがってるようにみえる
"Each total function from R to R is continous"を額面通りに読んではいけない、という要旨が伝わっていないようだ

CZF＝構成主義、というスローガンだけ知ってて、中身分かっていない駆け出しがウロウロしているようだ。
この等号はある意味では正しいが、ある意味では正しくない。
少なくとも>>820のような解釈をすると、CZF=構成主義は正しくない。理由は>>815の通り。
もし

It is true in Constructivism "Each function from R to R is contious"

と書いてあるのなら>>820みたいな解釈の余地があるので間違いではない。
しかしきっちり定義のある形式体系 CZF を使って

CZF proves ....

と書いてあれば明確に間違い。

　　　　　　　　　　__ﾉ)-'´￣￣`ｰ- ､_
　　　　　　　 ,　'´　　_. -‐'''"二ニﾆ=-`ヽ、
　　　　　　／　　 ／:::::; -‐''"　　　　　 　 `ｰノ
　　　　　/　　　／:::::／　　　　　　　　　　　＼
　　　　 /　 　 /::::::/　　　　　　　　　 |　|　|　 |
　　　　 |　　　|:::::/　/　　　　　|　　|　|　|　|　 |
　 　 　 |　　　|::/　/　/　|　　| ||　 |　| ,ﾊ .| ,ﾊ|
　 　 　 |　　　|/　/　/　/|　,ﾊﾉ|　/|ﾉﾚ,ﾆ|ﾙ'　
　　　　 |　　　|　 |　/　/ ﾚ',二､ﾚ′ ,ｨｲ|ﾞ/　　　私は只の数ヲタなんかとは付き合わないわ。
.　　　 　|　　　＼ ∠イ　 ,ｲイ|　　　 ,`-' |　　　　　　頭が良くて数学が出来てかっこいい人。それが必要条件よ。
　　　　 | 　　　　l＾,人| 　` `-' 　 　 ゝ　 |　　　　　　　　さらに Ann.of Math に論文書けば十分条件にもなるわよ。
　 　 　 | 　　　　 ` -'＼　　　 　 　ｰ' 　人　　　　　　　　　　一番嫌いなのは論文数を増やすためにくだらない論文を書いて
　　　　|　　　　　　　 /(l 　　 　＿＿／　 ヽ、　　　　　　　　　　　良い論文の出版を遅らせるお馬鹿な人。
　　 　 |　　　　　　　（:::::`‐-､__ 　|::::`､ 　 　 ﾋﾆﾆヽ、　　　　　　　　　あなたの論文が Ann of Math に accept される確率は?
　 　　|　　　　　　／ `‐-､::::::::::`‐-､::::＼　　 /,ﾆﾆ､＼　　　　　　　　　　　　それとも最近は Inv. Math. の方が上かしら？
　　　|　　　　　　|::::::::::::::::::|` -､:::::::,ﾍ￣|'､　 ﾋﾆ二、　＼
.　　 |　　　　　　/::::::::::::::::::|::::::::＼/:::Ｏ`､::＼ 　 |　'､　　 ＼
　　 |　　　　　 /:::::::::::::::::::/:::::::::::::::::::::::::::::'､::::＼ﾉ　　ヽ、　 |
　　|　　　　　 |:::::／:::::::::/:::::::::::::::::::::::::::::::::::'､',::::'､ 　/:＼__/‐､
　　|　　　　　 |／:::::::::::/::::::::::::::::::::::::::::::::::Ｏ::| '､::|　く:::::::::::::￣|
　　 |　　　　 /_..-'´￣`ｰ-､:::::::::::::::::::::::::::::::::::|/:/`‐'::＼;;;;;;;＿|
　　　|　　　　|／::::::::::::::::::::::＼:::::::::::::::::::::::::::::|::/::::|::::/:::::::::::/
　　　 |　　　/:::::::::::::::::::::::::::::::::|:::::::::::::::::::::Ｏ::|::|::::::|:::::::::::::::/

直観主義数学というのを形式化されてないもので、いうのなら別だが、
通常よく知られており正しいのは、実関数が閉区間で定義されていること
が証明可能なら、（一様）連続である。

>>840
CZF は古典数学、直観主義数学、再帰数学の共通部分を抜き出したもの。
直観主義数学を形式化したものが CZF だなんて思っているようじゃ論外だよ、君は。

>>835
＞だからその構成主義的な解釈の仕方で或る命題を読むと
＞そういう表現になるというだけだろ。

>>837
＞"Each total function from R to R is continous"を額面通りに読んではいけない、という要旨が伝わっていないようだ

命題をすべて構成主義的に読むことにするのなら、
最初の CZF proves の部分は意味がないのでは？
ZF proves に置き換えてもいいことになるんじゃない？

┌∩┐(◣_◢)┌∩┐
Let's Fucking!!
Let's Dancing!!!
CZF |- "Each total CZF function from R to R is continous"
=> ZF |- "Each total CZF function from R to R is continous"
But,
not（ZF |- "Each total function from R to R is continous"）

Fuckin QED!!

You mother fuckin fucker!!
Triceps extension
burbel curls
set ups

>>837
構成的逆数学で、"Each function from R to R is continuous" と書いてあったら
それは「額面通り」というか、素直にこの命題を形式化したものの意味だよ。
もしその文書の部分を「額面通り」に解釈していけないのだとしたら、
その後の構成的逆数学の部分も「額面通り」解釈してはいけないことになって、
その文書で解説している構成的逆数学は、
実際に研究が行われている構成的逆数学とは全然別のもの、ということになってしまうよ。

836は「定理であったもの」ってのを具体的に形式的に書き下してみれば良いじゃん。

"Each total function from R to R is continous"
ってのは要は
CZF |- "f:R → R は全域関数" ならばCZF |- "f は連続"
ってことでしょ。

もうう一つ。

>>835
>だからその構成主義的な解釈の仕方で或る命題を読むと
>そういう表現になるというだけだろ。
>その前にブラウワーの話とかをわざわざしているのだから
>文脈上そのくらいの補間をすることは求められているんじゃないか？

「その構成主義的な解釈の仕方」を>>820がいうような意味、或いは BHK-解釈だとすると、
もし「そのくらいの補間をする」ことにしたら今度はすぐ上に書いてある (#1) IL rejects AC がおかしい。
「『空でない(inhabited)な集合の族』として構成的数学において認められるモノ」には
必ず選択関数は存在するからね。BHK-解釈でも、これは定義から直ちに出てくる。

並べて書いてあるのに
(#1)は「額面通り」解釈すべきで
(#2)と(#4)は「額面通り」解釈してはいけない
というのは、無理があると思うな。

>>846
なんでわざわざ引用符付きで結合の強さ表示しているのに、
それを無視したような解釈するんだ？

CZF proves "...."

とあるんだから、"...." の部分の方が結合が強いに決まっている。
引用符を無視した解釈で、強引に正しいと主張しても意味ないだろ。

Ａが、Ｂのことをいかに的確に罵倒しても、Ａの主張の妥当さは増加しない

相手の論ではなく人格を否定し始めたらもう論議の正当性などどこかへ行ってしまっている