構成主義と実無限
数学における構成主義・直観主義を「実無限の拒否」と同一視するのはどうなのか，という@ytb_at_twt氏の問いかけを巡ってのやり取り．メインは「実無限を措定する」を「無限集合を表わす（一階の）名辞を認める」と同一視したら構成主義と両立し，「無限集合上の量化文の真偽が確定する（二値原理に従う）とみなす」と同一視したら構成主義と対立する，という話だが，それに尽きない話も少々．
-
Zahlangabeheft
- 9526
- 1
- 4
- 1
-
- いいね！1
Ryota Akiyoshi（秋吉亮太）
@georg_logic
Martin-Lofのタイプ理論にW-typeとか色々足すよ，という話は昔からあるけれど，確かMahlo typeとかだと意図したもの（KPM）よりも強くなるんだよな．タイプ理論ってtermとかに理論内で操作できるからそのせいかと思っていたのだけれど，よくわからないまま今に至る．
2012-11-19 12:25:14
Ryota Akiyoshi（秋吉亮太）
@georg_logic
type theoryと帰納的定義といえばW-typeやら色々あるけれど，一つの例はSpectorかなぁ．Bar Recursion (for arbitrary finite type)は二階算術を解釈できるので，ものすごい非可述なんだけれども．
2012-11-19 12:27:46
Ryota Akiyoshi（秋吉亮太）
@georg_logic
証明とかプログラムを対象化するというとやっぱりHilbertのことが浮かぶけれど，Brouwerって結構そういう面あるんだよね．Bar Theoremの証明読んでいて思ったんだけれど．
2012-11-19 12:32:54
Ryota Akiyoshi（秋吉亮太）
@georg_logic
で，van Attenの本はそこら辺が忠実に書いてあるので重宝している．Dummettの本はだいぶ現代的というか，証明論化されているというか．
2012-11-19 12:34:21
Ryota Akiyoshi（秋吉亮太）
@georg_logic
で，Veldmanの論文が色々とこだわりが見えるんだけれどよくわからないんだよね．``Brouwer's Real Thesis on Bars" http://t.co/RnV6jkr5
2012-11-19 12:36:29
Ryota Akiyoshi（秋吉亮太）
@georg_logic
VeldmanはTroelstraもDummettもvan Attenも，Bar Theoremの定式化としては不十分だ，とかなり強い主張をしているのでぜひともポイントを知りたいのだけれど，何回か読もうとして挫折．．．
2012-11-19 12:38:26