[FOM] Non-constructiveness.

[Robert Black]

>In current constructivist foundations, it is generally agreed that any
>true statement that has, merely in principle, a method for deciding it in a
>finite number of steps, can be (in fact *is* thereby) proved constructively.
>I have been told there are metatheorems to this effect, indeed.
>
>So that if someone proved by apparently non-constructive means in PA,
>that all naturals up to 10^10 were such-and-such, where such-and-such
>was simply checkable on any number by a finite procedure, then this
>would BE thereby constructively true.

I can't see anything wrong with this. (The constructive part of) PA 
obviously decides any such statement correctly. Furthermore we have a 
constructive proof that PA is consistent (Goedel/Genzen 1933) and 
thus the whole of PA only decides it one way. Thus we have a 
constructive proof that there is a constructive proof of the result, 
which of course is a constructive proof of the result. This is really 
just the basic idea of the Hilbert programme, only substituting 
'constructive' for 'finitary'.

Robert
-- 
Robert Black
Dept of Philosophy
University of Nottingham
Nottingham NG7 2RD

tel. 0115-951 5845