Systems of explicit mathematics with non-constructive μ-operator. Part II Original Research Article

This paper is mainly concerned with proof-theoretic analysis of some second-order systems of explicit mathematics with a non-constructive minimum operator. By introducing axioms for variable types we extend our first-order theory BON to the elementary explicit type theory EET and add several forms of induction as well as axioms for μ. The principal results then state: EET(μ) plus set induction (type induction, formula induction) is proof-theoretically equivalent to Peano arithmetic PA (the second-order system (Π0∞-CA<ε0, the second-order system (Π0∞-CA)<εε0).