[FOM] the amazing language of set theory

[Charlie]

	   For foundational studies, why not use (a sort of)  “function theory” instead of set theory (different from Von Neumann’s f’n theory  modified by Bernays,…)  There are different ways to look at f’n theory.  I’m proposing that the ordered pair <x,y> be the primitive sentence, saying y is a function of x.  Intuitively, let’s say  of two books on your bookshelf that one (x) is left of the other (y).

	  There are many advantages (it seems to me).  One would be that functions are dynamic, whereas sets are static, thus applying instantly to computer programs  as well as math.  I’ll stop here and wait for replies, assuming my suggestion is not so simplistic as 1) to not even pass muster with the governors of FOM, and 2) to be completely ignored by the many ZF(C) advocates reading this (that is, assuming  (1) doesn’t hold and it is “published” on FOM).


Charlie Silver
P.S.  Before telling me sets and f'ns are interchangeable, I know that in a sense they are. (And {it seems to me that } f’n theory does not necessarily lead to a variant of NBG set theory.) (Why isn’t there an ‘R’ in the middle of NBG for Rafael Robinson?)

> On Mar 26, 2016, at 12:22 AM, Arnon Avron <aa at tau.ac.il> wrote:
> 
> 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
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom