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

[Martin Davis]

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