证明论序数:修订间差异
来自Googology Wiki
更多操作
小无编辑摘要 |
QuantumJack1(留言 | 贡献) 无编辑摘要 |
||
| (未显示2个用户的4个中间版本) | |||
| 第12行: | 第12行: | ||
=== 证明论序数表 === | === 证明论序数表 === | ||
{| class="wikitable class="article-table" border="0" cellpadding="1" cellspacing="1"" | {| class="wikitable class="article-table" border="0" cellpadding="1" cellspacing="1"" | ||
! scope="col" | | ! scope="col" |证明论序数(OCF及其他记号) | ||
!证明论序数(BMS及其他记号) | |||
! scope="col" |算术论体系 | ! scope="col" |算术论体系 | ||
! scope="col" |集合论体系 | ! scope="col" |集合论体系 | ||
! scope="col" |其他体系 | ! scope="col" |其他体系 | ||
|- | |- | ||
| | |<math>\omega</math> | ||
|(0)(1) | |||
|<math>Q</math> | |<math>Q</math> | ||
|<math>\rm KP^-</math> | |<math>\rm KP^-</math> | ||
| 第23行: | 第25行: | ||
|- | |- | ||
|<math>\omega^2</math> | |<math>\omega^2</math> | ||
|(0)(1)(1) | |||
|<math>\rm RFA</math><br><math>\rm I\Delta_0</math> | |<math>\rm RFA</math><br><math>\rm I\Delta_0</math> | ||
| | | | ||
| 第28行: | 第31行: | ||
|- | |- | ||
|<math>\omega^3</math> | |<math>\omega^3</math> | ||
|(0)(1)(1)(1) | |||
|<math>\rm RCA_0^*</math><br><math>\rm WKL_0^*</math><br><math>\rm I\Delta_0+exp</math> | |<math>\rm RCA_0^*</math><br><math>\rm WKL_0^*</math><br><math>\rm I\Delta_0+exp</math> | ||
| | | | ||
| 第33行: | 第37行: | ||
|- | |- | ||
|<math>\omega^n</math> | |<math>\omega^n</math> | ||
|(0)(1)^n | |||
|<math>{\rm I\Delta_0}+\mathcal{E}_n\text{ is total}</math> | |<math>{\rm I\Delta_0}+\mathcal{E}_n\text{ is total}</math> | ||
| | | | ||
| 第38行: | 第43行: | ||
|- | |- | ||
|<math>\omega^\omega</math> | |<math>\omega^\omega</math> | ||
|(0)(1)(2) | |||
|<math>\rm RCA_0</math><br><math>\rm WKL_0</math><br><math>\rm PRA</math><br><math>\rm RCA_0^2</math> | |<math>\rm RCA_0</math><br><math>\rm WKL_0</math><br><math>\rm PRA</math><br><math>\rm RCA_0^2</math> | ||
|<math>\rm CPRC</math><br><math>\rm KP^-+\Pi_1^{set}\ Fondation+IND</math> | |<math>\rm CPRC</math><br><math>\rm KP^-+\Pi_1^{set}\ Fondation+IND</math> | ||
| 第43行: | 第49行: | ||
|- | |- | ||
|<math>\omega^{\omega^{\omega^\omega}}</math> | |<math>\omega^{\omega^{\omega^\omega}}</math> | ||
|(0)(1)(2)(3)(4) | |||
|<math>\rm RCA_0+(\Pi_2^0)^--IND</math> | |<math>\rm RCA_0+(\Pi_2^0)^--IND</math> | ||
| | | | ||
| 第48行: | 第55行: | ||
|- | |- | ||
|<math>\omega\uparrow\uparrow(n+2)</math> | |<math>\omega\uparrow\uparrow(n+2)</math> | ||
|(0)(1)(2)...(n+2) | |||
|<math>{\rm I}\Sigma_{n+1}</math> | |<math>{\rm I}\Sigma_{n+1}</math> | ||
| | | | ||
| 第53行: | 第61行: | ||
|- | |- | ||
|<math>\varepsilon_0</math> | |<math>\varepsilon_0</math> | ||
|(0)(1,1) | |||
|<math>\rm PA</math><br><math>\rm ACA_0</math><br><math>\rm \Delta_1^1-CA_0</math><br><math>\rm \Sigma_1^1-AC_0</math> | |<math>\rm PA</math><br><math>\rm ACA_0</math><br><math>\rm \Delta_1^1-CA_0</math><br><math>\rm \Sigma_1^1-AC_0</math> | ||
|<math>\rm KP^{-\infty}</math> | |<math>\rm KP^{-\infty}</math> | ||
| 第58行: | 第67行: | ||
|- | |- | ||
|<math>\varepsilon_1</math> | |<math>\varepsilon_1</math> | ||
|(0)(1,1)(1,1) | |||
|<math>\rm ACA_0+KPHT</math> | |<math>\rm ACA_0+KPHT</math> | ||
| | | | ||
| 第63行: | 第73行: | ||
|- | |- | ||
|<math>\varepsilon_\omega</math> | |<math>\varepsilon_\omega</math> | ||
|(0)(1,1)(2) | |||
|<math>\rm ACA_0+iRT</math><br><math>{\rm RCA_0}+\forall Y\forall n\exists X({\rm TJ}(n,X,Y))</math> | |<math>\rm ACA_0+iRT</math><br><math>{\rm RCA_0}+\forall Y\forall n\exists X({\rm TJ}(n,X,Y))</math> | ||
| | | | ||
| 第68行: | 第79行: | ||
|- | |- | ||
|<math>\varepsilon_{\varepsilon_0}</math> | |<math>\varepsilon_{\varepsilon_0}</math> | ||
|(0)(1,1)(2)(3,1) | |||
|<math>\rm ACA</math><br><math>{\rm FP}_n-{\rm ACA'_0}</math><br><math>{\rm FP}_n-{\rm ACA'}</math> | |<math>\rm ACA</math><br><math>{\rm FP}_n-{\rm ACA'_0}</math><br><math>{\rm FP}_n-{\rm ACA'}</math> | ||
| | | | ||
| 第73行: | 第85行: | ||
|- | |- | ||
|<math>\zeta_0</math> | |<math>\zeta_0</math> | ||
|(0)(1,1)(2,1) | |||
|<math>{\rm ACA_0}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math><br><math>\rm ACA_0+(BR)</math><br><math>\rm p_1(ACA_0)</math> | |<math>{\rm ACA_0}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math><br><math>\rm ACA_0+(BR)</math><br><math>\rm p_1(ACA_0)</math> | ||
| | | | ||
| 第78行: | 第91行: | ||
|- | |- | ||
|<math>\varphi(2,\varepsilon_0)</math> | |<math>\varphi(2,\varepsilon_0)</math> | ||
|(0)(1,1)(2,1)(2)(3,1) | |||
|<math>{\rm ACA}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math><br><math>\rm RFN</math> | |<math>{\rm ACA}+\forall X\exists Y({\rm TJ}(\omega,X,Y))</math><br><math>\rm RFN</math> | ||
| | | | ||
| 第83行: | 第97行: | ||
|- | |- | ||
|<math>\varphi(\omega,0)</math> | |<math>\varphi(\omega,0)</math> | ||
|(0)(1,1)(2,1)(3) | |||
|<math>\rm \Delta_1^1-CR</math><br><math>\rm RCA_0^*+\Pi_1^1-CA^-</math><br><math>\rm \Sigma_1^1-DC_0</math> | |<math>\rm \Delta_1^1-CR</math><br><math>\rm RCA_0^*+\Pi_1^1-CA^-</math><br><math>\rm \Sigma_1^1-DC_0</math> | ||
| | | | ||
| 第88行: | 第103行: | ||
|- | |- | ||
|<math>\varphi(\nu+1,0)</math> | |<math>\varphi(\nu+1,0)</math> | ||
| | |||
|<math>{\rm ACA_0}+\forall X\exists Y({\rm TJ}(\omega^\nu,X,Y))</math> | |<math>{\rm ACA_0}+\forall X\exists Y({\rm TJ}(\omega^\nu,X,Y))</math> | ||
| | | | ||
| 第93行: | 第109行: | ||
|- | |- | ||
|<math>\psi(\Omega^{\varepsilon_0})</math> | |<math>\psi(\Omega^{\varepsilon_0})</math> | ||
|(0)(1,1)(2,1)(3)(4,1) | |||
|<math>\rm \Delta_1^1-CA</math><br><math>\rm \Sigma_1^1-AC</math><br><math>\rm{(\Pi_1^0-CA)}_{<\varepsilon_0}</math> | |<math>\rm \Delta_1^1-CA</math><br><math>\rm \Sigma_1^1-AC</math><br><math>\rm{(\Pi_1^0-CA)}_{<\varepsilon_0}</math> | ||
| | | | ||
| 第98行: | 第115行: | ||
|- | |- | ||
|<math>\psi(\Omega^{\psi(\Omega^\omega)})</math> | |<math>\psi(\Omega^{\psi(\Omega^\omega)})</math> | ||
|(0)(1,1)(2,1)(3)(4,1)(5,1)(6) | |||
| | | | ||
|<math>\rm PRS\ \omega</math> | |<math>\rm PRS\ \omega</math> | ||
| 第103行: | 第121行: | ||
|- | |- | ||
|<math>\Gamma_0</math> | |<math>\Gamma_0</math> | ||
|(0)(1,1)(2,1)(3,1) | |||
|<math>\rm ATR_0</math><br><math>\rm \Delta_1^1-CA+BR</math><br><math>\rm RCA_0+\Sigma_1^0-RT</math><br><math>\rm RCA_0+\Delta_1^0-RT</math><br><math>\rm RCA_0+\Sigma_1^0-det.</math><br><math>\rm RCA_0+\Delta_1^0-det.</math><br><math>\rm FP_0</math> | |<math>\rm ATR_0</math><br><math>\rm \Delta_1^1-CA+BR</math><br><math>\rm RCA_0+\Sigma_1^0-RT</math><br><math>\rm RCA_0+\Delta_1^0-RT</math><br><math>\rm RCA_0+\Sigma_1^0-det.</math><br><math>\rm RCA_0+\Delta_1^0-det.</math><br><math>\rm FP_0</math> | ||
|<math>\rm KPi^-</math><br><math>\rm CZF^-+INAC</math> | |<math>\rm KPi^-</math><br><math>\rm CZF^-+INAC</math> | ||
| 第108行: | 第127行: | ||
|- | |- | ||
|<math>\varphi(1,0,\omega^\omega)</math> | |<math>\varphi(1,0,\omega^\omega)</math> | ||
|(0)(1,1)(2,1)(3,1)(2)(3) | |||
| | | | ||
|<math>\rm KPl_0+(\Sigma_1-I_\omega)</math> | |<math>\rm KPl_0+(\Sigma_1-I_\omega)</math> | ||
| 第113行: | 第133行: | ||
|- | |- | ||
|<math>\varphi(1,0,\varepsilon_0)</math> | |<math>\varphi(1,0,\varepsilon_0)</math> | ||
|(0)(1,1)(2,1)(3,1)(2)(3,1) | |||
|<math>\rm ATR</math> | |<math>\rm ATR</math> | ||
| | | | ||
| 第118行: | 第139行: | ||
|- | |- | ||
|<math>\psi(\Omega^{\Omega+1})</math> | |<math>\psi(\Omega^{\Omega+1})</math> | ||
|(0)(1,1)(2,1)(3,1)(2,1) | |||
|<math>{\rm RCA_0}+\forall X\exists M(X\in M\land M\vDash_\omega{\rm ATR_0})</math> | |<math>{\rm RCA_0}+\forall X\exists M(X\in M\land M\vDash_\omega{\rm ATR_0})</math> | ||
| | | | ||
| 第123行: | 第145行: | ||
|- | |- | ||
|<math>\psi(\Omega^{\Omega+\omega})</math> | |<math>\psi(\Omega^{\Omega+\omega})</math> | ||
|(0)(1,1)(2,1)(3,1)(2,1)(3) | |||
|<math>\rm ATR_0+\Sigma_1^1-DC</math> | |<math>\rm ATR_0+\Sigma_1^1-DC</math> | ||
| | | | ||
| 第128行: | 第151行: | ||
|- | |- | ||
|<math>\psi(\Omega^{\Omega+\varepsilon_0})</math> | |<math>\psi(\Omega^{\Omega+\varepsilon_0})</math> | ||
|(0)(1,1)(2,1)(3,1)(2,1)(3)(4,1) | |||
|<math>\rm ATR+\Sigma_1^1-DC</math> | |<math>\rm ATR+\Sigma_1^1-DC</math> | ||
| | | | ||
| 第133行: | 第157行: | ||
|- | |- | ||
|<math>\psi(\Omega^{\Omega+\Gamma_0})</math> | |<math>\psi(\Omega^{\Omega+\Gamma_0})</math> | ||
|(0)(1,1)(2,1)(3,1)(2,1)(3)(4,1)(5,1)(6,1) | |||
| | | | ||
| | | | ||
| 第138行: | 第163行: | ||
|- | |- | ||
|<math>\varphi(2,0,0)</math> | |<math>\varphi(2,0,0)</math> | ||
|(0)(1,1)(2,1)(3,1)(2,1)(3,1) | |||
|<math>\rm FTR_0</math> | |<math>\rm FTR_0</math> | ||
|<math>\rm KPh^-</math> | |<math>\rm KPh^-</math> | ||
| 第143行: | 第169行: | ||
|- | |- | ||
|<math>\varphi(2,0,\varepsilon_0)</math> | |<math>\varphi(2,0,\varepsilon_0)</math> | ||
|(0)(1,1)(2,1)(3,1)(2,1)(3,1)(2)(3,1) | |||
|<math>\rm FTR</math> | |<math>\rm FTR</math> | ||
| | | | ||
| 第148行: | 第175行: | ||
|- | |- | ||
|<math>\varphi(2,\varepsilon_0,0)</math> | |<math>\varphi(2,\varepsilon_0,0)</math> | ||
|(0)(1,1)(2,1)(3,1)(2,1)(3,1)(2,1)(3)(4,1) | |||
| | | | ||
|<math>\rm KPh^0+(F-I_\omega)</math> | |<math>\rm KPh^0+(F-I_\omega)</math> | ||
| 第153行: | 第181行: | ||
|- | |- | ||
|<math>\psi(\Omega^{\Omega\omega})</math> | |<math>\psi(\Omega^{\Omega\omega})</math> | ||
|(0)(1,1)(2,1)(3,1)(3) | |||
| | | | ||
|<math>\rm KPM^-</math> | |<math>\rm KPM^-</math> | ||
| 第158行: | 第187行: | ||
|- | |- | ||
|<math>\varphi(\varepsilon_0,0,0)</math> | |<math>\varphi(\varepsilon_0,0,0)</math> | ||
|(0)(1,1)(2,1)(3,1)(3)(4,1) | |||
|<math>\rm \Sigma_1^1-TDC</math> | |<math>\rm \Sigma_1^1-TDC</math> | ||
| | | | ||
| 第163行: | 第193行: | ||
|- | |- | ||
|<math>\varphi(1,0,0,0)</math> | |<math>\varphi(1,0,0,0)</math> | ||
|(0)(1,1)(2,1)(3,1)(3,1) | |||
|<math>\rm p_1(\Sigma_1^1-TDC_0)</math> | |<math>\rm p_1(\Sigma_1^1-TDC_0)</math> | ||
| | | | ||
| 第168行: | 第199行: | ||
|- | |- | ||
|<math>\psi(\Omega^{\Omega^\omega})</math> | |<math>\psi(\Omega^{\Omega^\omega})</math> | ||
|(0)(1,1)(2,1)(3,1)(4) | |||
|<math>\rm RCA_0^*+\Pi_1^1-CA^-</math><br><math>\rm p_3(ACA_0)</math> | |<math>\rm RCA_0^*+\Pi_1^1-CA^-</math><br><math>\rm p_3(ACA_0)</math> | ||
| | | | ||
| 第173行: | 第205行: | ||
|- | |- | ||
|<math>\vartheta(\Omega^\Omega)</math> | |<math>\vartheta(\Omega^\Omega)</math> | ||
|(0)(1,1)(2,1)(3,1)(4,1) | |||
|<math>\rm p_1(p_3(ACA_0))</math> | |<math>\rm p_1(p_3(ACA_0))</math> | ||
| | | | ||
| 第178行: | 第211行: | ||
|- | |- | ||
|<math>\theta_{(n+2)(\Omega^\omega)}0</math> | |<math>\theta_{(n+2)(\Omega^\omega)}0</math> | ||
| | |||
|<math>{\rm ACA_0}+\Pi_{n+2}^1-{\rm BI}</math><br><math>\Pi_{n+1}^1-{\rm RFN}</math><br><math>(\Pi_{n+2}^1-{\rm BI})_0</math><br><math>(\Pi_{n+2}^1-{\rm BI})_0^-</math> | |<math>{\rm ACA_0}+\Pi_{n+2}^1-{\rm BI}</math><br><math>\Pi_{n+1}^1-{\rm RFN}</math><br><math>(\Pi_{n+2}^1-{\rm BI})_0</math><br><math>(\Pi_{n+2}^1-{\rm BI})_0^-</math> | ||
|<math>{\rm KP}\omega^-+\Pi_{n+2}^{\rm set}-{\rm Foundation}</math> | |<math>{\rm KP}\omega^-+\Pi_{n+2}^{\rm set}-{\rm Foundation}</math> | ||
| 第183行: | 第217行: | ||
|- | |- | ||
|<math>\theta_{(n+2)(\Omega^\omega)}0</math> | |<math>\theta_{(n+2)(\Omega^\omega)}0</math> | ||
| | |||
|<math>{\rm ACA}+\Pi_{n+2}^1-{\rm BI}</math><br><math>(\Pi_{n+2}^1-{\rm BI})^-</math> | |<math>{\rm ACA}+\Pi_{n+2}^1-{\rm BI}</math><br><math>(\Pi_{n+2}^1-{\rm BI})^-</math> | ||
|<math>{\rm KP}\omega^-+{\rm IND}+\Pi_{n+2}^{\rm set}-{\rm Foundation}</math> | |<math>{\rm KP}\omega^-+{\rm IND}+\Pi_{n+2}^{\rm set}-{\rm Foundation}</math> | ||
| 第188行: | 第223行: | ||
|- | |- | ||
|<math>\psi(\psi_1(0))</math> | |<math>\psi(\psi_1(0))</math> | ||
|(0)(1,1)(2,2) | |||
|<math>\rm ACA+BI</math><br><math>\rm ACA_0+\Pi_1^1-CA^-</math><br><math>\rm \Pi_1^0-FXP_0</math> | |<math>\rm ACA+BI</math><br><math>\rm ACA_0+\Pi_1^1-CA^-</math><br><math>\rm \Pi_1^0-FXP_0</math> | ||
|<math>\rm KP</math><br><math>\rm KP+\Pi_2^{set}-Reflection</math><br><math>\rm KP+(BI^*)</math><br><math>\rm KP+(ATR_0^*)</math><br><math>\rm CZF</math><br><math>{\rm KP}\omega_2\upharpoonright+\Delta_1-{\rm CA}+s\Pi_1^1-{\rm ref}</math> | |<math>\rm KP</math><br><math>\rm KP+\Pi_2^{set}-Reflection</math><br><math>\rm KP+(BI^*)</math><br><math>\rm KP+(ATR_0^*)</math><br><math>\rm CZF</math><br><math>{\rm KP}\omega_2\upharpoonright+\Delta_1-{\rm CA}+s\Pi_1^1-{\rm ref}</math> | ||
| 第193行: | 第229行: | ||
|- | |- | ||
|<math>\psi(\Omega_2)</math> | |<math>\psi(\Omega_2)</math> | ||
|(0)(1,1)(2,2)(3,2) | |||
|<math>{\rm RCA_0}+\forall X\exists M(X\in M\land M\vDash_\omega{\rm ACA+BI})</math> | |<math>{\rm RCA_0}+\forall X\exists M(X\in M\land M\vDash_\omega{\rm ACA+BI})</math> | ||
| | | | ||
| 第198行: | 第235行: | ||
|- | |- | ||
|<math>\psi(\Omega_2^{\Omega_2})</math> | |<math>\psi(\Omega_2^{\Omega_2})</math> | ||
|(0)(1,1)(2,2)(3,2)(4,2) | |||
|<math>\rm ATR_0^\bullet</math><br><math>\rm FP_0^\bullet</math><br><math>\rm \Sigma_1^1-DC_0^\bullet+(SUB^\bullet)</math><br><math>\rm \Sigma_1^1-AC_0^\bullet+(SUB^\bullet)</math> | |<math>\rm ATR_0^\bullet</math><br><math>\rm FP_0^\bullet</math><br><math>\rm \Sigma_1^1-DC_0^\bullet+(SUB^\bullet)</math><br><math>\rm \Sigma_1^1-AC_0^\bullet+(SUB^\bullet)</math> | ||
| | | | ||
| 第203行: | 第241行: | ||
|- | |- | ||
|<math>\psi(\psi_2(0))</math> | |<math>\psi(\psi_2(0))</math> | ||
|(0)(1,1)(2,2)(3,3) | |||
| | | | ||
|<math>\rm KP+\exists\omega_1^{CK}</math> | |<math>\rm KP+\exists\omega_1^{CK}</math> | ||
| 第208行: | 第247行: | ||
|- | |- | ||
|<math>\psi(\Omega_\omega)</math> | |<math>\psi(\Omega_\omega)</math> | ||
|(0)(1,1,1) | |||
|<math>\rm \Pi_1^1-CA_0</math><br><math>\rm \Delta_2^1-CA_0</math><br><math>\rm RCA_0+\Sigma_1^0\land\Pi_1^0-det.</math><br><math>\rm RCA_0+\Delta_2^0-RT</math> | |<math>\rm \Pi_1^1-CA_0</math><br><math>\rm \Delta_2^1-CA_0</math><br><math>\rm RCA_0+\Sigma_1^0\land\Pi_1^0-det.</math><br><math>\rm RCA_0+\Delta_2^0-RT</math> | ||
|<math>{\rm KPl}^r</math><br><math>{\rm KPi}^r</math><br><math>{\rm KP}\beta^r</math> | |<math>{\rm KPl}^r</math><br><math>{\rm KPi}^r</math><br><math>{\rm KP}\beta^r</math> | ||
| 第213行: | 第253行: | ||
|- | |- | ||
|<math>\psi(\Omega_\omega\cdot\omega^\omega)</math> | |<math>\psi(\Omega_\omega\cdot\omega^\omega)</math> | ||
|(0)(1,1,1)(2)(3) | |||
|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-IND</math> | |<math>\rm \Pi_1^1-CA_0+\Pi_2^1-IND</math> | ||
| | | | ||
| 第218行: | 第259行: | ||
|- | |- | ||
|<math>\psi(\Omega_\omega\cdot\varepsilon_0)</math> | |<math>\psi(\Omega_\omega\cdot\varepsilon_0)</math> | ||
|(0)(1,1,1)(2)(3,1) | |||
|<math>\rm \Pi_1^1-CA</math> | |<math>\rm \Pi_1^1-CA</math> | ||
|<math>\rm W-KPl</math> | |<math>\rm W-KPl</math> | ||
| 第223行: | 第265行: | ||
|- | |- | ||
|<math>\psi(\Omega_\omega\cdot\Omega)</math> | |<math>\psi(\Omega_\omega\cdot\Omega)</math> | ||
|(0)(1,1,1)(2,1) | |||
|<math>\rm \Pi_1^1-CA+BR</math> | |<math>\rm \Pi_1^1-CA+BR</math> | ||
| | | | ||
| 第228行: | 第271行: | ||
|- | |- | ||
|<math>\psi(\Omega_\omega^\omega)</math> | |<math>\psi(\Omega_\omega^\omega)</math> | ||
|(0)(1,1,1)(2,1)(3) | |||
|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-BI</math> | |<math>\rm \Pi_1^1-CA_0+\Pi_2^1-BI</math> | ||
| | | | ||
| 第233行: | 第277行: | ||
|- | |- | ||
|<math>\psi(\Omega_\omega^{\omega^\omega})</math> | |<math>\psi(\Omega_\omega^{\omega^\omega})</math> | ||
|(0)(1,1,1)(2,1)(3)(4) | |||
|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-BI+\Pi_3^1-IND</math> | |<math>\rm \Pi_1^1-CA_0+\Pi_2^1-BI+\Pi_3^1-IND</math> | ||
| | | | ||
| 第238行: | 第283行: | ||
|- | |- | ||
|<math>\psi(\psi_\omega(0))</math> | |<math>\psi(\psi_\omega(0))</math> | ||
|(0)(1,1,1)(2,1)(3,2) | |||
|<math>\rm \Pi_1^1-CA+BI</math> | |<math>\rm \Pi_1^1-CA+BI</math> | ||
|<math>\rm KPl</math> | |<math>\rm KPl</math> | ||
| 第243行: | 第289行: | ||
|- | |- | ||
|<math>\psi(\Omega_{\omega^\omega})</math> | |<math>\psi(\Omega_{\omega^\omega})</math> | ||
|(0)(1,1,1)(2,1,1)(3) | |||
|<math>\rm \Delta_2^1-CR</math><br><math>\rm (\Pi_1^1-CA_{<\omega^\omega})</math> | |<math>\rm \Delta_2^1-CR</math><br><math>\rm (\Pi_1^1-CA_{<\omega^\omega})</math> | ||
|<math>{\rm KPl}_{\omega^\omega}^r</math> | |<math>{\rm KPl}_{\omega^\omega}^r</math> | ||
| 第248行: | 第295行: | ||
|- | |- | ||
|<math>\psi(\Omega_{\varepsilon_0})</math> | |<math>\psi(\Omega_{\varepsilon_0})</math> | ||
|(0)(1,1,1)(2,1,1)(3)(4,1) | |||
|<math>\rm \Delta_2^1-CA</math><br><math>\rm \Sigma_2^1-AC</math><br><math>\rm (\Pi_1^1-CA_{<\varepsilon_0})</math> | |<math>\rm \Delta_2^1-CA</math><br><math>\rm \Sigma_2^1-AC</math><br><math>\rm (\Pi_1^1-CA_{<\varepsilon_0})</math> | ||
|<math>{\rm KPl}_{\varepsilon_0}^r</math><br><math>\rm W-KPi</math><br><math>{\rm W-KP}\beta</math> | |<math>{\rm KPl}_{\varepsilon_0}^r</math><br><math>\rm W-KPi</math><br><math>{\rm W-KP}\beta</math> | ||
| 第253行: | 第301行: | ||
|- | |- | ||
|<math>\psi(\Omega_{\nu\cdot\omega})</math> | |<math>\psi(\Omega_{\nu\cdot\omega})</math> | ||
| | |||
|<math>\rm (\Pi_1^1-CA_\nu^+)_0</math> | |<math>\rm (\Pi_1^1-CA_\nu^+)_0</math> | ||
|<math>{\rm KPl}_{\nu+}^r</math> | |<math>{\rm KPl}_{\nu+}^r</math> | ||
| 第258行: | 第307行: | ||
|- | |- | ||
|<math>\psi(\Omega_\gamma\cdot\omega)</math> | |<math>\psi(\Omega_\gamma\cdot\omega)</math> | ||
| | |||
|<math>\rm (\Pi_1^1-CA_{\gamma-})_0</math> | |<math>\rm (\Pi_1^1-CA_{\gamma-})_0</math> | ||
|<math>{\rm KPl}_\gamma^r</math> | |<math>{\rm KPl}_\gamma^r</math> | ||
| 第263行: | 第313行: | ||
|- | |- | ||
|<math>\psi(\Omega_{\nu\cdot\omega}\cdot\varepsilon_0))</math> | |<math>\psi(\Omega_{\nu\cdot\omega}\cdot\varepsilon_0))</math> | ||
| | |||
|<math>\rm \Pi_1^1-CA_\nu^+</math> | |<math>\rm \Pi_1^1-CA_\nu^+</math> | ||
|<math>\rm W-KPl_{\nu+}</math> | |<math>\rm W-KPl_{\nu+}</math> | ||
| 第268行: | 第319行: | ||
|- | |- | ||
|<math>\psi(\Omega_\gamma\cdot\varepsilon_0)</math> | |<math>\psi(\Omega_\gamma\cdot\varepsilon_0)</math> | ||
| | |||
|<math>\rm (\Pi_1^1-CA_\gamma)</math><br><math>\rm \Pi_1^1-CA_{\gamma-}</math> | |<math>\rm (\Pi_1^1-CA_\gamma)</math><br><math>\rm \Pi_1^1-CA_{\gamma-}</math> | ||
|<math>\rm W-KPl_\gamma</math> | |<math>\rm W-KPl_\gamma</math> | ||
| 第273行: | 第325行: | ||
|- | |- | ||
|<math>\psi(\Omega_{\nu\cdot\omega}\cdot\Omega))</math> | |<math>\psi(\Omega_{\nu\cdot\omega}\cdot\Omega))</math> | ||
| | |||
|<math>\rm \Pi_1^1-CA_\nu^++BR</math> | |<math>\rm \Pi_1^1-CA_\nu^++BR</math> | ||
| | | | ||
| 第278行: | 第331行: | ||
|- | |- | ||
|<math>\psi(\Omega_\gamma\cdot\Omega)</math> | |<math>\psi(\Omega_\gamma\cdot\Omega)</math> | ||
| | |||
|<math>\rm \Pi_1^1-CA_{\gamma-}+BR</math> | |<math>\rm \Pi_1^1-CA_{\gamma-}+BR</math> | ||
| | | | ||
| 第283行: | 第337行: | ||
|- | |- | ||
|<math>\psi(\Omega_{\omega^\gamma})</math> | |<math>\psi(\Omega_{\omega^\gamma})</math> | ||
| | |||
|<math>\rm (\Pi_1^1-CA_{\omega\gamma})_0</math><br><math>\rm (\Pi_1^1-CA_{<\omega\gamma})</math><br><math>\rm (\Pi_1^1-CA_{<\omega\gamma})+BI</math> | |<math>\rm (\Pi_1^1-CA_{\omega\gamma})_0</math><br><math>\rm (\Pi_1^1-CA_{<\omega\gamma})</math><br><math>\rm (\Pi_1^1-CA_{<\omega\gamma})+BI</math> | ||
| | | | ||
| 第288行: | 第343行: | ||
|- | |- | ||
|<math>\psi(\psi_\nu(0))</math> | |<math>\psi(\psi_\nu(0))</math> | ||
| | |||
|<math>\rm (\Pi_1^1-CA_\nu)_0</math> | |<math>\rm (\Pi_1^1-CA_\nu)_0</math> | ||
|<math>\rm KPl_\nu</math> | |<math>\rm KPl_\nu</math> | ||
| 第293行: | 第349行: | ||
|- | |- | ||
|<math>\psi(\psi_\nu(\varepsilon_0))</math> | |<math>\psi(\psi_\nu(\varepsilon_0))</math> | ||
| | |||
|<math>\rm \Pi_1^1-CA_\nu</math> | |<math>\rm \Pi_1^1-CA_\nu</math> | ||
| | | | ||
| 第298行: | 第355行: | ||
|- | |- | ||
|<math>\psi(\psi_\nu(\Omega))</math> | |<math>\psi(\psi_\nu(\Omega))</math> | ||
| | |||
|<math>\rm \Pi_1^1-CA_\nu+BR</math> | |<math>\rm \Pi_1^1-CA_\nu+BR</math> | ||
| | | | ||
| 第303行: | 第361行: | ||
|- | |- | ||
|<math>\psi(\psi_\nu(\psi_\nu(0)))</math> | |<math>\psi(\psi_\nu(\psi_\nu(0)))</math> | ||
| | |||
| | | | ||
| | | | ||
| 第308行: | 第367行: | ||
|- | |- | ||
|<math>\psi(\psi_{\nu+1}(0))</math> | |<math>\psi(\psi_{\nu+1}(0))</math> | ||
| | |||
|<math>\rm \Pi_1^1-CA_\nu+BI</math> | |<math>\rm \Pi_1^1-CA_\nu+BI</math> | ||
|<math>\rm KPl_{\nu+1}</math> | |<math>\rm KPl_{\nu+1}</math> | ||
| 第313行: | 第373行: | ||
|- | |- | ||
|<math>\psi(\psi_{\nu\cdot\omega}(0))</math> | |<math>\psi(\psi_{\nu\cdot\omega}(0))</math> | ||
| | |||
|<math>\rm \Pi_1^1-CA_\nu^++BI</math> | |<math>\rm \Pi_1^1-CA_\nu^++BI</math> | ||
|<math>\rm KPl_{\nu+}</math> | |<math>\rm KPl_{\nu+}</math> | ||
| 第318行: | 第379行: | ||
|- | |- | ||
|<math>\psi(\psi_\gamma(0))</math> | |<math>\psi(\psi_\gamma(0))</math> | ||
| | |||
|<math>\rm (\Pi_1^1-CA_\gamma)_0</math><br><math>\rm (\Pi_1^1-CA_\gamma)+BI</math><br><math>\rm \Pi_1^1-CA_{\gamma-}+BI</math> | |<math>\rm (\Pi_1^1-CA_\gamma)_0</math><br><math>\rm (\Pi_1^1-CA_\gamma)+BI</math><br><math>\rm \Pi_1^1-CA_{\gamma-}+BI</math> | ||
|<math>\rm KPl_\gamma</math> | |<math>\rm KPl_\gamma</math> | ||
| 第323行: | 第385行: | ||
|- | |- | ||
|<math>\psi(\psi_\Omega(0))</math> | |<math>\psi(\psi_\Omega(0))</math> | ||
|(0)(1,1,1)(2,1,1)(3,1) | |||
| | | | ||
|<math>\rm KPl^*</math><br><math>{\rm KPl}_\Omega^r</math> | |<math>\rm KPl^*</math><br><math>{\rm KPl}_\Omega^r</math> | ||
| 第328行: | 第391行: | ||
|- | |- | ||
|<math>\psi_{\Omega_1}(\psi_I(0))</math> | |<math>\psi_{\Omega_1}(\psi_I(0))</math> | ||
|(0)(1,1,1)(2,1,1)(3,1)(2) | |||
|<math>\rm \Pi_1^1-TR_0</math><br><math>\rm \Pi_1^1-TR_0+\Delta_2^1-CA_0</math><br><math>\rm \Delta_2^1-CA+BI(impl\ \Sigma_2^1)</math><br><math>\rm \Delta_2^1-CA+BR(impl\ \Sigma_2^1)</math><br><math>\rm RCA_0+\Delta_2^0-det.</math><br><math>\rm RCA_0+\Delta_1^1-RT</math> | |<math>\rm \Pi_1^1-TR_0</math><br><math>\rm \Pi_1^1-TR_0+\Delta_2^1-CA_0</math><br><math>\rm \Delta_2^1-CA+BI(impl\ \Sigma_2^1)</math><br><math>\rm \Delta_2^1-CA+BR(impl\ \Sigma_2^1)</math><br><math>\rm RCA_0+\Delta_2^0-det.</math><br><math>\rm RCA_0+\Delta_1^1-RT</math> | ||
|<math>{\rm Aut-KPl}^r</math><br><math>{\rm Aut-KPl}^r+{\rm KPi}^r</math><br><math>\rm KPi^\omega+FOUNDR(impl-\Sigma)</math><br><math>\rm KPi^\omega+FOUND(impl-\Sigma)</math> | |<math>{\rm Aut-KPl}^r</math><br><math>{\rm Aut-KPl}^r+{\rm KPi}^r</math><br><math>\rm KPi^\omega+FOUNDR(impl-\Sigma)</math><br><math>\rm KPi^\omega+FOUND(impl-\Sigma)</math> | ||
| 第333行: | 第397行: | ||
|- | |- | ||
|<math>\psi_{\Omega_1}(\psi_I(0)\cdot\varepsilon_0)</math> | |<math>\psi_{\Omega_1}(\psi_I(0)\cdot\varepsilon_0)</math> | ||
|(0)(1,1,1)(2,1,1)(3,1)(2)(3,1) | |||
|<math>\rm \Pi_1^1-TR</math> | |<math>\rm \Pi_1^1-TR</math> | ||
|<math>\rm W-Aut-KPl</math> | |<math>\rm W-Aut-KPl</math> | ||
| 第338行: | 第403行: | ||
|- | |- | ||
|<math>\psi_{\Omega_1}(\psi_{\Omega_{\psi_I(0)+1}}(0))</math> | |<math>\psi_{\Omega_1}(\psi_{\Omega_{\psi_I(0)+1}}(0))</math> | ||
|(0)(1,1,1)(2,1,1)(3,1)(2,1)(3,2) | |||
|<math>\rm \Pi_1^1-TR+BI</math> | |<math>\rm \Pi_1^1-TR+BI</math> | ||
|<math>\rm Aut-KPl</math> | |<math>\rm Aut-KPl</math> | ||
| 第343行: | 第409行: | ||
|- | |- | ||
|<math>\psi_{\Omega_1}(\psi_I(I^\omega))</math> | |<math>\psi_{\Omega_1}(\psi_I(I^\omega))</math> | ||
|(0)(1,1,1)(2,1,1)(3,1)(3) | |||
|<math>\rm \Delta_2^1-TR_0</math><br><math>\rm \Sigma_2^1-TRDC_0</math><br><math>\rm \Delta_2^1-CA_0+\Sigma_2^1-BI</math> | |<math>\rm \Delta_2^1-TR_0</math><br><math>\rm \Sigma_2^1-TRDC_0</math><br><math>\rm \Delta_2^1-CA_0+\Sigma_2^1-BI</math> | ||
| | | | ||
| 第348行: | 第415行: | ||
|- | |- | ||
|<math>\psi_{\Omega_1}(\psi_I(I^{\varepsilon_0}))</math> | |<math>\psi_{\Omega_1}(\psi_I(I^{\varepsilon_0}))</math> | ||
|(0)(1,1,1)(2,1,1)(3,1)(3)(4,1) | |||
|<math>\rm \Delta_2^1-TR</math><br><math>\rm \Sigma_2^1-TRDC</math><br><math>\rm \Delta_2^1-CA+\Sigma_2^1-BI</math> | |<math>\rm \Delta_2^1-TR</math><br><math>\rm \Sigma_2^1-TRDC</math><br><math>\rm \Delta_2^1-CA+\Sigma_2^1-BI</math> | ||
| | | | ||
| 第353行: | 第421行: | ||
|- | |- | ||
|<math>\psi_{\Omega_1}(\varepsilon_{I+1})</math> | |<math>\psi_{\Omega_1}(\varepsilon_{I+1})</math> | ||
|(0)(1,1,1)(2,1,1)(3,1)(4,2) | |||
|<math>\rm \Delta_2^1-CA+BI</math><br><math>\rm \Sigma_2^1-AC+BI</math> | |<math>\rm \Delta_2^1-CA+BI</math><br><math>\rm \Sigma_2^1-AC+BI</math> | ||
|<math>\rm KPi</math><br><math>{\rm KP}\beta</math><br><math>\rm CZF+REA</math> | |<math>\rm KPi</math><br><math>{\rm KP}\beta</math><br><math>\rm CZF+REA</math> | ||
| 第358行: | 第427行: | ||
|- | |- | ||
|<math>\psi_{\Omega_1}(\Omega_{I+\omega})</math> | |<math>\psi_{\Omega_1}(\Omega_{I+\omega})</math> | ||
|(0)(1,1,1)(2,1,1)(3,1)(4,2,1) | |||
| | | | ||
|<math>\rm KPi^+</math> | |<math>\rm KPi^+</math> | ||
| 第363行: | 第433行: | ||
|- | |- | ||
|<math>\psi_{\Omega_1}(\varepsilon_{M+1})</math> | |<math>\psi_{\Omega_1}(\varepsilon_{M+1})</math> | ||
|(0)(1,1,1)(2,1,1)(3,1,1)(3,1)(4,2) | |||
|<math>\rm \Delta_2^1-CA+BI+(M)</math> | |<math>\rm \Delta_2^1-CA+BI+(M)</math> | ||
|<math>\rm KPM</math><br><math>\rm CZFM</math> | |<math>\rm KPM</math><br><math>\rm CZFM</math> | ||
| 第368行: | 第439行: | ||
|- | |- | ||
|<math>\psi_{\Omega_1}(\Omega_{M+\omega})</math> | |<math>\psi_{\Omega_1}(\Omega_{M+\omega})</math> | ||
|(0)(1,1,1)(2,1,1)(3,1,1)(3,1)(4,2,1) | |||
| | | | ||
|<math>\rm KPM^+</math> | |<math>\rm KPM^+</math> | ||
| 第373行: | 第445行: | ||
|- | |- | ||
|<math>\Psi_{\Omega_1}^0(\varepsilon_{K+1})</math> | |<math>\Psi_{\Omega_1}^0(\varepsilon_{K+1})</math> | ||
|(0)(1,1,1)(2,1,1)(3,1,1)(4,1)(5,2) | |||
|<math>{\rm ACA+BI}+\Pi_4^1-\beta\text{-model-Reflection}</math> | |<math>{\rm ACA+BI}+\Pi_4^1-\beta\text{-model-Reflection}</math> | ||
|<math>{\rm KP}+\Pi_3^{\rm set}\text{-Reflection}</math> | |<math>{\rm KP}+\Pi_3^{\rm set}\text{-Reflection}</math> | ||
| 第378行: | 第451行: | ||
|- | |- | ||
|<math>\Psi_\mathbb{X}^{\varepsilon_{\xi_n+1}}</math> | |<math>\Psi_\mathbb{X}^{\varepsilon_{\xi_n+1}}</math> | ||
|(0)(1,1,1)(2,1,1)(3,1,1)(4,1,1)(5,1)(6,2) | |||
|<math>{\rm ACA+BI}+\Pi_{n+5}^1-\beta\text{-model-Reflection}</math> | |<math>{\rm ACA+BI}+\Pi_{n+5}^1-\beta\text{-model-Reflection}</math> | ||
|<math>{\rm KP}+\Pi_{n+4}^{\rm set}\text{-Reflection}</math> | |<math>{\rm KP}+\Pi_{n+4}^{\rm set}\text{-Reflection}</math> | ||
| 第383行: | 第457行: | ||
|- | |- | ||
|<math>\Psi_\mathbb{X}^{\varepsilon_{\Xi+1}}</math> | |<math>\Psi_\mathbb{X}^{\varepsilon_{\Xi+1}}</math> | ||
|(0)(1,1,1)(2,2) | |||
|<math>{\rm ACA+BI}-\beta\text{-model-Reflection}</math> | |<math>{\rm ACA+BI}-\beta\text{-model-Reflection}</math> | ||
|<math>{\rm KP}+\Pi_\omega^{\rm set}\text{-Reflection}</math> | |<math>{\rm KP}+\Pi_\omega^{\rm set}\text{-Reflection}</math> | ||
| 第388行: | 第463行: | ||
|- | |- | ||
|<math>\Psi_\mathbb{H}^{\varepsilon_{\Upsilon+1}}</math> | |<math>\Psi_\mathbb{H}^{\varepsilon_{\Upsilon+1}}</math> | ||
|(0)(1,1,1)(2,2)(3,2)(4,1)(2) | |||
| | | | ||
|<math>{\rm KPi}+\forall\alpha\exists\kappa(L_\kappa\prec_1L_{\kappa+\alpha})</math> | |<math>{\rm KPi}+\forall\alpha\exists\kappa(L_\kappa\prec_1L_{\kappa+\alpha})</math> | ||
| 第393行: | 第469行: | ||
|- | |- | ||
|<math>\psi(\Omega_{\mathbb{S}+\omega})</math> | |<math>\psi(\Omega_{\mathbb{S}+\omega})</math> | ||
| | |||
|<math>\rm \Pi_1^1-CA_0+\Pi_2^1-CA^-</math> | |<math>\rm \Pi_1^1-CA_0+\Pi_2^1-CA^-</math> | ||
|<math>{\rm KPl}^r+\exists M(\text{Trans}(M)\land M\prec_1 V)</math> | |<math>{\rm KPl}^r+\exists M(\text{Trans}(M)\land M\prec_1 V)</math> | ||
| 第398行: | 第475行: | ||
|- | |- | ||
|<math>\Psi_\mathbb{K}^{\varepsilon_{I+1}}</math> | |<math>\Psi_\mathbb{K}^{\varepsilon_{I+1}}</math> | ||
| | |||
|<math>\rm \Delta_2^1-CA+BI+\Pi_2^1-CA^-</math> | |<math>\rm \Delta_2^1-CA+BI+\Pi_2^1-CA^-</math> | ||
|<math>{\rm KPi}+\exists M(\text{Trans}(M)\land M\prec_1 V)</math> | |<math>{\rm KPi}+\exists M(\text{Trans}(M)\land M\prec_1 V)</math> | ||
| 第403行: | 第481行: | ||
|- | |- | ||
|<math>\mathcal{I}_\omega\cap\omega_1^{\rm CK}</math> | |<math>\mathcal{I}_\omega\cap\omega_1^{\rm CK}</math> | ||
|(0)(1,1,1,1)? | |||
|<math>\rm \Pi_2^1-CA_0</math><br><math>\rm \Delta_3^1-CA_0</math> | |<math>\rm \Pi_2^1-CA_0</math><br><math>\rm \Delta_3^1-CA_0</math> | ||
| | | | ||
| 第408行: | 第487行: | ||
|- | |- | ||
|<math>\mathcal{I}_{\omega+1}\cap\omega_1^{\rm CK}</math> | |<math>\mathcal{I}_{\omega+1}\cap\omega_1^{\rm CK}</math> | ||
|(0)(1,1,1,1)(2,1,1)(3,2,2)? | |||
|<math>\rm \Pi_2^1-CA+BI</math> | |<math>\rm \Pi_2^1-CA+BI</math> | ||
|<math>\rm KP+\Sigma_1^{set}-Separation</math><br><math>{\rm KPi}+\forall\alpha\exists\beta(\beta>\alpha)(\beta\text{ stable})</math> | |<math>\rm KP+\Sigma_1^{set}-Separation</math><br><math>{\rm KPi}+\forall\alpha\exists\beta(\beta>\alpha)(\beta\text{ stable})</math> | ||
| 第413行: | 第493行: | ||
|- | |- | ||
|<math>\mathcal{I}_{\varepsilon_0}\cap\omega_1^{\rm CK}</math> | |<math>\mathcal{I}_{\varepsilon_0}\cap\omega_1^{\rm CK}</math> | ||
| | |||
|<math>\rm \Delta_3^1-CA</math><br><math>\rm \Sigma_3^1-AC</math> | |<math>\rm \Delta_3^1-CA</math><br><math>\rm \Sigma_3^1-AC</math> | ||
| | | | ||
| 第418行: | 第499行: | ||
|- | |- | ||
|<math>\text{maybe }\psi_\Omega(\varepsilon_{\mathbb{I}+1})</math> | |<math>\text{maybe }\psi_\Omega(\varepsilon_{\mathbb{I}+1})</math> | ||
| | |||
|<math>\rm \Delta_3^1-CA+BI</math><br><math>\rm \Sigma_3^1-AC+BI</math><br><math>\rm \Sigma_3^1-DC+BI</math> | |<math>\rm \Delta_3^1-CA+BI</math><br><math>\rm \Sigma_3^1-AC+BI</math><br><math>\rm \Sigma_3^1-DC+BI</math> | ||
|<math>{\rm KP}+\Delta_2^{\rm set}\text{-Separation}</math> | |<math>{\rm KP}+\Delta_2^{\rm set}\text{-Separation}</math> | ||
| 第423行: | 第505行: | ||
|- | |- | ||
|<math>\psi_\Omega(\varepsilon_{\mathbb{I}+1})</math> | |<math>\psi_\Omega(\varepsilon_{\mathbb{I}+1})</math> | ||
| | |||
| | | | ||
|<math>{\rm KP}+\Pi_1^{\rm set}\text{-Collection}</math> | |<math>{\rm KP}+\Pi_1^{\rm set}\text{-Collection}</math> | ||
| | | | ||
|- | |- | ||
| | |||
| | | | ||
|<math>\Pi_{n+3}^1{\rm-CA+BI}</math> | |<math>\Pi_{n+3}^1{\rm-CA+BI}</math> | ||
| 第432行: | 第516行: | ||
| | | | ||
|- | |- | ||
| | |||
| | | | ||
|<math>\Pi_{n+3}^1{\rm-CA}+\Sigma_{n+3}^1{\rm-AC+BI}</math> | |<math>\Pi_{n+3}^1{\rm-CA}+\Sigma_{n+3}^1{\rm-AC+BI}</math> | ||
| 第438行: | 第523行: | ||
|- | |- | ||
| | | | ||
|>=Y(1,3) | |||
|<math>\rm Z_2=\Pi_\infty^1-CA</math><br><math>\rm \Delta_1^2-CA_0</math><br><math>\rm Z_2+\Sigma_\infty^1-AC</math> | |<math>\rm Z_2=\Pi_\infty^1-CA</math><br><math>\rm \Delta_1^2-CA_0</math><br><math>\rm Z_2+\Sigma_\infty^1-AC</math> | ||
|<math>{\rm KP}+\Sigma_\omega^{\rm set}\text{-Separation}</math><br><math>{\rm KP^-}+\Sigma_\omega^{\rm set}\text{-Separation}+\Sigma_\omega^{\rm set}\text{-Collection}</math><br><math>\rm ZFC^-=ZFC-Powerset</math> | |<math>{\rm KP}+\Sigma_\omega^{\rm set}\text{-Separation}</math><br><math>{\rm KP^-}+\Sigma_\omega^{\rm set}\text{-Separation}+\Sigma_\omega^{\rm set}\text{-Collection}</math><br><math>\rm ZFC^-=ZFC-Powerset</math> | ||
| | | | ||
|- | |- | ||
| | |||
| | | | ||
|<math>{\rm Z}_{n+3}=\Pi_\infty^{n+2}{\rm-CA}</math><br><math>\Delta_1^{n+3}{\rm-CA_0}</math> | |<math>{\rm Z}_{n+3}=\Pi_\infty^{n+2}{\rm-CA}</math><br><math>\Delta_1^{n+3}{\rm-CA_0}</math> | ||
| 第447行: | 第534行: | ||
| | | | ||
|- | |- | ||
| | |||
| | | | ||
|<math>\rm Z_\infty=\Pi_0^\infty-CA</math> | |<math>\rm Z_\infty=\Pi_0^\infty-CA</math> | ||
| 第453行: | 第541行: | ||
|- | |- | ||
| | | | ||
|<math> \qquad \qquad \qquad \qquad \qquad </math> | |||
| | | | ||
|<math>\rm IZF=CZF+Powerset+\Pi_\omega^{set}-Reflection</math><br><math>\rm ZF=CZF+LEM=IZF+LEM</math><br><math>\rm ZFC</math><br><math>\rm ZFC+V=L</math><br><math>\rm AST</math><br><math>\rm IST</math><br><math>\rm NBG=GBC</math><br><math>\rm GB</math> | |<math>\rm IZF=CZF+Powerset+\Pi_\omega^{set}-Reflection</math><br><math>\rm ZF=CZF+LEM=IZF+LEM</math><br><math>\rm ZFC</math><br><math>\rm ZFC+V=L</math><br><math>\rm AST</math><br><math>\rm IST</math><br><math>\rm NBG=GBC</math><br><math>\rm GB</math> | ||
| 第533行: | 第622行: | ||
* <math>\mathrm{ZF}_j + \mathrm{DC} + \text{(there is a Reinhardt cardinal )}</math> | * <math>\mathrm{ZF}_j + \mathrm{DC} + \text{(there is a Reinhardt cardinal )}</math> | ||
* <math>\mathrm{ZF} + \mathrm{DC} + \text{(there is a Berkeley cardinal)}</math> | * <math>\mathrm{ZF} + \mathrm{DC} + \text{(there is a Berkeley cardinal)}</math> | ||
[[分类:集合论相关]] | |||
2025年9月17日 (三) 01:41的最新版本
证明论序数(或称证明论强度序数,Proof-Theoretic Ordinal)是衡量形式理论强度的核心工具,通过将理论映射到序数上,刻画其能证明的良序关系的复杂度。该概念源于希尔伯特的证明论计划,旨在通过有限方法证明数学基础理论的一致性,后由阿克曼(Wilhelm Ackermann)和根岑(Gerhard Gentzen)发展为序数分析技术。
定义和性质
对形式理论 ,其证明论序数 ( 或 )定义为能用超限归纳证明的原始递归良序的序型最大值。
证明论序数满足:
- 对任意递归序数 ,理论 能证明“所有序数小于 的原始递归良序关系都是良序的”;对 ,理论 无法证明“所有序数小于 的原始递归良序关系都是良序的”。
- 存在一种递归记号系统,自然表示所有小于 的序数;理论 能通过超限归纳(序数是良序集的序型,满足超限归纳原理:,其中 是任意性质)到 ,证明自身的一致性(即 );理论 能证明所有初等递归函数在小于 的序数上总停止;对任意递归序数 ,至少不满足上述条件中的一条。
- 证明论序数必为递归序数(recursive ordinal),即存在递归关系定义其良序。
证明论序数表
| 证明论序数(OCF及其他记号) | 证明论序数(BMS及其他记号) | 算术论体系 | 集合论体系 | 其他体系 |
|---|---|---|---|---|
| (0)(1) | ||||
| (0)(1)(1) | ||||
| (0)(1)(1)(1) | ||||
| (0)(1)^n | ||||
| (0)(1)(2) | ||||
| (0)(1)(2)(3)(4) | ||||
| (0)(1)(2)...(n+2) | ||||
| (0)(1,1) | ||||
| (0)(1,1)(1,1) | ||||
| (0)(1,1)(2) | ||||
| (0)(1,1)(2)(3,1) | ||||
| (0)(1,1)(2,1) | ||||
| (0)(1,1)(2,1)(2)(3,1) | ||||
| (0)(1,1)(2,1)(3) | ||||
| (0)(1,1)(2,1)(3)(4,1) | ||||
| (0)(1,1)(2,1)(3)(4,1)(5,1)(6) | ||||
| (0)(1,1)(2,1)(3,1) | ||||
| (0)(1,1)(2,1)(3,1)(2)(3) | ||||
| (0)(1,1)(2,1)(3,1)(2)(3,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3)(4,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3)(4,1)(5,1)(6,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3,1)(2)(3,1) | ||||
| (0)(1,1)(2,1)(3,1)(2,1)(3,1)(2,1)(3)(4,1) | ||||
| (0)(1,1)(2,1)(3,1)(3) | ||||
| (0)(1,1)(2,1)(3,1)(3)(4,1) | ||||
| (0)(1,1)(2,1)(3,1)(3,1) | ||||
| (0)(1,1)(2,1)(3,1)(4) | ||||
| (0)(1,1)(2,1)(3,1)(4,1) | ||||
| (0)(1,1)(2,2) | ||||
| (0)(1,1)(2,2)(3,2) | ||||
| (0)(1,1)(2,2)(3,2)(4,2) | ||||
| (0)(1,1)(2,2)(3,3) | ||||
| (0)(1,1,1) | ||||
| (0)(1,1,1)(2)(3) | ||||
| (0)(1,1,1)(2)(3,1) | ||||
| (0)(1,1,1)(2,1) | ||||
| (0)(1,1,1)(2,1)(3) | ||||
| (0)(1,1,1)(2,1)(3)(4) | ||||
| (0)(1,1,1)(2,1)(3,2) | ||||
| (0)(1,1,1)(2,1,1)(3) | ||||
| (0)(1,1,1)(2,1,1)(3)(4,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(2) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(2)(3,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(2,1)(3,2) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(3) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(3)(4,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(4,2) | ||||
| (0)(1,1,1)(2,1,1)(3,1)(4,2,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1,1)(3,1)(4,2) | ||||
| (0)(1,1,1)(2,1,1)(3,1,1)(3,1)(4,2,1) | ||||
| (0)(1,1,1)(2,1,1)(3,1,1)(4,1)(5,2) | ||||
| (0)(1,1,1)(2,1,1)(3,1,1)(4,1,1)(5,1)(6,2) | ||||
| (0)(1,1,1)(2,2) | ||||
| (0)(1,1,1)(2,2)(3,2)(4,1)(2) | ||||
| (0)(1,1,1,1)? | ||||
| (0)(1,1,1,1)(2,1,1)(3,2,2)? | ||||
| >=Y(1,3) | ||||
ZFC 相关证明论序数: