巨大数研究 Wiki
Advertisement
巨大数研究 Wiki
巨大数研究 Wiki
583
ページ
分類: 順序数、数理論理学、証明論、一覧の一覧

証明論的順序数の例

編集するにはログイン

証明論的順序数の例を挙げる。以下，\(\varphi\)をヴェブレン関数，\(\vartheta\)をヴァイアーマンのϑ関数，\(\psi\)をイェーガー・ブーフホルツのψ関数とする．よって弱到達不能基数の存在を仮定する．また出典は歴史的に古いものから明記しているわけではなく，また証明が載っている全ての文献を示しているわけでもない．また証明論的順序数が\(\Gamma_0\)以下の体系を可述的 (predicative) といい，証明論的順序数が\(\Gamma_0\)を超えるが可述的な体系と同一の手法で順序数解析を行える体系を超可述的 (metapredicative) ，\(\psi_{\Omega_1}(\varepsilon_{\Omega_1+1})\)以上を非可述的 (impredicative) という．

可述的体系[]

一階算術 二階算術 集合論 その他 順序数
\(\mathsf{EFA}\)[注 1],\(\mathsf{PRA}\)[1] \(\omega^2\)
\(\mathsf{I}\Sigma^0_1\)[1] \(\mathsf{RCA}_0,\mathsf{WKL}_0\)[注 2][4] \(\omega^\omega\)
\(\mathsf{I}\Sigma^0_n\)[1] \(\varphi_0^n(\omega)\)
\(\mathsf{PA}\)[5][6] \(\mathsf{ACA}_0\)[6][4],\(\Delta^1_1\text{-}\mathsf{CA}_0\)[注 3],\(\Sigma^1_1\text{-}\mathsf{AC}_0\)[6][4][注 4] \(\mathsf{KP}\omega^0,\mathsf{KP}^0_0,\mathsf{KP}\omega^r\)[6] \(\mathsf{EM}_0\)[9][10] \(\varepsilon_0=\varphi_1(0)\)
\(\mathsf{ACA}_0'\)[11][12][13],\(\mathsf{ACA}_0+\mathsf{iRT}\)[14] \(\varphi_1(\omega)\)
\(\mathsf{ACA}\)[6][4] \(\varphi^2_1(0)=\varepsilon_{\varepsilon_0}\)
\(\mathsf{ACA}+\mathsf{BR}\)[6][15],\(\mathsf{ACA}_0^+\)[注 5][16][13][4],\(\mathsf{p}_1(\mathsf{ACA}_0)\)[17] \(\varphi_2(0)\)
\(\mathsf{p}_1(\mathsf{ACA}_0)+(\mathsf{I}_\mathsf{N})\)[17] \(\varphi_2(\varphi_1(0))\)
\(\mathsf{ID}_1^*\!\restriction\)[18][19][注 6],\(\mathsf{ID}_1^\#\)[20],\(\mathsf{PA}^r_\Omega+(\Sigma^\Omega\text{-}\mathsf{I}_\mathsf{N})\)[20] \(\Delta^1_1\text{-}\mathsf{CR}\)[6][21][注 7],\(\Sigma^1_1\text{-}\mathsf{DC}_0\)[注 8] \(\mathsf{BON}(\mu)+(\mathsf{N}\text{-}\mathsf{I}_\mathsf{N}),\mathsf{BON}(\mu)+(\mathsf{N}\text{-}\mathsf{O}_\mathsf{N}),\mathsf{BON}(\mu)+(\mathsf{F}^+\text{-}\mathsf{I}_\mathsf{N})\)[20],\(\mathsf{EM}_0+\mathsf{JR}\)[9][10] \(\varphi_\omega(0)\)
\(\widehat{\mathsf{ID}}_1\)[22][4][23]\(\mathsf{SID}_1\)[24],\(\mathsf{SID}_{<\omega}\)[24][25],\(\mathsf{ID}_1^*\)[18][19][注 9] \(\Delta^1_1\text{-}\mathsf{CA}\)[6][注 10],\(\Sigma^1_1\text{-}\mathsf{AC}\)[6][4],\(\Sigma^1_1\text{-}\mathsf{DC}\)[注 11] \(\mathsf{KP}\omega^r+(\mathsf{IND}_\omega),\widetilde{\mathsf{KP}}^r_0\)[6] \(\mathsf{EM}_0+\mathsf{J}\)[9][10] \(\varphi_{\varphi_1(0)}(0)\)
\(\Pi^0_1\text{-}\mathsf{CA}_{0,\mu}\)[26][4][23] \(\varphi(\mu)\)[注 12]
\(\Pi^0_1\text{-}\mathsf{CA}_{0,<\omega\mu}\)[26][4][23] \(\mathsf{RA}_\mu\)[26][27][28] \(\sup_{\xi<\mu}\varphi(\omega\mu)\)
\(\mathsf{SID}_\mu\)[24] \(\varphi_{\varphi(\mu)}(0)\)[注 13]
\(\Pi^0_{\omega^\mu}\text{-}\mathsf{CA}_0\)[13] \(\varphi_{\mu+1}(0)\)
\(\widehat{\mathsf{ID}}_n\)[22][4][23] \(\Gamma_0[n+1]\)
\(\widehat{\mathsf{ID}}_{<\omega}\)[22][4][23] \(\mathsf{ATR}_0\)[29][30][6][26][4][23][13],\(\mathsf{FP}_0\)[26][31] \(\mathsf{KPl}_0,\mathsf{KPi}_0\)[6][30] \(\mathsf{IR}\)[26][27][28],\(\mathsf{EMU}\restriction\)[32][33] \(\Gamma_0=\varphi_{1,0}(0)\)

超可述的体系[]

一階算術 二階算術 集合論 その他 順序数
\(\mathsf{KPl}_0+(\Sigma_1\text{-}\mathsf{I}_\omega)\)[34][注 14] \(\varphi_{1,0}(\varphi_0^3(0))\)
\(\widehat{\mathsf{ID}}_\omega\)[22] \(\mathsf{ATR}\)[6][4][23][22][34],\(\mathsf{FP}\)[26][31] \(\mathsf{KPl}_0+(\mathsf{F}\text{-}\mathsf{I}_\omega)\)[34][注 15] \(\Gamma_{\varepsilon_0}=\varphi_{1,0}(\varphi_1(0))\)
\(\mathsf{ATR}_0^+\)[26] \(\varphi_{1,1}(0)\)
\(\widehat{\mathsf{ID}}_{<\omega^\omega}\)[22] \(\mathsf{ATR}_0+(\Sigma^1_1\text{-}\mathsf{DC})\)[22][34] \(\mathsf{KPi}_0+(\Sigma_1\text{-}\mathsf{I}_\omega)\)[34][注 16] \(\mathsf{EMU}\restriction +(\Sigma^+\text{-}\mathsf{I}_\mathsf{N})\)[33][注 17] \(\varphi_{1,\omega}(\varphi_1(0))\)
\(\widehat{\mathsf{ID}}_{<\varepsilon_0}\)[22] \(\mathsf{ATR}+(\Sigma^1_1\text{-}\mathsf{DC})\)[22][34] \(\mathsf{KPi}_0+(\mathsf{F}\text{-}\mathsf{I}_\omega)\)[34][注 18] \(\mathsf{EMU}\)[33] \(\varphi_{1,\varphi_1(0)}(0)\)
\(\mathsf{ID}_\mu^*\!\restriction\)[18] \(\varphi'\!\restriction\!(\mu)\)[注 19]
\(\widehat{\mathsf{ID}}_\mu\)[22],\(\mathsf{ID}_\mu^*\)[18] \(\varphi'(\mu)\)[注 20]
\(\mathsf{Aut}(\widehat{\mathsf{ID}})\)[35] \(\mathsf{FTR}_0\)[35] \(\mathsf{KPh}_0,\mathsf{KPh}_0^-\)[35] \(\varphi_{2,0}(0)\)
\(\mathsf{FTR}\)[35] \(\mathsf{KPh}_0^-+(\mathsf{F}\text{-}\mathsf{I}_\omega)\)[35] \(\varphi_{2,0}(\varphi_1(0))\)
\(\mathsf{KPh}_0+(\mathsf{F}\text{-}\mathsf{I}_\omega)\)[35][注 21] \(\varphi_{2,\varphi_1(0)}(0)\)
\(\mathsf{T}_n\)[注 22][36][37] \(\mathsf{S}_n,(n+1)\text{-}\mathsf{INAC}\)[36][37] \(\varphi_{n+1,0}(0)\)
\((n+1)\text{-}\mathsf{INAC}+(\mathcal{L}_\mathbb{O}\text{-}\mathsf{I}_\mathsf{N})\)[36][37] \(\varphi_{n+1,\varphi_1(0)}(0)\)
\(\Pi^1_2\text{-}\mathsf{REF}_0^{(\Sigma^1_1\text{-}\mathsf{DC})},\Sigma^1_1\text{-}\mathsf{TDC}_0\)[38][39][17] \(\mathsf{KPm}_0\)[36][37] \(\mathsf{EMA}\)[36][37],\(\mathsf{OMA}\)[36][37], \(\varphi_{\omega,0}(0)\)
\(\Pi^1_2\text{-}\mathsf{REF}^{(\Sigma^1_1\text{-}\mathsf{DC})},\Sigma^1_1\text{-}\mathsf{TDC}\)[38][39][17] \(\mathsf{KPm}_0+(\mathcal{L}^*\text{-}\mathsf{I}_\mathsf{N})\)[36][37] \(\mathsf{EMA}+(\mathbb{L}\text{-}\mathsf{I}_\mathsf{N})\)[36][37],\(\mathsf{OMA}+(\mathcal{L}_\mathbb{O}\text{-}\mathsf{I}_\mathsf{N})\)[36][37] \(\varphi_{\varphi_1(0),0}(0)\)
\(\mathsf{p}_1(\Sigma^1_1\text{-}\mathsf{TDC}_0)\)[17] \(\varphi_{1,0,0}(0)\)
\(\mathsf{p}_2^{n+2}(\mathsf{ACA}_0)\)[17] \(\varphi_{\omega,\underbrace{0,\ldots,0}_n}(0)\)
\(\mathsf{p}_2^{n+2}(\mathsf{ACA}_0)+(\mathsf{I}_\mathsf{N})\)[17] \(\varphi_{\varphi_1(0),\underbrace{0,\ldots,0}_n}(0)\)
\(\mathsf{p}_1\mathsf{p}_2^{n+2}(\mathsf{ACA}_0)\)[17] \(\varphi_{1,\underbrace{0,\ldots,0}_{n+1}}(0)\)
\(\mathsf{TID}\)[40] \(\Pi^1_3\text{-}\mathsf{RFN}_0\)[40],\(\mathsf{p}_3(\mathsf{ACA_0})\)[17] \(\mathsf{KPi}_0+(\Pi_3\text{-}\mathsf{Ref})\)[41][注 23],\(\mathsf{KP}\omega^-+(\Pi_2\text{-}\mathsf{Found})\)[42] \(\mathsf{EU}+(2\text{-}\mathsf{Uni})\)[41][注 24],\(\mathsf{FIT}\)[40] \(\varphi((\omega,0))=\vartheta(\Omega^\omega)\)
\(\mathsf{KPi}_0+(\Pi_3\text{-}\mathsf{Ref})+(\mathcal{L}^*\text{-}\mathsf{I}_\mathsf{N})\)[41][注 25] \(\mathsf{EU}+(2\text{-}\mathsf{Uni})+(\mathbb{L}\text{-}\mathsf{I}_\mathsf{N})\)[41][注 26] \(\varphi((\varphi_1(0),0))=\vartheta(\Omega^{\varepsilon_0})\)
\(\mathsf{TID}_1^+\)[43] \(\mathsf{p}_1\mathsf{p}_3(\mathsf{ACA}_0)\)[17] \(\mathsf{FIT}_1^+\)[43] \(\vartheta(\Omega^\Omega)\)
\(\mathsf{TID}_2\)[43] \(\mathsf{p}_{5}(\mathsf{ACA}_0)\)[17] \(\mathsf{FIT}_2\)[43] \(\vartheta(\Omega^{\Omega^\omega})\)
\(\mathsf{TID}_2^+\)[43][注 27] \(\mathsf{p}_1\mathsf{p}_{5}(\mathsf{ACA}_0)\)[17] \(\mathsf{FIT}_2^+\)[43][注 28] \(\vartheta(\Omega^{\Omega^\Omega})\)
\(\Pi^0_{n+1}(\Omega)\text{-}\mathsf{ID}(\Pi^0_1)\)[44] \(\Pi^1_{n+2}\text{-}\mathsf{BI}_0,\Pi^1_{n+2}\text{-}\mathsf{BI}_0^-\)[45]\(\Pi^1_{n+3}\text{-}\mathsf{REF}_0\)[45][41],\(\mathsf{p}_{n+4}(\mathsf{ACA}_0)\)[17],\(\Pi^1_1(\Pi^0_{n+3})\text{-}\mathsf{CA}_0^-\)[44] \(\mathsf{KP}\omega^-+(\Pi_{n+2}\text{-}\mathsf{Found})\)[45][42] \(\vartheta(\Omega(n+1,\omega))\)[注 29]
\(\mathsf{TID}_n\)[43][注 30] \(\mathsf{p}_{n+3}(\mathsf{ACA}_0)\)[17] \(\mathsf{FIT}_n\)[43][注 31] \(\vartheta(\Omega(n,\omega))\)[注 32]
\(\Pi^1_{n+2}\text{-}\mathsf{BI},\Pi^1_{n+2}\text{-}\mathsf{BI}^-\)[45],\(\mathsf{p}_{n+4}(\mathsf{ACA})\)[17] \(\vartheta(\Omega(n+1,\varepsilon_0))\)[注 33]
\(\mathsf{TID}_n^+\)[注 34] \(\mathsf{p}_1\mathsf{p}_{n+3}(\mathsf{ACA}_0)\)[17] \(\mathsf{FIT}_n^+\)[注 35] \(\vartheta(\Omega(n,\Omega))\)[注 36]
\(\mathsf{ID}_1\),\(\mathsf{TID}_{<\omega}\)[43][注 37] \(\Pi^1_1\text{-}\mathsf{CA}^-_0,\mathsf{ID}^2_1\) \(\mathsf{KP}\omega,\mathsf{KP}\Pi_2\) \(\psi_{\Omega_1}(\varepsilon_{\Omega_1+1})=\vartheta(\varepsilon_{\Omega+1})\)

非可述的体系[]

一階算術 二階算術 集合論 その他 順序数
\(\mathsf{ID}_1\),\(\mathsf{TID}_{<\omega}\)[43][注 38] \(\Pi^1_1\text{-}\mathsf{CA}^-_0,\mathsf{ID}^2_1\) \(\mathsf{KP}\omega,\mathsf{KP}\Pi_2\) \(\psi_{\Omega_1}(\varepsilon_{\Omega_1+1})=\vartheta(\varepsilon_{\Omega+1})\)
\(\mathsf{ID}_{<\omega}\) \(\Pi^1_1\text{-}\mathsf{CA}_0\),\(\Delta^1_2\text{-}\mathsf{CA}_0\),\(\Pi^0_1\text{-}\mathsf{Fix}\) \(\mathsf{KPl}^r,\mathsf{KPi}^r,\mathsf{KP}\beta^r\) \(\mathrm{T}_2\) \(\psi_{\Omega_1}(\Omega_\omega)\)
\(\Pi^1_1\text{-}\mathsf{CA}\) \(\mathsf{W}\text{-}\mathsf{KPl}\) \(\psi_{\Omega_1}(\Omega_\omega\varepsilon_0)\)
\(\Pi^1_1\text{-}\mathsf{CA}+\Pi^1_0\text{-}\mathsf{BR}\) \(\psi_{\Omega_1}(\Omega_\omega\Omega_1)\)
\(\Pi^1_1\text{-}\mathsf{CA}+\mathsf{Bi},\Pi^1_1\text{-}\mathsf{BI}\) \(\mathsf{KPl}\) \(\psi_{\Omega_1}(\varepsilon_{\Omega_\omega+1})\)
\(\Delta^1_2\text{-}\mathsf{CR},\Pi^1_2\text{-}\mathsf{SR},\Pi^1_2\text{-}\mathsf{SR}+\Pi^1_1\text{-}\mathsf{BI}\) \(\psi_{\Omega_1}(\Omega_{\omega^\omega})\)
\(\Delta^1_2\text{-}\mathsf{CA},\Pi^1_2\text{-}\mathsf{SP},\Sigma^1_2\text{-}\mathsf{AC}\) \(\psi_{\Omega_1}(\Omega_{\varepsilon_0})\)

\(\Delta^1_2\text{-}\mathsf{CA}+\Pi^1_0\text{-}\mathsf{BR},\Pi^1_2\text{-}\mathsf{SP}+\Pi^1_0\text{-}\mathsf{BR}\)

\(\psi_{\Omega_1}(\Omega_{\Omega_1})\)
\(\Delta^1_2\text{-}\mathsf{CA}+\mathsf{Bi},\Sigma^1_2\text{-}\mathsf{AC}+\mathsf{Bi},\Pi^1_2\text{-}\mathsf{SP}+\mathsf{Bi}\) \(\mathsf{KPi},\mathsf{KP}\beta\) \(\mathsf{T}_0\) \(\psi_{\Omega_1}(\varepsilon_{\mathbb{I}+1})\)


より非可述性が強い体系[]

新井・ラティエンを中心としてより強い体系の証明論的順序数が求められているが，それを記述するには技術的に統一的な表記を用いることが難しくなる．よって個別に紹介する．

再帰的マーロ順序数に関連した体系[]

以下の表は\(\mathsf{ZFC}+\mathsf{MC}\)にて，つまり弱マーロ基数の存在を仮定し，最小の弱マーロ基数を\(\mathbb{M}\)とする．

帰納的定義 二階算術 集合論 その他 順序数図形 ラティエンのマーロ基数によるψ関数 ブーフホルツのマーロ基数によるψ関数
\([\Pi^0_1,\Pi^0_1]\text{-}\mathsf{Fix}\)[46][47][注 39] \(\mathsf{MSA}\)[48] \(\mathsf{KPM}\)[49][47][50][51][52] \(\mathrm{T}_{22}\)[47][49][注 40] \((\mathrm{Od}(\mu)\mid\Omega,<),(\mathrm{O}(\mu)\mid\Omega,<)\)[47][49] \(\psi_{\chi_0(0)}\left(\psi_{\chi_{\varepsilon_{\mathbb{M}+1}}(0)}(0)\right)\)[53] \(\psi_{\Omega_1}(\varepsilon_{\mathbb{M}+1})\)[52][注 41]

ラティエン，新井によって未出版ながらも1989年代にはこの結果は知られていた．

再帰的コンパクト順序数，\(\Pi_3\)-反映順序数に関係した体系[]

以下の表は\(\mathsf{ZFC}+\mathsf{WCC}\)にて，つまり弱コンパクト基数の存在を仮定し，最小の弱コンパクト基数を\(\mathbb{K}\)とする．

帰納的定義 集合論 その他 順序数図形 ラティエンの弱コンパクト基数によるψ関数 新井の記述不能基数によるψ関数
\(\Pi^0_2\text{-}\mathsf{Fix}\)[46][54][55][注 42] \(\mathsf{KP}\Pi_3\)[56][54][57][58],\(\mathsf{KP}+\{V\in\mathsf{RM}_2(\ulcorner\omega_n(\mathrm{On}+1)\urcorner)\mid n\in\omega\}\)[59][60][26] \(\mathrm{T}_3\)[54] \((\mathrm{Od}(\Pi_3)\mid\Omega,<),(\mathrm{O}(\Pi_3)\mid\Omega,<)\)[54][55] \(\Psi^0_{\Omega_1}(\varepsilon_{\mathbb{K}+1})\)[56][注 43] \(\psi_{\Omega_1}(\varepsilon_{\mathbb{K}+1})\)[57][58]

ラティエン[56]によればシュッテの恐らく未出版であろう結果[61]も同時期に行われた．また新井[55]の参考文献によれば恐らく未出版であろう[62]などで1990年には知られていた結果であると推測される．


\(\Pi_4\)-反映順序数に関係した体系[]

\(\mathbb{K}_4\)を最小の\(\Pi^1_2\)-記述不能基数とする．

帰納的定義 集合論 その他 順序数図形 ダーンハルトのψ関数 新井の記述不能基数によるψ関数
\(\Pi^0_3\text{-}\mathsf{Fix}\)[46][63][64][注 44] \(\mathsf{KP}\Pi_4\)[46][63][64][65],\(\mathsf{KP}+\{V\in\mathsf{RM}_3(\ulcorner\omega_n(\mathrm{On}+1)\urcorner)\mid n\in\omega\}\)[59][60][26] \(\mathrm{T}_4\)[63][57][64] \((\mathrm{Od}(\Pi_4)\mid\Omega,<),(\mathrm{O}(\Pi_4)\mid\Omega,<)\)[54][55][46][63][64] \(\Psi^{\omega_1}_{\varepsilon_{\mathbb{K}_4+1}}\)[65][注 45] \(\psi_{\Omega_1}(\varepsilon_{\mathbb{K}_4+1})\)[57][64]

\(\Pi_{n+3}\)-反映順序数に関係した体系[]

\(\mathbb{K}_{n+3}\)を最小の\(\Pi^1_{n+1}\)-記述不能基数とする．

帰納的定義 集合論 その他 順序数図形 新井の記述不能基数によるψ関数
\(\Pi^0_{n+2}\text{-}\mathsf{Fix}\)[46][63][64][注 46] \(\mathsf{KP}\Pi_{n+3}\)[46][63][64][65],\(\mathsf{KP}+\{V\in\mathsf{RM}_{n+2}(\ulcorner\omega_n(\mathrm{On}+1)\urcorner)\mid n\in\omega\}\)[59][60][26] \(\mathrm{T}_{n+3}\)[63][57][64] \((\mathrm{Od}(\Pi_{n+3})\mid\Omega,<),(\mathrm{O}(\Pi_{n+3})\mid\Omega,<)\)[54][55][46][63][64] \(\psi_{\Omega_1}(\varepsilon_{\mathbb{K}_{n+3}+1})\)[57][64]


一階反映順序数に関係した体系[]

\(\Xi\)を最小の\(\Pi^2_0\)-記述不能基数とする．

集合論 シュテガートのψ関数
\(\mathsf{KP}\Pi_{<\omega}\)[66][67] \(\Psi^{\varepsilon_{\Xi+1}}_{(\omega^+;\mathsf{P}_0;\epsilon;\epsilon;0)}\)[注 47]


安定順序数に関係した体系　[]

\(\theta\)-記述不能基数からなるクラスを\(\theta\text{-}\mathrm{Indesc}\)とし，\(\Upsilon\)を以下を満たす最小の基数とする．

\(\begin{align*}(\forall \theta<\Upsilon)(\exists\kappa<\Upsilon)&[\kappa\in\theta\text{-}\mathrm{Indesc}]\\ (\forall \theta<\Upsilon)(\forall\kappa<\Upsilon)&[\kappa\in\theta\text{-}\mathrm{Indesc}\to\theta<\kappa]\end{align*}\)

集合論 ラティエンのθ-記述不能基数によるψ関数 シュテガートのθ-記述不能基数によるψ関数
\(\mathsf{KP}+(\mathsf{Stab}),\mathsf{Stability}\)[67][68] \(\Psi^{\varepsilon_{\Upsilon+1}}_{(\omega^+;\mathsf{RSC};\emptyset;0)}\)[68][注 48][注 49] \(\Psi^{\varepsilon_{\Upsilon+1}}_{(\omega^+;\mathsf{P}_0;\epsilon;\epsilon;0)}\)[67][注 50]


\(\Pi^1_2\text{-}\mathsf{CA}\)に関連する体系[]

\(\mathbb{S}\)を最小の鋭敏基数 (shrewed cardinal) とする．

二階算術 集合論 新井の鋭敏基数によるψ関数
\(\Pi^1_1\text{-}\mathsf{CA}_0+(\Sigma^1_2\text{-}\mathsf{CA}^{-})\)[69][70] \(\mathsf{KPl}^r+(\exists x)[\mathrm{Tran}(x)\land x\prec_{\Sigma_1}V]\)[69][70] \(\psi_\Omega(\Omega_{\mathbb{S}+\omega})\)[69][70]


弱到達不能基数\(\mathbf{I}\)で，\(\Xi\leq\rho<\mathbf{I}\)に対し\(\Xi\)が\(\rho\)-可約基数 (\(\rho\)-reducible cardinal) となるものが存在すると仮定する．また，\(\mathbf{I}\)を上を満たす弱到達不能基数の中で最小なものとする．

二階算術 集合論 ラティエンの可約基数によるψ関数
\(\Delta^1_2\text{-}\mathsf{CA}+\mathsf{Bi}+(\Pi^1_2\text{-}\mathsf{CA}^-)\)[71][72][73] \(\mathsf{KPi}+(\exists x)[\mathrm{Tran}(x)\land x\prec_{\Sigma_1}V]\)[71][72][73] \(\Psi^{\varepsilon_{\mathbf{I}+1}}_{(\omega^+;\mathsf{RSC};\emptyset;0)}\)[注 51][注 52]

\(\Pi^1_2\text{-}\mathsf{CA}\)に関連する体系[]

\(\mathbb{I}\) を正則かつ，\(\mathbb{I}\) の下に \(<\mathbb{I}\)-鋭敏基数が定常に存在する基数とする．

二階算術 集合論 新井の鋭敏基数が下に定常に存在する正則基数によるψ関数
\(\Sigma^1_3\text{-}\mathsf{DC}_0+(\Pi_1\text{-}\mathsf{Coll})\)[74] \(\mathsf{KP}\omega+(\Pi_1\text{-}\mathsf{Coll})\)[74] \(\leq\psi_\Omega(\varepsilon_{\mathbb{I}+1})\)[注 53]


また新井も\(\Pi^1_2\text{-}\mathsf{CA}\)周りに順序数解析を行っている[75][76]が，証明が書かれている出版された論文はなく，同様にラティエンの論文も出版されていないのがいくつか存在する[72]．


ペアノ算術に超限帰納法を加えた体系[]

適当な順序数表記に対する超限帰納法を持つ体系に対する証明論的順序数はある程度一般的に知られている．

定義4.6.1（標準\(\varepsilon\)-順序）

\(\prec\)が標準\(\varepsilon\)-順序 (standard \(\varepsilon\)-order) であるとは以下を満たすことである．

  1. \(\prec\)が初等再帰的で，\(\prec\)の定義域\(\mathrm{field}(\prec)\)も初等再帰で，\(\mathrm{field}(\prec)\)上の二項演算\(+,\omega^\alpha n\)も初等再帰的である．ここで\(\alpha,\beta,\gamma\)は\(\mathrm{field}(\prec)\)の元，\(1=\omega^0,\omega=\omega^1\)，\(n,m\)は\([0,\omega]\)の元とし，\(\alpha\preceq \beta:\Leftrightarrow \alpha\prec \beta\lor\alpha=\beta\)とする．
  2. 以下の\(\langle \mathrm{field}(\prec),\prec,0,+,\omega^\alpha n\rangle\)の基本的な代数的性質が\(\mathsf{EFA}\)で証明可能である．
    1. \(\prec\)は線形順序である．
    2. \(0\)は\(\prec\)の最小元である．
    3. \(+\)は結合的である．
    4. \(\alpha+0=0+\alpha=0\)である．
    5. \(\omega^\alpha 0=0\)である．
    6. \(\omega^\alpha (n+1)=\omega^\alpha n+\omega^\alpha\)である．
    7. \(\alpha\prec \beta+1\)と\(\alpha\preceq \beta\)は同値である．
    8. \(0\prec \alpha\land\gamma\prec\beta+\omega^\alpha\to(\exists\delta\prec \alpha)(\exists n)[\gamma\prec\beta+\omega^\delta n]\)である．
    9. カントール標準形が存在する，すなわち任意の\(\alpha\succ 0\)に対し，ある\(\alpha_0\succ\cdots\succ\alpha_n\)と\(m_0,\ldots,m_n\succ 0\)が一意に存在し\(\alpha_0\prec\alpha\)かつ\(\alpha=\omega^{\alpha_0}m_0+\cdots+\omega^{\alpha_n}m_n\)である．
    10. \(\alpha_0\succ\cdots\succ\alpha_i,\beta_0\succ\cdots\succ\beta_j\)と\(n_0,\ldots,n_i,m_0,\ldots,m_j\succ 0\)に対し\(\omega^{\alpha_0}n_0+\cdots+\omega^{\alpha_i}n_i\prec \omega^{\beta_0}m_0+\cdots+\omega^{\beta_j}m_j\)であるには，\(i<j\land(\forall k\leq i)[\alpha_k=\beta_k\land n_k=m_k]\)または，ある\(l\leq \min\{i,j\}\)が存在し\((\forall k<l)[\alpha_k=\beta_k\land n_k=m_k]\land(\alpha_l\prec\beta_l\lor (\alpha_l=\beta_l\land n_l\prec m_l))\)であることが必要十分である．

また\(\prec\)が底 (base) \(\Omega\)の標準\(\varepsilon\)-順序であるとは\(\prec\)が標準\(\varepsilon\)-順序であり，\(\Omega\in\mathrm{field}(\prec)\)かつ\((\forall \alpha)(\exists n)[\alpha\prec\omega_n(\Omega+1)]\)が成り立つことである．ここで\(\omega_0(\alpha)=\alpha,\omega_{n+1}(\alpha)=\omega^{\omega_n(\alpha)}\)とする．

\(\prec\)は整列的な標準\(\varepsilon\)-順序で\(\mathsf{WO}(\prec\!\restriction)\)を\(\prec\)の始切片に対する超限帰納法の図式とする．

算術 直観主義算術 順序数
\(\mathsf{PA}+\mathsf{WO}(\prec\!\restriction)\)[26] \(\mathsf{HA}+\mathsf{WO}(\prec\!\restriction)\)[26] \(\mathrm{otyp}(\prec)\)

\(\prec\)は整列的な標準\(\varepsilon\)-順序で\(\mathsf{WO}(\prec,\Omega)\)を\(\Omega\)に対する超限帰納法とする．

算術 直観主義算術 順序数
\(\mathsf{PA}+\mathsf{WO}(\prec,\Omega)\)[26] \(\mathsf{HA}+\mathsf{WO}(\prec,\Omega)\)[26] \(\varepsilon_{\mathrm{otyp}_\prec(\Omega)+1}\)

\(\Pi^1_1\)-健全ではない体系[]

矛盾する体系は証明能力が非常に高く，証明論的順序数が\(\omega_1^{\mathrm{CK}}\)と最大になる．上記した定理3.5.1により，矛盾していなくても\(\Pi^1_1\)-健全でない体系は証明論的順序数が\(\omega_1^{\mathrm{CK}}\)となる．以下は全て証明論的順序数が\(\omega_1^{\mathrm{CK}}\)である体系である．

算術 集合論 非健全性
\(\mathsf{PA}+\neg\mathsf{Con}(\mathsf{PA})\) 無矛盾かつ\(\Sigma^0_1\)-不健全
\(\mathsf{PA}+(0=1)\) \(\mathsf{ZFC}+(\exists x(x \neq x))\) 矛盾


脚注[]

  1. ↑ 証明が正確に書かれた文献はないと思われる．しかし，ベックマン[1]による\(\mathsf{PRA}\)の証明論的順序数の証明を適当にし修正すれば容易に示せる．
  2. ↑ 古典的な定理だが証明論的証明が書いてある文献を見つけることができなかった．\(\mathsf{I}\Sigma^0_1\)に対する証明を適当に修正することで\(\mathsf{RCA}_0\)の証明論的順序数が分かり，\(\mathsf{RCA}_0,\mathsf{WKL}_0\)が\(\Pi^1_1\)-保存的であることを主張するハーリントン (Paris Harrington) の定理(原論文はunpublishedであるがシンプソン[2]などに証明は見つけられる)や，それの一般化であるSTY定理[3]などを用いれば良い．後述する文献は算術のモデル理論による手法で示されている
  3. ↑ \(\Sigma^1_1\text{-}\mathsf{AC}_0\)が\(\Delta^1_1\text{-}\mathsf{CA}_0\)を含み[2]，\(\Delta^1_1\text{-}\mathsf{CA}_0\)は\(\mathsf{ACA_0}\)を含むことから不等式評価によって証明論的順序数が分かる．
  4. ↑ \(\Sigma^1_1\text{-}\mathsf{AC}_0\)は\(\mathsf{ACA}_0\)と\(\Pi^1_2\)-保存的となる[7][8]ことからも分かる．
  5. ↑ 後述の文献は順に証明論(逆数学)的，再帰理論的，算術のモデル理論的なものとなる．
  6. ↑ アフシャリ・ラティエン[19]で\(\mathsf{ID}_1^*\)と表記されているのがプロブスト[18]での\(\mathsf{ID}_1^*\!\restriction\)である．
  7. ↑ シュッテ[21]での\(\mathsf{DA}\)で示されているのが証明になるが，その証明から\(\Delta^1_1\text{-}\mathsf{CR}\)の証明論的順序数を求めるのはそこまで明らかではない．
  8. ↑ \(\Sigma^1_1\text{-}\mathsf{AC}_0\)は\(\Pi^0_1\text{-}\mathsf{CA}_{0,<\omega^\omega}\)と\(\Pi^1_2\)-保存的となる[7][8]ことから分かる．
  9. ↑ アフシャリ・ラティエン[19]で\(\mathsf{ID}_1^*+(\mathsf{IND}_\mathbb{N})\)と表記されているのがプロブスト[18]での\(\mathsf{ID}_1^*\)であることに注意
  10. ↑ ポーラーズ[6]に事実としては載っていたが証明が書いてある文献は見つけられなかった．上限は\(\Delta^1_1\text{-}\mathsf{CA}\)を\(\Sigma^1_1\text{-}\mathsf{AC}\)が含む[2]ことから良く，下限は\(\Sigma^1_1\text{-}\mathsf{AC}\)に対するものを適切に修正すれば良い．
  11. ↑ \(\Sigma^1_1\text{-}\mathsf{AC}_0\)は\(\Pi^0_1\text{-}\mathsf{CA}_{0,<\varepsilon_0}\)と\(\Pi^1_2\)-保存的となる[7][8]ことから分かる．
  12. ↑ \(\mu=_{\mathrm{CNF} }\omega^{\mu_1}+\cdots+\omega^{\mu_k}\)，\(\xi^\varepsilon:=\min\{\varepsilon_\zeta\mid \varepsilon_\zeta>\xi\}\)としたとき，\(\varphi(\mu):=\varphi_{\mu_k}(\cdots(\varphi_{\mu_1}(\mu^\varepsilon)))\)とする．
  13. ↑ \(\mu=_{\mathrm{CNF} }\omega^{\mu_1}+\cdots+\omega^{\mu_k}\)，\(\xi^\varepsilon:=\min\{\varepsilon_\zeta\mid \varepsilon_\zeta>\xi\}\)としたとき，\(\varphi(\mu):=\varphi_{\mu_k}(\cdots(\varphi_{\mu_1}(\mu^\varepsilon)))\)とする．
  14. ↑ 事実のみはイェーガー・ストラム[34]にかかれているが証明は見つけられなかった．
  15. ↑ 事実のみはイェーガー・ストラム[34]にかかれているが証明は見つけられなかった．
  16. ↑ 事実のみはイェーガー・ストラム[34]にかかれているが証明は見つけられなかった．
  17. ↑ 事実のみはストラム[33]にかかれているが証明は見つけられなかった．
  18. ↑ 事実のみはイェーガー・ストラム[34]にかかれているが証明は見つけられなかった．
  19. ↑ \(\mu\)以下の最大の極限順序数を\(\mu'\)とし\(\mu'=\omega^{1+\mu_1}+\cdots+\omega^{1+\mu_n},\mu_0\geq\cdots\geq\mu_n\)とし，\(\mu=\mu'+m\)とする．また\((\mu\!\restriction\! 0)\)を\(\varphi_{1,\mu_1}(\xi)>\mu\)となる最小の順序数とし，\((\mu\!\restriction\! 1):=\sup\{\varphi_{k,\mu+1}\mid k<\omega\}\)とし，\((\mu\!\restriction\! i+2):=\varphi_{(\mu\!\restriction\! i+1)}(0)\)とする．このとき\(\varphi'\!\restriction\!(\mu)\)を\(\varphi_{1,\mu_n}(\varphi_{1,\mu_{n-1} }(\cdots(\varphi_{1,\mu_0}((\mu\!\restriction\! m)))\cdots))\)を表すものとする
  20. ↑ \(\mu\)以下の最大の極限順序数を\(\mu'\)とし\(\mu'=\omega^{1+\mu_1}+\cdots+\omega^{1+\mu_n},\mu_0\geq\cdots\geq\mu_n\)とし，\(\mu=\mu'+m\)とする．また\((\mu\vert 0)=\mu^\varepsilon,(\mu\vert n+1)=\varphi_{(\mu\vert n)}(0)\)とする．このとき\(\varphi'(\mu)\)を\(\varphi_{1,\mu_n}(\varphi_{1,\mu_{n-1} }(\cdots(\varphi_{1,\mu_0}((\mu\vert m)))\cdots))\)を表すものとする
  21. ↑ ストラム[35]のRemark 2.で言及されているが証明は見つけられなかった．
  22. ↑ 後の\(\mathsf{T}_0\)とは一切関係ない．
  23. ↑ イェーガー・ストラム[41]によれば証明はイェーガーとストラムによってなされたが論文として出版はされていない．
  24. ↑ イェーガー・ストラム[41]によれば証明はイェーガーとストラムによってなされたが論文として出版はされていない．
  25. ↑ イェーガー・ストラム[41]によれば証明はイェーガーとストラムによってなされたが論文として出版はされていない．
  26. ↑ イェーガー・ストラム[41]によれば証明はイェーガーとストラムによってなされたが論文として出版はされていない．
  27. ↑ 下限の証明はランツィ[43]では未解決である．
  28. ↑ 下限の証明はランツィ[43]では未解決である．
  29. ↑ \(\Omega(0,\alpha):=\Omega\alpha,\Omega(1,\alpha):=\Omega^\alpha,\Omega(n+1,\beta):=\Omega^{\Omega(n,\beta)}\)とする．
  30. ↑ 下限の証明はランツィ[43]では未解決である．
  31. ↑ 下限の証明はランツィ[43]では未解決である．
  32. ↑ \(\Omega(0,\alpha):=\Omega\alpha,\Omega(1,\alpha):=\Omega^\alpha,\Omega(n+1,\beta):=\Omega^{\Omega(n,\beta)}\)とする．
  33. ↑ \(\Omega(0,\alpha):=\Omega\alpha,\Omega(1,\alpha):=\Omega^\alpha,\Omega(n+1,\beta):=\Omega^{\Omega(n,\beta)}\)とする．
  34. ↑ 下限の証明はランツィ[43]では未解決である．
  35. ↑ 下限の証明はランツィ[43]では未解決である．
  36. ↑ \(\Omega(0,\alpha):=\Omega\alpha,\Omega(1,\alpha):=\Omega^\alpha,\Omega(n+1,\beta):=\Omega^{\Omega(n,\beta)}\)とする．
  37. ↑ 下限の証明はランツィ[43]では未解決である．
  38. ↑ 下限の証明はランツィ[43]では未解決である．
  39. ↑ 上限の証明は\(\mathsf{KPM}\)に埋め込めることによると思われる[46]．
  40. ↑ 誤字ではない．また後で述べる\(\mathrm{T}_n\)の\(n\)に\(22\)を代入したものとも異なる．
  41. ↑ 下限の証明されてない，あるいは未出版であると思われる．
  42. ↑ 上限の証明は\(\mathsf{KP}\Pi_3\)に埋め込めるからと新井[46]に書いてあるが証明は見つけられなかった．
  43. ↑ 下限の証明は未出版であると思われるがラティエン[56]はこの評価が正確であることを主張している．
  44. ↑ 上限の証明は\(\mathsf{KP}\Pi_4\)に埋め込めるからと新井[46]に書いてあるが，その証明は見つけられなかった．
  45. ↑ 下限の証明は未出版であると思われるがダーンハルト[65]はこの評価が正確であることを主張している．
  46. ↑ 上限の証明は\(\mathsf{KP}\Pi_{n+3}\)に埋め込めるからと新井[46]に書いてあるが，その証明は見つけられなかった．
  47. ↑ 下限の証明は未出版であると思われるがシュテガート[67]はこの評価が正確であることを主張している．
  48. ↑ 下限の証明は未出版であると思われるがラティエン[68]はこの評価が正確であることを主張している．
  49. ↑ [68]による上限の証明はあるシュテガート[67]によって欠陥があると指摘されている．
  50. ↑ 下限の証明は未出版であると思われるがシュテガート[67]はこの評価が正確であることを主張している．
  51. ↑ 下限の証明は未出版であると思われるがラティエン[73]はこの評価が正確であることを主張している．
  52. ↑ [68]と同様の欠陥が[73]にもあるとシュテガート[67]によって指摘されている．
  53. ↑ この値は恐らく正確だが証明はまだ書いていないと新井はRIMS共同研究 (公開型)「証明と計算の理論と応用」で述べていた．

出典[]

  1. ↑ 1.0 1.1 1.2 1.3 A. Beckmann. Separating fragments of bounded arithmetic. Dissertion. Verlag nicht ermittelbar, 1996.
  2. ↑ 2.0 2.1 2.2 S.G. Simpson. Subsystems of second order arithmetic. Vol. 1. Cambridge University Press, 2009.
  3. ↑ S.G. Simpson, T. Kazuyuki, and Y. Takeshi. Some conservation results on weak König's lemma. Annals of Pure and Applied Logic 118.1-2 (2002): 87-114.
  4. ↑ 4.00 4.01 4.02 4.03 4.04 4.05 4.06 4.07 4.08 4.09 4.10 4.11 4.12 J. Avigad, and S. Richard. A model-theoretic approach to ordinal analysis. Bulletin of Symbolic Logic (1997): 17-52.
  5. ↑ G. Gentzen, Beweisbarkeit und Unbeweisbarkeit von Anfangsfällen der trasfiniten Induktion in der reinen Zahlentheorie, Math. Ann. 119(1943), 143-161.
  6. ↑ 6.00 6.01 6.02 6.03 6.04 6.05 6.06 6.07 6.08 6.09 6.10 6.11 6.12 6.13 W. Pohlers. Proof theory: The first step into impredicativity. Springer Science & Business Media, 2009.
  7. ↑ 7.0 7.1 7.2 A. Cantini. On the relationship between choice and comprehension principles in second order arithmetic, Journal of Symbolic Logic 52(1986), 360-373
  8. ↑ 8.0 8.1 8.2 Iterated inductive definitions and \(\Sigma^1_2\text{-}\mathsf{AC}\), in "Intuitionism and proof theory, Proceedings of the summer conference at Buffalo, N.Y.,1968. A. Kino, J. Myhil, R.E. Vesley (eds), North-Holland, 1970," 435-442.
  9. ↑ 9.0 9.1 9.2 W. Buchholz, et al. Iterated inductive definitions and subsystems of analysis: Recent proof-theoretical studies. Vol. 897. Springer, 2006.
  10. ↑ 10.0 10.1 10.2 S. Feferman, and W. Sieg. Proof theoretic equivalences between classical and constructive theories for analysis. in "Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies." Springer, Berlin, Heidelberg, 1981. 78-142.
  11. ↑ K. McAloon. Paris-Harrington incompleteness and progressions of theories. In Anil Nerode and Richard A. Shore, editors, Proceedings of the AMS-ASL summer institute held in Ithaca, N.Y., June 28–July 16, 1982, volume 42 of Proceedings of Symposia in Pure Mathematics, pages 447–460. American Mathematical Society, Providence, RI, 1985
  12. ↑ B. Afshari. Relative computability and the proof-theoretic strength of some theories. PhD thesis, University of Leeds, 2008
  13. ↑ 13.0 13.1 13.2 13.3 A. Marcone, and A. Montalbán. The Veblen functions for computability theorists. The Journal of Symbolic Logic 76.2 (2011): 575-602.
  14. ↑ B. Afshari, and M. Rathjen. Ordinal analysis and the infinite ramsey theorem. Conference on Computability in Europe. Springer, Berlin, Heidelberg, 2012.
  15. ↑ Alwe, \(\mathsf{PA}\)と周辺の順序数解析，handwritten note，2020．
  16. ↑ B. Afshari, and M. Rathjen. Reverse mathematics and well-ordering principles: A pilot study. Annals of Pure and Applied Logic 160.3 (2009): 231-237.
  17. ↑ 17.00 17.01 17.02 17.03 17.04 17.05 17.06 17.07 17.08 17.09 17.10 17.11 17.12 17.13 17.14 17.15 D. Probst. A modular ordinal analysis of metapredicative subsystems of second order arithmetic. Dissertion. Institute of Computer Science, 2017.
  18. ↑ 18.0 18.1 18.2 18.3 18.4 18.5 D. Probst. The proof-theoretic analysis of transfinitely iterated quasi least fixed points. The journal of symbolic logic 71.3 (2006): 721-746.
  19. ↑ 19.0 19.1 19.2 19.3 B. Afshari, and M. Rathjen. A note on the theory of positive induction, \(\mathsf{ID}_1^*\). Archive for Mathematical Logic 49.2 (2010): 275-281.
  20. ↑ 20.0 20.1 20.2 G. Jäger, and T. Strahm. Some theories with positive induction of ordinal strength \(\varphi\omega 0\) Journal of Symbolic Logic (1996): 818-842.
  21. ↑ 21.0 21.1 K. Schütte. Proof theory. Vol. 225. Springer Science & Business Media, 2012.
  22. ↑ 22.00 22.01 22.02 22.03 22.04 22.05 22.06 22.07 22.08 22.09 G. Jäger., R. Kahle., A. Setzer. and T. Strahm. The proof-theoretic analysis of transfinitely iterated fixed point theories. Journal of Symbolic Logic (1999): 53-67.
  23. ↑ 23.0 23.1 23.2 23.3 23.4 23.5 23.6 J. Avigad, and S. Richard. The model-theoretic ordinal analysis of theories of predicative strength. Journal of Symbolic Logic (1999): 327-349.
  24. ↑ 24.0 24.1 24.2 G. Jäger, and D. Probst. A proof-theoretic analysis of theories for stratified inductive definitions. Gentzen's Centenary. Springer, Cham, 2015. 425-454.
  25. ↑ F. Ranzi, and T Strahm. A note on the theory \(\mathsf{SID}_{<\omega}\) of stratified induction. Mathematical Logic Quarterly 60.6 (2014): 487-497.
  26. ↑ 26.00 26.01 26.02 26.03 26.04 26.05 26.06 26.07 26.08 26.09 26.10 26.11 26.12 26.13 26.14 T. Arai. Ordinal Analysis with an Introduction to Proof Theory, Springer Singapore, 2020(prearranged).
  27. ↑ 27.0 27.1 S. Feferman, Systems of predicative analysis, Jour. Symb. Logic 29(1964), 1-30.
  28. ↑ 28.0 28.1 K. Schütte, Predicative well-orderings, in: Formal systems and recursive functions, J. N. Crossley and M. Dummett (eds), North-Holland,280-303(1965).
  29. ↑ H. Friedman., M.K. McAloon. and S.G. Simpson. A finite combinatorial principle which is equivalent to the 1-consistency of predicative analysis. Studies in Logic and the Foundations of Mathematics. Vol. 109. Elsevier, 1982. 197-230.
  30. ↑ 30.0 30.1 G. Jäger. Theories for Admissible Sets: A Unifying Approach to Proof Theory (Studies in Proof Theory Lecture Notes, Vol 2). 1986.
  31. ↑ 31.0 31.1 J. Avigad. On the relationship between \(\mathsf{ATR}_0\) and \(\widehat{\mathsf{ID}}_{<\omega}\). The Journal of Symbolic Logic 61.3 (1996): 768-779.
  32. ↑ R. Kahle. Uniform limit in explicit mathematics with universes. Tech. Rep. IAM-97-002, Institut für Informatik und angewandte Mathematik, Universität Bern, 1997.
  33. ↑ 33.0 33.1 33.2 33.3 T. Strahm. First steps into metapredicativity in explicit mathematics. LONDON MATHEMATICAL SOCIETY LECTURE NOTE SERIES (1999): 383-402.
  34. ↑ 34.00 34.01 34.02 34.03 34.04 34.05 34.06 34.07 34.08 34.09 34.10 G. Jäger and T. Strahm. Fixed point theories and dependent choice. Archive for Mathematical Logic 39.7 (2000): 493-508.
  35. ↑ 35.0 35.1 35.2 35.3 35.4 35.5 35.6 T. Strahm. Autonomous fixed point progressions and fixed point transfinite recursion. Logic colloquium. Vol. 98. 2000.
  36. ↑ 36.0 36.1 36.2 36.3 36.4 36.5 36.6 36.7 36.8 G. Jäger. and T. Strahm. Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory. The Journal of Symbolic Logic 66.2 (2001): 935-958.
  37. ↑ 37.0 37.1 37.2 37.3 37.4 37.5 37.6 37.7 37.8 T. Strahm. Wellordering proofs for metapredicative Mahlo. Journal of Symbolic Logic (2002): 260-278.
  38. ↑ 38.0 38.1 C. Rüede. Metapredicative Subsystems of Analysis, Ph.D. thesis, Institut für Informatik und angewandte Mathematik, Univeristät Bern, 2000.
  39. ↑ 39.0 39.1 C. Rüede. The proof-theoretic analysis of \(\Sigma^1_1\) transfinite dependent choice. (2003).
  40. ↑ 40.0 40.1 40.2 F. Ranzi., and T. Strahm. A flexible type system for the small Veblen ordinal. Archive for mathematical logic 58.5-6 (2019): 711-751.
  41. ↑ 41.0 41.1 41.2 41.3 41.4 41.5 41.6 41.7 41.8 G. Jäger., T.Strahm. Reflections on reflections in explicit mathematics. Annals of Pure and Applied Logic 136.1-2 (2005): 116-133.
  42. ↑ 42.0 42.1 M. Rathjen, Fragments of Kripke–Platek set theory with infinity. In P. Aczel, H. Simmons, and S.S. Wainer, editors, Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, pages 251–273. Cambridge University Press, 1992.
  43. ↑ 43.00 43.01 43.02 43.03 43.04 43.05 43.06 43.07 43.08 43.09 43.10 43.11 43.12 43.13 43.14 43.15 43.16 43.17 F. Ranzi. From a flexible type system to metapredicative wellordering proofs. PhD thesis, Universität Bern, 2015.
  44. ↑ 44.0 44.1 T. Arai. Proof-theoretic strengths of weak theories for positive inductive definitions. The Journal of Symbolic Logic 83.3 (2018): 1091-1111.
  45. ↑ 45.0 45.1 45.2 45.3 M Rathjen. and A. Weiermann. Proof-theoretic investigations on Kruskal's theorem. Annals of Pure and applied Logic 60.1 (1993): 49-88.
  46. ↑ 46.00 46.01 46.02 46.03 46.04 46.05 46.06 46.07 46.08 46.09 46.10 46.11 T. Arai. Wellfoundedness Proofs by Means of Non-Monotonic Inductive Definitions I: \(\Pi^0_2\)-Operators. Journal of Symbolic Logic (2004): 830-850.
  47. ↑ 47.0 47.1 47.2 47.3 T. Arai. Proof theory for theories of ordinals—I: recursively Mahlo ordinals. Annals of Pure and applied Logic 122.1-3 (2003): 1-85.
  48. ↑ M. Rathjen. The recursively Mahlo property in second order arithmetic. Mathematical Logic Quarterly 42.1 (1996): 59-66.
  49. ↑ 49.0 49.1 49.2 T. Arai. Ordinal diagrams for recursively Mahlo universes. Arch Math Logic 39, 353–391 (2000).
  50. ↑ M. Rathjen. Proof-theoretic analysis of \(\mathsf{KPM}\). Archive for Mathematical Logic 30.5-6 (1991): 377-403.
  51. ↑ M. Rathjen. Collapsing functions based on recursively large ordinals: A well-ordering proof for KPM. Archive for Mathematical Logic 33.1 (1994): 35-55.
  52. ↑ 52.0 52.1 W. Buchholz. A note on the ordinal analysis of KPM. (1991): 1-9.
  53. ↑ Rathjen, Michael. Ordinal notations based on a weakly Mahlo cardinal. Archive for Mathematical Logic 29.4 (1990): 249-263.
  54. ↑ 54.0 54.1 54.2 54.3 54.4 54.5 T. Arai. Proof theory for theories of ordinals II: \(\Pi_3\)-reflection. Annals of Pure and Applied Logic 129.1-3 (2004): 39-92.
  55. ↑ 55.0 55.1 55.2 55.3 55.4 T. Arai. Ordinal diagrams for \(\Pi_3\)-reflection. The Journal of Symbolic Logic 65.3 (2000): 1375-1394.
  56. ↑ 56.0 56.1 56.2 56.3 M. Rathjen. Proof theory of reflection. Annals of Pure and Applied Logic 68.2 (1994): 181-224.
  57. ↑ 57.0 57.1 57.2 57.3 57.4 57.5 T. Arai. A simplified ordinal analysis of first-order reflection. arXiv preprint arXiv:1907.07611 (2019).
  58. ↑ 58.0 58.1 T. Arai. Well-foundedness proof for first-order reflection. arXiv preprint arXiv:1506.05280 (2015).
  59. ↑ 59.0 59.1 59.2 T. Arai. Iterating the recursively Mahlo operations. arXiv preprint arXiv:1005.1987 (2010).
  60. ↑ 60.0 60.1 60.2 T. Arai. Conservations of first-order reflections. The Journal of Symbolic Logic (2014): 814-825.
  61. ↑ K. Schütte. Zur Beweistheorie von \( \mathsf{KP}+\Pi_3\text{-}\mathsf{Ref}\), type–written manuscript. 1993
  62. ↑ T. Arai. Proof theory for reflecting ordinals III: \(\Pi_3\)-reflecting ordinals, handwritten note, December 1990.
  63. ↑ 63.0 63.1 63.2 63.3 63.4 63.5 63.6 63.7 T. Arai. Wellfoundedness proofs by means of non-monotonic inductive definitions II: first order operators. Annals of Pure and Applied Logic 162.2 (2010): 107-143.
  64. ↑ 64.00 64.01 64.02 64.03 64.04 64.05 64.06 64.07 64.08 64.09 T. Arai. Proof Theory for Theories of Ordinals III: \(\Pi_N\)-Reflection. Gentzen's Centenary. Springer, Cham, 2015. 357-424.
  65. ↑ 65.0 65.1 65.2 65.3 C. Duchhardt. Thinning Operators and \(\Pi_4\)-Reflection. Diss. thesis, 2008.
  66. ↑ W. Pohlers, and J.C. Stegert. Provably recursive functions of reflection. Logic, Construction, Computation, Ontos Mathematical Logic 3 (2012): 381-474.
  67. ↑ 67.0 67.1 67.2 67.3 67.4 67.5 67.6 J-C. Stegert. Ordinal proof theory of Kripke-Platek set theory augmented by strong reflection principles. Diss. Ph. D. thesis, Westfälische Wilhelms-Universität, Münster, 2011.
  68. ↑ 68.0 68.1 68.2 68.3 68.4 M. Rathjen. An ordinal analysis of stability. Archive for Mathematical Logic 44.1 (2005): 1-62.
  69. ↑ 69.0 69.1 69.2 T. Arai. An ordinal analysis of a single stable ordinal. Reserachmap. 2022.
  70. ↑ 70.0 70.1 70.2 T. Arai. Wellfoundedness proof with the maximal distinguished set. Reserachmap. 2022.
  71. ↑ 71.0 71.1 M. Rathjen. An Ordinal Representation System for \(\Pi^1_2\)-Complehension and Related Systems. (1995).
  72. ↑ 72.0 72.1 72.2 Rathjen, Michael. Recent Advances in Ordinal Analysis: \(\Pi^1_2\text{-}\mathsf{CA}\) and Related System. Bulletin of Symbolic Logic 1.4 (1995): 468-485.
  73. ↑ 73.0 73.1 73.2 73.3 M. Rathjen. An ordinal analysis of parameter free \(\Pi^1_2\)-comprehension. Archive for Mathematical Logic volume 44, 263–362(2005).
  74. ↑ 74.0 74.1 T. Arai. An Ordinal Analysis of \(\Pi_1\text{-}\mathsf{Coll}\). Arxiv. 2021.
  75. ↑ T. Arai. A Sneak Preview of Proof Theory of Ordinals (< Special Section> Infinity in Philosophy and Mathematics). Annals of the Japan Association for Philosophy of Science 20 (2012): 29-47.
  76. ↑ T. Arai. Introducing the hardline in proof theory. arXiv preprint arXiv:1104.1842 (2011).
特に記載のない限り、コミュニティのコンテンツはCC-BY-SAライセンスの下で利用可能です。
Advertisement