[FOM] Constructive reactions to Goedel Incompleteness

praatika@mappi.helsinki.fi praatika at mappi.helsinki.fi
Wed Dec 13 00:38:12 EST 2006

Peter Aczel posted an admirably clear message. Just a couple of 

Peter Aczel <petera at cs.man.ac.uk>:
> 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.

Well, the infinity of domain cannot in general be the essential issue; 
think of Presbuger Arithmetic, of RCF. By the way, speaking about finite 
models, I still find Trakhtenbrot's theorem (i.e., that validity in all 
*finite* models is not completely axiomatizable) surprising. 

> 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.

Whether a completeness result would be surprising or not, for the 
(absolute) notion of provability presupposed in the standard  
interpretation of intuitionistic logic, one can - in a definite sense - 
prove certain incompleteness results (as was noted already by Goedel in 

And I, for one, find this quite puzzling... It is fair, I think, to ask 
what, more exactly, such proofs are supposed to be.

All the Best


Panu Raatikainen

Ph.D., Academy Research Fellow,
Docent in Theoretical Philosophy
Department of Philosophy
University of Helsinki

E-mail: panu.raatikainen at helsinki.fi

More information about the FOM mailing list