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

Paulo Oliva, Thomas Powell

Research output: Contribution to journalArticlepeer-review

7 Citations (Scopus)

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.
Original languageEnglish
Pages (from-to)1755-1778
JournalMathematical Structures in Computer Science
Volume25
Issue number8
Publication statusPublished - 2015

Fingerprint Dive into the research topics of 'A constructive interpretation of Ramsey's theorem via the product of selection functions'. Together they form a unique fingerprint.

Cite this