[FOM] Another constructivist query.

[Bill Taylor]

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