[FOM] Non-constructiveness.

[Lucas Wiman]

> 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'.

I think you're missing his point.  The point is that mathematicians 
would be very reluctant to call these "constructive proofs," though 
they're generally labeled as such.  There is an area of combinatorics 
called Ramsey theory which (often) deals solely with finite numbers.  
Here is a big open problem in Ramsey theory:

For each number n, find the smallest number R(n) such that each 
2-coloring of the edges of the complete graph on n vertices, there is a 
monochromatic complete graph on n vertices.

The existence of this number for every n is pretty easy to show, but say 
we want to know that R(6)=178 (which is one possible value for it, as 
far as we know).  Then we much show that every graph of order 178 has a 
complete subgraph of order 6, and that there is some graph of order 177 
that has no complete subgraph of order 6.  Any such graph must be really 
weird, and is hence rather hard to find by looking for it 
intelligently.  We can't do a brute search because there are a whole lot 
of graphs of order 177!

The methods of modern combinatorics give no aid in finding the exact 
value, so we have to accept it on what's been called "religious faith" 
on this list.  This is the sense in which it is non-constructive:  an 
existence theorem, even in the "large finite" arena can fail to really 
give you the object of which it speaks.

- Lucas Wiman