[FOM] 606: Simple Theory of Types

[Harvey Friedman]

This posting is about Adventures in Russell Type Theory.

1. Philosophical considerations.
2. Mathematical consolidation..
   2a. Interpretation between structures.
   2b. Interpretation between theories.
3. Research Projects..

1. PHILOSOPHICAL CONSIDERATIONS

What is a natural number, 0,1,2,...? These are as counts.

It is a property of properties of objects. This locates it in the
Russell hierarchy. Each natural number is in type 2. Being a natural
number is in type 3.

type 0    objects
type 1    properties of objects
type 2    properties of properties of objects
...

i.e., the simple theory of types. We may ultimately want to go to more
elaborate type theories, but we want to be careful to avoid a
proliferation of complications before anything interesting gets
done.See section 3.

We could also think of the natural numbers at higher types, but we
think of the objects as incredibly rich, and so we will initially be
focused at the minimal places where our favorite objects naturally
lie.

Now what is an integer? These can't be as counts, in the direct sense
of the natural numbers, because of the presence of negatives.

So what are integers, really? They must be quantities associated with
the application of reversible processes. 0 is doing nothing, 1 is
doing it once, or going forward, one step -1 is undoing it once, or
going backward one step.

Well, we haven't even discussed what a function is. And before that,
we need to discuss what an ordered pair of objects is. Before this,
there is the singleton and the unordered pair. of objects The latter
two are properties of objects. The ordered pair of objects is a
property of properties of objects.

NOTE: The robustness of the philosophy has weakened some here with
this well known treatment of ordered pairs - compared to the opening
example of the natural numbers. Can it be improved on? Of course, we
can go to a more elaborate system of types, where we allow Cartesian
products as primitive. But that would be premature as we try to build
this OLD and I think ABANDONED subject up in a systematic way.

In summary so far:

Each natural number is of type 2.
N is of type 3.
{a}, {a,b} is of type 1.
(a,b) is of type 2.
(a_1,...,a_n) is of type 2.

What about a function from type 0 to type 0? Each such must be of type
3. Reversible functions are a kind of function.

So an integer is an operation from reversible functions to reversible
functions. Operations from type k to type k, by the previous
constructions, are naturally of type k+3.

So each (signed) integer is of type 6.

What is a rational number? These are certain relationships between
integers. Integers are of type 6, and therefore each rational number
is of type 9.

Obviously, as we go through elementary mathematics, we are moving into
very very very high types this way.

We can properly ask for the minimum number of types needed in order to
"reasonably accomplish existing standard mathematics". This seems to
have a good answer in section 2 below.

However, "reasonably accomplish" does NOT entail Philosophically
Sensitive. We were very philosophically sensitive at least at the
outset with the natural numbers as type 2 objects.

QUESTION. What does Philosophically Sensitive mean here? What is
Philosophically Insensitive about what I am about to say below? What
types are needed for Philosophical Sensitivity?

2. MATHEMATICAL CONSOLIDATION

CLAIM. The vast preponderance of mathematics can comfortably be
developed in type 0, type 1, type 2. Theorems 2 and ? below.

What theorems support this? Interpretations. There are two main kinds.
One is interpretations between structures. The other is
interpretations between theories.

   2a. Interpretations Between Structures.

One structure is interpretable in another if the second structure
defines an isomorphic copy of the first structure. Here we allow

i. Finitely many parameters in the definitions of the domains and the
constants, relations, and functions. .
ii.  Equality can be interpreted by an equivalence relation.
iii. Functions are treated as relations, and so with ii allowed, the
univalence is only required to be up to the equivalence relation for
equality.
iv. Domains can be subsets of finite unions of Cartesian products.

See section 3.

THEOREM 1. Let D be arbitrary. (V(omega),epsilon) is not interpretable
in (D,PD,epsilon).

Proof: This can be proved using elimination of quantifiers.
Developments in monadic second order logic and in Boolean algebras
seem to give this directly. E.g., (D,PD,epsilon) is decidable, even
with any parameters, but  (V(omega),epsilon) is not decidable. QED

THEOREM 2. Let D be countably infinite.  If n >= 2, then  (V(omega +
n,epsilon) is interpretable in (D,PD,...,P^nD,epsilon,...,epsilon).
If n >= 1, then (D,PD,...,P^nD,epsilon,...,epsilon) is interpretable
in (V(omega + n,epsilon).

THEOREM 3. Let D be any set. (V(omega),epsilon) is not interpretable
in (D,PD,epsilon).

Proof: Elimination of quantifiers, or well known work in Boolean
algebra or monadic second order logic. QED

   2b. Interpretations Between Theories.

Interpretation between theories, even if parameters are allowed and
equality is interpreted by an equivalence relation, is sufficient to
establish relative consistency, and also conservation when formulated
appropriately..

On the one hand we are going to use Z_n, n >= 1, which is n-th order
arithmetic. Z_1 is PA. Z_2 is the famous two sorted first order system
of second order arithmetic. And so forth. It has 0,S,+,dot for the
bottom sort, sort 1 in the usual way of counting here, induction for
sets of sort 2, and full comprehension for sets of each sort.

On the other hand, we have RT_n, n >= 1, which is the Russell Type
Theory with types 0,...,n. We have just full comprehension at each
level. We will have the epsilon symbols for each type >= 1, but no
equality symbols.

Of course, RT_n has no logical strength because there may be exactly
one object of type 0.

So to get things going, we really need to have an axiom of infinity
for the RT_n.

We are not going to be able to state any kind of axiom of infinity
just with types 0,1, in light of the following.

COMPLETENESS. Let phi be a sentence in types 0,1. phi is provable in
the union of the RT_n if and only if phi is provable in RT_1. This is
recursive. Furthermore, if phi is consistent with RT_1 then phi has a
model with finitely many objects of type 0.

Proof: Elimination of quantifiers, or well known work in Boolean
algebra or monadic second order logic. QED

Here is a common formulation of the axiom of infinity in RT. It is the
simplest that I know of.

INF = There exists a type 2 object with an element, and where every
element is a proper subset of an element.

THEOREM 4. If n >= 2, then Z_n is interpretable in RT_n + INF is
interpretable in Z_n+1.

If we strengthen INF to

INF(lin) = "there exists a type 2 object forming a nonempty linear
ordering with no right endpoint under inclusion."

then we get

THEOREM 5. If n >= 2, then Z_n and  RT_n + INF are mutually interpretable.

3. RESEARCH PROJECTS

1. Determine if n+1 can be replaced by n in Theorem 4.

2. Recall these conditions on interpretations, which we allowed above:

i. Finitely many parameters in the definitions of the domains and the
constants, relations, and functions. .
ii.  Equality can be interpreted by an equivalence relation.
iii. Functions are treated as relations, and so with ii allowed, the
univalence is only required to be up to the equivalence relation for
equality.
iv. Domains can be subsets of finite unions of Cartesian products.

There are obviously 8 = 2^3 possible restricted kinds of
interpretations (I'm not viewing iii as an independent option). Redo
the above Theorems under each of the 7 remaining restrictions on
allowable interpretations, and of course revisit 1.

3. Prove or refute that INF is the simplest possible axiom of infinity
in the simple theory of types. Count the number of quantifiers.

4. Revisit 1-3 using alternative fundamental type theories. Here are
some important ones.

objects
functions from objects to objects
functions from (functions from objects to objects) to objects
...

objects
functions from objects to objects
 functions from (functions from objects to objects) to (functions from
objects to objects)
...

objects
binary relations on objects
binary relations on binary relations on objects
...

************************************************************
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 606th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM

Harvey Friedman