Constructive set theory
Axiomatic constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory.
The same first-order language with "" and "" 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 set bounded. The latter is motivated by results tied to impredicativity.
Introduction
Constructive outlook
Preliminary on the use of intuitionistic logic
The logic of the set theories discussed here is constructive in that it rejects the principle of excluded middle, i.e. that the disjunction automatically holds for all propositions. This is also often called the law of excluded middle in contexts where it is assumed. Constructively, as a rule, to prove the excluded middle for a proposition, i.e. to prove the particular disjunction, either or 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 and more commonly, a predicate for in a domain is said to be decidable when the more intricate statement is provable. Non-constructive axioms may enable proofs that formally claim decidability of such in the sense that they prove excluded middle for without demonstrating the truth of either side of the disjunction. This is often the case in classical logic. In contrast, axiomatic theories deemed constructive tend to not permit many classical proofs of statements involving properties that are provenly computationally undecidable.The law of noncontradiction is a special case of the propositional form of modus ponens. Using the former with any negated statement, one valid De Morgan's law thus implies already in the more conservative minimal logic. 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. Here the double-negation captures that the disjunction statement now provenly can never be ruled out or rejected, even in cases where the disjunction may not be provable from the assumed axioms.
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.
The intuitionistic logic underlying the set theories discussed here, unlike minimal logic, still permits double negation elimination for individual propositions for which excluded middle holds. In turn the theorem formulations regarding finite objects tends to not differ from their classical counterparts. Given a model of all natural numbers, the equivalent for predicates, namely Markov's principle, does not automatically hold, but may be considered as an additional principle.
In an inhabited domain and using explosion, the disjunction implies the existence claim, which in turn implies. Classically, these implications are always reversible. If one of the former is classically valid, it can be worth trying to establish it in the latter form. For the special case where is rejected, one deals with a counter-example existence claim, which is generally constructively stronger than a rejection claim : Exemplifying a such that is contradictory of course means it is not the case that holds for all possible. But one may also demonstrate that holding for all would logically lead to a contradiction without the aid of a specific counter-example, and even while not being able to construct one. In the latter case, constructively, here one does not stipulate an existence claim.
Imposed restrictions on a set theory
Compared to the classical counterpart, one is generally less likely to prove the existence of relations that cannot be realized. A restriction to the constructive reading of existence apriori leads to stricter requirements regarding which characterizations of a set involving unbounded collections constitute a function. This is often because the predicate in a case-wise would-be definition may not be decidable. Adopting the standard definition of set equality via extensionality, 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 existence claim, as shown below. The latter has a classically equivalent inductive substitute.So a genuinely intuitionistic development of set theory requires the rewording of some standard axioms to classically equivalent ones. Apart from demands for computability and reservations regrading of impredicativity, technical question regarding which non-logical axioms effectively extend the underlying logic of a theory is also a research subject in its own right.
Metalogic
With computably undecidable propositions already arising in Robinson arithmetic, even just Predicative separation lets one define elusive subsets easily. In stark contrast to the classical framework, constructive set theories may be closed under the rule that any property that is decidable for all sets is already equivalent to one of the two trivial ones, or. Also the real line may be taken to be indecomposable in this sense. 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. This determines whether the relation is trichotomous. A weakened theory of ordinals in turn affects the proof theoretic strength defined in ordinal analysis.In exchange, constructive set theories can exhibit attractive disjunction and existence properties, as is familiar from the study of constructive arithmetic theories. These are features of a fixed theory which metalogically relate judgements of 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 numbers, 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, and so one may consider a more general so-called strong existence property that is harder to come by, as will be discussed. A theory has this property if the following can be established: For any property, 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 that uniquely describes such a set instance. More formally, for any predicate there is a predicate so that
The role analogous to that of realized numbers in arithmetic is played here by defined sets proven to exist by the theory. Questions concerning the axiomatic set theory's strength and its relation to term construction are subtle. 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 theories with a classical reading of existence can in fact also be constrained so as to exhibit the strong existence property. In Zermelo–Fraenkel set theory with sets all taken to be ordinal-definable, a theory denoted, no sets without such definability exist. The property is also enforced via the constructible universe postulate in.
For contrast, consider the theory given by plus the full axiom of choice existence postulate: Recall that this collection of axioms proves the well-ordering theorem, implying well-orderings exists for any set. In particular, this means that relations formally exist that establish the well-ordering of . This is despite the fact that definability of such an ordering is known to be independent of. The latter implies that for no particular formula 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 with the property of being a well-ordering relation, but at the same time no particular set for which the property could be validated can possibly be defined.
Anti-classical principles
As mentioned above, a constructive theory may exhibit the numerical existence property,, for some number and where denotes the corresponding numeral in the formal theory. Here one must carefully distinguish between provable implications between two propositions,, and a theory's properties of the form. When adopting a metalogically established schema of the latter type as an inference rule of one's proof calculus and nothing new can be proven, one says the theory is closed under that rule.One may instead consider adjoining the rule corresponding to the meta-theoretical property as an implication to, as an axiom schema or in quantified form. A situation commonly studied is that of a fixed exhibiting the meta-theoretical property of the following type: For an instance from some collection of formulas of a particular form, here captured via and, one established the existence of a number so that. Here one may then postulate, where the bound is a number variable in language of the theory. For example, Church's rule is an admissible rule in first-order Heyting arithmetic and, furthermore, the corresponding Church's thesis principle may consistently be adopted as an axiom. The new theory with the principle added is anti-classical, in that it may not be consistent anymore to also adopt. Similarly, adjoining the excluded middle principle to some theory, the theory thus obtained may prove new, strictly classical statements, and this may spoil some of the meta-theoretical properties that were previously established for. In such a fashion, may not be adopted in, also known as Peano arithmetic.
The focus in this subsection shall be on set theories with quantification over a fully formal notion of an infinite sequences space, i.e. function space, as it will be introduced further below.
A translation of Church's rule into the language of the theory itself may here read
Kleene's T predicate together with the result extraction expresses that any input number being mapped to the number is, through, witnessed to be a computable mapping. Here now denotes a set theory model of the standard natural numbers and is an index with respect to a fixed program enumeration. Stronger variants have been used, which extend this principle to functions defined on domains of low complexity. The principle rejects decidability for the predicate defined as, expressing that 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, 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 classical, weak so called second-order arithmetic theory, a subsystem of the two-sorted first-order theory.
The collection of 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. When adopting the subcountability of the collection of all unending sequences of natural numbers as an axiom in a constructive theory, the "smallness" of this collection, in some set theoretical realizations, is then already captured by the theory itself.
A constructive theory may also adopt neither classical nor anti-classical axioms and so stay agnostic towards either possibility.
Constructive principles already prove for any. And so for any given element of, the corresponding excluded middle statement for the proposition cannot be negated. Indeed, for any given, by noncontradiction it is impossible to rule out and rule out its negation both at once, and the relevant De Morgan's rule applies as above. But a theory may in some instances also permit the rejection claim. Adopting this does not necessitate providing a particular witnessing the failure of excluded middle for the particular proposition, i.e. witnessing the inconsistent. Predicates on an infinite domain correspond to decision problems. Motivated by provenly computably undecidable problems, one may reject the possibility of decidability of a predicate without also making any existence claim in.
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 states that a sequence is everywhere zero. Concerning this property, of being conclusively identified as the sequence which is forever constant, adopting Brouwer's continuity principle strictly 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, say rings modeling smooth infinitesimal analysis.