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, 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 . 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, 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 (and/or ) in the sense that they prove excluded middle for (resp. the statement using the quantifier above) without demonstrating the truth of either side of the disjunction(s). 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 (for example, by demonstrating one of the disjuncts, thus deciding ) 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.