Ramsey's Theorem and the Pigeonhole Principle in Intuitionistic Mathematics

Authors

Wim Veldman, Marc Bezem

Type: Article

Publication Date: 1993-04-01

Citations: 38

DOI: https://doi.org/10.1112/jlms/s2-47.2.193

View Ask PDF

Abstract

Locations

Journal of the London Mathematical Society
View
Data Archiving and Networked Services (DANS)
View PDF

Ask a Question About This Paper

Summary

Similar Works

Ramsey's theorem and the pigeonhole principle in intuitionistic mathematics

1992-01-01

Wim Veldman , Bezem

At first sight, the argument which F.P. Ramsey gave for (the infinite case of) his famous theorem from 1927, is hopelessly unconstructive. If suitably reformulated, the theorem is true intuitionistically … At first sight, the argument which F.P. Ramsey gave for (the infinite case of) his famous theorem from 1927, is hopelessly unconstructive. If suitably reformulated, the theorem is true intuitionistically as well as classically: we offer a proof which should convince both the classical and the intuitionistic reader.

Ramsey theory with and without the pigeonhole principle

2016-01-01

Noé de Rancourt

The Pigeonhole Principle and Ramsey Numbers

1992-07-01

RAMSEY'S THEOREM

1990-08-31

Nils‐Eric Sahlin

In his essay entitled ‘Mathematical Logic’ written in 1926, Ramsey gives his opinion of the evolution of mathematical logic after the publication of Principia Mathematica. The essay is largely a … In his essay entitled ‘Mathematical Logic’ written in 1926, Ramsey gives his opinion of the evolution of mathematical logic after the publication of Principia Mathematica. The essay is largely a defence of the ideas of logicism against the attacks by Hilbert's formalism and Brouwer's intuitionism. Ramsey had already criticized Hilbert and Brouwer in ‘The Foundation of Mathematics’, and ‘Mathematical Logic’ is only a popular version of this criticism.

Ramsey Theory

2021-05-28

Manuel Bodirsky

A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content. A summary is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.

Review: K. Chandrasekharan, The Logic of Intuitionistic Mathematics

1942-12-01

Alonzo Church

A direct proof of the intuitionistic Ramsey Theorem

2005-11-23

Thierry Coquand

Ramsey Theory

1998-01-01

Béla Bollobás

Mathematical Intuition

1983-12-01

John Nolt

Mathematical Intuition

1989-01-01

Richard Tieszen

A. G. Dragalin. Mathematical intuitionism. Introduction to proof theory. English translation by E. Mendelson of Matématičéskij intuicionizm, Vvédénié v téoriúdokazatél'stv. Translations of mathematical monographs, vol. 67. American Mathematical Society, Providence1988, ix + 228 pp.

1990-09-01

A. S. Troelstra

An abstract is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content. An abstract is not available for this content so a preview has been provided. Please use the Get access link above for information on how to access this content.

G. F. C. Griss and his negationless intuitionistic mathematics

1955-01-01

A. Heyting

Intuition in Mathematics

2014-08-25

Elijah Chudnoff

Ramsey’s Theorem

2021-07-31

Vašek Chvátal

Ramsey theory

2019-06-12

Ramsey Theory

2014-01-01

Steven G. Krantz , Harold R. Parks

Ramsey Theory

2019-11-28

Gary Chartrand , Ping Zhang

Ramsey Theory

2020-07-23

Fan Chung , Ron Graham

Ramsey Theory

1990-07-01

Ronald Graham , Joel H. Spencer

Ramsey Theory

2010-08-12

Cited by (21)

Reifying dynamical algebra: Maximal ideals in countable rings, constructively

2024-04-26

Ingo Blechschmidt , Peter Schuster

The existence of a maximal ideal in a general nontrivial commutative ring is tied together with the axiom of choice. Following Berardi, Valentini and thus Krivine but using the relative … The existence of a maximal ideal in a general nontrivial commutative ring is tied together with the axiom of choice. Following Berardi, Valentini and thus Krivine but using the relative interpretation of negation (that is, as “implies 0 = 1”) we show, in constructive set theory with minimal logic, how for countable rings one can do without any kind of choice and without the usual decidability assumption that the ring is strongly discrete (membership in finitely generated ideals is decidable). By a functional recursive definition we obtain a maximal ideal in the sense that the quotient ring is a residue field (every noninvertible element is zero), and with strong discreteness even a geometric field (every element is either invertible or else zero). Krull’s lemma for the related notion of prime ideal follows by passing to rings of fractions. By employing a construction variant of set-theoretic forcing due to Joyal and Tierney, we expand our treatment to arbitrary rings and establish a connection with dynamical algebra: We recover the dynamical approach to maximal ideals as a parametrized version of the celebrated double negation translation. This connection allows us to give formal a priori criteria elucidating the scope of the dynamical method. Along the way we do a case study for proofs in algebra with minimal logic, and generalize the construction to arbitrary inconsistency predicates. A partial Agda formalization is available at an accompanying repository.11 See https://github.com/iblech/constructive-maximal-ideals/. This text is a revised and extended version of the conference paper (In Revolutions and Revelations in Computability. 18th Conference on Computability in Europe (2022) Springer). The conference paper only briefly sketched the connection with dynamical algebra; did not compare this connection with other flavors of set-theoretic forcing; and sticked to the case of commutative algebra only, passing on the generalization to inconsistency predicates and well-orders.

Finite sets in homotopy type theory

2018-01-08

Dan Frumin , Herman Geuvers , Léon Gondelman +1 more

We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. … We study different formalizations of finite sets in homotopy type theory to obtain a general definition that exhibits both the computational facilities and the proof principles expected from finite sets. We use higher inductive types to define the type K(A) of "finite sets over type A" à la Kuratowski without assuming that K(A) has decidable equality. We show how to define basic functions and prove basic properties after which we give two applications of our definition.

Chat View PDF

An intuitionistic version of Ramsey's Theorem and its use in Program Termination

2015-08-20

Stefano Berardi , Silvia Steila

Another proof of the intuitionistic Ramsey theorem

1993-07-01

Thierry Coquand

Brouwer’s Real Thesis on Bars

2006-09-01

Wim Veldman

L.E.J. Brouwer made a mistake in the formulation of his famous bar theorem, as was pointed out by S.C. Kleene. By repeating this mistake several times, Brouwer has caused confusion. … L.E.J. Brouwer made a mistake in the formulation of his famous bar theorem, as was pointed out by S.C. Kleene. By repeating this mistake several times, Brouwer has caused confusion. We consider the assumption underlying his bar theorem, calling it Brouwer's Thesis. This assumption is not refuted by Kleene's example and we use it to obtain a conclusion different from Brouwer's. Thus we come to support a view first expressed and defended by E. Martino and P. Giaretta in [Martino 1981]. We also indicate that Brouwer's Thesis has many more applications than Brouwer dreamt of.

Chat View PDF

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

2014-11-13

Paulo Oliva , Thomas Powell

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 … 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.

Chat View PDF

An intuitionistic proof of Kruskal?s theorem

2004-02-01

Wim Veldman

Chat View PDF

A Mechanized Proof of Higman’s Lemma by Open Induction

2020-01-01

Christian Sternagel

A MARRIAGE OF BROUWER’S INTUITIONISM AND HILBERT’S FINITISM I: ARITHMETIC

2021-01-07

Takako Nemoto , Kentaro Sato

Abstract We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics (i.e., which part … Abstract We investigate which part of Brouwer’s Intuitionistic Mathematics is finitistically justifiable or guaranteed in Hilbert’s Finitism, in the same way as similar investigations on Classical Mathematics (i.e., which part is equiconsistent with $\textbf {PRA}$ or consistent provably in $\textbf {PRA}$ ) already done quite extensively in proof theory and reverse mathematics. While we already knew a contrast from the classical situation concerning the continuity principle, more contrasts turn out: we show that several principles are finitistically justifiable or guaranteed which are classically not. Among them are: (i) fan theorem for decidable fans but arbitrary bars; (ii) continuity principle and the axiom of choice both for arbitrary formulae; and (iii) $\Sigma _2$ induction and dependent choice. We also show that Markov’s principle MP does not change this situation; that neither does lesser limited principle of omniscience LLPO (except the choice along functions); but that limited principle of omniscience LPO makes the situation completely classical.

Higman's lemma in type theory

1998-01-01

Daniel Fridlender

An Analysis of Ramsey′s Theorem

1994-05-01

Thierry Coquand

Ramsey Theorem as an Intuitionistic Property of Well Founded Relations

2014-01-01

Stefano Berardi , Silvia Steila

Finite sets in homotopy type theory

2017-12-22

Dan Frumin , Herman Geuvers , Léon Gondelman +1 more

Chat View PDF

Investigating Streamless Sets

2015-01-01

Erik Parmann

In this paper we look at streamless sets, recently investigated by Coquand and Spiwack. A set is streamless if every stream over that set contain a duplicate. It is an … In this paper we look at streamless sets, recently investigated by Coquand and Spiwack. A set is streamless if every stream over that set contain a duplicate. It is an open question in constructive mathematics whether the Cartesian product of two streamless sets is streamless. We look at some settings in which the Cartesian product of two streamless sets is indeed streamless; in particular, we show that this holds in Martin-Loef intentional type theory when at least one of the sets have decidable equality. We go on to show that the addition of functional extensionality give streamless sets decidable equality, and then investigate these results in a few other constructive systems.

The Principle of Open Induction on Cantor space and the Approximate-Fan Theorem

2014-08-11

Wim Veldman

The paper is a contribution to intuitionistic reverse mathematics. We work in a weak formal system for intuitionistic analysis. The Principle of Open Induction on Cantor space is the statement … The paper is a contribution to intuitionistic reverse mathematics. We work in a weak formal system for intuitionistic analysis. The Principle of Open Induction on Cantor space is the statement that every open subset of Cantor space that is progressive with respect to the lexicographical ordering of Cantor space coincides with Cantor space. The Approximate-Fan Theorem is an extension of the Fan Theorem that follows from Brouwer's principle of induction on bars in Baire space and implies the Principle of Open Induction on Cantor space. The Principle of Open Induction in Cantor space implies the Fan Theorem, but, conversely the Fan Theorem does not prove the Principle of Open Induction on Cantor space. We list a number of equivalents of the Principle of Open Induction on Cantor space and also a number of equivalents of the Approximate-Fan Theorem.

Chat View PDF

Intuitionism: an inspiration?

2021-01-01

Wim Veldman

The paper is an introduction to intuitionistic mathematics. The paper is an introduction to intuitionistic mathematics.

Chat View PDF

On Bar Recursive Interpretations of Analysis.

2013-08-01

Thomas Powell

A Locale for Minimal Bad Sequences

2012-08-07

Christian Sternagel

We present a locale that abstracts over the necessary ingredients for constructing a minimal bad sequence, as required in classical proofs of Higman's lemma and Kruskal's tree theorem. We present a locale that abstracts over the necessary ingredients for constructing a minimal bad sequence, as required in classical proofs of Higman's lemma and Kruskal's tree theorem.

Variations on Noetherianness

2016-04-01

Denis Firsov , Tarmo Uustalu , Niccolò Veltri

In constructive mathematics, several nonequivalent notions of finiteness exist. In this paper, we continue the study of Noetherian sets in the dependently typed setting of the Agda programming language. We … In constructive mathematics, several nonequivalent notions of finiteness exist. In this paper, we continue the study of Noetherian sets in the dependently typed setting of the Agda programming language. We want to say that a set is Noetherian, if, when we are shown elements from it one after another, we will sooner or later have seen some element twice. This idea can be made precise in a number of ways. We explore the properties and connections of some of the possible encodings. In particular, we show that certain implementations imply decidable equality while others do not, and we construct counterexamples in the latter case. Additionally, we explore the relation between Noetherianness and other notions of finiteness.

Chat View PDF

On streams that are finitely red

2012-10-10

Marc Bezem , Keiko Nakata , Tarmo Uustalu

Mixing induction and coinduction, we study alternative definitions of streams being finitely red. We organize our definitions into a hierarchy including also some well-known alternatives in intuitionistic analysis. The hierarchy … Mixing induction and coinduction, we study alternative definitions of streams being finitely red. We organize our definitions into a hierarchy including also some well-known alternatives in intuitionistic analysis. The hierarchy collapses classically, but is intuitionistically of strictly decreasing strength. We characterize the differences in strength in a precise way by weak instances of the Law of Excluded Middle.

Chat View PDF

Constructive Analysis of S1S and Büchi Automata

2018-01-01

Moritz Lichter , Gert Smolka

We study S1S and Büchi automata in the constructive type theory of the Coq proof assistant. For UP semantics (ultimately periodic sequences), we verify Büchi's translation of formulas to automata … We study S1S and Büchi automata in the constructive type theory of the Coq proof assistant. For UP semantics (ultimately periodic sequences), we verify Büchi's translation of formulas to automata and thereby establish decidability of S1S constructively. For AS semantics (all sequences), we verify Büchi's translation assuming that sequences over finite semigroups have Ramseyan factorisations (RF). Assuming RF, UP semantics and AS semantics agree. RF is a consequence of Ramsey's theorem and implies the infinite pigeonhole principle, which is known to be unprovable constructively. We show that each of the following properties holds for UP semantics but is equivalent to RF for AS semantics: excluded middle of formula satisfaction, excluded middle of automaton acceptance, and existence of complement automata.

Chat View PDF

References (2)

Ramsey's theorem and recursion theory

1972-06-01

Carl G. Jockusch

Let N be the set of natural numbers. If A ⊆ N , let [ A ] n denote the class of all n -element subsets of A . If … Let N be the set of natural numbers. If A ⊆ N , let [ A ] n denote the class of all n -element subsets of A . If P is a partition of [ N ] n into finitely many classes C 1 , …, C p , let H ( P ) denote the class of those infinite sets A ⊆ N such that [ A ] n ⊆ C i for some i . Ramsey's theorem [8, Theorem A] asserts that H ( P ) is nonempty for any such partition P . Our purpose here is to study what can be said about H ( P ) when P is recursive, i.e. each C i , is recursive under a suitable coding of [ N ] n . We show that if P is such a recursive partition of [ N ] n , then H ( P ) contains a set which is Π n 0 in the arithmetical hierarchy. In the other direction we prove that for each n ≥ 2 there is a recursive partition P of [ N ] n into two classes such that H ( P ) contains no Σ n 0 set. These results answer a question raised by Specker [12]. A basic partition is a partition of [ N ] 2 into two classes. In §§2, 3, and 4 we concentrate on basic partitions and in so doing prepare the way for the general results mentioned above. These are proved in §5. Our “positive” results are obtained by effectivizing proofs of Ramsey's theorem which differ from the original proof in [8]. We present these proofs (of which one is a generalization of the other) in §§4 and 5 in order to clarify the motivation of the effective versions.

Ramsey's Theorem does not Hold in Recursive Set Theory

1971-01-01

Bonny Specker