[FOM] Constructive reactions to Goedel Incompleteness

[giovanni sambin]

Peter Aczel points out two ways of understanding completeness (of a 
formal system) constructively:

At 12:26 +0000 12-12-2006, Peter Aczel wrote:
>1) Every sentence of the formal language is formally provable or
>    formally refutable (i.e. its negation is formally provable).
>
>2) Every true sentence of the formal language is formally provable.

I would like to make it clear, first of all, that failure of both is 
easily provable in a fully constructive way. In fact,  in recent 
joint work with M. E. Maietti, we have found a formula F such that 
both F and not-F are unprovable in Heyting arithmetic HA. Moreover, 
not-F is certainly true, since it is just the formula asserting 
consistency of HA (btw., this is established by a proof, which by 
Goedel's second theorem is outside HA itself).

Why have constructivists been so little interested in Goedel's 
theorems? (For example, the proof mentioned above is absolutely 
elementary, but I could not find anything similar in the literature.) 
It seems to me that the explanation of this is shown by Brouwer's 
beliefs, as reported in Mark van Atten's posting. For Brouwer, 
incompleteness was neither as surprising nor as dramatic, as it was 
for Hilbert.

Upon reflection, he was right. Actually, I personally see in the 
incompleteness phenomenon a good reason to become a constructivist. 
Incompleteness (and unprovability of consistency) is just part of a 
dynamic view, which is fully compatible with constructivism, while it 
is very disappointing when truth is seen as fixed, as is common to 
the classic view.

As a constructivist, I see incompleteness as a natural phenomenon, 
which is part of the world in which we live. Goedel's theorems compel 
one to recall that there is no language without a metalanguage. As 
observed by Goedel himself (see van Atten's posting), the key of his 
contribution is showing that language itself reflects this fact. In 
nature, there is no organism without an environment. And this is 
exactly what prevents an organism to be fully aware of him/her/itself 
(this remark is due to Gregory Bateson).

If something is accepted as true only when a proof is given, then it 
is obvious that no fixed system of rules will give all truths: one 
can immediately obtain a new true proposition (e.g. a statement of 
underivability) in which those rules are taken as objects. Note en 
passant that, since mathematics is not reducible to logic, one still 
can consider intuitionistic logic as central and see that Panu 
Raatikainen's fear is unfounded.

In conclusion, as a constructivist, it is difficult for me to see why 
Goedel's theorems are still a source of so much surprise.

Giovanni Sambin
Professor of Mathematical Logic
Dipartimento di Matematica Pura e Applicata,
Universita' di Padova