[FOM] 606: Simple Theory of Types

[Harvey Friedman]

I received the following query offline:

> Harvey,
>
> please what is the type of reals, R?
> How this number can be computed?

It may depend on how you view R mathematically. Simplest of course is
to view R as the set of all left Dedekind cuts.

But there are more philosophically sensitive approaches to what reals
are related to their functionality. I haven't thought through this for
R.

Here is a table based on a philosophically sensitive treatment of N
and Z discussed in
http://www.cs.nyu.edu/pipermail/fom/2015-August/018951.html and
somewhat philosophically sensitive treatments of ordered pairs, and
mathematically standard treatments of Q (as sets of ordered pairs of
integers) and R (as left Dedekind cuts).

each natural number: type 2
N is of type 3
each ordered pair of natural numbers: type 4
each function from natural numbers to natural numbers: type 5
N^N is of type 6
each ordered pair from N^N: type 7
each integer: type 8
Z is of type 9
each ordered pair of integers: type 10
each rational: type 11
Q is of type 12
each real number is of type 13
R is of type 14

Of course, from
http://www.cs.nyu.edu/pipermail/fom/2015-August/018951.html we know
that Z_2 or ZFC\P can be interpreted in type theory of levels 0,1,2
with INF. If you want a smooth theory of sets of real numbers, you can
use levels 0,1,2,3 with INF.

Harvey Friedman