Abstract
The infinite Ramsey theorem is known to be equivalent to the statement ‘for every set X and natural number n, the n-th Turing jump of X exists’, over RCA0 due to results of Jockusch [5]. By subjecting the theory RCA0 augmented by the latter statement to an ordinal analysis, we give a direct proof of the fact that the infinite Ramsey theorem has proof-theoretic strength ε ω . The upper bound is obtained by means of cut elimination and the lower bound by extending the standard well-ordering proofs for ACA0. There is a proof of this result due to McAloon [6], using model-theoretic and combinatorial techniques. According to [6], another proof appeared in an unpublished paper by Jäger.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Afshari, B.: Relative computability and the proof-theoretic strength of some theories, Ph.D. Thesis, University of Leeds, U.K. (2008)
Friedman, H., McAloon, K., Simpson, S.: A finite combinatorial principle equivalent to the 1-consistency of predicative analysis. In: Metakides, G. (ed.) Patras Logic Symposion, pp. 197–230. North-Holland (1982)
Hinman, P.G.: Recursion-theoretic hierarchies. Springer, Heidelberg (1978)
Jäger, G.: Theories for iterated jumps (1980) (unpublished notes)
Jockusch, C.G.: Ramsey’s theorem and recursion theory. Journal of Symbolic Logic 37, 268–280 (1972)
McAloon, K.: Paris-Harrington incompleteness and progressions of theories. Proceedings of Symposia in Pure Mathematics 42, 447–460 (1985)
Ramsey, F.P.: On a problem of formal logic. Proceedings of the London Mathematical Society 30(1), 264–286 (1930)
Schmerl, U.: A fine structure generated by reflection formulas over primitive recursive arithmetic. In: Boffa, M., McAloon, K., van Dalen, D. (eds.) Studies in Logic and the Foundations of Mathematics, vol. 97, pp. 335–350. Elsevier (1979)
Schütte, K.: Proof theory. Springer, Heidelberg (1977)
Schwichtenberg, H.: Proof theory: Some applications of cut-elimination. In: Barwise, J. (ed.) Handbook of Mathematical Logic, pp. 867–895. North-Holland, Amsterdam (1977)
Simpson, S.G.: Subsystems of second order arithmetic. Springer, Heidelberg (1999)
De Smet, M., Weiermann, A.: A Miniaturisation of Ramsey’s Theorem. In: Ferreira, F., Löwe, B., Mayordomo, E., Mendes Gomes, L. (eds.) CiE 2010. LNCS, vol. 6158, pp. 118–125. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Afshari, B., Rathjen, M. (2012). Ordinal Analysis and the Infinite Ramsey Theorem. In: Cooper, S.B., Dawar, A., Löwe, B. (eds) How the World Computes. CiE 2012. Lecture Notes in Computer Science, vol 7318. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30870-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-30870-3_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30869-7
Online ISBN: 978-3-642-30870-3
eBook Packages: Computer ScienceComputer Science (R0)