FOM: Effective Bounds in Core Mathematics

[Fred Richman]

Harvey Friedman wrote:
 
> But many constructivists take the additional step of saying that
 
> *a classical proof of an arithmetic sentence that is not constructive isn't
> a proof of that arithmetic sentence*
 
> and there I view the position taken as counterproductive and needlessly
> provocative.

Surely they have to feel that way. If a constructivist were to accept
such a classical proof as a proof, in what sense would he be a
constructivist? 
 
> It would make sense for someone to take this position if they had a single
> instance where somebody had a classical proof of an arithmetical sentence
> that later turned out to be refutable - even classically refutable.

Of course you are not serious about this. The justification of the
constructivist position doesn't hinge on showing that classical
mathematics is inconsistent. An analysis of a classical proof of P
might reveal a constructive proof of a classically equivalent theorem
Q. The constructivist would maintain that Q is what had been proved,
not P. If the classical mathematician sees no essential difference
between P and Q, in what way is the constructivist being
"counterproductive and needlessly provocative"? He is simply
interested in finer distinctions than the classical mathematician
wishes to make.

> These results do say that for all practical purposes, a mathematician can
> think of classical proofs and effectivity instead of constructivity when it
> comes to prenex arithmetical sentences.

Do they. I suppose that if you find constructivity repugnant, then you
might celebrate these results. But what if you find constructivity
attractive? Is constructive proof so hard to understand that we have
to talk about Pi-0-n, recursive functions, PA, HA, and prenex
arithmetical sentences in order to grasp it?

--Fred