[FOM] Artificial sweetener for ZFC

[Joe Shipman]

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