[FOM] Strict RM/Reverse Number Theory

[Harvey Friedman]

Reply to Simpson Reverse Number Theory 5:17PM 5/14/03.

I want to clarify the relationship between what Simpson says here and 
my postings on Strict Reverse Mathematics:

175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM

>I would like to call attention to some work by a group of Europeans
>over a number of years, in an area which I propose to call Reverse
>Number Theory.  They investigate which theorems of elementary Number
>Theory require exponentiation.  One of the papers is by Paola
>D'Aquino, in Annals of Pure and Applied Logic, 1996.  She shows that
>EXP is equivalent over a certain system of Bounded Arithmetic, IE_1 if
>it matters, to the statement
>
>    Every Pell equation has a nontrivial solution in integers.
>
>A Pell equation is a Diophantine equation of the form x^2 - d y^2 = 1,
>where d is a positive integer which is not a square.  The trivial
>solutions are x = 1, - 1, y = 0.  This existence of nontrivial
solutions is a standard result in Number Theory textbooks.

A. ABOUT POSTING 175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM

This work Simpson is referring to is explicitly discussed in my posting #175.

in section 4 there, which is entitled  "4. COMPARISON WITH D'AQUINO."

In particular, I discussed the systems

1. DOR.
2. PELL. Every Pell equation has a nontrivial solution.
3. BDI. Bounded Diophantine Induction.

1. DOR.
2. PELL.
3'. The values of every quadratic in any number of variables, with 
variables restricted to finite intervals, contains a maximum interval 
about 0.

In particular, I mentioned that D'Aquino shows that the first system 
is equivalent to IDelta0(Z) + EXP. The system IE_1 that D'Aquino uses 
corresponds exactly to DOR + BOI.

I proved that the second system is equivalent to IDelta0(Z) + EXP.

A main point of posting #175 is that the base theory

IE_1

is replaced by the mathematical statement 3' involving quadratics 
only, which is well known to be a rather tame and importantly 
productive area of number theory, as opposed to general integral 
polynomials.

Simpson says above

"...EXP is equivalent over a certain system of Bounded arithmetic, 
IE_1 IF IT MATTERS, to the statement"

The capitals there are mine.

The essential point of Strict Reverse Mathematics is that it matters 
CRUCIALLY just what the base theory is. In fact, the essential point 
of Strict Reverse Mathematics is there is to be ABSOLUTELY NO base 
theory.

 From this point of view, a scheme like IE_1 is undesirable. In fact, 
any scheme whatsoever is undesirable. This criterion applies to the 
second system as well, since 3' is also a scheme.

So we raised the question of whether we can bound the number of 
variables needed in 3' to something mathematically palatable. We also 
raised a number of other open questions in #175.

We stated in #175 that we can restrict to five variables for this system:

1. DOR.
2. CM. (axiom of common multiples).
3. The values of every quadratic in at most 5 variables, with 
variables restricted to finite intervals, contains a maximum interval 
about 0.

Here CM asserts "for all n, the numbers 1,...,n have a positive 
common multiple". This is a fundamental mathematical fact that is 
logically implied in any context in which the factorial sign appears.

The above system is also equivalent to IDelta0(Z) + EXP.

In particular, we raised the question of whether in 1-3 above, CM can 
be replaced by PELL.

In fact, a basic piece of useful metamathematics is this:

CM and EXP are equivalent over IDelta_0(Z).

B. THE FOUNDATIONAL MOTIVATION BEHIND STRICT REVERSE MATHEMATICS.

As discussed in posting #175, section 1, entitled HILBERT'S PROGRAM 
REVISITED, there is an issue as to whether one can get any logical 
strength at all using just what mathematicians assert, without 
writing down axiom schemes that they use. The significance of this is 
that the mathematicians can argue that they only use certain NATURAL 
instances of these axiom schemes, and that the logicians always work 
with ARBITRARY. There may be a way of cleverly cutting down what 
mathematicians actually use in order to get around having any logical 
strength.

So this is why Strict Reverse Mathematics is intended to be done, 
ideally, with no trace of any kind of base theory, and in fact, where 
one only lists finitely many icons from the mathematical literature.

C. THE MOVE AWAY FROM JUST THE LANGUAGE OF ORDERED RINGS.

In the subsequent postings

177:Strict Reverse Mathematics 1  6/10/03  8:27PM
181:Strict Reverse Mathematics 2:06/19/03  2:06AM

I move away from just the language of ordered rings, augmenting it 
with variables over finite sequences of integers. What I do with 
finite sequences of integers is really EXTREMELY elemental and easily 
matched to the mathematical literature.

Nevertheless, in support of the approach in #175, it turns out that 
the study of the structure of the ranges of quadratics with integer 
coefficients is the subject of intensive investigation by 
professional number theorists. These ranges are very recursive, but 
very delicate. So my maximality principle for quadratics is likely to 
be extractable from the number theory literature, if not now, in the 
relatively near future.

However, the move to finite sequences of integers is probably 
inevitable, anyways, since it is needed to move along the road to 
developing the strict reverse mathematics of diverse areas of 
mathematics; in particular, combinatorics and real analysis.

In posting #181, I gave a very careful axiomatization, DORISE, using 
integers and infinite sequences of integers. The standards of Strict 
Reverse Mathematics are met.

Finite sequences there are handled in terms of truncation. This 
system, DORISE, corresponds to Simpson's RCA0*. I then also recovered 
RCA0 and ACA0, by obvious additional axioms.

I plan to return to the development of Strict Reverse Mathematics in 
due course.

One of many goals of Strict Reverse Mathematics is to give a strictly 
mathematical system which is mutually interpretable with large 
cardinals. I know how to do this using Boolean Relation Theory. This 
will be discussed in detail later.

Harvey Friedman