Abstract
We have given here an alternative proof of the intuitionistic Ramsey theorem, using first Brouwer's thesis 1927. We have explained then how to formulate this proof in a framework of inductive definitions without assuming Brouwer's thesis 1927. The statement we prove then is the relativised version of the statement over an arbitrary locale.
This example, which can be seen as a concrete illustration of some ideas in Fourman 1984, suggests a possible way of presenting the logic of a process described by a transition system, which consists in working in the topos of sheaves over a locale canonically associated to this transition system. From the logical point of view, this has the advantage of working with points (and actually, generic points), without having to introduce any further axioms.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Brouwer, L. E. J., Uber definitionsbereiche von Funktionen, Math. Ann. 96 (1927), 60–75.
Martin-Löf, P., Notes on Constructive Mathematics, Almqvist & Wiksell, 1970.
Richman F. and Stolzenberg G., Well Quasi-Ordered Sets, To appear in Advances in Mathematics (1991).
Paris J. and Harrington L., A Mathematical Incompleteness in Peano Arithmetic, in the Hanbook of Mathematical Logic (1977), J. Barwise, editor, North-Holland.
Veldman W., Ramsey's Theorem and the Pigeonhole principle in Intuitionistic Mathematics. Report 9017, Department of Mathematics, catholic University, Toernooiveld, 6525 ED Nijmegen,.
Ramsey, F.P., On a Problem of Formal Logic, Proc. London Math. Soc. 48 (1928), 122–160.
Coquand, Th., An analysis of Ramsey's Theorem, Submitted to Information and Computation (1991).
Kleene, S.C. and Vesley, R.E., The Foundations of Intuitionistic Mathematics, North-Holland Publishing Company, 1965.
Abramsky, S., Domain Theory in Logical Form, Annals of Pure and Applied Logic 51 (1991), 1–77.
Fourman, M. P., Continuous Truth I, in Logic Colloquium '82 (1984), North-Holland.
Bell, J.L., Toposes and Local Set Theories, An Introduction, Oxford Science Publications, 1988.
Coquand, Th., Constructive Topology and Combinatorics, to appear in the proceeding of Constructivity in Computer Science, Trinity University, San Antonio, Texas.
Vickers, S., Topology via Logic, Cambridge Tracts in Theoretical Computer Science 5, 1989.
De Bruijn, N. G. and Van Der Meiden, W., Notes on Gelfand's theory, Indagationes 31 (1968), 467–474.
Kripke, S., Semantics analysis of intuitionistic logic I, in: Formal Systems and Recursive Functions. North-Holland, 1965, pp. 92–130.
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Coquand, T. (1991). A direct proof of the intuitionistic Ramsey Theorem. In: Pitt, D.H., Curien, PL., Abramsky, S., Pitts, A.M., Poigné, A., Rydeheard, D.E. (eds) Category Theory and Computer Science. CTCS 1991. Lecture Notes in Computer Science, vol 530. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013465
Download citation
DOI: https://doi.org/10.1007/BFb0013465
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54495-1
Online ISBN: 978-3-540-38413-7
eBook Packages: Springer Book Archive