[FOM] the amazing language of set theory

[WILLIAM TAIT]

Martin,

I’m not sure that the comparison with Descartes is sound. The advantage gained by Cartesian geometry was in ease of solving problems. No one would claim that translation of a problem—e.g.of analysis---into one in set theory generally makes it easier to solve. (The opponents of ‘set theoretic foundations’ often point to just this fact.) A real contribution of set theoretic foundations is that it provides ONE framework for all problems and the reasoning about their solutions. In each case, one can assume that the objects in question are in some universe of sets. The coherence of the statement of the problem and of the reasoning about it then becomes a question about the coherence of reasoning in one theory, namely set theory (together with whatever set theoretic assumptions the problem demands). 

I want to point out that this point of view is not an endorsement of the view that ‘everything in math is a set’. [As Dedekind (sort of) said: it is meaningless to ask whether 0 is an element of 1.]

But I also want to point out that the very virtues of the categorical / type-theoretical foundations, which I completely understand, preclude this particular virtue of set theoretic foundations. 

I suggest for this reason that many current arguments  about set-theoretic foundations versus (one’s favorite version of ) type theory just spin their wheels. Its nice that both are around.

Bill

On Mar 25, 2016, at 6:39 PM, Martin Davis <martin at eipye.com> 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