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