# [FOM] Another constructivist query.

S. Spijkerman / F. Waaldijk sufra at hetnet.nl
Mon Apr 3 12:59:59 EDT 2006

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

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

```