[FOM] Constructive reactions to Goedel Incompleteness

[praatika@mappi.helsinki.fi]

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

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

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



Panu Raatikainen

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


E-mail: panu.raatikainen at helsinki.fi
 
http://www.helsinki.fi/collegium/eng/Raatikainen/raatikainen.htm