Bar Induction and Π11-CA
Harvey Friedman · Journal of Symbolic Logic · 1969
This paper compares the subsystem of analysis based on the Π11-comprehension axiom (Π11-CA) with classical Bar Induction (BI). An extension of Bar Induction using infinitary formulae is also considered, which was suggested to us by G. Kreisel (oral communication). To describe these formal systems, we first describe the language, L, appropriate for their formalization. L contains the language of ENT (1st order arithmetic) plus function variables ƒi, gi, hi, etc. Number-theoretic terms are built up from +, × , ′ , 0, and application.