[FOM] Godel sentence (Avron-Franzen exchange)

[A.P. Hazen]

General observations, followed by reference.

G.O.: We're interested in an "intensionally correct" formulation: one in
which the formula expressing provability "really means" provable, and so
on. Starting out with a formalization of syntax (Franzen recommends the
last chapter of Quine's "Mathematical Logic" as an example) seems like a
useful suggestion: at least there we don't have to worry about codings, and
are likely to have more intuitive feel for whether the formal definition
(of, say, "proof") is an accurate translation of our usual mathematical
English (or whatever) into the formal language. Note that this is a pruely
SEMANTIC question: it depends on the intended meaning of predicates of the
formal language, and the intended domain of interpretation, and NOT on the
axiomatization of the syntactic theory. It's probably best, however, to
work with a RICH formalization of syntax: one formulated in 2nd Order
Logic, for example (Quine's is 1st Order): fewer artificial dodges will be
needed in formalizing, e.g., inductive definitions, so the formal
definition will come closer to being a direct translation of what we do in
non-formalized metamathematics.

Reference: Corcoran, Frank, and Maloney, "String Theory," in JSL vol. 39
(1974), pp. 625-637. This presents two 2nd Order axiomatizations of syntax,
proving them equivalent in a very strong sense. The primitives of one are
close to those of Quine's 1st Order formulation. The axiomatizations of
syntax are also, in a very strong sense, equivalent to PA2 (= 2nd Order
Peano Arithmetic), so a proof of the incompleteness of one of these systems
would carry over directly to the arithmetic system.

(Postscript: The standard Godel sentences don't contain names for
themselves, let alone their own quotations: where G is such a setence, it
is only "equivalent" to the sentence Not(Bew('G')). This has caused a great
deal of conceptual confusion over the years, but is in a sense accidental.
Saul Kripke pointed out (in lectures at Princeton in 1982 -- I don't know
if he has published this observation anywhere) that we could add a new
constant, g,to our syntactical (or arithmetical) formal language, denoting
the sentence Not(Bew(g)) (or its Godel number) and, with some complications
about the axiomatization, prove Godel's incompleteness theorem by reference
to an EXPLICITLY and directly self-referential sentence.)

---

Allen Hazen
Philosophy Department
University of Melbourne
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: text/enriched
Size: 2546 bytes
Desc: not available
Url : /pipermail/fom/attachments/20030829/0786090e/attachment.bin