NOTES ON CONSTRUCTIVE SET THEORY

P. ACZEL and M. RATHJEN

REPORT No. 40, 2000/2001

ISSN 1103-467X ISRN IML-R- -40-00/01- -SE

INSTITUT MITTAG-LEFFLER

THE ROYAL SWEDISH ACADEMY OF SCIENCES

Notes on Constructive Set Theory

Peter Aczel^{∗}and Michael Rathjen^{†}

July 16, 2001

Contents

1 Introduction 1-1

2 Some Axiom Systems 2-1 2.1 Classical Set Theory . . . . . . . . . . . . . . . . . . . . . . . 2-1 2.2 Intuitionistic Set Theory . . . . . . . . . . . . . . . . . . . . . 2-2 2.3 Constructive Set Theory . . . . . . . . . . . . . . . . . . . . . 2-2

3 Elementary Mathematics in Constructive Set Theory 3-1 3.1 Class Notation . . . . . . . . . . . . . . . . . . . . . . . . . . 3-1 3.2 Pairing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3-2 3.3 On Restricted Separation . . . . . . . . . . . . . . . . . . . . . 3-3 3.4 Some Consequences of Union-Replacement . . . . . . . . . . . 3-6 3.5 The Natural Numbers . . . . . . . . . . . . . . . . . . . . . . 3-8 3.6 The Real Numbers . . . . . . . . . . . . . . . . . . . . . . . . 3-10

4 Exploiting Set Induction 4-1 4.1 Transitive Closure . . . . . . . . . . . . . . . . . . . . . . . . . 4-1 4.2 Iterations of a monotone set operator . . . . . . . . . . . . . . 4-3 4.3 The Natural Numbers again . . . . . . . . . . . . . . . . . . . 4-4 4.4 Restricted Separation again . . . . . . . . . . . . . . . . . . . 4-6

5 Inductive Definitions 5-1 5.1 Inductive Definitions of Classes . . . . . . . . . . . . . . . . . 5-1 5.2 The Regular Extension Axiom . . . . . . . . . . . . . . . . . . 5-4 5.3 Inductive definitions of Sets . . . . . . . . . . . . . . . . . . . 5-5

Notes on Constructive Set Theory  Section 0

0-1 5.4 Tree Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5-6 5.5 The Set Compactness Theorem . . . . . . . . . . . . . . . . . 5-10

∗Departments of Mathematics and Computer Science, Manchester University †School of Mathematics, Leeds University

6 ⋁-Semilattices 6-1 6.1 Closure Operations on a po-class . . . . . . . . . . . . . . . . 6-1 6.2 Set-generated ⋁-Semilattices . . . . . . . . . . . . . . . . . . . 6-2 6.3 Set Presentable ⋁-Semilattices . . . . . . . . . . . . . . . . . . 6-4 6.4 ⋁-congruences on a ⋁-semilattice . . . . . . . . . . . . . . . 6-6

7 Regarding the Subset Collection Scheme 7-1

8 Choice Principles 8-1 8.1 Diaconescu’s result . . . . . . . . . . . . . . . . . . . . . . . . 8-1 8.2 Constructive Choice Principles . . . . . . . . . . . . . . . . . . 8-3 8.3 The Presentation Axiom . . . . . . . . . . . . . . . . . . . . . 8-6

9 Principles that ought to be avoided in CZF 9-1

10 Large sets in constructive set theory 10-1 10.1 Some metamathematical results about REA . . . . . . . . . . 10-3 10.2 Inaccessibility . . . . . . . . . . . . . . . . . . . . . . . . . . . 10-10 10.3 A nicer rendering of set-inaccessibility . . . . . . . . . . . . . . 10-11 10.4 Mahloness in constructive set theory . . . . . . . . . . . . . . 10-14

11 Intuitionistic Kripke-Platek Set Theory 11-1 11.1 Basic principles . . . . . . . . . . . . . . . . . . . . . . . . . . 11-1 11.2 Σ Recursion in IKP . . . . . . . . . . . . . . . . . . . . . . . 11-4 11.3 Inductive Definitions in IKP . . . . . . . . . . . . . . . . . . . 11-8

Preface

These notes represent work in progress on producing a comprehensive introduction to Constructive Set Theory. An earlier version has been available on the web page of the first author for several years now.

We are both grateful to the Mittag-Leffler Institute for giving us the opportunity to be working in the same place for an extended period during the Logic Year (2000-01), which enabled our collaboration to get off the ground and produce the present version of the notes. We are also grateful to our home institutions^{1} for allowing us to take part in the Logic Year^{2}

1Manchester University Mathematics and Computer Science Departments for Peter Aczel and Leeds University for Michael Rathjen

2In the case of Peter Aczel this involved three months sabbatical leave and he is grateful to his colleagues for allowing this.

1 Introduction

The general topic of Constructive Set Theory originated in the seminal 1975 paper of John Myhill, [Myh75], where a specific axiom system CST was introduced. Constructive Set Theory provides a standard set theoretical framework for the development of constructive mathematics in the style of Errett Bishop^{3} and is one of several such frameworks for constructive mathematics that have been considered. It is distinctive in that it uses the standard first order language of classical axiomatic set theory^{4} and makes no explicit use of specifically constructive ideas. Of course its logic is intuitionistic, but there is no special notion of construction or constructive object. There are just the sets, as in classical set theory. This means that mathematics in constructive set theory can look very much like ordinary classical mathematics. The advantage of this is that the ideas, conventions and practise of the set theoretical presentation of ordinary mathematics can be used also in the set theoretical development of constructive mathematics, provided that a suitable discipline is adhered to. In the first place only the methods of logical reasoning available in intuitionistic logic should be used. In addition only the set theoretical axioms allowed in constructive set theory can be used. With some practise it is not difficult for the constructive mathematician to adhere to this discipline.

Of course the constructive mathematician is concerned to know that the axiom system she is being asked to use as a framework for presenting her mathematics makes good constructive sense. What is the constructive notion of set that constructive set theory claims to be about? An answer to this question has been given in a series of three papers on the Type Theoretic Interpretation of Constructive Set Theory, [Acz78, Acz82, Acz86]. These papers are based on taking Martin-Lof’s Constructive Type Theory as the most acceptable foundational framework of ideas that make precise the constructive approach to mathematics. Those papers show how a particular type of the type theory can be used as the type of sets forming a universe of objects to interprete constructive set theory so that by using the Curry-Howard ‘propositions as types’ idea the axioms of constructive set theory get interpreted as provable propositions.

Why not present constructive mathematics directly in the type theory? This is an obvious option for the constructive mathematician. It has the drawback that there is no extensive tradition of presenting mathematics in a type theoretic setting. So, many techniques for representing mathematical ideas in a set theoretical language have to be reconsidered for a type theoretical language. This can be avoided by keeping to the set theoretical language.

3See [BB85], by Bishop and Bridges

4Myhill’s original paper used some other primitives in CST besides the notion of set.

But this was inessential and it here seems preferable to keep to the standard language of axiomatic set theory.

Surprisingly there is still no extensive presentation of an approach to constructive mathematics that is based on a completely explicitly described axiom system - neither in constructive set theory, constructive type theory or any other axiom system.

One of the aims of these notes is to initiate an account of how constructive mathematics can be developed on the basis of a set theoretical axiom system. At first we will be concerned to prove each basic result relying on as weak an axiom system as possible. But later we will be content to explore the consequences of stronger axiom systems provided that they can still be justified on the basis of the type theoretic interpretation. Because of the open ended nature of constructive type theory we also think of constructive set theory as an open ended discipline in which it may always be possible to consider adding new axioms to any given axiom system.

In particular there is current interest in the formulation of stronger and stronger notions of type universes and hierarchies of type universes in type theory. This activity is analogous to the pursuit of ever larger large cardinal principles by classical set theorists. In the context of constructive set theory we are led to consider set theoretical notions of universe. As an example there is the notion of inaccessible set of Rathjen (see [RGP]). An aim of these notes is to lay the basis for a thorough study of the notion of inaccessible set and other notions of largeness in constructive set theory.

A further motivation for these notes is the current interest in the development of a ‘formal topology’ in constructive mathematics. It would seem that constructive set theory may make a good setting to represent formal topology. We wish to explore the extent to which this is indeed the case.

These notes represent work in progress and are necessarily very incomplete and open to change.

2 Some Axiom Systems

Constructive Set Theory is a variant of Classical Set Theory which uses intuitionistic logic. It differs from another such variant called Intuitionistic Set Theory because of its avoidance of the full impredicativity that Intuitionistic Set Theory has. Constructive Set Theory does not have the Powerset axiom or the full Separation Axiom Scheme. We introduce constructive set theory here by contrasting it with the other two theories. Note that we consider each of these theories as a framework and consider representative axiom systems for them, ZF and IZF for the Classical and Intuitionistic set Theories and CZF_{0} and CZF for Constructive Set Theory.

2.1 Classical Set Theory

The classical Zermelo-Fraenkel axiomatic set theory, ZF, is formulated in first order logic with equality, using a binary predicate symbol ∈ as its only non-logical symbol. We will use 𝕊yθ(y) to abbreviate

∃b∀y[y ∈ b ↔ θ(y).

The axiom system ZF uses the axioms and axiom schemes

Pairing

∀a∀b𝕊y[y = a ∨ y = b]

Union

∀a𝕊y∃x∈a[y ∈ x]

Powerset

∀a𝕊y∀x∈y[x ∈ a]

Infinity

∃a [∃x x ∈ a ∧ ∀x∈a∃y∈a x ∈ y]

Extensionality

∀a∀b[∀x[x ∈ a ↔ x ∈ b] → a = b]

Foundation

∀a[∃x[x ∈ a] → ∃x∈a∀y∈a[y ∉ x]]

Separation

∀ ⋯ ∀a𝕊x [x ∈ a ∧ ϕ(x, …)]

for all formulae ϕ(x, …). Replacement

∀ ⋯ ∀a[∀x∈a∃!yϕ(x, y, …) → 𝕊y∃x∈aϕ(x, y, …)]
for all formulae ϕ(x, y, …).

2.2 Intuitionistic Set Theory

A natural Intuitionistic version of ZF is Intuitionistic Zermelo-Fraenkel (IZF). It is like ZF except that the following changes are made.

1. It uses Intuitionistic logic instead of Classical logic.

2. It uses the Set Induction Scheme instead of the Foundation axiom.

3. It uses the Collection Scheme instead of the Replacement Scheme. Set Induction

∀ ⋯ ∀a [∀x∈aϕ(x, …) → ϕ(a, …)] → ∀aϕ(a, …)

Collection

∀ ⋯ ∀a[∀x∈a∃yθ(x, y, …) → ∃b ∀x∈a∃y∈b θ(x, y, …)]

2.3 Constructive Set Theory

CZF_{0}

Our first axiom system for Constructive Set Theory, CZF_{0}, is like IZF except for the following changes.

1. It uses the Replacement Scheme instead of the Collection Scheme.

2. It drops the Powerset Axiom.

3. It uses the Mathematical Induction Scheme instead of the Set Induction Scheme.

4. It uses the Restricted Separation Scheme instead of the full Separation

Scheme.

\overline{2-2}

5. It uses the Strong Infinity Axiom instead of the Infinity axiom.

Restricted Separation

∀ ⋯ ∀a𝕊x [x ∈ a ∧ ϕ(x, …)]

for all restricted formulae ϕ(x, …). A formula is restricted if all its quantifiers are restricted; i.e. occur only in one of the forms ∃x∈y or ∀x∈y.

Strong Infinity

𝕊xNat(x)]

where we use the following abbreviations.

• T rans(a) for (∀y ∈ a)(∀z ∈ y)[z ∈ a],

• Empty(y) for (∀z ∈ y)⊥,

• Succ(z, y) for ∀u[u ∈ y ↔ u ∈ z ∨ u = z],

• Nat(x) for ∃a[T rans(a) ∧ (∀y ∈ a)[Empty(y) ∨ ∃zSucc(z, y) ∧ x ∈

a].

Mathematical Induction

∃y[Empty(y) ∧ ϕ(y, …)] ∧
∀x[ϕ(x, …) → ∃y(ϕ(y, …) ∧ Succ(x, y))]
→ ∀x[Nat(x) → ϕ(x, …)]

The Union-Replacement Scheme

This is a natural scheme that combines the Union Axiom with the Replacement Scheme.

∀ ⋯ ∀a[∀x∈a𝕊yϕ(x, y, ⋯) → 𝕊y∃x∈aϕ(x, y, ⋯)]

Proposition: 2.1 Given the Extensionality and Pairing axioms the Union-Replacement axiom scheme is equivalent to the combination of the Union axiom and the Replacement axiom scheme.

Proof: Assume Union-Replacement and let ∀x ∈ ∃!y ϕ(x, y). Then, as singleton classes are sets,

∀x∈a𝕊yϕ(x, y)

so that by Union-Replacement

𝕊y∃x∈aϕ(x, y).

So we have proved replacement. The Union axiom follows from the instance of Union-replacement where ϕ(x, y) is y ∈ x.

Conversely, given the Union axiom and the Replacement scheme, suppose that ∀x∈a𝕊yϕ(x, y). Then

∀x∈a∃!z∀y[y ∈ z ↔ ϕ(x, y)].

So, by Replacement we may form the set

{z | ∃x∈a∀y[y ∈ z ↔ ϕ(x, y)]}.

By the Union axiom we may form the union set of this set, which is

{y | ∃x∈aϕ(x, y)}.

Thus we have proved the Union-Replacement axiom scheme. ■

So the axiom system CZF_{0} can be considered to consist of the three axioms of Extensionality, Pairing and Strong Infinity and the three schemes of Restricted Separation, Union-Replacement and Mathematical Induction.

Constructive Zermelo Fraenkel, CZF

The constructive Set Theory CZF is obtained from CZF_{0} as follows.

1. Add the Set Induction Scheme and drop Mathematical Induction,

2. Add the Subset Collection Scheme,

3. Use the Strong Collection Scheme instead of the Replacement Scheme.

4. Use the ordinary Infinity axiom instead of Strong Infinity.

In stating the two Collection schemes we shall use 𝔹(x ∈ a, y ∈ b)ϕ as an abbreviation for

∀x∈a∃y∈bϕ ∧ ∀y∈b∃x∈aϕ.

Subset Collection

∀a∀b∃c [ ∀u ∀x∈a∃y∈b θ(x, y, u) → ∃z∈c 𝔹(x∈a, y∈z)θ(x, y, u) ]

Strong Collection

∀ ⋯ ∀a[ ∀x∈a∃yθ(x, y, …) → ∃b 𝔹(x∈a, y∈b) θ(x, y, …) ]

3 Elementary Mathematics in Constructive Set Theory

We show how to develop some of the standard apparatus for representing mathematical ideas in CZF_{0}. Recall that the non-logical axioms and schemes of this constructive set theory are the three axioms of Extensionality, Pairing and Strong Infinity and the three schemes of Restricted Separation, Union-Replacement and Mathematical Induction.

3.1 Class Notation

In doing mathematics in Constructive Set Theory we shall exploit the use of class notation and terminology, just as in Classical Set Theory. So, if ϕ(x) is a first order formula in the language of set theory with one free variable x, that may have parameters for sets, then we may define a class A.

A = {x | ϕ(x)}

with defining axiom

∀x[ x ∈ A ↔ ϕ(x) ].

In particular each set a is identified with the class {x | x ∈ a}. Classes A, B are defined to be equal if

∀x[x ∈ A ↔ x ∈ B].

Also, A is a subclass of B, written A ⊆ B, ∀x ∈ A x ∈ B. So, without assuming any non-logical axioms we may form the following classes, where A, B, C are classes and a, a_{1}, …, a_{n} are sets.

1. {a_{1}, …, a_{n}} = {x | x = a_{1} ∨ ⋯ ∨ x = a_{n}}. When n = 0 this is the empty class ∅.

2. ⋃ A = {x | ∃y∈A x ∈ y}.

3. A ∪ B = {x | x ∈ A ∨ x ∈ B}.

4. a^{+} = a ∪ {a}.

5. P ow(A) = {x | x ⊆ A}.

6. {x ∈ B | ϕ(x)} = {x | x ∈ B ∧ ϕ(x)}.

7. V = {x | x = x}.

If A is a class and θ(x, y) is a formula in the language of set theory, that may have parameters for sets and has at most the variables x, y occuring free, then we may form a family of classes (B_{a})_{a∈A}, where for each a ∈ A

B_{a} = {y | θ(a, y)}.

If (B_{a})_{a∈A} is a family of classes then we may form the class

⋃_{a∈A} B_{a} = {y | ∃a∈A y ∈ B_{a}}.

3.2 Pairing

Here we introduce unordered and ordered pairs, cartesian products of classes and relations and function between classes. We will only use the axioms of Extensionality and Pairing.

The Pairing axiom asserts that for all sets a, b the class {a, b} is a set, the unordered pair of a and b. In particular, when a = b we get that the singleton {a} is a set.

Ordered Pairs

We define ordered pairs as usual. For sets a, b let

(a, b) = {{a}, {a, b}}.

Proposition: 3.1

(a, b) = (c, d) ⇒ [a = c ∧ b = d].

Proof: The usual classical proof argues by cases depending, for example, whether or not a = b. This method is not available here as we cannot assume that instance of the classical law of excluded middle. Instead we can argue as follows. Assume that (a, b) = (c, 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 = c = b so that the two sets in (a, b) are equal and hence {c} = {c, d} giving c = d and hence b = d. So in either case b = d. ■ Cartesian Products of Classes

For classes A, B let A × B be the class given by

A × B = {z | ∃a∈A∃b∈B z = (a, b)}.

Relations and Functions between Classes

If R is a class of ordered pairs then we use aRb for (a, b) ∈ R. If A, B are classes and R ⊆ A × B such that

∀x∈A∃y∈B xRy

then we will write

R : A^{>−} B

and if also

∀y∈B∃x∈A xRy

then we write

R : A^{>−<} B.

If

∀x∈A∃!y∈B xRy

then we use the standard notation

R : A → B,

and for each a ∈ A we write R(a) for the unique b ∈ B such that aRb and let

{R(x) | x ∈ A} = {y ∈ B | ∃x ∈ A[y = R(x)]}.

3.3 On Restricted Separation

If a is a set and ϕ(x) is a restricted formula with only the variable x occuring free, but with parameters for sets then, by Restricted Separation the class

{x ∈ a | ϕ(x)}

is a set. We show that, given only the axioms of Extensionality and Pairing and the Union-Replacement scheme, the scheme of Restricted Separation is equivalent to the conjunction of the following three instances.

Emptyset: 𝕊y⊥.

Equality: (∀a)(∀b)(𝕊y)[Empty(y) ∧ a = b].

Infimum: ∀a[∀x∈a∀y∈x Empty(y) → 𝕊y[Empty(y) ∧ ∀x∈a y ∈ x]].

Proof of Restricted Separation We assume only the axioms of Extensionality and Pairing, the Union-Replacement scheme and the axioms Emptyset, Equality and Infimum.

By the Emptyset axiom we may form the set 0 = {y | ⊥} and so the set 1 = {0}. Let Ω = P ow(1). We think of the elements of Ω as truth values, with 0 representing falsity and 1 representing truth. In constructive mathematics we cannot assert that those are the only truth values. Moreover in constructive set theory we cannot even assert that the class of truth values form a set.

For each class A ⊆ Ω let

• ⋁ A = {x | x ∈ 1 ∧ ∃y∈A x ∈ y} = ⋃ A,

• ⋀ A = {x | x ∈ 1 ∧ ∀y∈A x ∈ y}.

For each set a ∈ P ow(Ω) the class ⋁ a is a set in Ω by the Union axiom and ⋀ a is a set in Ω by the Infimum Axiom.

If θ is a formula and c ∈ Ω such that [θ ↔ 0 ∈ c] then, by Extensionality, c is unique and we call c the truth value of θ. For any formula θ we use !θ to abbreviate

∃c∈Ω [θ ↔ 0 ∈ c]

Proposition: 3.2

1. If ∀x∈a !ϕ(x) then !∀x∈aϕ(x) and !∃x∈aϕ(x).

2. If !ϕ_{1} ∧ !ϕ_{2} then

(a) ![ϕ_{1} ∧ ϕ_{2}]

(b) ![ϕ_{1} ∨ ϕ_{2}]

(c) ![ϕ_{1} → ϕ_{2}]

3. !ϕ → !¬ϕ

4. ∀a∀b ![a = b].

5. ∀a∀b ![a ∈ b].

6. !ϕ for each restricted formula ϕ.

Proof:

1. By the assumption, using Union-Replacement we get

𝕊c[c ∈ Ω ∧ ∃x∈a[ϕ(x) ↔ 0 ∈ c]].

So we may form the set

b = {c ∈ Ω | ∃x∈a[ϕ(x) ↔ 0 ∈ c]}.

This is in P ow(Ω) so that ⋁ b, ⋀ b ∈ Ω and

∀x∈aϕ(x) ↔ 0 ∈ ⋀ b

and

∃x∈aϕ(x) ↔ 0 ∈ ⋁ b.

2. Let c_{1}, c_{2} ∈ Ω such that

ϕ_{i} ↔ 0 ∈ c_{i}

for i = 1, 2. Then c_{∧} = ⋀{c_{1}, c_{2}} ∈ Ω and

[ϕ_{1} ∧ ϕ_{2}] ↔ 0 ∈ c_{∧}

giving (i). Similarily c_{∨} = ⋁{c_{1}, c_{2}} ∈ Ω and

[ϕ_{1} ∨ ϕ_{2}] ↔ 0 ∈ c_{∨}

giving (ii). For (iii) let c_{→} = ⋀{c_{2} | x ∈ c_{1}} ∈ Ω and

[ϕ_{1} → ϕ_{2}] ↔ 0 ∈ c_{→}.

3. As 0 ∈ Ω and 0 = 1 ↔ 0 ∈ 0 and ¬ϕ ↔ [ϕ → 0 = 1].

4. This is just the Equality axiom.

5. a ∈ b ↔ ∃y∈b[a = y]. Hence, by 1 and 4, ![a ∈ b].

6. By induction on the way a restricted formula is built up, using 4,5 for

atomic ϕ, 2,3 for the connectives and 1 for the restricted quantifiers. Lemma: 3.3 For each formula ϕ(x)

∀x∈a!ϕ(x) → 𝕊x[x ∈ a ∧ ϕ(x)].

Proof: Assume that ∀x∈a!ϕ(x). Then for each x ∈ a we may form the set b_{y} = {y | y = 0 ∧ ϕ(x)} and hence, by Replacement, the set {(y, x) | y ∈ b_{x}}. Hence, by Replacement again we may form the set

f = {(x, {(y, x) | y ∈ b_{x}}) | x ∈ a}.

Note that f is a function with domain a such that for each x ∈ a the value f(x) is itself the constant function with value x defined on the set b_{x}. Hence, by Union-Replacement

{x ∈ a | ϕ(x)} = {x | x ∈ a ∧ ϕ(x)} = ⋃_{x∈a} ran(f(x))

is a set. ■

Theorem: 3.4 Every instance of Restricted Separation can be proved in the theory obtained from CZF_{0} by replacing the Restricted Separation scheme by the three axioms Emptyset, Equality and Infimum.

Proof: Let ϕ(x) be a restricted formula. Then by part 6 of Proposition 3.2 ∀x∈a !ϕ(x) and hence

𝕊x[x ∈ a ∧ ϕ(x)].

■

3.4 Some Consequences of Union-Replacement

We now consider a few consequences of Union-Replacement.

Quotients

Let A be a set and let R be a subset of A × A that is an equivalence relation on A. Then for each a ∈ A we may form its equivalence class

[a]_{R} = {x ∈ A | xRy}

which is actually a set, by Restricted Separation. To see that xRy can be given by a restricted formula observe that

xRy ⟺ (∃z ∈ R)[z = (x, y)]

where

\begin{aligned}z = (x, y) ⟺ & (∀u ∈ z)[u = \{x\} ∨ u = \{x, y\}] \\ & ∧ (∃u ∈ z)[u = \{x\}] ∧ (∃u ∈ z)[u = \{x, y\}] \end{aligned}

and

\begin{aligned}u = \{x\} & ⟺ [x ∈ u ∧ (∀z ∈ u)(z = x)] \\ u = \{x, y\} & ⟺ [x ∈ u ∧ y ∈ u ∧ (∀z ∈ u)(z = x ∨ z ∈ y)] \end{aligned}

We may then use Replacement to form the quotient set of A with respect to R.

A/R = {[a]_{R} | a ∈ A}.

If (B_{a})_{a∈A} is a family of classes and each B_{a} is actually a set then we have a family of sets and we may form the class

{B_{a} | a ∈ A} = {z | ∃a∈A z = B_{a}}.

If A is also a set then {B_{a} | a ∈ A} is a set, by Replacement and ⋃_{a∈A} B_{a} is a set, by Union-Replacement.

The Union Axiom asserts that the class ⋃ A is a set for each set A. So, using the Pairing axiom we get that the class A ∪ B is a set whenever A, B are sets and hence that {a_{1}, …, a_{n}} is a set whenever a_{1}, …, a_{n} are sets for n > 0.

Proposition: 3.5 If A, B are sets then so is the class A × B.

Proof: Let A,B be sets. Then, as

{a} × B = {(a, b) | b ∈ B}

is a set, by Replacement, so is

A × B = ⋃_{a∈A}({a} × B)

by Union-Replacement. ■ Classes of Functions

Note that if A is a set and F : A → B then, by Replacement,

F = {(a, F (a)) | a ∈ A}

is a set. If a is a set and B is a class then we may form the class ^{a}B of all functions from a to B, given by

aB = {f | f : a → B}.

3.5 The Natural Numbers

Recall from Subsection 2.3 that we defined Nat(x) to be ∃a[T rans(a)∧(∀y ∈ a)[Empty(y) ∨ ∃zSucc(z, y) ∧ x ∈ a]. Let ℕ be the class {x | Nat(x)} and let 0 = ∅ and S = {(n, n^{+}) | n ∈ ℕ}. Call a class A inductive if 0 ∈ A and (∀x ∈ A)[x^{+} ∈ A]. Note that ℕ is an inductive class and the Strong Infinity axiom expresses that it is an inductive set. On the other hand the Mathematical Induction scheme expresses that ℕ is a subclass of each inductive class and so is the smallest inductive class.

It is now easy to observe the following fundamental result.

Proposition: 3.6 The structure consisting of the class ℕ with 0 and S is a model of the Dedekind-Peano axioms for the natural numbers in the following sense.

1. 0 ∈ ℕ.

2. S : ℕ → ℕ.

3. S(n) ≠ 0 for n ∈ ℕ.

4. S(n) = S(m) ⇒ n = m for n, m ∈ ℕ.

5. 0 ∈ A ∧ (∀n ∈ A)(S(n) ∈ A) ⇒ ℕ ⊆ A for each class A.

The first three can be proved without assuming either of the Strong Infinity axiom or the Mathematical Induction scheme. The fifth is just the Mathematical Induction Scheme and the fourth can be proved using Mathematical Induction and the definition of S.

Theorem: 3.7 (Primitive Recursion - unparametrized) Let A be class, a_{0} ∈ A and F : ℕ × A → A. Then there is a unique function H : ℕ → A such that

\{ \begin{matrix}H(0) & = a_{0}, \\ H(n^{+}) & = F (n, H(n)), for n ∈ ℕ \end{matrix}

Proof: Call a set X good if, for some m ∈ ℕ, X : m^{+} → A such that X(0) = a_{0} and for all n ∈ m X(n^{+}) = F (n, X(n)). Let

H = ⋃{X | X is good}.

Then standard arguments, using mathematical induction show that H is the required function. An easy mathematical induction show that any two good functions agree where they are both defined. That

∀n∈ℕ∃a∈A (n, a) ∈ H

is proved by mathematical induction on n. For the base case observe that

X_{0} = {(0, a_{0})} : 0^{+} → A

is good. For the induction step observe that if X : n^{+} → A is good then so is

X^{+} = X ∪ {(n^{+}, F (n, X(n)))} : n^{++} → A.

As good functions agree where they are both defined H : ℕ → A and H agrees with every good function. It follows that H satisfies the above equations and is the unique function to do so. ■

Corollary: 3.8 The Dedekind-Peano axioms are categorical; i.e. any other triple (ℕ′, 0′, S′) satisfying the five axioms is isomorphic to (ℕ, 0, S).

Corollary: 3.9 (Primitive Recursion - parametrized) Let A, B be classes and let F_{0} : B → A and F_{1} : B × ℕ × A → A. Then there is a unique H : B × A → A such that

\{ \begin{matrix}H(b, 0) & = F_{0}(b), \\ H(b, n^{+}) & = F_{1}(b, n, H(b, n)), for n ∈ ℕ. \end{matrix}

Proof: By the theorem, for each b ∈ B there is a unique h ∈^{ℕ} A such that

(∗) \{ \begin{matrix}h(0) & = F_{0}(b), \\ h(n^{+}) & = F_{1}(b, n, h(n)), for n ∈ ℕ. \end{matrix}

Let H be the class of all ((b, n), a) such that b ∈ B and h(n) = a for some h ∈^{ℕ} A. Then H : B × ℕ → A has the desired properties. ■

Using this result we can give the usual primitive recursive definitions of the standard arithmetical operations on ℕ such as addition and multiplication. It follows that we get an interpretation of Heyting Arithmetic.

The Integers and Rationals

The ordered integral domain of integers and the ordered field of rationals can be defined from ℕ in CZF_{0} in any of the standard ways and will have the familiar properties. Moreover the sets ℕ of natural numbers, ℤ of integers and ℚ of rationals form discrete sets; i.e. equality on these sets is decidable, and also the ordering relations on these sets are decidable. This is in contrast to the situation for real numbers.

3.6 The Real Numbers

We assume given the ordered field of rational numbers and discuss the constructive set theoretical construction of the real numbers.

The real numbers are introduced to fill gaps in the ordered set of rationals. So, for example, the real number \sqrt{2} fills the gap between the rationals r on the left such that r^{2} < 2 and the rationals s on the right such that s^{2} > 2. This gap is infinitely small in the sense that for any rational ϵ > 0 there is a rational r on the left of the gap such that r + ϵ is on the right of the gap. So r is a rational approximation to \sqrt{2} with error < ϵ. Exactly one real number can fill such a gap. This idea of real numbers as objects that uniquely fill infinitely small gaps leads to the Dedekind cut approach to the set theoretic construction of the real numbers.

For each set X of rational numbers let

\begin{aligned}X^{<} & = \{r ∈ ℚ | ∃s ∈ X[r < s]\}, \\ X^{>} & = \{r ∈ ℚ | ∃s ∈ X[r > s]\}. \end{aligned}

Definition: 3.10 A two-sided Dedekind cut is a pair (X, Y) of sets X, Y of rationals such that

1. r ∈ X ∧ s ∈ Y ⇒ r < s,

2. X = X^{<} ∧ Y = Y^{>},

3. ∃r ∈ X∃s ∈ Y [s − r = ϵ] for each rational ϵ > 0.

Each of the two sides of a two-sided Dedekind cut determines the other side.

Proposition: 3.11 If (X, Y) is a two-sided Dedekind cut then Y = (ℚ−X)^{>} and X = (ℚ − Y)^{<}.

In view of this we will focus just on the left side.

Definition: 3.12 A (left) cut is a set X of rationals such that X = X^{<} and, for each rational ϵ > 0, there is r ∈ X such that r + ϵ ∉ X. Let ℝ_{d} be the class of all cuts.

Proposition: 3.13 (X, Y) is a two-sided Dedekind cut iff X ∈ ℝ_{d} and Y = (ℚ − X)^{>}.

Proposition: 3.14 A set X of rationals is in ℝ_{d} iff X = X^{<}, ∃r[r ∈ X], ∃s[s ∈ (ℚ − X)] and

(∀r, s ∈ ℚ)[r < s ⇒ (r ∈ X ∨ s ∉ X)].

Note that, classically, the last condition on the right hand side of the previous proposition is redundant. In CZF_{0} we cannot show that ℝ_{d} is a set. But if we assume the impredicative Powerset axiom then it is a set.

Proposition: 3.15 If P ow(ℕ) is a set then ℝ_{d} is a set.

So, for example, in any topos with a natural numbers object we can form the object ℝ_{d} of Dedekind reals and this is the main notion of real considered in topos theory.

By contrast the usual approach to the reals in constructive mathematics is to focus on Cauchy sequences of rationals. For example in the Bishop approach a real number is defined to be a regular sequence; i.e. a family {r_{n}} of rationals r_{n}, indexed by positive integers n > 0, such that for all n, m > 0,

|r_{n} − r_{m}| < n^{−1} + m^{−1}.

Distinct regular sequences can represent equal real numbers. For regular sequences {r_{n}}, {r′_{n}},

{r_{n}} ∼ {r′_{n}} ⟺ |r_{n} − r′_{n}| < 2n^{−1} for all n > 0.

Let ℝ_{b} be the class of all regular sequences. Although the Powerset axiom is impredicative the Exponentiation axiom is predicative in constructive mathematics. On the assumption of this axiom ℝ_{b} is a set. In fact we have the following result.

Proposition: 3.16 If ^{ℕ}ℕ is a set then ℝ_{b} is a set, so that we can form the quotient set ℝ_{b}/ ∼.

In constructive set theory the elements of this quotient set are the equivalence classes with respect to the equivalence relation. In Bishop’s approach to constructive mathematics the quotient construction is treated in a different way. In that approach each set A comes equipped with its equality relation =_{A}, which can be any defined equivalence relation. So, to form the quotient of A with respect to an equivalence relation ∼ on A, it is only necessary to replace =_{A} by ∼.

What is the relation between ℝ_{b} and ℝ_{d}? With each r̂ = {r_{n}} ∈ ℝ_{b} we can associate

Xr̂ = {r ∈ ℚ | ∃n > 0[r < r_{n} − n^{−1}]}.

Proposition: 3.17 For each r̂ ∈ ℝ_{b}, Xr̂ ∈ ℝ_{d} and, for r̂_{1}, r̂_{2} ∈ ℝ_{b},

r̂_{1} ∼ r̂_{2} ⟺ Xr̂_{1} = Xr̂_{2}.

Definition: 3.18 Let ℝ_{c} = {Xr̂ | r̂ ∈ ℝ_{b}}.

Which elements of ℝ_{d} are in ℝ_{c}?

Proposition: 3.19 ℝ_{c} is the class of those sets X of rationals such that X = X^{<} and, for some f : ℚ_{>0} → X,

f(ϵ) + ϵ ∉ X for all rational ϵ > 0.

For any set A let D(A) be the class of decidable subsets of A, where a subset X of A is a decidable subset of A if

(∀x ∈ A)[x ∈ X ∨ x ∉ X].

Theorem: 3.20 The following are equivalent.

1. ^{ℕ}ℕ is a set.

2. D(ℕ) is a set.

3. ℝ_{b} is a set.

4. ℝ_{c} is a set.

In the Bishop approach to constructive mathematics it has been usual to assume the axiom scheme of Dependent Choices, which implies the Countable Choice Scheme AC_{ℕ,A} for each class A, where

AC_{ℕ,A} If R : ℕ^{>−} A then there is f : ℕ → A such that f ⊆ R.

Proposition: 3.21 (AC_{ℕ,ℕ}) ℝ_{c} = ℝ_{d}.

When AC_{ℕ,A} is not assumed then it is known to be consistent, even with IZF, to assume that there are Dedekind reals that are not Cauchy reals. So it is relevent to ask under what conditions, weaker than the assumption that P ow(ℕ) is a set, does the class ℝ_{d} of Dedekind reals form a set. It turns out that ℝ_{d} is a set in CZF. In fact it is enough, working in CZF_{0}, to assume the special instance SubColl(ℕ, ℕ) of the Subset Collection Scheme.

Definition: 3.22 For sets A, B we define SubColl(A, B) to hold if there is a set C of subsets of B such that for every set R : A^{>−} B there is a set B′ ∈ C such that R : A^{>−<} B′.

Proposition: 3.23 The Subset Collection Scheme implies

(∀A)(∀B)SubColl(A, B).

Theorem: 3.24 1. If AC_{ℕ,ℕ} and ^{ℕ}ℕ is a set then SubColl(ℕ, ℕ).

2. If SubColl(ℕ, ℕ) then ℝ_{d} is a set.

3. If ℝ_{d} is a set then ℝ_{c} is a set. The proofs of parts 1 and 3 of this result are straightforward. We now give an outline of the proof of 2. First note that a set X of rationals is a cut iff X = X^{<} and R_{X} : ℚ_{>0} ^{>−} ℚ, where

R_{X} = {(ϵ, r) ∈ ℚ_{>0} × ℚ | r ∈ X ∧ r + ϵ ∉ X}.

Call a set R : ℚ_{>0} ^{>−} ℚ a Cauchy relation if, for all (ϵ, r), (ϵ′, r′) ∈ R,

|r − r′| < max(ϵ, ϵ′).

The following result is straightforward to prove Proposition: 3.25

1. If X is a Dedekind real then R_{X} is a Cauchy relation.

2. If R is a Cauchy relation then X_{R} is a Dedekind real, where X_{R} = {s ∈ ℚ | (∃(ϵ, r) ∈ R)[s < r − ϵ]}.

3. If X is a Dedekind real and R is a Cauchy subrelation of R_{X} then

X = X_{R}. Because both ℚ and ℚ_{>0} are in one-one correspondence with ℕ, the assumption SubColl(ℕ, ℕ) implies that SubColl(ℚ_{>0}, ℚ). Using this it is not hard to see that there is a set C of Cauchy relations such that every Cauchy relation has a subrelation in C. It follows from Proposition 3.25 that ℝ^{d} = {X_{R} | R ∈ C} so that, by Replacement, ℝ^{d} is a set.

4 Exploiting Set Induction

In this section we generally assume only the axioms of Extensionality and Pairing and the axiom schemes of Union-Replacement and Set Induction. Note that we do not assume the scheme of Restricted Separation.

4.1 Transitive Closure

We show that for each set a there is a smallest set T C(a) that is transitive and has a as a subset.

Let T ransClos(x, y) be the formula

x ⊆ y ∧ T rans(y) ∧ ∀z[x ⊆ z ∧ T rans(z) → y ⊆ z].

Proposition: 4.1 For all a

(∗) ∃!b T ransClos(a, b).

Proof: This will be proved by Set Induction on a. So we may assume as induction hypothesis that

∀x∈a ∃!y T ransClos(x, y).

By Replacement there is a set b such that

∀y[y ∈ b ↔ ∃x∈a T ransClos(x, y).

Let c = a ∪ ⋃ b. We show that T ransClos(a, c).

That a ⊆ c is immediate from the definition of c. To see that c is transitive let x ∈ c. We must show that x is a subset of c. As x ∈ c, either x ∈ a or x ∈ y for some y ∈ b. Note that if y ∈ b then y ⊆ ⋃ b ⊆ c. If x ∈ a then T ransClos(x, y) for some y ∈ b so that x ⊆ y ⊆ c. If x ∈ y for some y ∈ b then x ⊆ y ⊆ c, as T rans(y).

It remains to show that c ⊆ z for each set z such that [a ⊆ z ∧ T rans(z)]. By the definition of c, as a ⊆ z it is only necessary to show that ⋃ b ⊆ z. So let u ∈ ⋃ b. Then u ∈ y for some y ∈ b. So T ransClos(x, y) for some x ∈ a. Then x ∈ z and hence x ⊆ z, as z is transitive. So, as T ransClos(x, y) and T rans(z), y ⊆ z. As u ∈ y, u ∈ z.

We have now proved that T ransClos(a, c). The uniqueness of c is a consequence of the definition of T ransClos(x, y). If also T ransClos(a, c′) then both c ⊆ c′ and c′ ⊆ c so that c = c′. ■

By this proposition for each a we can define T C(a) to be the unique b such that T ransClos(a, b).

Proposition: 4.2

1. [x ∈ a ∨ x ⊆ a] → T C(x) ⊆ T C(a).

2. T C(a) = a ∪ ⋃_{x∈a} T C(x).

We can now prove a convenient variant of Set Induction.

Proposition: 4.3 (T C-Induction)

∀a[∀x∈T C(a)θ(x) → θ(a)] → ∀aθ(a).

Proof: Let θ′(x) be the formula ∀y∈T C(x)θ(y). We will assume that

(∗) ∀a[θ′(a) → θ(a)]

and show that ∀aθ(a).

Claim: ∀x∈a θ′(x) → θ′(a).

Proof of Claim: Let ∀x∈a θ′(x). Then

(1) ∀x∈a∀y∈T C(x) θ(y)

and by (∗),

(2) ∀x∈a θ(x).

Now let z ∈ T C(a). Then, by 2 of the previous proposition, either z ∈ a or z ∈ T C(x) for some x ∈ a. In either case θ(z). Thus we have proved that θ′(a). ■

By the claim we may use Set Induction to get that ∀aθ′(a) and hence, by (∗), we get that ∀aθ(a). ■

4.2 Iterations of a monotone set operator

For any class Y of ordered pairs, for each set a let

Y^{a} = {y | (a, y) ∈ Y }

and

Y^{∈a} = {y | ∃x∈a (x, y) ∈ Y } = ⋃_{x∈a} Y^{x}.

Also let

Y^{∞} = {y | ∃a (a, y) ∈ Y } = ⋃_{a∈V} Y^{a}.

Theorem: 4.4 Let Γ be a monotone operation on sets; i.e. Γ(X) is a set for each set X such that for all sets X, Y

X ⊆ Y → Γ(X) ⊆ Γ(Y).

Then there is a class J of ordered pairs having the following properties.

1. For each set a

(i)_{a} J^{a} = Γ(J^{∈a}),

(ii)_{a} J^{a} is a set.

2. Let Y be a class such that for all sets X

X ⊆ Y → Γ(X) ⊆ Y.

Then

(a) J^{a} ⊆ Y for all a and hence J^{∈a} ⊆ Y for all a.

(b) J^{∞} ⊆ Y. Moreover, assuming Collection, J^{∞} is such a class Y and so is the smallest such class.

Proof: We define J = {G | G is good} where we call a set G of ordered pairs good if, for some transitive set X

(∗) G = {(a, x) | a ∈ X ∧ x ∈ Γ(G^{∈a}).

1. The two parts (i)_{a} and (ii)_{a} will be proved simultaneously by T C-Induction. So, we assume as induction hypothesis that for all b ∈ T C(a) both (i)_{b} and (ii)_{b} hold. So, as a ⊆ T C(a), J^{b} is a set for each b ∈ a so that by Union-Replacement J^{∈a} is a set and hence so is Γ(J^{∈a}). Note that this shows that (i)_{a} → (ii)_{a}. Also, if b ∈ a then x ∈ a and hence J^{x} is a set for each x ∈ b, so that J^{∈b} is a set. It follows that G is a set where

G = ⋃_{b∈T C(a)∪{a}}{b} × Γ(J^{∈b}).

Note that G^{b} = J^{b} for each b ∈ T C(a) so that G^{∈b} = J^{∈b} for all b ∈ T C(a) ∪ {a}. So (∗) holds, with X = T C(a) ∪ {a} and so G is good. It follows that Γ(J^{∈a}) = G^{a} ⊆ J^{a}.

To see that J^{a} ⊆ Γ(J^{∈a}) let x ∈ J^{a}. Then x ∈ G^{a} for some good G. So x ∈ Γ(G^{∈a}) ⊆ Γ(J^{∈a}).

So we have proved (i)_{a} and so (ii)_{a} as we have seen.

2. (a) An easy proof by Set Induction on a.

(b) The first part is an immediate consequence of (a). For the second part let X be a subset of J^{∞}. Then ∀x∈X∃a[x ∈ J^{a}]. So by Collection there is a set b such that ∀x∈X∃a∈b[x ∈ J^{a}]. It follows that X ⊆ J^{∈b} and hence Γ(X) ⊆ Γ(J^{∈b}) = J^{b}.

■

4.3 The Natural Numbers again

Recall that in Subsection 3.5 we defined the class ℕ = {x | Nat(x)} of natural numbers, where Nat(x) is the formula ∃a[T rans(a) ∧ (∀y ∈ a)[Empty(y) ∨ ∃zSucc(z, y) ∧ x ∈ a]. We observed there that ℕ is an inductive class; i.e. it has 0 = ∅ as an element and is closed under the successor operation that maps x to x^{+} = x ∪ {x}. Here this observation makes use of the Emptyset axiom to obtain that the class ∅ is a set. We now exploit Set Induction to obtain the Mathematical Induction scheme, which just expresses that ℕ is a subclass of each Inductive class.

Proposition: 4.5 If A is an inductive class then ℕ ⊆ A.

Proof: Let A be inductive; i.e. 0 = ∅ is a set in A and (∀x ∈ A)[x^{+} ∈ A]. We prove by Set Induction that, for any x,

x ∈ ℕ ⇒ x ∈ A.

The Induction Hypothesis is

(∀y ∈ x)[y ∈ ℕ ⇒ y ∈ A].

So let x ∈ ℕ; i.e. x ∈ X for some transitive set X such that

(∀y ∈ X)[y = 0 ∨ (∃z ∈ y)(y = z^{+})].

As x ∈ X either x = 0 ∈ A or else x = z^{+} for some z ∈ x, in which case z ∈ X ⊆ ℕ, as X is transitive, so that z ∈ A by the Induction Hypothesis and hence x = z^{+} ∈ A. So x ∈ A in either case. ■

Corollary: 4.6 The Emptyset axiom implies that ℕ is the smallest inductive class.

We now exploit Set Induction to show that the Strong Infinity axiom, that ℕ is a set, can be derived from the Emptyset axiom and the ordinary axiom of Infinity:

∃a [∃x x ∈ a ∧ ∀x∈a∃y∈a x ∈ y]

Proposition: 4.7 Assuming the Emptyset axiom the Infinity axiom implies that ℕ is a set.

Proof: Let Γ be the set operator such that for each set Y

Γ(Y) = {0} ∪ {y^{+} | y ∈ Y }.

Observe that, by Replacement, Γ(Y) is a set. It follows that J^{a} is a set for each set a and hence that J^{∈a} is also a set for each set a. Observe that for each set X ⊆ ℕ we have Γ(X) ⊆ ℕ. Hence by part 2(a) of Theorem 4.4 J^{∈a} ⊆ ℕ for all a. To show that ℕ is a set it suffices to show the converse inclusion for some a, as then ℕ is equal to the set J^{∈a}. For that it suffices to have J^{a} ⊆ J^{∈a} for that a, as then J^{∈a} is a set Y satisfying 1,2 above.

So it suffices to find such a set a. Now let a be a set assumed to exist by the Infinity axiom. We must show that Γ(J^{∈a}) ⊆ J^{∈a}. So let b ∈ Γ(J^{∈a}). Then either (i) b = 0 or (ii) b = z^{+} for some z ∈ J^{∈a}.

If (i) then, as by the choice of a there is x ∈ a. So

b = 0 ∈ Γ(J^{∈x}) = J^{x} ⊆ J^{∈a}.

If (ii) then, z ∈ J^{x} for some x ∈ a. Now, by the choice of a, there is y ∈ a such that x ∈ y. It follows that

b = z^{+} ∈ Γ(J^{∈y}) = J^{y} ⊆ J^{∈a}.

So, in either case b ∈ J^{∈a}, as desired. ■

4.4 Restricted Separation again

Recall that we have shown that all instances of the Restricted Separation scheme can be derived using the Emptyset, Equality and Infimum axioms. Here we exploit Set Induction to show that the Equality axiom can be derived from the other two.

Proposition: 4.8 Assuming the Emptyset and Infimum axioms we can derive the Equality axiom and hence all instances of the Restricted Separation scheme.

Proof: Recall that only the proof of part 4 of Proposition 3.2 used the Equality axiom. So we may use parts 1 and 2, the following consequence of the Extensionality axiom and a double set induction on a, b to show that, for all a, b, ![a = b].

a = b ↔ ∀x∈a∃y∈b[x = y] ∧ ∀y∈b∃x∈a[x = y]

■

5 Inductive Definitions

We will think of an inductive definition as a generalised notion of axiom system. We may chacterise a (finitary) axiom system as follows. There are objects, which we will call the statements of the axiom system, and there are axioms and rules of inference. Each axiom is a statement and each rule of inference has instances that consist of finitely many premisses and a conclusion, both the premisses and conclusion being statements. So we may think of an instance of a rule of inference as an inference step \frac{X}{a} where X is the finite set of premisses and a is the conclusion. It is also convenient to think of each axiom a as such a step where the set X of premisses is empty. The theorems of an axiom system may be characterised as the smallest set of statements that include all the axioms and are closed under the rules of inference. Here, a set of statements is closed under a rule if, for each instance of the rule, if the premisses are in the set then so is the conclusion. If we let Φ be the set of steps determined by the axioms and the instances of the rules then we may characterise the set of theorems as the smallest set of statements such that for every step in Φ, if the premisses are in the set then so is the conclusion. Our generalisation is to allow any objects to be statements and to start from an arbitrary class of steps, with each step having a set of premisses that need not be finite. So we are led to the following definitions.

5.1 Inductive Definitions of Classes

We define an inductive definition to be a class of ordered pairs. If Φ is an inductive definition and (X, a) ∈ Φ then we write

\frac{X}{a} Φ

and call \frac{X}{a} an (inference) step of Φ, with set X of premisses and conclusion a. For any class Y, if \frac{X}{a} Φ for some subset X of Y then we will write

⊂\frac{Y}{a} Φ.

The class Y is Φ-closed if for all a

⊂\frac{Y}{a} Φ ⇒ a ∈ Y.

We define the class inductively defined by Φ to be the smallest Φ-closed class. The main result of this section states that this class I(Φ) always exists.

Theorem: 5.1 (Class Inductive Definition Theorem) For any inductive definition Φ there is a smallest Φ-closed class I(Φ).

This result will be proved in the axiom system consisting of Extensionality, Set Induction, Pairing, Union-Replacement and Strong Collection. Note that Union can be used instead of Union-Replacement as Replacement is a consequence of Strong Collection.

The Proof

The proof involves the iteration of the following monotone operator on classes until it closes up at its least fixed point which turns out to be the required class I(Φ). For each class Y let

Γ(Y) = \{a | ⊂\frac{Y}{a} Φ\}.

Note that Γ is monotone; i.e. for classes Y_{1}, Y_{2}

Y_{1} ⊆ Y_{2} ⇒ Γ(Y_{1}) ⊆ Γ(Y_{2}).

As an inductive definition need not be finitary; i.e. it can have steps with infinitely many premisses, we will need transfinite iterations of Γ in general. In classical set theory it is customary to use ordinal numbers to index iterations. Here it is unnecessary to develop a theory of ordinal numbers and we simply use sets to index iterations. This is not a problem as we can carry out proofs by set induction. The following result gives us the iterations we want.

Lemma: 5.2 There is a class J such that for each a,

J^{a} = Γ(⋃_{x∈a} J^{x}).

Proof: Call a set G of ordered pairs good if

(∗) (a, y) ∈ G ⇒ y ∈ Γ(G^{∈a}).

where

G^{∈a} = {y′ | ∃x∈a (x, y′) ∈ G}.

Let J = ⋃{G | G is good}. We must show that for each a

J^{a} = Γ(J^{∈a}).

First, let y ∈ J^{a}. Then (a, y) ∈ G for some good set G and hence by (∗), above, y ∈ Γ(G^{∈a}). As G^{∈a} ⊆ J^{∈a} it follows that y ∈ Γ(J^{∈a}). Thus J^{a} ⊆ Γ(J^{∈a}).

For the converse inclusion let y ∈ Γ(J^{∈a}). Then \frac{Y}{y} Φ for some set Y ⊆ J^{∈a}. It follows that ∀y′∈Y ∃x∈a y′ ∈ J^{x} so that

∀y′∈Y ∃G [ G is good and y′ ∈ G^{∈a}].

By Strong Collection there is a set Z of good sets such that

∀y′∈Y ∃G∈Z y′ ∈ G^{∈a}.

Let G = \{(a, y)\} ∪ ⋃ Z. Then ⋃ Z is good and, as \frac{Y}{y} Φ and Y ⊆ G^{∈a}, G is good. As (a, y) ∈ G we get that y ∈ J^{a}. Thus Γ(J^{∈a}) ⊆ J^{a}. ■

We can now prove the theorem. It only remains to show that J^{∞} is the smallest Φ-closed class. Our argument follows the lines of the proof of part 2 of Theorem 4.4.

To show that J^{∞} is Φ-closed let \frac{Y}{y} Φ for some set Y ⊆ J^{∞}. Then ∀y′∈Y ∃x y′ ∈ J^{x}. So, by Collection, there is a set a such that

∀y′∈Y ∃x∈a y′ ∈ J^{a};

i.e. Y ⊆ J^{∈a}. Hence y ∈ Γ(J^{∈a}) = J^{a} ⊆ I. Thus J^{∞} is Φ-closed.

Now let I be a Φ-closed class. We show that J^{∞} ⊆ I. It sufices to show that J^{a} ⊆ I for all a. We do this by Set Induction on a. So we may assume, as induction hypothesis, that J^{x} ⊆ I for all x ∈ a. It follows that J^{∈a} ⊆ I and hence

J^{a} = Γ(J^{∈a}) ⊆ Γ(I) ⊆ I,

the inclusions holding because Γ is monotone and I is Φ-closed. ■

Call an inductive definition Φ local if Γ(X) is a set for all sets X.

Proposition: 5.3 If Φ is local then both J^{a} and J^{∈a} are sets for each set a.

Proof: We show that J^{a} is a set for each set a by Set Induction on a. The induction hypothesis is that J^{x} is a set for each x ∈ a. It follows that J^{∈a} is a set by Union-Replacement. So, by the assumption, J^{a} = Γ(J^{∈a}) is a set. ■ Note that we could use the alternative construction of Theorem 4.4 to get this result, thereby avoiding the need for Lemma 5.2 which uses Strong Collection. The two constructions of classes J are easily seen to give (extensionally) the same class.

Examples

Let A be a class.

1. H(A) is the smallest class X such that for each set a that is an image

of a set in A

a ∈ P ow(X) ⇒ a ∈ X.

Note that H(A) = I(Φ) where Φ is the class of all pairs (a, a) such that a is an image of a set in A.

2. If R is a subclass of A × A such that R_{a} = {x | xRa} is a set for each a ∈ A then W f(A, R) is the smallest subclass X of A such that

∀a ∈ A [R_{a} ⊆ X ⇒ a ∈ X].

Note that W f(A, R) = I(Φ) where Φ is the class of all pairs (R_{a}, a) such that a ∈ A.

3. If B_{a} is a set for each a ∈ A then W_{a∈A}B_{a} is the smallest class X such

that

a ∈ A & f : B_{a} → X ⇒ (a, f) ∈ X.

Note that W_{x∈A} = I(Φ) where Φ is the class of all pairs (ran(f), (a, f)) such that a ∈ A and f : B_{a} → V.

5.2 The Regular Extension Axiom

A class A is transitive if ∀a∈A a ⊆ A. A regular set is a transitive set A such that

∀a∈A SubColl(a, A, A),

where SubColl(a, b, c) abbreviates

∀r [[r : a^{>−} b] → ∃b′∈c [r : a^{>−<} b′]].

The Regular Extension Axiom (REA) is as follows.

Every set is a subset of a regular set Proposition: 5.4 The Subset Collection Scheme is equivalent to the axiom

∀a∀b∃c SubColl(a, b, c).

Proposition: 5.5 The Subset Collection Scheme is a consequence of REA.

The following weakened notion may also be useful. We call a transitive set A weakly regular if

∀a∈A ∀r [[r : a^{>−} A] → ∃b∈A r : a^{>−} b].

The weakly Regular Extension Axiom (wREA) is as follows.

Every set is a subset of a weakly regular set

5.3 Inductive definitions of Sets

We define a class B to be a bound for Φ if whenever \frac{X}{a} Φ then X is an image of a set b ∈ B; i.e. there is a function from b onto X. We define Φ to be (regular, weakly regular) bounded if

1. \{y | \frac{X}{y} Φ\} is a set for all sets X,

2. Φ has a bound that is a (regular, weakly regular) set.

Proposition: 5.6 Assuming Exponentiation, every bounded inductive definition Φ is local; i.e. Γ(X) is a set for each set X.

Proof: Let B be a bound for Φ. If \frac{Y}{y} Φ then for some b ∈ B there is a surjective f : b → Y. So if X is a set then

Γ(X) = ⋃_{f∈C}\{y | \frac{ran(f)}{y} Φ\}

where C = ⋃_{b∈B} ^{X}b. By Exponentiation and Union-Replacement C is a set. As Φ is bounded \{y | \frac{ran(f)}{y} Φ\} is always a set, so that, by Union-Replacement Γ(X) is a set. ■

The following result does not seem to need any form of Collection.

Theorem: 5.7 (Set Definition Theorem) If Φ is a weakly regular bounded local inductive definition then there is a smallest Φ-closed class I(Φ) which is a set.

Proof: Let A be a weakly regular bound for Φ. Then, as Φ is local, we may apply Proposition 5.3 to get that J^{∈A} is a set. As J^{∈A} ⊆ Y for any Φ-closed class Y it suffices to show that J^{∈A} is Φ-closed.

So let \frac{X}{x} Φ with X a subset of J^{∈A}. Then, as A is a bound for Φ, there is Z ∈ A and surjective f : Z → X. So ∀z ∈ Z f(z) ∈ J^{∈A} and hence ∀z ∈ Z∃a ∈ A f(z) ∈ J^{a}. As A is a weakly regular set and Z ∈ A there is b ∈ A such that ∀z ∈ Z∃a ∈ b f(z) ∈ J^{a}. Hence X ⊆ ⋃_{a∈b} J^{a} so that x ∈ Γ(⋃_{a∈b} J^{a}) = J^{b} ⊆ J^{∈A}. ■

Corollary: 5.8 Assume the Exponentiation Axiom and wREA.

1. Every bounded Φ is weakly regular bounded.

2. If A is a set then

(a) H(A) is a set,

(b) if R ⊆ A × A such that R_{a} = {x | xRa} is a set for each a ∈ A then W f(A, R) is a set.

(c) if B_{a} is a set for each a ∈ A then W_{a∈A}B_{a} is a set.

5.4 Tree Proofs

We may relativise the notion of theorem for an axiom system to a set, X, of assumptions treated as additional axioms. The set of theorems relative to X is then the smallest set of statements of the axiom system that include the axioms, are closed under the rules of inference and also include the assumptions from X. We generalise this idea to inductive definitions. Let I(Φ, X) be the smallest Φ-closed class that has X as a subclass. This exists as it can be defined as I(Φ_{X}) where

Φ_{X} = Φ ∪ ({∅} × X).

We will give another characterisation of I(Φ, X) in terms of a suitable notion of proof. These will be well-founded trees having two kinds of nodes, assumption nodes that will always be leaves and step nodes.

We define the class ℙ of proto-proofs to be the smallest class Y such that for any a

1. (0, a) ∈ Y,

2. If Z is a subset of Y then (1, a, Z) ∈ Y.

For each proto-proof p ∈ ℙ we can define its conclusion concl(p) as follows.

\{ \begin{matrix}concl((0, a)) & = a \\ concl((1, a, Z)) & = a \end{matrix}

For each set Z ⊆ ℙ of proto-proofs let

τ(Z) = {concl(p) | p ∈ Z}.

By recursion on p ∈ ℙ we can define the sets ass(p) of assumptions of p and steps(p) of steps of p using the following equations.

\{ \begin{matrix}ass((0, a)) & = \{a\} \\ ass((1, a, Z)) & = ⋃_{p∈Z} ass(p) \end{matrix}

\{ \begin{matrix}steps((0, a)) & = ∅ \\ steps((1, a, Z)) & = \{(τ(Z), a)\} ∪ ⋃_{p∈Z} steps(p) \end{matrix}

Theorem: 5.9 For any class Φ of ordered pairs and any class X

I(Φ, X) = I′(Φ, X),

where

I′(Φ, X) = {concl(p) | p ∈ ℙ & ass(p) ⊆ X & steps(p) ⊆ Φ}.

Proof: Let

ℙ′ = {p ∈ ℙ | concl(p) ∈ I(steps(p), ass(p))}.

Claim 1: p ∈ ℙ ⇒ p ∈ ℙ′ We will show this by ℙ-induction. So we must show that for all a

1. (0, a) ∈ ℙ′,

2. if Z ∈ P ow(ℙ′) then (1, a, Z) ∈ ℙ′.

For 1: Let p = (0, a). Then

\{ \begin{matrix}concl(p) & = a \\ steps(p) & = ∅ \\ ass(p) & = \{a\} \end{matrix}

So p ∈ ℙ′ as a ∈ I(∅, {a}).

For 2: Let p = (1, a, Z) with Z ∈ P ow(ℙ′). Then

\{ \begin{matrix}concl(p) & = a \\ steps(p) & = \{(τ(Z), a)\} ∪ ⋃_{p′∈Z} steps(p′) \\ ass(p) & = ⋃_{p′∈Z} ass(p′) \end{matrix}

As Z ∈ P ow(ℙ′)

∀p′∈Z [concl(p′) ∈ I(steps(p′), ass(p′))];

But

∀p′∈Z [ steps(p′) ⊆ steps(p) and ass(p′) ⊆ ass(p) ].

It follows that τ(Z) ⊆ I(steps(p), ass(p)). As (τ(Z), a) ∈ steps(p) we get that concl(p) = a ∈ I(steps(p), ass(p)); i.e. p ∈ ℙ′ as required.

Claim 2: I′(Φ, X) ⊆ I(Φ, X).

Let a ∈ I′(Φ, X). Then a = concl(p) for some p ∈ ℙ such that ass(p) ⊆ X and steps(p) ⊆ Φ. By claim 1 p ∈ ℙ′ so that

concl(p) ∈ I(steps(p), ass(p)).

It follows that a = concl(p) ∈ I(Φ, X), as required.

Claim 3: X ⊆ I′(Φ, X) and I′(Φ, X) is Φ-closed.

If a ∈ X then a = concl(p), where p = (0, a) ∈ ℙ with ass(p) = {a} ⊆ X and steps(p) = ∅ ⊆ Φ, so that a ∈ I′(Φ, X).

To see that I′(Φ, X) is Φ-closed let \frac{Y}{y} Φ with Y ⊆ I′(Φ, X). Let R be the class of all pairs (a, p) such that p ∈ ℙ, concl(p) = a, ass(p) ⊆ X and steps(p) ⊆ Φ. Then

∀a∈Y ∃p aRp.

By Strong Collection there is a set Z such that

∀a∈Y ∃p∈Z aRp ∧ ∀p∈Z∃a∈Y aRp.

It follows that Z ∈ P ow(ℙ) and τ(Z) = Y so that p = (1, y, Z) ∈ ℙ so that y = concl(p) ∈ I′(Φ, X).

Claim 4: Let I′ be a class such that X ⊆ I′ and I′ is Φ-closed. Then I′(Φ, X) ⊆ I′. We must show that

∀p∈ℙ ∀a [aRp ⇒ a ∈ I′].

We will do this by induction on p ∈ ℙ. So we must show that

1. if p = (0, a) then aRp ⇒ a ∈ I′,

2. if p = (1, a, Z), with Z ∈ P ow(ℙ) such that

∀p′∈Z ∀a′ [a′Rp′ ⇒ a′ ∈ I′],
then aRp ⇒ a ∈ I′.

For 1: if p = (0, a) and aRp then a ∈ ass(p) ⊆ X ⊆ I′ so that a ∈ I′.

For 2: let p = (1, a, Z), with Z ∈ P ow(ℙ) such that

∀p′∈Z ∀a′ [a′Rp′ ⇒ a′ ∈ I′],
and let aRp. Then \frac{τ(Z)}{a} Φ and τ(Z) ⊆ I′ so that a ∈ I′.

By claims 3 and 4 we get that I(Φ, X) ⊆ I′(Φ, X), so that with claim 2 we are done. ■

Theorem: 5.10 Let A be a regular set such that 2 ∈ A. For any class Φ of ordered pairs such that Φ ⊆ A and any class X

I(Φ, X) = I_{A}(Φ, X),

where

I_{A}(Φ, X) = {concl(p) | p ∈ (ℙ ∩ A) & ass(p) ⊆ X & steps(p) ⊆ Φ}.

Moreover ℙ ∩ A = ℙ_{A} is a set, where ℙ_{A} is the smallest class Y satisfying the conditions 1,2, used in defining ℙ, for all a, Z ∈ A.

Proof: Trivially I_{A}(Φ, X) ⊆ I′(Φ, X) ⊆ I(Φ, X). To show that I(Φ, X) ⊆ I_{A}(Φ, X) it suffices to show that X ⊆ I_{A}(Φ, X) and I_{A}(Φ, X) is Φ-closed. This can be done along the lines of the proof of claim 3 in the previous proof, using the assumption that A is a regular set instead of Strong Collection.

For the last part, that ℙ_{A} ⊆ (ℙ∩A) follows from the fact that Y = (ℙ∩A) satisfies the conditions 1,2, used in defining ℙ, for all a, Z ∈ A. To show that (ℙ ∩ A) ⊆ ℙ_{A} it is enough to show that Y = {p | p ∈ A → p ∈ ℙ_{A}} satisfies the conditions 1,2, used in defining ℙ. Finally observe that ℙ_{A} = I(Ψ) where Ψ is a weakly regular bounded local inductive definition, so that by Theorem 5.7 ℙ_{A} is a set. ■

5.5 The Set Compactness Theorem

Theorem: 5.11 (In CZF + REA) Let A be a set and let Φ be an inductive definition that is a subset of P ow(A) × A. Then there is a set B of subsets of A such that for all classes X and all a

a ∈ I(Φ, X) ⇒ ∃Y ∈B [Y ⊆ X & a ∈ I(Φ, Y)].

Proof: By REA let A′ be a regular set such that {2} ∪ A ∪ Φ ⊆ A′. Let B = {ass(p) | p ∈ ℙ_{A′} & steps(p) ⊆ Φ}. By Theorem 5.10 and Replacement, B is a set and if a ∈ I(Φ, X) then a ∈ I_{A′}(Φ, X) so that a = concl(p) for some p ∈ ℙ_{A′} such that ass(p) ⊆ X and steps(p) ⊆ Φ. Now let Y = ass(p). Then Y ∈ B, Y ⊆ X and a ∈ I(Φ, Y), as desired. ■

6 ⋁-Semilattices

6.1 Closure Operations on a po-class

Given a class A a partial ordering of A is a subclass ≤ of A × A satisfying the standard axioms for a partial ordering; i.e.

1. a ≤ a for all a ∈ A,

2. [a ≤ b ∧ b ≤ c] → a ≤ c,

3. [a ≤ b ∧ b ≤ a] → a = b,

A po-class is a class A with a partial ordering ≤.

Let A be a po-class. Then f : A → A is monotone if

x ≤ y → f(x) ≤ f(y).

We define c : A → A to be a closure operation on A if it is monotone and for all a ∈ A

a ≤ c(c(a)) ≤ c(a).

Note that, for a closure operation c on A, if a ∈ A then

c(a) ≤ a ↔ c(a) = a ↔ ∃y∈A[a = c(y)].

We call a subclass C of A a closure class on A if for each a ∈ A there is \overline{a} ∈ C such that

1. a ≤ \overline{a},

2. a ≤ y → \overline{a} ≤ y for all y ∈ C.

Proposition: 6.1 There is a one-one correspondence between closure operations and closure classes on a po-class A. To each closure operation c : A → A there corresponds the closure class C = {a | c(a) = a} of fixed points of c. Conversely to each closure class C there corresponds the closure operation c which associates with each a ∈ A the unique \overline{a} ∈ C satisfying 1,2 above. These correspondences are inverses of each other.

Example: Let A be a set. Then P ow(A) is a class that is a po-class, when partially ordered by the subset relation on P ow(A).

Let Φ be an inductive definition that is a subset of P ow(A) × A. We call Φ an inductive definition on A. Let

C_{Φ} = {X ∈ P ow(A) | X is Φ-closed}.

Then C_{Φ} is a closure class on P ow(A) whose associated closure operation c_{Φ} : P ow(A) → P ow(A) can be given by

c_{Φ}(X) = I(Φ, X)

for all sets X ⊆ A.

Which closure operations arise in this way? Call a monotone operation f : P ow(A) → P ow(A) set-based if there is a subset B of P ow(A) such that whenever a ∈ f(X), with X ∈ P ow(A), then there is Y ∈ B such that Y ⊆ X and a ∈ f(Y). We call B a baseset for f.

Theorem: 6.2 Let c : P ow(A) → P ow(A), where A is a set. Then c = c_{Φ} for some inductive definition Φ on A if and only if c is a set-based closure operation on P ow(A).

Proof: Let c = c_{Φ}, where Φ is an inductive definition on the set A. That c is a closure operator is an easy consequence of its definition. That it is set-based is the content of Theorem 5.11. For the converse, let c be a set based closure operator on P ow(A), with baseset B and associated closure class C. Let Φ be the set of all pairs (Y, a) such that Y ∈ B and a ∈ c(Y). This is a set by Union-Replacement, as B = ⋃_{Y ∈B}({Y } × c(Y)). It is clearly an inductive definition on A. It is easy to check that for any set X ⊆ A X is Φ-closed if and only if X ∈ C, which will give us the desired result that c = c_{Φ}. ■

6.2 Set-generated ⋁-Semilattices

Let S be a po-class. If X ⊆ S and a ∈ S then a is a supremum of X if for all x ∈ S

∀y∈X[y ≤ x] ↔ a ≤ x.

Note that a supremum is unique if it exists. The supremum of a subclass X of S will be written ⋁ X. A po-class is a ⋁-semilattice if every subset has a supremum.

Let S be a ⋁-semilattice . A subset G is a generating set for S if for every a ∈ S

G_{a} = {x ∈ G | x ≤ a}

is a set and a = ⋁ G_{a}. An ⋁-semilattice is set-generated if it has a generating set.

Example: For each set A the po-class P ow(A) is a set-generated ⋁- semilattice with set G = {{a} | a ∈ A} of generators.

Theorem: 6.3 Let C be a closure class on an ⋁-semilattice S. Then C is a ⋁-semilattice, when given the partial ordering induced from S. If S is setgenerated then so is C. Moreover every set-generated ⋁-semilattice arises in this way from a closure class C on a ⋁-semilattice P ow(A) for some set A.

Proof: Let c be the closure operator associated with the closure class C on the ⋁-semilattice S. It is easy to check that C has the supremum operation ⋁^{C} given by ⋁^{C} X = c(⋁ X) for each subset X of C. Now assume that S has a set G of generators. Let

G^{C} = {c(x) | x ∈ G}.

We show that G^{C} is a set of generators for C. For each a ∈ C let

G_{a}^{C} = {y ∈ G^{C} | y ≤ a}.

We must show that G_{a}^{C} is a set and a = ⋁^{C} G_{a}^{C}. Observe that

G_{a}^{C} = {c(x) | x ∈ G ∧ c(x) ≤ a}
= {c(x) | x ∈ G ∧ x ≤ a}
= {c(x) | x ∈ G_{a}}

so that G_{a}^{C} is a set. Also observe that ⋁^{C} G_{a}^{C} = c(⋁{c(x) | x ∈ G_{a}}). It follows first that a = ⋁{x | x ∈ G_{a}} ≤ ⋁{c(x) | x ∈ G_{a}} ≤ ⋁^{C} G_{a}^{C} and second that ⋁^{C} G_{a}^{C} = ⋁{c(x) | x ∈ G_{a}} ≤ a, as if x ∈ G_{a} then x ≤ a so that c(x) ≤ a. So we get that a = ⋁^{C} G_{a}^{C}.

Finally suppose that S is a set-generated ⋁-semilattice , with set G of generators. Let c : P ow(G) → P ow(G) be given by

c(X) = G_{⋁ X}

for all X ∈ P ow(G). Then it is easy to observe that c is a closure operation on P ow(G). If C is the associated closure class then the function C → S that maps each X ∈ C to ⋁ X ∈ S is an isomorphism between C and S with inverse the function that maps each a ∈ S to G_{a} ∈ C. ■

6.3 Set Presentable ⋁-Semilattices

Given a generating set G for S a subset R of G × P ow(G) is a relation set over G for S if for all (a, X) ∈G×P ow(G)

a ≤ ⋁ X ↔ ∃Y ⊆ X [ (a, Y) ∈ R ].

A set presentation of S is a pair (G, R) consisting of a generating set G for S and a relation set R over G for S.

Definition: 6.4 A set presentable ⋁-semilattice is a ⋁-semilattice that has a set presentation.

Example: For each set A the po-class P ow(A) is a set presentable ⋁- semilattice with set G = {{a} | a ∈ A} of generators and relation set

R = {({a}, {{a}}) | a ∈ A}.

Theorem: 6.5 If S = P ow(A), for some set A and C is a closure class then C is set-presentable if and only if the closure operation associated with C is set-based.

Proof: Assume that S = P ow(A), for some set A, and that c is the closure operation on S associated with C. Also assume that B ⊆ S is a baseset for c. Then for all X ⊆ A and all a ∈ A

(∗) a ∈ c(X) ↔ ∃Y ∈B [Y ⊆ X ∧ a ∈ c(Y)].

Now let A′ be a regular set such that B ∪ G ⊆ A′ and let

R = {(Q, Z) | Q ∈ G ∧ Z ∈ A′ ∧ Q ⊆ c(∪Z) ∧ Z ⊆ G}.

Claim 1: R is a set.

Proof: First observe that T = {Z ∈ A′ | Z ⊆ G} is a set. Also, for each Z ∈ T we may form the set ∪Z so that c(∪Z) is also a set and hence S_{Z} = {Q ∈ G | Q ⊆ c(∪Z)} is a set. Hence, by Union-Replacement R = ⋃_{Z∈T} (S_{z} × {Z}) is a set. ■

Now let X ∈ P ow(G) and Q ∈ C.

Claim 2: Z ⊆ X ∧ QRZ → Q ⊆ ⋁ X.

Proof: Let Z ⊆ X ∧ QRZ. Then Q ⊆ c(∪Z) ⊆ c(∪X) and hence

Q ⊆ ⋁ X.
■

Claim 3: Q ⊆ ⋁ X → ∃Z[Z ⊆ X ∧ QRZ].

Proof: Let Q ⊆ ⋁ X. Then by (∗) there is Y ∈ B such that

Y ⊆ ∪X ∧ Q ⊆ c(Y).

As Y ⊆ ∪X

∀y∈Y ∃Q′∈X y ∈ Q′.

As A′ is regular, Y ∈ A′ and X ⊆ A′ there is Z ∈ A′ such that

𝔹(y∈Y, Q′∈Z)[ y ∈ Q′ ∧ Q′ ∈ X ].

So Y ⊆ ∪Z and Z ⊆ X so that Q ⊆ c(∪Z) and Z ⊆ X ⊆ G and hence also QRZ. ■

It follows from these claims that (G, R) is a set presentation of C.

Now let (G, R) be a set presentation of a ⋁-semilattice S. We show that S is isomorphic to a set presentable ⋁-semilattice obtained from an inductive definition as above. Let Φ be the converse relation to R; i.e. it is the set of all pairs (X, a) such that aRX. Then Φ is an inductive definition that is a subset of P ow(G) × G. Observe that there is a one-one correspondence between the class C of subsets X of G that are Φ-closed and the elements of S given by the function C → S mapping X ↦ ⋁ X and its inverse function S → C mapping a ↦ G_{a} = {x ∈ G | x ≤ a}. This is easily seen to be an isomorphism of the po-classes. ■

6.4 ⋁-congruences on a ⋁-semilattice

Let S be a ⋁-semilattice . We define an equivalence relation ≈ on S to be a ⋁-congruence on S if, for each set I, if x_{i}, y_{i} ∈ S such that x_{i} ≈ y_{i} for all i ∈ I then

⋁_{i∈I} x_{i} ≈ ⋁_{i∈I} y_{i}.

A preorder ⪯ on S is a ⋁-congruence pre-order on S if for each subset X of S and each a ∈ S

⋁ X ⪯ a ↔ ∀x∈X [x ⪯ a].

Proposition: 6.6 There is a one-one correspondence between ⋁-congruences and ⋁-congruence pre-orders on S. To each ⋁-congruence ≈ there corresponds the ⋁-congruence pre-order ⪯ where

x ⪯ y ↔ ⋁{x, y} ≈ y.

Conversely to each ⋁-congruence pre-order ⪯ corresponds the ⋁-congruence ≈ where

x ≈ y ↔ [x ⪯ y ∧ y ⪯ x].

These correspondences are inverses of each other.

Proposition: 6.7 If c : S → S is a closure operation on S and we define ≈ by

x ≈ y ↔ c(x) = c(y)

for all x, y ∈ S then ≈ is a ⋁-congruence on S.

Proof: The relation ≈ is obviously an equivalence relation on S. Now suppose that x_{i} ≈ y_{i} for all i ∈ I, where I is a set. So c(x_{i}) = c(y_{i}) for all i ∈ I. Let x = ⋁_{i∈I} x_{i} and y = ⋁_{i∈I} y_{i}. Note that, as y_{i} ≤ c(y_{i}) = c(x_{i}) for all i ∈ I,

y = ⋁_{i∈I} y_{i} ≤ ⋁_{i∈I} c(y_{i}) = ⋁_{i∈I} c(x_{i}).

As x_{i} ≤ x for each i ∈ I and c is monotone, y ≤ ⋁_{i∈I} c(x_{i}) ≤ c(x) and hence c(y) ≤ c(x). Similarily c(x) ≤ c(y) so that c(x) = c(y). Thus we have shown that ≈ is a ⋁-congruence on S. ■ Proposition: 6.8 Let ⪯ be a ⋁-congruence preorder on S = P ow(A), where A is a set. Then the associated ⋁-congruence ≈ comes from a closure operation c, as in the previous theorem, provided that for every X ∈ S the class {a ∈ A | {a} ⪯ X} is a set. Then we can define c(X) to be that set.

7 Regarding the Subset Collection Scheme

In this section we study some of the consequences of the Subset Collection Scheme as well as equivalent axioms. The Subset Collection schema easily qualifies as the most intricate axiom of CZF. To explain this axiom in different terms, we introduce the notion of fullness (cf. [Acz78]).

Definition: 7.1 For sets A, B let ^{A}B be the class of all functions with domain A and with range contained in B. Let mv(^{A}B) be the class of all sets R ⊆ A × B satisfying ∀u∈A ∃v∈B ⟨u, v⟩∈R. A set C is said to be full in mv(^{A}B) if C ⊆ mv(^{A}B) and

∀R∈mv(^{A}B) ∃S∈C S ⊆ R.

The expression mv(^{A}B) should be read as the collection of multi-valued functions from the set A to the set B.

Additional axioms we shall consider are:

Exponentiation: ∀x∀y∃z z = ^{x}y.

Fullness: ∀x∀y∃z “ z full in mv(^{x}y)”.

Proposition: 7.2 (i) CZF_{0} + Strong Collection ⊢ Subset Collection ↔ Fullness.

(ii) CZF_{0} + Subset Collection ⊢ Exponentiation.

Proof: (i): For “→” let ϕ(x, y, u) be the formula y∈u ∧ ∃z∈B (y = ⟨x, z⟩). Using the relevant instance of Subset Collection and noticing that for all R ∈ mv(^{A}B) we have ∀x∈A ∃y∈A × B ϕ(x, y, R), there exists a set C such that ∀R∈mv(^{A}B) ∃S∈C S ⊆ R.

“←”: Let C be full in mv(^{A}B). Assume ∀x∈A∃y∈Bϕ(x, y, u). Define ψ(x, w, u) := ∃y ∈ B [w = ⟨x, y⟩ ∧ ϕ(x, y, u)]. Then ∀x ∈ A∃wψ(x, w, u). Thus, by Strong Collection, there exists v ⊆ A × B such that

∀x∈A ∃y∈B [⟨x, y⟩∈v ∧ ϕ(x, y, u)] ∧ ∀x∈A ∀y∈B [⟨x, y⟩∈v → ϕ(x, y, u)].

As C is full, we find w∈C with w ⊆ v. Consequently, ∀x∈A∃y∈ran(w)ϕ(x, y, u) and ∀y∈ran(w)∃x∈A ϕ(x, y, u), where ran(w) := {v : ∃z ⟨z, v⟩∈w}.

Whence D := {ran(w) : w∈C} witnesses the truth of the instance of Subset Collection pertaining to ϕ.

(ii) Let C be full in mv(^{A}B). If now f∈^{A}B, then ∃R∈C R ⊆ f. But then R = f. Therefore ^{A}B = {f∈C : f is a function}. ■

As the next result will show, Fullness does not entail that, given sets A and B, mv(^{A}B) is always a set.

Proposition: 7.3 (i) CZF_{0} ⊢ ∀A∀B (mv(^{A}B) is a set) ↔ Powerset.

(ii) CZF does not prove ∀A∀B (mv(^{A}B) is set).

Proof: (i): We argue in CZF_{0}. It is obvious that Powerset implies that mv(^{A}B) is a set for all sets A, B. Henceforth assume the latter. Let C be an arbitrary set and D = mv(^{C}{0, 1}). By our assumption D is a set. To every subset X of C we assign the set X^{∗} := {⟨u, 0⟩| u∈X} ∪ {⟨z, 1⟩| z∈C}. As a result, X^{∗} ∈ D. For every S∈D let pr(S) be the set {u∈C| ⟨u, 0⟩ ∈ S}. We then have X = pr(X^{∗}) for every X ⊆ C, and thus

P ow(C) = {pr(S)| S∈D}.

Since {pr(S)| S∈D} is a set by Replacement, P ow(S) is a set as well.

(ii): The strength of CZF + Powerset exceeds that of second order arithmetic whereas CZF has only the strength of a small fragment of second order arithmetic. ■

Remark 7.4 On page 623 of[TvD88], a different rendering of Fullness is introduced:

Fullness^{tvd} ∀A∀B∃C ∀r∈mv(^{A}B) ran(r)∈C.

Proposition 8.9, page 623 of [TvD88] claims that Subset Collection implies Fullness^{tvd} on the basis of CZF. That this is not correct can be seen as follows. Let A, B be arbitrary sets. For R ∈∈ mv(^{A}B) let R^{d} be the set {⟨u, ⟨u, v⟩⟩| ⟨u, v⟩ ∈ R}. Then R^{d} ∈ mv(^{A}(A × B)) and ran(R^{d}) = R. By Fullness^{tvd} there exists a set C such that ran(S) ∈ C for all S ∈ mv(^{A}(A × B)). Consequently mv(^{A}B) ⊆ C and thus mv(^{A}B) is a set by Δ_{0} Separation. The latter collides with Proposition 7.3 (ii).

Let EM be the principle of excluded third, i.e. the schema consisting of all formulae of the form ϕ ∨ ¬ϕ. The first central fact to be noted about CZF is:

Proposition: 7.5 CZF + EM = ZF.

Proof: Note that classically Collection implies Separation. Powerset follows classically from Exponentiation. ■

8 Choice Principles

The axiom of choice does not have an unambiguous status in constructive mathematics. On the one hand it is said to be an immediate consequence of the constructive interpretation of the quantifiers. Any proof of ∀x∈a ∃y∈ b ϕ(x, y) must yield a function f : a → b such that ∀x∈a ∃y∈b ϕ(x, f(x)). This is certainly the case in Martin-Löf’s intuitionistic theory of types. On the other hand, from the very earliest days, the axiom of choice has been criticised as an excessively non-constructive principle even for classical set theory. Moreover, it has been observed that the full axiom of choice cannot be added to systems of constructive set theory without yielding constructively unacceptable cases of excluded middle (see [Dia] and Proposition 8.2). Therefore one is naturally led to the question: Which choice principles are acceptable in constructive set theory? As constructive set theory has a canonical interpretation in Martin-Löf’s intuitionistic theory of types this interpretation lends itself to being a criterion for constructiveness. We will consider settheoretic choice principles as constructively justified if they can be shown to hold in the interpretation in type theory. Moreover, looking at constructive set theory from a type-theoretic point of view has turned out to be valuable heuristic tool for finding new constructive choice principles.

In this section we will study differing choice principles and their deductive relationships. To set the stage we present Diaconescu’s result that the full axiom of choice implies certain forms of excluded middle.

8.1 Diaconescu’s result

Restricted Excluded Middle, REM, is the schema ϕ ∨ ¬ϕ where ϕ is a restricted formula.

Recall that P ow(x) := {u : u ⊆ x}, and Powerset is the axiom ∀x∃y y = P ow(x).

Proposition: 8.1 (i) CZF_{0} + Exponentiation + REM ⊢ Powerset.

(ii) The strength of CZF_{0}+Exponentiation+REM exceeds that of classical type theory with extensionality.

Proof: (i): Set 0 := ∅, 1 := {0}, and 2 := {0, {0}}.

Suppose u ⊆ 1. On account of REM we have 0 ∈ u ∨ 0∉u. Thus u = 1 ∨ u = 0; and hence u ∈ 2. This shows that P ow(1) ⊆ 2. As a result, P ow(1) = {u∈2 : u ⊆ 1}, and thus P ow(1) is a set by Restricted Separation.

Now let x be an arbitrary set, and put b := x(P ow(1)). Exponentiation ensures that b is a set. For v ⊆ x define f_{v} ∈ b by

f_{v}(z) := {y∈1 : z∈v},

and put

c := {{z∈x : g(z) = 1} : g∈b}.

c is a set by Strong Collection. Observe that ∀w∈c (w ⊆ x). For v ⊆ x it holds v = {z∈x : f_{v}(z) = 1}, and therefore v∈c. Consequently, P ow(x) = {v∈c : v ⊆ x} is a set.

(ii): By means of ω many iterations of Powerset (starting with ω) we can build a model of intuitionistic type theory within CZF_{0} + Exponentiation + REM. The Gödel-Gentzen negative translation can be extended so as to provide an interpretation of classical type theory with extensionality in intuitionistic type theory (cf. [Myh74]).

In particular, CZF_{0} + Exponentiation + REM is stronger than classical second order arithmetic (with full Comprehension). ■

The Axiom of Choice, AC, asserts that for all sets A and functions F with domain A such that ∀i∈A ∃y∈F (i) there exists a function f with domain A such that ∀i∈A f(i)∈F (i).

Proposition: 8.2 Let CZF_{1} be CZF_{0} + Exponentiation.

(i) CZF_{1} + full Separation + AC = ZFC.

(ii) CZF_{0} + AC ⊢ REM.

(iii) CZF_{1} + AC ⊢ Powerset.

(iv) The strength of CZF_{1} + AC exceeds that of classical type theory with extensionality.

Proof: (i): Let ϕ be an arbitrary formula. Put

X = {n∈ω : n = 0 ∨ [n = 1 ∧ ϕ]},
Y = {n∈ω : n = 1 ∨ [n = 0 ∧ ϕ]}.

X and Y are sets by full Separation. We have

∀z ∈ {X, Y } ∃k∈ω (k∈z).

Using AC, there is a choice function f defined on {X, Y } such that

∀z ∈ {X, Y } [f(z)∈ω ∧ f(z)∈z],

in particular, f(X) ∈ X and f(Y) ∈ Y. Next, we are going to exploit the important fact

∀n, m∈ω (n = m ∨ n ≠ m).  (1)

As ∀z ∈ {X, Y } [f(z)∈ω], we obtain

f(X) = f(Y) ∨ f(X) ≠ f(Y)

by (1). If f(X) = f(Y), then ϕ by definition of X and Y. So assume f(X) ≠ f(Y). As ϕ implies X = Y (this requires Extensionality) and thus f(X) = f(Y), we must have ¬ϕ. Consequently, ϕ ∨ ¬ϕ. Thus (i) follows from the fact that CZF_{1} + EM = ZF.

(ii): If ϕ is restricted, then X and Y are sets by Restricted Separation. The rest of the proof of (i) then goes through unchanged.

(iii) follows from (ii) and Proposition 8.1,(i).

(iv) follows from (ii) and Proposition 8.1,(ii). ■

8.2 Constructive Choice Principles

The weakest constructive choice principle we consider is the Axiom of Countable Choice, AC_{ω}, i.e. whenever F is a function with with domain ω such that ∀i∈ω ∃y∈F (i), then there exists a function f with domain ω such that ∀i∈ω f(i)∈F (i).

A mathematically very useful axiom to have in set theory is the Dependent Choices Axiom, DC, i.e., for all formulae ψ, whenever

(∀x∈a) (∃y∈a) ψ(x, y)

and b_{0}∈a, then there exists a function f : ω → a such that f(0) = b_{0} and

(∀n∈ω) ψ(f(n), f(n + 1)).

The restriction of DC to Δ_{0} formulas will be denoted by Δ_{0}-DC.

Even more useful in constructive set theory is the Relativized Dependent Choices Axiom, RDC.^{5} It asserts that for arbitrary formulae ϕ and ψ, whenever

5In Aczel [Acz82], RDC is called the dependent choices axiom and DC is dubbed the axiom of limited dependent choices. We deviate from the notation in [Acz82] as it deviates from the usage in classical set theory texts.

∀x[ϕ(x) → ∃y(ϕ(y) ∧ ψ(x, y))]

and ϕ(b_{0}), then there exists a function f with domain ω such that f(0) = b_{0} and

(∀n∈ω)[ϕ(f(n)) ∧ ψ(f(n), f(n + 1))].

A restricted form of RDC is Δ_{0}-RDC: For all Δ_{0}-formulae θ and ψ, whenever

(∀x∈a)[θ(x) → (∃y∈a)(θ(y) ∧ ψ(x, y)]

and b_{0}∈a ∧ ϕ(b_{0}), then there exists a function f : ω → a such that f(0) = b_{0} and

(∀n∈ω)[θ(f(n)) ∧ ψ(f(n), f(n + 1))].

Letting ϕ(x) stand for x∈a ∧ θ(x), one sees that Δ_{0}-RDC is a consequence of RDC.

Proposition: 8.3 (i) CZF_{0} + Δ_{0}-DC ⊢ AC_{ω}.

(ii) CZF_{0} ⊢ Δ_{0}-DC ↔ Δ_{0}-RDC.

(iii) CZF_{0} ⊢ RDC → DC.

Proof: (i): If z is an ordered pair ⟨x, y⟩ let 1^{st}(z) denote x and 2^{nd}(z) denote y.

Suppose F is a function with domain ω such that ∀i∈ω ∃x∈F (i). Let A = {⟨i, u⟩| i∈ω ∧ u∈F (i)}. A is a set by Union, Cartesian Product and restricted Separation. We then have

∀x∈A ∃y∈A 1^{st}(y) = 1^{st}(x) + 1.

Pick x_{0} ∈F (0) and let a_{0} = ⟨0, x_{0}⟩. Using Δ_{0}-DC there exists a function g : ω → A satisfying g(0) = a_{0} and

∀i∈ω [g(i)∈A ∧ 1^{st}(g(i + 1)) = 1^{st}(g(i)) + 1].

Letting f be defined on ω by f(i) = 2^{nd}(g(i)) one gets ∀i∈ω f(i)∈F (i). (ii) We argue in CZF_{0} + Δ_{0}-DC to show Δ_{0}-RDC. Assume

∀x∈a[ϕ(x) → ∃y∈a(ϕ(y) ∧ ψ(x, y))]

and ϕ(b_{0}), where ϕ and ψ are Δ_{0}. Let θ(x, y) be the formula ϕ(x) ∧ ϕ(y) ∧ ψ(x, y) and A = {x∈a| ϕ(x)}. Then θ is Δ_{0} and A is a set by Δ_{0} Separation. From the assumtions we get ∀x ∈ A ∃y ∈ A θ(x, y) and b_{0} ∈ A. Thus, by DC, there is a function f with domain ω such that f(0) = b_{0} and ∀n ∈ ω θ(f(n), f(n + 1)). Hence we get ∀n ∈ ω [ϕ(n) ∧ ψ(f(n), f(n + 1))].

The other direction is obvious.

(iii) follows by specializing the formula ϕ(x) to x ∈ a in the schema RDC. ■

The relationship between Δ_{0}-RDC and DC is dealt with in the next lemma.

Lemma: 8.4 (CZF_{0} + Strong Collection) Δ_{0}-RDC implies DC.

Proof: Assume (∀x∈a) (∃y∈a) ψ(x, y) and b_{0}∈a. Then

(∀x∈a) (∃z) [(∃y∈a) (z = ⟨x, y⟩ ∧ ψ(x, y))].

Using strong collection there exists a set S such that (∀x∈a) (∃z∈S) (∃y∈a) [z = ⟨x, y⟩ ∧ ψ(x, y)] and

(∀z∈S) (∃x′∈a) (∃y′∈a) (z = ⟨x′, y′⟩ ∧ ψ(x′, y′)).  (2)

In particular we have (∀x∈a) (∃y∈a) ⟨x, y⟩ ∈ S. Employing Δ_{0}-RDC (with ϕ(x) and ψ(x, y) being x∈a and ⟨x, y⟩ ∈ S, respectively) there exists a function f : ω → a such that f(0) = b_{0} and (∀n∈ω) ⟨f(n), f(n + 1)⟩ ∈ S. By (2) we get (∀n∈ω) ψ(f(n), f(n + 1)). ■

Proposition: 8.5 (CZF_{0} + RDC + Collection)

Suppose ∀x∃yϕ(x, y). Then for every set a there exists a transitive set A such that a∈A and

∀x∈A ∃y∈A ϕ(x, y).

Moreover, for every set d there exists a function f : ω → A such that f(0) = d and ∀n∈ω ϕ(f(n), f(n + 1).

Proof: The assumption yields that ∀x∈b ∃yϕ(x, y) holds for every set b. Thus, by Collection and the existence of the transitive closure of a set, we get

∀b ∃c [θ(b, c) ∧ T ran(c)],

where θ(b, c) is the formula ∀x∈b ∃y∈c ϕ(x, y). Employing RDC there exists a function g with domain ω such that g(0) = {d} and ∀n∈ω θ(g(n), g(n+1)). Obviously A = ⋃_{n∈ω} g(n) satisfies our requirements.

The existence of the function f follows from the latter since RDC entails DC. ■

8.3 The Presentation Axiom

The Presentation Axiom is an example of a principle inspired by the interpretation in type theory.

A set B is a base if every relation R with domain B extends a function with domain B.

The Presentation Axiom, PA, is the statement that every set has a presentation, where a presentation of a set A is a function with range A whose domain is a base.

Using the above terminolgy, AC_{ω} expresses that ω is a base whereas AC amounts to saying that every set is a base.

Proposition: 8.6 CZF_{0} + Strong Collection + PA ⊢ DC

Proof: Assume (∀x∈A) (∃y∈A) ψ(x, y) and b_{0}∈A. By PA there exists a base B and a function h : B → A such that A is the range of h. As a result,

∀u∈B ∃v∈B ψ(h(u), h(v)).

Using Strong Collection there exists a relation R ⊆ B × B with domain B such that

∀u∈B ∃v∈B [⟨u, v⟩∈R ∧ ψ(h(u), h(v))]

and

∀u∈B ∀v∈B[⟨u, v⟩∈R → ψ(h(u), h(u))].

Since B is a base there exists a function g : B → A such that g ⊆ R. Pick u_{0} ∈B such that h(u_{0}) = b_{0}. Now define f′ : ω → B by f′(0) = u_{0} and f′(n + 1) = g(f′(n)). By induction on ω one easily verifies

∀n∈ω ψ(h(f′(n)), h(f′(n + 1))).

Thus, letting f(n) = h(f′(n)) one obtains a function f : ω → A satisfying f(0) = b_{0} and ∀n∈ωψ(f(n), f(n + 1)). ■

Proposition: 8.7 CZF_{0} + Exponentiation + PA ⊢ Fullness.

Proof: Let A, B be sets. By Exponentiation, ^{A}B is a set as well. On account of PA, ^{A}B is full in mv(A, B). ■ Corollary: 8.8 CZF_{0} + Exponentiation + PA + Strong Collection proves Subset Collection.

Proof: This follows from the previous Proposition and Proposition 7.2. ■

9 Principles that ought to be avoided in CZF

In the previous section we saw that the unrestricted Axiom of Choice implies undesirable form of excluded middle. There are several other well known principles provable in classical set theory which also imply versions of excluded middle. Among them are the Foundation Axiom and Linearity of Ordinals.

Foundation Schema: ∃xϕ(x) → ∃x[ϕ(x) ∧ ∀y∈x¬ϕ(y)] for all formulae ϕ.

Foundation Axiom: ∀x [∃y(y∈x) → ∃y(y∈x ∧ ∀z∈y z∉x)].

Linearity of Ordinals We shall conceive of ordinals as transitive sets whose elements are transitive too.

Let Linearity of Ordinals be the statement formalizing that for any two ordinals α and β the following trichotomy holds: α∈β ∨ α = β ∨ β∈α.

Proposition: 9.1 (i) CZF + Foundation Schema = ZF.

(ii) CZF + Separation + Foundation Axiom = ZF.

(iii) CZF + Foundation Axiom ⊢ REM.

(iv) CZF + Foundation Axiom ⊢ Powerset.

(v) The strength of CZF+Foundation Axiom exceeds that of classical type theory with extensionality.

Proof: (i): For an arbitrary formula ϕ, consider

S_{ϕ} := {x∈ω : x = 1 ∨ [x = 0 ∧ ϕ]}.

We have 1∈S_{ϕ}. By the Foundation Schema, there exists x_{0}∈S_{ϕ} such that ∀y∈x_{0} y∉S_{ϕ}. By definition of S_{ϕ}, we then have

x_{0} = 1 ∨ [x_{0} = 0 ∧ ϕ].

If x_{0} = 1, then 0∉S_{ϕ}, and hence ¬ϕ. Otherwise we have x_{0} = 0 ∧ ϕ; thus ϕ. So we have shown EM, from which (i) ensues. (ii): With full Separation S_{ϕ} is a set, and therefore the Foundation Axiom

suffices for the previous proof.

(iii): For restricted ϕ, S_{ϕ} is a set be Restricted Separation, and thus ϕ ∨ ¬ϕ follows as in the proof of (i).

(iv) follows from (iii) and Proposition 8.1,(i).

(v) follows from (iii) and Proposition 8.1,(ii). ■

Proposition: 9.2 (i) CZF + “Linearity of Ordinals” ⊢ Powerset.

(ii) CZF + “Linearity of Ordinals” ⊢ REM.

(iii) CZF + “Linearity of Ordinals” + Separation = ZF.

Proof: (i): Note that 1 is an ordinal. If u ⊆ 1, then u is also an ordinal because of ∀z∈u z = 0. Furthermore, one readily shows that 2 is an ordinal. Thus, by Linearity of Ordinals,

∀u ⊆ 1 [u∈2 ∨ u = 2 ∨ 1∈u].

The latter, however, condenses to ∀u ⊆ 1 [u∈2]. As a consequence we have,

P ow(1) = {u∈2 : u ⊆ 1},

and thus P ow(1) is a set. Whence, proceeding onwards as in the proof of Proposition 8.1,(i), we get Powerset.

(ii): Let ϕ be restricted. Put

α := {n∈ω : n = 0 ∧ ϕ}.

α is a set by Restricted Separation, and α is an ordinal as α ⊆ 1. Now, by Linearity of Ordinals, we get

α∈1 ∨ α = 1.

In the first case, we obtain α = 0, which implies ¬ϕ by definition of α. If α = 1, then ϕ. Therefore, ϕ ∨ ¬ϕ.

(iii): Here α := {n∈ω : n = 0 ∧ ϕ} is a set by Separation. Thus the remainder of the proof of (ii) provides ϕ ∨ ¬ϕ. ■

10 Large sets in constructive set theory

The first large set axioms proposed in the context of constructive set theory was the Regular Extension Axiom, REA, which Aczel introduced to accommodate inductive definitions in CZF (cf. [Acz78], [Acz86]).

Definition: 10.1 A set C is said to be regular if it is transitive, inhabited (i.e. ∃u u ∈ C) and for any u∈C and R ∈ mv(^{u}C) there exists a set v ∈ C such that

∀x∈u ∃y∈v ⟨x, y⟩∈R ∧ ∀y∈v ∃x∈u ⟨x, y⟩∈R.

We write Reg(C) to express that C is regular.

REA is the principle

∀x ∃y (x∈y ∧ Reg(y)).

Definition: 10.2 There are interesting weakend notions of regularity.

A transitive inhabited set C is weakly regular if for any u∈C and R ∈ mv(^{u}C) there exists a set v ∈ C such that

∀x∈u ∃y∈v ⟨x, y⟩∈R.

We write wReg(C) to express that C is regular. The weakly Regular Extension Axiom (wREA) is as follows.

Every set is a subset of a weakly regular set.

A transitive inhabited set C is functionally regular if for any u∈C and function f : u → C, ran(f) ∈ C. We write fReg(C) to express that C is functionally regular. The weakly Regular Extension Axiom (wREA) is as follows.

Every set is a subset of a functionally regular set.

Lemma: 10.3 (CZF_{0}) If A is regular then A is weakly regular and functionally regular.

Proof: Obvious. ■

Lemma: 10.4 (CZF_{0}) If A is functionally regular and 2 ∈ A, then A is closed under Pairing, that is ∀x, y ∈ A {x, y} ∈ A.

Proof: Given x, y ∈ A define a function g : 2 → A by g(0) = x and g(1) = y. Then {x, y} = ran(g) ∈ A. ■ Proposition: 10.5 CZF_{0} + REA ⊢ Fullness

Proof: Let A, B be sets. Using REA iteratively there exists a regular set Z such that 2, A, B, A × (A × B) ∈ Z. Let C = {S∈Z| S ∈ mv(^{A}B)}. S is a set by Δ_{0} Separation. We claim that C is full in mv(^{A}B). To see this let R ∈ mv(^{A}B). Let

R^{∗} = {⟨x, ⟨x, y⟩⟩| x∈A ∧ ⟨x, y⟩ ∈ R}.

2 ∈ Z guarantees that Z is a model of Pairing and thus R^{∗} ∈ mv(^{A}Z). Employing the regularity of Z there exists S^{∗}∈Z such that

∀x∈A ∃z∈S^{∗} (⟨x, z⟩∈R^{∗}) ∧ ∀z∈S^{∗} ∃x∈A (⟨x, z⟩∈S^{∗}).

As a result, S^{∗} ⊆ R and S^{∗} ∈ mv(^{A}B). Moreover, S^{∗} ∈ C. ■

Corollary: 10.6 CZF_{0} + Strong Collection + REA ⊢ Subset Collection

Proof: By Proposition 10.5 and Proposition 7.2. ■

Lemma: 10.7 (CZF_{0} + Strong Collection) Assume that A is a regular set, b∈A and ∀x∈b ∃y∈A ϕ(x, y). Then there exists a set c∈A such that

∀x∈b ∃y∈c ϕ(x, y) ∧ ∀y∈c ∃x∈b ϕ(x, y).

Proof: ∀x∈b ∃y∈A ϕ(x, y) implies ∀x∈b ∃z ψ(x, z), with ψ(x, z) being the formula ∃y∈A ϕ(x, y) ∧ z = ⟨x, y⟩. Using Strong Collection there exists a set R such that

∀x∈b ∃z∈R ψ(x, z) ∧ ∀z∈R ∃x∈b ψ(x, z).

Thus R ∈ mv(^{b}A). Owing to the regularity of A there exists a set c∈A such that

∀x∈b ∃y∈c ⟨x, y⟩∈R ∧ ∀y∈c ∃x∈b ⟨x, y⟩∈R.

As a consequence we get ∀x∈b ∃y∈c ϕ(x, y) ∧ ∀y∈c ∃x∈b ϕ(x, y). ■

10.1 Some metamathematical results about REA

Lemma: 10.8 On the basis of ZFC, a set B is regular if and only if B is functionally regular.

Proof: Obvious. ■

Proposition: 10.9 ZFC ⊢ REA.

Proof: The axiom of choice implies that arbitrarily large regular cardinals exists and that for each regular cardinal κ, H(κ) is a regular set. Given any set b let μ be the cardinality of b. Then the next cardinal after μ, μ^{+}, is regular and b ∈ H(μ^{+}). ■

Proposition: 10.10 (i) CZF + AC_{ω} does not prove that H(ω ∪ {ω}) is a set.

(ii) CZF does not prove REA.

Proof: It has been shown by Rathjen (cf. [RG94]) that CZF+AC_{ω} has the same proof-theoretic strength as Kripke-Platek set theory, KP. The prooftheoretic ordinal of CZF + AC_{ω} is the so-called Bachmann-Howard ordinal ψ_{Ω_{1}}ε_{Ω_{1}+1}. Let

T := CZF + AC_{ω} + H(ω ∪ {ω}) is a set.

Another theory which has proof-theoretic ordinal ψ_{Ω_{1}}ε_{Ω_{1}+1} is the intuitionistic theory of arithmetic inductive definitions ID_{1}^{i}. We aim at showing that T proves the consistency of ID_{1}^{i}. The latter implies that T proves the consistency of CZF + AC_{ω} as well, yielding (i), owing to Gödel’s Incompleteness Theorem.

Let L_{HA}(P) be the language of Heyting arithmetic augmented by a new unary predicate symbol P. The language of ID_{1}^{i} comprises L_{HA} and in addition contains a unary predicate symbol I_{ϕ} for each formula ϕ(u, P) of L_{HA}(P) in which P occurs only positively. The axioms of ID_{1}^{i} comprise those of Heyting arithmetic with the induction scheme for natural numbers extended to the language of ID_{1}^{i} plus the following axiom schemes relating to the predicates I_{ϕ}:

(ID_{ϕ}^{1}) ∀x [ϕ(x, I_{ϕ}) → I_{ϕ}(x)]
(ID_{ϕ}^{2}) ∀x [ϕ(x, ψ) → ψ(x)] → ∀x [I_{ϕ}(x) → ψ(x)]

for every formula ψ, where ϕ(x, ψ) arises from ϕ(x, P) by replacing every occurrence of a formula P (t) in ϕ(x, P) by ψ(t).

Arguing in T we want to show that ID_{1}^{i} has a model. The domain of the model will be ω. The interpretation of ID_{1}^{i} in T is given as follows. The quantifiers of ID_{1}^{i} are interpreted as ranging over ω. The arithmetic constant 0 and the functions +1, +, · are interpreted by their counterparts on ω. It remains to provide an interpretation for the predicates I_{ϕ}, where ϕ(u, P) is a P positive formula of L_{HA}(P). Let ϕ(u, v)^{∗} be the set-theoretic formula which arises from ϕ(u, P) by, firstly, restricting all quantifiers to ω, secondly, replacing all subformulas of the form P (t) by t∈v, and thirdly, replacing the arithmetic constant and function symbols by their set-theoretic counterparts. Let

Γ_{ϕ}(A) = {x∈ω| ϕ(x, A)^{∗}}

for every subset A of ω, and define a mapping x ↦ Γ_{ϕ}^{x} by recursion on H(ω ∪ {ω}) via

Γ_{ϕ}^{x} = Γ_{ϕ}(⋃_{u∈x} Γ_{Φ}^{u}).

Finally put

I_{ϕ}^{∗} = ⋃_{x∈H(ω∪{ω})} Γ_{ϕ}^{x}.

It is obvious that the above interpretation validates the arithmetic axioms of ID_{1}^{i}. The validity of the interpretation of (ID_{ϕ}^{1}) follows from

Γ_{ϕ}(I_{ϕ}^{∗}) ⊆ I_{ϕ}^{∗}.  (3)

Let HC = H(ω ∪ {ω}). Before we prove (3) we show

Γ_{ϕ}^{∈a} ⊆ Γ_{ϕ}^{a}  (4)

for a ∈ HC, where Γ_{ϕ}^{∈a} = ⋃_{x∈a} Γ_{ϕ}^{x}. (4) is shown by Set Induction on a. The induction hypothesis then yields, for x∈a,

Γ_{ϕ}^{∈x} ⊆ Γ_{ϕ}^{x} ⊆ Γ_{ϕ}^{∈a}.

Thus, by monotonicity of the operator Γ_{ϕ},

Γ_{ϕ}(Γ_{ϕ}^{∈x}) = Γ_{ϕ}^{x} ⊆ Γ_{ϕ}(Γ_{ϕ}^{∈a}) = Γ_{ϕ}^{a},

and hence Γ_{ϕ}^{∈a} ⊆ Γ_{ϕ}^{a}, confirming (4).

To prove (3) assume n ∈ Γ_{ϕ}(I_{ϕ}^{∗}). Then ϕ(n, ⋃_{x∈HC} Γ_{ϕ}^{x})^{∗} by definition of Γ_{Φ}. Now, since ⋃_{x∈HC} Γ_{ϕ}^{x} occurs positively in the latter formula one can show, by induction on the built up of ϕ, that

ϕ(n, Γ_{ϕ}^{a})^{∗}  (5)

for some a ∈ HC. The atomic cases are obvious. The crucial case is when ϕ(n, v)^{∗} is of the form ∀k ∈ ωψ(k, n, v). Inductively one then has

∀k ∈ ω ∃y ∈ HC ψ(k, n, Γ_{ϕ}^{y}).

Employing Strong Collection, there exists R ∈ mv(^{ω}HC) such that

∀k ∈ ω ∃y [⟨k, y⟩ ∈ R ∧ ψ(k, n, Γ_{ϕ}^{y}).

Using AC_{ω} there exists a function f : ω → HC such that ∀k ∈ ω ⟨k, f(k)⟩ ∈ R and hence

∀k ∈ ω ψ(k, n, Γ_{ϕ}^{f(k)}).

Let b = ran(f). It follows from (4) that Γ_{ϕ}^{f(k)}) ⊆ Γ_{ϕ}^{b}, and thus, by positivity of the occurrence of P in ϕ we get,

∀k ∈ ω ψ(k, n, Γ_{ϕ}^{b}))^{∗}.

The validity of the interpretation of (ID_{ϕ}^{2}) can be seen as follows. Assume

∀i∈ω [ϕ(i, X) → i∈X],  (6)

where X is a definable class. We want to show I_{ϕ}^{∗} ⊆ X. It suffices to show Γ_{ϕ}^{a} ⊆ X for all a ∈ HC. We proceed by induction on a∈HC. The induction hypothesis provides Γ_{ϕ}^{∈a} ⊆ X. Monotonicity of Γ_{ϕ} yields Γ_{ϕ}(Γ_{ϕ}^{∈a}) = Γ_{ϕ}^{a} ⊆ Γ_{ϕ}(X). By (4) it holds Γ_{ϕ}(X) ⊆ X. Hence Γ_{ϕ}^{a} ⊆ X.

We have now shown within T that ID_{1}^{i} has a model. Note also that, arguing in T, this model is a set as the mapping ϕ(u, P) ↦ I_{ϕ}^{∗} is a function when we assume a coding of the syntax of ID_{1}^{i}. As a result, by formalizing the notion of truth for this model, T proves the consistency of ID_{1}^{i}, establishing (i).

(ii) It has been shown by Rathjen (cf. [RG94]) that CZF + REA is of much greater proof-theoretic strength than CZF. However, (ii) also follows from (i) as REA implies that H(ω ∪ {ω}) is a set. ■

ZF proves fREA, though this is not a triviality. Here we shall draw on [Je82], where it was shown that ZF proves that H(ω ∪ {ω}) is a set.

Proposition: 10.11 ZF ⊢ fREA

Proof: Every set x is contained in a transitive set A. Thus if we can show that H(A) is a set we have found a set comprising x which is functionally regular. The main task of the proof is therefore to show that H(A) is a set. Let α = ⋃{rank(u)| u∈A}. Let κ = (α^{+})^{+} (where ρ^{+} denotes the least cardinal bigger than ρ). We shall show that rank(s) < κ for every s ∈ H(A), and thus

H(A) ⊆ V_{κ}.  (7)

For a set X let ⋃^{n} X be the n-fold union of X, i.e., ⋃^{0} X = X, and ⋃^{n+1} X = ⋃(⋃^{n} X). Note that

rank(X) = {rank(u)| u ∈ TC(x)} = ⋃_{n∈ω}{rank(u)| u ∈ ⋃^{n}X}.

Let Θ be the set of all non-empty finite sequences of ordinals < α^{+}. We shall define a function F on H(A) × ω × Θ such that for each s ∈ H(A), if F_{s} denotes the function F_{s}(n, t) = F (s, n, t), then F_{s} maps ω × Θ onto rank(s). Since there is a bijection between Θ and α^{+}, we then have rank(s) < κ, and thus s ∈ V_{κ}. We define the function F by recursion on n. For each n, we denote by F_{s}^{n} the function F_{s}^{n}(t) = F (s, n, t). For n = 0 we let for each s ∈ H(A) and each β < α^{+},

F_{s}^{0}(⟨β⟩) = the βth element of {rank(u)| u∈s}

if the set {rank(u)| u∈s} has order-type > β, and F_{s}^{0}(t) = 0 otherwise. Since there exists b∈A and g : b → H(A) such that s = ran(g), the order type of {rank(x)| x∈s} is an ordinal < α^{+}, and hence F_{s}^{0} maps Θ onto the set {rank(x)| x∈s}.

For n = 1, s ∈ H(A), and β_{0}, β_{1} < α^{+} we let

F_{s}^{1}(⟨β_{0}, β_{1}⟩) = the β_{1}th element of {F_{u}^{0}(⟨β_{0}⟩)| u∈s},

if it exists, and F_{s}^{1}(t) = 0 otherwise. In general, let

F_{s}^{n+1}(⟨β_{0}, …, β_{n+1}⟩) = the β_{n+1}th element of {F_{u}^{n}(⟨β_{0}, …, β_{n}⟩)| u∈s},

if it exists, and F_{s}^{n+1}(t) = 0 otherwise. For each s ∈ H(A) and each ⟨β_{0}, …, β_{n}⟩ ∈ Θ, the order-type of the set is an ordinal < α^{+}. F_{s}^{n+1} maps Θ onto the set

{F_{u}^{n}(⟨β_{0}, …, β_{n}⟩)| x∈s ∧ ⟨β_{0}, …, β_{n}⟩ ∈ α^{+} × ⋯ × α^{+}}.

It follows by induction that for each n and for each s ∈ H(A), the function F_{s}^{n} maps Θ onto the set {rank(u)| u ∈ ⋃^{n} s}. For each s ∈ H(A), F_{s} therefore maps ω × Θ onto the set {rank(u)| u ∈ TC(s)}.

This concludes the proof of (7). Finally, by Separation, it follows that H(A) is a set. ■

Proposition: 10.12 Let HC = H(ω ∪ {ω}). If ZF is consistent, then ZF does not prove that HC is weakly regular.

Assume that ZF is consistent. Let T be the theory ZF plus the assertion that the real numbers are a union of countably many countable sets. By results of Feferman and Levy it follows that T is consistent as well (see [FL] or [Je73], Theorem 10.6). In the following we argue in T and identify the set of reals, ℝ, with the set of functions from ω to ω. Working towards a contradiction, assume that HC is weakly regular. Let ℝ = ⋃_{n∈ω} X_{n}, where each X_{n} is countable and infinite. By induction on n∈ω one verifies that n ∈ HC for every n ∈ ω, and thus ω ∈ HC. If f : ω → ω define f^{∗} by f^{∗}(n) = ⟨n, f(n)⟩. Then f^{∗} : ω → HC as HC is closed under Pairing, and hence f = ran(f^{∗}) ∈ HC. As a result, ℝ ⊆ HC and, moreover, X_{n} ∈ HC since each X_{n} is countable. Furthermore, {X_{n}| n∈ω} ∈ HC.

For each X_{n} let

G_{n} = {f : ω → X_{n}| f is 1-1 and onto}.

Note that G_{n} ⊆ HC. Define R ∈ mv(^{{X_{n}| n∈ω}}HC) by

⟨X_{n}, f⟩ ∈ R iff f ∈ G_{n}.

By weak regularity there exists B ∈ HC such that

∀n∈ω ∃f∈B ⟨X_{n}, f⟩ ∈ R.

Now pick g : ω → B such that B = ran(g). For every x ∈ ℝ define J(x) as follows. Select the least n such that x∈X_{n} and then pick the least m such that ⟨X_{n}, g(m)⟩ ∈ R, and let

J(x) = ⟨n, (g(m))^{−1}(x)⟩,

where (g(m))^{−1} denotes the inverse function of g(m). It follows that

J : ℝ → ω × ω

is a 1-1 function, implying the contradiction that ℝ is countable. ■ Definition: 10.13 A class A is said to be ⋃-closed if for all x∈A, ⋃ x ∈ A.

A class A is said to be closed under Exponentiation (Exp-closed) if for all x, y∈A, ^{x}y ∈ A.

Proposition: 10.14 (ZF) If A is a functionally regular ⋃-closed set with 2 ∈ A, then the least ordinal not in A, o(A), is a regular ordinal.

Proof: If f : α → o(A), where α < o(A), then α∈A and thus ran(f) ∈ A, and hence ⋃ ran(f) ∈ A. Since ran(f) is a set of ordinals, ⋃ ran(f) is an ordinal, too. Let β = ⋃ ran(f). Then β∈A. Note that β + 1 ∈ A as well since 2 ∈ A entails that A is closed under Pairing and β + 1 = ⋃{β, {β}}. Since f : α → β + 1 this shows that o(A) is a regular ordinal. ■

Corollary: 10.15 If ZF is consistent, then so is the theory

ZF + HC is not ⋃-closed.

Proof: This follows from Proposition 10.14 and Propostion 10.12. ■

Corollary: 10.16 If ZFC+∀α ∃κ > α (κ is a strongly compact cardinal) is consistent, then so is the theory ZF plus the assertion that there are no ⋃-closed functionally regular sets containing ω.

Proof: By the previous Proposition, the existence of a functionally regular set A with ω∈A would yield the existence of an uncountable regular ordinal. By [Gi], however, all uncountable cardinals can be singular under the assumption that ZFC + ∀α ∃κ > α (κ is a strongly compact cardinal) is a consistent theory. ■

The consistency assumption of the previous Proposition might seem exaggerated. It is, however, known that the consistency of

          ZF + All uncountable cardinals are singular

cannot be proved without assuming the consistency of the existence of some large cardinals. It was shown in [DJ] that if ℵ_{1} and ℵ_{2} are both singular one can obtain an inner model with a measurable cardinal.

One is naturally led to consider strengthenings of the notion of of a regular set, for instance that the set should also be ⋃-closed and Exp-closed. It has been shown that adding these strengthened version of REA to CZF does not yield more proof-theoretic strength than CZF + REA.

Proposition: 10.17 The theories CZF + REA and

CZF + ∀x ∃A [Reg(A) ∧ A ⋃-closed and Exp-closed]

have the same proof-theoretic strength.

Proof: See [R01], Theorem 4.7. ■

The next result shows, however, that these strengthenings of REA are not provable in CZF + REA.

Proposition: 10.18 If ZF is consistent, then CZF + REA does not prove that there exists a regular set containing ω which is Exp-closed and ⋃-closed.

Proof: For a contradiction assume

CZF + REA ⊢ ∃A [Reg(A) ∧ ω∈A ∧ A is Exp-closed and ⋃-closed.

Then ZFC would prove this assertion. In the following we work in ZFC. By Proposition 10.14 κ = o(A) is a regular uncountable cardinal. We claim that κ is a limit cardinal, too. Let ρ < κ and F : ^{ρ}2 → μ be a surjective function. Suppose κ ≤ μ. Then let X = {g ∈^{ρ} 2 → 2| F (g) < κ}. Note that

{F (g)| g∈X} = κ

since F is surjective. Since A is Exp-closed we have ^{(^{ρ}2)}2 ∈ A. Define a function G : ^{ρ}2 → 2 by G(h) = 1 if h∈X, and G(h) = 0 otherwise. Then G ∈ A. Further, define j : G → A by j(⟨h, i⟩) = F (h) if i = 1, and j(⟨h, i⟩) = 0 otherwise. Then ran(j) ∈ A. However, ran(j) = {F (g)| g∈X} ∪ {0} = κ, yielding the contradiction κ∈κ.

As a result, μ < κ and therefore κ cannot be a successor cardinal. Consequently we have shown the existence of a weakly inaccessible cardinal. But that cannot be done in ZFC providing ZF is consistent. ■

10.2 Inaccessibility

The background theory for this section will be CZF_{0}^{S} which is CZF_{0} plus Strong Collection and Subset Collection.

Definition: 10.19 Let INAC be the principle

∀x ∃y (x∈y ∧ Reg(y) and y is a model of CZF_{0}^{S}),

i.e. the structure ⟨y, ∈↾ (y × y)⟩ is a model of CZF_{0}^{S}.

We say that a set is set-inaccessible if it is regular and a model of CZF_{0}^{S} and write INAC(y) for ‘y is set-inaccessible’.

Remark 10.20 As it makes perfect sense to study notions of largeness in set theories without or with restricted Set Induction, we have formalized setinaccessibility by requiring that y is a model of CZF_{0}^{S} rather than CZF. On the other hand, if one assumes Set Induction in the background theory than INAC(y) readily implies that y is a model of Set Induction as well, and hence y ⊧ CZF.

The formalization of the notion of inaccessibility in Definition 10.19 is somewhat akward as it is very syntactic in that it requires a satisfaction predicate for formulae interpreted over a set. An alternative and more ‘algebraic’ characterization will be given in the next section.

Viewed classically inaccessible sets are closely related to inaccessible cardinals. Let V_{α} denote the αth level of the von Neumann hierarchy.

Proposition: 10.21 (ZFC) I is set-inaccessible if and only if I = V_{κ} for some strongly inaccessible cardinal κ.

Proof: This is a consequence of the proof of [RGP], Corollary 2.7. ■

Proposition: 10.22 Let EM denote the principle of excluded middle. The theories CZF^{−} + INAC + EM and

ZFC + ∀α ∃κ (α < κ ∧ κ is a strongly inaccessible cardinal)

have the same proof theoretic strength.

Proof: [CR00], Lemma 2.10. ■

10.3 A nicer rendering of set-inaccessibility

Definition: 10.23 Let Ω := {x : x ⊆ {0}}. Ω is the class of truth values with 0 representing falsity and 1 = {0} representing truth. Classically one has Ω = {0, 1} but intuitionistically one cannot conclude that those are the only truth values.

For a ⊆ Ω define

⋀ a = {x∈1 : (∀u∈a)x∈u}
⋁ a = {x∈1 : (∃u∈a)x∈u} (= ⋃ a).

A class B is ⋀-closed if for all a∈B, whenever a ⊆ Ω, then ⋀ a ∈ B.

Definition: 10.24 For sets a, b let ^{a}b be the class of all functions with domain a and with range contained in b. Let mv(^{a}b) be the class of all sets r ⊆ a × b satisfying ∀u∈a ∃v∈b ⟨u, v⟩∈r. A set c is said to be full in mv(^{a}b) if c ⊆ mv(^{a}b) and

∀r∈mv(^{a}b) ∃s∈c s ⊆ r.

The expression mv(^{a}b) should be read as the collection of multi-valued functions from a to b.

The Fullness axiom is the assertion

∀a∀b ∃c ⊆ mv(^{a}b) [∀r∈mv(^{a}b) ∃s∈c s ⊆ r].

Lemma: 10.25 (CZF_{0}) If I is set-inaccessible, then for all A, B ∈ I there exists C ∈ I such that C is full in mv(^{A}B).

Proof: Let I be a regular model of CZF. We first show:

∀A∈I “I ∩ mv(^{A}I) is full in mv(^{A}I)”;  (8)
∀A, B∈I ∃C∈I I ⊧ “C is full in mv(^{A}B)”.  (9)

To prove (8), let A∈I and R ∈ mv(^{A}I). Then R is a subset of A × I such that for all x∈A there is y∈I such that xRy. Let R′ be the set of all (x, (x, y)) such that xRy. Then R′ ∈ mv(^{A}I) also, as I is closed under Pairing. Hence, as I is regular, there is S∈I such that ∀x∈A ∃z∈S xR′z ∧ ∀z∈S ∃x∈A xR′z. Hence S ∈ (I ∩ mv(^{A}I)) and S is a subset of R. So (8) is proved. (9) is just stating that I ⊧ ”Fullness”, which follows from 7.2 since I is a model of CZF_{0}.

To prove (A), let A, B∈I and choose C∈I as in (9). It follows that C ⊆ mv(^{A}B) and:

∀R′∈I [R′ ∈ mv(^{A}B) → ∃R_{0}∈C (R_{0} ⊆ R′) ].

So to complete the proof of (A) it suffices, given R ∈ mv(^{A}B) to find a subset R′ of R such that R′ ∈ (I ∩ mv(^{A}B)), as then we can get R_{0}∈C, as above, a subset of R′ and hence of R.

But, as B is a subset of I, R ∈ mv(^{A}I) so that, by (8), there is a subset R′ of R such that R′∈(I ∩ mv(^{A}I)). It follows that R′ ∈ (I ∩ mv(^{A}B)) and we are done. ■

Proposition: 10.26 (CZF_{0}^{S}) I is set-inaccessible if and only if the following are satisfied:

1. I is a regular set,

2. ω∈I,

3. (∀a∈I) ⋃ a∈I,

4. I is ⋀-closed,

5. (∀a, b ∈ I)[ {x∈1 : a∈b} ∈ I].

6. (∀a, b ∈ I)(∃c∈I) [c is full in mv(^{a}b)].

Proof: Firstly, suppose that I is set-inaccessible. Then (1)–(5) are obvious.

(6) follows from Lemma 10.25.

Now assume that (1)-(6) hold. The regularity of I implies that I is a model of Strong Collection and (6) implies that I is a model of Subset Collection by Proposition 7.2 providing that I is a model of the remaining axioms of CZF_{0}^{S}. By (2) I is a model of Infinity. By (5) and the transitivity of I we have 2 = {0, 1} ∈ I. If a, b∈I let f : 2 → I be the function defined by f(0) = a and f(1) = b. The range of f is {a, b}. Regularity of I implies that the range of f is in I and thus {a, b} ∈ I. The latter shows that I is a model of Pairing. By (3), I is a model of Union. It remains to verify that I is a model of Restricted Separation. Firstly, we will show that for every restricted formula θ which only contains parameters from I there exists a set c ∈ Ω ∩ I such that

θ ↔ 0∈c.  (10)

The proof of (10) follows the proof of Proposition 3.2. We proceed by induction on the construction of θ. Note that, by Extensionality, c is unique.

If θ is of the form a ∈ b, then the claim follows from (5). Due to Extensionality we can consider = as a defined symbol since a = b ↔ (∀x∈a x ∈ b ∧ ∀x∈b x∈a).

Next we address the propositional connectives. Let c_{1}, c_{2}∈Ω ∩ I such that

ϕ_{i} ↔ 0∈c_{i}.

Then c_{∧} := ⋀{c_{1}, c_{2}} ∈ Ω ∩ I (by (4)) and

[ϕ_{1} ∧ ϕ_{2}] ↔ 0∈c_{∧}.

Similarly c_{∨} = ⋁{c_{1}, c_{2}} ∈ Ω ∩ I (by (3)) and [ϕ_{1} ∨ ϕ_{2}] ↔ 0 ∈ c_{∨}. Let c_{→} := ⋀{c_{2} : x∈c_{1}} ∈ Ω. As c_{→} is the range of the function x ↦ c_{2} with domain c_{1}, regularity of I implies c_{→}∈I. Moreover,

[ϕ_{1} → ϕ_{2}] ↔ 0∈c_{→}.

Set c_{¬} := ⋀{0 : x ∈ c_{1}}. As 0 ∈ Ω ∩ I, the above shows c_{¬} ∈ Ω ∩ I. As 0 = 1 ↔ 0∈0 and ¬ϕ_{1} ↔ [ϕ_{1} → 0 = 1], it follows that ¬ϕ_{1} ↔ 0∈c_{¬}.

Finally, we address the bounded quantifiers. Suppose that a∈I and that for all x ∈ a there exists a c_{x} ∈ Ω ∩ I such that ϕ(x) ↔ x ∈ c_{x}. Let f be the function with domain a such that f(x) = c_{x}. Let b be the range of f. As f : a → I, the regularity of I implies b∈I. By (3) and (4) we get ⋀ b, ⋁ b ∈ Ω ∩ I. Moreover,

(∀x∈a)ϕ(x) ↔ 0∈⋀ b,
(∃x∈a)ϕ(x) ↔ 0∈⋁ b,

concluding the proof of (10).

No let a ∈ I and let ϕ(x) be a restricted formula with all parameters in I. Then for every x∈a there exists exactly one set c_{x}∈I such that c_{x}∈Ω and ϕ(x) ↔ 0∈c_{x}. For each set x∈a let d_{x} be the function with domain c_{x} such that d_{x}(u) = x for u∈c_{x}. Regularity of I implies that ran(d_{x}) (the range of d_{x}) is in I. Let g be the function with domain a satisfying g(x) = ran(d_{x}). Then g : a → I and, by the regularity of I, we get ran(g)∈I. As

{x∈a : ϕ(x)} = {x∈a : 0∈c_{x}} = {x∈a : x∈ran(d_{x})} = ⋃ ran(g)

we get {x∈a : ϕ(x)} ∈ I. ■ Corollary: 10.27 (CZF) I is set-inaccessible if and only if the following are satisfied:

1. I is a regular set,

2. ω∈I,

3. (∀a∈I) ⋃ a∈I,

4. I is ⋀-closed,

5. (∀a, b ∈ I)(∃c∈I) [c is full in mv(^{a}b)].

Proof: In the presence of Set Induction for restricted formulas, clause (5) of Proposition is not needed in the proof of (10). If θ is the formula a = b, one uses a double Set Induction on a, b and the equivalence

a = b ↔ ((∀x∈a)(∃y∈b)[x = y] ∧ (∀x∈b)(∃y∈a)[x = y])

to show (10). If θ is the formula a∈b one uses the equivalence a∈b ↔ (∃y∈ b)a = y. ■

10.4 Mahloness in constructive set theory

This section introduces the notion of a Mahlo set and explores some of its CZF provable properties.

Recall that in classical set theory a cardinal κ is said to be weakly Mahlo if the set {ρ < κ : ρ is regular} is stationary in κ. A cardinal μ is strongly Mahlo if the set {ρ < κ : ρ is a strongly inaccessible cardinal} is stationary in μ.

Definition: 10.28 A set M is said to be Mahlo if M is set-inaccessible and for every R ∈ mv(^{M}M) there exists a set-inaccessible I ∈ M such that

∀x ∈ I ∃y ∈ I ⟨x, y⟩ ∈ R.

Proposition: 10.29 (ZFC) A set M is Mahlo if and only if M = V_{μ} for some strongly Mahlo cardinal μ.

Proof: This is an immediate consequence of Proposition 10.21. ■ Lemma: 10.30 (CZF_{0}^{S}) If M is Mahlo and R ∈ mv(^{M}M), then for every a ∈ M there exists a set-inaccessible I ∈ M such that a ∈ I and

∀x ∈ I ∃y ∈ I ⟨x, y⟩ ∈ R.

Proof: Set S := {⟨x, ⟨a, y⟩⟩ : ⟨x, y⟩ ∈ R}. Then S ∈ mv(^{M}M) too. Hence there exists I ∈ M such that ∀x ∈ I ∃y ∈ I ⟨x, y⟩ ∈ S. Now pick c ∈ I. Then ⟨c, d⟩ ∈ S for some d ∈ I. Moreover, d = ⟨a, y⟩ for some y. In particular, a ∈ I.

Further, for each x ∈ I there exists u ∈ I such that ⟨x, u⟩ ∈ S. As a result, u = ⟨a, y⟩ and ⟨x, y⟩ ∈ R for some y. Since u ∈ I implies y ∈ I, the latter shows that ∀x ∈ I ∃y ∈ I ⟨x, y⟩ ∈ R. ■

Lemma: 10.31 (CZF_{0}^{S}) Let M be Mahlo. If ∀x∈M ∃y ∈M ϕ(x, y), then there exists S ∈ mv(^{M}M) such that

∀xy [⟨x, y⟩ ∈ S → ϕ(x, y)].

Proof: The assumption yields ∀x∈M ∃z∈M ψ(x, z), where

ψ(x, z) := ∃y∈M (z = ⟨x, y⟩ ∧ ϕ(x, y)).

By Strong Collection there exists a set S such that ∀x∈M ∃z∈S ψ(x, z) and ∀z∈S ∃x∈M ψ(x, z). As a result, S ∈ mv(^{M}M) and ∀x∈M ∃y∈M ⟨x, y⟩ ∈ S. Moreover, if ⟨x, y⟩ ∈ S, then y∈M and ϕ(x, y) holds. ■

Corollary: 10.32 (CZF_{0}^{S}) Let M be Mahlo. If ∀x∈M ∃y∈M ϕ(x, y), then for every a ∈ M there exists a set-inaccessible I ∈ M such that a ∈ I and

∀x ∈ I ∃y ∈ I ϕ(x, y).

Proof: This follows from Lemma 10.31 and Lemma 10.30. ■

In a paper from 1911 Mahlo [Ma11] investigated two hierarchies of regular cardinals. In view of its early appearance this work is astounding for its refinement and its audacity in venturing into the higher infinite. Mahlo called the cardinals considered in the first hierarchy π_{α}-numbers. In modern terminology they are spelled out as follows:

κ is 0-weakly inaccessible iff κ is regular;
κ is (α + 1)-weakly inaccessible iff κ is a regular limit of α-weakly inaccessibles
κ is λ-weakly inaccessible iff κ is α-weakly inaccessible for every α < λ

for limit ordinals λ. Mahlo also discerned a second hierarchy which is generated by a principle superior to taking regular fixed-points. Its starting point is the class of ρ_{0}-numbers which later came to be called weakly Mahlo cardinals.

A hierarchy of em strongly α-inaccessible cardinals is analogously defined, except that the strongly 0-inaccessibles are the strongly inaccessible cardinals.

In classical set theory the notion of a strongly Mahlo cardinal is much stronger than that of a strongly inaccessible cardinal. This is e.g. reflected by the fact that for every strongly Mahlo cardinal μ and α < μ the set of strongly α-inaccessible cardinals below μ is closed and unbounded in μ (cf.[Ka], Ch.I,Proposition 1.1). In the following we show that similar relations hold true in the context of constructive set theory as well.

Definition: 10.33 An ordinal is a transitive set whose elements are transitive too. We use letters α, β, γ, δ to range over ordinals.

Let A, B be classes. A is said to be unbounded in B if

∀x∈B ∃y∈A (x∈y ∧ y∈B).

Let Z be set. Z is said to be α-set-inaccessible if Z is set-inaccessible and there exists a family (X_{β})_{β∈α} of sets such that for all β∈α the following hold:

• X_{β} is unbounded in Z.

• X_{β} consists of set-inaccessible sets.

• ∀y∈X_{β} ∀γ∈β X_{γ} is unbounded in y.

The function F with domain α satisfying F (β) = X_{β} will be called a witnessing function for the α-set-inaccessibility of Z.

Corollary: 10.34 (CZF) If Z is α-set-inaccessible and β ∈ α, then Z is β-set-inaccessible.

Lemma: 10.35 (CZF) If Z is set-inaccessible, then Z is α-set-inaccessible iff for all γ∈α the γ-set-inaccessibles are unbounded in Z.

Proof: One direction is obvious. So suppose that for all γ∈α the γ-set-inaccessibles are unbounded in Z. By 10.34 this implies that for all β∈α the β-set-inaccessibles are unbounded in Z; thus

∀β∈α∀x∈Z∃u∈Z(x∈u ∧ u is β-set-inaccessible).

Using Strong Collection, there is a set S such that S consists of triples ⟨β, u, x⟩, where β ∈ α, x ∈ u ∈ Z and u is β-set-inaccessible, and for each β∈α and x∈Z there is a triple ⟨β, u, x⟩∈S. Put

S_{β} = {u : ∃x∈Z ⟨β, u, x⟩∈S}.

Again by Strong Collection there exists a set F of functions such that for β∈α) and any u∈S_{β} there is a function f∈F witnessing the β-set-inaccessi-bility of u, and, conversely, any f∈F is a witnessing function for some u∈S_{β} for some β∈α. Now define a function F with domain α via

F (β) = S_{β} ∪ ⋃{f(β) : f∈F; β∈dom(f)}.

As S_{β} is unbounded in Z, so is F (β). Let y∈F (β) and suppose γ∈β. If y∈S_{β}, then there is an f ∈F witnessing the β-set-inaccessibility of y, thus f(γ) is unbounded in y and a fortiori F (γ) is unbounded in y.

Now assume that y∈f(β) for some f ∈F. As f ↾ β witnesses the β-set-inaccessibility of y, f(γ) is unbounded in y, thus F (γ) is unbounded in y. ■

The preceding lemma shows that the notion of being α-set-inaccessible is closely related to Mahlo’s π_{α}-numbers. To state this precisely, we recall the notion of κ being α-strongly inaccessible (for ordinals α and cardinals κ) which is defined as α-weak inaccessibility except that κ is also required to be a strong limit, i.e. ∀ρ < κ (2^{ρ} < κ).

Corollary: 10.36 (ZFC) Let Z = V_{κ} be set-inaccessible. Then κ is αstrongly inaccessible iff V_{κ} is α-set-inaccessible.

Theorem: 10.37 (CZF) Let M be Mahlo. Then for every α∈M, the set of α-set-inaccessibles is unbounded in M.

Proof: We will prove this by induction on α. Suppose this is true for all β∈α. By the regularity of M we get

∀x∈M ∃y∈M [x∈y ∧ ∀β∈α ∃z∈y z is β-set-inaccessible].  (11)

Using Lemma 10.31 and Lemma 10.28, we conclude that for every a∈M there exists a set-inaccessible I∈M such that a∈I and

∀x∈I ∃y∈I (x∈y ∧ ∀β∈α ∃z∈y z is β-set-inaccessible).

Hence the β-set-inaccessibles are unbounded in I and, by Lemma 10.35, I is α-set-inaccessible. As a result, the α-set-inaccessibles are unbounded in M. ■

Corollary: 10.38 (CZF) Let M be Mahlo. If α ∈ M, then M is α-set-inaccessible.

Proof: Follows from Theorem 10.37 and Lemma 10.35. ■

11 Intuitionistic Kripke-Platek Set Theory

One of the fragments of ZF which has been studied intensively is Kripke-Platek set theory, KP. Its standard models are called admissible sets. One of the reasons that this is a truly remarkable theory is that a great deal of set theory requires only the axioms of KP. An even more important reason is that admissible sets have been a major source of interaction between model theory, recursion theory and set theory. KP arises from ZF by completely omitting the Powerset axiom and restricting Separation and Collection to absolute predicates (cf. [Ba75]), i.e. Δ_{0} formulas. These alterations are suggested by the informal notion of ‘predicative’. The intuitionistic version of KP, IKP, arises from CZF by omitting Subset Collection and replacing Strong Collection by Δ_{0} Collection, i.e.,

∀x∈a ∃y ϕ(x, y) → ∃z ∀x∈a ∃y∈z ϕ(x, y)

for all Δ_{0} formulae ϕ.

By IKP_{0} we denote the system IKP bereft of Set Induction.

11.1 Basic principles

The intent of this section is to explore which of the well known provable consequences of KP carry over to IKP.

Proposition: 11.1 (IKP_{0}) If A, B are sets then so is the class A × B.

Proof: First note that the proof of the uniqueness of ordered pairs in Proposition 3.1 is a IKP_{0} proof. Further, the existence proof of the Cartesian product given in Proposition 3.5 requires only Δ_{0} Collection. ■

Definition: 11.2 The collection of Σ formulae is the smallest collection containing the Δ_{0} formulas closed under conjunction, disjunction, bounded quantification and unbounded existential quantification.

Given a formula ϕ and a variable w not appearing in ϕ, we write ϕ^{w} for the result of replacing each unbounded quantifier ∃x and ∀x in ϕ by ∃x∈w and ∀x∈w, respectively.

Lemma: 11.3 For each Σ formula the following are intuitionistically valid:

(i) ϕ^{u} ∧ u ⊆ v → ϕ^{v}, (ii) ϕ^{u} → ϕ.

Proof: Both facts are proved by induction following the inductive definition of Σ formula. ■

Theorem: 11.4 (The Σ Reflection Principle). For all Σ formulae ϕ we have the following:

IKP_{0} ⊢ ϕ ↔ ∃aϕ^{a}.

(Here a is any set variable not occurring in ϕ; we will not continue to make these annoying conditions on variables explicit.) In particular, every Σ formula is equivalent to a Σ_{1} formula in IKP_{0}.

Proof: We know from the previous lemma that ∃a ϕ^{a} → ϕ, so the axioms of IKP_{0} come in only in showing ϕ → ∃a ϕ^{a}. proof is by induction on ϕ, the case for Δ_{0} formulae being trivial. We take the three most interesting cases, leaving the other two to the reader.

Case 1. ϕ is ψ ∧ θ. By induction hypothesis, IKP_{0} ⊢ ψ ↔ ∃a ψ^{a} and IKP_{0} ⊢ θ ↔ ∃a θ^{a}. Let us work in IKP_{0}, assuming ψ ∧ θ. Now there are a_{1}, a_{2} such that ψ^{a_{1}}, θ^{a_{2}}, so let a = a_{1} ∪ a_{2}. Then ψ^{a} and θ hold by the previous lemma, and hence ϕ^{a}.

Case 2. ϕ is ∀u ∈ v ψ(u). The inductive assumption yields IKP_{0} ⊢ ψ(u) ↔ ∃a ψ(u)^{a}. Again, working in IKP_{0}, assume ∀u∈v ψ(u) and show ∃a ∀u∈v ψ(u)^{a}. For each u∈v there is a b such that ψ(u)^{b}, so by Δ_{0} Collection there is an a_{0} such that ∀u∈v ∃b∈a_{0}ψ(u)^{b}. Let a = ⋃ a_{0}. Now, for every u∈v, we have ∃b ⊆ a ψ(u)^{b}; so ∀u∈vψ(u)^{a}, by the previous lemma.

Case 3. ϕ is ∃u ψ(u). Inductively we have IKP_{0} ⊢ ψ(u) ↔ ∃b ψ(u)^{b}. Working in IKP_{0}, assume ∃u ψ(u). Pick u_{0} such ψ(u_{0}) and b such that ψ(u_{0})^{b}. Letting a = b ∪ {u_{0}} we get u_{0}∈a and ψ(u_{0})^{a} by the previous lemma. Thence ∃a ∃u∈a ψ(u)^{a}. ■

In Platek’s original definition of admssible set he took the Σ Reflection Principle as basic. It is very powerful, as we’ll see below. Δ_{0} Collection is easier to verify, however.

Theorem: 11.5 (The Strong Σ Collection Principle). For every Σ formula ϕ the following is a theorem of IKP_{0}: If ∀x∈a ∃yϕ(x, y) then there is a set b such that ∀x∈a ∃y∈b ϕ(x, y) and ∀y∈b ∃x∈a ϕ(x, y).

Proof: Assume that

∀x∈a∃y∈b ϕ(x, y).

By Σ Reflection there is a set c such that

∀x∈a ∃y∈c ϕ(x, y)^{c}.  (12)

Let

b = {y∈c| ∃x∈a ϕ(x, y)^{c}},  (13)

by Δ_{0} Separation. Now, since ϕ(x, y)^{c} → ϕ(x, y) by 11.3, (12) gives us ∀x∈a ∃y∈b ϕ(x, y), whereas (13) gives us ∀y∈b ∃x∈a ϕ(x, y). ■

Theorem: 11.6 (Σ Replacement). For each Σ formula ϕ(x, y) the following is a theorem of IKP_{0}: If ∀x∈a ∃!y ϕ(x, y) then there is a function f, with dom(f) = a, such that ∀x∈a ϕ(x, f(x)).

Proof: By Σ Reflection there is a set d such that

∀x∈a ∃y∈d ϕ(x, y)^{d}.

Since ϕ(x, y)^{d} implies ϕ(x, y) we get ∀x ∈ a ∃!y ∈ d ϕ(x, y)^{d}. Thus, defining f = {⟨x, y⟩ ∈ a × d| ϕ(x, y)^{d}} by Δ_{0} Separation, f is a function satisfying dom(f) = a and ∀x∈a ϕ(x, f(x)). ■

The above is sometimes unuseable because of the uniqueness requirement ∃! in the hypothesis. In these situations it is usually the next result which comes to the rescue.

Theorem: 11.7 (Strong Σ Replacement). For each Σ formula ϕ(x, y) the following is a theorem of IKP_{0}: If ∀x∈a ∃y ϕ(x, y) then there is a function f with dom(f) = a such that forall x∈a, f(x) is inhabited and ∀x∈a ∀y∈ f(x) ϕ(x, y).

Proof: By Strong Σ Collection there is a b such that ∀x∈a ∃y∈b ϕ(x, y) and ∀y∈b ∃x∈a ϕ(x, y). Hence, by Σ Reflection, there is a d such that

∀x∈a ∃y∈b ϕ(x, y)^{d} and ∀y∈b ∃x∈a ϕ(x, y)^{d}.

For any fixed x∈a there is a unique set c_{x} such that

c_{x} = {y∈b| ϕ(x, y)^{d}}

by Δ_{0} Separation and Extensionality; so, by Σ Replacement, there is a function f with domain a such that f(x) = c_{x} for each x∈a. ■

One principle of KP that is not provable in IKP is Δ_{1} Separation. This is the principle that whenever ∀x∈a [ϕ(x) ↔ ψ(x)] holds for a Σ formula ϕ and a Π formula ψ then the class {x ∈ a| ϕ(x)} is a set. The reason is that classically ∀x∈a [ϕ(x) ↔ ψ(x)] entails ∀x∈a [ϕ(x) ∨ ¬ψ(x)] which is classically equivalent to a Σ formula.

11.2 Σ Recursion in IKP

The mathematical power of KP resides in the possibility of defining Σ functions by ∈-recursion and the fact many interesting functions in set theory are definable by Σ Recursion. Moreover the scheme of Δ_{0} Separation allows for an extension with provable Σ functions occurring in otherwise bounded formulae.

Proposition: 11.8 (Definition by Σ Recursion in IKP.) If G is a total (n + 2)–ary Σ definable class function of IKP, i.e.

IKP ⊢ ∀x⃗yz∃!u G(x⃗, y, z) = u

then there is a total (n + 1)–ary Σ class function F of IKP such that^{6}

IKP ⊢ ∀x⃗y[F (x⃗, y) = G(x⃗, y, (F (x⃗, z)|z ∈ y))].

Proof: Let Φ(f, x⃗) be the formula

[f is a function]∧[dom(f) is transitive]∧[∀y ∈ dom(f) (f(y) = G(x⃗, y, f ↾ y))].

Set

ψ(x⃗, y, f) = [Φ(f, x⃗) ∧ y ∈ dom(f)].

Claim IKP ⊢ ∀x⃗, y∃!fψ(x⃗, y, f).

Proof of Claim: By ∈ induction on y. Suppose ∀u ∈ y ∃g ψ(x⃗, u, g). By Strong Σ Collection we find a set A such that ∀u ∈ y ∃g ∈ A ψ(x⃗, u, g) and ∀g ∈ A∃u ∈ y ψ(x⃗, u, g). Let f_{0} = ⋃{g : g ∈ A}. By our general assumption there exists a u_{0} such that G(x⃗, y, (f_{0}(u)|u ∈ y)) = u_{0}. Set f = f_{0} ∪{⟨y, u_{0}⟩}. Since for all g ∈ A, dom(g) is transitive we have that dom(f_{0}) is transitive. If u ∈ y, then u ∈ dom(f_{0}). Thus dom(f) is transitive and y ∈ dom(f). We have to show that f is a function. But it is readily shown that if g_{0}, g_{1} ∈ A, then ∀x ∈ dom(g_{0}) ∩ dom(g_{1})[g_{0}(x) = g_{1}(x)]. Therefore f is a function. This also shows that ∀w ∈ dom(f)[f(w) = G(x⃗, w, f ↾ w)], confirming the claim (using Set Induction).

6(F (x⃗, z)|z ∈ y) := {⟨z, F (x⃗, z)⟩ : z ∈ y}

Now define F by

F (x⃗, y) = w := ∃f[ψ(x⃗, y, f) ∧ f(y) = w].

■

Corollary: 11.9 There is a Σ function TC of IKP such that

IKP ⊢ ∀a[TC(a) = a ∪ ⋃{TC(x) : x ∈ a}].

Proposition: 11.10 (Definition by TC–Recursion) Under the assumptions of Proposition 11.8 there is an (n + 1)–ary Σ class function F of IKP such that

IKP ⊢ ∀x⃗y[F (x⃗, y) = G(x⃗, y, (F (x⃗, z)|z ∈ TC(y)))].

Proof: Let θ(f, x⃗, y) be the Σ formula

[f is a function]∧[dom(f) = TC(y)]∧[∀u ∈ dom(f)[f(u) = G(x⃗, u, f ↾ TC(u))]].

Prove by ∈–induction that ∀y∃!f θ(f, x⃗, y). Suppose ∀u ∈ y ∃!g θ(g, x⃗, u). By Strong Collection we find a set A such that ∀u ∈ y ∃g ∈ A θ(g, x⃗, u) and ∀g ∈ A ∃u ∈ y θ(g, x⃗, u). By assumption, we also have

∀u ∈ y∃!z∃g∃a[θ(g, x⃗, u) ∧ G(x⃗, u, g) = a ∧ z = ⟨u, a⟩].

Again by Strong Collection there is a function h such that dom(h) = y and

∀u ∈ y ∃g [θ(g, x⃗, u) ∧ G(x⃗, u, g) = h(u)] .

Now let f = (⋃{g : g ∈ A}) ∪ h. Then θ(f, x⃗, y). ■ Definition: 11.11 Let T be theory whose language comprises the language of set theory. Let ϕ(x_{1}, …, x_{n}, y) be a Σ formula such that

T ⊢ ∀x_{1} … ∀x_{n} ∃!y ϕ(x_{1}, …, x_{n}, y).

Let f be a new n-ary function symbol and define f by:

∀x_{1} … ∀x_{n} ∀y [f(x_{1}, …, x_{n}) = y ↔ ϕ(x_{1}, …, x_{n}, y)].

f is then called a Σ function symbol of T.

It is an important property of classical Kripke-Platek set theory that Σ function symbols can be treated as though they were atomic symbols of the basic language, thereby expanding the notion of Δ_{0} formula. The usual proofs of this fact employ Δ_{1} Separation (cf. [Ba75], I.5.4). As this principle is not available in IKP some care has to be exercised in obtaining the same results for IKP_{0} and IKP.

Proposition: 11.12 (Extension by Σ Function Symbols) Let T be one of the theories IKP_{0} or IKP. Suppose T ⊢ ∀x⃗ ∃!y Φ(x⃗, y), where Φ is a Σ formula. Let T_{Φ} be obtained by adjoining a Σ function symbol F_{Φ} to the language, extending the schemata to the enriched language, and adding the axiom ∀x⃗ Φ(x⃗, F_{Φ}(x⃗)). Then T_{Φ} is conservative over T.

Proof: We define the following translation ^{∗} for formulas of T_{Φ}:

ϕ^{∗} ≡ ϕ if F_{Φ} does not occur in ϕ
(F_{Φ}(x⃗) = y)^{∗} ≡ Φ(x⃗, y)

If ϕ is of the form t = x with t ≡ G(t_{1}, …, t_{k}) such that one of the terms t_{1}, …, t_{k} is not a variable, then let

(t = x)^{∗} ≡ ∃x_{1} … ∃x_{k} [(t_{1} = x_{1})^{∗} ∧ ⋯ ∧ (t_{k} = x_{k})^{∗} ∧ (G(x_{1}, …, x_{k}) = x)^{∗}] .

The latter provides a definition of (t = x)^{∗} by induction on t. If either t or s contains F_{Φ}, then let

(t ∈ s)^{∗} ≡ ∃x∃y[(t = x)^{∗} ∧ (s = y)^{∗} ∧ x ∈ y],
(t = s)^{∗} ≡ ∃x∃y[(t = x)^{∗} ∧ (s = y)^{∗} ∧ x = y],
(¬ϕ)^{∗} ≡ ¬ϕ^{∗}
(ϕ_{0}□ϕ_{1})^{∗} ≡ ϕ_{0}^{∗}□ϕ_{1}^{∗}, if □ is ∧, ∨, or →
(∃xϕ)^{∗} ≡ ∃xϕ^{∗}
(∀xϕ)^{∗} ≡ ∀ϕ^{∗}.

Let T_{Φ}^{−} be the restriction of T_{Φ}, where F_{Φ} is not allowed to occur in the Δ_{0} Separation Scheme and the Δ_{0} collection Scheme. Then it is obvious that T_{Φ}^{−} ⊢ ϕ implies T ⊢ ϕ^{∗}. So it remains to show that T_{Φ}^{−} proves the same theorems as T_{Φ}. In actuality, we have to prove T_{Φ}^{−} ⊢ ∃x∀y [y ∈ x ↔ y ∈ a ∧ ϕ(a)] for any Δ_{0} formula ϕ of T_{Φ}. We proceed by induction on ϕ.

1. ϕ(y) ≡ t(y) ∈ s(y). Now

T_{Φ} ⊢ ∀y ∈ a∃!z[(z = t(y)) ∧ ∀y ∈ a∃!u(u = s(y))].

Using Σ Replacement we find functions f and g such that

dom(f) = dom(g) = a and ∀y ∈ a [f(y) = t(y) ∧ g(y) = s(y)] .

Therefore {y ∈ a : ϕ(y)} = {y ∈ a : f(y) ∈ g(y)} exists by Δ_{0} Separation in T_{Φ}^{−}.

2. ϕ(y) ≡ t(y) = s(y). Similar.

3. ϕ(y) ≡ ϕ_{0}(y)□ϕ_{1}(y), where □ is any of ∧, ∨, →. This is immediate by induction hypothesis.

4. ϕ(y) ≡ ∀u ∈ t(y) ϕ_{0}(u, y). We find a function f such that dom(f) = a and ∀y ∈ a f(y) = t(y). Inductively, for all b ∈ a, {u ∈ ⋃ ran(f) : ϕ_{0}(u, b)} is a set. Hence there is a function g with dom(g) = a and ∀b ∈ a g(b) = {u ∈ ⋃ ran(f) : ϕ_{0}(u, b)}. Then {y ∈ a : ϕ(y)} = {y ∈ a : ∀u ∈ f(y)(u ∈ g(y))}.

5. ϕ(y) ≡ ∃u ∈ t(y) ϕ_{0}(u, y). With f and g as above, {y ∈ a : ϕ(y)} = {y ∈ a : ∃u ∈ f(y)(u ∈ g(y))}.

■

Remark 11.13 The proof of Proposition 11.12 shows that the process of adding defined function symbols to IKP or IKP_{0} can be iterated. So if e.g. T_{Φ} ⊢ ∀x⃗∃y ψ(x⃗, y) for a Δ_{0} formula of T_{Φ}, then also T_{Φ} + {∀x⃗∃y ψ(x⃗, F_{ψ}(x⃗))} will be conservative over T.

11.3 Inductive Definitions in IKP

Here we investigate some parts of the theory of inductive definitions which can be developed in IKP.

An inductive definition Φ is a class of pairs. Intuitively an inductive definition is an abstract proof system, where ⟨x, A⟩ ∈ Φ means that A is a set of premises and x is a Φ-consequence of these premises.

Φ is a Σ inductive definition if Φ is a Σ definable class.

A class X is said to be Φ-closed if A ⊆ X implies a ∈ X for every pair ⟨a, A⟩ ∈ Φ.

Theorem: 11.14 (IKP) For any Σ inductive definition Φ there is a smallest Φ-closed class I(Φ); moreover, I(Φ) is a Σ class as well.

Proof: Call a set relation G good if whenever ⟨x, y⟩ ∈ G there is a set A such that ⟨y, A⟩ ∈ Φ and

∀u ∈ A ∃v ∈ x ⟨v, u⟩ ∈ G.

Call a set Φ-generated if it is in the range of some good relation. Note that the notion of being a good set relation and of being a Φ-generated set are both Σ definable.

To see that the class of Φ-generated sets is Φ-closed, let A be a set of Φ-generated sets, where ⟨a, A⟩ ∈ Φ. Then

∀y ∈ A ∃G [G is good ∧ ∃x (⟨x, y⟩ ∈ G)].

Thus, by Strong Σ Collection, there is a set C of good sets such that

∀y ∈ A ∃G ∈ C ∃x (⟨x, y⟩ ∈ G).

Letting G_{0} = ⋃ C ∪ {⟨b, a⟩}, where b = {u : ∃y ⟨u, y⟩ ∈ ⋃ C}, G_{0} is good and ⟨b, a⟩ ∈ G_{0}. Thus a is Φ-generated. Whence I(Φ) is Φ-closed. Now if X is another Φ-closed class and G is good, then by set induction on x it follows that ⟨x, y⟩ ∈ G implies y ∈ X, so that I(Φ) ⊆ X. ■

Theorem: 11.15 (IKP) Let Φ be a Σ inductive definition. For any class X define

Γ_{Φ}(X) = {y| ∃A (⟨y, A⟩ ∈ Φ ∧ A ⊆ X)}.

Then there exists a unique Σ class K such that

K^{a} = Γ_{Φ}(⋃_{x∈a} K^{x})  (14)

holds for all sets b, where K^{a} = {u| ⟨a, u⟩ ∈ K}. Moreover, it holds I(Φ) = ⋃_{a} K^{a}.

Proof: Uniqueness is obvious by Set Induction on a. Let Γ = Γ_{Φ}. Note that Γ is monotone, i.e., if X ⊆ Y then Γ(X) ⊆ Γ(Y). Define

K = ⋃{G| G is a good set}.

We first show (14).

”⊆”: Let z∈K^{a}. Then there exists a good set G such that ⟨a, z⟩ ∈ G. Hence z ∈ Γ(⋃_{b∈a} G^{b}). Since ⋃_{b∈} G^{b} ⊆ ⋃_{b∈a} K^{b} and Γ is monotone we get z ∈ Γ(⋃_{b∈a} K^{b}).

”⊇”: Let z ∈ Γ(⋃_{b∈a} K^{b}). Then there exists a set A ⊆ ⋃_{b∈a} K^{b} such that ⟨z, A⟩ ∈ Φ. Furthermore

∀u∈A ∃G [G is good ∧ ∃x∈a ⟨x, u⟩ ∈ G].

Hence, using Strong Σ Collection, there exists a set Z such that

∀u∈A ∃G ∈ Z [G is good ∧ ∃x∈a ⟨x, u⟩ ∈ G]

and, moreover, all sets in Z are good. Put

G_{0} = ⋃ Z ∪ {⟨a, z⟩}.

Then A ⊆ ⋃_{b∈a} G_{0}^{b}. We claim that G_{0} is good. To see this let ⟨c, w⟩ ∈ G_{0}. Then (∃G ∈ Z ⟨c, w⟩ ∈ G) ∨ ⟨c, w⟩ = ⟨a, z⟩. Thus (∃G ∈ Z w ∈ Γ(⋃_{x∈c} G^{x}) ∨ w ∈ Γ(A), and hence w ∈ Γ(⋃_{x∈c} G_{0}^{x}), showing that G_{0} is good. Now, since z∈G_{0}^{a} and G_{0} is good it follows z ∈ K^{a}.

Using (14) one shows by set induction on a that K^{a} ⊆ I(Φ), yielding ⋃_{a} K^{a} ⊆ I(Φ). For the reverse inclusion it suffices to show that ⋃_{u∈b} K^{b} is Φ-closed. So let z ∈ Γ(⋃_{a} K^{a}). Then there exists a set A ⊆ ⋃_{a} K^{a} such that ⟨z, A⟩ ∈ Φ. Since ∀u∈A ∃x u ∈ K^{x}, by Σ Collection we can find a set b such that ∀u∈A ∃x ∈ b u ∈ K^{x}. Whence A ⊆ ⋃_{u∈b} K^{b}. Consequently we have z ∈ Γ(⋃_{u∈b} K^{b}) = K^{b} by (14), showing that ⋃_{u∈b} K^{b} is Φ-closed. ■

The section K^{b} of the above class will be denoted by Γ_{Φ}^{b}.

Corollary: 11.16 (IKP) If for every set x, Γ_{Φ}(x) is a set then the assignment b ↦ Γ_{Φ}^{b} defines a Σ function.

Proof: Obvious. ■

References

[Acz78] P. Aczel. The type theoretic interpretation of constructive set theory. In MacIntyre, A. and Pacholski, L. and Paris, J, editor, Logic Colloquium ’77, Amsterdam, 1978. North Holland.

[Acz82] P. Aczel. The type theoretic interpretation of constructive set theory: Choice principles. In S.S. Troelstra and D. van Dalen, editors, The L.E.J. Brouwer Centenary Symposium, Amsterdam, 1982. North Holland.

[Acz86] P. Aczel. The type theoretic interpretation of constructive set theory: Inductive definitions. In R.B. et al. Marcus, editor, Logic, Methodology and Philosophy of Science VII, Amsterdam, 1986. North Holland.

[Ba75] J. Barwise. Admissible Sets and Structures. Springer-Verlag, Berlin, Heidelberg, New York, 1975.

[BB85] E. Bishop and D. Bridges. Constructive Analysis. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1985.

[Bee85] M. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, Berlin, Heidelberg, New York, Tokyo, 1985.

[Dia] R. Diaconescu. Axiom of choice and complementation. Proc. Amer. Math. Soc., 51:176–178, 1975.

[CR00] L. Crosilla and M. Rathjen: Inaccessible set axioms may have little consistency strength. To appear in: Annals of Pure and Applied Logic.

[DJ] T. Dodd and R. Jensen: The core model. Annals of Mathematical Logic 20 (1981) 43-75.

[FL] S. Feferman and A. Levy: Independence results in set theory by Cohen’s method. II. (abstract) Notices of the american Mathematical Society 10 (1963) 593.

[Gi] M. Gitik: All uncountable cardinals can be singular. Israel Journal of Mathematics 35 (1980) 61–88.

[Je73] T. Jech: The axiom of choice. (North-Holland, Amsterdam, 1973).

[Je82] T. Jech: On hereditarily countable sets. Journal of symbolic Logic (1982) 43–47.

[Ka] A. Kanamori: The higher infinite. (Springer, Berlin, 1995).

[Ma11] P. Mahlo: Über lineare transfinite Mengen, Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig, Mathematisch-Physische Klasse, 63 (1911) 187–225.

[Ma12] P. Mahlo: Zur Theorie und Anwendung der ρ_{0}-Zahlen, ibid. 64 (1912) 108–112.

[Ma13] P. Mahlo: Zur Theorie und Anwendung der ρ_{0}-Zahlen, ibid. 65 (1913) 268–282.

[ML75] P. Martin-Löf: An intuitionistic theory of types: predicative part, in: H.E. Rose and J. Sheperdson (eds.): Logic Colloquium ’73 (North-Holland, Amsterdam, 1975) 73–118.

[ML84] P. Martin-Löf: Intuitionistic Type Theory, (Bibliopolis, Naples, 1984).

[Myh74] J. Myhill. “Embedding classical type theory in intuitionistic type theory” a correction. Axiomatic set theory. Proceedings of Symposia in Pure Mathematics, Volume XIII, Part II, American Mathematical Society, Providence, 185– 188, 1974.

[Myh75] J. Myhill. Constructive set theory. Journal of Symbolic Logic, 40:347–382, 1975.

[R90] M. Rathjen: Ordinal notations based on a weakly Mahlo cardinal, Archive for Mathematical Logic 29 (1990) 249–263.

[R91] M. Rathjen: Proof-Theoretic Analysis of KPM, Arch. Math. Logic 30 (1991) 377–403.

[RG94] M. Rathjen and E. Griffor. The strength of some Martin-Löf type theories. Archiv for Mathematical Logic, 33:347–385, 1994.

[RGP] M. Rathjen, E. Griffor, E. Palmgren: Inaccessibility in constructive set theory and type theory. Annals of Pure and Applied Logic 94 (1998) 181–200.

[R00] M. Rathjen: The superjump in Martin-Löf type theory. S. Buss, P. Hajek, P. Pudlak (eds.): Logic Colloquium ’98, Lecture Notes in Logic 13. (Association for Symbolic Logic, 2000) 363–386.

[R01] M. Rathjen: The anti-foundation in constructive set theories. To appear in: I. van Loon, G. Mints, R. Muskens (eds.) Proceedings of the 9th CSLI Workshop on Logic, Language and Computation (CSLI Publications, Stanford, 2001).

[Set00] A. Setzer: Extending Martin-Löf type theory by one Mahlo-universe, Archive for Mathematical Logic 39, Issue 3 (2000) 155-181.

[TvD88] S.S. Troelstra and D. van Dalen. Constructivism in Mathematics, Volumes I, II. North Holland, Amsterdam, 1988.