12/01/29 10:38:06.58
量化記号がダブるとか、∀zが入れ子になるとか、束縛したwが出て来ないとか
そんな理由で論理式にしないなんてことよくするの？
415:１３２人目の素数さん
12/01/29 11:04:29.57
>>414
とにかくあれは問題のための問題（悪問）と思う。
実際に使うために論理式を書く場合は、変数はダブらないように書くし、
中に出てこない変数を束縛するなんてこともしないだろ。
416:１３２人目の素数さん
12/01/29 11:08:55.44
そうだな。あんなことをやってるから教養は要らないってことになる。あれは文系かな？どうせ論理を教えるならもっと違うやりかたがあるがな。
417:１３２人目の素数さん
12/01/29 12:44:33.77
圏論上の形式的議論を圏論だけでできるんですか？
述語論理は当然のように使っているようにみえるんですが、これでは圏論は自立していないと
いうことにはならないのですか？
418:１３２人目の素数さん
12/01/29 13:06:57.12
集合論だって述語論理は使っている。
述語論理の上のレベル（というか非論理的公理）として、
集合論などのほかの「数学の基礎」から自立できているかが問題。
述語論理から独立させようなんて誰も考えてないよ。
419:１３２人目の素数さん
12/01/29 14:55:33.43
そうだけど、集合論におけるメタ数学的議論は集合論で形式的に扱う事が出来るけど
圏論におけるメタ数学的議論は圏論で形式的に扱うのはかなりの困難があるし、
その全ての側面を扱うのは難しいと思う
420:１３２人目の素数さん
12/01/29 15:19:53.03
>圏論におけるメタ数学的議論は圏論で形式的に扱うのはかなりの困難がある
慣れの問題でしかない、という説もある。そしてその説には一理ある。
421:１３２人目の素数さん
12/01/29 16:12:47.01
前にちらっと話題に出てきた STS (Structural Theory of Sets) は、
述語論理から独立させて、様相命題論理で集合論を記述しようという話。
つまり比喩的に左側が機械語側、右側がユーザー側として階層をまとめると、
>>412が圏論と巨大基数の話に関して言ったこと：
一階述語論理 － 集合論 － 各数学（圏論もこの一つ）
数学の基礎として圏論
一階述語論理 － 圏論 － 各数学
STSの目指すもの
様相命題論理 ー 集合論 － 各数学
422:１３２人目の素数さん
12/01/29 17:40:49.18
>>418
>述語論理から独立させようなんて誰も考えてないよ。
だったら圏論は述語論理の単なるマクロ集であって、共通の基盤言語だなんて言い方は
しないほうがよいのではないですか？
423:１３２人目の素数さん
12/01/29 17:53:39.66
>>412
こんなんあるでよ
URLﾘﾝｸ(www.math.ucla.edu)
RELATING FIRST-ORDER SET THEORIES AND ELEMENTARY TOPOSES
424:１３２人目の素数さん
12/01/29 18:07:13.66
>>422
なんか色々なことをごっちゃに理解しているように見受けられるな。
「圏論が数学の共通の基盤言語」というのは、
数学の色々な構造から共通の性質を抜き出すのに便利というプラグマティックな話であって
「圏論は数学の基礎として数学と述語論理の橋渡しとなる」というのとは
また別の話だと俺は理解しているのだが。
425:１３２人目の素数さん
12/01/29 18:30:21.14
いや、巷で「数学の基礎」と言われていることの中身を突き詰めれば
>>422の言うとおりマクロ集ということでしかないのでは？
もちろん、それは集合論が数学の基礎というときも同様だけど。
＞なんて言い方はしないほうがよいのではないですか？
「集合論が数学の基礎だ」とか「圏論が集合論に代わる基礎となり得る」とかというのは、
ある意味使い古された言い回し。ここの住人が言い出したことではないので、
こんなところで「その言い方はおかしい」と言っても始まらない。
426:１３２人目の素数さん
12/01/29 18:52:36.82
>>425
「数学の基礎」と「数学の共通の基盤言語」は同じ意味内容だと主張したいの？
427:１３２人目の素数さん
12/01/29 19:32:32.95
数学の共通言語はTEXだよ
428:１３２人目の素数さん
12/01/29 22:07:17.38
圏論は所詮モデル論なんだよ。しかし言語の本質はシンタックスだ。
だから圏論は、共通も何もそもそも言語ですらないんだよ。
同じことは集合論にも言える。
わかるかな。
429:１３２人目の素数さん
12/01/29 22:08:49.88
↑あふぉ
430:１３２人目の素数さん
12/01/29 22:41:02.09
シンタックスだのセマンティクスというのは
メタレベルからオブジェクトレベルをいじる場合の手段の区分。
一階述語論理 － 集合論or圏論 － 数学各論
という階層は、
オブジェクトレベル、メタレベル、メタメタレベルなどの
一つのレベルの中での話。
（オブジェクトレベルの一階述語論理は、
セマンティクスだろうとシンタクスだろうとメタレベルの数学各論の一つになる。）
一つのレベルの中でセマンティクスだのシンタクスだの言うのは無意味。
431:１３２人目の素数さん
12/01/29 22:58:00.44
>>430 ややこしいな
432:１３２人目の素数さん
12/01/29 23:04:50.75
基礎付けの話になると、最終的にどっかで循環にならざるをえないからな。
それを尤もらしい美辞麗句で隠したのが、メタレベルと対象レベルの分離、ともいえるわけだｗ
433:１３２人目の素数さん
12/01/29 23:54:17.46
>>430
なるほど。数理論理学を学ぶために最低限必要なセンスとして
＊シンタックスとセマンティクスが区別できること
＊オブジェクトレベルとメタレベルが区別できること
＊シンタックスとセマンティクスの区別と、オブジェクトレベルとメタレベルの区別が、区別できること
の３つを伺っていましたが、最後の区別がよく分かりました。
434:１３２人目の素数さん
12/01/30 00:02:11.87
＞＊シンタックスとセマンティクスが区別できること
＞＊オブジェクトレベルとメタレベルが区別できること
＞＊シンタックスとセマンティクスの区別と、オブジェクトレベルとメタレベルの区別が、区別できること
これ至言だな
435:１３２人目の素数さん
12/01/30 00:18:37.06
シンタックスとセマンティックがはじめに理解すれば良い
メタな視点は後から考えれば良いし、ロジック学習の基礎において必須でもない。
436:１３２人目の素数さん
12/01/30 00:19:16.47
ソースは誰？ぐぐったら鴨さんのはてなが出てきたけど、これが初出？
437:１３２人目の素数さん
12/01/30 00:23:44.56
俺様勉強法を語って自分の無理解をひけらかしちまう馬鹿＝435、哀れだなｗｗ
438:１３２人目の素数さん
12/01/30 00:36:52.08
>>430で言われているように、
シンタックス（構文論）もセマンティクス（モデル論）もどちらもメタ的な視点の話なので、
良い子の皆さんは435のいうことを真に受けてはいけませんよ
439:１３２人目の素数さん
12/01/30 00:48:22.65
そんなことより、圏論による基礎の話はどうなった？
>>423のリンク先の論文の評価を聞きたい。
440:１３２人目の素数さん
12/01/30 05:32:38.82
>>432
ともいえる、なんて控えめである必要はなく、そう断言してしまってもいいと思う
というか「メタレベルとオブジェクトレベルは、避けられない循環を飾る美辞麗句」なんて
基礎付けの本質を突いた至言だと思う、鴨さんの３つの区別と並んで。
441:435
12/01/30 07:17:42.79
はじめはメタな視点を意識する必要がないという話しだが。
>>438の考えを認めるとすべての数学はメタな視点に基いている。
メタを意識する必要が出てくるのは不完全性定理や内部モデルから。
442:１３２人目の素数さん
12/01/30 07:40:09.73
435=441 のいうことが正しい。
430 に書いてあることは、形式論理の研究者のなかにさえ、そのように
思っている人がありが、無限連鎖に陥るだけで、意味を考えることができ
ない。
443:１３２人目の素数さん
12/01/30 09:06:38.39
学部教養レベルの確認が一段落したら、圏論によってシンタックスとセマンティックスの
区別がなくなるという話もしようぜ。
444:名無しさん
12/01/30 18:58:02.88 Nob3XfwW
ちょうど話題が出たんで、甲鳥さんのページで質問です。
URLﾘﾝｸ(taurus.ics.nara-wu.ac.jp)
＞著者は、また、自然数論は完全性定理が成り立つには強すぎる体系である旨の
＞主張もしている。それも大違いである（こちらは、かなり広まっている誤解だ
＞が、どんなに広まっていようと、専門家に一言相談すれば「それは間違ってい
＞る」と言ってもらえるのだから、言い訳にはならない）。一階ペアノ算術（自
＞然数の加減乗除と大小比較ができて数学的帰納法が自由に使えるが、関数一般
＞や集合一般を自由に扱うことはできない世界と思って、ほぼ間違いない）は一
＞階述語論理上の公理系なので、完全性定理が適用できる。したがって、一階ペ
＞アノ算術の公理系から証明可能な式全体と、一階ペアノ算術の公理系が真とな
＞るすべての解釈で真となる式全体は、一致する。これを、「一階ペアノ算術は、
＞一階ペアノ算術のすべてのモデルに対して、健全かつ完全である」という。
という部分ですが、
「一階ペアノ算術は、一階ペアノ算術のすべてのモデルに対して、健全かつ完全である」
というのは本当に成り立つんでしょうか？今一書いてあることが理解できないのですが。
445:名無しさん
12/01/30 19:03:08.17 qQ0NhdK4
>>444
もちろん本当だと思うが、どう理解できないの？
446:444
12/01/30 19:44:03.54
あぁ勘違いしていた。
完全性定理は論理だけに関する定理だった。
447:名無しさん
12/01/30 20:09:26.65 ZFRpVEeB
>>443
こういう人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場
448:444
12/01/30 20:37:41.38
林さんの数理論理学では
述語論理の完全性と古典算術の完全性を別の定理として区別していますね。（独言
449:名無しさん
12/01/30 20:58:41.96 qQ0NhdK4
>>447 駆け出しだな
450:名無しさん
12/01/30 21:05:58.07
＞圏論によってシンタックスとセマンティックスの区別がなくなる
別にそんなこと無いですけど……
と書こうと思ったら既出だった
451:名無しさん
12/01/31 05:56:45.85
専門家をバカにできるとは 441=442 はアスペか？隔離スレからでてくんな。
452:435
12/01/31 07:13:02.56
どうでもいいことだが、>>442は別人。
453:名無しさん
12/01/31 07:35:35.85
>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
454:名無しさん
12/01/31 07:46:24.58
どうも本当にアスペが隔離スレから出てきたようだな
455:名無しさん
12/01/31 10:16:28.28
>>441
通常の数学（特に代数構造など）の話でも、
★そういう見方をすれば★メタ的な視点に立っているものが多い、
ということに気づけないようでは数理論理学のお先真っ暗。
456:名無しさん
12/01/31 18:12:14.65
とりあえず宣言しとくけど
今夜0時までに
田中の数学基礎論講義の5章までの定理をすべて
Coqで証明するよ＾＾
457:名無しさん
12/01/31 19:23:22.88
すげえ！
458:名無しさん
12/01/31 23:52:26.53
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).
今日はここらへんまでかな。
459:名無しさん
12/02/01 09:29:56.50 S/Q8pgaI
スレの勢いからして
もうそろそろ次スレの季節だな
460:１３２人目の素数さん
12/02/02 00:08:01.24
Record L_PA:Type:=
language
(Func:Set)
(Rela:Set)
(arity:Func+Rela->nat).
今夜はここまで
461:１３２人目の素数さん
12/02/02 04:30:22.70
＞430 に書いてあることは、形式論理の研究者のなかにさえ、そのように
＞思っている人がありが、無限連鎖に陥るだけで、意味を考えることができない。
馬の耳に念仏だな、こりゃ。念仏の「こころ」がまるで分かっちゃない。
馬＝442
念仏＝「メタレベルとオブジェクトレベルは、避けられない循環を飾る美辞麗句」
462:１３２人目の素数さん
12/02/02 05:28:18.34
圏論話は終了か？
463:１３２人目の素数さん
12/02/02 07:31:16.88
┌∩┐(◣_◢)┌∩┐
上の方にある、
一階述語論理 － 集合論 － 各数学
の図式は古典的で、考えているのは数学屋だけ。
実際には一階述語論理 － 集合論の間の区別は曖昧。
464:１３２人目の素数さん
12/02/02 11:50:41.14
参考文献を上げて下さい
465:１３２人目の素数さん
12/02/02 18:25:33.46
┌∩┐(◣_◢)┌∩┐
この本にZFCを一階論理で厳密に展開しているので参考にすること。
Axiomatic Set Theory (Graduate Texts in Mathematics) [Paperback]
Gaisi Takeuti (Author), Wilson M. Zaring (Author)
URLﾘﾝｸ(www.amazon.com)
466:１３２人目の素数さん
12/02/02 18:32:31.58
>>423
（圏論的意味での）イデアル全体とか取っているのは、
そのトポスが集合論の世界に含まれている前提での話。
「一階述語論理と数学をつなぐ」という意味での
「基礎としての圏論」の研究とは言いがたい。
467:１３２人目の素数さん
12/02/02 19:58:10.03
463が言ってる集合論ってまさか
「集合と位相」で習うようなことじゃないだろうか
468:１３２人目の素数さん
12/02/02 20:43:10.06
>>467 だから言っただろ。駆け出しがうようよしてんだよ
469:１３２人目の素数さん
12/02/02 21:34:56.20
┌∩┐(◣_◢)┌∩┐
一階述語論理の言語にZFCの公理系を添加したものと∈-モデルからなる数学は、
厳密に分離することが出来ない、これは実際に展開してみないと気付きにくい。
例えばキューネンなどの本では述語論理の箇所が省略されているので気付けない。
>>465の本の冒頭が参考になる。
470:１３２人目の素数さん
12/02/02 22:25:47.07
「∈-モデルからなる数学」って何のこと言ってるの？
そもそも>>469では述語論理＋ZFCとその上の数学とを
厳密に区別できないと言っているのに対して
>>463では述語論理と集合論（ZFC）とは区別できないと
少し別のことを言っているように思うんだが
集合論は数学をやる上での基本的な言葉みたいなものだから
基本的な論理と一体だとか言うのは普通の数学やってる人達で、
却って情報系・哲学系の人とか数学でもロジックやってる人は
集合論（ZFC）の公理と述語論理の公理は別のレベルのものだとして明確に区別すると思う
（一部の新論理主義の立場に立つ哲学者等を除く）
471:１３２人目の素数さん
12/02/03 04:35:23.02
他人には意味不明な用語法を断りなしにするのは、トンデモか駆け出しの証拠ｗ
472:１３２人目の素数さん
12/02/03 06:24:32.83
>>463
等号公理は、一階述語論理の公理なのか、集合論の公理なのかはっきりしない、
とかそういう意味で区別が曖昧と言っているのかな？
それはイエメンとサウジアラビアの国境が未画定（つまり曖昧）だから
国家としてのイエメンとサウジアラビアの区別が厳密に区別できない
と言っているようなもので的外れ。
473:１３２人目の素数さん
12/02/03 07:11:59.26
>>466
確かにイデヤールの部分はそうなんだけど、
かなりの部分は一階述語論理の直上のものとして理解できるでしょ、
elementary topos というのは正にそれ故に意義のある概念。
集合論に依存していいのなら Grothendieck topos で十分だった。
その論文では「canonical injection である」という述語が、
集合論と同じ表現力を持たせる為に圏論側で必要な「述語記号」だと言ってる。
とはいえ、集合論に依存している部分とそうでない部分をごちゃ混ぜにしているのは確かに問題。
圏論による基礎を標榜している指導的な研究者である著者達がこんな書き方をするから、
「圏論は集合論に変わる基礎」と言っても
一階述語論理 － 集合論 － 圏論 － 各数学
みたいに「屋上屋を重ねる」ような無駄なこと、っていう印象を持たれてしまう。
474:１３２人目の素数さん
12/02/03 07:21:18.20
┌∩┐(◣_◢)┌∩┐
Oh,Motherfucker!（＾＾；
等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれるので問題なし。
475:１３２人目の素数さん
12/02/03 07:25:41.91
問、等号なし一階述語論理でZFC外延公理から以下を導け：
∀x(x∈a ⇔ x∈b) ⇒ (a∈c ⇔ b∈c)
476:１３２人目の素数さん
12/02/03 08:05:16.63
＞等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれるので問題なし。
こういう人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場
477:１３２人目の素数さん
12/02/03 10:06:55.24
>>473
>みたいに「屋上屋を重ねる」ような無駄なこと
それ以前に、圏論が述語論理（λhol含む）や集合論のような共通言語には到底なりえんのじゃないかな。
言語（道具）にしては難しすぎるし奇妙すぎる。
478:１３２人目の素数さん
12/02/03 16:04:59.16
>述語論理（λhol含む）や集合論のような共通言語
述語論理上の理論である集合論と述語論理を並列な言語としてる時点でアウト！
479:１３２人目の素数さん
12/02/03 17:27:53.50
>等号なし一階述語論理でZFC外延公理から等号に関する公理はすべて導かれる
「等号なし」とは、等号記号が言語に入っていないのか、記号はあるが等号公理が入っていないのか。
中身以前に、自分の発言に必要な情報が欠けていて多義的であることに気づかないってのは、やっぱり駆け出しの証拠だ。
謙虚に勉強しなおすがよろしかろう。
ちなみに、前者だとすると、標準的な外延性公理がそもそも記述できない。
後者ならば>>475の言う通り。どちらにしてもおかしい。
480:１３２人目の素数さん
12/02/03 18:12:32.14
>>478 あんたもそういう区別がやっとできるようになった駆け出しだな。
もっと大事なことを言えよ。
481:１３２人目の素数さん
12/02/03 19:14:49.34
欠けた情報は集合論という言葉に対してもそう。
一階述語論理上のZFC⇒集合論だが逆は成り立たん。
482:１３２人目の素数さん
12/02/03 19:39:41.34
┌∩┐(◣_◢)┌∩┐
Suck me!
等号公理を抜いた一階述語論理。
こいつさんに2項述語＝をぶち込むさかい。
483:１３２人目の素数さん
12/02/04 00:23:06.52
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.
先ずは準備っと。
484:１３２人目の素数さん
12/02/04 02:08:35.82
>>473
「数学の基礎としての○○論」の研究なんてのはきょうび流行らない。
元祖の集合論でも、数学の基礎としての集合論の研究なんて久しく聞かないね。
485:１３２人目の素数さん
12/02/04 04:09:04.46
482を恥の上塗りというのだなｗｗｗ
486:１３２人目の素数さん
12/02/04 05:08:41.52
>>485
同感。
ところでmother fuckerの┌∩┐(◣_◢)┌∩┐って
馬鹿さ加減というか無知さ加減が以前の「考える人」と良く似てると思うのだが。
487:１３２人目の素数さん
12/02/04 06:18:45.27
>>484
確かに。部外者が想像する集合論と、実際に集合論で研究されている内容には差異があるかも。
数学の基礎として集合論を志すと、研究の現場に行ってみると
「こういうことをやりたかったのではない！」と思うだろうな。
たしかに専門分野としての集合論は「集合というものの性質を定める規約集」ではなく「累積階層という対象の構造を探求する研究」になっていますね。
とはキューネン本の訳者の言。
488:１３２人目の素数さん
12/02/04 06:47:41.58
>>486
禿堂
489:１３２人目の素数さん
12/02/04 09:32:19.48
(*鶏慣れのために算術命題をチェック。*)
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.
490:１３２人目の素数さん
12/02/04 11:17:47.41
スレチですまんのだけど、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
というような等号公理が導かれてしまうけど、これってどういう原理なの？
わかりやすい説明とか文献あったら教えてくだされ。エラいひと！
491:１３２人目の素数さん
12/02/04 12:25:40.34
>>481
欠けた情報：⇒の意味
怪しげな記号の使い方をするのもトンデモや駆け出しの証拠ｗ
492:１３２人目の素数さん
12/02/04 13:27:08.40
>>473
>かなりの部分は一階述語論理の直上のものとして理解できる
とすると、ZFC その他一階述語理論としての集合論と同じく、
一階述語理論としての圏論がある筈だけど、そんなん聞いたことないぞ
493:１３２人目の素数さん
12/02/04 13:34:28.50
>>491
それはつまらん言い掛かりにしか見えない
494:１３２人目の素数さん
12/02/04 18:53:42.74
>>491
いや、言いがかりではなく481は何を言いたいのか分からん。
自分で読み返してみてそれに気づけないのなら真性駆け出し。
玄人に質問の意図を伝えられない素人の図、だなｗｗ
495:１３２人目の素数さん
12/02/04 19:14:08.17
Awodeyの教科書に
集合論は数学の基礎だというのと
圏論は数学の基礎だというのは意味合いが違うよ的な話が書いてあるよ
496:１３２人目の素数さん
12/02/04 19:19:34.73
こういうのこそ2chらしくていい
俺は「真性」は大歓迎よ
もっと自己主張してほしい
497:１３２人目の素数さん
12/02/04 19:36:05.78
「集合論の公理系」と「ZFC（＋追加公理）」は
イコールじゃないよというようなことを言いたいんだろうけど、
handbook of set theoryとかJechとかは
事実上ZFCかその保守拡大のBGのことしか書いてないよ
良くてMKにちょっと言及するくらい
498:１３２人目の素数さん
12/02/04 19:41:01.53
結局、「⇒」で何を言おうとしているのかが分からないことが原因。
499:１３２人目の素数さん
12/02/04 19:53:43.05
多分
一階述語論理にZFCの公理を加えることだけが
集合を展開する唯一の手段ではない、という趣旨かと。
500:１３２人目の素数さん
12/02/04 20:42:18.03
>>495
定着した古典的な言葉に新しい意味を付与するってのは、研究を宣伝する際の古典的な定石。
他にも逆数学の Simpson がホームページで「数学の基礎」の彼流の意味を解説している。
「集合論は数学の基礎」というのも、Simpson 的な意味で言われる場合もあって、
Awodey が彼の本で言及しているような意味とは必ずしもならない。
結局のところ、言われている文脈を考慮しなければ、どういう意味かは分からない。
しかし「ひねっていない」言葉の意味、というか伝統的なオーソドックスな意味というのがあって、
特に断り書きがないような場合には暗黙の了解的にその意味で理解すべき、というのがある。
それが「数学各論と一階述語論理を繋ぐ」という意味だし、
これがオーソドックスだからこと Awodey が対比の為に言及している。
（オーソドックスでなければわざわざ対比に使わない。）
このオーソドックスな意味での「圏論による基礎」は、
オーソドックスなだけにかなり長いこと研究されている。
いまどき流行らないというのは認めざるを得ないところだが。
501:１３２人目の素数さん
12/02/04 20:53:10.81
>>492
Elementary topos は、確かにモデルに関して記述される場合が多いけれど、
object と morphism の２つの sort を持つ一階述語論理
（お好みなら identity を使って morphism だけの方法でもいいが）を考え、
identity と composition を関数記号として入れれば、
elementary topos であることを一階述語論理で記述できる。
元々 "elementary" という言葉は、
elementary extension, elementary submodel 等々、
一階述語論理の観点という意味合いを持つ。
トポスの重要な性質をすべて
（上述の言語による）一階述語論理で記述できた、
というのが elementary topos の意義。
公理系に関する研究がないじゃないか、というかも知れないが：
完全性があるのだから、
そうやって記述された elementary topos の公理系で何が証明できるか調べることと、
elementary topos に共通する("elementary" な)性質を調べることは同値。
502:１３２人目の素数さん
12/02/04 20:54:57.50
誤字訂正：
×これがオーソドックスだからこと Awodey が対比の為に言及している。
○これがオーソドックスだからこそ Awodey が対比の為に言及している。
503:１３２人目の素数さん
12/02/04 21:27:37.21
>>501
勉強になる
>トポスの重要な性質をすべて（上述の言語による）一階述語論理で記述できた
これはFOLの記述力から自明じゃないかと思うんだが？
504:１３２人目の素数さん
12/02/04 23:06:32.52
>>503
FOLの記述力に関するどういう定理から自明なんだい？
Lawvere が elementary topos の概念を出す前には、
トポスというのは「層全体のなす構造」って定義しかなかったんだよ？
505:１３２人目の素数さん
12/02/04 23:22:32.52
＞定着した古典的な言葉に新しい意味を付与するってのは、研究を宣伝する際の古典的な定石。
＞他にも逆数学の Simpson がホームページで「数学の基礎」の彼流の意味を解説している。
基礎と言ったらヒルベルトプログラムでの意味しか考えられない単細胞なアスペに聞かしてやりたい。
と思ったらいま自分の隔離スレで活動始めやがったとこだった。
ということはこのレスも読んでいるに違いない。
506:１３２人目の素数さん
12/02/04 23:38:56.73
500だけど、>>505に補足：
「数学の基礎」の一番オーソドックスな伝統的な意味は、
Hilbert Programme の意味での基礎付けね。
でも、アスペに言われるまでもなく、
それが数学的に不可能なのことは既に分かっているので、
それ以降は（数学史の文脈などを除けば）
オーソドックスな意味は500で言った通りってこと。
507:? ＊＊論研究報告
12/02/04 23:50:11.10
＊＊論数学では虚数 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
虚数の意味は前から言っているんだが
未だに数学会では遅れた考えを外国でもやっていて
未だ＊＊論には追い付いていない。これは人類の
知的衰退と思われる。我が新人類右脳同盟の啓蒙が
必要と思われる。長年の物質欲ボケがたたってると
思われる。身を引き締めよ。
508:１３２人目の素数さん
12/02/05 00:10:26.39
>>497
確かに「専門分野としての集合論」では、ZFC に公理を加えたものばかりしか考えませんね。
仰る通り、たまにBGとかMKとか出てきますけど。
古典的な数学は殆ど展開できると言われている KP (kripke-Platek 集合論)や
圏論と関係が深い MacLane 集合論や Lawvere 集合論、
直観主義論理の数学は殆ど展開できると言われる CZF (Constructiv ZF)、
某所で話題沸騰中の Quine の NF (New Foundation)などなどの
「その他の集合論」は、集合論というより証明論で研究されているって印象。
「集合というものの性質を定める規約集」を志す人は、集合論じゃなくて証明論に行くべきだな。
509:スレタイスレ446
12/02/05 00:23:04.68
>>490
スレチじゃないと思いますね。
Coqはバージョンによって多少違うようですが、
シンタックスはCIC（帰納的構成計算）という型言語で出来ています。
Coqは帰納的な定理から型理論の導出規則に基づいて、
自動的に新たな定理を作る機能があります、等号公理以外についても。
URLﾘﾝｸ(www3.di.uminho.pt)
の23ページ位からですね。
510:１３２人目の素数さん
12/02/05 00:46:34.99
お、スレ主がお帰りになられたか
511:１３２人目の素数さん
12/02/05 00:59:14.15
C.C. Chang , H. Jerome Keisler
Model Theory: Third Edition がDoverで出るか。
512:１３２人目の素数さん
12/02/05 02:06:56.09
「駆け出し」って煽り文句が流行ってるようだな。
513:１３２人目の素数さん
12/02/05 05:30:41.05
>>501
そうやって一階述語論理上の理論としての圏論は考えられるのは事実だけど、
そういうのがあまり出てこないのは別の理由からじゃないか？
圏論と型理論（高階算術ともいう）との間にかなり密接な関係があることは
かなり早い段階で分かっていた。
(Lambek & Scott の Introduction to Higher Order Categorical Logic など参照。)
型理論は、圏論云々よりはるか前からある「数学の基礎」候補だった。
だから圏論に合わせた一階述語理論をわざわざ作るまでもなく、
型理論を「圏論による基礎のための一階述語理論」として研究されてきたのだと
俺は理解しているがどうか。
514:１３２人目の素数さん
12/02/05 06:37:46.43
いつものことながら圏論基礎ネタは盛り上がるのう
駆け出しから玄人まで一言いいたくなるテーマなんだろうな
515:１３２人目の素数さん
12/02/05 10:35:20.26
>>514
というか、裸の王様のニオイがするからじゃないかな？
516:１３２人目の素数さん
12/02/05 15:25:59.50
集合論は数学の基礎だと言い出したのは
HilbertじゃなくてBourbakiだと思うけど。
集合論はとても超越性の高い理論だから
Hilbertとかは、とても数学全体の基礎にはなりにくいという感覚をまだ持ってたんじゃないかな
517:１３２人目の素数さん
12/02/05 18:18:25.21
>>516
集合論が数学の基礎だというのはまあ違和感はない。
述語論理上の最小限の言語だろう。
その点圏論はまったく違う。いろんな怪しげな概念を強制してくる。
518:１３２人目の素数さん
12/02/05 19:04:10.61
圏論の概念が怪しげだと思うのは、メタな思考に慣れてないからでは？
519:１３２人目の素数さん
12/02/05 19:17:41.18
>>517
圏論が各数学と一階述語論理と繋げるという意味で基礎となりうるかかどうかは既に技術的な問題になっている。
違和感があろうがなかろうがそういう主観的なものはもはや関係ない。
ま、流行るかどうかは主観的な問題も込みなので、知らんけどな。
520:１３２人目の素数さん
12/02/05 19:50:34.43
>集合論が数学の基礎だというのはまあ違和感はない。
>述語論理上の最小限の言語だろう。
どういう意味で最小限と言っているの？
集合論より大きくない述語論理の言語は存在するのだから最小ではないと思うけど？
521:１３２人目の素数さん
12/02/05 20:09:38.23
言語の大小なんて、公理の数を数えるのと同じでナンセンスだろ。
（二つの公理も連言で繋げば一つになるように）
ちょっとした小細工で本質的に変わらないのに大きくも小さくもできる。
522:１３２人目の素数さん
12/02/05 20:14:19.87
>>518
メタなのはむしろ望ましいが、そのメタレベルの概念が怪しげに見えると言っている。
圏論の独自性（の一つ）は、まさにそういう理論の怪しさや不格好のようなことを見抜ける
ところにあるのかなと思っていたんだ。
>>519
言葉はちょっと違うが、流行るかどうかがやっぱり最も大事じゃないの？
技術的に詰めているものが望遠鏡なのか単なるガラスなのか
523:１３２人目の素数さん
12/02/05 20:23:13.33
なんか「ユークリッド幾何は違和感はない、射影幾何は違和感がある」と同レベルに見えるんだよね。
確かに非ユークリッド幾何は、ユークリッド幾何ほどは流行らない。
しかし非ユークリッド幾何には非ユークリッド幾何にしかない意義がある。
両者の比較や、目的による使い分けなどをすることによる相乗効果で幾何学がより深化することになった。
集合論による数学の基礎と圏論による数学の基礎も同じではないのかな？
両方あることで、数学の形式化の理解を深化させてくれる。
524:１３２人目の素数さん
12/02/05 20:33:54.72
優等生の模範解答ですな
525:１３２人目の素数さん
12/02/05 20:39:05.54
射影幾何は非ユークリッド幾何ではないけどね
526:１３２人目の素数さん
12/02/05 20:42:59.35
>>523
紳士的な議論だが、
集合論もあるけどこれもある。流行らないかもしれないが、あったらあったで
いいじゃないか、なんていう圏論は嫌でしょ。
>>520
∈だけ追加だよね？たしか
極小といえばよかったかな
>>521
そんなことはない
527:１３２人目の素数さん
12/02/05 20:50:02.47
>...なんていう圏論は嫌でしょ。
いや、君が嫌ならそれでいいんじゃない？
でも他人に嫌がるように強制できないことも分かるでしょ。
つーか、議論のレベルを女子高生みたいな好き嫌いレベルまで落とすんなら
っこでは誰も君との議論に付き合わなくなると思うけどね。
528:１３２人目の素数さん
12/02/05 20:59:27.54
＞>>521
＞そんなことはない
それだけだと>>527で批判されている「嫌でしょ」と同じく全く説得力ないんだが？
どう「そんなことはない」のか説明してくれないと反論のしようがない。
529:１３２人目の素数さん
12/02/05 21:09:49.50
どんな言語でも、述語記号・関数記号・定数記号が全部有限なら、
小細工することで極小な言語にすることが出来ますね。
公理が極小というのが無意味なのと一緒。最小は勿論無理ですが。
530:490
12/02/05 21:17:56.23
>>509
情報ありがとうございます。参考になりました。他にもなにか文献等
ご紹介いただけないでしょうか。
531:１３２人目の素数さん
12/02/05 21:21:15.51
何を言っているのかさっぱり分かんない…
ちょっと気まぐれで覗いてみたが、まるで地獄だ…
532:１３２人目の素数さん
12/02/05 21:24:59.11
>>522
>流行るかどうかがやっぱり最も大事じゃないの？
そもそも基礎論自体が流行っていないｗｗ
集合論が圏論より流行ってると言っても団栗の背比べｗｗｗ
533:１３２人目の素数さん
12/02/05 21:42:26.99
>>527
へたに柔らかく言い過ぎたか？
そんな圏論ならそんなふうにニッチにやっていけばいい。
だが圏論にはもっと大きな意味があると聞こえているので、もしそうなら衆人にそれが分かるように
言ってくれと言った。
>>528
だって公理の数の件は数えるものが悪いだけだね？
それくらいあなたにも分かっているだろと思うから。
>>529
528とも同じくいまは本質的なことじゃないと思うのでごめん。
534:スレタイスレ446
12/02/05 21:46:45.82
>>530
URLﾘﾝｸ(citeseerx.ist.psu.edu)
私に探せるものであなたに探せないものはない。
535:１３２人目の素数さん
12/02/05 21:58:06.95
＞圏論にはもっと大きな意味があると聞こえているので
こういう誤解をする人は、初心者時代の手作業的な訓練をおろそかにしているのが通り相場
536:スレタイスレ446
12/02/05 22:01:36.30
URLﾘﾝｸ(www.springerlink.com)
>>530
申し訳ないが読んだことがない本で・・・。
537:１３２人目の素数さん
12/02/05 22:10:19.25
>>533
>そんな圏論ならそんなふうにニッチにやっていけばいい。
そんなふうがニッチと思うかどうかは結局主観の問題だからね。
「集合論の問題はニッチなものだけじゃない」と何人かの専門家が解説しているのを見てきたけど、
ほとんどの部外者には「なんだ、やっぱりニッチな話じゃん」としか思わないだろうし。
ニッチかどうかなんてそんなもんよ。
538:１３２人目の素数さん
12/02/05 22:14:10.18
>535 これは必ずしも誤解ではなく、たしかに昔からよく耳にするな
539:１３２人目の素数さん
12/02/05 22:20:50.39
>>537
客観性のない主観的な罵り言葉なんて、負け惜しみの捨て台詞なんだから生暖かくスルーしてやればよろし。
540:１３２人目の素数さん
12/02/05 22:32:07.80
>>538
「もっと大きな意味」とか曖昧な言葉を含んでいるものに
「誤解ではなく」とか断言できる神経が全く理解できないな。
541:１３２人目の素数さん
12/02/05 22:40:37.13
>>540
まさか圏論の近くにはこんな人が多いんじゃないだろなｗ
542:１３２人目の素数さん
12/02/05 22:48:13.06
低俗な煽り合いはもう終了でいい？
もっと生産的な話がしたくてさっきから待ってるんだけど。
>>513
圏論に対応させる形式体系として型理論の方がよく出てくるのは確かにそおの通り。
だけど、圏論をそのまま一階述語論理にのっける公理系も Lwavere を始め研究されている。
最近でも以下のような論文が出ている。最近つっても10年以上前だけど。
URLﾘﾝｸ(www.cwru.edu)
543:１３２人目の素数さん
12/02/05 23:06:11.24
>538,541
そこまで言うのなら「よく耳にする」で済ませないで、
出典を明らかにするなりリンク貼るなりすれば？
そうすれば「低俗な煽り合い」と言われないで済むと思うけど。
544:１３２人目の素数さん
12/02/05 23:41:57.51
>>529
A∧BよりAの方が短い、という意味では公理系の極小性は定義できない？
もちろん、Aと全然違うCとどちらが小さいとも言えないから
集合論と圏論の比較には役に立たないだろうけどさ。
545:１３２人目の素数さん
12/02/06 01:01:17.41
>>526,>>533
数学の基礎付け・形式化に、集合論は必須のものなのか、
それとも別の方法も可能だけど歴史的経緯や使いやすさで集合論が選ばれているだけなのか、
という問題は重要な問題だと思う。
だから「集合論もあるけどこれもある」っていう圏論の研究は意味があるし、全くニッチな研究だとは思わない。
数学の基礎付け・形式化そのものがニッチだという人には「興味が違うのね」としか言えないけど。
546:１３２人目の素数さん
12/02/06 01:17:56.40
哲オタ乙。研究にどんな意味があるかどうかなんて言い方次第って実例だなｗ
547:１３２人目の素数さん
12/02/06 02:25:02.65
538が言っているのは
「独立した個を重視する西洋近代の終焉が...、これからは関係性を重視した圏論が...」
っていうポモな人たち（いや本当にポモなのかも知らないけど）の発言なんじゃない？
そんなのに踊らされてるなんて...
548:１３２人目の素数さん
12/02/06 03:56:14.39
>>544
＞数学の基礎付け・形式化に、集合論は必須のものなのか、
＞それとも別の方法も可能だけど歴史的経緯や使いやすさで集合論が選ばれているだけなのか
その大事な大事な研究の結果、どっちだと分かったの？少なくとも結論には興味ある。
549:１３２人目の素数さん
12/02/06 06:32:36.80
>>548
横レスかもしらんが、型理論型理論と言ってるように、
型理論で形式化できるものは圏論を使って形式化できる。
「通常の数学」はこの範囲。しかし「通常ではない数学」が問題。
集合論でも圏論が形式化できるかが色々微妙なように、
逆に圏論での形式化では集合論的な数学が問題になる。
特に置換公理が型理論（よって圏論）とは相性が悪いので、
このスレか関連スレでも何度か話題になっているように
置換公理を使った数学（要するに集合論的な数学）をどう評価するべきかという問題になる。
550:１３２人目の素数さん
12/02/06 07:10:13.30
集合論派は「群全体のなす圏、環全体のなす圏などは集合論で記述できないがそんなのは数学の中でごく例外的」と言い、
圏論派は「置換公理を使うような数学は圏論では記述できないがそんなのは数学の中でごく例外的」と言うわけですね。
お互い自分に都合がいいように「数学」というものを設定していると。
551:１３２人目の素数さん
12/02/06 07:18:52.67
>>531
何が地獄なの？？
552:１３２人目の素数さん
12/02/06 07:32:15.44
>>550
そうやって党派的な図式にするのは楽しいのだろうが
>>549は「どう評価するべきかという問題になる」と至って中立的なことしか言っていないぞ
553:１３２人目の素数さん
12/02/06 07:48:24.74
どんな定理に置換公理が必要化はこのスレの上のほうで話題になっていたけど、
そういう背景があったわけね。
554:１３２人目の素数さん
12/02/06 08:26:51.39
亀レスだが>>532が絶妙に本質を突いている件
555:１３２人目の素数さん
12/02/06 17:03:49.97
>>549
型理論に埋め込めるCZFは置換公理を含むんだが？
556:１３２人目の素数さん
12/02/06 19:18:19.50
>>551
文系の俺には全くついていけない別世界、とでも言うかな…
557:１３２人目の素数さん
12/02/06 20:57:01.17
集合論と圏論って、互いに直交していたりしないの？
558:１３２人目の素数さん
12/02/06 21:07:53.82
なんだよ直交って
559:１３２人目の素数さん
12/02/06 21:38:40.59
>>557
そりゃ点（要素）対 矢（射）に象徴されるように直交してるさ。
だがこのスレの大勢的論調では、２つはx軸メインかy軸メインかくらいの
違いしかないらしいんでがっかりしたところだ。
>>558
話が遅いな。少しは推察してやれよ。
560:１３２人目の素数さん
12/02/06 22:49:38.08
>>559
そんじゃおまえがその「直交している」ことの偉大な意義を解説してくれや
561:１３２人目の素数さん
12/02/06 23:01:32.01
トンデモ出現のようだな。基礎論スレの恒例行事。
562:１３２人目の素数さん
12/02/06 23:57:09.75
直交しているという表現を使う>>557は多分プログラマの人なんだろ。
処理系作っていた人がそんな表現使ってた。独立しているぐらいの意味だったはず。
プログラマの人は勝手に変な言葉をあやふやに定義して、形式的に定義された言葉で
みんな知っている、という意味不明な前提を持ち出すから話が成立しない。
563:557
12/02/07 00:16:22.09
>562
そうそう、そんな感じ。
関数空間の基底みたいな話がメタ数学にもあったりしないのかな、と思って。
564:１３２人目の素数さん
12/02/07 00:35:55.15
538=559って要するに、
どこかの哲オタの話を真に受けてゲーデルの不完全性定理には深遠な意味があると勝手に期待したものの、
専門家一同の「ハァ？」を買ってしまって逆ギレ、
という構図だね。
565:１３２人目の素数さん
12/02/07 01:08:20.94
>>563
関数空間に、内積を定義しておかないと、直交も何もないってことは理解できてる？
566:１３２人目の素数さん
12/02/07 01:22:43.08
>>557は
直交しているという言葉にきちんとした意味があるのが
前提になっている書き方だろ
せめて「直交しているみたいな概念がメタ数学にも無いのかな」と言わないと
意味分からん
567:557
12/02/07 01:47:35.76
>565
そういわれてみればそうだね。
プログラムコードなら位相を入れられるけど、集合論と圏論といった概念だとムリなのかなぁ。
568:１３２人目の素数さん
12/02/07 01:57:44.20
>>564
不完全性定理以外にそういうネタがあるってのは新たな発見だったｗ
569:１３２人目の素数さん
12/02/07 03:00:59.43
>>562
＞プログラマの人は勝手に変な言葉をあやふやに定義して、形式的に定義された言葉で
＞みんな知っている、という意味不明な前提を持ち出すから話が成立しない。
変な言葉といえば、ポインタで使われる「指す」という用語の
明示的な定義を未だに見たことが無い。
int a = 0;
int *p = &a;
この場合、「pはaを指す」のか「pはaのアドレスを指す」のか？
ネットを徘徊すると、どっちの使われ方も見かける。
だが、前者の方がより多く使われているように見える。
また、経験上、前者の方がより "正しい" ように思える。
しかし、結局のところ、「指す」の明示的な定義は知らない。
一方で、「代入する」という用語には明示的な定義が用意されていることが多い。
この差は何なのか？
570:１３２人目の素数さん
12/02/07 03:30:24.08
>>569
アドレスを指すというのはもともとは誤用であろう（意味は伝わるが）
アドレスそのものはどこにも無いので指せない。（アドレスが示すメモリはある）
ポインタが指すのはメモリであってアドレスではない。
しかしアドレスというのは住所である。
住所は、実際には土地（場所）を指しているのだが
その土地を住所で代表し、「住所」宛の手紙と言うのと同じ。
つまり、「aを指す」と「aのアドレスを指す」は同じ意味であり
どちらが正しいというものではない。
571:１３２人目の素数さん
12/02/07 03:42:49.95
そもそも 「指す」てのはスラングだわな、だから定義なんかされてない
ポインタがアドレスを保持することを「指す」と言ってるだけで
cそのものの動作に「指す」なんてないわな。
572:１３２人目の素数さん
12/02/07 05:11:52.83
>>570
＞ポインタが指すのはメモリであってアドレスではない。
ところがどっこい、どこかのポインタスレにおいて、
「ポインタが指すのはメモリではなくオブジェクトである。これが分からん奴は半人前だ(ｷﾘｯ」
などと主張する輩がいた。あなたとは正反対の主張だ。
また、>>571によれば「ただのスラング」だそうだ。
これは、あなたの主張とも上記の輩とも違う主張だ。
やはり「指す」は変な用語である。人によって全く見解が違う。
プログラミング業界は、なぜ、「代入する」のように明示的な定義を
早い段階で用意しておかなかったのか？この差は何なのか？
仮に「スラング」が正しいにしても、それならそれで
「指すという用語はスラングである」
という "明示的な定義" が必要である。しかし、このような
定義は広く一般に普及しているとは言い難い。
573:１３２人目の素数さん
12/02/07 05:17:35.35
連投失礼。ちょっと訂正する。
× などと主張する輩がいた。あなたとは正反対の主張だ。
○ などと主張する輩がいた。あなたとは異なる主張だ。
574:１３２人目の素数さん
12/02/07 05:36:09.16
世の中にはソフトリンクもハードリンクもあるのだが
575:１３２人目の素数さん
12/02/07 06:03:05.41
>>572
そういうのを人の褌で相撲を取る、というのだ。
誰かの主張を引用するのなら引用元を明示するべきだろう、
でなければ本当にそういう主張がなされたのか、単なる君の誤解なのか確認するすべがない。
そもそも他人の主張を根拠に何かを批判するのならば、
自分もその主張に賛同する旨を明言するべき。
さもなくば、相手が反論しても「それ、俺の主張じゃないし」と言うのと同じ。
学問的な議論をする際の最低限のルールすら身につけていなかったようだから、
以後気をつけるよーに！
576:１３２人目の素数さん
12/02/07 06:18:34.13
>>572
オブジェクトを指すってのはまたずいぶん抽象的な話だな。
オブジェクトはメモリにのっている。なにも異なる主張ではない。
でなけりゃ void * は何を指しているんだ？
そして「指す」はスラングだと言うのにも矛盾しない。
＞ 「指すという用語はスラングである」
＞ という "明示的な定義" が必要である。
なんで？ そんなもんいらんだろ。
「指す」という語は日本語であるという明示的な定義がなくても
みなが問題なく使用しているように。
577:１３２人目の素数さん
12/02/07 06:28:20.37
>>555
その埋め込みは排中律に適用できない。
つまり直観主義論理でないと成り立たない。
「通常の数学」が排中律を使っていないというのなら、
それに加えて置換公理も含めて圏論で扱える、ということ。
578:１３２人目の素数さん
12/02/07 08:46:49.33
圏論による基礎に関して誰かまとめて下さいませんか？
ぱっと見ただけでも色々な流儀（？）があって、私なりにまとめると以下の通りですが
互いの関係がよく分かりません。
・「集合論が数学の基礎」というのと「基礎」の意味は同じなのか異なるのか、
・述語論理と数学を繋ぐのかそうではないのか、
・型理論と「圏論をそのまま一階述語論理にのっける公理系」、
・古典論理を採用して置換公理がないのと、直観主義論理で置換公理があるもの
579:１３２人目の素数さん
12/02/07 19:11:10.11
ただの言葉遊び
580:１３２人目の素数さん
12/02/07 22:14:19.35
>>557-568 >>569-576
しょうもない話だな
581:１３２人目の素数さん
12/02/08 02:01:03.73
>>579
プログラムってのは言葉だからな、日常では「言葉遊び」と軽んずるようなことが、
致命的な問題を起こすことがあるのよ。値呼出しと名前呼出しの違いとかな。
もっとも、嘘つきの逆理とかラッセルの逆理とかだって、日常では「言葉遊び」と軽んじられる。
プログラムと違って現実に問題になることもない、本当のお遊びｗ
582:スレタイスレ446
12/02/08 07:44:11.19
>>578
HANDBOOK OF PHILOSOPHICAL LOGICの12巻に大体載ってる。
583:１３２人目の素数さん
12/02/08 13:59:04.85
>HANDBOOK OF PHILOSOPHICAL LOGICの12巻に大体載ってる
どなたか要点だけでも書いていただけないでしょうか？この本がすぐ見えないので
特に、型理論と「圏論をそのまま一階述語論理にのっける公理系」をなぜ考えるのか
ということだけでもいいのですが。
584:490
12/02/08 22:17:01.19
>>534,536
レス遅れてすみません。すばらしい文献を紹介していただいて感謝しております。
夢中で読んでました。勘違いも見つかったり、まあ、とりあえず自分の疑問を治めることが
できました。ただ、ショックなのは、以前ネットをあさって集めた文書の中に、紹介いた
だいた文献が、既にあったことです。なんとも愚かですなあ。
とにかく感謝感激です。ありがとうございました。
585:１３２人目の素数さん
12/02/08 23:39:35.60
>>582
目次見た感じ、圏論っぽい話はないけど、本当にその巻に書いてある？
586:１３２人目の素数さん
12/02/09 01:34:33.86
>>583
Categorical Logicについて勉強したいならばBart Jacobsの大作"Categorical Logic and Type Theory"を読めばいいんじゃないの？
今はペーパバック版が出て安く買えるようになってるはずだし
587:スレタイスレ446
12/02/09 08:00:19.67
>>583
以前こんな書き込みがありました。
623 ：１３２人目の素数さん：2011/11/23(水) 15:34:26.24
＞哲学ではうん十年前から圏論（カテゴリー論）を扱っており、これと数学基礎論を関連付けせず語るのは片手落ちだ。
哲学（論理学？）と圏論の関係って
証明図の代わりにダイアグラムで書こうってもの。
そのために高階直観主義論理⇔トポス
の対応を考えているだけ。
初等トポス⇔ハイティングモデル
選択公理付きトポス⇔ブールモデル
グロタンディークトポス⇔一階無限論理
また逆にトポスを与えたら
Mitchel Benabou Languageという言語がつくれる。
上のような圏論的解釈の完全性定理に該当するものも証明されている。
そして圏論が数学の基礎となるのは初等トポスに自然数、
1→N→N
｜ ｜ ｜
｜ ↓ ↓
└→X→X
を加えて1→0をとったものが集合論に該当しますというだけのことだろう。
588:スレタイスレ446
12/02/09 08:01:45.94
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)
589:１３２人目の素数さん
12/02/09 21:54:09.74
>>586 >>587 >>588
レスありがとう。今読ませてもらっています。
Jacobsはちょっと高いのでどうしようか．．．
590:１３２人目の素数さん
12/02/10 13:29:32.27
＜コメ作付け制限＞新基準に福島１１市町村が否定的 福島県の１１年産米
緊急調査で放射性セシウムが４月適用予定の新基準値（１キロ当たり１００
ベクレル）を超えた地区があった１２市町村のうち、１１市町村が「１００
ベクレル超５００ベクレル以下」の地区での今春の作付け制限に否定的なこ
とが毎日新聞の取材で分かった。うち４市町は現行の暫定規制値（同５００
ベクレル）を超えた地区でも作付けを認めてほしいとした。農林水産省は自
治体の意向を踏まえた上で２月中にも作付け制限計画をまとめる方針だが、
調整は難航しそうだ。(毎日新聞)
591:１３２人目の素数さん
12/02/10 23:06:31.65
>を加えて1→0をとったものが集合論に該当します
「とった」ってどういう意味だろう？
「公理から取り除く」という意味だとすると、トポスの公理に1→0なんてないし。
「公理として付け加える」という意味だと、1点集合から空集合に射があったら矛盾するし。
同じ言葉が正反対の意味に解釈できるって日本語難しい。
592:スレタイスレ446
12/02/10 23:40:04.42
>>589
圏論的論理学のテキストが無料公開されているのを忘れてました。
URLﾘﾝｸ(www.cs.unibo.it)
ところで以下は型理論学習のための大雑把な予備知識ですが・・・。
λ計算は関数の抽象にλ記号を使った型システムとなります。
型なしλ計算は単一の型を持つシステムとして、やはり型システムに組み込まれます。
究極の型理論として強正規化不能（停止しない式変形がある程度のイメージ、
ただし決定不可能性とは別）ないくつかの型システムがあり、
このシステムの循環する型や、不動点コンビネータを制限することで、
断片としてλ-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の構成さえも許してしまう型システム系の数学が作れます。
593:１３２人目の素数さん
12/02/11 08:58:24.42
>>583
とりあえず>>513の言及している本と>>542のリンク先をそれぞれ見てみたらどうでしょう？
594:557
12/02/11 23:06:33.22
毎度です。>557と関係のあるような関係の無いような話ですが、
CNFに距離空間を突っ込んでHornCNF!=CNFにチャレンジしてみました。
＃数理論理学というよりも計算複雑性の話ですね。
どこか間違っているような気がするのですが、素人なので追いきれず……
どなたかコメント頂けませんでしょうか？
まとめた資料はURLﾘﾝｸ(arxiv.org)にあります。
.tar.gzを付ける必要があるみたいです。
595:１３２人目の素数さん
12/02/12 00:57:16.49
突っ込まなかったけど、>>567について言っておくと、
位相を入れたからって直交は定義できないんですけど。
内積から位相は決まるが、位相から内積は決まらない。
区別は出来ている？
596:557
12/02/12 02:10:25.82
>595
大丈夫です。区別できています。
>567はベクトル空間の間違いですね。
597:１３２人目の素数さん
12/02/12 03:18:53.07
73 ：１３２人目の素数さん：2012/02/09(木) 21:15:32.88
決定性公理 AD って二階算術の命題として定式化出来ますか？
定式化出来るとして、 ADの否定は
ATR0やΠ11-CA0などの体系で証明できますか？
598:１３２人目の素数さん
12/02/12 06:38:58.21
なぜADはATR0やΠ11-CA0などの体系で証明できますか？ではなく
ADの否定は証明できますか、なのだろうか。
599:１３２人目の素数さん
12/02/12 08:34:44.69
選択公理と矛盾する公理じゃなかったっけ
600:１３２人目の素数さん
12/02/12 08:43:40.45
二階算術で定式化できる範囲では選択公理と矛盾しないし（ただし consistency strength は巨大基数レベル）。
つーか、二階算術で定式化できる選択公理もかなり狭い範囲でADと矛盾しないし。
601:１３２人目の素数さん
12/02/12 10:06:01.76
巨大基数レベルってのは巨大基数の帰納的類似物であるような可算順序数レベルってこと？
602:１３２人目の素数さん
12/02/14 10:16:43.45
もちょっと易しい話題にしてくれんかな？
603:490
12/02/15 11:08:49.50
再帰型Tから、T_rectを作るアルゴリズムがご紹介いただいた文献>>534,536 でわかり、
大変感激している最中です。∧、∨、＝や∃までもが再帰型で定義できるというのは
すごい。しかもその定義から作られるT_rectがまさに論理にぴったりとあてはまるのは
不思議としか言いようがない。さて、「再帰型Tから、T_rectを作るアルゴリズム」
というのは、もしかして天下り的に受け取るしかしょうがないのかもしれませんが、
もう少し「再帰型Tから、T_rectを作るアルゴリズム」を深く理解できるような解説
がしてある文献を紹介していただけないでしょうか。あわよくば、「再帰型Tから、
T_rectを作るアルゴリズム」が、当たり前のように思えるようになるといいのですが。
とりあえず今は、圏を知らなければならない気がして予習してます。
どうか偉い方、神様、よろしくお願いします。
604:スレタイスレ446
12/02/15 23:59:02.73
URLﾘﾝｸ(ci.nii.ac.jp)
有名なので既知かもしれませんが
滝田氏の型理論１～４のPDFを参照してください。
Lofの構成的型理論やλ-CubeやL-Cubeの話題まで一通り解説があります。
私はこのPDFで、論理が型理論に埋め込まれる理由が大分理解できました。
※以下、私的メモでレスとは※
URLﾘﾝｸ(www.shayashi.jp)
LET-quantifier condition formula