[FOM] Solution for Buckner?
Harvey Friedman
friedman at math.ohio-state.edu
Sun May 4 11:20:39 EDT 2003
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".
More information about the FOM
mailing list