Hostname: page-component-8448b6f56d-sxzjt Total loading time: 0 Render date: 2024-04-24T18:12:26.036Z Has data issue: false hasContentIssue false
  • English
  • Français

Choice principles, the bar rule and autonomously iterated comprehension schemes in analysis

Published online by Cambridge University Press:  12 March 2014

S. Feferman  and
G. Jäger
S. Feferman
Affiliation:
Stanford University, Stanford, California 94305
G. Jäger
Affiliation:
Ludwig-Maximilians-Universität München, D-8000 München 2, Federal Republic of Germany
Get access Rights & Permissions [Opens in a new window]

Extract

In [10] Friedman showed that (-AC) is a conservative extension of (-CA)<ε0 for -sentences where i = min(n + 2, 4), i.e., i = 2, 3, 4 for n = 0, 1, 2 + m. Feferman [5], [7] and Tait [11], [12] reobtained this result for n = 0, 1 and even with (-DC) instead of (-AC). Feferman and Sieg established in [9] the conservativeness of (-DC) over (-CA)<ε0 for -sentences (i as above) for all n. In each paper, different methods of proof have been used. In particular, Feferman and Sieg showed how to apply familiar proof-theoretical techniques by passing through languages with Skolem functionals.

In this paper we study the same choice principles in the presence of the Bar Rule (BR), which permits one to infer the scheme of transfinite induction on a primitive recursive relation ≺ when it has been proved that ≺ is wellfounded. The main result (Theorem 1 below) characterizes (-DC) + (BR) as a conservative extension of a system of the autonomously iterated -comprehension axiom for -sentences (i depending on n as above). For n = 0 this has been proved by Feferman in the form that (-DC) + (BR) is a conservative extension of (-CA)<Γ0; this was first done in [8] by use of the Gödel functional interpretation for the stronger system Zω + μ + (QF-AC) + (BR) and then more recently by the simpler methods of [9]. Jäger showed how the latter methods could also be used to obtain the general result of Theorem 1 below.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 48 , Issue 1 , March 1983 , pp. 63 - 70
Copyright
Copyright © Association for Symbolic Logic 1983

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.)

References

REFERENCES

[1]Buchholz, W. and Pohlers, W., Provable wellorderings of formal theories for transfinitely iterated inductive definitions, this Journal, vol. 43 (1978), pp. 118–125.Google Scholar
[2]Feferman, S., Systems of predicative analysis, this Journal, vol. 29 (1964), pp. 1–30.Google Scholar
[3]Feferman, S., Autonomous transfinite progressions andthe extent of predicative mathematics, Logic, methodology, and philosophy of science. III, North-Holland, Amsterdam, 1968, pp. 121–135.CrossRefGoogle Scholar
[4]Feferman, S., Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis, Intuitionism and proof theory, North-Holland, Amsterdam, 1970, pp. 303–326.Google Scholar
[5]Feferman, S., Ordinals and functional in proof theory, Proceedings of the International Congress of Mathematicians, Nice, 1970, Gauthier-Villars, Paris, 1971, pp. 229–233.Google Scholar
[6]Feferman, S., A language and axioms for explicit mathematics, Algebra and logic, Lecture Notes in Mathematics, no. 450, Springer, Berlin, 1975, pp. 87–139.CrossRefGoogle Scholar
[7]Feferman, S., Theories of finite type related to mathematical practice, Handbook of mathematical logic, North-Holland, Amsterdam, 1977, pp. 913–971.CrossRefGoogle Scholar
[8]Feferman, S., A more perspicuous formal system for predicativity, Konstruktionen versus Positionen. I, de Gruyter, Berlin, 1978, pp. 68–93.CrossRefGoogle Scholar
[9]Feferman, S. and Sieg, W., Proof theoretic equivalences between classical and constructive theories for analysis. Iterated inductive definitions and subsystems of analysis; recent proof-theoretical studies, Lecture Notes in Mathematics, no. 897, Springer, Berlin, 1981, pp. 78–142.Google Scholar
[10]Friedman, H., Iterated inductive definitions and -AC, Intuitionism and proof theory, North-Holland, Amsterdam, 1970, pp. 435–442.Google Scholar
[11]Tait, W.W., Normal derivability in classical logic, The syntax and semantics of infinitary languages, Lecture Notes in Mathematics, no. 72, Springer, Berlin, 1968.Google Scholar
[12]Tait, W.W., Applications of the cut-elimination theorem to some subsystems of classical analysis, Intuitionism and proof theory, North-Holland, Amsterdam, 1970, pp. 475–488.Google Scholar
[13]Troelstra, A.S., Metamathematical investigations of intuitionistic arithmetic and analysis, Lecture Notes in Mathematics, no. 344, Springer, Berlin, 1973.Google Scholar