[FOM] Godel and PA

[Richard Heck]

On 03/02/2017 06:34 PM, Martin Davis wrote:
> Godel proved his theorems not for PA, but for a system with a
> countable  infinity of types and atomic formulas of the form a(b)
>  where a is one type higher than b. Peano postulates were assumed for
> the bottom type. And he did prove, as a separate result, that all
> primitive recursive relations are arithmetic.

Just to be completely precise: In the system Gödel calls P, the axioms
he assumes at type 1 are just the successor axioms and induction (as a
single axiom). I.e., he does not include axioms for addition and
multiplication. Indeed, + and × are not primitives but are treated as
defined, presumably via the Dedekind-Frege method. (The same goes for
equality.) What this means is that the proof Gödel actually gives does
make real use of the type structure. Moreover, as Gödel notes, the
system has variables only for monadic types, and relations are to be
handled via tuples; these are to be defined by the Wiener-Kuratowski
definition, which means that pairs of numbers live at type 3. So sets of
these are at type 4, and so the definition of addition quantifes at
least over type 4 objects; and if we treat triples as pairs of pairs
(Gödel does not say how to do this), then it quantifies over type 5 objects.

One would have to plow through all the details to get a definite
statement of what I'm about to say, then, but something like the
following is true: What Gödel's proof of Theorem VI (the first(!) first
incompleteness theorem) shows, most directly, is that (every recursive
extension of) fourth-order arithmetic is incomplete (assuming it is
ω-consistent).

As Martin says, Gödel goes on to show, in section 3, as Theorem VII,
that all (primitive) recursive relations are arithmetical. But he does
*not* use this to show, say, that PA (as opposed to simple type theory)
is incomplete, and he does not mention any such application. Rather, his
purpose in proving this result is to characterize the *kind of sentence*
that cannot be decided by the sorts of systems he is considering: These
can be taken to be, as he puts it in the first paragraph, "relatively
simple problems in the theory of integers". Thus, Theorem VIII, which is
just a corollary of VI and VII, says that "In [P and any of its
ω-consistent (primitive) recursive extensions], there are undecidable
*arithmetical* propositions". As said: It's the kind of proposition
that's undecidable that Gödel is interested in here, not ths system
that's doing the deciding.

It seems to me that this point is of some (minor) historical interest.
Later authors would of course become interested in the question just how
weak we can make the system to which the incompleteness theorem
applies---an investigation that, I take it, culminates with the work of
Raphael Robinson in the early 1950s (best known from Tarski, Mostowski,
and Robinson's /Undecidable Theories/). But that is not where Gödel is
at in 1931. His motivation is different, and is nicely explained in the
first paragraph of his paper:

The development of mathematics towards greater precision has led, as is
well-known, to the formalization of large tracts of it, so that one can
prove any theorem using noting but a few mechanical rules. The most
comprehensive formal systems that have been set up hitherto are the
system of Principia Mathematica (PM) on the one hand the
Zermelo-Fraenkel axiom system of set theory...on the other. These two
systems are so comprhensive that in them all methods of proof today used
in mathematics are formalized, that is, reduced to a few axioms and
rules of inference. One might therefore conjecture that these axioms and
rules of inference are sufficient to decide any mathematical question
that can at all be formally expressed in these systems. It will be shown
below that this is not the case, that on the contrary there are in the
two systems mentioned relatively simple problems in the theory of
integers that cannot be decided on the basis of the axioms. [And this
goes for lots of other systems, too, including recursive extensions of
those ones.]

Gödel, then, is interested not so much in whether his theorem applies to
*weak* systems, but in the fact that it applies to *arbitrarily strong*
ones (so long as they are ω-consistent and have a (primitive) recursive
set of axioms). That, I take it, is why he is happy to work with such a
strong system as P and does not really evince (at that time) any
interest in restricting the resources he is using.

I'd be interested in learning more about the history that gets us from
Gödel to Robinson, if anyone wishes to explain some of it. Obviously,
Hilbert and Bernays must have had a role to play, but I don't know what
else happens between 1931 and 1953.

Richard Heck

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20170303/514eb2ce/attachment.html>