[FOM] The definition of the natural numbers vs. the axiom of infinity

[Dana Scott]

It is well known that there are many ways to define "finite" and not
use the Axiom of Infinity.  As to natural numbers, if we use

    0 = empty set and

    n+1 = n u {n} for successor ("u" means union),

AND if we have enough Axiom of Foundation to prove

(0) (All n,m)[n+1 = m+1 ==> n = m],

THEN a definition by "counting down", rather than by "counting up"
seems to work well.  Specifically, define

      NN(n) <==> (All s)[ n in s & (All x)[x+1 in s ==> x in s] ==> 0 in s]

We then prove:

(1) NN(0)  -- Obvious.

(2) NN(n) ==> NN(n+1)

    For, assume n+1 in s and s is "closed under predecessor" (as
    above).  Then n in s follows.  And, by assumption, 0 in s follows
    as well.

(3) Phi(0) & (All x)[Phi(x) ==> Phi(x+1)] ==> (All n)[NN(n) ==> Phi(n)]

    Assume the hypotheses and assume NN(n) but not Phi(n).  Define

        s = {x subset n | not Phi(x) }

    Then, by assumption n in s.  Suppose x+1 in s.  Then x+1 subset n.  
    So, x subset n as well.  Also not Phi(x+1).  Thus, not Phi(x).
    Therefore x in s.  But, since NN(n), we would have 0 in s, which
    contradicts the assumption Phi(0).

Inasmuch as 0 cannot be a successor, I think this gives all the Peano
Axioms.  (Note in (3) it is not necessary to restrict "x" to "NN", as
that version follows in the light of (1) and (2).)

This must be known.