[FOM] Constructive reactions to Goedel Incompleteness
sambin at math.unipd.it
Thu Dec 14 03:19:35 EST 2006
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
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.
Professor of Mathematical Logic
Dipartimento di Matematica Pura e Applicata,
Universita' di Padova
More information about the FOM