[FOM] Indispensability of the natural numbers

[Andrew Boucher]

On May 16, 2004, at 21:15, Timothy Y. Chow wrote:
> Therefore, assuming that one has a clear notion of
> what "PA is consistent" *means*, and of the notion of a "proof" of such
> a thing (as in something that would compel assent to such a meaningful
> proposition), already presupposes a clear enough notion of the natural
> numbers to make the consistency of PA obvious.
>

There exist second-order systems which do not assume that the
natural numbers continue ad infinitum (i.e. do not assume that the
sequential relationship is total).  In these systems one is able to 
define
the notion of a wff, the notion of a proof, and the notion of 
consistency
itself.  (Certain of these systems can even prove their own 
consistency.)
It would seem, then, that these notions do not pre-suppose a notion
of the natural numbers as you probably think of the natural numbers, as
an unending sequence.

Here's one way to think of it.  It is true that formal systems are often
defined with the pre-supposition that there are unending sequences.
E.g. Mendelson defines, "If A and B are wfs, then (A => B) is a wff."
This definition explicitly assumes that one can generate wffs of
arbitrarily long length:  (A => A), (A => (A => A), etc.

But nothing really is lost if one changes the definition to work in the
reverse direction.  Say instead:  "X is a wff if:  it is atomic, or if 
it is
of the form (A => B), or ..."  That is, rather than saying how to create
a new X, one assumes that one has X and one gives a definition
which explains what it takes for it to be a wff.  One can do the same
for the notion of proof, and so one can define consistency without
assuming ad infinitum.