On Sun, 2 Mar 2008, John F. Sowa wrote:
> Chris and Pat,
>
> I'm traveling now and I don't have a copy of Goedel's paper
> handy, but I'll try to reconstruct as much as I can recall.
>
> > To expand on Pat's point: Goedel's mapping of the proof theory
> > of predicate logic into arithmetic had nothing to do with
> > foundational issues. Rather, it was the mechanism that enabled
> > him to prove the essential incompleteness of number theory.
>
> As I recall, Goedel was not trying to prove the incompleteness of
> number theory, but the incompleteness of higher-order logic. (01)
Well, first of all, let's be careful. You've got two very different
notions of (in)completeness here: negation completeness and semantic
completeness. A system S is negation complete if, for any sentence A of
the language of S, either A or its negation ~A is a theorem of S. Note
that this is a purely proof theoretic notion. A *logic* L -- that is, a
language + semantics + proof theory -- is semantically complete if every
logical truth of the language of L is a theorem of L. Note that nothing
we typically call a system of *logic* is negation complete. For
example, in propositional logic, no propositional variable p or its
negation ~p is a logical theorem. In predicate logic, neither (x)Px nor
~(x)Px, for example, is a theorem. (02)
That said, Goedel's Theorem (more exactly, his first incompleteness
theorem) is simply that every consistent, "sufficiently strong" system
of number theory is negation incomplete; for every such system, there is
a sentence of the language of the system that is *undecidable* by the
system, i.e., neither provable nor refutable by the system. (Actually,
in Goedel's formulation you need the somewhat stronger condition known
as omega-consistency, but as I noted in a previous msg, Rosser showed
that only consistency is needed.) This result holds for first- and
higher-order number theories alike. (03)
As for specifics, it is true that the system Principia Mathematica (PM)
of Russell and Whitehead that Goedel appeared to be singling out in his
1931 paper was a higher-order logic, indeed, a so-called omega-order
logic that encompassed nth-order logic for every n. However, bear in
mind that the title of Goedel's paper was "On Formally Undecidable
Propositions of Principia Mathematica *and Related Systems*". In fact,
Goedel did not use PM to prove his result but one of these related
systems. Specifically, he used an *explicitly* number theoretic,
higher-order variant that he called "P". The language of P included a
constant "0" to denote 0 (in the intended semantics of P), a 1-place
function symbol "f" to denote the successor relation, and simply typed
variables ranging over natural numbers, classes of natural numbers,
classes of classes of natural numbers, etc. It is this system that he
explicitly proved to be negation incomplete (his Theorem VI). (04)
However, Goedel goes on to show that the relations that are needed in a
system to code the system's own proof theory are all *arithmetical* --
that is to say, they can all be defined in terms of addition,
multiplication, and *first-order* quantification (Theorem VII). He then
shows that every (omega-)consistent extension P' of P has an undecidable
*arithmetical* sentence (Theorem X), i.e., an arithmetical sentence that
it neither proves nor refutes. It is immediate from this fact that
Goedel's result applies to any *first-order* system that contains the
bit of number theory (now often called Robinson Arithmetic) needed to
code its proof theory -- basically, this means just a couple of axioms
for 0 and the successor function ("0 is no number's successor"; "numbers
with the same successor are identical") and the usual axioms for
arithmetic and multiplication ("x+0=x", "x+fy = f(x+y)", "x*0=0", "x*fy
= x*(x*y)"). In a higher-order system like P, it is possible to
*define* addition and multiplication recursively instead of building
them in as primitives and characterizing them axiomatically, as would be
done in a first-order system. But Goedel's results are entirely
independent of his choice of P. (05)
Bottom line: (i) Goedel's intended target was indeed number theory, not
higher-order logic per se, and what he showed is that any consistent
extension of a particular higher-order system P of number theory is
negation incomplete. However, (ii) it follows immediately from several
theorems in Goedel's proof that any system of first-order number theory
containing just a few basic number theoretic axioms is also negation
incomplete. (iii) It is in fact a *consequence* of Goedel's Theorem
that every consistent system of second- (and higher-) order logic is
*semantically* incomplete. But this was actually proved some years
after Goedel's original publication. (Indeed, the modern distinction
between first- and higher-order logic was only just becoming clear
around 1931.) (06)
> In other words, the point of the proof was to show that HOL is
> incomplete, and arithmetic was used as a well-established system whose
> consistency was not in doubt. (07)
This is not historically correct. (08)
> To carry out his proof, Goedel made the following assumption:
>
> The computational methods of ordinary arithmetic are consistent.
>
> Then he carried out his proof of incompleteness of HOL in the
> following stages:
> ...[Overview of the proof elided]...
> ...
> This proof, as I interpret it, does not prove that arithmetic
> is incomplete, but that the system of PM is incomplete. (09)
Again, Goedel used a related higher-order system, but it is a simple
consequence of his proof that the result holds for any first- or
higher-order system containing Robinson Arithmetic. (010)
> Henkin, for example, showed that proofs from Peano's axioms could be
> complete if nonstandard models were included. (011)
I think you have a very different result in mind. Henkin showed that
higher-order logic with a so-called "general" semantics is
*semantically* complete. The trick is to broaden the range of the
higher-order variables beyond what is allowed in standard higher-order
logic -- therby opening the door to what might be called nonstandard
interpretations of the language of higher-order logic. The upshot of
this is that higher-order logic with a general semantics is, in effect,
just first-order logic in higher-order garb. Henkin's result has no
implications whatever for Peano Arithmetic vis-oedvis its negation
incompleteness. (012)
-chris (013)
_________________________________________________________________
Message Archives: http://ontolog.cim3.net/forum/ontolog-forum/
Subscribe/Config: http://ontolog.cim3.net/mailman/listinfo/ontolog-forum/
Unsubscribe: mailto:ontolog-forum-leave@xxxxxxxxxxxxxxxx
Shared Files: http://ontolog.cim3.net/file/
Community Wiki: http://ontolog.cim3.net/wiki/
To Post: mailto:ontolog-forum@xxxxxxxxxxxxxxxx (014)
|