Hostname: page-component-78c5997874-m6dg7 Total loading time: 0 Render date: 2024-11-12T22:30:21.497Z Has data issue: false hasContentIssue false
  • English
  • Français

Bar Induction and Π11-CA1

Published online by Cambridge University Press:  12 March 2014

Harvey Friedman
Harvey Friedman*
Affiliation:
Stanford University
Get access Rights & Permissions [Opens in a new window]

Extract

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.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 34 , Issue 3 , 17 November 1969 , pp. 353 - 362
Copyright
Copyright © Association for Symbolic Logic 1969

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

1

This research was partially supported by NSF GP 8764. We wish to thank G. Kreisel for many helpful suggestions concerning the writing of this paper.

References

[1]Friedman, H., Basic model theory and recursion theory in Π∞0-CA, in preparation.Google Scholar
[2]Friedman, H., Generalized inductive definitions and Σ21-AC, Proceedings of the 1968 Buffalo Conference in Proof Theory and Inflationism.Google Scholar
[3]Howard, W. A. and Kreisel, G., Transfinite induction and bar induction of types 0 and 1, and the role of continuity in intuitionistic analysis, this Journal, vol. 31 (1966), pp. 325–358.Google Scholar
[4]Kreisel, G., Survey of proof theory, this Journal, vol. 33 (1968), pp. 321–388.Google Scholar
[5]Kreisel, G. and Levy, A., Reflection principles and their use for establishing the complexity of axiomatic systems, Zeitschrift für mathematische logik, vol. 14 (1968), pp. 97–142.CrossRefGoogle Scholar