# [FOM] Are proofs in mathematics based on sufficient evidence?

Martin Davis eipye at pacbell.net
Thu Jul 8 20:17:41 EDT 2010

```I am astonished that on a list devoted to foundations of mathematics,
none of the comments on Vaughan Pratt's post has even mentioned the
valuable insights obtained in more than a century of  work in this field.

Gottlob Frege discovered the simple logical rules of inference that
underlie mathematical proofs. Published proofs are presented in a
level of detail thought to be appropriate for the intended audience.
What is appropriate for a first course introducing students to
rigorous proofs about limits and compactness is very different from
what is appropriate in an advanced textbook on real analysis, and
this in turn is much more elaborate than what would appear in a
professional journal. Carnap proposed the useful metaphor of a
microscope: if you don't understand how a certain step in a proof
follows from the previous steps, you turn up the power in Carnap's
microscope and the gap is filled by more detail. Just as a conceptual
microscope applied to matter will eventually reach down to the
molecular level, then to atoms, and then to the atomic constituents,
so Carnap's microscope will eventually reach down to steps belonging
to pure logic. Of course no mathematician will want to, or be able
to, read a proof of anything serious in which all of the steps have
been filled in. That's where computers come usefully into play as
much current research shows (despite the prognostications of R.A. de
Millo, R.J. Lipton and A.J. Perlis).

Already in 1933 G"odel outlined a foundation for mathematics based on
axioms for sets of higher and higher type (or rank as we would now
say) stretching into the transfinite. (See Feferman et al eds,
Collected Works, vol III, pp. 45-53.) The more or less canonical
Zermelo-Fraenkel axioms encapsulate this process up to a level
sufficient for almost all ordinary mathematics. G"odel pointed out
that his construction of an undecidable proposition carried out for
the set-theoretic hierarchy at a given level becomes provable at the
next level. There are those who find proofs in terms of the lower
levels of the hierarchy more convincing than those at higher levels,
thus providing better evidence for the truth of what is proved. Going
beyond what can be proved from the full Zermelo-Fraenkel axioms are
propositions that depend on assumptions about so-called large
cardinals. Harvey Friedman has been submitting many posts to FOM that
provide examples.

In addition to this mainstream development, are proposals to restrict
mathematics to what are thought to be more reliable methods, in
particular, either by requiring proofs of existence to provide
constructions (in a suitable sense) of the objects whose existence is
claimed, or to refuse to permit so-called impredicative definitions.
Researchers have proposed formal systems intended to encapsulate
these foundational stances, and much interesting work has shown how
these systems relate to one another and to mainstream foundations.

Martin Davis

```