Hostname: page-component-7b7567c8c-2n9c9 Total loading time: 0 Render date: 2026-11-14T11:31:03.184Z Has data issue: false hasContentIssue false
  • English
  • Français

On the relation between choice and comprehension principles in second order arithmetic1

Published online by Cambridge University Press:  12 March 2014

Andrea Cantini
Andrea Cantini*
Affiliation:
University of Trieste, Trieste, Italy
*
Current address: Via Adriano Mari 5, I-50136 Firenze, Italy
Get accessRights & Permissions [Opens in a new window]

Abstract

We give a new elementary proof of the comparison theorem relating and ; the proof does not use Skolem theories.

By the same method we prove:

a) , for suitable classes of sentences;

b) proves the consistency of , for finite k, and hence is stronger than .

a) and b) answer a question of Feferman and Sieg.

Information

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 51 , Issue 2 , June 1986, pp. 360 - 373
Copyright
Copyright © Association for Symbolic Logic 1986

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

Article purchase

Temporarily unavailable

Footnotes

1

The results of this paper were presented at the Mathematisches Forschungsinstitut Oberwolfach during the meeting held from January 2 to January 7, 1984.

References

REFERENCES

[AM] Apt, K. and Marek, W., Second order arithmetic and related topics, Annals of Mathematical Logic, vol. 6 (1974), pp. 177–229.CrossRefGoogle Scholar
[BFPS] Buchholz, W., Feferman, S., Pohlers, W. and Sieg, W., Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies, Lecture Notes in Mathematics, vol. 897, Springer-Verlag, Berlin and New York, 1981.Google Scholar
[BS] Barwise, J. and Schlipf, J., On recursively saturated models of arithmetic, Model theory and algebra (a memorial tribute to Abraham Robinson), Lecture Notes in Mathematics, vol. 498, Springer-Verlag, Berlin and New York, 1975, pp. 42–55.CrossRefGoogle Scholar
[BHP] Boyd, R., Hensel, G. and Putnam, H., A recursion-theoretic characterization of the ramified analytical hierarchy, Transactions of the American Mathematical Society, vol. 141(1969), pp. 37–62.CrossRefGoogle Scholar
[C] Cantini, A., On weak theories of sets and classes, which are based on strict -reflection, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik (to appear).Google Scholar
[Fa] Feferman, S., Formal theories for transfinite iterations of generalized inductive definitions and some subsystems of analysis, Intuitionism and proof theory (Kino, A., Myhill, J. and Vesley, R., editors), North-Holland, Amsterdam, 1970, pp. 303–325.Google Scholar
[Fb] Feferman, S., Theories of finite type related to mathematical practice, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 913–971.CrossRefGoogle Scholar
[Fc] Feferman, S., Theories of finite type related to mathematical practice, mimeographed manuscript, to appear in the series Perspectives in Mathematical Logic, Springer-Verlag, Berlin and New York.CrossRefGoogle Scholar
[FSa] Feferman, S. and Sieg, W., Iterated inductive definitions and subsystems of analysis, in [BFPS], pp. 16–77.CrossRefGoogle Scholar
[FSb] Feferman, S. and Sieg, W., Proof theoretic equivalences between classical and constructive theories of analysis, in [BFPS], pp. 79-144.Google Scholar
[Fra] Friedman, H., Iterated inductive definitions and -AC, Intuitionism and proof theory (Kino, A., Myhill, J. and Vesley, R., editors), North-Holland, Amsterdam, 1970, pp. 435–442.Google Scholar
[Frb] Friedman, H., Systems of second order arithmetic. I, II, this Journal, vol. 41 (1976), pp. 557–559.Google Scholar
[G] Girard, J. Y., A survey of -logic, Logic, methodology and philosophy of science. VI (Pfeiffer, H., Łoś, J. and Cohen, L. J., editors) North-Holland, Amsterdam, 1982, pp. 89–107.Google Scholar
[H] Hinman, P., Recursion theoretic hierarchies, Springer-Verlag, Berlin and New York, 1977.Google Scholar
[P] Pohlers, W. Proof theoretical analysis of IDv by the method of local predicativity, in [BFPS], pp. 262–357.Google Scholar
[P1] Plater, R., Eliminating the continuum hypothesis, this Journal, vol. 34 (1969), pp. 219–225.Google Scholar
[R] Rogers, H., Theory of recursive functions and effective computability, McGraw-Hill, New York, 1967.Google Scholar
[Schw] Schwichtenberg, H., Some applications of cut elimination, Handbook of mathematical logic (Barwise, J., editor), North-Holland, Amsterdam, 1977, pp. 868–895.Google Scholar
[Tta] Tait, W., Normal derivability in classical logic, The syntax and semantics of infinitary languages (Barwise, J., editor), Lecture Notes in Mathematics, vol. 72, Springer-Verlag, Berlin and New York, 1968, pp. 204–236.CrossRefGoogle Scholar
[Ttb] Tait, W., Applications of the cut elimination theorem to some subsystems of analysis, Intuitionism and proof theory (Kino, A., Myhill, J. and Vesley, R., editors), North-Holland, Amsterdam, 1970, pp. 475–488.Google Scholar
[Y] Yasuhara, A.. Recursive function theory and logic, Academic Press, New York and London, 1971.Google Scholar