Hostname: page-component-7b7567c8c-fvjsw Total loading time: 0 Render date: 2026-11-13T18:13:42.756Z Has data issue: false hasContentIssue false
  • English
  • Français

A constructive interpretation of Ramsey's theorem via the product of selection functions

Published online by Cambridge University Press:  13 November 2014

PAULO OLIVA and
THOMAS POWELL
PAULO OLIVA
Affiliation:
Queen Mary University of London, School of Electronic Engineering and Computer Science, London E1 4NS, United Kingdom Email: paulo.oliva@eecs.qmul.ac.uk, tpowell@eecs.qmul.ac.uk
THOMAS POWELL
Affiliation:
Queen Mary University of London, School of Electronic Engineering and Computer Science, London E1 4NS, United Kingdom Email: paulo.oliva@eecs.qmul.ac.uk, tpowell@eecs.qmul.ac.uk
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

We use Gödel's dialectica interpretation to produce a computational version of the well-known proof of Ramsey's theorem by Erdős and Rado. Our proof makes use of the product of selection functions, which forms an intuitive alternative to Spector's bar recursion when interpreting proofs in analysis. This case study is another instance of the application of proof theoretic techniques in mathematics.

References

Avigad, J. (2009) The metamathematics of ergodic theory. Annals of Pure and Applied Logic 157 64–76.CrossRefGoogle Scholar
Avigad, J. and Feferman, S. (1998) Gödel's functional (‘Dialectica’) interpretation. In: Buss, S. R. (ed.) Handbook of Proof Theory. Studies in Logic and the Foundations of Mathematics volume 137, North Holland, Amsterdam 337–405.CrossRefGoogle Scholar
Bellin, G. (1990) Ramsey interpreted: A parametric version of Ramsey's theorem. In: Logic and Computation (Pittsburgh, PA, 1987), volume 106, American Mathematical Society, Providence, Rhode Island, U.S.A 17–37.Google Scholar
Coquand, T. (1994a) An analysis of Ramsey's theorem. Information and Computation 110 (2) 297–304.Google Scholar
Coquand, T. (1994b) A direct proof of Ramsey's theorem. Available at http://www.cse.chalmers.se/~coquand/ramsey2.pdf.Google Scholar
Erdős, P., Hajnal, A., Máté, A. and Rado, R. (1984) Combinatorial Set Theory: Partition Relations for Cardinals, Studies in Logic and the Foundations of Mathematics volume 106, North-Holland Publishing Company.Google Scholar
Escardó, M. H. and Oliva, P. (2010a) Computational interpretations of analysis via products of selection functions. In: Ferreira, F., Lowe, B., Mayordomo, E. and Gomes, L. M. (eds.) Computability in Europe 2010. Springer Lecture Notes in Computer Science 6158, 141–150.CrossRefGoogle Scholar
Escardó, M. H. and Oliva, P. (2010b) Selection functions, bar recursion, and backward induction. Mathematical Structures in Computer Science 20 (2) 127–168.Google Scholar
Escardó, M. H. and Oliva, P. (2011) Sequential games and optimal strategies. Royal Society Proceedings A 467 1519–1545.CrossRefGoogle Scholar
Escardó, M. H. and Oliva, P. (2012) Computing Nash equilibria of unbounded games. In: Proceedings of the Turing 100 Conference. Turing 100, Manchester.Google Scholar
Escardó, M. H., Oliva, P. and Powell, T. (2011) System T and the product of selection functions. In: Proceedings of CSL'11, Leibniz International Proceedings in Informatics 12 233–247.Google Scholar
Gödel, K. (1958) Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica 12 280–287.CrossRefGoogle Scholar
Kohlenbach, U. (2008) Applied Proof Theory: Proof Interpretations and their Use in Mathematics, Monographs in Mathematics, Springer.Google Scholar
Kohlenbach, U. and Kreuzer, A. (2009) Ramsey's theorem for pairs and provably recursive functions. Notre Dame Journal of Formal Logic 50 427–444.CrossRefGoogle Scholar
Kreisel, G. (1951) On the interpretation of non-finitist proofs, part I. Journal of Symbolic Logic 16 241–267.Google Scholar
Kreisel, G. (1952) On the interpretation of non-finitist proofs, part II: Interpretation of number theory. Journal of Symbolic Logic 17 43–58.CrossRefGoogle Scholar
Kreuzer, A. (2009) Der Satz von Ramsey für Paare und beweisbar rekursive Funktionen, Diploma thesis, Technische Universität Darmstadt.Google Scholar
Oliva, P. and Powell, T. (2012) A game-theoretic computational interpretation of proofs in classical analysis. (Preprint available at arxiv.org/abs/1204.5244.)Google Scholar
Ramsey, F. (1930) On a problem of formal logic. In: Proceedings of the London Mathematical Society s2–30 (1) 264–286.CrossRefGoogle Scholar
Simpson, S. G. (1999) Subsystems of Second Order Arithmetic, Perspectives in Mathematical Logic, Springer, Berlin.CrossRefGoogle Scholar
Spector, C. (1962) Provably recursive functionals of analysis: A consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In: Dekker, F. D. E. (ed.) Recursive Function Theory: Proceedings Symposia in Pure Mathematics, volume 5, American Mathematical Society, Providence, Rhode Island 1–27.Google Scholar
Tao, T. (2008) Structure and Randomness: Pages from Year one of a Mathematical Blog, American Mathematical Society.CrossRefGoogle Scholar
Veldman, W. and Bezem, M. (1993) Ramsey's theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society 2 (47) 193–211.CrossRefGoogle Scholar