[FOM] Non-constructiveness.

Robert Black Robert.Black at Nottingham.ac.uk
Thu Jul 3 05:16:54 EDT 2003

>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 Black
Dept of Philosophy
University of Nottingham
Nottingham NG7 2RD

tel. 0115-951 5845

More information about the FOM mailing list