Chris and Pat, (01)
I'm traveling now and I don't have a copy of Gödel's paper
handy, but I'll try to reconstruct as much as I can recall. (02)
> To expand on Pat's point: Gödel'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. (03)
As I recall, Gödel was not trying to prove the incompleteness
of number theory, but the incompleteness of higher-order logic.
In his PhD dissertation, Gödel (1930) proved the completeness
of first-order logic: (04)
From any given set of axioms A stated in FOL, every
proposition p that is true in all models of A can be
proved from A by the usual rules of inference of FOL. (05)
But in his incompleteness paper, Gödel (1931) proved that any
version of higher order logic that is sufficiently expressive
to define arithmetic is incomplete. (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. That approach was important
because the proof procedure involved a reductio ad absurdum;
i.e., either arithmetic is inconsistent or HOL is incomplete.
If Gödel had decided to prove something like "Either ZFC is
inconsistent or HOL is incomplete", mathematicians in 1931
would be likely to say "A pox on both houses". (07)
To carry out his proof, Gödel made the following assumption: (08)
The computational methods of ordinary arithmetic are consistent. (09)
Then he carried out his proof of incompleteness of HOL in the
following stages: (010)
1. Choose a particular version of HOL -- the one defined by
Whitehead and Russell in the _Principia Mathematica_ (PM). (011)
2. Define a method of encoding every symbol, formula, and proof
in PM into an integer. (012)
3. Assume common functions over integers and common notions,
such as 'prime number', and assume that the published
definitions and proofs based on Peano's axioms are correct. (013)
4. Define various functions over integers, such as (014)
isaFormula(i) -> integer i is an encoding of a PM formula (015)
isaProof(i,j) -> integer i is an encoding of a PM proof
of the formula encoded by integer j (016)
isProvable(i) -> integer i is an encoding of a PM formula
for which there exists an integer j which encodes
a PM proof of the formula encoded by i. (017)
5. Define an integer k, which encodes a formula that says,
in effect, this formula is not provable. (018)
6. Prove that isProvable(k) is false. (019)
7. Since the formula encoded by k must be either true or false,
there are two options: (020)
(a) k is true, and it correctly states that k is not provable. (021)
(b) k is false, therefore k must be provable, and the system
of arithmetic used to encode all the functions defined
above must be inconsistent. (022)
Since all mathematicians have for many millennia assumed that
arithmetic is consistent, they would naturally prefer option (a),
which implies that there are statements in HOL that are true in
all possible models, but they are not provable by the rules of
inference of HOL. (023)
This proof, as I interpret it, does not prove that arithmetic
is incomplete, but that the system of PM is incomplete. Henkin,
for example, showed that proofs from Peano's axioms could be
complete if nonstandard models were included. (024)
John (025)
_________________________________________________________________
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 (026)
|