[FOM] Proof "from the book" (the last reply)

[Arnon Avron]

After some messages exchanged on the FOM, Torkel Franzen and I turned
to a personal exchange, in order to clarify what exactly is the difference 
between what we say (I had the impression that do not agree about
the *mathematical* facts, and this is an unacceptable situation). The 
following short message of Torkel finally makes me undrstand his point:

>   My concern has only been to emphasize the difference between
> 
>     If S is consistent, Godel's proof proves "G_S is true"
> 
> and
> 
>     Godel's proof proves "If S is consistent, G_S is true".

I doubt if ordinary mathematical texts or the usual understanding of 
natural languages really distinguish between the two. Still, the two
statements, if understood the way Torkel intends here to understand
them, are indeed different. As usual, this can be seen by translating
them into a language which is more exact than English. For example, suppose
Godel's proof concerning S is carried in some mathematical
metatheory T. Then the translation of the first sentence above might be:

         Con_S -> Pr_T(G_S)


while the translation of the second might be:

         Pr_T(Con_S -> G_S)

The first of these two sentences is false, the second is true.

In my original message I indeed did not pay any attention to this fine
difference - it was just a short comment, and the difference is not
really relevant to the point I was trying to make. Anyway, let me
reformulate my claim there in a more exact (but technical) terms.
The difference between Godel's original argument and the short, direct
argument based on Tarski's theorem (provability is definable, truth is not,
where the later is proved by reduction ad absurdum) is that
Godel's  proof proves that what Feferman calls "the reflective closure
of S" (the truth of all elements of which follows from the truth of S)
is a proper superset of the logical deductive closure of S. This is 
an extremely important part of Godel's theorem, which the short
"proof from the book" suggested by Davis (again: if I understood 
him correctly) does not provide.


Arnon Avron