915: Base Theory Proposals for Third Order RM/8

Wed Oct 20 19:48:29 EDT 2021

*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 - #5
6. Strict Reverse Math Research - #6
7. Strict Reverse Math Research/more - #7
8. More History of RM and ICM paper - here
9. The Two Founding JSL Abstracts - #9

MORE HISTORY OF RM AND RCA0

We go into more depth about early history of RM and in particular the
emergence of RCA0 than we did in the previous posting #913.

For some perspectives from a leading recursion theorist see, e.g.,
REVERSE MATHEMATICS: THE PLAYGROUND OF LOGIC Author(s): RICHARD A. SHORE
Source: The Bulletin of Symbolic Logic , SEPTEMBER 2010, Vol. 16, No.
3 (SEPTEMBER 2010), pp. 378-402
Published by: Association for Symbolic Logic

Most frequently cited for the invention/discovery of RM are two
publications. First  the 1974 ICM paper
https://www.mathunion.org/fileadmin/ICM/Proceedings/ICM1974.1/ICM1974.1.ocr.pdf
Lecture given in August 1974, Proceedings  appeared in 1975.

which explicitly states the main theme of RM in this way on page 235:

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

And the two ASL abstracts

[Fr76] Subsystems of Second Order Arithmetic with Restricted Induction
I,II, abstracts, J. of Symbolic Logic, Vol. 1, No. 2 (1976), pp.
557-559.

Links to both ICM paper and [Fr76] above are now on my Downloadable
Manuscripts page

I mentioned the unpublished early RM manscripts on my website at
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
which include

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

My RM was brewing for many years before the August 1974 lecture date,
as can be seen by the following statement in the first of those four
TEXTS  manuscripts:

"1. In 1969, I discovered that a certain subsystem of second order
arithmetic based on a *mathematical* statement (that every perfect
tree which does not have at most countably many paths, has a perfect
subtree), was provably equivalent to a *logical picnicpal* (the weak
Pi11 axiom of choice) modulo a weak base theory (comprehension for
arithmetic formulae)."

I don't have documents for this but this is what i wrote there. The
words within the asterisks shown are actually underlined in the
manuscript. This clearly indicates that a clear conception of RM based
on the base theory ACA was clearly on my mind as early as 1969. As I
said earlier, the base theory clearly indicates the kind of
mathematics targeted, and is critical in the crucial distinction
between RM and the cited cases of Reverse Mathematics with base
theories ZF and formalized Absolute Geometry (first and second order).
Actually RM based on the base theory ACA - rather than the commonly
accepted RCA0 - is already quite a significant enterprise with plenty
of rich phenomena. I was doing this with some frequency since 1969 and
in my characteristic way, especially when I was young, I would tell
everybody everywhere about everything that I do, and routinely mention
them in correspondence. So I would think it likely that there is some
documentary evidence for this very old development. It has been only
gradual that I learned how tough the world can be on attributions, and
maybe the level of trust I placed in some people was upon reflection
rather naive.

Z2 is generally credited to Hilbert and Bernays. Depending on
recollections of interaction with Feferman and Kreisel when I was at
Stanford, without looking at their papers, I think the systems RCA,
ACA, Pi11-CA, as well as many other systems with full induction like
Delta11-CA, Sigma11-AC, Sigma11-DC, and many others, are due to them.
But not WKL and ATR. Although Feferman's IR has an ATR *rule* as a
principal component.

THE 1974 ICM PAPER

Here is the overall structure of the 1974 ICM paper.

0. Introduction with two principal themes stated explicitly, the first
being the RM theme, we discussed earlier.

"When the theorem is proved from the irght axioms, the axioms can be
proved from the theorem."

1. Axioms for arithmetic sets. Here RCA, WKL, ACA are discussed, the
first and third being I think due to Kreisel and Feferman. RCA is
stated with Delta01 comprehension and full induction. ACA is stated
with arithmetic comprehension and full induction. WKL is stated with
"every infinite 0,1 finite sequence tree has an infinite path" and
full induction. KL is also considered where 0,1 is dropped. The
following reversals are given:

KL
SHB (sequential Heine Borel).
SLUB (sequential least upper bound)
MLUB (monotone least upper bound).
SBW (sequential Bolzano Weierstrass)

Reversal of all five above over ACA is claimed, except for SHB. The
reversal of SHB to WKL over RCA is claimed. Also reversals of several
logical statements about propositional predicate calculus to WKL over
RCA0 are claimed.

Conservation of WKL over RCA is stated for all sentences starting with
universal set quantifiers followed by anything arithmetical.. I
definitely had in mind the following argument using Scott systems..
Let M be a countable model of RCA. We define within M a complete
diagram W for a countable nonstandard model of EFA in a delta-0-2
fashion with the help of induction in M. Then we can define the Scott
system of M and get a model of WKL with the same arithmetic part. This
will show conservation for arithmetic sentences. To handle the
universal set quantifier, we first assume in M that we have a set X
without the arithmetic property in question; We repeat the argument
but making sure that the nonstandard complete diagram W incorporates X
(many convenient ways to do that).

So the ICM paper starts off with the first three of the "big five" but
with full induction.

2. Axioms for hyperarithmetic sets. My idea was to move to systems
reflecting relative arithmeticity to systems reflecting relative
hyperarithmeticity. I introduce HCA, HAC, HDC, which are the Feferman
Kriesel systems Delta11-CA, Sigma11-AC, Sigma11-DC with full
induction. Then I give two mathematical statements ABW (arithmetic
Bolzano Weierstrass) and SL (sequential limit system). I claim the
second reverses to HAC over RCA, and claim the first is proved in HAC.

For a long time this level of RM, which is off the levels of the "big
five", was virtually inactive. It is now become active and these
subsequent developments vindicates my including this level in the ICM
paper. See https://math.berkeley.edu/~antonio/slides/kyotoh.pdf
https://people.math.wisc.edu/~jgoh/files/goh_irt_slides.pdf
https://pi.math.cornell.edu/~shore/papers/pdf/ATHA32.pdf
https://www.worldscientific.com/doi/10.1142/S0219061306000517

And two papers of Chris Conidis et al:
Comparing theorems of hyperarithmetic analysis with the arithmetic
Bolzano-Weierstrass theorem.
Transactions of the American Mathematical Society, vol. 364(9) 4465–4494 (2012).
Galvin’s “Racing Pawns” game, internal hyperarithmetic comprehension,
and the law of the excluded middle. (with N. Greenberg and D.
Turetsky)
Notre Dame Journal of Formal Logic, 54(2) 233–252 (2013).

3. Axioms for arithmetic recursion. I present ATR, weak Pi11-AC, and
then three reversals. CWO for comparability of well orderings, PST for
perfect subtree theorem, and CS for countability of discrete sets. I
claimed that all of these are provably equivalent over RCA. I claimed
that ATR proves HAC but not HDC, and this was proved in my PhD Thesis.
ATR is the fourth of the big five systems with full induction.

4. Axioms for transfinite induction. TI is RCA together with
transfinite induction on all well orderings. It is more commonly
referred to as BI and is probably due to Kreisel with his analysis of
Spector's famous paper on bar recursive functionals. TI does not fit
so nicely in the big five picture. However, there is an important
fragment of TI which is TI for Pi12 formulas, which according to
Rathen and Weiermann, is provably equivalent to KT with well quasi
ordered labels. See their paper, Proof-theoretic investigations on
Kruskal's theorem, Annals of Pure and Applied Logic, Volume 60, Issue
1, 24 February 1993, Pages 49-88

It would seem likely that each of the TI restricted to Pi1n formulas
should have interesting reversals, n >= 3.

I also introduce RFN, a reflection principle, that says that any
second order property that holds of certain sets holds in some
countable omega structure of those given sets. I claim that RFN and TI
are equivalent over RCA.

5. Axioms for the hyperump. I present Pi11-CA which is the Pi11
comprehension axiom scheme on top of RCA. This system is due to
Feferman and Kreisel. I claim two equivalents over RCA, one for the
perfect kernel theorem for trees of finite sequences of natural
numbers, and the arithmetic least upper bound principle.This is the
fifth of the big five with full induction.

I finish the paper by referring to work on restricting induction
pointing to the two JSL abstracts which can conveniently be obtained
from item 1 in my Downloadable Manuscripts
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
In the next posting we discuss these two abstracts in some detail.

In summary, the ICM presents and discusses some major reversals in the
setting of the big five with full induction: RCA, WKL, ACA, ATR,
Pi11-CA.

It also discusses some key systems with limited reversals strictly
between ACA and ATR: HCA, HAC, HDC.This hyperarithmetic level has
proved to be increasingly important in recent years for RM.

It also discusses TI, a system strictly between ATR and Pi11-CA with
an equivalent RFN (reflection). A fragment of this, also strictly
between, has proved to be important for RM in connection with the full
Kruskal Theorem.

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

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 915th 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
912: Base Theory Proposals for Third Order RM/5
913: Base Theory Proposals for Third Order RM/6
914: Base Theory Proposals for Third Order RM/7