# [FOM] Indispensability of the natural numbers

Mon May 17 14:34:33 EDT 2004

```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