[FOM] Another constructivist query

[Rupert McCallum]

Bill Taylor wrote:

> I recall reading something to the effect that if a number theoretic
> statement has been proved classically, and it states something that
> (in principle) needs only a finite number of cases to check,
> then there also exists a constructive proof.

> This would mean, for example, that there is a constructive proof,
> that there exists a prime between  10^10^10^10 and 2x10^10^10^10.

> (a) Is the above correct?

> (b) Would a full-blown subjectivist intuitionist assent to the above?

I have just looked over a proof of Bertrand's postulate and it seems to
me that it goes through in PRA.

I'll be interested to see what people say about the general case.
Obviously it depends what you mean by "constructive proof".



	
		
__________________________________ 
Yahoo! Mail - PC Magazine Editors' Choice 2005 
http://mail.yahoo.com