Lectures on Constructive Set Theory

(Padua, Spring 1998)

Lecture 3: 8th May (16.30 - 18.00)

See Lecture 2

Lecture 3, first part: More on the constructive theory of Dedekind cuts, based on Rudin(1964).

1. (1.15) continued.
The proposition (1.15) expresses that the cut A can be aproximated arbitrarily closely by a rational number, a property that is surely an essentail property of real numbers. We have seen that to prove 1.15 constructively for a cut A we can assume that A satisfies II'; i.e. that A is a cut'. In fact this is a necessary as well as sufficient condition. So we have the following proposition for a cut A.

Prop: The cut A satisfies (1.15) iff A is a cut'.

Each rational number r determines a cut r* = { p | p < r }. In fact r* is a cut' and is even a decidable cut.

Def: The cut A is decidable if (forall r)[ r:A or not r:A ]

Note that any decidable cut is a cut'. Also note that decidable cuts can be irrational. For example the irrational cut
{ p | p2 < 2 } is decidable.

2. Addition of cuts.

As in Rudin(1964), if A, B are cuts then we can define

A+B = { p+q | p:A & q:B }

and show that A+B is a cut. Moreover it is a cut' if both A and B are. We can prove the basic properties of +; e.g. it is commutative and associative, with identity 0*. Also r*+s* = (r+s)*.

3. Subtraction of cuts.

This needs some care. For each cut A we can define

-A = { -p | (exists q< p)[ not q:A] }

and show that this is a cut and is a cut' if A is. We can then define the cut A-B = A+(-B), for cuts A, B. But, for a cut A, while A-A is a subset of 0* we cannot prove equality unless we assume that A is a cut'. In fact we have the following proposition.

Prop: For each cut A, [A-A = 0*] iff A is a cut'.

Note that if A is a cut' then -A is the unique cut' B such that A+B=0*. So the cut' form an additive group with group operation +.

4. The absolute value of a cut.

We cannot in general decide if a cut' is positive, negative or 0*. So we cannot use the procedure in (1.24) of Rudin(1964) to define the absolute value |A| of an arbitrary cut A by cases. A more elaborate procedure is needed and we may as well describe the procedure in some generality. Given any uniformly continuous function f:Q->Q, such as the absolute value function on Q that maps r to |r|, we show how to determine a function f* that assigns a cut' f*(A) to each cut' A so that f*(r*)=f(r)* for each r:Q. We first define uniform continuity. The variables k,i range over the set of natural numbers.

Def: A function f:Q->Q is uniformly continuous if, for every k there is an i such that for all r,r'

|r-r'| <= 2-i ==> |f(r)-f(r')| <= 2-k.

Def: Let f:Q->Q be uniformly continuous. For each cut A let

f*(A) = { p | (exists p'>p)(exists r:A)(forall r':A)[r'>r => p'<f(r')] }

Prop: If A is a cut' then so is f*(A). Moreover for each rational r, f*(r*)=f(r)*.

Prop: If f,g:Q->Q are both uniformly continuous then so is their composition fog and, for each cut' A, (fog)*(A)=f*(g*(A)).

Using this last proposition we can get equalities such as

|A| = |-A| for all cuts' A.

Exe: Let f,g:Q->Q be uniformly continuous. Show that if (forall r>0)[f(r)=g(r)] then, for all cuts' A,

A>0* ==> f*(A) = g*(A).

We can apply this to get that

[A>0* ==> |A| = A] and [A<0* ==> |A| = -A].

5. Multiplication of cuts.

The definition of multiplication of cuts in (1.25) of Rudin(1964) will not do constructively, as again it involves using cases which do not cover all possible cuts'. Instead we can carry over the previous construction of f* from a unary uniformly continuous function f on Q to n-ary uniformly continuous functions f on Q in a straightforward way and then apply the general construction to the binary multiplication function, which is uniformly continuous, of course. We then get the definition, for cuts A,B,

A.B = { p | (exists p'>p)(exists r:A)(exists s:B)
(forall r':A)(forall s':B) [(r'>r and s'>s) => p'< r'.s'] }

At this point we have to end our introduction to the constructive theory of Dedekind cuts. The interested reader should be able to make the necessary further changes to chapter 1 of Rudin(1964) so as to get a constructive reformulation.

Lecture 3, second part: Types, classes and sets

The word `set' and related words such as `type', `class', `collection', `domain', `system', `manifold', etc ... have been used for many distinct notions, often in a confusing way. We need to disentangle these notions from each other.

The notion of Type

We will use a notion of type in the following principle.
The Typing Principle
This notion of type has its roots in Aristotle's notion of category. I think of the category of an object as something that represents the essential properties of the object in contrast to its accidental properties. For example I think that the natural numbers form a category (and a type). It is an essential property of the natural number two that it is a natural number. But it is accidental that the number two is an even natural number.

In my view the typing principle is an essential starting point in thinking about the nature of mathematics. But it has not generally been adopted by philosophers. Russell introduced his notion of type as a way to resolve his paradox and used it in his monumental three volume work with Whitehead, Principia Mathematica. His notion is close to the one expressed in the above typing principle. Frege had earlier introduced a formal language with a hierarchy of `types' of entity. But he did not adopt the typing principle as, from the start, he assumed that there is a `type' of all objects, his other `types' consisting of entities that he called functions. He sharply contrasted functions with objects, functions being incomplete entities in contrast to the completed entities that are objects. The distinction was based on a corresponding syntactic distinction in language.

The notion of Class on a Type

Given a type A, a class, B={x:A|P(x)}, on A is given by a predicate P(x). For each object c of type A we write c:B for the proposition that is true if c satisfies the predicate; i.e. if the proposition P(c) is true.

Example: We have the type N of natural numbers. But we do not want to say that the even natural numbers form a type, rather they form the class {x:N|x is even} on N. An even natural number is first of all a natural number and only secondarily even.

We may want to quantify over a class B on a type A. But this can be reduced to quantifying over the type A. Instead of (for all x:B)Q(x) we can write (for all x:A)[x:B -> Q(x)] and instead of (exists x:B)Q(x) we can write (exists x:A)[x:B & Q(x)]. When working with classes on a type A it is usual to adopt the following principle.

The Class Extensionality Principle
If B,C are classes on a type A then we consider them equal and write [B=C] if
(for all x:A)[x:B <-> x:C].

See Lecture 4

Draft. Last Revised: 13th May, 1998.