HOME

TheInfoList



OR:

Constructive set theory is an approach to
mathematical constructivism In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove th ...
following the program of
axiomatic set theory Set theory is the branch of mathematical logic that studies Set (mathematics), sets, which can be informally described as collections of objects. Although objects of any kind can be collected into a set, set theory, as a branch of mathematics, ...
. The same
first-order In mathematics and other formal sciences, first-order or first order most often means either: * "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of high ...
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 Boundedness or bounded may refer to: Economics * Bounded rationality, the idea that human rationality in decision-making is bounded by the available information, the cognitive limitations, and the time available to make the decision * Bounded e ...
, motivated by results tied to
impredicativity In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
.


Introduction


Constructive outlook


Use of intuitionistic logic

The logic of the set theories discussed here is
constructive Although the general English usage of the adjective constructive is "helping to develop or improve something; helpful to someone, instead of upsetting and negative," as in the phrase "constructive criticism," in legal writing ''constructive'' has ...
in that it rejects , i.e. that the
disjunction In logic, disjunction is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is raining or it is snowing" can be represented in logic using the disjunctive formula R \lor S ...
\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 Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
underlying the set theories discussed here, unlike the more conservative
minimal logic Minimal logic, or minimal calculus, is a symbolic logic system originally developed by Ingebrigt Johansson. It is an intuitionistic and paraconsistent logic, that rejects both the law of the excluded middle as well as the principle of explosion (' ...
, still permits
double negation elimination In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition ''A'' is logically equivalent to ''not (not ...
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 Markov's principle, named after Andrey Markov Jr, is a conditional existence statement for which there are many equivalent formulations, as discussed below. The principle is logically valid classically, but not in intuitionistic constructive m ...
, does not automatically hold, but may be considered as an additional principle. Expressing the instance for \neg P of the valid
law of noncontradiction In logic, the law of non-contradiction (LNC) (also known as the law of contradiction, principle of non-contradiction (PNC), or the principle of contradiction) states that contradictory propositions cannot both be true in the same sense at the sa ...
and using a valid
De Morgan's law In propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both valid rules of inference. They are named after Augustus De Morgan, a 19th-century British mathem ...
, 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 In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics. This contrasts with ''classical analysis'', which (in this context) simply means analysis done according to the (more comm ...
, one cannot prove the
intermediate value theorem In mathematical analysis, the intermediate value theorem states that if f is a continuous function whose domain contains the interval , then it takes on any given value between f(a) and f(b) at some point within the interval. This has two import ...
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 Total may refer to: Mathematics * Total, the summation of a set of numbers * Total order, a partial order without incomparable pairs * Total relation, which may also mean ** connected relation (a binary relation in which any two elements are comp ...
) 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 In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...
is such a non-constructive principle that implies for the formulas permitted in one's adopted Separation schema, by
Diaconescu's theorem In mathematical logic, Diaconescu's theorem, or the Goodman–Myhill theorem, states that the full axiom of choice is sufficient to derive the law of the excluded middle, or restricted forms of it, in constructive set theory. It was discovered in 19 ...
. Similar results hold for the
Axiom of Regularity In mathematics, the axiom of regularity (also known as the axiom of foundation) is an axiom of Zermelo–Fraenkel set theory that states that every non-empty set ''A'' contains an element that is disjoint from ''A''. In first-order logic, the axi ...
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 In set theory, an ordinal number, or ordinal, is a generalization of ordinal numerals (first, second, th, etc.) aimed to extend enumeration to infinite sets. A finite set can be enumerated by successively labeling each element with the least n ...
, 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 In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has ...
.


Metalogic

As in the study of constructive arithmetic theories, constructive set theories can exhibit attractive
disjunction and existence properties In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005). Disjunction property The disjunction property is satisfi ...
. 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 In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano a ...
, with quantifiers over numbers and which can often be realized by numerals, as formalized in
proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...
. 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 Computability is the ability to solve a problem in an effective manner. It is a key topic of the field of computability theory within mathematical logic and the theory of computation within computer science. The computability of a problem is close ...
. 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 In set theory, Zermelo–Fraenkel set theory, named after mathematicians Ernst Zermelo and Abraham Fraenkel, is an axiomatic system that was proposed in the early twentieth century in order to formulate a theory of sets free of paradoxes such as ...
with the
constructible universe In mathematics, in set theory, the constructible universe (or Gödel's constructible universe), denoted by , is a particular class of sets that can be described entirely in terms of simpler sets. is the union of the constructible hierarchy . It w ...
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 In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...
''existence postulate''. Recall that this set of axioms implies the
well-ordering theorem In mathematics, the well-ordering theorem, also known as Zermelo's theorem, states that every set can be well-ordered. A set ''X'' is ''well-ordered'' by a strict total order if every non-empty subset of ''X'' has a least element under the orde ...
, 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 Knowledge can be defined as awareness of facts or as practical skills, and may also refer to familiarity with objects or situations. Knowledge of facts, also called propositional knowledge, is often defined as true belief that is distinc ...
to be
independent Independent or Independents may refer to: Arts, entertainment, and media Artist groups * Independents (artist group), a group of modernist painters based in the New Hope, Pennsylvania, area of the United States during the early 1930s * Independ ...
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 The word schema comes from the Greek word ('), which means ''shape'', or more generally, ''plan''. The plural is ('). In English, both ''schemas'' and ''schemata'' are used as plural forms. Schema may refer to: Science and technology * 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 logic, a rule of inference is admissible in a formal system if the set of theorems of the system does not change when that rule is added to the existing rules of the system. In other words, every formula that can be derived using that rule is ...
in
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano a ...
and the corresponding Church's thesis principle may be adopted, but the same is not possible in +, also known as
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
. 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 In computability theory, the T predicate, first studied by mathematician Stephen Cole Kleene, is a particular set of triples of natural numbers that is used to represent computable functions within formal theories of arithmetic. Informally, the ''T ...
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 A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
. 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 Non-classical logics (and sometimes alternative logics) are formal systems that differ in a significant way from standard logical systems such as propositional and predicate logic. There are several ways in which this is done, including by way of ...
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 John R. Myhill Sr. (11 August 1923 – 15 February 1987) was a British mathematician. Education Myhill received his Ph.D. from Harvard University under Willard Van Orman Quine in 1949. He was professor at SUNY Buffalo from 1966 until his death ...
'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 Errett Albert Bishop (July 14, 1928 – April 14, 1983) was an Americans, American mathematician known for his work on analysis. He expanded constructive analysis in his 1967 ''Foundations of Constructive Analysis'', where he Mathematical proof, p ...
's program of constructive mathematics. The main discussion presents sequence of theories in the same language as , leading up to
Peter Aczel Peter Henry George Aczel (; born 31 October 1941) is a British mathematician, logician and Emeritus joint Professor in the Department of Computer Science and the School of Mathematics at the University of Manchester. He is known for his work in n ...
'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 In set theory and mathematical logic, the Lévy hierarchy, introduced by Azriel Lévy in 1965, is a hierarchy of formulas in the formal language of the Zermelo–Fraenkel set theory, which is typically called just the language of set theory. This i ...
. 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 In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
Powerset axiom is discarded, generally in favor of related but weaker axioms. The strong form is very casually used in classical
general topology In mathematics, general topology is the branch of topology that deals with the basic set-theoretic definitions and constructions used in topology. It is the foundation of most other branches of topology, including differential topology, geomet ...
. Adding to a theory even weaker than recovers , as detailed below. The system, which has come to be known as Intuitionistic Zermelo–Fraenkel set theory (), is a strong set theory without . It is similar to , but less conservative or predicative. The theory denoted is the constructive version of , the classical
Kripke–Platek set theory The Kripke–Platek set theory (KP), pronounced , is an axiomatic set theory developed by Saul Kripke and Richard Platek. The theory can be thought of as roughly the predicative part of ZFC and is considerably weaker than it. Axioms In its fo ...
without a form of Powerset and where even the Axiom of Collection is bounded.


Models

As far as constructive realizations go there is a relevant
realizability In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way t ...
theory. Relatedly, Aczel's theory constructive Zermelo-Fraenkel has been interpreted in a Martin-Löf type theories, as described below. In this way, set theory theorems provable in and weaker theories are candidates for a computer realization. For a set theory context without infinite sets, constructive first-order arithmetic can also be taken as an apology for most axioms adopted in : The arithmetic theory is bi-interpretable with a weak constructive set theory, as described in the article on
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano a ...
. One may arithmetically characterize a membership relation "\in" and with it prove - instead of the existence of a set of natural numbers \omega - that all sets in its theory are in bijection with a (finite) von Neumann natural, a principle denoted =. This context further validates Extensionality, Pairing, Union, Binary Intersection (which is related to the
Axiom schema of predicative separation In axiomatic set theory, the axiom schema of predicative separation, or of restricted, or Δ0 separation, is a schema of axioms which is a restriction of the usual axiom schema of separation in Zermelo–Fraenkel set theory. This name &Del ...
) and the Set Induction schema. Taken as axioms, the aforementioned principles constitute a set theory that is already identical with the theory given by minus the existence of \omega but plus = as axiom. All those axioms are discussed in detail below. Relatedly, also proves that the hereditarily finite sets fulfill all the previous axioms. This is a result which persists when passing on to and minus Infinity. Many theories studied in constructive set theory are mere restrictions of Zermelo–Fraenkel set theory () with respect to their axiom as well as their underlying logic. Such theories can then also be interpreted in any model of . More recently,
presheaf In mathematics, a sheaf is a tool for systematically tracking data (such as sets, abelian groups, rings) attached to the open sets of a topological space and defined locally with regard to them. For example, for each open set, the data could ...
models for constructive set theories have been introduced. These are analogous to presheaf models for intuitionistic set theory developed by
Dana Scott Dana Stewart Scott (born October 11, 1932) is an American logician who is the emeritus Hillman University Professor of Computer Science, Philosophy, and Mathematical Logic at Carnegie Mellon University; he is now retired and lives in Berkeley, Ca ...
in the 1980s.


Subtheories of ZF


Notation


Language

The propositional connective symbols used to form syntactic formulas are standard. The axioms of set theory give a means to prove equality "=" of sets and that symbol may, by
abuse of notation In mathematics, abuse of notation occurs when an author uses a mathematical notation in a way that is not entirely formally correct, but which might help simplify the exposition or suggest the correct intuition (while possibly minimizing errors an ...
, be used for classes. Negation "\neg" of elementhood "\in" is often written "\notin", and usually the same goes for non-equality "\neq", although in constructive mathematics the latter symbol is also used in the context with apartness relations.


Variables

Below the Greek \phi denotes a predicate variable in
axiom schema In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom. Formal definition An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables ap ...
s and P or Q is used for particular predicates. The word "predicate" is often used interchangeably with "formulas" as well, even in the unary case. Quantifiers range over sets and those are denoted by lower case letters. As is common, one may use argument brackets to express predicates, for the sake of highlighting particular free variables in their syntactic expression, as in "P(z)". One abbreviates \forall z. \big(z\in A\to P(z)\big) by \forall (z\in A). P(z) and \exists z. \big(z\in A\land P(z)\big) by \exists (z\in A). P(z). The syntactic notion of bounded quantification in this sense can play a role in the formulation of axiom schemas, as seen below. Express the subclass claim \forall (z\in A). z\in B, i.e. \forall z. (z\in A\to z\in B), by A\subset B. The similar notion of subset-bounded quantifiers, as in \forall (z\subset A). z\in B, has been used in set theoretical investigation as well, but will not be further highlighted here. Unique existence \exists!x. P(x) here means \exists x. \forall y. \big(y=x \leftrightarrow P(y)\big).


Classes

As is also common in the study of set theories, one makes use set builder notation for classes, which, in most contexts, are not part of the object language but used for concise discussion. In particular, one may introduce notation declarations of the corresponding class via "A=\", for the purpose of expressing P(a) as a\in A. Logically equivalent predicates can be used to introduce the same class. One also writes \ as shorthand for \. For a property P, trivially \forall z.\big((z\in B\land P(z))\to z\in B\big). And so follows that \\subset B.


Equality

Denote by A\simeq B the statement expressing that two classes have exactly the same elements, i.e. \forall z. (z\in A \leftrightarrow z\in B), or equivalently (A\subset B)\land (B\subset A). This is not to be conflated with the concept of
equinumerosity In mathematics, two sets or classes ''A'' and ''B'' are equinumerous if there exists a one-to-one correspondence (or bijection) between them, that is, if there exists a function from ''A'' to ''B'' such that for every element ''y'' of ''B'', ther ...
. The following axiom gives a means to prove equality "=" of two ''sets'', so that through substitution, any predicate about x translates to one of y. By the logical properties of equality, the converse direction holds automatically. In a constructive interpretation, the elements of a subclass A=\ of B may come equipped with more information than those of B, in the sense that being able to judge b\in A is being able to judge Q(b)\lor\neg Q(b). And (unless the whole disjunction follows from axioms) in the
Brouwer–Heyting–Kolmogorov interpretation In mathematical logic, the Brouwer–Heyting–Kolmogorov interpretation, or BHK interpretation, of intuitionistic logic was proposed by L. E. J. Brouwer and Arend Heyting, and independently by Andrey Kolmogorov. It is also sometimes called the real ...
, this means to have proven Q(b) or having rejected it. As Q may be not decidable for all elements in B, the two classes must a priori be distinguished. Consider a property P that provenly holds for all elements of a set y, so that \\simeq y, and assume that the class on the left hand side is established to be a set. Note that, even if this set on the left informally also ties to proof-relevant information about the validity of P for all the elements, the Extensionality axiom postulates that, in our set theory, the set on the left hand side is judged equal to the one on the right hand side. While often adopted, this axiom has been criticized in constructive thought, as it effectively collapses differently defined properties, or at least the sets viewed as the extension of these properties, a Fregian notion. Modern type theories may instead aim at defining the demanded equivalence "\simeq" in terms of functions, see e.g. type equivalence. The related concept of function
extensionality In logic, extensionality, or extensional equality, refers to principles that judge objects to be equal if they have the same external properties. It stands in contrast to the concept of intensionality, which is concerned with whether the internal ...
is often not adopted in type theory. Other frameworks for constructive mathematics might instead demand a particular rule for equality or apartness come for the elements z\in x of each and every set x discussed. Even then, the above definition can be used to characterize equality of
subsets In mathematics, set ''A'' is a subset of a set ''B'' if all elements of ''A'' are also elements of ''B''; ''B'' is then a superset of ''A''. It is possible for ''A'' and ''B'' to be equal; if they are unequal, then ''A'' is a proper subset of ...
u\subset x and v\subset x. Note that adopting "=" as a symbol in a predicate logic theory makes equality of two terms a quantifier-free expression.


Merging sets

Two other basic axioms are as follows. Firstly, saying that for any two sets x and y, there is at least one set p, which hold at least those two sets (z). And then, saying that for any set x, there is at least one set u, which holds all members y, of x's members z. The two axioms may also be formulated stronger in terms of "\leftrightarrow". In the context of with Separation, this is not necessary. Together, the two previous axioms imply the existence of the binary union of two classes a and b when they have been established to be sets, and this is denoted by \bigcup\ or a\cup b. For a fixed set y, to validate membership y\in a\cup b in the union of two given sets z=a and z=b, one needs to validate the y\in z part of the axiom, which can be done by validating the disjunction of the predicates defining the sets a and b, for y. Define class notation for a few given elements via disjunctions, e.g. c\in\ says (c=a)\lor(c=b). Denote by \langle x, y\rangle the standard
ordered pair In mathematics, an ordered pair (''a'', ''b'') is a pair of objects. The order in which the objects appear in the pair is significant: the ordered pair (''a'', ''b'') is different from the ordered pair (''b'', ''a'') unless ''a'' = ''b''. (In con ...
model \.


Set existence

The property that is false for any set corresponds to the empty class, which is denoted by \ or zero, 0. That the empty class is a set readily follows from other axioms, such as the Axiom of Infinity below. But if, e.g., one is explicitly interested in excluding infinite sets in one's study, one may at this point adopt the This axiom would also readily be accepted, but is not relevant in the context of stronger axioms below. Introduction of the symbol \ (as abbreviating notation for expressions in involving characterizing properties) is justified as uniqueness for this set can be proven. If there provenly ''exists'' a set t\in s inside a set s, then we call s ''inhabited'' and it is then provenly not the empty set. While classically equivalent, constructively ''non-empty'' is a weaker notion with two negations. Unfortunately, the word for the more useful notion of 'inhabited' is rarely used in classical mathematics. For a set x, define the successor set Sx as x\cup\, for which x\in Sx. A sort of blend between pairing and union, an axiom more readily related to the successor is the
Axiom of adjunction In mathematical set theory, the axiom of adjunction states that for any two sets ''x'', ''y'' there is a set ''w'' = ''x'' âˆª  given by "adjoining" the set ''y'' to the set ''x''. : \forall x \,\forall y \,\exists w \,\forall z ...
. It is relevant for the standard modeling of individual Neumann ordinals. A simple and provenly false proposition then is, for example, \\in\, corresponding to 0 < 0 in the standard arithmetic model. Again, here symbols such as \ are treated as convenient notation and any proposition really translates to an expression using only "\in" and logical symbols, including quantifiers. Accompanied by a metamathematical analysis that the capabilities of the new theories are equivalent in an effective manner, formal extensions by symbols such as 0 may also be considered.


BCST

The following makes use of
axiom schema In mathematical logic, an axiom schema (plural: axiom schemata or axiom schemas) generalizes the notion of axiom. Formal definition An axiom schema is a formula in the metalanguage of an axiomatic system, in which one or more schematic variables ap ...
s, i.e. axioms for some collection of predicates. Note that some of the stated axiom schemas are often presented with set parameters v as well, i.e. variants with extra universal closures \forall v such that the \phi's may depend on the parameters.


Separation

Basic constructive set theory consists of several axioms also part of standard set theory, except the Separation axiom is weakened. Beyond the four axioms above, it the Predicative Separation as well as the Replacement schema. This axiom amounts to postulating the existence of a set s obtained by the intersection of any set y and any predicatively described class \. When the predicate is taken as x\in z for z proven to be a set, one obtains the binary intersection of sets and writes s=y\cap z. Intersection corresponds to conjunction in an analog way to how union corresponds to disjunction. As noted, from Separation and the existence of at least one set (e.g. Infinity below) and a predicate that is false of any set, like \neg(x=x), will follow the existence of the empty set. Within this conservative context of , the Bounded Separation schema is actually equivalent to Empty Set plus the existence of the binary intersection for any two sets. The latter variant of axiomatization does not make use of a formula schema. The axiom schema is also called Bounded Separation, as in Separation for set-
bounded quantifiers In the study of formal theories in mathematical logic, bounded quantifiers (a.k.a. restricted quantifiers) are often included in a formal language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and " ...
only. It is a schema that takes into account syntactic aspects of predicates. The scope of legal formulas is enriched by further set existence postulates. The bounded formulas are also denoted by \Delta_0 in the set theoretical Lévy hierarchy, in analogy to \Delta_0^0 in the
arithmetical hierarchy In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
. (Note however that the arithmetic classification is sometimes expressed not syntactically but in terms of subclasses of the naturals. Also, the bottom level of the arithmetical hierarchy has several common definitions, some not allowing the use of some total functions. The distinction is not relevant on the level \Sigma_1^0 or higher.) The schema is also the way in which
Mac Lane Saunders Mac Lane (4 August 1909 – 14 April 2005) was an American mathematician who co-founded category theory with Samuel Eilenberg. Early life and education Mac Lane was born in Norwich, Connecticut, near where his family lived in Taftville ...
weakens a system close to
Zermelo set theory Zermelo set theory (sometimes denoted by Z-), as set out in a seminal paper in 1908 by Ernst Zermelo, is the ancestor of modern Zermelo–Fraenkel set theory (ZF) and its extensions, such as von Neumann–Bernays–Gödel set theory (NBG). It be ...
, for mathematical foundations related to
topos theory In mathematics, a topos (, ; plural topoi or , or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally: on a site). Topoi behave much like the category of sets and possess a notion ...
.


No universal set

The following holds for any relation E, giving a purely logical condition by which two terms s and y non-relatable :\forall x. \big(xEs\leftrightarrow(xEy \land \neg xEx)\big) \to \neg(yEs\lor sEs\lor sEy) The expression \neg(x\in x) is a bounded one and thus allowed in separation. By virtue of the rejection of the final disjunct above, \neg sEy, Russel's construction shows that \\notin y. So for any set y, Predicative Separation alone implies that there exists a set which is not a member of y. In particular, no
universal set In set theory, a universal set is a set which contains all objects, including itself. In set theory as usually formulated, it can be proven in multiple ways that a universal set does not exist. However, some non-standard variants of set theory inc ...
can exist in this theory. In a theory with the
axiom of regularity In mathematics, the axiom of regularity (also known as the axiom of foundation) is an axiom of Zermelo–Fraenkel set theory that states that every non-empty set ''A'' contains an element that is disjoint from ''A''. In first-order logic, the axi ...
, like , of course that subset \ can be proven to be equal to y itself. As an aside, in a theory with
stratification Stratification may refer to: Mathematics * Stratification (mathematics), any consistent assignment of numbers to predicate symbols * Data stratification in statistics Earth sciences * Stable and unstable stratification * Stratification, or str ...
, a universal set may exist because use of the syntactic expression x\in x may be disallowed in proofs of existence by, essentially, separation.


Predicativity

The restriction in the axiom is also gatekeeping
impredicative In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
definitions: Existence should at best not be claimed for objects that are not explicitly describable, or whose definition involves themselves or reference to a proper class, such as when a property to be checked involves a universal quantifier. So in a constructive theory without
Axiom of power set In mathematics, the axiom of power set is one of the Zermelo–Fraenkel axioms of axiomatic set theory. In the formal language of the Zermelo–Fraenkel axioms, the axiom reads: :\forall x \, \exists y \, \forall z \, \in y \iff \forall w \ ...
, when Q denotes some 2-ary predicate, one should not generally expect a subclass s of y to be a set, in case that it is defined, for example, as in :\, or via a similar definitions involving any quantification over the sets t\subset y. Note that if this subclass s of y is provenly a set, then this subset itself is also in the unbounded scope of set variable t. In other words, as the subclass property s\subset y is fulfilled, this exact set s, defined using the expression Q(x, s), would play a role in its own characterization. While predicative Separation leads to fewer given class definitions being sets, it must be emphasized that many class definitions that are classically equivalent are not so when restricting oneself to constructive logic. So in this way, one gets a broader theory, constructively. Due to the potential undecidability of general predicates, the notion of subset and subclass is more elaborate in constructive set theories than in classical ones. This remains true if full Separation is adopted, as in the theory , which however spoils the
existence property In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005). Disjunction property The disjunction property is satisfi ...
as well as the standard type theoretical interpretations, and in this way spoils a bottom-up view of constructive sets. As an aside, as
subtyping In programming language theory, subtyping (also subtype polymorphism or inclusion polymorphism) is a form of type polymorphism in which a subtype is a datatype that is related to another datatype (the supertype) by some notion of substitutabilit ...
is not a necessary feature of
constructive type theory Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and ph ...
, constructive set theory can be said to quite differ from that framework.


Replacement

Next consider the It is granting existence, as sets, of the range of function-like predicates, obtained via their domains. In the above formulation, the predicate is not restricted akin to the Separation schema, but this axiom already involves an existential quantifier in the antecedent. Of course, weaker schemas could be considered as well. With the Replacement schema, this theory proves that the
equivalence classes In mathematics, when the elements of some set S have a notion of equivalence (formalized as an equivalence relation), then one may naturally split the set S into equivalence classes. These equivalence classes are constructed so that elements ...
or indexed sums are sets. In particular, the
Cartesian product In mathematics, specifically set theory, the Cartesian product of two sets ''A'' and ''B'', denoted ''A''×''B'', is the set of all ordered pairs where ''a'' is in ''A'' and ''b'' is in ''B''. In terms of set-builder notation, that is : A\ti ...
, holding all pairs of elements of two sets, is a set. Equality of elements inside a set x is decidable if the corresponding relation as a subset of x\times x is decidable. Replacement is not necessary in the design of a weak constructive set theory that is bi-interpretable with
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano a ...
. However, some form of induction is. Replacement together with Set Induction (introduced below) also suffices to axiomize hereditarily finite sets constructively and that theory is also studied without Infinity. For comparison, consider the very weak classical theory called
General set theory General set theory (GST) is George Boolos's (1998) name for a fragment of the axiomatic set theory Z. GST is sufficient for all mathematics not requiring infinite sets, and is the weakest known set theory whose theorems include the Peano axioms. ...
that interprets the class of natural numbers and their arithmetic via just Extensionality, Adjunction and full Separation. Replacement can be seen as a form of comprehension. Only when assuming does Replacement already imply full Separation. In , Replacement is mostly important to prove the existence of sets of high
rank Rank is the relative position, value, worth, complexity, power, importance, authority, level, etc. of a person or object within a ranking, such as: Level or position in a hierarchical organization * Academic rank * Diplomatic rank * Hierarchy * H ...
, namely via instances of the axiom schema where \phi(x,y) relates relatively small set x to bigger ones, y. Constructive set theories commonly have Axiom schema of Replacement, sometimes restricted to bounded formulas. However, when other axioms are dropped, this schema is actually often strengthened - not beyond , but instead merely to gain back some provability strength. Such stronger axioms exist that do not spoil the strong existence properties of a theory, as discussed further below. The discussion now proceeds with axioms granting existence of objects also found in
dependent type theory In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers lik ...
, namely natural numbers and
products Product may refer to: Business * Product (business), an item that serves as a solution to a specific consumer problem. * Product (project management), a deliverable or set of deliverables that contribute to a business solution Mathematics * Produ ...
.


ECST

Denote by \mathrm(A) the inductive property, 0\in A\land\forall (n\in A). Sn \in A. Here n denotes a generic set variable. In terms of a predicate P underlying the class so that \forall n. (n\in A)\leftrightarrow P(n), this translates to P(0) \land \forall n. \big(P(n)\to P(Sn)\big). For some fixed predicate Q, the statement Q(a)\land\big(\forall x. Q(x)\to a\subset x\big) expresses that a is the smallest (in the sense of "\subset") set among all sets x for which Q(x) holds true. The elementary constructive Set Theory has the axiom of as well as the postulate of the existence of a smallest inductive set Write \bigcap B for \, the general intersection. Define a class \omega=\bigcap\, the intersection of all inductive sets. With the above axiom, \omega is a uniquely characterized set, the smallest infinite
von Neumann ordinal In set theory, an ordinal number, or ordinal, is a generalization of ordinal numerals (first, second, th, etc.) aimed to extend enumeration to infinite sets. A finite set can be enumerated by successively labeling each element with the least n ...
. Its elements include the empty set and, for each set in \omega, another set in \omega that contains one element more. Symbols called zero and successor are in the
signature A signature (; from la, signare, "to sign") is a handwritten (and often stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and intent. The writer of a ...
of the theory of
Peano Giuseppe Peano (; ; 27 August 1858 – 20 April 1932) was an Italian mathematician and glottologist. The author of over 200 books and papers, he was a founder of mathematical logic and set theory, to which he contributed much notation. The stand ...
. In , the above defined successor of any number also being in the class \omega follow directly from the characterization of the natural naturals by our von Neumann model. Since the successor of such a set contains itself, one also finds that no successor equals zero. So two of the
Peano axioms In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
regarding the symbols zero and the one regarding closedness of S come easily. Fourthly, in , where \omega is a set, S can be proven to be an injective operation. The pairwise order "<" on the naturals is captured by their membership relation "\in". It is important to note that the theory proves the order as well as the equality relation on this set to be decidable. The value of formulating the axiom using the inductive property is explained in the discussion on arithmetic. Weak forms of axioms of infinity can be formulated, all postulating that some set containing elements with the common natural number properties exist. Then full Separation may be used to obtain the "sparse" such set, the set of natural numbers. In the context of otherwise weaker axiom systems, an axiom of infinity should be strengthened so as to imply existence of such a sparse set on its own. One weaker form of Infinity is :\exists w. \forall m. \big( m \in w \leftrightarrow (m=0 \lor (\exists p \in w). E(p, m)) \big), where E(p, m) captures the predecessor membership relation in the von Neumann model :\forall n. (n\in m \leftrightarrow (n = p \lor n \in p)). This weaker axioms characterizes the infinite set by expressing that all elements m of it are either equal to 0 or themselves hold a predecessor set which shares all other members with m. This form can also be written more concisely using the successor notation S.


Number bounds

For a class of numbers I\subset\omega, the statement :\exists(m\in \omega).\forall(n\in\omega).(n\in I\to n or the weaker contrapositive variant :\exists(m\in \omega).\forall(n\in\omega).(m\le n\to n\notin I) are statements of finiteness. For decidable properties, these are \Sigma_2^0-statements in arithmetic, but with the axiom of Infinity, the two quantifiers are set-bound. Denote an initial segment of the natural numbers, i.e. \ for any m\in\omega and including the empty set, by \. This set equals m and so at this point "m-1" is mere notation for its predecessor (i.e. not involving subtraction function). To reflect more closely the discussion of functions below, write the above condition as :\exists(m\in \omega).\forall(n\in I).(n. Now for a general set, to be finitely enumerable shall mean that there is a surjection from a von Neumann natural number onto it, which is a function existence claim. Further, to be finite means there is a bijective function to a natural. To be subfinite means to be a subset of a finite set. The claim that being a finite set is equivalent to being subfinite is equivalent to . Terminology for finiteness conditions varies with authors and there are many more related definitions. For a class C, the statement :\forall(m\in\omega).\exists(n\in\omega).(m\le n\land n\in C) is one of infinitude. It is \Pi_2^0 in the decidable arithmetic case. To validate infinitude of a set, this property even works if the set holds other elements besides infinitely many of members of \omega. But more generally, call a set infinite if one can inject \omega into it, which is again a function existence claim. It is appropriate to discuss the function concept at this point.


Functions


General notes on functions

Naturally, the logical meaning of existence claims is a topic of interest in intuitionistic logic, be it for a theory of sets or any other mathematical framework. A constructive proof calculus may validate statements as above, :\forall (a\in A). \exists (c\in C). P(a, c) , in terms of programs on represented domains. Consider for example the notions of proof through type- or realizability theory. Roughly, the task then is to provide a mapping a\mapsto c_a and
witness In law, a witness is someone who has knowledge about a matter, whether they have sensed it or are testifying on another witnesses' behalf. In law a witness is someone who, either voluntarily or under compulsion, provides testimonial evidence, e ...
the
rewriting In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a well-formed formula, formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewr ...
\forall (a\in A). P(a, c_a) . It is a theorem that already
Robinson arithmetic In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by R. M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is ...
''represents'' exactly the recursive functions in terms of particular predicates P, which are then also proven total ''functional'', :\forall (a\in). \exists! (c\in). P(a, c). The weak classical arithmetic theory postulates, instead of using the full
mathematical induction Mathematical induction is a method for proving that a statement ''P''(''n'') is true for every natural number ''n'', that is, that the infinitely many cases ''P''(0), ''P''(1), ''P''(2), ''P''(3), ...  all hold. Informal metaphors help ...
schema for arithmetic formulas, that every number is either zero or that there exists a predecessor number to it. Finally, beware of a common ambiguity in related texts on
recursion theory Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since e ...
, where "function" needs to be understood in the computable sense, which is generally narrower than what is discussed further below. Similarly, below there is also no need to speak of "''total'' functions", as this is part of the definition of a set theoretical function.


Total functional relations

Now in the current set theoretical approach, define the property involving the
function application In mathematics, function application is the act of applying a function to an argument from its domain so as to obtain the corresponding value from its range. In this sense, function application can be thought of as the opposite of function abst ...
brackets, f(a)=c, as \langle a, c\rangle \in f and speak of a function f\subset A\times C when provenly :\forall (a\in A).\, \exists! (c\in C). f(a)=c , i.e. :\forall (a\in A).\, \exists (c\in C).\, \forall (d\in C). \big(d=c \leftrightarrow \langle a, d\rangle \in f\big) , which notably involves quantifier explicitly asking for existence. So one studies sets capturing particular
total relation In mathematics, a binary relation ''R'' ⊆ ''X''×''Y'' between two sets ''X'' and ''Y'' is total (or left total) if the source set ''X'' equals the domain . Conversely, ''R'' is called right total if ''Y'' equals the range . When ''f'': ''X'' â ...
s. Whether a subclass can be judged to be a function will depend on the strength of the theory, which is to say the axioms one adopts. Notably, a general class could fulfill the above predicate without being a subclass of the product A\times C, i.e. the property is expressing not more or less than functionality w.r.t. inputs from A. If the domain is a set, then the function has a pair for each of its elements and so exists as set. If domain and codomain are sets, then the above predicate only involves bounded quantifiers. Let C^A (also written ^AC) denote the class of set functions. When functions are understood as just function graphs as above, the membership proposition f\in C^A is also written f\colon A\to C. Below might write x\to y for y^x for the sake of distinguishing it from ordinal exponentiation. Common notions such as surjectivity and
injectivity In mathematics, an injective function (also known as injection, or one-to-one function) is a function that maps distinct elements of its domain to distinct elements; that is, implies . (Equivalently, implies in the equivalent contrapositi ...
can be expressed in a bounded fashion as well. Note that injectivity shall be defined positively, not by its contrapositive, which is common practice in classical mathematics. The axiom scheme of Replacement can also be formulated in terms of the ranges of such set functions. It is a metatheorem for theories containing that adding a function symbol for a provenly total class function is a conservative extension, despite this changing the scope of bounded Separation. Separation lets us cut out subsets of products A\times C, at least when they are described in a bounded fashion. Write 1 for S0. Given any B\subset A, one is now led to reason about classes such as :\. The boolean-valued characteristic functions \chi_B\colon A\to\ are among such classes. But be aware that a\in B may in generally not be decidable. That is to say, in absence of any non-constructive axioms, the disjunction a\in B\lor a\notin B may not be provable, since one requires an explicit proof of either disjunct. Constructively, when :\exists(y\in\). f(a) = y cannot be
witness In law, a witness is someone who has knowledge about a matter, whether they have sensed it or are testifying on another witnesses' behalf. In law a witness is someone who, either voluntarily or under compulsion, provides testimonial evidence, e ...
ed for all a\in A, or uniqueness of a term y associated with a not be proven, then one cannot judge the comprehended collection to be total functional. Variants of the functional predicate definition using apartness relations on
setoid In mathematics, a setoid (''X'', ~) is a set (or type) ''X'' equipped with an equivalence relation ~. A setoid may also be called E-set, Bishop set, or extensional set. Setoids are studied especially in proof theory and in type-theoretic fou ...
s have been defined as well. A function will be a set if its range is. Care must be taken with nomenclature "function", which sees use in most mathematical frameworks, also because some tie a function term itself to a particular codomain.


Computable sets

Given Infinity and any propositions Q, let I=\. Given any natural n\in\omega, then :\big(Q(n)\lor \neg Q(n)\big)\to\big(n\in I\lor n\notin I\big). In classical set theory, as Q is formally decidable just by , so is subclass membership. If the class I is not finite, then successively going through the natural numbers n, and thus "listing" all numbers in I by simply skipping those with n\notin I, classically constitutes an increasing surjective sequence a:\omega\twoheadrightarrow I. There, one can obtain a bijective ''function''. In this way, the classical class of functions is provenly rich, as it also contains objects that are beyond what we know to be ''effectively'' computable, or programmatically listable in praxis. In
computability theory Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since e ...
, the
computable set In computability theory, a set of natural numbers is called computable, recursive, or decidable if there is an algorithm which takes a number as input, terminates after a finite amount of time (possibly depending on the given number) and correctly ...
s are ranges of non-decreasing total functions ''in the recursive sense'', at the level \Sigma_1^0 \cap \Pi_1^0 = \Delta_1^0 of the
arithmetical hierarchy In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
, and not higher. Deciding a predicate at that level amounts to solving the task of eventually finding a
certificate Certificate may refer to: * Birth certificate * Marriage certificate * Death certificate * Gift certificate * Certificate of authenticity, a document or seal certifying the authenticity of something * Certificate of deposit, or CD, a financial pro ...
that either validates or rejects membership. As not every predicate Q is computably decidable, the theory alone will not claim (prove) that all infinite I\subset \omega are the range of some bijective function with domain \omega. See also Kripke's schema. But being compatible with , the development in this section still always permits "function on \omega" to be interpreted as an object not necessarily given as lawlike sequence. Applications may be found in the common models for claims about probability, e.g. statements involving the notion of "being given" an unending random sequence of coin flips.


Choice functions

Choice principles postulate the existence of functions. These can then be translated to claims of existence of inverses, ordering, and so on. Choice moreover implies statements about cardinalities of different sets, e.g. they imply or rule out countability of sets. The constructive development here proceeds in a fashion agnostic to any discussed choice principles, but here are well studied variants: *
Axiom of countable choice The axiom of countable choice or axiom of denumerable choice, denoted ACω, is an axiom of set theory that states that every countable collection of non-empty sets must have a choice function. That is, given a function ''A'' with domain N (where ...
: If g\colon\omega\to z, one can form the one-to-many relation-set \. The axiom of countable choice would grant that whenever \forall (n\in\omega). \exists u. u\in g(n), one can form a function mapping each number to a unique value. Countable choice can also be weakened further. One common consideration is to restrict the possible cardinalities of the range of g, giving the weak countable choice into countable, finite or even just binary sets. Another means of weakening countable choice is by restricting the involved definitions w.r.t. their place in the syntactic hierarchies. Countable choice is not valid in the
internal logic In classical logic, classical deductive logic, a consistent theory (mathematical logic), theory is one that does not lead to a logical contradiction. The lack of contradiction can be defined in either semantic or syntactic terms. The semantic de ...
of a general
topos In mathematics, a topos (, ; plural topoi or , or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally: on a site). Topoi behave much like the category of sets and possess a notion ...
, which can be seen as
models A model is an informative representation of an object, person or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin ''modulus'', a measure. Models c ...
of constructive set theories. *
Axiom of dependent choice In mathematics, the axiom of dependent choice, denoted by \mathsf , is a weak form of the axiom of choice ( \mathsf ) that is still sufficient to develop most of real analysis. It was introduced by Paul Bernays in a 1942 article that explores whi ...
: Countable choice is implied by the more general axiom of dependent choice, extracting a function from any entire relation on an inhabited set. Countable choice is akin to constructive Church's thesis principle and indeed dependent choice holds in many
realizability In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way t ...
models and it is thus adopted in many constructive schools. * Relativized dependent choice: The stronger relativized dependent choice principle is a variant of it - a schema involving an extra predicate variable. Adopting this for just bounded formulas in , the theory already proves the \Sigma_1-
induction Induction, Inducible or Inductive may refer to: Biology and medicine * Labor induction (birth/pregnancy) * Induction chemotherapy, in medicine * Induced stem cells, stem cells derived from somatic, reproductive, pluripotent or other cell t ...
. * \Pi\Sigma-AC: A family of sets is better controllable if it comes indexed by a function. A set B is a base if all indexed families of sets i_S\colon B\to S over it, have a choice function f_S, i.e. \forall (x\in B). f_S(x)\in i_S(x). A collection of sets holding \omega and its elements and which is closed by taking indexed sums and products (see
dependent type In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers lik ...
) is called \Pi\Sigma-closed. While the axiom that all sets in the smallest \Pi\Sigma-closed class are a base does need some work to formulate, it is the strongest principle over that holds in the type theoretical interpretation . *
Axiom of choice In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...
: The axiom of choice concerning functions on general sets of inhabited sets. The codomain here is the general union of sets. It implies Dependent choice. It also implies instances of via Diaconescu's theorem. In turn, extensional theories with full choice broadly tend to contradict the constructive Church's rule.


Diaconescu's theorem

To highlight the strength of full Choice and its relation to matters of
intentionality ''Intentionality'' is the power of minds to be about something: to represent or to stand for things, properties and states of affairs. Intentionality is primarily ascribed to mental states, like perceptions, beliefs or desires, which is why it ha ...
, one should consider the classes :a=\ :b=\ from the proof of
Diaconescu's theorem In mathematical logic, Diaconescu's theorem, or the Goodman–Myhill theorem, states that the full axiom of choice is sufficient to derive the law of the excluded middle, or restricted forms of it, in constructive set theory. It was discovered in 19 ...
. Referring back to the introductory elaboration on the meaning of such convenient class notation, as well as to the
principle of distributivity The principle of distributivity states that the algebraic distributive law is valid, where both logical conjunction and logical disjunction are distributive over each other so that for any propositions ''A'', ''B'' and ''C'' the equivalences :A \l ...
, t\in a\leftrightarrow \big(t=0\lor (t=1\land P)\big). So unconditionally, 0\in a, 1\in b. But otherwise, the uncountable classes a and b are as contingent as the proposition P involved in their definition. Nonetheless, the setup entails several consequences, when inspecting the provable case, starting with P\to(a=\\land b=\). So P\to a=b and indeed the equality is equivalent and decides P. As a are b are then sets, also P\to \=\. A
contrapositive In logic and mathematics, contraposition refers to the inference of going from a conditional statement into its logically equivalent contrapositive, and an associated proof method known as proof by contraposition. The contrapositive of a statemen ...
gives \neg(a=b)\leftrightarrow\neg P, which is important for the proof of the theorem. In fact, as \neg P\to(a=\\land b=\) and, as \neg(0=1), one finds in which way the sets are then different. One may moreover reason using the
disjunctive syllogism In classical logic, disjunctive syllogism (historically known as ''modus tollendo ponens'' (MTP), Latin for "mode that affirms by denying") is a valid argument form which is a syllogism having a disjunctive statement for one of its premise ...
that both 0\in b and 1\in a are each equivalent to P. In the following assume a context in which a, b are established to be sets, and thus subfinite sets. Then for inhabited such sets, the general axiom of choice claims existence of a function f\colon\\to a\cup b with f(z)\in z. It is important that the elements a,b of the function's domain are different than the natural numbers 0, 1 in that a priori less is known about the former. When forming then union of the two classes, u=0\lor u=1 is a necessary but then also sufficient condition. Thus a\cup b = \ and one is dealing with functions f into a set of two ''distinguishable'' values. With choice come the conjunction f(a)\in a \land f(b)\in b in the codomain of the function. Using the distributivity, there arises a list of conditions on the ''possible'' function return values, a disjunction. Expanding what is then established, one finds that either both P as well as the sets equality, or that the return values are different and P can be rejected. The conclusion is that the choice postulate actually implies P\lor\neg P whenever a Separation axiom allows for set comprehension using undecidable P. Consider, for example, an undecidable membership claim inside a given set. So full choice is generally non-constructive. The issue is that propositions, as part of set comprehension used to separate and define the classes a and b from \, ramify truth values into set terms. Equality defined by the set theoretical
axiom of extensionality In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of extensionality, or axiom of extension, is one of the axioms of Zermelo–Fraenkel set theory. It says that sets having the same elements ...
, which itself is not related to functions, in turn couples knowledge about the predicate to information about function values. Spoken in terms function values: On the one hand, witnessing f(a)=1 implies P and a=b and this conclusion independently also applies to witnessing f(b)=0. On the other hand, witnessing f(a)=0\land f(b)=1 implies the two function arguments are not equal and this rules out P. There are really only three combinations, as the axiom of extensionality in the given setup makes f(a)=1\land f(b)=0 inconsistent. The conclusion can be summarized by the already formally derived equivalence of disjuncts \big((1\in a)\lor(0\in b)\lor\neg(a=b)\big) \leftrightarrow (P\lor\neg P). So if the constructive reading of existence is to be preserved, full choice may be not adopted in the set theory, because the mere claim of function existence does not realize a particular function. To better understand why we cannot expect to be granted a definitive (total) function, consider naive function candidates. It was noted that it is the case that 0\in a and 1\in b, regardless of P. So without further analysis, this would seem to make :f = \ a contender for a choice function. Indeed, if P can be rejected, this is the only option. But in the case of provability of P, when \=\, there is extensionally only one possible function input to a choice function. So in that situation, a choice function would have type f\colon\\to\, for example :f = \ and this would rule out the initial contender. For general P, the domain of a would-be choice function is not concrete but contingent on P and uncountable. When considering the above functional assignment f(a)=0, then neither unconditionally declaring f(b)=1 nor f(b)=0 is necessarily consistent. Having identified 1 with \, the two candidates described above can be represented simultaneously via the uncountable f = \ with the would-be natural j = \. In j, the proposition P in the "if-clause" may be replaced by a=b. As (P\to j=0)\land(\neg P\to j=1), postulating the classical P\lor\neg P here would indeed imply that this is a choice function no matter which of two truth values P takes. And as in the constructive case, given a ''particular'' choice function - a set holding either exactly one or exactly two pairs - one could actually infer whether P or whether \neg P does hold. Vice versa, the third and last candidate :f = \ can be captured as part of f = \, where i=\. This is a classical choice function either way as well. Constructively, the domain and values of such P-dependent would-be functions will be undecidable and as such one fails to prove functional totality. In computable interpretations, set theory axioms postulating (total) function existence lead to the requirement for recursive functions. From a function realization one can infer the branches taken by the "if-clauses" of the classical solutions, which were undecided in the interpreted theory.


Regularity implies PEM

The
axiom of regularity In mathematics, the axiom of regularity (also known as the axiom of foundation) is an axiom of Zermelo–Fraenkel set theory that states that every non-empty set ''A'' contains an element that is disjoint from ''A''. In first-order logic, the axi ...
states that for every inhabited set s, there ''exists'' an element t in s, which shares no elements with s. As opposed to the axiom of choice, this existence claim reaches for an element of every inhabited set, i.e. the "domain" are all inhabited sets. Its formulation does not involve a unique existence claim but instead guarantees a set with a specific property. As the axiom correlates membership claims at different rank, the axiom also ends up implying : The proof from choice above had used a particular set \ from above. The proof below also uses this b, for which it was already established that 0\in b\leftrightarrow P. Also recall that when Separation applies to P, the set b is defined using the clause u\in\, so that any given u\in b has u=0\lor u=\. Now let t\in b be the postulated member with the empty intersection property, which in particular means t=\\to\neg(0\in b). Together, one finds (0\in b)\lor\neg(0\in b), which also formally decides P.


Arithmetic

The four
Peano axioms In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
for 0 and S, characterizing \omega as a model of the natural numbers in , have been discussed. The order "<" of natural numbers is captured by membership "\in" in this von Neumann model and this set is discrete, i.e. also equality is decidable. Indeed, also
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano a ...
proves :\vdash\forall n. \forall m. \big((n=m)\lor\neg(n=m)\big) The first-order theory has the same non-logical axioms as Peano arithmetic. An account of induction is given in the next paragraph. Then, it is clarified which set theory axiom must be asserted to prove existence of the binary functions addition "+" and multiplication "\times" with their respective relation to zero and successor.


Moderate induction in ECST

The second universally quantified conjunct in the axiom of Infinity expresses mathematical induction for all x in the universe of discourse, i.e. for sets. This is because sets x can be read as corresponding to predicates and the consequent \omega\subset x states that all n\in\omega fulfill said predicate. So proves induction for all predicates \phi(n) involving only set-bounded quantifiers. The much stronger axiom of full mathematical induction for any predicate expressed though set theory language could also be adopted at this point in our development. That induction principle follows from full (i.e. unbounded) Separation as well as from (full) Set induction. Note: In naming induction statements, one must take care not to conflate terminology with arithmetic theories. The first-order induction schema of natural number arithmetic claims induction for all predicates definable in the language of first-order arithmetic, namely predicates of just numbers. So to interpret the axiom schema of , one interprets these arithmetical formulas. One may also speak about the induction in second-order arithmetic, explicitly expressed for subsets of the naturals. The class of subsets can be taken to correspond to a richer collection of formulas than the first-order arithmetic definable ones. Typical set theories like the one discussed here are also first-order, but those theories are not arithmetics and so formulas may also quantify over the subsets of the naturals. Finally, bounded quantification in that context here means quantification over the elements of whatever is established to be a set.


Recursion

In , many mathematical statements can be proven per individual set, opposed to many formulas involving universal quantification, as would be possible, for example, with an induction principle for classes. With this, the set theory axioms listed so far suffice as formalized framework for a good portion of basic mathematics. That said, the constructive set theory does actually not even enable primitive recursion for function definitions of what would be h\colon(x\times\omega)\to y. Indeed, despite having the Replacement axiom, the theory does not prove the addition function +\colon(\omega\times\omega)\to \omega to be a set function. Going beyond with regards to arithmetic, the axiom granting definition of set functions via iteration-step set functions must be added: For any set y, set z\in y and f\colon y\to y, there must also exist a function g\colon \omega\to y attained by making use of the former, namely such that g(0)=z and g(Sn)=f(g(n)). This postulate is akin to the transfinite recursive theorem, except it is restricted to set functions and finite ordinals, i.e. there is no clause about limit ordinals. It functions as the set theoretical equivalent of a natural numbers object in
category theory Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, cate ...
. This then enables a full interpretation of
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano a ...
in our set theory, including addition and multiplication functions. With this, arithmetic of rational numbers can then also be defined and its properties, like uniqueness and countability, be proven. A set theory with this will also prove that, for any naturals n and m, the function spaces :\to are sets. (As an aside, note that, moreover, a bounded variant of this iteration schema that grants the existence of a unique such g, proves the existence of a
transitive closure In mathematics, the transitive closure of a binary relation on a set is the smallest relation on that contains and is transitive. For finite sets, "smallest" can be taken in its usual sense, of having the fewest related pairs; for infinite s ...
for every set with respect to \in.) Now conversely, a proof of the spelled out, -model enabling iteration principle can be based on the collection of functions one would want to write as the union \cup_y^. The existence of this becomes provable when asserting that the individual function spaces on finite domains into sets y form sets themselves. That principle may be written as :\forall(n\in\omega). \forall y.\ \ \exists h. h=y^n This should further motivate the adoption of an even stronger axiom of more set theoretical flavor, instead of just directly embedding arithmetic principles into our theory. This more set theoretical exponentiation axiom will, however, still not prove the full induction schema for formulas with quantifiers over sets.


Induction without Infinity

Before discussing (even classically) uncountable sets, here taking a step back to , note that induction schemas may be adopted without ever postulating that the collection of naturals exists as a set. It is worth noting that in the program of
predicative arithmetic Predicative may refer to: * Something having the properties of a grammatical predicate ** Predicative expression, part of a clause that typically follows a copula (linking verb) ** Predicative verb, a verb that behaves as a grammatical adjective ...
, the mathematical induction schema has been criticized as possibly being
impredicative In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
, when natural numbers are defined as the object which fulfill this schema, which itself is defined in terms of all naturals. The minimal assumptions necessary to obtain theories of natural number arithmetic are thoroughly studied in
proof theory Proof theory is a major branchAccording to Wang (1981), pp. 3–4, proof theory is one of four domains mathematical logic, together with model theory, axiomatic set theory, and recursion theory. Jon Barwise, Barwise (1978) consists of four correspo ...
and are naturally framed as insights into first- and second-order arithmetic theories. The classical theories starting with
bounded arithmetic Bounded arithmetic is a collective name for a family of weak subtheories of Peano arithmetic. Such theories are typically obtained by requiring that quantifiers be bounded in the induction axiom or equivalent postulates (a bounded quantifier is of ...
adopt different conservative induction schemas and may add symbols for particular functions. On the first-order side, this leads to theories between the
Robinson arithmetic In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by R. M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is ...
and
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
: The theory does not have any induction. has full mathematical induction for arithmetical formulas and has ordinal \varepsilon_0, meaning the theory lets one encode ordinals of weaker theories as recursive relation on just the naturals. Many of the well studied arithmetic theories are weak regarding proof of totality for some more fast growing functions. Some of the most basic examples of arithmetics include
elementary function arithmetic In proof theory, a branch of mathematical logic, elementary function arithmetic (EFA), also called elementary arithmetic and exponential function arithmetic,C. Smoryński, "Nonstandard Models and Related Developments" (p. 217). From ''Harvey Frie ...
, which includes induction for just bounded arithmetical formulas, here meaning with quantifiers over finite number ranges. The theory has a proof theoretic ordinal (the least not provenly recursive
well-ordering In mathematics, a well-order (or well-ordering or well-order relation) on a set ''S'' is a total order on ''S'' with the property that every non-empty subset of ''S'' has a least element in this ordering. The set ''S'' together with the well-o ...
) of \omega^3. The \Sigma_1^0-induction schema for arithmetical existential formulas allows for induction for those properties of naturals a validation of which is computable via a finite search with unbound (any, but finite) runtime. The schema is also classically equivalent to the \Pi_1^0-induction schema. The relatively weak classical first-order arithmetic which adopts that schema is denoted \mathsf_1 and proves the
primitive recursive function In computability theory, a primitive recursive function is roughly speaking a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop can be determined ...
s total. The theory \mathsf_1 is \Pi_2^0-conservative over
primitive recursive arithmetic Primitive recursive arithmetic (PRA) is a quantifier-free formalization of the natural numbers. It was first proposed by Norwegian mathematician , reprinted in translation in as a formalization of his finitist conception of the foundations of ar ...
. Note that the \Sigma_1^0-induction is also part of the
second-order Second-order may refer to: Mathematics * Second order approximation, an approximation that includes quadratic terms * Second-order arithmetic, an axiomatization allowing quantification of sets of numbers * Second-order differential equation, a di ...
reverse mathematics base system \mathsf_0, its other axioms being plus \Delta_1^0-comprehension of subsets of naturals. The theory \mathsf_0 is \Pi_1^1-conservative over \mathsf_1. Those last mentioned arithmetic theories all have ordinal \omega^\omega. Let us mention one more step beyond the \Sigma_1^0-induction schema. Lack of stronger induction schemas means, for example, that some infinite versions of the
pigeon hole principle In mathematics, the pigeonhole principle states that if items are put into containers, with , then at least one container must contain more than one item. For example, if one has three gloves (and none is ambidextrous/reversible), then there m ...
are unprovable. One relatively weak one being the Ramsey theorem type claim here expressed as follows: For any m>0 and coding of a coloring map f, associating each n\in\omega with a color \, it is not the case that for every color c there exists a threshold input number n_c beyond which c is not ever the mappings return value anymore. Higher indirection as in induction for mere existential statements is needed to rewrite such a negation and prove it. Namely to rewrite it as the negation of the existence of a joint threshold number, depending on all the ''hypothetical'' n_c's, beyond which the function would still have to attain some color value. More specifically, the strength of the required bounding principle is strictly between the induction schema in \mathsf_1^0 and \mathsf_2^0. For properties in terms of return values of functions on finite domains, brute force verification through checking all possible inputs has computational overhead which is larger the larger the size of the domain, but always finite. Acceptance of an induction schema as in \mathsf_2^0 validates the former so called infinite pigeon hole principle, which concerns unbounded domains, and so is about mappings with infinitely many inputs. In the classical context, this claim about coloring may be phrased positively, in terms of sets, as saying that there always exists at least one return value k such that, in effect, for some infinite domain K\subset\omega it holds that \forall(n\in K). f(n) = k. In words, when f provides infinite enumerated assignments, each being of one of m different possible colors, then a particular k coloring infinitely many numbers is claimed to exist and that the set can be specified. When read constructively, one would want k to be concretely specifiable. Higher-order classical arithmetics with low
complexity Complexity characterises the behaviour of a system or model whose components interaction, interact in multiple ways and follow local rules, leading to nonlinearity, randomness, collective dynamics, hierarchy, and emergence. The term is generall ...
comprehension are a relevant reference point for weaker set theories insofar as their language does not merely express
arithmetical set In mathematical logic, an arithmetical set (or arithmetic set) is a set of natural numbers that can be defined by a formula of first-order Peano arithmetic. The arithmetical sets are classified by the arithmetical hierarchy. The definition can be ...
s, while all sets of naturals particular such theories prove to exist are just
computable set In computability theory, a set of natural numbers is called computable, recursive, or decidable if there is an algorithm which takes a number as input, terminates after a finite amount of time (possibly depending on the given number) and correctly ...
s. Constructive
reverse mathematics Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
, which lacks
double negation elimination In propositional logic, double negation is the theorem that states that "If a statement is true, then it is not the case that the statement is not true." This is expressed by saying that a proposition ''A'' is logically equivalent to ''not (not ...
for undecidable sentences, exists as a field but is less developed than its classical counterpart.


Exponentiation

Classical without the Powerset axiom is still consistent with all existing sets of reals being
subcountable In constructive mathematics, a collection X is subcountable if there exists a partial surjection from the natural numbers onto it. This may be expressed as \exists (I\subseteq).\, \exists f.\, (f\colon I\twoheadrightarrow X), where f\colon I\twohea ...
, and there even countable. Possible choice principles were discussed, a weakened form of the Separation schema was already adopted, and more of the standard axioms shall be weakened for a more predicative and constructive theory. The first one of those is the Powerset axiom, which is adopted in the form of the space of characteristic functions, itself tied to exactly the decidable subclasses. So consider the axiom . The formulation here uses the convenient notation for function spaces. Otherwise the axiom is lengthier, characterizing h using bounded quantifiers in the total function predicate. In words, the axiom says that given two sets x, y, the class y^x of all functions is, in fact, also a set. This is certainly required, for example, to formalize the object map of an internal
hom-functor In mathematics, specifically in category theory, hom-sets (i.e. sets of morphisms between objects) give rise to important functors to the category of sets. These functors are called hom-functors and have numerous applications in category theory and ...
like (,-). Existence statements like Exponentiation, i.e. function spaces being sets, enable the derivation of more sets via bounded Separation. Adopting the axiom, quantification \forall f over the elements of certain classes of functions only ranges over a set, also when such function spaces are even classically
uncountable In mathematics, an uncountable set (or uncountably infinite set) is an infinite set that contains too many elements to be countable. The uncountability of a set is closely related to its cardinal number: a set is uncountable if its cardinal numb ...
. E.g. the collection of all functions f\colon\omega\to 2 where 2=\, i.e. the set 2^ of points underlying the
Cantor space In mathematics, a Cantor space, named for Georg Cantor, is a topological abstraction of the classical Cantor set: a topological space is a Cantor space if it is homeomorphic to the Cantor set. In set theory, the topological space 2ω is called "the ...
, is uncountable, by
Cantor's diagonal argument In set theory, Cantor's diagonal argument, also called the diagonalisation argument, the diagonal slash argument, the anti-diagonal argument, the diagonal method, and Cantor's diagonalization proof, was published in 1891 by Georg Cantor as a m ...
, and can at best be taken to be a
subcountable In constructive mathematics, a collection X is subcountable if there exists a partial surjection from the natural numbers onto it. This may be expressed as \exists (I\subseteq).\, \exists f.\, (f\colon I\twoheadrightarrow X), where f\colon I\twohea ...
set. (In this section and beyond, the symbol for the semiring of natural numbers in expressions like y^ is used, or written \omega\to y, just to avoid conflation of cardinal- with ordinal exponentiation.) Roughly, classically uncountable sets tend to not have computably decidable equality.


On countable sets

Enumerable forms of the
pigeon hole principle In mathematics, the pigeonhole principle states that if items are put into containers, with , then at least one container must contain more than one item. For example, if one has three gloves (and none is ambidextrous/reversible), then there m ...
can now be proven, e.g. that on a finitely enumerable set, every injection is also a surjection. At last, all finitely enumerable sets are finite. The finitely enumerable union of a family of subfinite resp. subcountable sets is itself subfinite resp. subcountable. For any countable family of counting functions together with their ranges, the theory proves the union of those ranges to be countable. Recall that not even classical (without countable choice) proves a countable union of countable sets to be countable, as this requires infinitely many
existential instantiation In predicate logic, existential instantiation (also called existential elimination)Moore and Parker is a rule of inference which says that, given a formula of the form (\exists x) \phi(x), one may infer \phi(c) for a new constant symbol ''c''. Th ...
s of functions. With Exponentiation, the union of all finite sequences over a countable set is now a countable set. With function spaces with the finite von Neumann ordinals as domains, we can model as discussed and can thus encode ordinals in the arithmetic. One then furthermore obtains the ordinal-exponentiated number \omega^\omega as a set, which may be characterized as \cup_\omega^n. Relatedly, the set theory then also proves the existence of any
primitive recursive function In computability theory, a primitive recursive function is roughly speaking a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop can be determined ...
on the naturals \omega, as set functions in the uncountable set \omega\to\omega. As far as comprehension goes, the dependent or indexed products \Pi_\,y_i are now sets. The theory now proves the collection of all the countable subsets of any set (the collection is a subclass of the powerclass) to be a set.


The class of subsets of a set

The characterization of the class _x of all subsets of a set x involves unbounded universal quantification, namely \forall u. \left(u\subset x\leftrightarrow u\in _x\right). Here \subset has been defined in terms of the membership predicate \in above. So in a mathematical set theory framework, the power class is defined not in a bottom-up construction from its constituents (like an algorithm on a list, that e.g. maps \langle a,b\rangle \mapsto \langle \langle \rangle ,\langle a\rangle ,\langle b\rangle ,\langle a,b\rangle \rangle ) but via a comprehension over all sets. If _x is a set, that defining quantification even ranges over _x, which makes the axiom of powerset
impredicative In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
. The statement y=_x itself is \Pi_1. The richness of the powerclass in a theory without excluded middle can best be understood by considering small classically finite sets. For any proposition P, the class \\subset\ equals 0 when P can be rejected and 1 (i.e. \) when P can be proven, but P may also not be decidable at all. Consider three different undecidable proposition, none of which provenly imply another. They can ben used to define three subclasses of the singleton \, none of which are provenly the same. In this view, the powerclass _1 of the singleton, usually denoted by \Omega, is called the
truth value In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values (''true'' or '' false''). Computing In some progr ...
algebra Algebra () is one of the broad areas of mathematics. Roughly speaking, algebra is the study of mathematical symbols and the rules for manipulating these symbols in formulas; it is a unifying thread of almost all of mathematics. Elementary a ...
and does not necessarily provenly have only two elements. The set 2^x of \-valued functions on a set x injects into the function space ^x and corresponds to just its decidable subsets. It has been pointed out that the empty set 0 and the set 1 itself are of course two subsets of 1. Whether also _1\subset \ is true in a theory is contingent on a simple disjunction: :\big(\forall x. x\subset 1 \to(0\in x\lor 0\notin x)\big)\to _1\subset \. So assuming for just bounded formulas, predicative Separation then lets one demonstrate that the powerclass _1 is a set. With exponentiation, _1 being a set already implies Powerset for sets in general. The proof is via replacement for the association of f\in^x to \\in_x, and an argument why all subsets are covered. So in this context, also full Choice proves Powerset. Moreover, with bounded excluded middle, _x is in bijection with 2^x. See also . Full Separation is equivalent to just assuming that each individual subclass of 1 is a set. Assuming full Separation, both full Choice and Regularity prove . Relatedly, assuming in this theory, Set induction becomes equivalent to Regularity and Replacement becomes capable of proving full Separation.


Metalogic

While the theory + does not exceed the consistency strength of
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano a ...
, adding Excluded Middle gives a theory proving the same theorems as classical minus Regularity! Thus, adding Regularity as well as either or full Separation to + gives full classical . Adding full Choice and full Separation gives minus Regularity. So this would thus lead to a theory beyond the strength of typical
type theory In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundat ...
.


Category and type theoretic notions

So in this context with Exponentiation, function spaces are more accessible than classes of subsets, as is the case with
exponential object In mathematics, specifically in category theory, an exponential object or map object is the categorical generalization of a function space in set theory. Categories with all finite products and exponential objects are called cartesian closed ca ...
s resp.
subobject In category theory, a branch of mathematics, a subobject is, roughly speaking, an object that sits inside another object in the same category. The notion is a generalization of concepts such as subsets from set theory, subgroups from group theory,M ...
s in category theory. In category theoretical terms, the theory + essentially corresponds to constructively well-pointed
Cartesian closed In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in math ...
Heyting __NOTOC__ Arend Heyting (; 9 May 1898 – 9 July 1980) was a Dutch mathematician and logician. Biography Heyting was a student of Luitzen Egbertus Jan Brouwer at the University of Amsterdam, and did much to put intuitionistic logic on a foot ...
pre
topos In mathematics, a topos (, ; plural topoi or , or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally: on a site). Topoi behave much like the category of sets and possess a notion ...
es with (whenever Infinity is adopted) a natural numbers object. Existence of powerset is what would turn a Heyting pretopos into an
elementary topos In mathematics, a topos (, ; plural topoi or , or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally: on a site). Topoi behave much like the category of sets and possess a notion ...
. Every such topos that interprets is of course a model of these weaker theories, but locally Cartesian closed pretoposes have been defined that e.g. interpret theories with Exponentiation but reject full Separation and Powerset. A form of corresponds to any subobject having a complement, in which case we call the topos Boolean. Diaconescu's theorem in its original topos form says that this hold iff any
coequalizer In category theory, a coequalizer (or coequaliser) is a generalization of a quotient by an equivalence relation to objects in an arbitrary category. It is the categorical construction dual to the equalizer. Definition A coequalizer is a co ...
of two nonintersecting
monomorphism In the context of abstract algebra or universal algebra, a monomorphism is an injective homomorphism. A monomorphism from to is often denoted with the notation X\hookrightarrow Y. In the more general setting of category theory, a monomorphism ...
s has a section. The latter is a formulation of choice. Barr's theorem states that any topos admits a surjection from a Boolean topos onto it, relating to classical statements being provable intuitionistically. In type theory, the expression "x\to y" exists on its own and denotes
function spaces In mathematics, a function space is a set of functions between two fixed sets. Often, the domain and/or codomain will have additional structure which is inherited by the function space. For example, the set of functions from any set into a vector ...
, a primitive notion. These types (or, in set theory, classes or sets) naturally appear, for example, as the type of the
currying In mathematics and computer science, currying is the technique of translating the evaluation of a function that takes multiple arguments into evaluating a sequence of functions, each with a single argument. For example, currying a function f that ...
bijection between (z\times x)\to y and z\to y^x, an adjunction. A typical type theory with general programming capability - and certainly those that can model , which is considered a constructive set theory - will have a type of integers and function spaces representing \to, and as such also include types that are not countable. This is just to say, or implies, that among the function terms f\colon \to(\to), none have the property of being a bijection. Constructive set theories are also studied in the context of applicative axioms.


Analysis

In this section the strength of + is elaborated on. For context, possible further principles are mentioned, which are not necessarily classical and also not generally considered constructive. Here a general warning is in order: When reading proposition equivalence claims in the computable context, one shall always be aware which ''choice'', ''induction'' and ''comprehension'' principles are silently assumed. See also the related
Constructive analysis In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics. This contrasts with ''classical analysis'', which (in this context) simply means analysis done according to the (more comm ...
and
Computable analysis In mathematics and computer science, computable analysis is the study of mathematical analysis from the perspective of computability theory. It is concerned with the parts of real analysis and functional analysis that can be carried out in a compu ...
.


Cauchy sequences

Exponentiation implies recursion principles and so in +, one can comfortably reason about sequences s\colon\omega\to, their regularity properties such as , s_n-s_m, \le \tfrac+\tfrac, or about shrinking intervals in \omega\to(\times). So this enables speaking of
Cauchy sequences In mathematics, a Cauchy sequence (; ), named after Augustin-Louis Cauchy, is a sequence whose elements become arbitrarily close to each other as the sequence progresses. More precisely, given any small positive distance, all but a finite num ...
and their arithmetic.


Cauchy reals

Any Cauchy real number is a collection of sequences, i.e. subset of a set of functions on \omega. More axioms are required to always grant completeness of equivalence classes of such sequences and strong principles need to be postulated to imply the existence of a
modulus of convergence In real analysis, a branch of mathematics, a modulus of convergence is a function that tells how quickly a convergent sequence converges. These moduli are often employed in the study of computable analysis and constructive mathematics. If a sequ ...
for all Cauchy sequences. Weak countable choice is generally the context for proving
uniqueness Uniqueness is a state or condition wherein someone or something is unlike anything else in comparison, or is remarkable, or unusual. When used in relation to humans, it is often in relation to a person's personality, or some specific characterist ...
of the Cauchy reals as complete (pseudo-)ordered field. The prefix "pseudo" here highlights that the order will, in any case, constructively not always be decidable.


Towards the Dedekind reals

As in the classical theory,
Dedekind cuts In mathematics, Dedekind cuts, named after German mathematician Richard Dedekind but previously considered by Joseph Bertrand, are а method of construction of the real numbers from the rational numbers. A Dedekind cut is a partition of the rati ...
are characterized using subsets of algebraic structures such as : The properties of being inhabited, numerically bounded above, "closed downwards" and "open upwards" are all bounded formulas with respect to the given set underlying the algebraic structure. A standard example of a cut, the first component indeed exhibiting these properties, is the representation of \sqrt 2 given by :\big\langle\,\,\\big\rangle\,\ \in\,\ \times (Depending on the convention for cuts, either of the two parts or neither, like here, may makes use of the sign \le.) The theory given by the axioms so far validates that a pseudo-
ordered field In mathematics, an ordered field is a field together with a total ordering of its elements that is compatible with the field operations. The basic example of an ordered field is the field of real numbers, and every Dedekind-complete ordered field ...
that is also Archimedean and Dedekind complete, if it exists at all, is in this way characterized uniquely, up to isomorphism. However, the existence of just function spaces such as \^ does not grant to be a set, and so neither is the class of all subsets of that do fulfill the named properties. What is required for the class of Dedekind reals to be a set is an axiom regarding existence of a set of subsets and this is discussed further below in the section on Binary refinement. In a context without or Powerset, countable choice into finite sets is commonly assumed to prove the uncountability of the Dedekind reals. Whether Cauchy or Dedekind reals, fewer statements about the arithmetic of the reals are decidable, compared to the classical theory.


Constructive schools

Non-constructive claims valuable in the study of
constructive analysis In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics. This contrasts with ''classical analysis'', which (in this context) simply means analysis done according to the (more comm ...
are commonly formulated as concerning all binary sequences, i.e. functions f\colon\omega\to\. That is to say claims which are now set bound via "\forall (f \in 2^)". A most prominent example is the
limited principle of omniscience In constructive mathematics, the limited principle of omniscience (LPO) and the lesser limited principle of omniscience (LLPO) are axioms that are nonconstructive but are weaker than the full law of the excluded middle . The LPO and LLPO axioms are ...
, postulating a disjunctive property, like at the level of \Pi_1^0-sentences or functions. (
Example Example may refer to: * '' exempli gratia'' (e.g.), usually read out in English as "for example" * .example, reserved as a domain name that may not be installed as a top-level domain of the Internet ** example.com, example.net, example.org, ex ...
functions can be constructed in raw such that, if is consistent, the competing disjuncts are -unprovable.) The principle is independent of e.g. introduced below. In that constructive set theory, implies its "weaker" version, itself implying the "lesser" version, denoted and . moreover implies
Markov's principle Markov's principle, named after Andrey Markov Jr, is a conditional existence statement for which there are many equivalent formulations, as discussed below. The principle is logically valid classically, but not in intuitionistic constructive m ...
, a form of proof by contradiction motivated by (unbound memory capacity) computable search, as well as the \Pi_1^0-version of the fan theorem. Mention of such principles holding for \Pi_1^0-sentences generally hint at equivalent formulations in terms of sequences, deciding apartness of reals. In a constructive analysis context with countable choice, is e.g. equivalent to the claim that every real is either rational or irrational - again without the requirement to witness either disjunct. The three omniscience principles are each equivalent to theorems of the apartness, equality or order of two reals in this way. Here a list of some propositions employed in theories of constructive analysis that are not provable using just base intuitionistic logic. For example, see or even the anti-classical constructive Church's thesis principle for number-theoretic functions as a postulate in the theory, or some of its consequences on the recursive mathematics side (variously called , or ). This is discussed below. On another end, there are Kripke's schema (turning all subclasses of \omega countable),
bar induction Bar induction is a reasoning principle used in intuitionistic mathematics, introduced by L. E. J. Brouwer. Bar induction's main use is the intuitionistic derivation of the fan theorem, a key result used in the derivation of the uniform continuity ...
, the decidable fan theorem _\Delta (which contradicts strong forms of Church's thesis), or even Brouwer's anti-classical continuity principle determining functions on unending sequences through finite initial segments, on the Brouwerian
intuitionist In the philosophy of mathematics, intuitionism, or neointuitionism (opposed to preintuitionism), is an approach where mathematics is considered to be purely the result of the constructive mental activity of humans rather than the discovery of fu ...
side (). Both mentioned schools contradict , so that choosing to adopt certain of its laws makes the theory inconsistent with theorems in classical analysis. Those two schools are moreover not consistent with one another.


Infinite trees

Through the relation between computability and the arithmetical hierarchy, insights in this classical study are also revealing for constructive considerations. A basic insight of
reverse mathematics Reverse mathematics is a program in mathematical logic that seeks to determine which axioms are required to prove theorems of mathematics. Its defining method can briefly be described as "going backwards from the theorems to the axioms", in cont ...
concerns computable infinite finitely branching binary trees. Such a tree may e.g. be encoded as an infinite set of finite sets :T\,\subset\,\cup_\^, with decidable membership, and those trees then provenly contain elements of arbitrary big finite size. The so called Weak KÅ‘nigs lemma states: For such T, there always exists an infinite path in \omega\to\, i.e. an infinite sequence such that all its initial segments are part of the tree. In reverse mathematics, the second-order arithmetic \mathsf_0 does not prove . To understand this, note that there are computable trees K for which no ''computable'' such path through it exists. To prove this, one enumerates the partial computable sequences and then diagonalizes all total computable sequences in one partial computable sequences d. One can then roll out a certain tree K, one exactly compatible with the still possible values of d everywhere, which by construction is incompatible with any total computable path. In , the principle implies the non-constructive lesser limited principle of omniscience . In a more conservative context, they are equivalent assuming \Pi_1^0-_ (a very weak countable choice). It is also equivalent to the
Brouwer fixed point theorem Brouwer's fixed-point theorem is a fixed-point theorem in topology, named after L. E. J. (Bertus) Brouwer. It states that for any continuous function f mapping a compact convex set to itself there is a point x_0 such that f(x_0)=x_0. The simplest ...
and other theorems regarding values of continuous functions on the reals. The fixed point theorem in turn implies the
intermediate value theorem In mathematical analysis, the intermediate value theorem states that if f is a continuous function whose domain contains the interval , then it takes on any given value between f(a) and f(b) at some point within the interval. This has two import ...
, but be aware that the classical theorems can translate to different variants when expressed in a constructive context. The concerns ''infinite'' graphs and so its contrapositive gives a condition for finiteness. Again to connect to analysis, over the classical arithmetic theory \mathsf_0, the claim of is for example equivalent to the Borel compactness regarding finite subcovers of the real unit interval. A closely related existence claim involving finite sequences in an infinite context is the decidable fan theorem _\Delta. Over \mathsf_0, they are actually equivalent. In those are distinct, but, after again assuming some choice, here then implies _\Delta.


Restricting function spaces

In the following short remark ''function'' and claims made about them is again meant in the sense of computability theory: The
μ operator In computability theory, the μ-operator, minimization operator, or unbounded search operator searches for the least natural number with a given property. Adding the μ-operator to the five primitive recursive operators makes it possible to define ...
enables all partial
general recursive function In mathematical logic and computer science, a general recursive function, partial recursive function, or μ-recursive function is a partial function from natural numbers to natural numbers that is "computable" in an intuitive sense – as well as i ...
s (or programs, in the sense that they are Turing computable), including ones e.g. non-primitive recursive but -total, such as the
Ackermann function In computability theory, the Ackermann function, named after Wilhelm Ackermann, is one of the simplest and earliest-discovered examples of a total computable function that is not primitive recursive. All primitive recursive functions are total ...
. The definition of the operator involves predicates over the naturals and so the theoretical analysis of functions and their totality depends on the formal framework and proof calculus at hand. This is highlighted because of the concern with axioms in theories other than arithmetic. The predicate expressing a program to be total is famously computably undecidable. An anti-classical constructive Church's principle , expressed in the language of the theory, concerns those set functions and it postulates that they corresponds to computable programs. The natural numbers which are thought of as indices (for the computable functions which are total) in computability theory are \Pi_2^0 in the
arithmetical hierarchy In mathematical logic, the arithmetical hierarchy, arithmetic hierarchy or Kleene–Mostowski hierarchy (after mathematicians Stephen Cole Kleene and Andrzej Mostowski) classifies certain sets based on the complexity of formulas that define th ...
. Which is to say it is still a subclass of the naturals and so this is, when put in relation to some classical function spaces, a conceptually small class. In this sense, adopting the postulate makes \omega\to\omega into a "sparse" set, as viewed from classical set theory. Subcountability of sets can also be postulated independently. is still consistent with some choice, but it contradicts classically valid principles such as and _\Delta, which are amongst the weakest often discussed principles.


Induction


Mathematical induction

In set language, induction principles can read \mathrm(A)\to \omega\subset A, with the antecedent \mathrm(A) defined as further above, and with \omega\subset A meaning \forall (n\in\omega). n\in A where \omega is always the set of naturals. Via the strong axiom of Infinity and bounded Separation, the validity of induction for bounded definitions was already established. At this point it is instructive to recall how set comprehension was encoding statements in predicate logic. For an example, given set y, let P(n) denote the existential statement that a certain function space set exist, \exists x. x=y^. Here the existential quantifier is not merely one over natural numbers or bounded by any other set. Now a proposition like the exponentiation claim \forall(n\in\omega). P(n) and the subclass claim \omega\subset\, are just two ways of formulating the same desired claim, namely an n-indexed conjunction of existential propositions where n spans over the set of all naturals. The second form is expressed using class notation involving a subclass comprehension that may not constitute a set, in which case many set axioms won't apply, so that establishing it as a theorem may not be possible. A set theory with just ''bounded'' Separation can thus also be strengthened by adopting arithmetical induction schemas for predicates beyond just the bounded ones. The iteration principle for set functions mentioned in the section dedicated to arithmetic is also implied by the full induction schema over one's structure modeling the naturals (e.g. \omega). So for that theorem, granting a model of Heyting arithmetic, it represents an alternative to Exponentiation. The schema is often formulated in terms of predicates as follows: Here the 0 denotes \ as above, and the set Sn denotes the successor set of n\in\omega, with n\in Sn. By Axiom of Infinity above, it is again a member of \omega. The full induction schema is implied by the full Separation schema. As elaborated in the section on induction from infinity, here formulas in schemas are to be understood as formulas in first-order set theory. And as stated in the section on Choice, induction principles are also implied by various forms of choice principles.


Set Induction

Full Set Induction in proves induction in
transitive set In set theory, a branch of mathematics, a set A is called transitive if either of the following equivalent conditions hold: * whenever x \in A, and y \in x, then y \in A. * whenever x \in A, and x is not an urelement, then x is a subset of A. Simil ...
s and so transitive sets or transitive sets (ordinals). This enables ordinal arithmetic. In particular, it proves full mathematical induction. Replacement is not required to prove induction over the set of naturals, but it is for their arithmetic modeled within the set theory. It then reads as follows: Here \forall(z\in \). \phi(z) holds trivially and so this covers to the "bottom case" \phi(\) in the standard framework. The variant of the axiom just for bounded formulas is also studied independently and may be derived from other axioms. The axiom allows definitions of class functions by
transfinite recursion Transfinite induction is an extension of mathematical induction to well-ordered sets, for example to sets of ordinal numbers or cardinal numbers. Its correctness is a theorem of ZFC. Induction by cases Let P(\alpha) be a property defined for a ...
. The study of the various principles that grant set definitions by induction, i.e. inductive definitions, is a main topic in the context of constructive set theory and their comparatively weak strengths. This also holds for their
counterparts Counterpart or Counterparts may refer to: Entertainment and literature * "Counterparts" (short story), by James Joyce * Counterparts, former name for the Reel Pride LGBT film festival * ''Counterparts'' (film), a 2007 German drama * ''Counterp ...
in type theory. The
axiom of regularity In mathematics, the axiom of regularity (also known as the axiom of foundation) is an axiom of Zermelo–Fraenkel set theory that states that every non-empty set ''A'' contains an element that is disjoint from ''A''. In first-order logic, the axi ...
is a single statement with universal quantifier over sets and not a schema. As show, it implies , and so is non-constructive. Now for \phi taken to be the negation of some predicate \neg S and writing \Sigma for the class \, induction reads :\forall(x\in\Sigma).x\cap \Sigma\neq\\,\to\,\Sigma=\ Via the contrapositive, set induction implies all instances of regularity but only with double-negated existence in the conclusion. In the other direction, given enough
transitive set In set theory, a branch of mathematics, a set A is called transitive if either of the following equivalent conditions hold: * whenever x \in A, and y \in x, then y \in A. * whenever x \in A, and x is not an urelement, then x is a subset of A. Simil ...
s, regularity implies each instance of set induction.


Metalogic

This now covers variants of all of the eight Zermelo–Fraenkel axioms. Extensionality, Pairing, Union and Replacement are indeed identical. Infinity is stated in a strong formulation and implies Emty Set, as in the classical case. Separation, classically stated redundantly, is constructively not implied by Replacement. Without the
Law of Excluded Middle In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradic ...
, the theory here is lacking, in its classical form, full Separation, Powerset as well as Regularity. Adding at this point would already give . Replacement and Exponentiation can be further strengthened without losing a type theoretical interpretation and in a way that is not going beyond . Those two alterations are discussed next. Like the axiom of regularity, set induction restricts the possible models of the membership relation "\in" and thus that of a set theory, as was the motivation for the principle in the 20's. The added proof-theoretical strength attained with Induction in the constructive context is significant, even if dropping Regularity in the context of does not reduce the proof-theoretical strength. Aczel was also one of the main developers or
Non-well-founded set theory Non-well-founded set theories are variants of axiomatic set theory that allow sets to be elements of themselves and otherwise violate the rule of well-foundedness. In non-well-founded set theories, the foundation axiom of ZFC is replaced by axiom ...
, which rejects this last axiom.


Strong Collection

Having discussed all the weakened form of axioms of , one can reflect upon the strength of the
axiom of replacement In set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory (ZF) that asserts that the image of any set under any definable mapping is also a set. It is necessary for the construction of certain infinite ...
, also in the context of the classical set theory. For any set y and any natural n, there exists the product y^n recursively given by y^\times y, which have ever deeper
rank Rank is the relative position, value, worth, complexity, power, importance, authority, level, etc. of a person or object within a ranking, such as: Level or position in a hierarchical organization * Academic rank * Diplomatic rank * Hierarchy * H ...
. Induction for unbound predicates proves that these sets exist for all of the infinitely many naturals. Replacement "for n\mapsto y^n" now moreover states that this infinite class of products can be turned into the infinite set, \. This is also not a subset of any previously established set. Going beyond those axioms also seen in Myhill's typed approach, consider the discussed constructive theory with Exponentiation and Induction, but now strengthened by the collection schema. This is an alternative to the Replacement schema and indeed supersedes it, due to not requiring the
binary relation In mathematics, a binary relation associates elements of one set, called the ''domain'', with elements of another set, called the ''codomain''. A binary relation over Set (mathematics), sets and is a new set of ordered pairs consisting of ele ...
definition to be functional, but possibly multi-valued. The principle may be used in the constructive study of larger sets beyond the everyday need of analysis. The axiom concerns a property for relations, giving rise to a somewhat repetitive format in its first-order formulation. The antecedent states that one considers relation \phi between sets x and y that are total over a certain domain set a, that is, \phi has at least one "image value" y for every element x in the domain. This is more general than an inhabitance condition x\in y in a choice axiom, but also more general than the condition of Replacement, which demands unique existence \exists!y. In the consequent, firstly, the axioms states that then there exists a set b which contains at least one "image" value y under \phi, for every element of the domain. Secondly, in this axioms formulation it then moreover states that only such images y are elements of that new codomain set b. It is guaranteeing that b does not overshoot the codomain of \phi and thus the axiom is also expressing some power akin to a Separation procedure. The axiom may be expressed as saying that for every total relation, there exists a set b such that the relation is total in both directions.


Metalogic

This theory without , without unbounded separation and without "naive" Power set enjoys various nice properties. For example, as opposed to with its subset collection schema below, it has the
existence property In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005). Disjunction property The disjunction property is satisfi ...
.


Constructive Zermelo–Fraenkel


Subset Collection

One may approach Power set further without losing a type theoretical interpretation. The theory known as is the axioms above plus a stronger form of Exponentiation. It is by adopting the following alternative, which can again be seen as a constructive version of the
Power set axiom In mathematics, the axiom of power set is one of the Zermelo–Fraenkel axioms of axiomatic set theory. In the formal language of the Zermelo–Fraenkel axioms, the axiom reads: :\forall x \, \exists y \, \forall z \, \in y \iff \forall w \ ...
: An alternative that is not a schema is elaborated on below.


Fullness

For given a and b, let _ be the class of all
total relation In mathematics, a binary relation ''R'' ⊆ ''X''×''Y'' between two sets ''X'' and ''Y'' is total (or left total) if the source set ''X'' equals the domain . Conversely, ''R'' is called right total if ''Y'' equals the range . When ''f'': ''X'' â ...
s between a and b. This class is given as :r \in _ \leftrightarrow \Big(\big(\forall (x \in a). \exists (y \in b). \langle x, y \rangle \in r\big) \, \land\, \big(\forall (p \in r). \exists (x \in a). \exists (y \in b). p = \langle x, y \rangle\big)\Big) As opposed to the function definition, there is no unique existence quantifier in \exists!(y \in b). The class _ represents the space of "non-unique-valued functions" or "
multivalued function In mathematics, a multivalued function, also called multifunction, many-valued function, set-valued function, is similar to a function, but may associate several values to each input. More precisely, a multivalued function from a domain to a ...
s" from a to b, but as set of individual pairs with right projection in b, and only those. One does not postulate _ to be a set, since with Replacement one can use this collection of relations between a set a and the finite b=\, i.e. the "bi-valued functions on a", to extract the set _a of all its subsets. In other words _ being a set would imply the Powerset axiom. Over +\text, there is a single, somewhat clearer alternative axiom to the Subset Collection schema. It postulates the existence of a sufficiently large ''set'' _ of total relations between a and b. This says that for any two sets a and b, there exists a set _\subset _ which among its members inhabits a still total relation s\in _ for any given total relation r\in _. On a given domain a, the functions are exactly the sparsest total relations, namely the unique valued ones. Therefore, the axiom implies that there is a set such that all functions are in it. In this way, Fullness implies Exponentiation. The Fullness axiom is in turn also implied by the so-called Presentation Axiom about sections, which can also be formulated category theoretically.


Binary refinement

The so called binary refinement axiom says that for any a there exists a set _a\subset_a such that for any covering a=x\cup y, the set _a holds two subsets c\subset x and d\subset y that also do this covering job, a=c\cup d. It is a weakest form of the powerset axiom and at the core of some important mathematical proofs. Fullness for relations between the set a and the finite \ implies that this is indeed possible. Taking another step back, plus Recursion and plus Binary refinement already proves that there exists an Archimedean, Dedekind complete pseudo-ordered field. That set theory also proves that the class of left
Dedekind cut In mathematics, Dedekind cuts, named after German mathematician Richard Dedekind but previously considered by Joseph Bertrand, are а method of construction of the real numbers from the rational numbers. A Dedekind cut is a partition of the rat ...
s is a set, not requiring Induction or Collection. And it moreover proves that function spaces into discrete sets are sets (there e.g. \omega\to\omega), without assuming . Already over the weak theory (which is to say without Infinity) does binary refinement prove that function spaces into discrete sets are sets, and therefore e.g. the existence of all
characteristic function In mathematics, the term "characteristic function" can refer to any of several distinct concepts: * The indicator function of a subset, that is the function ::\mathbf_A\colon X \to \, :which for a given subset ''A'' of ''X'', has value 1 at points ...
spaces \^a.


Unprovable claims

The bounded notion of a transitive sets of transitive sets is a good way to define ordinals and enables induction on ordinals. With this, in , assuming that membership of 0 is decidable in all successor ordinals S\alpha proves for bounded formulas. Also, neither
linearity Linearity is the property of a mathematical relationship (''function'') that can be graphically represented as a straight line. Linearity is closely related to '' proportionality''. Examples in physics include rectilinear motion, the linear r ...
of ordinals, nor existence of power sets of finite sets are derivable in this theory, as assuming either implies Power set. The theory does not prove that all function spaces formed from sets in the
constructible universe In mathematics, in set theory, the constructible universe (or Gödel's constructible universe), denoted by , is a particular class of sets that can be described entirely in terms of simpler sets. is the union of the constructible hierarchy . It w ...
L are sets ''inside'' L, and this holds even when assuming Powerset instead of the weaker Exponentiation axiom. So such theories do not prove L to be a model of .


Metalogic

This theory has the numerical existence property and the disjunctive property, but there are concessions: lacks the existence property due to the Subset Schema or Fullness axiom. The existence property is not lacking when the weaker Exponentiation or the stronger but impredicative Powerset axiom axiom is adopted instead. The latter is in general lacking a constructive interpretation. In 1977 Aczel showed that can still be interpreted in
Martin-Löf type theory Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative Foundations of mathematics, foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a ...
, using the propositions-as-types approach, providing what is now seen a standard model of in type theory, . This is done in terms of images of its functions as well as a fairly direct constructive and predicative justification, while retaining the language of set theory. Conversely, interprets . All statements validated in the
subcountable In constructive mathematics, a collection X is subcountable if there exists a partial surjection from the natural numbers onto it. This may be expressed as \exists (I\subseteq).\, \exists f.\, (f\colon I\twoheadrightarrow X), where f\colon I\twohea ...
model of the set theory can be proven exactly via plus the choice principle \Pi\Sigma-AC, stated further above. Exhibiting a type theoretical model, the theory has modest proof theoretic strength, the
Bachmann–Howard ordinal In mathematics, the Bachmann–Howard ordinal (also known as the Howard ordinal, or Howard-Bachmann ordinal) is a large countable ordinal. It is the ordinal analysis, proof-theoretic ordinal of several mathematical theory (logic), theories, such as ...
(see also ). Those theories with choice have the existence property for a broad class of sets in common mathematics. Martin-Löf type theories with additional induction principles validate corresponding set theoretical axioms.


Breaking with ZF

One may further add the anti-classical claim that all sets are
subcountable In constructive mathematics, a collection X is subcountable if there exists a partial surjection from the natural numbers onto it. This may be expressed as \exists (I\subseteq).\, \exists f.\, (f\colon I\twoheadrightarrow X), where f\colon I\twohea ...
, as is the case in the type theoretical model, as an axiom. By Infinity and Exponentiation, \omega\to\omega is an uncountable set, while the class _\omega or even _1 is then provenly not a set, by
Cantor's diagonal argument In set theory, Cantor's diagonal argument, also called the diagonalisation argument, the diagonal slash argument, the anti-diagonal argument, the diagonal method, and Cantor's diagonalization proof, was published in 1891 by Georg Cantor as a m ...
. So this theory then logically rejects Powerset and . In 1989 Ingrid Lindström showed that non-well-founded sets obtained by replacing Set Induction, the constructive equivalent of the
axiom of regularity In mathematics, the axiom of regularity (also known as the axiom of foundation) is an axiom of Zermelo–Fraenkel set theory that states that every non-empty set ''A'' contains an element that is disjoint from ''A''. In first-order logic, the axi ...
(a.k.a. axiom of foundation), in with
Aczel's anti-foundation axiom In the foundations of mathematics, Aczel's anti-foundation axiom is an axiom set forth by , as an alternative to the axiom of foundation in Zermelo–Fraenkel set theory. It states that every accessible pointed directed graph corresponds to exact ...
() can also be interpreted in Martin-Löf type theory.Lindström, Ingrid: 1989
A construction of non-well-founded sets within Martin-Löf type theory
Journal of Symbolic Logic 54: 57–64.
The theory may be studied by also adding back the \omega-induction schema or relativized
dependent choice In mathematics, the axiom of dependent choice, denoted by \mathsf , is a weak form of the axiom of choice ( \mathsf ) that is still sufficient to develop most of real analysis. It was introduced by Paul Bernays in a 1942 article that explores whic ...
, as well as the assertion that every set is member of a
transitive set In set theory, a branch of mathematics, a set A is called transitive if either of the following equivalent conditions hold: * whenever x \in A, and y \in x, then y \in A. * whenever x \in A, and x is not an urelement, then x is a subset of A. Simil ...
.


Intuitionistic Zermelo–Fraenkel

The theory is adopting both the standard Separation as well as
Power set In mathematics, the power set (or powerset) of a set is the set of all subsets of , including the empty set and itself. In axiomatic set theory (as developed, for example, in the ZFC axioms), the existence of the power set of any set is po ...
and, as in , one conventionally formulates the theory with Collection below. As such, can be seen as the most straight forward variant of without . So as noted, in , in place of Replacement, one may use the While the axiom of replacement requires the relation \phi to be
functional Functional may refer to: * Movements in architecture: ** Functionalism (architecture) ** Form follows function * Functional group, combination of atoms within molecules * Medical conditions without currently visible organic basis: ** Functional sy ...
over the set z (as in, for every x in z there is associated exactly one y), the Axiom of Collection does not. It merely requires there be associated at least one y, and it asserts the existence of a set which collects at least one such y for each such x. In classical , the Collection schema implies the
Axiom schema of replacement In set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory (ZF) that asserts that the image of any set under any definable mapping is also a set. It is necessary for the construction of certain infinite ...
. When making use of Powerset (and only then), they can be shown to be classically equivalent. While is based on intuitionistic rather than classical logic, it is considered
impredicative In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
. It allows formation of sets using the
Axiom of Separation In many popular versions of axiomatic set theory, the axiom schema of specification, also known as the axiom schema of separation, subset axiom scheme or axiom schema of restricted comprehension is an axiom schema. Essentially, it says that any ...
with any proposition, including ones which contain quantifiers which are not bounded. Thus new sets can be formed in terms of the universe of all sets, distancing the theory from the bottom-up constructive perspective. With this general Separation, it is easy to define ''sets'' \ with undecidable membership, namely by making use of undecidable predicates defined on a set. Further, the power set axiom implies the existence of a set of
truth value In logic and mathematics, a truth value, sometimes called a logical value, is a value indicating the relation of a proposition to truth, which in classical logic has only two possible values (''true'' or '' false''). Computing In some progr ...
s. In the presence of excluded middle, this set has two elements. In the absence of it, the set of truth values is also considered impredicative. The axioms of are strong enough so that full is already implied by for bounded formulas, or in fact by \forall x. \big(0\in x\lor 0\notin x\big).


Metalogic

As implied above, the subcountability property cannot be adopted for all sets, given the theory proves _\omega to be a set. The theory has many of the nice numerical existence properties and is e.g. consistent with Church's thesis principle as well as with \omega\to\omega being
subcountable In constructive mathematics, a collection X is subcountable if there exists a partial surjection from the natural numbers onto it. This may be expressed as \exists (I\subseteq).\, \exists f.\, (f\colon I\twoheadrightarrow X), where f\colon I\twohea ...
. It also has the disjunctive property. with Replacement instead of Collection has the general existence property, even when adopting relativized dependent choice on top of it all. but as formulated does not. The combination of schemas including full separation spoils it. Even without , the proof theoretic strength of equals that of .


Intuitionistic Z

Again on the weaker end, as with its historical counterpart
Zermelo set theory Zermelo set theory (sometimes denoted by Z-), as set out in a seminal paper in 1908 by Ernst Zermelo, is the ancestor of modern Zermelo–Fraenkel set theory (ZF) and its extensions, such as von Neumann–Bernays–Gödel set theory (NBG). It be ...
, one may denote by the intuitionistic theory set up like but without Replacement, Collection or Induction.


Intuitionistic KP

Let us mention another very weak theory that has been investigated, namely Intuitionistic (or constructive)
Kripke–Platek set theory The Kripke–Platek set theory (KP), pronounced , is an axiomatic set theory developed by Saul Kripke and Richard Platek. The theory can be thought of as roughly the predicative part of ZFC and is considerably weaker than it. Axioms In its fo ...
. The theory has not only Separation but also Collection restricted to \Delta_0, i.e. it is similar to but with Induction instead of full Replacement. It is especially weak when studied without Infinity. The theory does not fit into the hierarchy as presented above, simply because it has Axiom schema of Set Induction from the start. This enables theorems involving the class of ordinals. Of course, weaker versions of are obtained by restricting the induction schema to narrower classes of formulas, say \Sigma_1.


Sorted theories


Constructive set theory

As he presented it, Myhill's system is a theory using constructive first-order logic with identity and three sorts, namely sets,
natural numbers In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called ''cardinal n ...
,
function Function or functionality may refer to: Computing * Function key, a type of key on computer keyboards * Function model, a structured representation of processes in a system * Function object or functor or functionoid, a concept of object-oriente ...
s. Its axioms are: * The usual
Axiom of Extensionality In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of extensionality, or axiom of extension, is one of the axioms of Zermelo–Fraenkel set theory. It says that sets having the same elements ...
for sets, as well as one for functions, and the usual
Axiom of union In axiomatic set theory, the axiom of union is one of the axioms of Zermelo–Fraenkel set theory. This axiom was introduced by Ernst Zermelo. The axiom states that for each set ''x'' there is a set ''y'' whose elements are precisely the elemen ...
. * The Axiom of restricted, or predicative, separation, which is a weakened form of the
Separation axiom In topology and related fields of mathematics, there are several restrictions that one often makes on the kinds of topological spaces that one wishes to consider. Some of these restrictions are given by the separation axioms. These are sometime ...
from classical set theory, requiring that any quantifications be bounded to another set, as discussed. * A form of the
Axiom of Infinity In axiomatic set theory and the branches of mathematics and philosophy that use it, the axiom of infinity is one of the axioms of Zermelo–Fraenkel set theory. It guarantees the existence of at least one infinite set, namely a set containing the ...
asserting that the collection of natural numbers (for which he introduces a constant \omega) is in fact a set. * The axiom of Exponentiation, asserting that for any two sets, there is a third set which contains all (and only) the functions whose domain is the first set, and whose range is the second set. This is a greatly weakened form of the
Axiom of power set In mathematics, the axiom of power set is one of the Zermelo–Fraenkel axioms of axiomatic set theory. In the formal language of the Zermelo–Fraenkel axioms, the axiom reads: :\forall x \, \exists y \, \forall z \, \in y \iff \forall w \ ...
in classical set theory, to which Myhill, among others, objected on the grounds of its
impredicativity In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
. And furthermore: * The usual
Peano axioms In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly ...
for natural numbers. * Axioms asserting that the
domain Domain may refer to: Mathematics *Domain of a function, the set of input values for which the (total) function is defined **Domain of definition of a partial function **Natural domain of a partial function **Domain of holomorphy of a function * Do ...
and
range Range may refer to: Geography * Range (geographic), a chain of hills or mountains; a somewhat linear, complex mountainous or hilly area (cordillera, sierra) ** Mountain range, a group of mountains bordered by lowlands * Range, a term used to i ...
of a function are both sets. Additionally, an Axiom of non-choice asserts the existence of a choice function in cases where the choice is already made. Together these act like the usual
Replacement axiom In set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory (ZF) that asserts that the image of any set under any definable mapping is also a set. It is necessary for the construction of certain infinit ...
in classical set theory. One can roughly identify the strength of this theory with a constructive subtheories of when comparing with the previous sections. And finally the theory adopts * An
Axiom of dependent choice In mathematics, the axiom of dependent choice, denoted by \mathsf , is a weak form of the axiom of choice ( \mathsf ) that is still sufficient to develop most of real analysis. It was introduced by Paul Bernays in a 1942 article that explores whi ...
, which is much weaker than the usual
Axiom of choice In mathematics, the axiom of choice, or AC, is an axiom of set theory equivalent to the statement that ''a Cartesian product of a collection of non-empty sets is non-empty''. Informally put, the axiom of choice says that given any collectio ...
.


Bishop style set theory

Set theory in the flavor of
Errett Bishop Errett Albert Bishop (July 14, 1928 – April 14, 1983) was an Americans, American mathematician known for his work on analysis. He expanded constructive analysis in his 1967 ''Foundations of Constructive Analysis'', where he Mathematical proof, p ...
's constructivist school mirrors that of Myhill, but is set up in a way that sets come equipped with relations that govern their discreteness. Commonly, Dependent Choice is adopted. A lot of
analysis Analysis ( : analyses) is the process of breaking a complex topic or substance into smaller parts in order to gain a better understanding of it. The technique has been applied in the study of mathematics and logic since before Aristotle (38 ...
and
module theory In mathematics, a module is a generalization of the notion of vector space in which the field of scalars is replaced by a ring. The concept of ''module'' generalizes also the notion of abelian group, since the abelian groups are exactly the mod ...
has been developed in this context.


Category theories

Not all formal logic theories of sets need to axiomize the binary membership predicate "\in" directly. A theory like the Elementary Theory of the Categories Of Set (), e.g. capturing pairs of composable mappings between objects, can also be expressed with a constructive background logic.
Category theory Category theory is a general theory of mathematical structures and their relations that was introduced by Samuel Eilenberg and Saunders Mac Lane in the middle of the 20th century in their foundational work on algebraic topology. Nowadays, cate ...
can be set up as a theory of arrows and objects, although
first-order In mathematics and other formal sciences, first-order or first order most often means either: * "linear" (a polynomial of degree at most one), as in first-order approximation and other calculus uses, where it is contrasted with "polynomials of high ...
axiomatizations only in terms of arrows are possible. Beyond that, topoi also have internal languages that can be intuitionistic themselves and capture a notion of sets. Good models of constructive set theories in category theory are the pretoposes mentioned in the Exponentiation section. For some good set theory, this may require enough projectives, an axiom about surjective "presentations" of set, implying Countable Dependent Choice.


See also

*
Axiom schema of predicative separation In axiomatic set theory, the axiom schema of predicative separation, or of restricted, or Δ0 separation, is a schema of axioms which is a restriction of the usual axiom schema of separation in Zermelo–Fraenkel set theory. This name &Del ...
*
Constructive mathematics In the philosophy of mathematics, constructivism asserts that it is necessary to find (or "construct") a specific example of a mathematical object in order to prove that an example exists. Contrastingly, in classical mathematics, one can prove th ...
*
Constructive analysis In mathematics, constructive analysis is mathematical analysis done according to some principles of constructive mathematics. This contrasts with ''classical analysis'', which (in this context) simply means analysis done according to the (more comm ...
* Constructive Church's thesis rule and principle *
Computable set In computability theory, a set of natural numbers is called computable, recursive, or decidable if there is an algorithm which takes a number as input, terminates after a finite amount of time (possibly depending on the given number) and correctly ...
*
Existence Property In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005). Disjunction property The disjunction property is satisfi ...
*
Diaconescu's theorem In mathematical logic, Diaconescu's theorem, or the Goodman–Myhill theorem, states that the full axiom of choice is sufficient to derive the law of the excluded middle, or restricted forms of it, in constructive set theory. It was discovered in 19 ...
*
Epsilon-induction In set theory, \in-induction, also called epsilon-induction or set-induction, is a principle that can be used to prove that all sets satisfy a given property. Considered as an axiomatic principle, it is called the axiom schema of set induction. ...
*
Hereditarily finite set In mathematics and set theory, hereditarily finite sets are defined as finite sets whose elements are all hereditarily finite sets. In other words, the set itself is finite, and all of its elements are finite sets, recursively all the way down to t ...
*
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano a ...
*
Impredicativity In mathematics, logic and philosophy of mathematics, something that is impredicative is a self-referencing definition. Roughly speaking, a definition is impredicative if it invokes (mentions or quantifies over) the set being defined, or (more com ...
*
Intuitionistic type theory Intuitionistic type theory (also known as constructive type theory, or Martin-Löf type theory) is a type theory and an alternative foundation of mathematics. Intuitionistic type theory was created by Per Martin-Löf, a Swedish mathematician and ph ...
*
Law of excluded middle In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradic ...
*
Ordinal analysis In proof theory, ordinal analysis assigns ordinals (often large countable ordinals) to mathematical theories as a measure of their strength. If theories have the same proof-theoretic ordinal they are often equiconsistent, and if one theory has ...
* Subcountability


References


Further reading

* * Aczel, P. and Rathjen, M. (2001)
Notes on constructive set theory
Technical Report 40, 2000/2001. Mittag-Leffler Institute, Sweden.


External links

* Laura Crosilla
Set Theory: Constructive and Intuitionistic ZF
Stanford Encyclopedia of Philosophy The ''Stanford Encyclopedia of Philosophy'' (''SEP'') combines an online encyclopedia of philosophy with peer-reviewed publication of original papers in philosophy, freely accessible to Internet users. It is maintained by Stanford University. Eac ...
, Feb 20, 2009 * Benno van den Berg
Constructive set theory – an overview
slides from Heyting dag, Amsterdam, 7 September 2012 {{DEFAULTSORT:Constructive Set Theory Constructivism (mathematics) Intuitionism Systems of set theory