[FOM] the amazing language of set theory

[Martin Davis]

Descartes revolutionized mathematics by showing that geometry could be
reinterpreted in the language of algebra. This was not always the most
appropriate language for actually dealing with some specific geometric
problem. But of course that was not the point. To take just one example:
The calculus of Leibniz and Newton made area and volume calculations that
had required artful innovations by such as Eudoxus, Archimedes, Cavalieri,
and Torricelli, into student exercises. Of course, having the equations of
the relevant curves and surfaces was crucial.

The somewhat analogous twentieth century discovery that all of mathematics
can be reinterpreted into statements in the language of set theory (just
one binary relation, usually written as the Greek letter "epsilon") has
revolutionized not mathematical practice, but rather foundational studies.
It became clear that Zermelo's axioms suffice for the great bulk of
ordinary mathematics, and, when suitably augmented to form our familiar
ZFC, for transfinite mathematics as well.
Then techniques developed by Gödel and Cohen made it possible to see that
it had been impossible to resolve various problems that had been around for
a long time, only because the ZFC axioms were insufficient for their
proofs. Many other fascinating foundational results have been obtained.

In the ongoing discussion here on FOM, I don't think the distinction has
always been made between a foundation suitable as the starting point of
metamathematical investigations, and one suited for use in a computerized
proof verification system for use by mathematicians in certifying the
correctness of their work. The tradeoffs inevitably involved in the latter
case seem to me to make it to a considerable extent, an engineering
decision. Harvey Friedman advocates using set theory itself, of course not
in the raw form presented above, but nicely "sugared" to make it pleasant
for working mathematicians. It may not be amiss to mention that my late
colleague Jack Schwartz had developed such a system. The Italian logicians
Domenico Cantone, Eugenio Omodeo, and Alberto Policriti have been carrying
the development further.

Martin
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160325/aab8e2db/attachment.html>