914: Base Theory Proposals for Third Order RM/7

[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 - #5
6. Strict Reverse Math Research - #6
7. Strict Reverse Math Research/more - #7
8. The logical power of Inversion/1 - #8
9. The logical power of Inversion/2 - #9

7. STRICT REVERSE MATH RESEARCH/more

NOTE: I have now decided that my little quibble about the iterated
concatenation axiom of FSQZ is really unfair to me. That is a visually
clear construction of the most familiar kind.

The last two statements in the list of 16 in elementary number theory
involve polynomials with integer coefficients. So they are of a more
advanced character than the previous 14. So some comments are in order
about how we construe them as within the ordered ring primitives. The
polynomial satisfying the existential quantifier is given by an
enormous block of existential quantifiers for the coefficients, where
the evaluation is of course a gigantic equation. The conclusion
involves all polynomials with integer coefficients and for the
purposes at hand, we take that as a scheme, with infinitely many
instances. Of course, for reversals here (very difficult it seems) it
would be most striking not to use them.

I discussed my current way of acheiving logical strength in #913 from
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
where I wrote paper 358 and I meant paper 58. This gets the mutual
interpretability of FSZEXP' and FSQZEXP with EFA. These are FSZ and
FSQZ with exponentiation appropriately incorporated. These are called
FSZEXP' and FSQZEXP.

We can go further with this using the following:

MINIMUM ABSOLUTE VALUE. MAV. Every polynomial with integer
coefficients and integer variables attains a value of least magnitude.

We can take this as a scheme in the number of variables and the degree.

THEOREM 7.1. FSZEXP' + MAV and FSQZEXP + MAV prove Sigma01 induction.
They are mutually interpretable with ISigma1 and RCA0.

An alternative is to define polynomials with integer coefficients and
their action within FSQZEXP. This is quite natural. Namely, we can
define polynomials as certain finite sequences from Z based on how we
actually write polynomials from left to right. Then we can naturally
define evaluation at integer arguments by means of an obvious Sigma01
formula. We don't yet have Sigma01 induction so we don't know if we
are getting functions, but we can still state MAV for all of these
possibly partial polynomials. Or we can alternatively state MAV for
all everywhere defined polynomials. In any case, we still get Sigma01
induction in FSQEXP + MAV because we only need MAV for a specific
number of variables and degree. Yet another route is to introduce
primitives for polynomials with integer coefficients and valuation.In
this route we have total polynomials via the notation, and don't need
any induction principle since we only need a specific number of
variables and degrees.

Further advances in SRM using FSQZEXP can be achieved rather easily
through my finite forms of Kruskal's and Graph Minor Theorems, and
weaker finite forms for PA and fragments. However, to do this
properly, there is the clear need for FINITE SEQUENCES OF FINITE
SEQUENCES FROM Z. This needs to be worked out carefully but poses no
obstacles to the SRM ideal.

Now lets come back to see what we can do in the language of discrete
ordered rings. We call this NUMBER THEORETIC LOGICAL STRENGTH.

Actually I just realized that i had made a great deal of progress on
Number Theoretic Logical Strength already in

24. Quadratic Axioms, January 3, 2000, 9 pages, draft.  QuadAxiom=1%5B1%5D.6.00
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/

Let PQV (positive quadratic values) be the system

1. Axioms for commutative ring with unit.
2. For every a,b,c,d,e,f, the values of axy + bx + cy + d, |x| <= e,
|y| <= f, have a least positive upper bound.
3. For every a,b,c,d,e,f,g,h,i,j,k,m, the values of axy + bzw + cx +
dy + ez + fw + g in [1,h], with |x| <= i, |y| <= j, |z| <= k, |w| <=
m, have a least positive common multiple.

I give a fully detailed proof that this system PQV is equivaelnt to
the formulation of EFA in 0,S,+,dot,<. The proof uses an earlier
version of the result in
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#58 for FTZ that we have been talking about., that FTZ implies bounded
arithmetic.

Note that 2,3 are trivial instances of induction, with 2 proved using
bounded induction, and 3 proved using either Sigma01 induction or
alternatively, bounded induction plus the exponential exists
(formulated in the language of discrete ordered rings).

So  we can look at this PQV result the following way. In the presence
of an exponential situation in the language of discrete ordered rings,
bounded induction is well known to be finitely axiomatizated, so only
finitely many instances of bounded induction give all, and they are
hair raising metamathematical ones. PQV shows we just need very
mathematical instances of these to generate EFA. That basically four
variable quadratics tell the tale.

Can we simplify these quadratics further in PQV? Can we leverage this
work with PQV to involve 1-14 in my 1-16 list of number theoretic
theorems in posting 913?

Coming back to FSZ and FSQZ, we can achieve EFA in their languages
without adding EXP, by using the additional axiom

CM. Each 1,...,n has a common nonzero multiple.

I forgot to mention that in posting #913 (previous posting), but it is
in Corollary 11.12 in paper
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#58

The prospects for major advances in Number Theoretic Logical Strength
look promising.

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

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 914th 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