[FOM] Constructive reactions to Goedel Incompleteness

[Peter Aczel]

Antonino Drago has raised an interesting issue:

What has been, historically, the reactions of constructive
mathematicians, such as the Intuitionists, to Goedel's incompleteness
results?

I think that Goedel's results have a different flavour from a
constructive perspective.

Two notions of completeness for a sound (i.e. formally provable
 implies true) formal language need to be distinguished from the
 constructive point of view, although they are equivalent from the
 classical point of view:

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.

 From the constructive point of view 1) would be very surprising,
except for formal languages about finite structures.

Concerning 2) it must be remembered that, from the constructive point
of view, a sentence is true if it has a 'proof', where here `proof'
has to be understood in an intuitive informal sense (e.g.  for
Brouwer a certain kind of mental construction).  So 2) asserts that to
every `proof' of a sentence of the formal language there corresponds a
proof in the formal language. 

My feeling is that any completeness result 2) for a sound formal
language about an infinite structure would be quite surprising to a
constructive mathematician.  Are there any such results?  And perhaps
incompleteness results are generally to be expected from the
constructive point of view.

Peter Aczel
Professor of Mathematical Logic and Computing Science
Schools of Mathematics and Computer Science
The University of Manchester