[FOM] classical/constructive mathematics
Harvey Friedman
friedman at math.ohio-state.edu
Wed Oct 15 00:36:36 EDT 2008
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
More information about the FOM
mailing list