[FOM] 606: Simple Theory of Types
Sam Sanders
sasander at cage.ugent.be
Sun Aug 30 05:39:06 EDT 2015
Dear Harvey,
As you have pointed out in the past, a non-trivial aspect of Reverse Math is the representation (aka “coding”) of mathematical objects in second-order arithmetic.
In your below posting, you also suggest that low levels of the type hierarchy suffice for formalising mathematics.
In general, I agree with that statement, but there are however non-trivial exceptions (which seem to tank associated grand claims).
In particular, while most of the coding in RM is innocent, it is not always completely faithful/harmless,
as shown by the following examples:
1) The definition of continuity (say on Baire space) in RM reduces type two objects to type one objects.
However, the RM-definition of continuity also gives rise to a type three “fan functional” as follows: The RM-theorem
“every RM-cont. function on Cantor space is uniform RM-cont on Cantor space”
is equivalent to
“there is a functional which takes as input an RM-cont function on Cantor space, and outputs a modulus of uniform (RM) cont.
in Kohlenbach’s higher-order RM. (See Theorem 4.1 in http://arxiv.org/abs/1502.03613 <http://arxiv.org/abs/1502.03613> )
Similar statements can be obtained for other theorems related to continuity, of course.
Thus, the practice of coding in RM, designed to obviate higher-type objects, actually introduces a host of new ones
2) Some RM of topology has been done in sosoa, where topologies are represented/coded by countable bases.
For instance, a theorem concerning topologies on the reals has the form:
(\forall Y^3)(Y is a topology on the reals => A(Y)) (2)
and (2) is interpreted in RM as:
(\forall X^1)(X is a countable basis for a topology on the reals => A(X)), (1)
assuming A is nice enough.
However, (1) has the problem that in Kohlenbach’s higher-order RM, the antecedent “there is a countable basis …” implies full second-order arithmetic.
Hence, when interpreting (1) in the higher-order framework again, it becomes a vacuous truth. (See the PhD thesis of James Hunter at Madison-Wisc. http://www.math.wisc.edu/~lempp/theses/hunter.pdf <http://www.math.wisc.edu/~lempp/theses/hunter.pdf> )
Thus, the RM of topology in second-order arithmetic has considerable problems when re-interpreted in the higher-order framework.
Ironically, Hunter proposes (also in his PhD) to adopt a new type “alpha” for "points in a topology". The subsequent RM of topology looks
a lot nicer as a result (See the final chapters in the aforementioned PhD).
Finally, as I stated at the beginning, the above are exceptions and Kohlenbach has even shown that coding of continuous functions does
not affect the RM of WKL (See his paper in the Feferman Festschrift).
Best,
Sam
> On 30 Aug 2015, at 00:30, 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/be32559b/attachment-0001.html>
More information about the FOM
mailing list