Delivery-Date: 
Date: Sun, 18 Apr 93 16:26:58 CDT
From: Robert "S." Boyer <boyer@COM.CLI>
Message-Id: <9304182126.AA13478@axiom.CLI.COM>
To: qed@gov.anl.mcs
Subject: PRA defined
Reply-To: boyer@COM.CLI
Sender: qed-owner@gov.anl.mcs
Precedence: bulk

Here is a very brief and easy to read description of Primitive
Recursive Arithmetic (PRA) copied (without permission) from Feferman's
paper `What rests on what? ...', invited lecture, 15th International
Wittgenstein Symposium, Kirchberg/Wechsel, Austria, August, 1992.

****************************************************************************

The language L0 is a type 0 (or first-order) single sorted formalism.
It contains variables x, y, z, ..., the constant symbol 0, the
successor symbol ', and symbols f0, f1, for each primitive recursive
function, beginning with f0(x,y) for x+y and f1(x,y) for x*y.  The
terms t, t1, t2, are build up from the variables and 0 by closing
under ' and the fi.  The atomic formulas are equations t1 = t2 
between terms.  Formulas are built up from these by closing under the
propositional operations (~, &, v, ->) and quantification (for all x,
exists x) with respect to any variable.  A formula is said to the
quantifier-free, or in the class QF, if it contains no quantifiers.
[...]
  Unless otherwise noted, the underlying logic is that of the classical
first-order predicate calculus with equality.  The basic non-logical
axioms Ax0 of arithmetic are:
  (1) x' =/= 0
  (2) x' = y' -> x = y
  (3) x + 0 = x & x + y' = (x + y)'
  (4) x * 0 = 0 & x * y' = x * y + x
and so on for each further fi (using its primitive recursive defining
equations as axioms).  To Ax0 may also be added certain instances of
the Induction Axiom scheme IA:
  phi(0) & (for all x (phi(x) -> phi(x'))) -> (for all x (phi(x))),
for each formula phi(x) (with possible additional free variables).
[...]  We use PA (Peano Arithmetic) to denote the system with axioms
Ax0 + IA where the full scheme is used.
  The language PRA (Primitive Recursive Arithmetic) is just the
quantifier-free part of L0.  In place of IA it uses an Induction Rule IR:

     phi(0),        phi(x) -> phi(x')
   -------------------------------------,    for each phi in QF
            phi(x)

****************************************************************************
End of quotation from Feferman.

I don't doubt that the Lowenheim-Skolem theorem can be used to show
that PRA admits models of arbitrarily large cardinality.  In another
reference on recursive arithmetic, Goodstein's book Recursive Number
Theory (North Holland, 1964), one can find a logic very similar to PRA
(except for the inclusion of recursive functions in a scheme richer
than primitive) and also a presentation of an explicit nonstandard
model of arithmetic (after Skolem), in which the integers are
interpreted as the single argument primitive recursive functions.

In Feferman's logic FS0, the role of integers is taken over by binary
trees (with 0 at the tips), constructed with a primitive pairing
operation (I think of the Lisp CONS).  This makes it more pleasant and
computationally tractable in ordinary programming languages to talk
about terms than does the technique of Goedel numbering of formulas.

Bob