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} < 2 } is
decidable.
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)*.
-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 +.
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].
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.
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.
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.
See Lecture 4
Draft. Last Revised: 13th May, 1998.