Intuitionistic Set Theory

Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory.
The same first-order language with "$=$" and "$\in$" of classical set theory is usually used, so this is not to be confused with a constructive types approach.
On the other hand, some constructive theories are indeed motivated by their interpretability in type theories.

In addition to rejecting the principle of excluded middle ($$), constructive set theories often require some logical quantifiers in their axioms to be bounded, motivated by results tied to impredicativity.

Introduction

Constructive outlook

Use of intuitionistic logic

The logic of the set theories discussed here is constructive in that it rejects $$, i.e. that the disjunction $\phi \lor \neg \phi$ automatically holds for all propositions. As a rule, to prove the excluded middle for a proposition $P$, i.e. to prove the particular disjunction $P \lor \neg P$, either $P$ or $\neg P$ needs to be explicitly proven. When either such proof is established, one says the proposition is decidable, and this then logically implies the disjunction holds. Similarly, a predicate $Q(x)$ on a domain $X$ is said to be decidable when the more intricate statement $\forall (x\in X). \big(Q(x) \lor \neg Q(x)\big)$ is provable. Non-constructive axioms may enable proofs that ''formally'' decide such $P$ (and/or $Q$) in the sense that they prove excluded middle for $P$ (resp. the statement using the quantifier above) without demonstrating the truth of any of the disjuncts, as is often the case in classical logic. In contrast, constructive theories tend to not permit many classical proofs of properties that are provenly computationally undecidable. Similarly, a counter-example existence claim $\exist(x\in X). \neg R(x)$ is generally constructively stronger than a rejection claim $\neg \forall(x\in X). R(x)$.

The intuitionistic logic underlying the set theories discussed here, unlike the more conservative minimal logic, still permits double negation elimination for individual propositions for which excluded middle holds, and in turn the theorem formulations regarding finite objects tends to not differ from their classical counterparts. Given a model of all numbers, the equivalent for predicates, namely Markov's principle, does not automatically hold, but may be considered as an additional principle.

Expressing the instance for $\neg P$ of the valid law of noncontradiction and using a valid De Morgan's law, already minimal logic does prove $\neg\neg(P \lor \neg P)$ for any given proposition $P$. So in words, intuitionistic logic still posits: It is impossible to rule out a proposition and rule out its negation both at once, and thus the rejection of any instantiated excluded middle statement for an individual proposition is inconsistent. More generally, constructive mathematical theories tend to prove classically equivalent reformulations of classical theorems. For example, in constructive analysis, one cannot prove the intermediate value theorem in its textbook formulation, but one can prove theorems with algorithmic content that, as soon as double negation elimination and its consequences are assumed legal, are at once classically equivalent to the classical statement. The difference is that the constructive proofs are harder to find.

Imposed restrictions

A restriction to the constructive reading of existence apriori leads to stricter requirements regarding which characterizations of a set $f\subset X\times Y$ involving unbounded collections constitute a (mathematical, and so always implying total) function. This is often because the predicate in a case-wise would-be definition may not be decidable. Compared to the classical counterpart, one is generally less likely to prove the existence of relations that cannot be realized. Adopting the standard definition of set equality via extentionality, the full Axiom of Choice is such a non-constructive principle that implies $$ for the formulas permitted in one's adopted Separation schema, by Diaconescu's theorem. Similar results hold for the Axiom of Regularity in its standard form, as shown below. So at the very least, the development of constructive set theory requires rejection of strong choice principles and the rewording of some standard axioms to classically equivalent ones. Undecidability of disjunctions also affects the claims about total orders such as that of all ordinal numbers, expressed by the provability and rejection of the clauses in the order defining disjunction $(\alpha \in \beta) \lor (\alpha = \beta) \lor (\beta \in \alpha)$. This determines whether the relation is trichotomous. And this in turn affects the proof theoretic strength defined in ordinal analysis.

Metalogic

As in the study of constructive arithmetic theories, constructive set theories can exhibit attractive disjunction and existence properties. These are features of a fixed theory which relate metalogical judgements and propositions provable in the theory. Particularly well-studied are those such features that can be expressed in Heyting arithmetic, with quantifiers over numbers and which can often be realized by numerals, as formalized in proof theory. In particular, those are the numerical existence property and the closely related disjunctive property, as well as being closed under Church's rule, witnessing any given function to be computable.

A set theory does not only express theorems about numbers. Furthermore, one may consider a more general strong existence property that is harder to come by, as will be discussed. The theory has the property if the following can be established: For any property $\phi$, if the theory proves that a set exist that has that property, i.e. if the theory claims the existence statement, then there is also a property $\psi$ that uniquely describes such a set instance. More formally, for any predicate $\phi$ there is a predicate $\psi$ so that
:$\vdash\exists x.\phi(x)\implies\vdash\exists !x. \phi(x)\land\psi(x)$
The analogous role of the realized numeral is played by defined sets proven to exist according to the theory, and so this is a subtle question concerning term construction and the theories strength. While many theories discussed tend have all the various numerical properties, the existence property can easily be spoiled, as will be discussed. Weaker forms of existence properties have been formulated.

Some classical theories can in fact also be constrained to exhibit the strong existence property. Zermelo–Fraenkel set theory $$ with the constructible universe postulate, $+(=)$, or $$ with sets all taken to be ordinal-definable, $+(=)$, do have the existence property. For contrast, consider the theory $$ given by $$ plus the full axiom of choice ''existence postulate''. Recall that this set of axioms implies the well-ordering theorem, which in particular means that relations for $$ that establish its well-ordering are formally proven to exist (and claim existence of a least element for all subsets of $$ with respect to those relations). This is despite that fact that definability of such an ordering is known to be independent of $$. The latter implies that for no particular formula $\psi$ in the language of the theory does the theory prove that the corresponding set is a well-ordering relation of the reals. So $$ formally ''proves the existence'' of a subset $x\subset\times$ with the property of being a well-ordering relation, but at the same time no particular set $x$ for which the property could be validated can possibly be defined.

Anti-classical principles

A situation commonly studied is that of a fixed theory $$ exhibiting the following meta-theoretical property: For an instance from some collection of formulas, here captured via $\phi$ and $\psi$, one established the existence of a numeral constant $e$ so that $\vdash \phi\implies\vdash \psi(e)$. When adopting such a schema as an inference rule and nothing new can be proven, one says the theory $$ is closed under that rule. Adjoining excluded middle $$ to $$, the new theory may then prove new, strictly classical statements for $\phi$ and this may spoil the meta-theoretical property that was previously established for $$.
One may instead consider adjoining the rule corresponding to the meta-theoretical property as an implication to $$, as a schema or in quantified form. That is to say, to postulate that any such $\phi$ implies $\exists (e\in)$ such that $\psi(e)$ holds, where the bound $e$ is a number variable in language of the theory. The new theory with the principle added might be anti-classical, in that it may not be consistent anymore to also adopt $$.
For example, Church's rule is an admissible rule in Heyting arithmetic $$ and the corresponding Church's thesis principle may be adopted, but the same is not possible in $+$, also known as Peano arithmetic $$.

Now for a context of set theories with quantification over a fully formal notion of an infinite sequences space, i.e. function spaces, as will be defined below. A translation of Church's ''rule'' into the language of the theory itself may then read
:$\forall (f\in^).\exists (e\in).\Big(\forall(n\in).\exists(w\in). T(e, n, w)\land U(w, f(n))\Big)$
Kleene's T predicate together with the result extraction expresses that any input number $n$ being mapped to the number $f(n)$ is, through $w$, witnessed to be a computable mapping. Here $$ now denotes a set theory model of the standard natural numbers and $e$ is an index with respect to a fixed program enumeration. Stronger variants have been used, which extend this principle to functions $f\in^X$ defined on domains $X\subset$ of low complexity. The principle rejects decidability for the predicate $Q(e)$ defined as $\exists(w\in). T(e, e, w)$, expressing that $e$ is the index of a computable function halting on its own index. Weaker, double negated forms of the principle may be considered too, which do not require the existence of a recursive implementation for every $f$, but which still make principles inconsistent that claim the existence of functions which provenly have no recursive realization. Some forms of a Church's thesis as principle are even consistent with the weak classical second order arithmetic $_0$.

The collection of total, computable functions is classically subcountable, which classically is the same as being countable. But classical set theories will generally claim that $^$ holds also other functions than the computable ones. For example there is a proof in $$ that total functions do exist that cannot be captured by a Turing machine.
Taking the computable world seriously as ontology, a prime example of an anti-classical conception related the Markovian school is the permitted subcountability of various uncountable collections. Adopting the subcountability of the collection of all unending sequences of natural numbers ($^$) as an axiom, the "smallness" (in classical terms) of this collection in some realizations of a set theory is then already captured by that theory.
A constructive theory may also adopt neither classical nor anti-classical axioms and so stay agnostic towards either possibility.

Constructive principles already prove $\forall (x\in X).\neg\neg\big(Q(x) \lor \neg Q(x)\big)$ and so for any given element $x$ of $X$, the corresponding excluded middle statement for the proposition cannot be negated. Indeed, for any given $x$, by noncontradiction it is impossible to rule out $Q(x)$ and rule out its negation both at once. But a theory may in some instances also permit the rejection claim $\neg\forall (x\in X). \big(Q(x) \lor \neg Q(x)\big)$. Adopting this does not necessitate providing a particular $t\in X$ witnessing the failure of excluded middle for the particular proposition $Q(t)$, i.e. witnessing the inconsistent $\neg\big(Q(t)\lor\neg Q(t)\big)$. One may reject the possibility of decidability of some predicate $Q(x)$ on an infinite domain $X$ without making any existence claim in $X$.
As another example, such a situation is enforced in Brouwerian intuitionistic analysis, in a case where the quantifier ranges over infinitely many unending binary sequences and $Q(x)$ states that a sequence $x$ is everywhere zero. Concerning this property, of being conclusively identified as the sequence which is forever constant, adopting Brouwer's continuity principle rules out that this could be proven decidable for all the sequences.

So in a constructive context with a so-called non-classical logic as used here, one may consistently adopt axioms which are both in contradiction to quantified forms of excluded middle, but also non-constructive in the computable sense or as gauged by meta-logical existence properties discussed previously. In that way, a constructive set theory can also provide the framework to study non-classical theories.

History and overview

Historically, the subject of constructive set theory (often also "$$") begun with John Myhill's work on the theories also called $$ and $$.
In 1973, he had proposed the former as a first-order set theory based on intuitionistic logic, taking the most common foundation $$ and throwing out the Axiom of choice as well as the principle of the excluded middle, initially leaving everything else as is. However, different forms of some of the $$ axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply $$, as will be demonstrated. In those cases, the intuitionistically weaker formulations were consequently adopted. The far more conservative system $$ is also a first-order theory, but of several sorts and bounded quantification, aiming to provide a formal foundation for Errett Bishop's program of constructive mathematics.

The main discussion presents sequence of theories in the same language as $$, leading up to Peter Aczel's well studied ''$$'', and beyond. Many modern results trace back to Rathjen and his students.
$$ is also characterized by the two features present also in Myhill's theory:
On the one hand, it is using the Predicative Separation instead of the full, unbounded Separation schema, see also Lévy hierarchy.
Boundedness can be handled as a syntactic property or, alternatively, the theories can be conservatively extended with a higher boundedness predicate and its axioms. Secondly, the impredicative Powerset axiom

HOME


Content is Copyleft
Website design, code, and AI is Copyrighted (c) 2014-2017 by Stephen Payne


Consider donating to Wikimedia



As an Amazon Associate I earn from qualifying purchases