[FOM] classical/constructive mathematics

[Harvey Friedman]

There seems to be a resurgence of interest in comparisons between  
classical and constructive (foundations of) mathematics. This is a  
topic that has been discussed quite a lot previously on the FOM. I  
have been an active participant in prior discussions.

There was a lot of basic information presented earlier, and I think  
that it would be best to restate some of this, so that the discussion  
can go forward with its benefit.

In this message, I would like to focus on some important ways in which  
classical and constructive foundations are alike or closely related.

For many formal systems for fragments of classical mathematics, T,  
there is a corresponding system T' obtained by merely restricting the  
classical logical axioms to constructive logical axioms - where the  
resulting system is readily acceptable as a formal system for a  
"corresponding" fragment of constructive mathematics. Of course, there  
may be good ways of restating the axioms in the classical system,  
which do NOT lead to any reasonable fragment of constructive  
mathematics in this way.

The most well known example of this is PA = Peano Arithmetic. Suppose  
we formalize PA in the most common way, with the axioms for successor,  
the defining axioms for addition and multiplication, and the axiom  
scheme of induction, with the usual axioms and rules of classical  
logic. Then HA = Heyting Arithmetic, is simply PA with the axioms and  
rules of classical logic weakened to the axioms and rules of  
constructive logic.

Why do we consider HA as being a reasonable constructive system? A  
common answer is simply that a constructivist reads the axioms as  
"true" or "valid".

An apparently closely related fact about HA is purely formal. HA  
possesses a great number of properties that are commonly associated  
with "constructivism". The early pioneering work along these lines is,  
if I remember correctly, due to S.C. Kleene. Members of this list  
should be able to supply really good references for this work, better  
than I can. PA possesses NONE of these properties.

RESEARCH PROBLEM: Is there such a thing as a complete list of such  
formal properties? Is there a completeness theorem along these lines?  
I.e., can we state and prove that HA obeys all such (good from the  
constructive viewpoint) properties?

On the other hand, we can formalize PA, equivalently, using the *least  
number principle scheme* instead of the induction scheme. If a  
property holds of n, then that property holds of a least n. Then, when  
we convert to constructive logic, we get a system PA# that is  
equivalent to PA - thus possessing none of these properties!

For many of these T,T' pairs, some very interesting relationships  
obtain between the T and T'. Here are three important ones.

1. It can be proved that T is consistent if and only if T' is  
consistent.
2. Every A...A sentence, whose matrix has only bounded quantifiers,  
that is provable in T, is already provable in T'.
3. More strongly, every A...AE...E sentence, whose matrix has only  
bounded quantifiers, that is provable in T, is already provable in T'.

The issue arises as to just where these proofs are carried out - e.g.,  
constructively or classically. This is particularly critical in the  
case of 1. The situation is about as "convincing" as possible:

Specifically, for each of these results, one can use weak quantifier  
free systems K of arithmetic, where constructive and classical amount  
to the same. E.g., for 1, there is a primitive operation in K which,  
provably in K, converts any inconsistency in T to a corresponding  
inconsistency in T'.

Results like 1 point in the direction of there being no difference  
between the "safety" of classical and constructive mathematics.

Results like 2,3 point in the direction of there being no difference  
between the "applicability" of classical and constructive mathematics,  
in many contexts.

CAUTION: For AEA sentences, PA and HA differ. There are some  
celebrated A...AE...EA...A theorems of PA which are not known to be  
provable in HA. Some examples were discussed previously on the FOM.

RESEARCH PROBLEM: Determine, in some readily intelligible terms  
(perhaps classical), necessary and sufficient conditions for a  
sentence of a given form is provable in HA and PA. Matters get  
delicate when there are several quantifiers and arrows (-->) present.

I will continue with this if sufficient responses are generated.

Harvey Friedman