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

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

---

---

[ 新着レスの取得/表示 (agate) ] / [ 携帯版 ]

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