Peter Aczel posted an admirably clear message. Just a couple of
comments...
Peter Aczel <petera-I9UBhjeNIXeFxr2TtlUqVg@xxxxxxxxxxxxxxxx>:
> 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-pxSi+dnQzZMxHbG02/KK1g@xxxxxxxxxxxxxxxx
http://www.helsinki.fi/collegium/eng/Raatikainen/raatikainen.htm
|
