901: Remarks on Reverse Mathematics 6

[Harvey Friedman]

I now want to discuss the choice of base theories for Reverse Mathematics.

1.Using Higher Types in a Base Theory
2. Using RM for "extended countable mathematics"

1. USING HIGHER TYPES IN A BASE THEORY

Using higher types in a base theory for foundational reverse
mathematics is very problematic. Normal mathematical practice has very
limited use of objects of higher types. The types don't go very far,
and whatever types are used they are used in every elemental ways that
are of a FUNDAMENTALLY COUNTABLE ESSENCE. I would doubt if any unusual
logical strength (like the higher levels of Z_2) would come out of
basic theorems like NIN and Riemann Integrability, and bounded
variation theorems, when combined with any higher type base theory.
reflecting mathematical practice.

I have yet to see any collection of normal mathematical statements
from the ordinary mathematical literature, even with unrestricted
third order notions, which, when combined with say ATR0, results in a
system that isn't readily interpretable in familiar systems from usual
RM. In particular, with statements such as NIN and Riemann
integrability, and bounded variation theorems, and so forth, when
combined with anything resembling a base theory, I don't see any
unusual logical strength.

There is this exchange:

ME:

> The use of any functionals of higher type in actual mathematics is
> almost nil and certainly is not fundamental like the use of RCA0 which
> is pervasive.

SANDERS:

I argue below that at least historically, third-order objects can be
found in the
the mainstream literature (Euler, Abel, Dirichlet, …), in the form of
discontinuous functions.

***********

When I said "the use of functionals of higher type in actual
mathematics is almost nil" what I meant was that for almost all of the
higher types it is almost nil. In fact, where is the last place one
sees a functional of type 24 in mainstream mathematics? And compared
to types 1,2? And I was talking about this in the context of the
choice of base theories, and comparing it to RCA0. The use of RCA0 in
mathematics is overwhelmingly common, incomparably more so than
GENERAL third order.

I have not seen any indication of an extension of say even ATR0 by
fundamental mathematical statements in types 1,2,3 in the classical
mathematical literature that carries any unusual logical strengths
like higher fragments of Z_2. Especially, I do not see any such thing
surrounding statements like NIN.

Nevertheless, it is still interesting to investigate possible base
theories for types 1,2,3. For instance "pointwise convergent sequences
of functions have a limit function", which along with composition will
give us the arithmetical operators from R into R with parameters from
R. One can propose primitive recursion here which will throw us into
weak fragments of ATR0. Also one can consider a sup operator which
yields the hyperjump, and do composition and primitive recursion here,
to get modest fragments of Pi-1-1-TR0.  All of this is definitely
worth working out carefully, laying out all of the obvious things that
are needed in the base theory to actually carry this out.

Now let me make a case that there are even a little bithigher types
are present in math. For this all we have to do is insist that the
real numbers be defined not by Dedekind cuts but rather as equivalence
classes of Cauchy sequences of rationals (with say 2^-n convergence).
Then every real is a type three object and sets of reals are type four
objects. I can see a base theory that allows us to manipulate real
numbers inside real functions, with some set formation. But I don't
see a legitimate base theory associated with this that is going to get
unusual logical strength from such statements as NIN which is now a
fourth order statement rather than a third order statement.

2. USING RM FOR "EXTENDED COUNTABLE MATHEMATICS"

There is already a highly developed and highly developing area of
substantial technical and foundational interest with an already fixed
base theory. Namely usual RM and RCA0. And this works extremely well
for a rather substantial portion of mathematics. The question to be
addressed here is how or even should we expand the scope of RM.

There are a number of ways we could expand the scope of RM. One way
alluded to above that requires serious care is to introduce
unrestricted third order objects. A straightforward way of doing this
has been worked in which is to lift arithmetic comprehension to type
3. This is a reasonably sensible system although it loses the lower
strength phenomena. I'm not sure we have fleshed out what we should
really have if we are just wanting to stay at the level of strength of
RCA0. We can use sensible base theories like this in order to
investigate the status of NIN, Riemann integrability, bounded
variation theory, Lebesgue theory, Borelain mathematics, and so forth.
In fact, along these lines, there should be good analogs of the big
five systems of usual RM.

Earlier I recommended the use of presentations in order to circumvent
any need for third order objects. But this here seems to be a good
approach that seems well controlled by the usual RM.

First some remarks concerning the existing scope of RM, with its base
theory RCA0.

The most obvious .kind of mathematics that lies comfortably within the
scope of RM is the mathematics where the objects involved are all
countable.By this I mean directly countable as in "sets of integers"
or "sets of rationals" or "Dedekind or Cauchy real numbers", Cauchy
without taking the equivalence classes and instead using the
equivalence relation. It also includes all kinds of countable
mathematical structures, like countable groups, rings, fields, and so
forth. This excludes functions of a real variable, for Polish spaces,
for example.

This fairly strict interpretation of what we mean by "countable
mathematics" is rather substantial, but we generally incorporate
certain extensions of it in various ways to stay within the scope of
RM. I will call this "extended countable mathematics".

The idea of the extended RM of extended countable mathematics is to
ultimately give an interpretation of extensions of the usual RM with
new sorts and new relations and operations,

Usually what we do in RM is just give the interpretations in the form
of RM codes. What we normally skip is even the identification of a
theory involving the new concepts which is being interpreted. Here is
a clear example.

Polish Spaces. These are treated in RM directly via the
interpretation. Namely a code for a Polish Space is just a countable
metric space M. Then one defines what the Polish Space is with code M
as the infinite sequences of 2^-n Cauchy sequences from M, with the
obvious equality relation, and also the obvious metric. This metric is
a defined concept as it would be of higher type as an object.

We don't normally try to rigorously "justify" or rigorously "prove"
the correctness of this way of coding Polish Spaces. After all, how
can you prove an interpretation when you haven't even given the theory
you are allegedly interpreting?

So what is missing is a theory of Polish Spaces where this coding is
in fact an interpretation of that theory.

This coding of Polish spaces is so unproblematic that we are not
compelled to carry this out but it follows a pattern that much of what
I did in https://cs.nyu.edu/pipermail/fom/2021-October/022899.html
with reals, infinite sequences of reals, and continuous real
functions.

We introduce two sorts. One is for Polish Space objects, and the other
for Polish Spaces themselves. See already there is something
interesting going on - namely we really do have to have these two
sorts, with this maybe mysterious "elements of Polish spaces", and
equality of elements of Polish Spaces. We have being an element of a
Polish space as a binary relation. Then we have the primitive - the
distance between two elements of a Polish space, which must be a
nonnegative real number.  We have the axiom that equality is the same
as distance 0. We have the triangle inequality.

We need an axiom that tells us that Polish Spaces are complete. For
that, we need to have more primitives, those supporting infinite
sequences of Polish space elements, and supporting principles. This
needs to be done by relating infinite sequences from Polish Spaces to
infinite sequences of integers in ordinary RM. We also need an axiom
that tells us that Polish spaces have a countable dense subset.
Density needs to be treated with some care, as it may be too
existential. And also we need to be able to build Polish Spaces and we
need to introduce a completion operation that takes a countable metric
space and completes it into a Polish Space. We see that quite a lot of
primitives have to be introduced to carry this out for Polish Spaces,
as well as associated axioms. We know what the result of this is
supposed to be. Namely that the usual treatment of Polish Spaces
actually constitutes a bona fide interpretation of this theory.

Obviously there are a lot of details that need to be gotten exactly
right for this to work. And this is only for the very unproblematic
case of Polish Spaces.

So there really is a big subject here, namely "the RM of essentially
countable mathematics" which of course includes Polish Spaces,
(partial) continuous functions between Polish Spaces, (partial) Baire
class alpha functions between Polish spaces, alpha <= omega1, and
presumably many many more things, The idea is of course one develops
countable codes, so ultimately we pull back to ordinary RM, but we
also set up a framework to PROVE that those codings are correct.

Let me close by another important aspect of RM. A great deal of
mathematics falls below the radar screen. I.e., it is provable in RCA0
and therefore a possibly great amount of phenomena is not falling
under usual RM. There has been some work on addressing this issue,
namely use of the weaker RCA0* replacing RCA0 (RCA0* due to Simpson).
The idea is to replace Sigma01 induction in RCA0 by Delta01 induction
with 0,1,+,x,exp,<, a conservative extension of EFA.

The SRM idea (strict reverse mathematics) is to disallow any of the
usual systems in f.o.m. which are generally schematics, and replace
them with actual mathematical theorems in the literature or what might
be called essentially in the literature. Then the phenomana that RM
misses below RCA0 or even RCA0* is taken head on and analyzed as it
comes in actual mathematics. This was discussed some in the earlier
Remarks on Reverse Mathematics. SRM is the ultimate discipline, both
for the very weak and for the ordinary and for the very strong. See
paper 58 at https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/

Harvey Friedman

##########################################

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 900th 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-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

900: Ultra Convergence/2  10/3/21  12:38AM