Hostname: page-component-8448b6f56d-gtxcr Total loading time: 0 Render date: 2024-04-25T02:37:07.134Z 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
Get access Rights & Permissions [Opens in a new window]

Abstract

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 25 , Special Issue 8: Computing with Infinite Data: Topological and Logical Foundations Part 2 , December 2015 , pp. 1755 - 1778
Copyright
Copyright © Cambridge University Press 2014 

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

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