Peano算術の無矛盾性証明
Peano算術
$ \sf PA
の無矛盾性
$ \mathrm{Con}_\mathsf{PA}
は、
$ \sf PA
に
$ \varepsilon_0
までの
超限帰納法
までを加えた体系において証明可能。