The non-constructive μ operator, fixed point theories with ordinals, and the bar rule Original Research Article

This paper deals with the proof theory of first-order applicative theories with non-constructive μ operator and a form of the bar rule, yielding systems of ordinal strength View the MathML source and ϕ20, respectively. Relevant use is made of fixed-point theories with ordinals plus bar rule.