[FOM] Role of Polemics

[Harvey Friedman]

This posting concerns the role of f.o.m. polemics, past and present.

The most common kind of f.o.m. polemic has the following form.

1. There are restrictions placed on allowable methods of proof. This can
either be a restriction on the rules of inference, or a restriction on the
kinds of mathematical objects allowed, or more subtle restrictions. The more
subtle restrictions may involve restrictions on the kinds of statements that
are allowed to be used in proofs, or restrictions on the form of properties
that can be used to form objects.

2. The polemical component consists of assertions of two basic kinds.

a. All of the existing "good" mathematics can be carried out within the
allowable methods. 

b. Use of the disallowed methods of proof is "invalid" in some sense.

3. Sometimes one simultaneously strengthens a and weakens b to:

c. All future "good" mathematics can be carried out within the allowable
methods.

4. The polemical nature of this setup becomes apparent because of the
absence of any convincing explanation as to what is "wrong" with the
disallowed methods, and the absence of any convincing explanation of what
"good" mathematics is.

*****************************************

There have been many polemics of this kind, including the most recent one in
http://www.cs.nyu.edu/pipermail/fom/2006-January/009581.html

It appears that polemics of this kind are considered now to be very
unconvincing - but nevertheless these polemics can be channeled along
productive lines.

The most common productive outlet for such polemics is a study of

i. What formal systems appropriately capture the allowable methods of proof.

ii. What existing theorems in the literature can or cannot be proved using
the restricted method of proof. Are they "good" or not?

iii. What "good" theorems, not in the literature, can or cannot be proved
using the restricted method of proof. After all, mathematics continually
evolves, with new "good" theorems created all the time. Moreover, on larger
time scales, new "good" subjects arise with lots of new "good" theorems.

******************************************

Let me now be more specific.

Let us start with the polemics against the law of excluded middle. This is
usually combined with complaints against certain kinds of mathematical
constructions. 

In the context of the ring of integers, complaints are not normally leveled
against mathematical constructions - the integers are usually accepted at
face value. 

The associated polemics have had very productive outlets.

First, Heyting formulated the important and surprisingly robust formalisms
of Heyting Propositional Logic, Heyting Predicate Calculus, and Heyting
Arithmetic (HA). 

Godel established deep relationships between these three systems and their
classical counterparts. These results tell us that we can interpret normal
classical reasoning in this intuitionistic framework.

In particular, Godel showed that any A...AE...E sentence provable in PA is
provable in HA, using his Dialectica interpretation. I found a hugely
simplified proof, using a purely syntactic manipulation, and showed that
this method works very generally - even in a broad variety of intuitionistic
set theories.  

These results have the effect of "reconciliation" between the classical and
intuitionistic points of view - at least in certain contexts.

But what about irreconcilable differences?

1. There are specific famous theorems in (essentially) the language of PA
which are not known to be provable in HA. In particular, various theorems in
Diophantine equations that assert "with finitely many exceptions", and also
in Diophantine approximation theory, also asserting "with finitely many
exceptions". These statements are Pi03.

2. To my knowledge, there is no famous theorem in (essentially) the language
of PA which is provable in PA, and KNOWN to be not provable in HA.

3. Concerning 2 in a different direction: I have conjectured that every
famous theorem in (essentially) the language of PA, is provable in EFA =
exponential function arithmetic. See http://www.andrew.cmu.edu/user/avigad/
Number theory and elementary arithmetic.

4. Perhaps one can find a genuine "real" theorem of PA that is not a theorem
of HA. 

5. There are stabs at 4 that are not fully convincing. At least, it appears
that one can productively attempt to find more and more convincing examples.

6. There is one I have proposed.

THEOREM A. Every polynomial of several variables, with integer coefficients,
assumes a value closest to the origin.

This is provable in PA but not in HA. In fact, it is provably equivalent,
over intuitionistic EFA, to classical Sigma01 induction. (EFA with
intuitionistic logic derives the axioms of EFA, and the law of excluded
middle for bounded formulas).

So Theorem A is in particular not provable in classical EFA.

7. However, one can still PRODUCTIVELY complain about Theorem A - that it is
more of a logical principle than a real theorem.

8. Note that 7 does not ENDORSE the complaint. One could also complain about
the complaint. 

9. In any case, it is a significant challenge to meet this complaint. But I
have no doubt that it can be met convincingly.

****************************************

Let us take another example. There are polemics associated with
predicativity. Associated formal systems were proposed by Schutte and
Feferman, and reworked by Feferman several times.

These formalisms have, to some extent, been criticized in various ways, and
some of these criticisms are based on polemics of their own. Others simply
express skepticism that there is a clear enough notion of predicativity to
support any kind of definitive analysis - thereby (trying to) shifting the
burden onto the analyzers of and supporters of predicativity.

After the formalisms of Schutte and Feferman became standard, basic work by
Feferman and others laid out how various mathematical developments are
normally done predicatively, and how various mathematical developments, not
normally done predicatively, could be done predicatively. Furthermore, there
were some examples of where predicative interpretations were impossible - in
various appropriate senses.

If I recall, these examples, given by Feferman and others, were Pi12, and as
noted, were not directly predicatively meaningful. The point is that the
Pi12 examples failed in the HYP sets, as noted. And, as noted, even if the
universal quantifiers were predicative objects - even recursively defined -
there was no predicative realization of the existential quantifier. EXAMPLE:
Every uncountable closed set of reals has a perfect subset.

But these examples are not at all fatal for the predicative point of view.
These Pi12 statements can be appropriately (for the predicativist)
rejected as false on ontological grounds - certain objects simply don't
exist, or at least cannot be demonstrated to exist, predicatively.

Call the above the ONTOLOGICAL DEFENSE.

There remained the very basic and essential question of whether there were
any "good" examples of mathematical theorems, which could not be proved
predicatively - but where the examples are not subject to the ontological
defense.

This set the stage for the key events:

1. The celebrated Kruskal tree theorem is Pi11 and cannot be proved
predicatively (on the Feferman Schutte analysis).

2. The celebrated graph minor theorem is Pi11 and cannot be proved
predicatively (on the Feferman Schutte analysis).

3. In fact, even if one extends the analysis of predicativity to the
substantially stronger system Pi11-CA0, or ID<omega, one also has the
unprovability, for the GMT (2 above).

4. I have started to talk to Neil Robertson here, about what axioms are
required to prove the graph minor theorem. We know that Pi11-CA is enough
for EKT, and Pi11-CA0 is not enough for EKT and GMT. It appears that Pi11-CA
is not enough for the current proof of GMT, but just how much is enough for
the current proof of GMT is unclear at the moment.

Because the statements involved are Pi11, the ontological dodge is not
available. One can still ask for more: what if the statements are restricted
to predicatively pristine objects?

E.g., one can consider

Kruskal's theorem for primitive recursive infinite sequences of trees.
GMT for primitive recursive infinite sequences of graphs.

The same results apply. These statements are provably equivalent to the
1-consistency of the relevant theories.

Note that we have already completely eliminated the ontological aspect of
things with this formulation, without getting into finite forms.

One can complain that "primitive recursive" is not a nice mathematical
concept, and that, for some reason or another, one wants a nice mathematical
concept for this particular issue.

If so, then one can pass to the finite forms. These are directly Pi02 and
are well recognized by many to be "good". E.g., see
http://www.cs.nyu.edu/pipermail/fom/2006-January/009550.html

*******************************************

Now let us see how we can complain about the previous section.

1. We can introduce modified polemics and complain that KT and GMT above are
now provable in somewhat stronger systems, and hence cease to be
counterexamples to an altered thesis.

There should be no doubt that one can "chase" higher and higher systems, of
the kind that the new polemics put forward, with very similar new results,
even staying nicely in wqo. Of course, this is a significant challenge, but
I have no doubt that it can be met.

E.g., there is Igor Kriz's extension of my EKT. The Kriz proof uses
something like light faced Pi12-CA0, if I recall. We have no idea how strong
Kriz's extension of my EKT is, at this point.

2. We can complain that KT and GMT are celebrated mathematics, but NOT core
mathematics. I.e, KT and GMT are NOT "good enough", in some sense or
another. Again, this is a significant challenge, but again I have no doubt
that it can be met.

Experiences like the following convince me. When Bill Thurston was at
Princeton many years ago, and I was visiting there for a week, we talked
about KT and he became keenly interested in the proof, including the fact
that there were very unusual features of any proof of KT. I gave a lecture
on the spot to Bill and a student or two of his, on one of the convenient
blackboards in the hall.

3. We can complain about using finite sequences in the Pi02 forms of KT and
GMT. As mentioned before on the FOM, I gave Pi02 forms of KT that involve a
single tree only, and this appears in Lecture Notes in Logic, in honor of
Sol Feferman. These involve structural properties of tall thin finite trees.

4. We can complain that the structural properties proved for tall thin
finite trees are too special or not systematic enough or don't have enough
clear geometric meaning, etcetera. Again I have no doubt that one can make
substantial improvements of various kinds.

*******************************************

There are many additional polemics that seem a lot "safer" than the
preceding ones.

It has always been considered VERY SAFE to complain about big set theory
such as ZFC, and more so about the biggest set theory - ZFC with large
cardinals. 

In particular, it has been considered to be a SAFE POLEMIC that the
underlying set concept behind ZFC and especially ZFC with large cardinals,
is useless for something "good".

Especially, it is considered VERY SAFE to complain that high powered set
theory is useless for something "good and finite".

BUT now we have http://www.cs.nyu.edu/pipermail/fom/2006-January/009565.html

Of course, one can continue the supposedly safe polemic in many ways.

1. These examples in finite graph theory are not "good".

They are getting better very rapidly. See the next few postings.

2. They are still not good enough.

But they will probably be "endorsed" in some public way by experts in graph
theory.

3. Graph theory is not good enough.

A significant challenge is to transfer these examples into the realm of
other mathematical subjects such as applied graph theory, optimization,
combinatorial group theory, semilinear algebra, semialagebraic geometry,
algebraic geometry, real analysis, complex analysis, functional analysis,
topology, geometry, etc.

The examples in finite graph theory are getting fundamental enough to
warrant full blown optimism about this.

4. Here is a complaint that one expects from philosophy and computer
science, and, perhaps from mathematics farther down the road: The concept of
arbitrary integer is the root of this evil. There are, after all,
nonstandard models.

5. Results are coming in that are of the following form.

The Pi01 sentences have positive integer parameters. Some of them have the
following property. When the parameters are set to be reasonable numbers
like, say, 8!!, one obtains a sentence B that involves only finitely many
objects (say at most 8!!! objects), such that

B is provable using large cardinals, in about 20 pages.
B is not provable in ZFC with abbreviations, without using more than 2^1000
pages.

6. Furthermore, any remotely reasonable standard of naturalness and
endorsements by experts in numerous fields, will be met, even for 5.

7. Some set theorists will complain that the statements involved only use
"small large cardinals". This will be completely overcome, with statements
at the level of VB + j:V into V, and higher.

8. Again, this will be ultimately put into forms that meet any remotely
reasonable standards of naturalness, and endorsements by experts in numerous
fields across mathematics, including applied mathematics.

********************************

THANK YOU, polemicists! May your retreats and retractions and reformulations
be eloquent!!

Harvey Friedman