The Role of Formal Logic
In Zermelo’s original system, the Separation Axiom refers to a “definite property”. The Replacement Axiom refers to a “rule”. In 1922, Skolem proposed interpreting “definite” as “first-order definable”. So properties and rules are just formulas in the language of ZF, ℒ(ZF). With this clarification, ZFC assumes its modern form as a first-order theory.
ZF boasts a spartan vocabulary: just ∈ plus the basic symbols of first-order logic. Writing things out formally, with no abbreviations or short-cuts, rapidly snows us under unreadable expressions. We handle this (like everyone else) with semi-formal expressions; I like to call these “vernacular”. Copious hand-waving suggests how a masochist could write these out in the formal language ℒ(ZF).
Example: here’s how we say p=〈x,y〉={{x},{x,y}}, partially expanded:
∃a,b(p={a,b}∧a={x}∧b={x,y})
“∃a,b’’ is vernacular for “∃a∃b’’. Next we expand p={a,b} into
∀u(u∈p↔(u=a∨u=b))
and likewise for a={x} and b={x,y}.
A relation r is a set of ordered pairs, so more formally
(∀p∈r)∃a,b(p=(a,b))
which still has some vernacular. (∀p∈r)… more formally is ∀p(p∈r→…). Likewise, (∃x∈z)… in formal dress is ∃x(x∈z∧…).
To say f is a function with domain D, we start with the vernacular
f is a relation
∧ (∀(a,b)∈f)a∈D
∧ (∀a∈D) ∃!b((a,b)∈f)
“∀(a,b)∈f’’ expands to “(∀p∈f)∀a,b(p=(a,b)→…)’’. ∃!bφ(b), “exists a unique b satisfying φ’’, expands to ∃bφ(b)∧∀b,c(φ(b)∧φ(c)→b=c).
The vernacular f(x)=y becomes 〈x,y〉∈f. These should be enough to give you the flavor.
Often we have lists of variables, like x1,…xn. We write x̄ to reduce clutter; ∀x̄ and ∃x̄ have the obvious meanings.
When we get to the formal versions of Separation and Replacement, we’ll see how “property” and “rule” are made precise.
Coda
We’ve seen the informal use of “class” in ZF. This proved so convenient that NBG, a theory developed in succession by von Neumann, Bernays, and Gödel, gave a home to it. It turns out that NBG is a so-called conservative extension of ZFC: any formula of NBG that “talks only about sets” is provable in NBG iff it is provable in ZF.
In NBG, we still have only the symbol ∈ plus the basic logical symbols. However, certain members of the “universe” have the left-hand side of ∈ barred to them. If x∈y, then we say x is a set; anything that’s not a set is a proper class. So proper classes can have sets as elements, but cannot themselves be elements. The term class encompasses both sets and proper classes; in NBG, the variables range over classes.
Here’s how NBG skirts around Russell’s paradox. We can still write the formal expression R={x:x∉x}. This defines the class R, which is the class of all sets that are not elements of themselves. Is R∈R? No, because if it were, it would have to be a set that was not an element of itself. OK, if R∉R, doesn’t that mean that R satisfies the condition to be an element of R? No, not if R is a proper class—R contains only sets, no proper classes allowed!
Zermelo’s original system did not include Replacement and Foundation, although it did include Choice. Somewhat ahistorically, people use Z to refer to ZF minus Replacement, but including Separation. ZC is Z plus Choice.
ZF is a theory of “pure sets”. ZFA is “ZF with atoms”. An atom is an object that is not the null set but has no elements. The axioms of ZF can be modified to allow for this. Before the invention of forcing, Mostowski used ZFA to investigate theories without Choice.
Diagonal Argument 