FOM: classical vs. intuitionistic logic

[Harvey Friedman]

My reading of Tennant's 5:30PM 10/15/98, and 11:45AM 10/18/98, is that
Tennant is advocating that mathematicians and also scientists reject
adherence to the generally accepted axioms and rules of classical logic,
and instead adhere to something akin to the usual axioms and rules of
intuitionistic logic (or less). Evidently this is also Simpson's reading of
Tennant's postings.

I regarded this as sufficiently preposterous that I spoke to Tennant about
it. He instantaneously denied having advocated this!

However!!!, Tennant writes:

 > The classical mathematical theorems sort of "melt away" and vanish
 > from the proof, in IR, of the main refutational result.  ...
 > As a tough-minded fellow, shouldn't you too throw away your
 > crutches (i.e., the law of excluded middle)?

Isn't is reasonable for us to interpret "shouldn't you too throw away your
crutches (i.e., the law of excluded middle)?" as advocating this?

This is quite typical of what happens on the fom list, where people are
from such disparate intellectual cultures and write so much differently.
Obviously, in order to avoid confusion, Tennant should clearly have stated
that he was not advocating this. Or state - as he appears to be - that he
is advocating this.

Thus I have no clear idea what the disagreement is about, if any. This is a
familiar theme on the fom. That is, people don't make clear exactly what
their disagreements are, and don't make clear what they are not saying. I
suggest that fom posters take a guess as to what the probable
misinterpretations are inevitably going to be of their postings, and modify
their postings accordingly.

It seems like all three of us - Simpson, Tennant and myself - agree that
classical logic is much more convenient and standard than alternatives, and
that there are good reasons to believe thet the use of classical logic is
best for the formalization of mathematics and natural science, and that
this can be justified in a number of different ways, even if one thinks
that it needs any justification.

**Perhaps Tennant thinks that he has the best justification of all for it,
that is superior to other justifications?**

There are a lot of interesting points regarding the relationship between
classical and intuitionistic mathematics. But they need further analysis
and clarification, and have limitations.

1. Can classical mathematics be interpreted in intuitionistic mathematics?
2. Can classical mathematics be proved to be free of contradiction within
intuitionistic mathematics?
3. Can classical mathematics be proved to be free of contradiction relative
to intuitionistiic mathematics being free of contradiction?
4. To what extent can cuts be removed from proofs in classical or
intuitionistic mathematics?

I am not going to address issue 4 in this posting, as there is work in
progress.

Tennant seems to focus on some other way of "justifying" classical logic,
which I don't yet see as convincing, and which does not seem to be nearly
as strong as 1-3.

First of all, responses to 1-3 vary according to what is accepted as
classical mathematics and intuitionistic mathematics. Let's first discuss
these issues with regard to arithmetic. Here classical arithmetic - for
such purposes - is most normally identified with PA = Peano Arithemtic, and
intuitionsitic arithmetic - for such purposes - is most normally identified
with HA = Heyting's Arithmetic. In the normal setups, these systems differ
only in that the classical predicate calculus is used for the former, and
the intuitionistic predicate calculus is used for the latter.

The usual interpretation of PA into HA is as follows. One puts two nots in
front of every existential quantifier, and two nots in front of every
disjunction. Every sentence provable in PA becomes provable in HA when so
interpreted. Furthermore, any proof in PA remains a proof in HA when the
lines are so interpreted, where the intermediate steps are of course
uniformly filled in. There is no significant blowup in the size of the
resulting proof.

Now 3 is immediate given what I have just said.

2 can be addressed in two ways. Firstly, one can add a truth predicate to
HA for arithmetic formulas, and also expand induction to include all new
formulas. Call this HA'. Then HA' proves the consistency of HA. Combining
this with what we have said, we get that HA' proves the consistency of PA.

Another way of addressing 2 is this. Consider the following **nearly logic
free** system K with

	i) successor axioms;
	ii) equations for primitive recursive function symbols;
	iii) the scheme that "every unary primitive recursive function
stops descending through epsilon_0" stated with new function symbols
specifying a place at which it stops descending. There are side parameters
here, so that the new function symbols will not simply be new constant
symbols;
	iv) rule of induction for quantifier free formulas.

Here we don't have any quantifiers. Its just a free variable system. We
allow arbitrary connectives and classical propositional logic, and the rule
of substitution. But we could insist on a very stripped down set of
connectives and logic, although that perhaps is not too important a matter
since the only formulas considered are quantifier free.

This system proves the consistency of PA, and is nearly logic free, which
is saying a lot more than its being intuitionistic.

Now what if we take classical arithmetic to be sigma-0-1 induction, a
rather robust fragment of PA, that plays an important role in all sorts of
f.o.m. situations? On the intuitionistic arithemtic side, we could take
intuitionistic sigma-0-1 induction. But then this interpretation above does
not work. E.g., the double negation translation of an instance of sigma-0-1
induction need not be provable in intuitionistic sigma-0-1 induction.
[NOTE: I haven't actually had the time to prove this point, but it seems
right].

But how do we proceed?

One passes to PRA = primitive recursive arithmetic, which can also be given
a **nearly logic free** formulation as above. It is well known (originally
Parsons?) that every pi-0-2 sentence provable in sigma-0-1 induction is
provable in PRA, and hence in intuitionistic sigma-0-1 induction. NOTE: PRA
is a fragment of intuitionistic sigma-0-1 induction. Also, sigma-0-1
induction is consistent relative to PRA. As for issue 2, one can trivially
extend PRA to incorporate the Ackerman function given by equations. If you
do, then this extension proves the consistency of PRA, and therefore of
sigma-0-1 induction.

Now let us move beyond arithmetic. Suppose we use RCA_0 for classical
mathematics? Then by additional considerations discussed in Simpson's book,
we can replace everything we said above about sigma-0-1 induction by RCA_0.
Again, this is not even remotely done by a slavish double negation
interpretation of RCA_0. That would involve also putting double nots in
front of statements t epilson x.

Now lets move on to classical analysis. Nowadays, foundational people
normally generate classical analysis out of an underlying set theory. Reals
are built from sets of rationals. The last prominent mathematician to adopt
and advocate intuitionistic analysis was the classical analyst Errett
Bishop. He did not start from set theory, in any substantial form. He did
not accept any of the usual intuitionistic set theories as constructively
valid. Bishop, for one, never accepted impredicative methods as
constructively valid. Other intuitionists take the same view, although
Brouwer, with his theory of species liberally interpreted, could be taken
as someone who accepted at least some impredicative methods.

The relevance for this is as follows. The most straightforward ways of
formalizing classical analysis involve impredicative principles such as the
unrestricted least upper bound principle. There is not going to be any
intuitionistic reduction in the sense of 1,2,3, if intuitionistic
mathematics does not include impredicative methods.

It makes no sense to divorce the pure predicate calculus reasoning used
from the axioms that are used, when formalizing intuitionistic mathematics.
For instance, you can use exclusively intuitionistic predicate calculus if
your axioms include the law of excluded middle! And that cannot accomplish
anything.

On the other hand, there are less straighforward ways of formalizing
classical analysis that do not involve impredicative principles. These lend
themselves to reductions (in the sense of 1-3) to predicative systems, even
with intuitionistic logic, of the sort that most intuitionistis are
comfortable with. But this is not done by simple formal syntactic
translations.

Finally, there is full blown set theory. I investigated several forms of
intuitionistic ZF, including a particularly sensible one that is based on
the axiom scheme of collection. I showed a strong reduction of classical
ZFC to this intuitionistic ZF. This can be accomplished largely by
syntactic translation methods. However, there is a real question of the
acceptability of this IZF to intuitionists.