#### 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 section 2 of 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.

For completeness, we recall all the axioms of CZF and IZF; our list overlaps with the principles presented in the entry on Zermelo Fraenkel set theory. 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, *X* and *Y*.

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*}. This set 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” *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. Clearly collection implies replacement. It is worth noting that
the standard classical proof of equivalence of replacement and
collection uses foundation.

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. To clarify the meaning of subset collection, we recall 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 (thus on
particular kinds of subsets of the cartesian product of two sets)
rather than on arbitrary subsets. 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 on the one
hand if one required the existence of a set of all total relations
between two sets, then one would obtain powerset in the context of CZF
minus subset collection (Aczel and Rathjen 2001, Ch. 3). On the
other hand, requiring that each relation can be “thinned
down” to a function, would assert the axiom of
choice.

We also note that fullness clearly implies Myhill's exponentiation axiom (discussed in section 1.3.2 of the main article) and is clearly implied by powerset. The fact that fullness 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). That exponentiation does not imply fullness in intuitionistic contexts has been proved by Lubarsky (Lubarsky 2005).

9. ∈-Induction:

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

for every formula φ(a).

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

This schema replaces the 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. Both 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.

Remark: 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 that the unrestricted schemata of collection are validated by Aczel's interpretation of constructive set theory in Martin-Löf type theory. However their interpretation makes essential use of the validity in type theory of the (intensional) axiom of choice (see the discussion on constructive choice principles in the main article). For an interpretation of CZF in a logic-enriched type theory (not requiring the type-theoretic axiom of choice) see (Aczel and Gambino 2002).

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 interesting variant of IZF, called IZF_{Rep}, is obtained by replacing
7 by 7′.

The following theorem holds (for CZF see Aczel 1978):

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

where EM denotes the principle of the excluded middle.

### 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:a→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. This principle is clearly valid in the set theories presented above, in which Replacement holds.

### 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 shows how intuitionistic logic is used in set theory. The second example illustrates how one can avoid unnecessary impredicative reasoning (thus the reasoning 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*, 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*).

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