917: Proof Theory of Arithmetic/1

Wed Dec 8 19:43:20 EST 2021

We now believe that with regard to almost ANY arithmetic theorem in
the Actual Math Literature, there are very interesting, productive,
deep, rich challenges awaiting mathematical logicians regarding their
status.

1. REGARDING THEOREMS OF PFA = polynomial function arithmetic =
bounded arithmetic = ISigma0 = I Delta0.

We ask about the prefix complexity of the formulas to which induction
is applied in order to prove the theorem. We allow bounded quantifiers
to be of the form (therexists n < t), (forall n < t), where t is a
polynomial term.

Thus we have delta0 at the lowest level here which is just open.
Then Sigma1, and Pi1.
Then Sigma2, and Pi2.
and so forth.

Lower bounds seem very difficult so one will be focusing on upper
bounds. Presumably, altered proofs with new ideas are needed to reduce
the complexity of the inductions needed.

Yet finer studies seem interesting, taking into account the degrees of
the polynomial terms.

There is an enormous supply of theorems in the literature provable in
PFA. A considerable amount of Diophantine theory is provable in PFA.

But what about finite combinatorics of various kinds? Like finite graph theory?

So that, it seems sensible to look at theories of integers and finite
sets of integers. Then finite graph theory fits in nicely and similar
investigations seem to make sense.

2. REGARDING Pi02 THEOREMS OF EFA THAT ARE OR PROBABLY ARE NOT THEOREMS OF PFA

The most  famous open problem of this kind is

QUESTION. Is (forall n)(therexists m > n)(m is prime) provable in PFA?

It is well known that (forall n)(therexists m > n)(m is prime) is
provable in PFA + (forall n)(n^log(n) exists), with its standard
formalization.

So what line of investigation is appropriate with regard to an
arithmetic theorem provable in EFA?

First of all, you can ask if the theorem is provable in PFA. And you
also ask if the theorem reverses to EFA over PFA. Here is a result of
that kind that I have been using in connection with SRM = strict
reverse mathematics.

Every 1,...,n has a positive common multiple.

This is provably equivalent to EFA over PFA.

But is there more to say in a situation like this?

Yes, definitely. We can try to get clear estimates on the witness
function. In this case, the witness function is going to grow faster
than exponential, and slower than double exponential. And I would
assume that the number theorists have a good handle on where these
lies in between. If we use some good estimate F(n) for the least
common multiple of 1,...,n then presumably

Every 1,...,n has a positive common multiple if and only if (forall
n)(F(n) exists)

is provable in PFA. Or even we should have the stronger result, that

1,...,n has a positive common multiple if and only if F(n) exists

is provable in PFA.

3. REGARDING Pi01 THEOREMS OF EFA THAT MAY OR MAY NOT BE PROVABLE IN PFA

We can't be talking about the usual witness function like we can, and
we did in the previous section. But we also saw the hint of how we can
get around this need for witness functions.

In fact, here is some theory.

As in this theory, we are going to take PFA = bounded arithmetic =
ISigma0 as the base, we take Pi01 sentences to mean sentences in the
ordered ring language of the form

Let's be more specific about what a Pi01 sentence is for our purposes.
Officially,

(forall n1,...,nk)(R(n1,...,nk))

where R uses bounded quantifiers. Here the bounded quantifiers are
bounded by terms in the ring. For convenience, we assume that the
multiple universal quantifiers are consolidated into a single
universal quantifier. This is particularly simple, as

(forall n1,...,nk)(R(n1,...,nk)) iff (forall m)((forall n1,...,nk <
m)(R(n1,...,nk))).

THEOREM 1. Let (forall n)(R(n)) be a Pi01 sentence. The following are
equivalent.
i. There exists k >= 0 such that the following is provable in PFA. "If
2^2^...^2^n exists then R(n)", where there are k 2's.
ii. EFA proves (forall n)(phi(n)).

DEFINITION 1. Let phi be a Pi01 sentence. #(phi) is the least k such
that PFA proves ."If 2^2^...^2^n exists then R(n)", where there are k
2's. If there is no such k, then #(phi) = infinity.

How do we know that we get a real hierarchy here of Pi01 sentences phi?

#(phi) = 0  this just means that phi is provable in PFA
#(phi) = 1
#(phi) = 2
...
#(phi) = infinity   this ust means that phi is not provable in EFA

DEFINITION 2. Con(PFA)/n is the sentence that PFA has no contradiction
in a Gentzen system using prenex formulas with bounded quantifiers
driven in, with quantifier complexity at most n.

THEOREM 2. Let n >= 1.
i. Con(PFA)/n is a Pi01 sentence provable in EFA.
ii. PFA + Con(PFA)/n+1 proves the cut free consistency of PFA +
Con(PFA)/n, in the following sense. Put the axioms in prenex form with
the bounded quantifiers pushed inside. There are no cuts.
iii. Con(PFA)/n+1 is not provable in PFA + Con(PFA/) by G2 for cut
free consistency proofs.

So we do have a hierarchy of Pi01 sentences provable in EFA. Namely

Con(PFA)/0
Con(PFA)/1
Con(PFA)/2

4. EXTENSION OF THE HIERARCHY OF Pi01 SENTENCES PROVABLE IN EFA TO PA AND BEYOND

Let (forall n)(R(n)) be a Pi01 sentence provable in PA. Then likewise,
there exists alpha < epsilon_0 such that

F_alpha(n) exists implies R(n)

is provable in EFA.

This defines a hierarchy of Pi01 sentences. And obviously this extends
to higher proof theoretic ordinals in a nice way. More about this in
later postings.
...
5. INVESTIGATIONS INTO SPECIFIC IMPORTANT ARITHMETIC THEOREMS FROM THE
LITERATURE PROVABLE IN EFA

We will take this up in the next posting on this topic.

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

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 917th 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  10/18/21 7:22PM
913: Base Theory Proposals for Third Order RM/6  10/18/21 7:23PM
914: Base Theory Proposals for Third Order RM/7  10/20/21 12:39PM
915: Base Theory Proposals for Third Order RM/8  10/20/21 7:48PM
916: Tangible Incompleteness and Clique Construction/1

Harvey Friedman