[FOM] Proof "from the book"

[Jeffrey Ketland]

Arnon Avron:

>I indeed
>believe that Godel's original proof is still the best, and I would
>have certainly put it in my private book of celebrated proofs!
>(Historically, Tarski's proof was a reproduction of Godel's
>proof, not the other way around...).

That's an interesting parenthetical comment. It raises interesting questions
about the history and significance of the Indefinability Theorem, and its
relation to Gödel's work. So, I apologise in advance for the following long
discussion, but it's something I'm deeply interested in, and perhaps might
be the basis for a fruitful discussion.

Somewhere in Gödel's recollections (either in the Wang volumes, or in the
Collected Works, or in Feferman's recent book), he says that, in his train
of thought in 1930, he found the Indefinability Theorem first, and then the
first Incompleteness Theorem came slightly later. I can't remember exactly
where this is located. If I remember right, the gist is this. In studying
the consistency problem, Gödel wanted initially to give an interpretation of
second-order arithmetic within first-order arithmetic, and tried to find a
definition of (second-order!) arithmetic truth in the first-order language.
He discovered however that even first-order arithmetic truth is not
arithmetically definable: i.e., what we now call Tarski's Indefinability
Theorem. But, as he also discovered, the concept "provable-in-F", with F
some fixed formal system, is arithmetically definable. This implies that
arithmetic truth is distinct from provable-in-F, for any formal system F.
This then gives us the quick proof of Gödel's first incompleteness theorem.

Gödel reported the indefinablity theorem in a letter to von Neumann (in
1931, I think). Tarski's version of the result first appears publicly 2
years later, in his 1933 book on truth (in Polish), which later appeared in
German as Der Wahrheitsbegriff (1935/6). While this is well-known, I am
tempted to speculate that a lot of the technical material that appeared in
Tarski's Der Wahrheitsbegriff had already been discovered by Gödel himself,
by 1931 (as his footnote 48a appears to indicate: see below).

Somewhat later, Gödel made a very interesting comment on these matters in a
letter to A.W. Burks, the editor of a work by von Neumann. Here Gödel refers
to the "true reason for the existence of undecidable propositions":

       
 the theorem of mine that von Neumann refers to is 

       the fact that a complete epistemological description of
       a language A cannot be given in the same language A,
       because the concept of truth of sentences in A cannot be
       defined in A. It is this theorem which is the true reason
       for the existence of undecidable propositions containing
       arithmetic. (von Neumann 1966, pp. 55-6.)

(Reference: von Neumann, J. 1966. Theory of Self-Reproducing Automata. A.W.
Burks (ed.). Urbana: University of Illinois Press.)

It seems here that Gödel is saying that the (Tarski-Gödel) Indefinability
Theorem is the "true reason" for the First Incompleteness Theorem. Aren't
"proofs from the book" meant to give the "true reason" for the proposition
proved? The underlying explanation? If I am interpreting Gödel correctly,
then he is saying that the underlying explanatory reason for the first
incompleteness theorem is in fact the indefinability theorem.

Also related to the question concerning the "true reason" for incompleteness
is Gödel's fascinating footnote 48a to his original 1931 paper, which says:

      The true source of the incompleteness attaching to all formal
      systems of mathematics, is to be found---as will be shown in
      Part II of this essay---in the fact that the formation of ever
      higher types can be continued into the transfinite (c.f., D. Hilbert,
      ‘Über das Unendliche’, Math. Ann. 95, p. 184), whereas in
      every formal system at most denumerably many types occur.
      It can be shown, that is, that the undecidable propositions here
      presented become always become decidable by the adjunction
      of suitable higher types (e.g., of type omega for the system P).
      A similar result also holds for the axiom system of set theory.
      (Gödel 1931, footnote 48a.)

Part II didn't appear, but the decidability of Gödel-type propositions by
higher-order semantical methods is first explicitly discussed by Tarski,
actually in the Postscript to his Der Wahrheitsbegriff. How could Gödel have
known about all this without having first have worked out the details? It
seems to me that Gödel must have already worked out the details of
formalized semantics before his 1931 paper appeared. If this is right, then
Gödel must have anticipated quite a few of the ideas we usually associate
with Tarski's 1933 work (the T-scheme, the inductive truth definition, the
definability of nth-order truth at (n+1)th-order, the non-conservation of
(n+1)th-order arithmetic over nth-order).

Turning to matters philosophical, it seems to me that this phenomenon of
non-conservation associated with higher-order semantical methods is related
to several recent philosophical debates. First, the Lucas-Penrose
argument(s) concerning the alleged "insight" whereby we "see" that G is
true; and second, some recent discussions of deflationism about truth.

As we now understand somewhat better, if you extend a formal system S of
sufficient richness (which contains an induction scheme) with a suitable
truth theory (e.g., Tarski's inductive definition), one obtains a
non-conservative extension, denoted Tr(S) in Feferman 1991 ("Reflecting on
Incompleteness", JSL). It is important to note that the induction scheme
must be expanded, to include formulas with the truth predicate, in obtaining
Tr(S). Crucially Tr(S) proves the reflection principles for S. So, Tr(S)
implies both Con(S) and G.

In some important sense, if we accept S as a fragment of our mathematical
knowledge, then we *ought* to accept Tr(S) too. And hence G. We might say
that sentences like G are "reflective consequences" of the original base
theory S. For example, if we accept PA, then we ought to accept Tr(PA), and
the corresponding reflection principles, which imply Con(PA). If our powers
of truth-theoretic reflection are working correctly, it doesn't make sense
to accept PA and to reject Con(PA), since Con(PA) is a reflective
consequence of PA. It would be a bit like accepting the axioms and rules of
PA and rejecting the commutativity of addition.

The usual reply to Lucas-Penrose is roughly:

      "Hang on: of course, we can prove G if we have a prior
      proof that S is consistent. Con(S)->G is provable, and
      thus it's a one-liner from Con(S) to G. But how exactly
      do we know the consistency of S? In general, we just
      don't know the consistency of an arbitrary given
      formal system S, even if it is in fact consistent."

I entirely agree with this reply. In order for their arguments to work at
all we should need empirical evidence for the claim,

      (*) For any consistent S, the human mind can reliably come to see
      that S is consistent.

So far as I can tell, there is no empirical reason whatsoever to suppose
that the human mind possesses this very rich capacity, which we can call the
Lucas-Penrose Capacity. If (*) is true, then their conclusions about the
mind somehow transcending the capacities of the machine seem correct. But I
have never seen any empirical evidence for the truth of (*). Sub specie
aeternitatis, the number of formal systems we have examined is very small.
In some cases, we have made mistakes regarding the consistency of certain
systems (Frege, Quine, a few others), fortunately later rectified. In other
cases, we appear to have a good understanding of why they must be
consistent---in each case, this appears to be semantical. But these examples
can only be a tiny fragment of the possible domain of consistent formal
systems. Unless we really do have this capacity to reliably recognise
consistency, then the Lucas-Penrose arguments do not go through.

However, if I am right, we can analyse our ability to see that G_{PA} is
true on the sort of truth-theoretic basis sketched above. For G_{PA} is a
reflective consequence of PA. And PA is a mathematical theory that we do in
fact accept (unless one pretends to be a strict finitist, or a potato, ...).

The notion of "reflective consequence" has been analysed by Feferman. Using
the Kripke-Feferman truth axioms, Feferman defines a theory Ref(S) which he
calls the "reflective closure" of S. This is meant to contain the sentences
one "ought to accept", when one initially accepts a mathematical theory S.
In a sense, Ref(S) is the result of iterating the construction from S to
Tr(S). Feferman doesn't advocate iterating Ref(S), but I do not see why. In
any case, both Ref(S) and Tr(S) are generically stronger than S. It is
curious that axioms for the notion of truth sometimes have this non-trivial
proof-theoretic power, a fact which can be deployed to argue against the
recently popular idea of deflationism---the idea that truth is
insubstantial.

--- Jeff
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Jeffrey Ketland
School of Philosophy, Psychology and Language Sciences
University of Edinburgh, David Hume Tower
George Square, Edinburgh  EH8 9JX, United Kingdom
jeffrey.ketland at ed.ac.uk
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~