Lectures on Constructive Set Theory

(Padua, Spring 1998)

Lecture 12: 10th June (16.30 - 18.00)

See Lecture 11

Inductive Definitions

By an inductive definition in constructive set theory I simply mean a class of ordered pairs. Each element (X,a) of the class is thought of as a(n) (inference) step with set X of premisses and conclusion a. Given an inductive definition, class Y is closed if for each step (X,a) of the inductive definition

if X is a subset of Y then a is in Y

Theorem 1 [Inductive Definitions of classes, provable in CZF]

For every inductive definition there is a smallest closed class, which may be called the class of theorems of the inductive definition.

Theorem 2 [Inductive Definitions of sets, provable in CZF+wREA]

For every inductive definition that has a set bound and is weakly local the class of theorems forms a set.

Definition

B is a bound for an inductive definition if for each step, its set of premisses is an image of a set in B. Here X is an image of b if there is a function from b onto X.

Definition

An inductive definition is weakly local if, for each set X the class of conclusions of all steps having exactly the set X of premisses, forms a set.

Definition

The axiom wREA is the weak regular extension axiom. It states that every set is a subset of some weakly regular set, where a set A is weakly regular if it is transitive and for every element a of A, if R:a>-A, where R is a set, there is a set a' in A such that R :a>- a'. Note that this axiom is a weakening of REA.

These definitions and theorems were illustrated with a list of examples of inductive definitions.

  1. The class of natural numbers, Nat, is inductively defined to be the smallest class Y such that

    Here 0 is the empty set and a^+ is the set [a union {a}].

  2. The class Ord_2 is the smallest class Y such that

  3. If A is a class and B(a) is a set for each a in A then W_{x in A}B(x) is the smallest class Y such that

  4. If A is a class then H(A) is the smallest class Y such that whenever the set X is in the class Im(:A) then

  5. The class V of all sets is the smallest class Y such that for every set X

    The Set Induction Scheme expresses this property of V.
In each example we can specify the inductive definition (i.e. class of ordered pairs) that we are using.
  1. The class {(0,0)} union {({a},a^+) | a in V},

  2. The class {(0,0)} union {(ran(f),f) | f:Nat -> V},

  3. The class {(ran(f),(a,f)) | a is in A and f:B(a) -> V},

  4. The class {(X,X) | X is in Im(:A)},

  5. The class {(X,X) | X is in V}.
The lecture ended with some general remarks to finish off the series of lectures.

Draft. Last Revised: 12th June, 1998.