[FOM] Godel's Theorems

[Giuseppe Longo]

> To: fom at cs.nyu.edu
> From: Harvey Friedman <friedman at math.ohio-state.edu>
> Tue, 29 Apr 2003 21:52:59 -0400
> Subject: [FOM] Godel's Theorems
>
> *) there is a true sentence in the language of PA which
> is not provable in PA.
>
> 1. Conventional wisdom is that this is now a fully established
> theorem of mathematics (or ordinary mathematics as currently
> practiced by the overwhelming majority of mathematicians). Is there
> agreement on this?

* is surely correct, but its statement, as given, should be only  
reserved to competent circles.  Otherwise, we often hear: Oh, ho ...  
what a miracle, there exist true mathematical statements that are not  
provable, THUS:
1 - they are accessible in view of non-separable quantum effects in  
neural microtubules,
or
2 - mathematicians see them by looking over the shoulders of God.
Two (or more?) books have been written on the grounds of 1 and 2. Of  
course, there may be relevant quantum effects (for cognition) in  
brain, by a scientific reduction is a theoretical operation: one  
reduces a phenomenal level to a given THEORY (of another phenomenal  
level: chemical, physical ...) by some evidence, while there is no  
empirical evidence no sound unified theoretical frame for such a  
reduction; moreover, Goedel's theorem in no way justifies such  
short-cuts.  Similarly, since Galileo and, more consistently, since  
Laplace, we learned not to refer to God in our scientific analysis  
(and there is no empirical evidence concerning the relative position  
of mathematicians' head and God's shoulders).

Wittgenstein is just pointing out to us that this philosophical  
debacle could take place if we are not careful to the actual meaning  
of * (and it did take place).
In modern terms, Witt. is telling us: consider, say, FFF (Friedman's  
Finite Form of Kruskal's theorem).  It is a statement of PA; however  
one can prove that it is not provable in PA, yet a proof of it may  
be given in a stronger theory (either by use of induction over a  
Sigma-1-1 set, or by a very large - impredicative - ordinal).
Of course, also Godel's undecidable sentence G may be shown to hold  
on N (HAS TO BE SHOWN, says Witt.): assume consistency, use  
undecidability (whose proof uses consistency) and continue by an easy  
classical argument ....  But the recent concrete incompleteness  
results show this more clearly to us, without the danger of confusing  
this easy proof of the truth of G with an absolute quantum/God-given  
truth, as the their truth is not "evident".  Witt. had the  
philosophical insight to tell this to us well before the concrete  
incompleteness results that forbid philosophical short-cuts and  
truth-miracles of various sorts.

Actually mathematicians understand the proof of FFF, say, in a sound  
"geometric" way. Just look at the number line, in your mind (the  
result of a complex conceptual construction: the well-ordered  
sequence of numbers as counting and its mental spatialization). Every  
mathematician sees it by training (don't you see it? it goes from  
left to right, doesn't it?). Observe that
       "a generic non-empty subset of it has a least element"
(an easy observation, that we may call a "geometric judgement").  
Then, in particular, the Sigma-1-1 set in the proof of the truth of  
FFF, if it is not empty, has a least element ... and the proof of FFF  
easily continues by contradiction (which gives the set to be empty).  
Since this set will be shown to be empty, the detailed Sigma-1-1  
definition is not used in the proof and the general geometric  
judgement convinces any (graduate) student in maths or Computer  
Science I lecture to. This geometric judgement is used everyday by  
mathematicians; by the way, it guarantees to them the consistency of  
strong forms of induction with no need of (logically very informative  
but) infinite regressions into infinities.

In short, in my view, Wittgenstein stresses that there is no other  
access to knowledge in Maths besides proofs.  That proofs may be  
grounded on assumptions, which must be made explicit.  Meaningful  
assumptions, as Husserl would add:
"... the axioms are mostly the result of an original formation of  
meaning and they already have this formation itself behind them" (The  
origin of Geometry, 1933). As for integer numbers, the evidence (as  
original formation of meaning) of strong forms for induction may be  
grounded on spatial/mental well-ordering.
Calling it a geometric judgement is compatible with (and in my case  
partially inspired by) a practice of Witt.,since in the '30s he often  
and soundly used space/geometric metaphors in his analysis of  
LANGUAGE (one of the original aspects of his philosophy of language).

Remarks on the proofs of Normalization for Type Theories and FFF may  
be found in

Giuseppe Longo. On the proofs of some formally unprovable  
propositions and Prototype Proofs in Type Theory. Invited  
Lecture,Types for Proofs and Programs, Durham, (GB), Dec. 2000;  
Lecture Notes in Computer Science, vol 2277 (Callaghan et al. eds),  
pp. 160 - 180, Springer, 2002.

Downloadable from   http://www.di.ens.fr/users/longo


-- Giuseppe Longo
Laboratoire et Departement d'Informatique
CNRS et Ecole Normale Superieure
et CREA, Ecole Polytechnique
(Postal addr.:  LIENS
45, Rue D'Ulm
75005  Paris   (France) )
http://www.di.ens.fr/users/longo
e-mail: longo at di.ens.fr