[FOM] Artificial sweetener for ZFC

[Arnon Avron]

It is somewhat annoying for me (as I guess it has been
for Larry Paulson) to repeatedly read on FOM
about the need to develop `a suitably "sugared" version of ZFC',
and then attempts to do it  from scratch  like in the message
below -  as if no such versions (or at least proposed candidates)
are already available. I have already mentioned here (with references
to published papers) the framework I have developed exactly
for this task. So this time I am attaching a short description
of it (whose  abstract is included below), as well
as the slides of an invited  talk I gave about it five years ago.
(In the next IJCAR I am going to deliver another invited talk on the
subject, which will include also recent works on applying the framework
in the study of predicative mathematics and for what I call
"computational universes"). Let me note here
that the fact that the main ideas and principles were
taken from the theory of finite databases supports
(to some degree) Harvey Friedman's Thesis about the
strong connections between the principles that govern
the universe of ZFC and those that hold in the universe of
finite sets.

 Now maybe Harvey or others might think that this is not
what they are looking for, or that it is not good enough,
or even (this is also legitimate!) that the ideas on which my 
work is based are rather stupid. If so - please tell me (on 
FOM or privately) what do you think is lacking and/or is wrong.

Arnon Avron

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

We present a unified framework for formalizations of axiomatic set
theories of different strength, from rudimentary set theory to full ZF.
It allows the use of set terms, but provides a *static* check of
their validity.  Like the inconsistent ``ideal calculus" for set theory,
it is essentially based on just two set-theoretical principles:
extensionality and comprehension (to which we add epsilon-induction and
optionally the axiom of choice).  Comprehension is formulated as:
x\in{x:A}<->A, where {x:A} is a legal set term of the language. (The
formula A itself may contain of course other valid set terms.)  In order
for {x:A} to be legal, A should be *safe* with respect to {x},
where safety is a relation between formulas and finite sets of variables.
The various systems we consider differ from each other mainly with
respect to the safety relations they employ. These relations are all
defined purely syntactically (using an induction on the logical structure
of formulas).  The basic one is based on the safety relation which
implicitly underlies commercial query languages for relational database
systems (like SQL).  Our framework makes it possible to
reduce all extensions by definitions to abbreviations. Hence
it is convenient for mechanical manipulations and for interactive
theorem proving. It also provides a unified treatment of comprehension
axioms and of absoluteness properties of formulas.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


On Tue, Mar 29, 2016 at 11:03:14AM -0400, Joe Shipman wrote:
> Harvey, you talk about a suitably "sugared" version of ZFC as a useful basis for machine formalization. What would such sweetening consist of? Here is one attempt.
> 
> Bare ZFC does not even need the = symbol, because you can make equality a defined relation and rewrite Extensionality as "sets with the same members are members of the same sets". To sweeten this, introduce
> 
> 1) equality relation symbol, as just described (may have full Extensionality or allow urelements and have Extensionality only for sets with at least one element)
> 2) pairing, union, and powerset function symbols, emptyset constant symbol, and global choice function symbol, replacing corresponding axioms with definitions of what their elements are (in the last case, with the axiom that Ch(X) is an element of X if X is not empty)
> 3) ordered pair function symbol and corresponding projection functions with appropriate definitions, notations for set intersection and set of functions from A to B with appropriate definitions (can define [x,y]={{x},{x,y}} but this is unnecessary)
> 4) Replacement and separation schemes (alternatively, an NBG style set-class setup with sets being those classes which are elements of other classes and a global comprehension axiom scheme and a limitation of size axiom)
> 5) add constant symbols for N, Z, R, C, 0, 1 and Successor and + and - function symbols and usual axioms for 1st and 2nd order arithmetic and complete ordered fields (can define 0=emptyset and S(x)=U(x,{x}) and N = omega but this is not necessary) and inclusion maps from N to Z to R to C if desired.
> 
> Note that there is no coding needed to work with the system, we just expand the language in a standard way. The whole reason for all the coding is to show that you can get away with a single 2-place relation symbol but mathematical practice need not be so restricted. The axiom of foundation doesn't contradict anything done so far so you can add it if you want!
> 
> -- JS
> 
> Sent from my iPhone
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
A non-text attachment was scrubbed...
Name: set-theories.pdf
Type: application/pdf
Size: 204513 bytes
Desc: not available
URL: </pipermail/fom/attachments/20160402/1ccb460d/attachment-0002.pdf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: set-theories-slides.pdf
Type: application/pdf
Size: 117936 bytes
Desc: not available
URL: </pipermail/fom/attachments/20160402/1ccb460d/attachment-0003.pdf>