FOM: Effective Bounds in Core Mathematics

[Harvey Friedman]

Reponse to Richman 8:27AM 6/25/00:

>Harvey Friedman wrote:
>
>> Constructivists should also bear in mind that the truth of these four
>> theorems is completely accepted by the mathematical community.
>
>I'm not completely sure I understand the point of this statement. In
>their professional lives, constructivists constantly run into
>reminders that their criteria for justifying theorems differ from
>those of the mathematical community at large. There is little danger
>that they would stop being aware of this situation.
>
>So the only purpose I can see to the statement is to suggest that the
>complete acceptance of these four theorems by the mathematical
>community should give constructivists pause as to their denial that
>these theorems have been proved, as indeed it should. In this forum,
>however, that sociological card is an ungentlemanly one to play. I
>would respond to it were I sure that it had been played.
>
I don't know what "card" I may or may not be playing, but characterizing it
as "sociological" is misleading.

It is clear that a constructive proof of an arithmetic sentence (we can
only consider nonarithmetic sentences, too) is not the same as a classical
proof of an arithmetic sentence. On this, both constructivists and
classicists can agree.

I also agree with constructivists that the distinction is of great interest.

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.

It would make sense for someone to take this position if they had a single
instance where somebody had a classical proof of an arithemtical sentence
that later turned out to be refutable - even classically refutable.

But the constructivist generally has a constructive proof that this state
of affairs cannot happen. E.g., it is provable constructively that PA
(Peano Arithmetic) is free of contradiction.

As for the general mathematical community, they are definitely interested
in issues of effectivity. An interesting question is to what extent can we
replace the notion of constructive proof (say, first, of arithematical
sentences only) with classical proofs of related statements involving
recursive functions?

Again let us take HA (Heyting arithmetic) and PA (Peano arithmetic) as the
preferred vehicle for discussing this.

Suppose A is a Pi-0-2 sentence. Then A is provable in PA if and only if A
is provable in HA if and only if the effective form of A is provable in PA
if and only if the effective form of A is provable in HA.

Suppose A is a Pi-0-3 sentence. This is the form that occurs so often in
mathematics where issues of effectivity arise. Then A is provable in HA if
and only if the effective form of A is provable in HA. This much is clear
from standard results. But what if we replace the second HA by PA? We
can't. There is a counterexample.

However, this is almost true. In fact, it is almost true for prenex sentences.

THEOREM 1. Let A be a Pi-0-n sentence, n >= 1. The following are equivalent.
a) A is provable in HA.
b) the effective form of A is provable in HA.
c) there exists an algorithm alpha such that "alpha is a Skolem function
for A" is provable in HA.
d) there exists an algorithm alpha such that "alpha is a Skolem function
for A" is provable in PA.

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.

How about arithmetical formulas of the form

A implies B

where A,B are Pi-0-1 formulas?

The effective version is to go from a counterexample of B to a
counterexample of A, effectively.

THEOREM 2. The following are equivalent:
a) the implication is provable in HA.
b) the implication is provable in PA.
c) the effective version is provable in HA.
d) the effective version is provable in PA.

One can continue such a study. This touches on Godel's Dialectica
interpretation and forms of the no counterexample interpretation. But I
would surmise that the delicate issues where things behave badly are
perhaps in quantifier complexities which are outside the range of normal
mathematics.

It would be quite interesting to get a very clear idea of what arithmetical
sentences are provable in HA.

This kind of investigation is much harder for stronger theories involving
higher type objects.