算術的超限再帰 ATR0
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/05/19 05:20 UTC 版)
ATR 0 {\displaystyle {\mbox{ATR}}_{0}\,} は、 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} に算術的超限再帰を追加した体系である。 ATR 0 {\displaystyle {\mbox{ATR}}_{0}\,} は ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} 上で、Σ11分離原理と同値である。 ATR 0 {\displaystyle {\mbox{ATR}}_{0}\,} は、 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} の無矛盾性を証明可能なのでゲーデルの不完全性定理より、 ACA 0 {\displaystyle {\mbox{ACA}}_{0}\,} より強い。 RCA 0 {\displaystyle {\mbox{RCA}}_{0}\,} で次が ATR 0 {\displaystyle {\mbox{ATR}}_{0}\,} と同値。 任意の二つの可算整列順序は比較可能（一方が他方または他方の始片に同型）である。 可算被約アーベル群に対するウルムの定理。 完備可分距離空間の任意の非可算閉部分集合が完全閉集合を含むことを述べた完全集合定理。 ルージンの分離定理（essentially Σ 1 1 {\displaystyle \Sigma _{1}^{1}\,} 分離）。 ベール空間における開集合の決定性。
※この「算術的超限再帰 ATR0」の解説は、「逆数学」の解説の一部です。
「算術的超限再帰 ATR0」を含む「逆数学」の記事については、「逆数学」の概要を参照ください。
- 算術的超限再帰 ATR0のページへのリンク
