Lectures on Constructive Set Theory

(Padua, Spring 1998)

Lecture 10: 3rd June (16.30 - 18.00)

In the first part of the lecture I described the extensional equality relation, =_V, and membership relation, \in_V on the type V = (W x:U)x. Recall that V is the inductive type with the introduction rule

 A:U   f:A_>V
--------------
  sup(A,f):V

The objects in this type represent well-founded trees and can be used to represent sets by thinking of sup(A,f) as a representation of the set whose elements can be represented by the objects f(a):V for a:A.

For each sentence \phi of the language of set theory, having objects of type V as parameters we can associate a type [[\phi]], so that when \phi is a restricted sentence; i.e. only involves restricted quantifiers and no unrestricted quantifiers, then [[\phi]] is a small type; i.e. a type in U.

[[\alpha = \beta]] = \alpha =_V \beta
[[\alpha \in \beta]] = \alpha \in_V \beta
[[\phi_1 \& \phi_2]] = [[\phi_1]] x [[\phi_2]]
[[\phi_1 v \phi_2]] = [[\phi_1]] + [[\phi_2]]
[[\phi_1 -> \phi_2]] = [[\phi_1]] -> [[\phi_2]]
[[(\forall x)\phi(x)]] = (\Pi \gamma :V) [[\phi(\gamma)]]
[[(\exists x)\phi(x)]] = (\Sigma \gamma :V) [[\phi(\gamma)]]
[[(\forall x\in\alpha)\phi(x)]] = (\Pi a:A) [[\phi(f(a))]]
[[(\exists x\in\alpha)\phi(x)]] = (\Sigma a:A)[[\phi(f(a))]]

Here, we assume that \alpha = sup(A,f) with A:U and f:A->V. Of course this translation uses the propositions as types idea for the logical operations.

THEOREM: If \phi is a sentence that has a proof in the axiom system CZF+REA+DC then [[\phi]] is true in the constructive type theory that has the forms of type: the finite types 0,1,2, the \Pi, \Sigma and W forms of type and the type U of small types that reflects the previous forms.

REA is the Regular Extension Axiom.

This axiom expresses that every set is a subset of a regular set.

The set A is a regular set if it is transitive and for every element a of A, if R:a>-A, where R is a set, then there is a set a' in A such that R:a>-< a'.

The set A is transitive if every element of A is a subset of A.
R:X>-Y if R is a subset of XxY such that for every x in X there is y in Y such that (x,y) is in R.
R:X>-< Y if R:X> -Y and also for every y in Y there is x in X such that (x,y) is in R.

DC is the axiom scheme of Dependent choices. Intuitively it expresses that an infinite sequence of choices
f(0), f(1),... can be made, where the choice of f(n+1) can depend on f(n).

I illustrated the theorem with some of the set existence axioms of Constructive Set Theory, such as the Emptyset Axiom, the Pairing and Union Axioms and the axiom Scheme of Restricted Separation. I tried to explain why the full separation axiom scheme of ZF could not be justified in constructive type theory and also why the Powerset Axiom could not be justified, although the Exponentiation Axiom could.

In the second part of my lecture I started to show how elementary constructive mathematics can be developed in constructive set theory. The main topics that I covered were.

The definition of ordered pairs and the proof that the definition works.
The use of class notation.
Proof that the cartesian product of two sets is a set using Replacement.
Definition of the class of natural numbers as the smallest class containing 0; i.e. the empty set and closed under the operation ()^+ that maps a set x to the set x^+ = [x union {x}]. Proof that such a class exists by explicitly defing it to be the set
```
{ y | \exists X 
     [ (X is a transitive set) \& (y is in X) \& (X is a subset of Z)]
}
```
where Z is the class { x | (x=0) or \exists y(x=y^+) }.
Set Induction is used to prove that the class is smallest, so that the scheme of mathematical induction can be shown to hold for the class of natural numbers.

See Lecture 11

Draft. Last Revised: 3rd June, 1998.