913: Base Theory Proposals for Third Order RM/6

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

6. STRICT REVERSE MATH RESEARCH/more

There is one publication in Strict Reverse Mathematics:

[1] On the Inevitability of Logical Strength, The Inevitability of
Logical Strength: strict reverse mathematics,
Logic Colloquium ’06, ASL, ed. Cooper, Geuvers, Pillay, Vaananen,
2009, 373 pages, Cambridge University Press, pp. 135-183.
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
358

For the highest standards, I rejected the idea of using primitive
recursion for the reasons stated in the previous posting. An explicit
bounded primitive recursion is also not nearly mathematical enough.

I want to critically examine what I did in [1], but first to wet
appetities here, I'll move to a totally unproblematic context.

Here is a list of theorems from elementary number theory whose
statements are particularly clean. They are first order in the
language of the integers as a discrete ordered ring.

1. The discrete ordered ring axioms.
2. Euclidean division.
3. If n is not the k-th power of an integer then n is not the k-th
power of a rational. This is a scheme over k.
4. For all positive a,b, gcd(a,b) is the least positive integer of the
form ax + by.
5. Fermat's Last Theorem as a scheme in each exponent > 2.
6. Every n >= 2 is divisible by a prime.
7. If a prime divides a product then it divides one of the factors.
8. For some integer N <= 246, there are infinitely many pairs of
primes that differ by N.
9. There are arbitrarily long arithmetic progressions consisting
entirely of primes.
10. For every n > 1 there is a prime in (n,2n).
11. If the terms of an infinite arithmetic progression have no common
divisor > 1 then it has infinitely many primes.
12. If p and q are odd primes, then:
((p is a quadratic residue mod q) if and only if (q is a quadratic
residue mod p)) if and only if (at least one of p and q is congruent
to 1 mod 4).
13. Every nonnegative integer is the sum of four squares.
14. Every odd number greater than 5 is the sum of three primes.
15. There is a polynomial with integer coefficients in 26 nonnegative
integer variables of degree 25 whose set of positive values is exactly
the prime numbers.
16. Every positive range of every polynomisl with integer coefficients
and nonnegative integer variables is the positive range of some
polynomails with 24 integer variables of degree 26.

QUESTION 1. Which of these sixteen theorems are provable in EFA? What
fragments of EFA suffice?

QUESTION 2. Is EFA interpretable in the conunction of all 16 of these theorems?

We now turn to [1] where I was able to derive EFA.

The signature of FSTZ is L(Z,fst). The nonlogical axioms of FSTZ are
stated informally as follows.

See section 7, seven strictly mathematical theories, page 28, in [1].

The signature of FSZ is the ordered ring language for first order, and
FINITE sets of first order objects for the second order, with epsilon
and cardinality (for full details see paper)..

1. Linearly ordered integral domain axioms.
2. Finite interval. [x,y] exists.
3. Boolean difference. A\B = {x in A: x not in B} exists.
4. Set addition. A+B = {x: x+y: x in A and y in B} exists.
5. Set multiplication. A⋅B = {x: x⋅y: x in A and x in B} exists.
6. Least element. Every nonempty set has a least element.

Because we are in Z and not N, axiom 6 has the effect of telling us
that every set is internally finite.

The signature of FSQZ is the ordered ring language for first order,
and FINITE sequences of first order objects for the second order, with
length and term extraction (for full details see paper). s.

1. Linearly ordered integral domain axioms.
2. lth(a) ≥ 0.
3. val(a,n) defined then 1 <= n <= lth(a).
4. The finite sequence (0,...,n) exists.
5. lth(a) = lth(b) implies -a,a+b,a⋅b exist.
6. The concatenation of a,b exists.
7. For all n ≥ 1, the concatenation of a, n times, exists.
8. There is a finite sequence enumerating the terms of a that are not
terms of b.
9. Every nonempty finite sequence has a least term.

In [1], we establish the crucial fact that FSZ proves bounded
induction in its language, and FSQZ proves bounded induction in its
language. This succeeds in opening up Pandora's Box.

But we don't have any exponentiation. Of course we then added
exponentiation to both these systems. And then we want to get a
conservative extension of EFA over Z. But there is a subtle point. You
can't just dump the usual quantifier free axioms for the exponential
ordered ring on FSZ and FSQZ. In the latter case you really need the
finite geometric sequences. I.e., the finite sequence
(exp(n,0),...,exp(n,m)) exists. Now in FSZ it is not enough to have
just the finite set {exp(n,0)+0,exp(n,1),...,exp(n,m)} exists. You
need to have the finite set The finite set
{exp(n,0)+0,exp(n,1)+1,...,exp(n,m)+m} exists.

Then FSZ and FSQZ so extended with exponentiation is a conservative
extension of EFA (for N and Z respectively).

A tiny quibble about axiom 7 above. It is almost perfect but it is
used really in algebraic systems where we write x^n - say in groups,
semigroups, rings, fields, etc. And finite sequences generally are
very much part of that algebraic culture through finite words. So
there is the idea of having some more algebraic based system that
might be yet more striking than FSQZ.

What is beginning to emerge is just what SRM research might look like.
I knew what RM research was going to look like when I set it up.
Namely pick any theorem of a certain fairly broad style, with some non
effectiveness going on. The theorem needs to be essentially countable,
and in my present day language, if it involves sets and functions on
Polish spaces, then it is teated with a countable presentation. Then
one is likely to be able to get reversals using recursion theoretic
techniques tempered with axiomatic sensibilities. Theorems of this
kind treated in this way should lead to a relatively small number of
equivalence classes under provable equivalence. Decades later, because
of the zoos that have been discovered, there are more equivalence
classes than perhaps was expected, but the number is still small
relative to the number of Theorems treated. Also the number of
equivalence classes so generated under mutual interpretability remains
very small despite these zoos. And furthermore, they are in practice
linearly ordered, so we are not seeing zoos under interpretability.

An interesting question is: what is the total number of equivalence
classes under mutual interpretability that we have seen in RM (from
strictly non logic literature theorems)?

But with SRM the situation is much more delicate.: Let us probe more
deeply. There are 2^16 sets of statements from 1-16 above from number
theory. What do they look like under mutual interpretability? We are
not going to get linearity here. But we should look for at least a
little bit of base theory. We should probably always be including 1,2.

I think with SRM we can pick a fairly narrowly focused mathematical
subarea and try to achieve logical strength using fundamental theorems
from that subarea or very close to those.

Also there is the overall program of giving strict mathematical
axiomatizations of major landmark systems like we have done for EFA.
This might be not outright equivalences but rather mutual
interpretations. Here it makes sense to grab what we want from perhaps
multiple areas.

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

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 913th 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/5h