Ramsey Theorem for pairs is a combinatorial result that cannot be intuitionistically proved. In this paper we present a new form of Ramsey Theorem for pairs we call H-closure Theorem. H-closure is a property of well-founded relations, intuitionistically provable, informative, and simple to use in intuitionistic proofs. Using our intuitionistic version of Ramsey Theorem we intuitionistically prove the Termination Theorem by Poldenski and Rybalchenko. This theorem concerns an algorithm inferring termination for while-programs, and was originally proved from the classical Ramsey Theorem, then intuitionistically, but using an intuitionistic version of Ramsey Theorem different from our one. Our long-term goal is to extract effective bounds for the while-programs from the proof of Termination Theorem, and our new intuitionistic version of Ramsey Theorem is designed for this goal. © 2014 Springer International Publishing Switzerland.
CITATION STYLE
Berardi, S., & Steila, S. (2014). Ramsey theorem as an intuitionistic property of well founded relations. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8560 LNCS, pp. 93–107). Springer Verlag. https://doi.org/10.1007/978-3-319-08918-8_7
Mendeley helps you to discover research relevant for your work.