Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "

=

" and "

\in

" of classical set theory is usually used, so this is not to be confused with a constructive types approach. On the other hand, some constructive theories are indeed motivated by their interpretability in type theories. In addition to rejecting the

principle of excluded middle 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 ...

(

), 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.

Introduction

Constructive outlook

Use of intuitionistic logic

The logic of the set theories discussed here is constructive in that it rejects

, i.e. that the

disjunction 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 ...

\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

\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, system ...

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

\neg P

of the valid law of noncontradiction and using a valid De Morgan's law, already minimal logic does prove

\neg\neg(P \lor \neg P)

for any given proposition

P

. So in words, intuitionistic logic still posits: It is impossible to rule out a proposition and rule out its negation both at once, and thus the rejection of any instantiated excluded middle statement for an individual proposition is inconsistent. More generally, constructive mathematical theories tend to prove classically equivalent reformulations of classical theorems. For example, in constructive analysis, one cannot prove the intermediate value theorem in its textbook formulation, but one can prove theorems with algorithmic content that, as soon as double negation elimination and its consequences are assumed legal, are at once classically equivalent to the classical statement. The difference is that the constructive proofs are harder to find.

Imposed restrictions

A restriction to the constructive reading of existence apriori leads to stricter requirements regarding which characterizations of a set

f\subset X\times Y

involving unbounded collections constitute a (mathematical, and so always implying

total 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 collection ...

is such a non-constructive principle that implies

for the formulas permitted in one's adopted Separation schema, by Diaconescu's theorem. Similar results hold for the Axiom of Regularity in its standard form, as shown below. So at the very least, the development of constructive set theory requires rejection of strong choice principles and the rewording of some standard axioms to classically equivalent ones. Undecidability of disjunctions also affects the claims about total orders such as that of all

ordinal numbers 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 ...

, expressed by the provability and rejection of the clauses in the order defining disjunction

(\alpha \in \beta) \lor (\alpha = \beta) \lor (\beta \in \alpha)

. This determines whether the relation is trichotomous. And this in turn affects the proof theoretic strength defined in ordinal analysis.

Metalogic

As in the study of constructive arithmetic theories, constructive set theories can exhibit attractive disjunction and existence properties. These are features of a fixed theory which relate metalogical judgements and propositions provable in the theory. Particularly well-studied are those such features that can be expressed in Heyting arithmetic, with quantifiers over numbers and which can often be realized by numerals, as formalized in proof theory. In particular, those are the numerical existence property and the closely related disjunctive property, as well as being closed under Church's rule, witnessing any given function to be computable. A set theory does not only express theorems about numbers. Furthermore, one may consider a more general strong existence property that is harder to come by, as will be discussed. The theory has the property if the following can be established: For any property

\phi

, if the theory proves that a set exist that has that property, i.e. if the theory claims the existence statement, then there is also a property

\psi

that uniquely describes such a set instance. More formally, for any predicate

\phi

there is a predicate

\psi

so that :

\vdash\exists x.\phi(x)\implies\vdash\exists !x. \phi(x)\land\psi(x)

The analogous role of the realized numeral is played by defined sets proven to exist according to the theory, and so this is a subtle question concerning term construction and the theories strength. While many theories discussed tend have all the various numerical properties, the existence property can easily be spoiled, as will be discussed. Weaker forms of existence properties have been formulated. Some classical theories can in fact also be constrained to exhibit the strong existence property. Zermelo–Fraenkel set theory

with the

constructible universe 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 ...

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 collection ...

''existence postulate''. Recall that this set of axioms implies the well-ordering theorem, which in particular means that relations for

that establish its well-ordering are formally proven to exist (and claim existence of a least element for all subsets of

with respect to those relations). This is despite that fact that definability of such an ordering is known to be

independent 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 * Independe ...

. 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

, 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 Heyting arithmetic

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 ...

. Now for a context of set theories with quantification over a fully formal notion of an infinite sequences space, i.e. function spaces, as will be defined below. A translation of Church's ''rule'' into the language of the theory itself may then read :

\forall (f\in^).\exists (e\in).\Big(\forall(n\in).\exists(w\in). T(e, n, w)\land U(w, f(n))\Big)

Kleene's T predicate together with the result extraction expresses that any input number

n

being mapped to the number

f(n)

is, through

w

, witnessed to be a computable mapping. Here

now denotes a set theory model of the standard natural numbers and

e

is an index with respect to a fixed program enumeration. Stronger variants have been used, which extend this principle to functions

f\in^X

defined on domains

X\subset

of low complexity. The principle rejects decidability for the predicate

Q(e)

defined as

\exists(w\in). T(e, e, w)

, expressing that

e

is the index of a computable function halting on its own index. Weaker, double negated forms of the principle may be considered too, which do not require the existence of a recursive implementation for every

f

, but which still make principles inconsistent that claim the existence of functions which provenly have no recursive realization. Some forms of a Church's thesis as principle are even consistent with the weak classical second order arithmetic

_0

. The collection of total, computable functions is classically subcountable, which classically is the same as being countable. But classical set theories will generally claim that

^

holds also other functions than the computable ones. For example there is a proof in

that total functions do exist that cannot be captured by a

Turing machine 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 algor ...

. Taking the computable world seriously as ontology, a prime example of an anti-classical conception related the Markovian school is the permitted

subcountability 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\twoh ...

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

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 Luitzen Egbertus Jan Brouwer (; ; 27 February 1881 – 2 December 1966), usually cited as L. E. J. Brouwer but known to his friends as Bertus, was a Dutch mathematician and philosopher, who worked in topology, set theory, measure theory and compl ...

intuitionistic analysis, in a case where the quantifier ranges over infinitely many unending binary sequences and

Q(x)

states that a sequence

x

is everywhere zero. Concerning this property, of being conclusively identified as the sequence which is forever constant, adopting Brouwer's continuity principle rules out that this could be proven decidable for all the sequences. So in a constructive context with a so-called non-classical logic as used here, one may consistently adopt axioms which are both in contradiction to quantified forms of excluded middle, but also non-constructive in the computable sense or as gauged by meta-logical existence properties discussed previously. In that way, a constructive set theory can also provide the framework to study non-classical theories.

History and overview

Historically, the subject of constructive set theory (often also "

") begun with John Myhill's work on the theories also called

and

. In 1973, he had proposed the former as a first-order set theory based on intuitionistic logic, taking the most common foundation

and throwing out the Axiom of choice as well as the principle of the excluded middle, initially leaving everything else as is. However, different forms of some of the

axioms which are equivalent in the classical setting are inequivalent in the constructive setting, and some forms imply

, as will be demonstrated. In those cases, the intuitionistically weaker formulations were consequently adopted. The far more conservative system

is also a first-order theory, but of several sorts and bounded quantification, aiming to provide a formal foundation for

Errett Bishop Errett Albert Bishop (July 14, 1928 – April 14, 1983) was an American mathematician known for his work on analysis. He expanded constructive analysis in his 1967 ''Foundations of Constructive Analysis'', where he proved most of the important th ...

's program of constructive mathematics. The main discussion presents sequence of theories in the same language as

, leading up to Peter Aczel's well studied ''

'', and beyond. Many modern results trace back to Rathjen and his students.

is also characterized by the two features present also in Myhill's theory: On the one hand, it is using the Predicative Separation instead of the full, unbounded Separation schema, see also Lévy hierarchy. Boundedness can be handled as a syntactic property or, alternatively, the theories can be conservatively extended with a higher boundedness predicate and its axioms. Secondly, the impredicative

Powerset axiom 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 \, classical general topology">Classical mathematics">classical general topology. 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">Impredicativity">predicative. The theory denoted

is the constructive version of

, the classical Kripke–Platek set theory 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 theory. Relatedly, Aczel's theory constructive Zermelo-Fraenkel

has been interpreted in a Intuitionistic type theory, 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. 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) 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 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 ...

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 models for constructive set theories have been introduced. These are analogous to presheaf models for intuitionistic set theory developed by Dana Scott 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 ...

, 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 In constructive mathematics, an apartness relation is a constructive form of inequality, and is often taken to be more basic than equality. It is often written as \# (⧣ in unicode) to distinguish from the negation of equality (the ''denial inequal ...

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 ...

s and

P

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)

\forall (z\in A). P(z)

and

\exists z. \big(z\in A\land P(z)\big)

\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)

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. 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=\

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, 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 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

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\

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 co ...

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

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. 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

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 Separation may refer to: Films * ''Separation'' (1967 film), a British feature film written by and starring Jane Arden and directed by Jack Bond * ''La Séparation'', 1994 French film * ''A Separation'', 2011 Iranian film * ''Separation'' (20 ...

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. (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

, for mathematical foundations related to topos theory.

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 can exist in this theory. In a theory with the axiom of regularity, like

, of course that subset

\

can be proven to be equal to

y

itself. As an aside, in a theory with stratification, 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 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, when

Q

denotes some 2-ary predicate, one should not generally expect a subclass

s

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

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 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 is not a necessary feature of constructive type theory, 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 a ...

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\ ...

, 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

. However, some form of induction is. Replacement together with Set Induction (introduced below) also suffices to axiomize

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 axiom ...

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, 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, namely natural numbers and products.

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. 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 of the theory of Peano. 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 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

\forall (a\in A). P(a, c_a)

. It is a theorem that already Robinson arithmetic

''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 sinc ...

, 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 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 relations. 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 In mathematics, a surjective function (also known as surjection, or onto function) is a function that every element can be mapped from element so that . In other words, every element of the function's codomain is the image of one element of i ...

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 contraposit ...

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

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

on setoids 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, the computable sets 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, 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: 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 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 notio ...

, which can be seen as models 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 w ...

: 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 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. *

\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) 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 collection ...

: 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, one should consider the classes :

a=\

b=\

from the proof of Diaconescu's theorem. 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 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 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, 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 states that for every inhabited set

s

, there ''exists'' an element

t

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 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 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

, 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 In set theory, a limit ordinal is an ordinal number that is neither zero nor a successor ordinal. Alternatively, an ordinal λ is a limit ordinal if there is an ordinal less than λ, and whenever β is an ordinal less than λ, then there exists an ...

. It functions as the set theoretical equivalent of a

natural numbers object In category theory, a natural numbers object (NNO) is an object endowed with a recursive structure similar to natural numbers. More precisely, in a category E with a terminal object 1, an NNO ''N'' is given by: # a global element ''z'' : 1 → ''N' ...

in category theory. This then enables a full interpretation of Heyting arithmetic

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 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, the mathematical induction schema has been criticized as possibly being impredicative, 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 and are naturally framed as insights into first- and second-order arithmetic theories. The classical theories starting with bounded arithmetic 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

and

: 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

, 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- ...

) 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 functions total. The theory

\mathsf_1

\Pi_2^0

-conservative over primitive recursive arithmetic

. Note that the

\Sigma_1^0

-induction is also part of the second-order reverse mathematics base system

\mathsf_0

, its other axioms being

plus

\Delta_1^0

-comprehension of subsets of naturals. The theory

\mathsf_0

\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 are unprovable. One relatively weak one being the

Ramsey theorem In combinatorics, Ramsey's theorem, in one of its graph-theoretic forms, states that one will find monochromatic cliques in any edge labelling (with colours) of a sufficiently large complete graph. To demonstrate the theorem for two colours (say ...

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 interact in multiple ways and follow local rules, leading to nonlinearity, randomness, collective dynamics, hierarchy, and emergence. The term is generally used to c ...

comprehension are a relevant reference point for weaker set theories insofar as their language does not merely express arithmetical sets, while all sets of naturals particular such theories prove to exist are just computable sets. Constructive reverse mathematics, which lacks double negation elimination for undecidable sentences, exists as a field but is less developed than its classical counterpart.

Exponentiation

Classical

without the

is still consistent with all existing sets of reals being subcountable, 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 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. 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, 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 ...

, and can at best be taken to be a subcountable 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 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 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 ...

) 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 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 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 \ ...

impredicative. 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

algebra Algebra () is one of the areas of mathematics, 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 mathem ...

and does not necessarily provenly have only two elements. The set

2^x

\

-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

\\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, 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 system, 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 theor ...

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 objects resp. subobjects 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 pre

es with (whenever Infinity is adopted) a

. 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 not ...

. 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 of two nonintersecting monomorphisms 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, a primitive notion. These types (or, in set theory, classes or sets) naturally appear, for example, as the type of the currying bijection between

(z\times x)\to y

and

z\to y^x

, an

adjunction In mathematics, the term ''adjoint'' applies in several situations. Several of these share a similar formalism: if ''A'' is adjoint to ''B'', then there is typically some formula of the type :(''Ax'', ''y'') = (''x'', ''By''). Specifically, adjoin ...

. 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 and Computable analysis.

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 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

is generally the context for proving uniqueness 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 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 that is also Archimedean and

Dedekind complete In mathematics, the least-upper-bound property (sometimes called completeness or supremum property or l.u.b. property) is a fundamental property of the real numbers. More generally, a partially ordered set has the least-upper-bound property if eve ...

, 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,

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 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, e ...

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

, 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 Fan commonly refers to: * Fan (machine), a machine for producing airflow, often used for cooling ** Hand fan, an implement held and waved by hand to move air for cooling * Fan (person), short for fanatic; an enthusiast or supporter, especially wit ...

. 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

). This is discussed below. On another end, there are Kripke's schema (turning all subclasses of

\omega

countable), bar induction, 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

intuitionist 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 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 and other theorems regarding values of continuous functions on the reals. The fixed point theorem in turn implies the intermediate value theorem, 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 enables all partial general recursive functions (or programs, in the sense that they are Turing computable), including ones e.g. non-primitive recursive but

-total, such as the Ackermann function. 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. 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 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\twoh ...

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 sets 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. 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 in type theory. The axiom of regularity 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 sets, 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, 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 axi ...

, 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, 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. 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.

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: An alternative that is not a schema is elaborated on below.

Fullness

For given

a

and

b

, let

_

be the class of all total relations 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 ...

s" from

a

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 ...

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 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 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

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, 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 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 (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, 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

. So this theory then logically rejects Powerset and

. In 1989 Ingrid Lindström showed that

non-well-founded set 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 ...

s obtained by replacing Set Induction, the constructive equivalent of the axiom of regularity (a.k.a. axiom of foundation), in

with Aczel's anti-foundation axiom (

) 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, as well as the assertion that every set is member of a transitive set.

Intuitionistic Zermelo–Fraenkel

The theory

adopting both the standard

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 ...

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 over the set

z

(as in, for every

x

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 infi ...

. 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. It allows formation of sets using the Axiom of Separation 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 values. 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. 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, 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 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 ...

, functions. Its axioms are: * The usual Axiom of Extensionality for sets, as well as one for functions, and the usual Axiom of union. * The Axiom of restricted, or predicative,

separation Separation may refer to: Films * ''Separation'' (1967 film), a British feature film written by and starring Jane Arden and directed by Jack Bond * ''La Séparation'', 1994 French film * ''A Separation'', 2011 Iranian film * ''Separation'' (20 ...

, which is a weakened form of the Separation axiom from classical set theory, requiring that any quantifications be bounded to another set, as discussed. * A form of the Axiom of Infinity 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 classical set theory, to which Myhill, among others, objected on the grounds of its impredicativity. And furthermore: * The usual Peano axioms for natural numbers. * Axioms asserting that the domain and range of a function are both sets. Additionally, an

Axiom of non-choice The axiom of non-choice, also called axiom of unique choice, axiom of function choice or function comprehension principle is a function existence postulate. The difference to the axiom of choice is that in the antecedent, the existence of y is al ...

asserts the existence of a choice function in cases where the choice is already made. Together these act like the usual Replacement axiom 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

, which is much weaker than the usual

Bishop style set theory

Set theory in the flavor of

'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 (3 ...

and module theory 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 can be set up as a theory of arrows and objects, although first-order 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.

References

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. E ...

, 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

Introduction

Constructive outlook

Use of intuitionistic logic

Imposed restrictions

Metalogic

Anti-classical principles

History and overview

Models

Subtheories of ZF

Notation

Language

Variables

Classes

Equality

Merging sets

Set existence

BCST

Separation

No universal set

Predicativity

Replacement

ECST

Number bounds

Functions

General notes on functions

Total functional relations

Computable sets

Choice functions

Diaconescu's theorem

Regularity implies PEM

Arithmetic

Moderate induction in ECST

Recursion

Induction without Infinity

Exponentiation

On countable sets

The class of subsets of a set

Metalogic

Category and type theoretic notions

Analysis

Cauchy sequences

Cauchy reals

Towards the Dedekind reals

Constructive schools

Infinite trees

Restricting function spaces

Induction

Mathematical induction

Set Induction

Metalogic

Strong Collection

Metalogic

Constructive Zermelo–Fraenkel

Subset Collection

Fullness

Binary refinement

Unprovable claims

Metalogic

Breaking with ZF

Intuitionistic Zermelo–Fraenkel

Metalogic

Intuitionistic Z

Intuitionistic KP

Sorted theories

Constructive set theory

Bishop style set theory

Category theories

See also

References

Further reading

External links