[FOM] Solution for Buckner?

[Harvey Friedman]

Reply to Buckner 5/3/03 2:40PM.

It is clear from your response that you

1. Accept the meaningfulness of any formula with perhaps several 
quantifiers, as long as the quantifiers range over the natural 
numbers, and the inner core (matrix) of the formula involves only the 
basic arithmetic operations such as, e.g., addition, multiplication, 
and exponentiation.

2. Moreover, accept the meaningfulness of any formula with perhaps 
several quantifiers, some of which range over all natural numbers, 
and some of which range over all finite sets of natural numbers, with 
matrix involving only addition, multiplication, exponentiation, and 
membership of natural numbers in finite sets.

3. In addition, you allow the introduction, by definition, of 
relations among natural numbers, as long as the introduction of such 
relations does not allow one to treat those relations as mathematical 
objects.

Now let me confirm that you accept the following principle:

4. Induction with respect to all formulas. I.e., if a formula holds 
of 0, and whenever it  holds of a natural number n then it holds of 
n+1, then it holds of all natural numbers.

If so, then you are committed to what amounts to PA (Peano 
Arithmetic) with abbreviation power. Since abbreviation power is 
really part of logic, let us just say PA for now.

The problem is: how do we develop real analysis in PA?

There are two approaches.

a. Rip apart and reassemble real analysis in order to do it in PA.

b. Find some extension of PA that Buckner will not accept as 
meaningful, which does naturally do real analysis, and which can be 
interpreted in PA.

There is a terrific such extension of PA that almost serves this 
purpose, called ACA0. See

Stephen Simpson, Subsystems of Second Order Arithmetic, ASL, 
http://www.aslbooks.org/PML/PMLbooklist.html

The vast bulk of real analysis can naturally be done in ACA0 - 
although some interesting things cannot be done there. However, it is 
not interpretable in PA, although it is "almost" interpretable in PA.

So fix this, we need to extend items 3,4 above as follows.

3'. In addition, allow the introduction, through definition by 
induction, of relations among natural numbers, as long as the 
introduction of such relations does not allow one to treat those 
relations as mathematical objects. For example, we can define

R(0) if and only if A.
R(n+1) if and only if B(n,R|<=n).

Here A is a sentence of kind 1 above. B(n,R|<=n) is a formula of kind 
1 above, except that it is allowed to use R restricted to the natural 
numbers <= n, and of course it is allowed to use n.

Let us call this system PA'.

THEOREM. ACA0 is interpretable in PA'.

Thus although undoubtedly you would regard ACA0 as meaningless, it 
can be interpreted in something you regard as meaningful and 
acceptable. The interpretation is of course such that not only does 
every sentence in the language of ACA0 get interpreted as a 
meaningful sentence in the language of PA', but also every proof in 
the system ACA0 gets interpreted as a proof in the system PA'.

The interpretation can be written down and verified to be an 
interpretation, although the interpretation is rather complicated and 
ugly.

ACA0 has variables over natural numbers and variables over sets of 
natural numbers. The axioms are just like PA, with induction for 
formulas that quantify over natural numbers only. There is no 
induction for formulas that quantify over sets of natural numbers. 
This much you would accept. However, the main axiom scheme is that of 
arithmetic comprehension:

(there exists X)(for all n)(n in X if and only if A(n))

where A has quantifiers only over natural numbers, and is allowed 
side parameters for natural numbers and sets of natural numbers.

Thus ACA0 proves that there are plenty of infinite sets of natural 
numbers. Also, ACA0 easily states and proves

CANTOR'S THEOREM: For any set of ordered pairs of natural numbers, 
there is a set of natural numbers that differs from each cross 
section.

But because of the THEOREM stated above, you may be satisfied with 
this "solution".