912: Base Theory Proposals for Third Order RM/5

[Harvey Friedman]

*Until Sanders and I agree on the foundational point of foundational
RM and the role of foundational base theories, it makes sense for me
to respond only to technical issues that may arise.*

1. Third Order RM Compliments RM - no radical foundational advance or
upheaval - #2
2. ACA0[3] at level of ACA - experimental - #2
3. Some Third Order Reverse Math - RM[3] - #3
4. Claims of High Logical Strength - #4
5. Reverse Math and Strict Reverse Math - Original Intent - here
6. Strict Reverse Math Research - next posting
7. The logical power of Inversion/1 - #6
8. The logical power of Inversion/2 - #7

5. REVERSE MATH AND STRICT REVERSE MATH - ORIGINAL INTENT

There are two well known examples of investigations that have the same
general structure as RM and greatly precede RM.

1. There is the logical analysis of statements in classical geometry
in the sense of Euclid. A second order axiomatization of Euclidean
Geometry was given by David Hilbert and later a first order
axiomatization of Euclidean Geometry was given by Alfred Tarski.
Hilbert's is complete in the second order sense, while Tarski's is
complete in the first order sense. The notorious parallel axiom became
very controversial and there came to be a clear division between
Euclidean Geometry and a fragment of Euclidean Geometry called
Absolute or Neutral Geometry. Second and first order axiomatizations
of the Absolute Geometry evolved, and served as a base theory for what
we now view as Reverse Geometry studies. Over Absolute Geometry, which
statements prove which statements, with special attention to which
statements prove the parallel axiom. I was looking for a robust
delineation of Absolute Geometry (second order and first order) so
that the particular axioms for it being used would not look to have
any ad hoc or accidental historical features. I didn't readily find
that, and I would appreciate it if some FOM subscribers can inform me.
Hilbert's axiomatization is 1899. Non Euclidean Geometries go back to
around 1830.Tarski's first order axiomatization is 1959. So there
really are two forms of Reverse Geometry here. One is second order and
one is first order. The first uses second order Absolute Geometry
axioms, whereas the second uses first order Absolute Geometry axioms.
But note that this is only aimed at rather special but quite
interesting mathematical statements.

2. There is the logical analysis of statements in set theory without
choice. The base theory is ZF and the main focus is whether one is
reversing to the AxC or what natural fragments of AxC. The classic is
Rubin and Rubin, 1963. Here the scrope is of course quite limited for
a somewhat different reason. The amount of mathematics that can be
proved in ZF, therefore under the radar screen, is enormous. Also
there is an interesting analog to the question I raised in 1 of
characterizing exactly what Absolute Geometry should mean 2nd order
and 1st order. Namely, suppose we are sitting in ZFC. Then what is ZF?
Is there a theorem to the effect that a sentence phi is provable in ZF
if and only if it is provable in ZFC and has certain properties? Or a
sentence phi is provable in ZF if and only if some associated sentence
phi* is provable in ZFC? Of course, there are uninteresting answers to
these questions, but we want informative answers. Or sharpen these
questions. Same for Absolute Geometry and Euclidean Geometry as in 1,
both second order and first order. Also notice that in 1, I was
careful to mention BOTH 2nd order and 1st order formulations. What I
am talking about here is normally discussed only for 1st order. But
what happens if we discuss 2nd order ZF and 2nd order ZFC? Is this
even interesting? If so, what would a discussion of this look like? If
not, why not? Of course one big difference is that Euclidean Geometry
is 2nd order categorical and ZF is not 2nd order categorical.

So the foundational interest of a brand of Reverse Mathematics depends
crucially on the base theory being used. I chose RCA0 to be weak
enough so that a large amount of mathematics would be unprovable in
RCA0, and strong enough so that I wouldn't be confronted by a wild zoo
right off the bat. Of course, much later wild zoos did develop out of
RM, but those wild zoos would have harmed the growth of the field if
they emerged right away. Also instead of the RCA with full induction,
I chose RCA0 with just set induction, strongly influenced by the SRM =
strict reverse mathematics idea. RCA0 is both finitely axiomatized and
set induction really does meet the standards of strictly mathematical.

My early papers on RM, besides ICM and those two JSL abstracts, are on
my website at https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
and include

The Analysis Of Mathematical Texts, And Their Calibration In Terms Of
Intrinsic Strength I-III, 1975.

As you can see, my original conception of RM was really SRM = strict
reverse mathematics, where there is no base theory at all. I
introduced a base theory because I saw quite clearly that the subject
was unworkable at a practical level with the SRM idea. Yes it is true
that these 1975 papers are a little bit after the ICM talk, but it was
my real motivation. However I realized that working without a proper
base theory would not lead to viable research project, because in
order to really get off the groun, there would have to be a  number of
major advances and clarifications and consolidations, including
bringing in foreign sounding qualitative judgments.

Such considerations were behind my choice to use a finitely
axiomatized system for a base theory. Hence RCA0 was the natural
choice. The particular essentially equivalent version of RCA0 and the
other finitely axiomatized systems in the JSL abstracts were attempts
to give axioms for these theories that were arguably basic actual
mathematical statements familiar and friendly to mathematicians. So in
those abstracts, instead of Sigma01 induction and Delta11-CA0, both
highly metamathematical,  I used bold faced primitive recursion and
inverses of permutations, both highly mathematical.

So why this obsession with not having a base theory and striving for
the actual mathematics to speak for itself when it comes to logical
strength?

A. CAN WE PROVE THAT THE WHOLE OF ACTUAL MATHEMATICS IS FREE OF
CONTRADICTION in systems as weak as maybe EFA = exponential
arithmetic?
B. CAN WE INTERPRET THE WHOLE OF ACTUAL MATHEMATICS IN EFA?

If we can, then this would essentially obsolete the Goedelian picture
that we have of foundations. It would pretty much render all of our
formal systems like ZFC moot.

This would happen if we found an alternative way to formalize
mathematics which avoids the systems we now use, and prove in EFA that
these alternative systems are consistent.

Addressing this is the essence of the SRM project.

There is an interesting criticism of A that goes like this. A is
assuming that actual mathematics is going to use unlimited axioms for
logic, and unlimited use of the rules of inference for logic. So just
I say that mathematicians aren't going to be using all instances of
schemes, we can say that mathematicians aren't going to use all
instances of logic. Well, there are three reasonable responses to
this:

a. The complete axiomatization of first order logic is sacrosanct and
we don't mess with it when formalizing mathematics.
b. We are open to the discovery of fragments of first logic that are
arguably sufficient for mathematical practice.
c. Let's sidestep this and ask for an interpretation as in B.

To sidestep the issue of logic fragments, we base SRM on the
motivating question B.

The 1974 ICM paper
https://www.mathunion.org/fileadmin/ICM/Proceedings/ICM1974.1/ICM1974.1.ocr.pdf
very explicitly states the main theme of RM inthis way on page 235:

I. When the theorem is proved from the right axioms, the axioms can be
proved from the theorem.

And already in this paper there are quite a number of reversals.
Whereas one can question what "right" axioms means, the idea is
crystal clear. And this was before I started calling RM by the name RM
and pretty much everybody thinking about RM immediately took that cue.

Looking at the JSL abstracts, where RCA0, WKL0, ACA0, ATR0, Pi11-CA0
are put forth, along with some theories of hyperarithmetic analysis
and some systems featuring mathematical assertions for reversals, we
see that the axiomatizations are really at least nearly strict. In
particular I define a version ETF (elementary theory of functions)
with four sorts, numbers, 1-ary, 2-ary, 3-ary functions. Variables
over each sort, constant 0, unary successor, = between numerical
terms, usual connectives and quantifiers over all four sorts. Axioms
for ETF are from there:

1. Successor axioms.
2. Initial functions.
3. Composition.
4. Primitive recursion.
5. Permutation. Every permutation has an inverse.
6. Atomic induction.

Note that 1-6 are totally motivated by the SRM idea, and 1-6 are
actually fairly close to what SRM is after. The main criticism lies
against 4. The idea of defining functions by recursion along N is
certainly fundamental to an enormous body of mathematics. However, it
appears in the ordinary mathematical literature in somewhat
specialized forms like iteration of nice functions. Or it is used in
the construction of fixed points. A sign that Primitive Recursion
unrestricted should be cut back for an ideal SRM advance is that the
growth rates for primitive recursion are truly staggering, whereas the
growth rates inherent in the vast bulk of mathematics are very limited
(say iterated exponential). So for SRM 1-6 is quite meritorious but
probably can be substantially perfected with some new ideas. The idea
of SRM research is to find weaker and weaker principles that are in
undisputed constant use in more and more mathematics.

NOTE: Even a crude form of bounded primitive recursion will make ETF
equivalent with RCA0 because of the power of Permutation.But even
bounded primitive recursion is subject to criticism.

What seems quite dubious is to give an SRM like axiom system
equivalent to the usual RCA0 which uses just natural numbers and sets
of natural numbers. Of course you can add sets to ETF with
extensionality and say that sets are the zero sets of unary functions.

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

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

900: Ultra Convergence/2  10/3/21 12:35AM
901: Remarks on Reverse Mathematics/6  10/4/21 5:55AM
902: Mathematical L and OD/RM  10/7/21  5:13AM
903: Foundations of Large Cardinals/1  10/12/21 12:58AM
904: Foundations of Large Cardinals/2  10/13/21 3:17PM
905: Foundations of Large Cardinals/3  10/13/21 3:17PM
906: Foundations of Large Cardinals/4  10/13/21  3:17PM
907: Base Theory Proposals for Third Order RM/1  10/13/21 10:22PM
908: Base Theory Proposals for Third Order RM/2  10/17/21 3:15PM
909: Base Theory Proposals for Third Order RM/3  10/17/21 3:25PM
910: Base Theory Proposals for Third Order RM/4  10/17/21 3:36PM
911: Ultra Convergence/3  1017/21  4:33PM

Harvey Friedman