Lectures on Constructive Set Theory

Lecture 3: 8th May (16.30 - 18.00)

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 | p² < 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 notion of Type

The Typing Principle

• Each mathematical object is given as being of some type.
• The notion of an arbitrary mathematical object cannot be used in a mathematical proposition. Of course we can use the notion of an arbitrary mathematical object in non-mathematical propositions; e.g. when we talk about mathematics.
• Each variable used in a mathematical proposition should range over a type (or possibly over a class on a type- see below for this inessential usage).
• Each type A carries with it a notion of equality on A which is reflexive, symmetric and transitive.

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

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

See Lecture 4

Draft. Last Revised: 13th May, 1998.