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, motivated by results tied to impredicativity. 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.