Proof of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols

Each result cited is universally quantified over the data in its own statement. We work in Class Theory NBG: the Axioms, Standing Conventions and Basic Notation. Every element of a class is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §elements, so a quantifier over a set variable ranges over all possible elements of a class; and every set is a class, every object being a class by Classes, Membership, Sets and Proper Classes.

closure. Call an expression, possibly written with abbreviations, set-quantified if every quantifier occurring in it, including those in the formula $\psi$ of a class abstraction $\{x:\psi\}$ occurring in it, is applied to a set variable. Here $\forall v\,\varphi$ abbreviates $\neg\exists v\,\neg\varphi$ by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula and so counts as a quantifier on $v$, while $\vee$, $\Rightarrow$, $\Leftrightarrow$ and $\notin$ add no quantifier. The hypothesis of the clause says that the expression is set-quantified, and a formula without abbreviations is set-quantified exactly when it has no part $\exists X\,\psi$ with $X$ a class variable, that is, when it is predicative. An elimination step of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-predicates, Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols or Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §class-terms changes the expression only in the atomic part it replaces; the bound variables of the formula substituted there may be renamed (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols), and renaming replaces a bound variable by one of the same kind, so it does not change the kind of any quantifier. Substituting variables or terms for free variables creates no quantifier.

(a) Every predicative expression $D$ is set-quantified. The only formulas written inside an atomic part are the formulas of class abstractions occurring in it. A quantifier of $D$ outside its atomic parts is left in place by every elimination step, applied to the same variable, so it occurs in the formula finally obtained, which is predicative; hence it is applied to a set variable. A quantifier inside the formula $\psi$ of a class abstraction $\{x:\psi\}$ occurring in $D$ is handled by the same argument applied to $\psi$, which is predicative by the hypothesis of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula, by induction on the nesting depth of class abstractions.

(b) Each elimination step turns a set-quantified expression $E$ into a set-quantified expression. Consider the step that replaces an atomic part $\alpha$ of $E$. For a defined predicate, $\alpha$ is replaced by the predicative formula abbreviated (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-predicates), with the arguments written in $\alpha$ substituted for its variables; its quantifiers are those of that formula, applied to set variables by (a), and those of the arguments, which occur in $E$. For a defined set symbol $\tau$ with defining formula $\theta$, $\alpha(\tau)$ is replaced by $\exists z\,(\theta\wedge\alpha(z))$ (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols), where $z$ is a set variable, the quantifiers of $\theta$ are applied to set variables by (a), and those of $\alpha(z)$ occur in $E$. For a class term $T$, each replacing formula listed in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §class-terms is built from atomic formulas, membership formulas $\sigma_{T}$ (and $\sigma_{T'}$) and the quantifiers $\exists z$ and $\forall w$, with $z$ and $w$ set variables. If $T$ is a class abstraction $\{x:\psi\}$ written in $E$, then $\sigma_{T}$ is $\psi$ with $w$ for $x$ (Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction), whose quantifiers occur in $E$; otherwise $\sigma_{T}$ is the predicative formula with which $T$ is introduced, set-quantified by (a). In each case every quantifier of the new expression is applied to a set variable.

Let $E$ be set-quantified. The elimination of its abbreviations terminates by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols, so by (b) and induction on the number of steps the formula finally obtained is set-quantified. It contains no abbreviation, so it is predicative, and therefore $E$ is predicative by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols.

elimination. Fix sets $v_{1},\dots,v_{k}$ satisfying $\gamma$ and write $\tau$ for $\tau(v_{1},\dots,v_{k})$; here $\varphi(\tau,v_{1},\dots,v_{k})$ is the statement $\varphi$ about the set $\tau$, as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading. If $\varphi(\tau,v_{1},\dots,v_{k})$ holds, then $z=\tau$ satisfies $\theta\wedge\varphi$, so $\exists z\,(\theta\wedge\varphi)$. If some set $z_{0}$ satisfies $\theta(z_{0},v_{1},\dots,v_{k})\wedge\varphi(z_{0},v_{1},\dots,v_{k})$, then every set $z$ with $\theta(z,v_{1},\dots,v_{k})$ equals $z_{0}$, both being the unique such set $\tau$, so $\varphi(z,v_{1},\dots,v_{k})$ holds by substitution of equals (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols); thus $\forall z\,(\theta\Rightarrow\varphi)$. If $\forall z\,(\theta\Rightarrow\varphi)$ holds, applying it to $z=\tau$, which satisfies $\theta$, gives $\varphi(\tau,v_{1},\dots,v_{k})$. This closes the cycle of implications. By (a) in the proof of the closure clause above, $\gamma$, $\theta$ and $\varphi$ are set-quantified; the formulas $\gamma\wedge\exists z\,(\theta\wedge\varphi)$ and $\gamma\Rightarrow\forall z\,(\theta\Rightarrow\varphi)$ add to them only connectives and a quantifier on the set variable $z$, so they are set-quantified and hence predicative by the closure clause.

empty. By The Empty Set, the Unordered Pair and the Singleton §empty, $\emptyset$ is the unique set with no element, given by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §empty. Let $z$ be a set. If $z=\emptyset$, then $z$ has no element, so $\forall w\,(w\notin z)$. Conversely, if $\forall w\,(w\notin z)$, then $z$ has no element, since every element is a set; by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §empty there is exactly one set with no element, and $\emptyset$ is one, so $z=\emptyset$.

pair. By The Empty Set, the Unordered Pair and the Singleton §pair, $\{u,v\}$ is the unique set whose elements are exactly $u$ and $v$, given by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §pair. Let $u$, $v$, $z$ be sets. If $z=\{u,v\}$, then a set $w$ lies in $z$ if and only if $w=u$ or $w=v$. Conversely, if $\forall w\,(w\in z\Leftrightarrow(w=u\vee w=v))$, then $z$ and $\{u,v\}$ both have the property of Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §pair for the sets $u$ and $v$, so $z=\{u,v\}$ by the uniqueness there. By The Empty Set, the Unordered Pair and the Singleton §singleton, $\{u\}=\{u,u\}$, so $z=\{u\}$ if and only if $z=\{u,u\}$, if and only if $\forall w\,(w\in z\Leftrightarrow(w=u\vee w=u))$, if and only if $\forall w\,(w\in z\Leftrightarrow w=u)$.

ordered-pair. Let $u$, $v$, $z$ be sets. By The Ordered Pair of Two Sets and Nested Tuples §pair, $(u,v)=\{\{u\},\{u,v\}\}$, where $\{u\}$ and $\{u,v\}$ are sets by The Empty Set, the Unordered Pair and the Singleton §singleton and The Empty Set, the Unordered Pair and the Singleton §pair. The pair clause for the sets $\{u\}$, $\{u,v\}$ and $z$ gives: $z=(u,v)$ if and only if $\forall w\,(w\in z\Leftrightarrow(w=\{u\}\vee w=\{u,v\}))$. For each set $w$, the pair clause for the sets $u$, $v$ and $w$, with its bound variable renamed to $t$, gives: $w=\{u\}$ if and only if $\forall t\,(t\in w\Leftrightarrow t=u)$, and $w=\{u,v\}$ if and only if $\forall t\,(t\in w\Leftrightarrow(t=u\vee t=v))$. Replacing the two disjuncts by these equivalents yields the displayed formula.

pair-membership. Apply the elimination clause with $k=2$, the sets $u$, $v$ as $v_{1}$, $v_{2}$, the variable $p$ in the role of $z$, $\gamma(u,v)$ the formula $u=u$, and $\theta(p,u,v)$ the formula $p=(u,v)$, which contains no quantifier and so is predicative by the closure clause. For all sets $u$ and $v$, $\gamma$ holds, and exactly one set $p$ satisfies $p=(u,v)$: the ordered pair $(u,v)$ is a set by The Ordered Pair of Two Sets and Nested Tuples §pair, its constituents $\{u\}$ and $\{u,v\}$ existing uniquely by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §pair, and every set equal to it is it. So $\tau(u,v)$ is $(u,v)$. Let $A$ be a class, possibly a set. With $\varphi(p)$ the atomic formula $p\in A$, predicative since it contains no quantifier, and $A$ a parameter of $\gamma$, $\theta$ and $\varphi$, the elimination clause gives $(u,v)\in A$ if and only if $\exists p\,(p=(u,v)\wedge p\in A)$. By the ordered-pair clause, for every set $p$ the formula $p=(u,v)$ is equivalent to the displayed formula there, so the equivalence holds with $p=(u,v)$ in that form. For a relation $R$, $u\,R\,v$ means $(u,v)\in R$ by Relations, Domain, Range, Inverse and Composition §relation, which is the case $A=R$.

union-power. By The Union Set and the Power Set of a Set §union, $\bigcup u$ is the unique set whose elements are exactly the sets $w$ for which there is a set $v$ with $w\in v$ and $v\in u$, given by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §union. Let $u$ and $z$ be sets. If $z=\bigcup u$, then $\forall w\,(w\in z\Leftrightarrow\exists v\,(w\in v\wedge v\in u))$ by this definition. Conversely, a set $z$ satisfying this formula has, like $\bigcup u$, the property of Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §union for the set $u$, so $z=\bigcup u$ by the uniqueness there.

By The Union Set and the Power Set of a Set §power, $\mathcal{P}(u)$ is the unique set whose elements are exactly the subsets of $u$, given by Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §power. By Subclasses and Subsets §subclass, a set $w$ is a subset of $u$ if and only if $\forall v\,(v\in w\Rightarrow v\in u)$. So if $z=\mathcal{P}(u)$, then $\forall w\,(w\in z\Leftrightarrow\forall v\,(v\in w\Rightarrow v\in u))$; conversely, a set $z$ satisfying this formula has, like $\mathcal{P}(u)$, the property of Subclasses of Sets Are Sets, the Union and Power Set of a Set Exist Uniquely, Binary Unions of Sets Are Sets, and the Universal Class Is Proper §power for the set $u$, so $z=\mathcal{P}(u)$ by the uniqueness there.

class-terms. Fix values of $Y_{1},\dots,Y_{m}$, a set $u$ and a class $A$. That $u\in T$ if and only if $\psi(u,Y_{1},\dots,Y_{m})$ is Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction. If $A=T$, then for every set $w$, $w\in A$ if and only if $w\in T$, by substitution of equals (Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols), if and only if $\psi(w,Y_{1},\dots,Y_{m})$, by the first equivalence. Conversely, if $\forall w\,(w\in A\Leftrightarrow\psi(w,Y_{1},\dots,Y_{m}))$, then for every set $w$, $w\in A$ if and only if $w\in T$ by the first equivalence, so $A=T$ by Axiom of Extensionality for Classes.

If $A\in T$, then $A$ is a set by Elements Are Sets, and the Empty Set and the Pair of Two Sets Exist and Are Unique §elements, and $z=A$ satisfies $\forall w\,(w\in z\Leftrightarrow w\in A)$ and, by the first equivalence, $\psi(z,Y_{1},\dots,Y_{m})$. Conversely, let $z$ be a set with $\forall w\,(w\in z\Leftrightarrow w\in A)$ and $\psi(z,Y_{1},\dots,Y_{m})$. Then $z=A$ by Axiom of Extensionality for Classes, and $z\in T$ by the first equivalence, so $A\in T$ by substitution of equals.

class-operations. Let $u$, $v$, $z$ be sets. By The Boolean Operations on Classes, Disjointness, and the Universal Class §operations, with the bound variable renamed to $x$, the classes $u\cap v$, $u\cup v$ and $u\setminus v$ are the class abstractions $\{x:x\in u\wedge x\in v\}$, $\{x:x\in u\vee x\in v\}$ and $\{x:x\in u\wedge x\notin v\}$. Their formulas $x\in u\wedge x\in v$, $x\in u\vee x\in v$ and $x\in u\wedge x\notin v$ contain no quantifier, so they have no part $\exists X\,\psi$ and are predicative directly by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §predicative. The second equivalence of the class-terms clause above, with $m=2$, the parameters $u$ and $v$, and the set $z$ as the class $A$, gives the three displayed equivalences.

value. Let $u$ and $z$ be sets. Suppose $u\in\operatorname{dom}F$ and $z=F(u)$. By Functions, Values of a Function, and Functions from One Class to Another §value, $F(u)$ is the unique set $v$ with $(u,v)\in F$, so $(u,z)\in F$. Conversely, suppose $(u,z)\in F$. By Relations, Domain, Range, Inverse and Composition §domain, $\operatorname{dom}F=\{u:\exists v\,((u,v)\in F)\}$, and $z$ witnesses $\exists v\,((u,v)\in F)$, so $u\in\operatorname{dom}F$ by Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction. Then $F(u)$ is the unique set $v$ with $(u,v)\in F$ by Functions, Values of a Function, and Functions from One Class to Another §value, and $z$ is such a set, so $z=F(u)$.

operation. By Binary Operations on a Set §operation and Functions, Values of a Function, and Functions from One Class to Another §map, $\ast$ is a function with $\operatorname{dom}\ast=a\times a$. Let $u$, $v$, $z$ be sets; $(u,v)$ is a set by The Ordered Pair of Two Sets and Nested Tuples §pair. Suppose $u\in a$, $v\in a$ and $z=u\ast v$. Then $(u,v)\in a\times a=\operatorname{dom}\ast$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, and $u\ast v=\ast((u,v))$ by Binary Operations on a Set §notation; so $z=\ast((u,v))$, and the value clause, for the function $\ast$ and the set $(u,v)$, gives $((u,v),z)\in\ast$. Conversely, suppose $((u,v),z)\in\ast$. The value clause gives $(u,v)\in\operatorname{dom}\ast=a\times a$ and $z=\ast((u,v))$; then $u\in a$ and $v\in a$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership, and $u\ast v=\ast((u,v))=z$ by Binary Operations on a Set §notation.