"A note on bounded arithmetic"(P. Pudlak) - あいまいな本日の私 blog

16時から所内セミナー、Yg氏が発表。bounded arithmeticの階層 $S^1_2$ について、 $S^1_2\not\vdash Con(S^1_2)$ であることが知られている。ここで、もし $S_2\vdash Con(S^1_2)$ であれば、 $S^1_2\subset S_2$ が示せたことになるが、残念ながらそれも証明できないことが知られている（Paris-Wilkee）。では、無矛盾性概念をもう少し制限してみたらどうだろうか。この論文は $S_2\not\vdash BDCon_{S^1_2}$ を証明している。ただし $BDCon_{S^1_2}$ の意味は、証明に現れる論理式が全てboundedであれば、 $S^1_2$ の公理から出発してその証明が 0=1 を導出することはない、というもの。

（内容については後で追加します）