#### Supplement to Set Theory: Constructive and Intuitionistic ZF

## Axioms of CZF and IZF

The theories Constructive Zermelo-Fraenkel (CZF) and Intuitionistic
Zermelo-Fraenkel (IZF) are formulated on the basis of intuitionistic
first order logic, **IQC** (see the entry on
Intuitionistic Logic). As they
are usually formulated, they include among the logical axioms
the equality axioms, which state
that equality, =, is reflexive and that equal terms can be substituted
for one another in any formula.
The language of CZF and IZF is the same as that of classical ZF, thus
it has only the binary predicate symbol ∈ (membership) as
non-logical symbol. We recall that as we work in intuitionistic logic,
all the binary connectives and the quantifiers (∧, ∨, →,
∃, ∀) are taken as primitive (none is defined in terms of
any of the others). As is usual, we define negation by means of
implication and the constant ⊥ (absurdity): ¬φ
abbreviates φ→⊥. We also write φ↔ψ for
φ→ψ ∧ψ →φ. We write
∀*X*∈*Y* and
∃*X*∈*Y* for
∀*X*(*X*∈*Y* →...) and
∃*X*(*X*∈*Y* ∧...), respectively.

In the following we first introduce all the axioms, with names, and then we define the two systems CZF and IZF. We also recall some choice principles which are compatible with constructive and intuitionistic ZF, and finally give two examples of very simple proofs in CZF. For the sake of readabiliy, we use lower and upper case letters to denote sets.

This document is organised as follows:

### Set-theoretic Axioms

1. Extensionality:

∀x∀y[∀z(z∈x↔z∈y) →x=y].

Extensionality enables us to identify sets which might be defined in
different ways but happen to have the same elements. This is the axiom
which enables us to use the article *the* after the application
of any of the other axioms. Consider, for example, the next axiom
(Pair): given two sets *X* and *Y*, the axiom ensures
the existence of *a* set whose elements equal either *X*
or
*Y*. Extensionality ensures furthermore that there is only one
such a set, *the* unordered pair of *X* and
*Y*. This set is usually informally written as: {*X*,
*Y*}.

2. Pair:

∀x∀y∃z∀w(w∈z↔w=x∨w=y).

As particular case of application of pair, given a set *X* we
can form the singleton set {*X*}, which is the pair
{*X*,*X*}.

3. Union:

∀x∃y∀z[z∈y↔ ∃w(w∈x∧z∈w)].

Given a set *X*, union allows us to form a set
*Y* whose elements are elements of elements of *X*. By
combining union and pair one can form the usual (binary) union of two
sets.

4. Empty set:

∃x∀y ¬(y∈x).

By extensionality the empty set is unique; we denote it by the symbol ∅.

5. Infinity:

∃x[∅∈x∧ ∀y(y∈x→suc(y)∈x)].

Here for set *X*,
*suc*(*X*) (the successor of *X*) is defined as
*X*∪{*X*}. For any
set *X*, *suc*(*X*) exists by union and pair (and
is unique by extensionality).

6. Separation schema:

∀a∃x∀y(y∈x↔y∈a∧ φ(y)),

wherexis not free in φ(y).

Given a set *A*, separation allows one to form a new set, all
of whose elements are elements of *A* and also satisfy a
condition described by a formula φ. This set is
informally written as: {*Y*∈*A* : φ(*Y*)}.

6′. Restricted separation schema:This is the same as separation but holds forboundedformulas φ(y) only. A formula isboundedif all its quantifiers are bounded;i.e., they occur only in one of the forms ∀X∈Yor ∃X∈Y. Bounded formulas are also called restricted or Δ_{0}-formulas. Accordingly, bounded separation is also calledrestricted separationorΔ._{0}separation

In *bounded* separation we require that if quantifiers occur in
φ, they do so only in bounded contexts. By so doing, we ensure
that quantification acts on “previously” constructed sets
only. We thus avoid impredicative contexts in which one quantifies on
the whole universe of sets, also including the set under construction
(see the section on
Predicativity in constructive set theory
of the main article).

7. Collection schema:

∀a[∀x∈a∃yφ(x,y) → ∃b∀x∈a∃y∈bφ(x,y)],

for all formulas φ(x,y) wherebis not free in φ(x,y).

Collection states that if for each element *X* of a given
set *A* we can find a set *Y* such that a relation holds
of *X* and *Y*, then we can find a set *B* which
collects “some” of these *Y*s. That is, *B* is such
that for each element *X* of *A* there is a *Y*
in
*B* such that the relation holds of *X* and
*Y*.

7′. Replacement:

∀a[∀x∈a∃!yφ(x,y) → ∃b∀x∈a∃y∈bφ(x,y)],

for all formulas φ(x,y) wherebis not free in φ(x,y).

Note that the antecedent of replacement is a strengthening of the
antecedent of collection, as it states that for each *X* in
*A* there is *exactly one* *Y* such that
φ(*X*,*Y*) holds. Replacement can be seen as stating
that if the domain of a function is a set, than its range is also a
set.

7″. Strong collection schema:

∀a[∀x∈a∃yφ(x,y) → ∃b(∀x∈a∃y∈bφ(x,y) ∧ ∀y∈b∃x∈aφ(x,y))],

for all formulas φ(x,y) wherebis not free in φ(x,y).

This is a strengthened form of collection which is introduced in systems with bounded separation.

8. Powerset:

∀x∃y∀z[z∈y↔ ∀w(w∈z→w∈x)].

Powerset allows us to form a set of all subsets of a given set
*X*.

8′. Subset collection schema:

∀a∀b∃c∀u[∀x∈a∃y∈bφ(x,y,u) →

∃d∈c(∀x∈a∃y∈dφ(x,y,u) ∧ ∀y∈d∃x∈aφ(x,y,u))],

for all formulas φ(x,y,u) wherecis not free in φ(x,y,u).

In CZF, the subset collection schema takes the place of the powerset
axiom. As the subset collection schema is particularly intricate,
we can clarify its meaning by introducing the
axiom of **fullness**, which is equivalent to subset
collection on the basis of CZF minus subset collection (Aczel
1978). First some terminology. The notion of relation between two
sets *A* and *B* is defined in CZF as usual: a relation
is a set of ordered pairs, the first component of which is an element
of *A* and the second component of which is an element of
*B*. The notion of ordered pair is also standard
(see example 2 below). We say that a
relation *R* between *A* and *B*
is *total* if for each element *X* in *A* there
is an element *Y* in *B* such that *R* holds
of *X* and *Y*. Given sets *A* and *B*, we
say that a set *C* is *full in* *A*
*and* *B* if

- every element of
*C*is a total relation, and - for each total relation
*R*between*A*and*B*, there is a total relation*S*in*C*such that*S*is a subset of*R*.

The axiom of **fullness** states:

∀A∀B∃C[Cis full inAandB].

Compared with powerset, fullness can be seen as focusing on total
relations, that is, on particular kinds of subsets of the Cartesian
product of two sets, rather than on arbitrary subsets of a given
set. Given two sets *A* and *B*, fullness may be read as
stating the existence of a set containing an
“approximation” of each total relation between *A*
and *B*. Note that fullness does not state the existence of a
set of *all* total relations between two sets, as this would be
the same as postulating powerset in the context of CZF minus subset
collection (Aczel and Rathjen 2001, Ch. 3). In addition, it does not
say that each relation can be “thinned down” to a
function, as this would amount to postulating the axiom of choice.

9. ∈-Induction:

∀a(∀y∈aφ(y) → φ(a)) → ∀aφ(a),

for every formula φ(a).

Set induction allows us to induct on the membership relation. It states the
following: suppose that for an arbitrary set *A*, whenever a property φ
holds of all elements of *A* then it propagates to *A* itself; then we can
conclude that the property φ holds of any set *A*.

This schema replaces ZF's axiom of foundation whose usual formulation, as we have explained in the main document, is incompatible with set theories based on intuitionistic logic (for the argument see the supplementary document Set theoretic principles incompatible with intuitionistic logic.)

We also note here that foundation is called Regularity in the
article
Zermelo Fraenkel set theory
in this Encyclopedia. Either terminology can be found in the literature.
Here we prefer to use the name *foundation* because in the context of CZF
regularity usually refers to a different notion, originating from the
classical notion of regular cardinal.

We can now define the theories in question:

CZF:

Principles 1, 2, 3, 4, 5, 6′, 7″, 8′, 9.

The system IZF extends CZF by allowing unrestricted separation and powerset.

IZF:

Principles 1, 2, 3, 4, 5, 6, 7, 8, 9.

Note that IZF has often been formulated with the natural numbers
as urelements (see Friedman 1973a, Beeson 1985).
A well-known variant of IZF, called IZF_{Rep}, is obtained by replacing
7 by 7′.

The following theorem holds:

CZF + EM = IZF + EM = IZR_{Rep}+ EM = ZF,

where EM denotes the principle of the excluded middle (for CZF see Aczel 1978).

Remark: In CZF only the bounded separation schema introduces a restriction on the complexity of the formulas occurring in it, while all the other schemata allow for arbitrary formulas. Note, in particular, that the schemata of collection are unrestricted. This is due to the fact that even the unrestricted schemata are validated by Aczel's interpretation of constructive set theory in Martin-Löf type theory. It is interesting to note that their interpretation makes essential use of the validity in type theory of the axiom of choice (see the discussion on constructive choice principles in the main article). To avoid making use of the type-theoretic axiom of choice Aczel and Gambino (2002) have proposed a refinement of Aczel's original interpretation of constructive set theory in type theory by introducing a variant of type theory known as logic-enriched type theory.

We also note that on the basis of CZF minus subset collection,
subset collection clearly implies Myhill's exponentiation axiom, which
states that the collection of all functions from a set *A* to a
set *B* is a set. Also, powerset clearly implies subset
collection. These implications, however, cannot be reverted. The fact
that subset collection is not as strong as powerset is a consequence
of the fact that the proof-theoretic strength of CZF minus subset
collection plus powerset exceeds by far that of CZF (Aczel and Rathjen
2001, Rathjen 2012b). That exponentiation does not imply fullness in
intuitionistic contexts has been proved by Lubarsky (2005).

### Choice Principles

We here recall the principles of **Countable** and
**Dependent Choice**.

Let ω denote the set of natural numbers (which exists by the
infinity axiom). Countable Choice, **AC _{0}**, is the
following principle (for any ψ):

∀x∈ ω ∃y∈vψ(x,y) → (∃f: ω →v) ∀x∈ ω ψ (x,f(x)),

where *f*: ω → *v* is an
abbreviation for a formal statement expressing the fact
that *f* is a function with domain ω and range contained
in *v*.

Dependent choice, **DC**, is the following statement
(for any ψ):

if ∀x∈a∃y∈aψ(x,y) andb_{0}∈a, then there isf:ω→asuch thatf(0) =b_{0}and ∀n∈ ω ψ (f(n),f(n+1)).

We should also like to mention a consequence of Replacement often
called the *axiom of unique choice* (it has
also been termed the

*axiom of*in (Myhill 1975) for obvious reasons). This is the statement: if for each element

**non-choice***X*of

*A*there is

*exactly one*

*Y*such that a property holds, than we can find a function

*F*with domain

*A*which assigns to each element

*X*of

*A*an element

*F*(

*X*) such the given property holds. That is:

∀x∈A∃!yψ(x,y) → ∃f( Function(f)∧ Domain(f)=A∧ ∀x∈Aψ (x,f(x))),

This principle is clearly valid in the set theories presented above, in which Replacement holds.

See also the discussion on choice principles in the main document: Constructive and intuitionistic ZF; there another constructive choice principle, the presentation axiom, is recalled.

### Two Examples

In a constructive context we sometimes need to be more careful than usual with the proofs of even simple facts. To illustrate this, we now give two simple examples. The first one exemplifies how intuitionistic logic can be used in set theory. The second example illustrates how one can avoid unnecessary impredicative reasoning (thus the proof is not specifically intuitionistic).

*Ordered pairs*In the first example we show that if two ordered pairs are equal, then their first and second coordinates are equal, respectively. The notion of ordered pair can be defined in the same way as in classical set theory, that is (

*A*,*B*) is {{*A*}, {*A*,*B*}}. The present proof differs from the one in the supplement Basic set theory to the entry on set theory, because that one argues by cases, depending on whether or not*A*=*B*. To avoid making use of the principle of excluded middle we can instead argue as follows. Assume that (*A*,*B*) = (*C*,*D*), that is, {{*A*}, {*A*,*B*}} = {{*C*}, {*C*,*D*}}. We want to prove that*A*=*C*and*B*=*D*. As {*A*} is an element of the left-hand side it is also an element of the right-hand side and so either {*A*} = {*C*} or {*A*} = {*C*,*D*}. In either case*A*=*C*. As {*A*,*B*} is an element of the left-hand side it is also an element of the right-hand side and so either {*A*,*B*} = {*C*} or {*A*,*B*} = {*C*,*D*}. In either case*B*=*C*or*B*=*D*. If*B*=*C*then*A*=*B*=*C*so that {*C*} = {*C*,*D*} giving*C*=*D*and hence*B*=*D*. So in either case*B*=*D*.*Cartesian products*Given sets

*A*and*B*we now want to form the cartesian product of*A*and*B*. This is the set, denoted*A*×*B*, of all ordered pairs of the from (*X*,*Y*), with*X*element of*A*and*Y*element of*B*. The present proof should be compared with standard ones which use powerset.Fix

*X*in*A*and observe that for every*Y*in*B*there is*Z*such that*Z*= (*X*,*Y*). By extensionality this set is unique. Apply now replacement to obtain a set*C*of those pairs of the form (*X*,*Y*) for*Y*in*B*,*i.e.**C*= {(*X*,*Y*) :*Y*∈*B*}. As for every*X*in*A*we can find such a*C*(and it is unique), we can apply replacement again and then union to get a set*D*as required. That is,*D*is such that for every*X*in*A*and*Y*in*B*there is*W*in*D*such that*W*= (*X*,*Y*).

For more detailed presentations of IZF and CZF the reader may wish to consult (Beeson 1985; Troelstra and van Dalen 1988; Aczel and Rathjen 2001; 2010).

Bibliographic information for this supplementary document is in the Bibliography for this entry.