[FOM] 606: Simple Theory of Types

[John Baldwin]

In the posting Adventures in Russell type theory

In section 2a Harvey Friedman writes:

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

a list follows. But what logic is being used to make these `definitions'?

John T. Baldwin
Professor Emeritus
Department of Mathematics, Statistics,
and Computer Science M/C 249
jbaldwin at uic.edu
851 S. Morgan
Chicago IL
60607

On Sat, Aug 29, 2015 at 5:30 PM, Harvey Friedman <hmflogic at gmail.com> wrote:

> 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
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150830/1668c94e/attachment.html>