[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
--
Robert Black
Dept of Philosophy
University of Nottingham
Nottingham NG7 2RD
tel. 0115-951 5845
More information about the FOM
mailing list