919: Proof Theory of Arithmetic/2

[Harvey Friedman]

PRINCIPAL THESIS. FOR EVERY THEOREM IN THE MATHEMATICAL LITERATURE,
THERE ARE METAMATHEMATICAL INVESTIGATIONS AS TO THE NATURE OF THEIR
PROOFS AND ALL POSSIBLE PROOFS, WHICH POSE MAJOR CHALLENGES FOR
MATHEMATICAL LOGICIANS AND WHICH WILL GENERALLY REQUIRE THE
EXPLOITATION OF EXISTING METHODS OF SUBSTANTIAL DEPTH OR THE INVENTION
OF NEW METHODS WITH SIGNIFICANT APPLICABILITY.

In this series of postings, I want to flesh out just what I have in
mind in the arena of FORMAL ARITHMETIC. This just means the language
of PA and some extensions thereof. We want to consider only statements
naturally formulated in this language. So this would NOT include say
finite graph theory. Because a finite graph is naturally a finite
second order object. Of course we do coding of finite sets into Formal
Arithmetics, but that is not strictly mathematical. A separate series
of postings about what this principal thesis means in integers and
relations on integers combined is planned.

In particular, all of the theorems of formal arithmetic in RCA0, or
equivalently, in PRA, have escaped the usual RM based on RCA0. That is
actually a very large amount of major mathematics. A major amount has
proofs in the literature well within PRA, and even that crowning jewel
FLT is believed to be provable in PRA, and even in EFA.

Before we start taking specific theorems of arithmetic, we first map
out some obviously significant fragments of formal arithmetic.

A basic reference is

[HP93] P. Hajek and Pavel Pudlak, Metamathematics of First-Order
Arithmetic, Perspectives in Mathematical Logic, 1993, Springer.

     1. THE THEORY Q

There is a question of how low to go with this systematic
investigation..We will use the system Q as presented in [HP93] in
0,S,+,dot,<=.

not(S(n) t= 0).
S(n) = S(m) implies n = m.
not(n = 0) implies (therexists y)(x = S(y)).
n+0 = n, n+S(m) = S(n+m).
n dot 0 = 0, n dot S(m) = n dot m + n.
n <= m iff (therexists r)(r+n = m).

Obviously the last axiom is purely definitional. That is because Q is
primarily used as the core axioms of stronger systems which do use <=.
But sometimes it is advantageous to have <= or < as primitives in the
stronger systems, with the recursive definition not(n < 0) and n <
S(m) iff n < m or n = m.

Q is very important in its own right as a principal representative of
an equivalent class under interpretability. Q has surprising
interpretation powers, interpreting bounded arithmetic and RCF. It's
interpretation level seems to be rather canonical in ways that we do
not yet understand.

[Je16] E. Jerabek, Division by zero, Archive for Mathematical Logic 55
(2016), no. 7, pp. 997–1013.

[Ot90] M. Otero, On Diophantine equations solvable in models of open
induction, Journal of Symbolic Logic 55 (1990), no. 2, pp. 779–786.

[Je16] gives a decision procedure for the provable Diophantine
sentences of Q. It also gives partial decidability results for the
provable universal sentences of Q.

[Ot90] discusses the provable Diophantine sentences of I(open). For
I(open), see the next section.

     2. THE THEORY I(open)

I(open) is Q together with induction for all quantifier free (open)
formulas in the language of Q.

I(open) proves a small amount of arithmetic, most notably the quotient
remainder theorem and that the function (n+m)(n+m+1)/2 + n is a
bijection from N2 onto N.

[HP93] starts off with Q as above, and then briefly works with I(open)
before going on to very extensive developments of bounded arithmetic =
PFA = ISigma0 = IDelta0 and beyond.

We looked at the [HP93] development of I(open) and it appears that all
of the uses of I(open) there are using very special open formulas.
Namely equations, negated equations, and s <= t. In other words, what
we call I(lit), where lit stands for literal. It is common to use the
word literal for atomic formulas and negated atomic formulas.

So given this observation, it makes sense to rethink questions for
I(open) also for I(lit). And also even I(=), I(<=), I(not =). It is
not so clear what the relationships are among these fragments of
I(open).

Models of I(open) are of an algebraic character (discrete subrings of
real closed fields) and have recursive models. See [Sh64.65] and
[BO96].

I(open) seems to be on the border between algebra and math logic.

[Sh64] J.C., Shepherdson, A nonstandard model for a free variable
fragment of number theory, Bulletin de l’académie Polonaise des
sciences, 12 (1964), 79–86.

[Sh65] J.C. Shepherdson, Nonstandard models for fragments of number
theory, in: Theory of Models, North-Holland, Amsterdam, 1965, pp. 342
- 358.

[Wi78] A. Wilkie, Some results and problems on weak systems of
arithmetic,In: Logic Colloquium '77,  Proc. Wroclaw 1977, Sstud. Logic
Found. Math. vol. 96, 1978, pp. 285-298.

[Dr80] L. van den Dries, Some model theory and number theory for
models of weak systems of arithmetic, in: Model Theory of Algebra and
Arithmetic, (Lect. Notes in Math. 834), Springer-Verlag, 1980 pp.
346-362.

[Ad86] Z. Adamowicz, Some results on open and Diophantine induction,
in: Logic Colloquium '84, North-Holland, 1986, pp. 1-20.

[Ad87] Z. Adamowicz, Open induction and true theory of rationals, JSL
vol. 52 1987 pp. 793-801.

[BO96] Berarducci A., Otero M., A recursive nonstandard model of
normal open induction, J. of Symbolic Logic, 61 (1996), no. 4,
1228–1241.

[BKK08] Biljakovic D., Kochetov M., Kuhlmann S., Primes and
irreducibles in truncation integer parts of real closed fields, in:
Logic, Algebra and Arithmetic, Lecture Notes in Logic, 26, Association
for Symbolic Logic, AK Peters, 42–65 (2006).

[MM89] Macintyre A., Marker D., Primes and their residue rings in
models of open induction, Annals of Pure and Applied Logic 43 (1989),
no. 1, 57-77.

[MR93] Mourgues M.H., Ressayre J.P., Every real closed field has an
integer part, J. of Symbolic Logic 58 (1993), no. 2, 641–647.

The following are from [HP93]. They prove them in I(open). Actually
quite a number of these are already proved there in I(=). These are
1,2,3,4,5 without (much) thought.

1.. Addition is commutative.
2. Addition is associative.
3. Multiplication is commutative.
4. Multiplication is associative.
5. Distributive Law.
6. x+y = x+z implies y = z.
7. <= is connected.
8. x <= y and y <= x implies x = y.
9. <= is transitive.
10. x <= y iff x+z <= y+z.
11. not(z = 0) and x dot z = y dot z implies x = y
12. not(z = 0) implies (x <= y iff x dot z <= y dot z).

For 6? Not clear. A try is to assume y not= z and try to prove by
induction on x that x+y not= x+z. Want x+y not= x+z implies S(x)+y
not= S(x)+z. That we do have, with the help of 1. But we didn't just
use I(=)  for this. We used I(=,not=)). So this suggests breaking down
I(open) into fragments, and even breaking down I(lit) into fragments.
.

[HP93] continues with the Quotient Remainder Theorem and the one-one
surjectivity of r = (n+m)(n+m+1)/2 + n. Both of these are proved in
I(lit).

I(open) does not go very far into arithmetic. It is not known if the
Diophantine sentences provable in I(open) is decidable. We raise this
same question for those fragments of I(open) including I(lit) and its
five obvious fragments..

This leads to the following questions.

1. I(lit) should be weaker than I(open)? What are the relationships
between the five obvious fragments of I(lit)?

2. What are some interesting theorems that are provable in I(open) but
not in I(lit)?

3. Are there interesting theorems of I(open) that prove significant
parts of I(open) over I(lit)?

4. Are there interesting theorems that are equivalent to I(lit) over Q?

5. Is there a precise way of saying that I(open) cannot prove any
interesting information about primes? Or at least a very strong
theorem to that effect?

There are obviously many variants of these kinds of questions. I(open)
is known to have some serious algebraic flavor of a kind that PFA
surely does not.

>From [MM89] and earlier we see that "infinitely many primes" and
"quadratic nonresidues of odd primes" are not provable in I(open). Not
even "every integer > 1 is divisible by a prime" and not even "any two
positive integers have a gcd" and not even "2 has no square root".

So it appears that I(open) is not really strong enough to prove
anything interesting about prime numbers and nothing interesting about
a lot of matters. It would be interesting to have some simple strong
results to reflect this weakness in a principled way.

     3.  PFA = polynomial function arithmetic = bounded arithmetic =
ISigma0 = IDelta0

PFA was introduced in

[Pa72] R. Parikh, Existence and feasibility in arithmetic, Journal of
Symbolic Logic, 36 (1971), pp. 494–508.

Here we know that nonstandard models cannot be recursive,

In the next posting we will create a large list of fundamental
theorems of arithmetic that are provable in PFA (and generally not in
I(open)). Then we will try to make good on our basic theme that every
one of these theorems

To whet our appetite, here are a few from [HP93], provable in PFA but
not in I(open)::

1. gcd of two nonzero positive integers exist.
2. gcd(n,m) = 1 implies there exists a,b such that an-bm = 1 or bn-am = 1.
3. gcd(n,m) = 1 implies (forall r)(m|nr implies m|r).
4. n > 1 implies some prime divides n.
5. If a prime divides a product it divides at least one of the factors.

Here is another paper on PFA.

[WP87] A. Wilkie and J. Paris, On the scheme of induction for bounded
arithmetic formulas, Annals of Pure and Applied Logic 35 (1987)
261-302

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

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 918th 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  12/8/21   7:25PM
917: Proof Theory of Arithmetic/1  12/8/21  7:43PM
918: Tangible Incompleteness and Clique Construction/1

Harvey Friedman