FOM: Effective Bounds in Core Mathematics

[Harvey Friedman]

Reply to Richman 3:35PM 6/27/00:

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

Under my suggestion, a constructivist would be defined as "someone who
studies constructivity in mathematics, or constructive proofs". This is
analogous to a proof theorist as "someone who studies formal proofs" or a
topologist as "someone who studies topological spaces".

I still don't see why it is attractive, or even reasonable, to take the
point of view that I put in between *'s above. As I said before, it is
counterproductive and needlessly provocative. Furthermore, it almost
guarantees that most logicians and mathematicians will not study
constructivity.

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

Taking a counterproductive and needlessly provocative stance like * needs a
justification such as this. Otherwise, it is just counterproductive and
needlessly provocative.

Here is a weaker version of * that is arguably productive and friendly:

**a constructive proof of an arithmetic sentence is preferable to a
classical proof of that arithmetic sentence**

Of course, the typical retort is: why? A good response is: it gives more
information. And this leads to important research programs that have only
been partially developed. Namely, systematically, just exactly what more
information is given, and in what form?, etcetera.

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

* is counterproductive and needlessly provocative, whereas ** is probably
not. Go test it out on your classical colleagues to see if I am right.
>
>> 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.

Yes, for their purposes. Maddy's naturalist would be happy to hear this.

>I suppose that if you find constructivity repugnant, then you
>might celebrate these results.

Almost everybody finds it repugnant when formulated in terms of *. Not in
terms of **. So I lot of people are potentially interested in such results.

>But what if you find constructivity
>attractive?

I find it attractive, but not in terms of *.

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

I was formulating a well defined research program of clear relevance to the
underlying issues. Let me state it more generally and perhaps more clearly.
Given a sentence in the language of PA, give interesting necessary and/or
sufficient criteria in ordinary classical terms (or at least neutral terms)
for it to be provable in HA. Naturally, this would involve provability in
PA.

E.g, Pi-0-2 sentence is provable in HA if and only if it is provable in PA.

But come to think of it, I have thought off and on about even giving a
sensible criterion for provability of sentences in PA. This seems very
difficult for Pi-0-1 sentences - and it seems like a problem of fundamental
importance. However, I know some ways of bootstrapping up - i.e., giving a
characterization in terms of PA provability of Pi-0-1 sentences.

To factor out this difficulty when coming to HA, a very good idea is to use
HA* instead of HA. HA* is a well known extension of HA by adding ordinary
induction for all primitive recursive presentations of actual well
orderings. There is no requirment that well foundedness be proved in any
particular way. So a problem is: when is a sentence of PA provable in HA*?
Incidentally, a sentence is provable in PA* if and only if it is true.

As a constructivist, one can state the thesis: a sentence of HA is provable
in HA* if and only if it is true. But it is well known that this is
refutable, constructively.