## 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 ∀XY and ∃XY for ∀X(XY →...) and ∃X(XY ∧...), 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:
xy[∀z(z xzy) → 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:
xyzw(wzw=xw=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:
xyz[z y ↔ ∃w(wxzw)].

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 ¬(yx).

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

5. Infinity:
x[∅∈x ∧ ∀y(yxsuc(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:
axy(y xya ∧ φ(y)),
where x is 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: {YA : φ(Y)}.

6′. Restricted separation schema: This is the same as separation but holds for bounded formulas φ(y) only. A formula is bounded if all its quantifiers are bounded; i.e., they occur only in one of the forms ∀XY or ∃XY. Bounded formulas are also called restricted or Δ0-formulas. Accordingly, bounded separation is also called restricted separation or Δ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[∀xay φ(x,y) → ∃bxayb φ(x,y)],
for all formulas φ(x,y) where b is 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” Ys. 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[∀xa ∃!y φ(x,y) → ∃bxayb φ(x,y)],
for all formulas φ(x,y) where b is 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[∀xay φ(x,y) → ∃b(∀xayb φ(x,y) ∧ ∀ybxa φ(x,y))],
for all formulas φ(x,y) where b is not free in φ(x,y).

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

8. Powerset:
xyz[z y ↔ ∀w(wzwx)].

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

8′. Subset collection schema:
abcu[∀xayb φ(x, y, u) →
∃dc(∀xayd φ(x, y, u) ∧ ∀ydxa φ(x, y, u))],
for all formulas φ(x,y,u) where c is 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

1. every element of C is a total relation, and
2. 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:

ABC [C is full in A and B].

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(∀ya φ(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 IZFRep, is obtained by replacing 7 by 7′.

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

CZF + EM = IZF + EM = IZRRep + 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, AC0, is the following principle (for any ψ):

x ∈ ω ∃ yv ψ(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 ∀ xaya ψ(x,y) and b0a, then there is f: aa such that f(0) = b0 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 non-choice in (Myhill 1975) for obvious reasons). This is the statement: if for each element 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.

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

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

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

2. 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) : YB}. 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).

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

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