[FOM] Constructive reactions to Goedel Incompleteness
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
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