[FOM] Another constructivist query.

[S. Spijkerman / F. Waaldijk]

this scenario needs little imagination.

take p(n) to say: there are 99 consecutive 9's in the decimal expansion of 
pi before the n-th digit.

take q(n) to be: (exists n < 10^10^10^10^10)  p(n)) OR (all n < 
10^10^10^10^10) NOT p(n))

and well, your scenario is healthy and kicking.

of course q(n) is a constructive truth. a constructive proof: just check all 
digits of pi up to the 10^10^10^10^10-th digit. the carrying out of this 
might seem grotesque (...) but in fact this is not necessary, the proof just 
relies on the indication of this method, not on the actual performance of 
all necessary calculations. the garden variety constructivist has infinite 
trust in a finite number of finite calculations...no matter how big `finite' 
is.

your question is therefore really about feasibility. also interesting, but 
more difficult, i believe. a good system which really describes 
feasibility/infeasibility in a sharp way and still allows for good 
mathematics, i don't know of it but please allow for large ignorance on my 
part!



----- Original Message ----- 
From: "Bill Taylor" <W.Taylor at math.canterbury.ac.nz>
To: <fom at cs.nyu.edu>
Cc: <W.Taylor at math.canterbury.ac.nz>
Sent: Monday, April 03, 2006 5:27 AM
Subject: [FOM] Another constructivist query.


> Here is another query on the basic philosophy of constructivism.
> It would be nice to hear responses from both committed constructivists,
> and from those committed away from it.
>
> Imagine the following scenario.   (It would have seemed ludicrous not
> too long ago; but in view of Friedman's recent work, maybe not, now.)
>
>
> p(n) is a numerical proposition with one free variable n,
>     recursively testable for the numeral for any n.
>
> q    is a numerical proposition with no free variables.
>
> Scenario
> ========
> It has been separately proved that
>
> (a)   [(exists n < 10^10^10^10^10)  p(n) ]  ==>  q
>
> (b)   [(all n < 10^10^10^10^10) NOT p(n) ]  ==>  q
>
>
> My query
> ========
> Do (a) & (b) together constitute an acceptable constructive proof of q?
>
>
> I'm almost sure the answer is "yes"; in which case I might wonder
> whether everyone here is entirely comfortable with this situation?
>
> Bill Taylor
>
>
>