Searcharxiv⌕ Search

arXiv subjects

Wim Veldman

Publications and source records attributed to Wim Veldman.

8 recordsLinked to original sources
arXiv2023

The Fan Theorem, its strong negation, and the determinacy of games

IIn the context of a weak formal theory called Basic Intuitionistic Mathematics $\mathsf{BIM}$, we study Brouwer's Fan Theorem and a strong negation of the Fan Theorem, Kleene's Alternative (to the Fan Theorem). We prove that the Fan Theorem is equivalent to contrapositions of a number of intuitionistically accepted axioms of countable choice and that Kleene's Alternative is equivalent to strong negations of these statements. We also discuss finite and infinite games and introduce a constructively useful notion of determinacy. We prove that the Fan Theorem is equivalent to the Intuitionistic Determinacy Theorem, saying that every subset of Cantor space is, in our constructively meaningful sense, determinate, and show that Kleene's Alternative is equivalent to a strong negation of a special case of this theorem. We then consider a uniform intermediate value theorem and a compactness theorem for classical propositional logic, and prove that the Fan Theorem is equivalent to each of these theorems and that Kleene's Alternative is equivalent to strong negations of them. We end with a note on a possibly important statement, provable from principles accepted by Brouwer, that one might call a Strong Fan Theorem.

math.LO↗
arXiv2023

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

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.

math.LO↗
arXiv2022

On some of Brouwer's axioms

We discuss the position of intuitionistic mathematics within the field of constructive mathematics. We discuss some principles defended and used by Brouwer but rejected by Bishop, like the Coninuity Principle, the Fan Theorem and the Bar Theorem. We explain some of their consequences in the development of constructive mathematics, like the Borel Hierarchy Theorem and the Intuitionistic Ramsey Theorem. We go into the theory of measure and integration as Bishop followed in this field a path different from Brouwer's.

math.LO↗
arXiv2022

Brouwer's Fan Theorem as an axiom and as a contrast to Kleene's Alternative

The paper is a contribution to intuitionistic reverse mathematics. We introduce a formal system called Basic Intuitionistic Mathematics BIM, and then search for statements that are, over BIM, equivalent to Brouwer's Fan Theorem or to its positive denial, Kleene's Alternative to the Fan Theorem. The Fan Theorem is true under the intended intuitionistic interpretation and Kleene's Alternative is true in the model of BIM consisting of the Turing-computable functions. The task of finding equivalents of Kleene's Alternative is, intuitionistically, a nontrivial extension of finding equivalents of the Fan Theorem, although there is a certain symmetry in the arguments that we shall try to make transparent. We introduce closed-and-separable subsets of Baire space and of the set of the real numbers. Such sets may be compact and also positively noncompact. The Fan Theorem is the statement that Cantor space, or, equivalently, the unit interval, is compact, and Kleene's Alternative is the statement that Cantor space, or, equivalently, the unit interval is positively noncompact. The class of the compact closed-and-separable sets and also the class of the closed-and-separable sets that are positively noncompact are characterized in many different ways and a host of equivalents of both the Fan Theorem and Kleene's Alternative is found.

math.LO↗
arXiv2022

Projective sets, intuitionistically

We study `definable' subsets of Baire space $\mathcal{N}$. The logic of our arguments is intuitionistic and we use L.E.J.~Brouwer's Thesis on bars in $\mathcal{N}$ and his continuity axioms. We avoid the operation of taking the complement of a subset of $\mathcal{N}$. A subset of $\mathcal{N}$ is $\mathbfΣ^1_1$ or: analytic if it is the projection of a closed subset of $\mathcal{N}$. Important $\mathbfΣ^1_1$ set are the set of the codes of all closed and located subsets of $\mathcal{N}$ that are positively uncountable and the set of the codes of all located and closed subsets of $\mathcal{N}$ containing at least one member coding a (positively) infinite subset of $\mathbb{N}$. A subset of $\mathcal{N}$ is strictly analytic if it is the projection of a closed and located subset of $\mathcal{N}$. Brouwer's Thesis on bars in $\mathcal{N}$ proves separation and boundedness theorems for strictly analytic subsets of $\mathcal{N}$. A subset of $\mathcal{N}$ is $\mathbfΠ^1_1$ or: co-analytic if it is the co-projection of an open subset of $\mathcal{N} \times \mathcal{N}=\mathcal{N}$. There is no symmetry between analytic and co-analytic sets like in classical descriptive set theory. An important $\mathbfΠ^1_1$ set is the set of the codes of all closed and located subsets of $\mathcal{N}$ all of whose members code an almost-finite subset of $\mathbb{N}$. The set of the codes of closed and located subsets of $\mathcal{N}$ that are almost-countable, or, equivalently, \{reducible in Cantor's sense, is treated at some length. This set is probably not $\mathbfΠ^1_1$. The projective hierarchy collapses: every (positively) projective set is $\mathbfΣ^1_2$: the projection of a co-analytic subset of $\mathcal{N}$.

math.LO↗
arXiv2019

Equality and equivalence, intuitionistically

We show that the intuitionistic first-order theory of equality has continuum many complete extensions. We also study the Vitali equivalence relation and show there are many intuitionistically precise versions of it.

math.LO↗