[FOM] the amazing language of set theory

[Arnon Avron]

I totally agree, and would only like to add that I believe that
Liron Cohen and I have been carrying the development (which is 
mentioned at the end of Martin's message) even further in the 
following papers:

A. Avron
"A Framework for Formalizing Set Theories 
   Based on the Use of Static Set Terms",
 In:  Pillars of Computer Science (A. Avron, N. Dershowitz,
 and A. Rabinovich, eds.), 87--106, LNCS 4800, Springer, 2008.
 (available from: http://www.springerlink.com/content/w23475760624/)

A. Avron and  L. Cohen
"Formalizing Scientifically Applicable Mathematics 
                      in a Definitional Framework",
 JOURNAL OF FORMALIZED REASONING (special issue:
 Twenty Years of the QED Manifesto) 9 (2016), 53--70.


Arnon Avron


On Fri, Mar 25, 2016 at 04:39:03PM -0700, Martin Davis wrote:
> 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

> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom