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