Proof of Typed Terms under a Predicative Guard: Variables, Parameters, Values of Maps and Ordered Pairs, and Predicative Equations and Memberships between Them

Each result cited is universally quantified over the data in its own statement. Parameters and their fixed values, guards, terms under $\gamma$ and their values, terms of a type and conditions expressed by a predicative formula are as in Conditions Expressed by a Predicative Formula, and Guards §data, Conditions Expressed by a Predicative Formula, and Guards §guard, Terms and Typed Terms under a Guard §term, Terms and Typed Terms under a Guard §typed-term and Conditions Expressed by a Predicative Formula, and Guards §expressed; throughout, the parameters have their fixed values.

Preliminaries. The following facts about formulas are used throughout.

Fresh variables. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols the set variables form an infinite list, while finitely many formulas, terms and variables contain only finitely many variables. So for any finitely many of them there are as many distinct set variables as needed that are other than $x_{1},\dots,x_{k}$ and occur in none of them; such variables are called fresh below.

Compound formulas. For predicative formulas $\varphi$ and $\chi$ and a set variable $w$, every atomic formula and the formulas $(\varphi\wedge\chi)$ and $\exists w\,\varphi$ are predicative by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §predicative, since their parts of the form $\exists X\,\psi$ with $X$ a class variable are parts of $\varphi$ or $\chi$, and by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §free the free variables of $(\varphi\wedge\chi)$ are those of $\varphi$ and of $\chi$, and those of $\exists w\,\varphi$ are those of $\varphi$ other than $w$.

Reading. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading, $(\varphi\wedge\chi)$ holds if and only if both $\varphi$ and $\chi$ hold, and $\exists w\,\varphi$ holds if and only if there is a set $w$ for which $\varphi$ holds; and, as usual, whether a formula holds depends only on the values of its free variables.

Pair formulas. For distinct set variables $r$, $p$ and $q$ and distinct set variables $b_{1}$ and $b_{2}$ other than them, let $\omega(r,p,q)$ be the formula

$$\forall b_{1}\,\bigl(b_{1}\in r\Leftrightarrow(\forall b_{2}\,(b_{2}\in b_{1}\Leftrightarrow b_{2}=p)\vee\forall b_{2}\,(b_{2}\in b_{1}\Leftrightarrow(b_{2}=p\vee b_{2}=q)))\bigr)$$

of Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §ordered-pair, with $r$, $p$, $q$, $b_{1}$ and $b_{2}$ for $z$, $u$, $v$, $w$ and $t$ there. It is written with the abbreviations of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula, whose elimination introduces no quantifier over a class variable, so it quantifies over set variables only and is predicative by Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §predicative. By Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §free, every occurrence of $b_{1}$ and $b_{2}$ in it is bound, so its free variables are among $r$, $p$ and $q$. By Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §ordered-pair, when sets are assigned to $r$, $p$ and $q$, $\omega(r,p,q)$ holds if and only if $r=(p,q)$, the ordered pair of $p$ and $q$. Below, for distinct set variables $z$, $u$ and $v$, the expression $z=(u,v)$ denotes the formula $\omega(z,u,v)$ with $b_{1}$ and $b_{2}$ fresh for all other variables of the surrounding formula.

For a term $t$ of type $A$ under $\gamma$ and a set variable $w$ that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $t$, write $\psi_{t}^{w}$ for a predicative formula expressing $\gamma\wedge w=t$, as Terms and Typed Terms under a Guard §type-expressed provides: by Conditions Expressed by a Predicative Formula, and Guards §expressed, its free variables are among $x_{1},\dots,x_{k}$, $w$ and the parameters of $\gamma$ and $t$, and, the parameters having their values, under every assignment of sets to $x_{1},\dots,x_{k}$ and $w$, it holds if and only if $\gamma$ holds and $w$ is the set $t$.

Clause variable. Under every assignment satisfying $\gamma$, the value of $x_{i}$ is the set assigned to $x_{i}$, so $x_{i}$ is a term under $\gamma$ by Terms and Typed Terms under a Guard §term; and this set lies in $A$ by hypothesis. Let $z$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $x_{i}$, and let $\psi$ be the formula $(\gamma\wedge z=x_{i})$. It is predicative by the compound formulas fact, and its free variables are those of $\gamma$, which are among $x_{1},\dots,x_{k}$ and the parameters of $\gamma$, together with $z$ and $x_{i}$. By the reading fact, under every assignment of sets to $x_{1},\dots,x_{k}$ and $z$, $\psi$ holds if and only if $\gamma$ holds and $z$ is the set $x_{i}$.

Clause parameter. Likewise, with $c$ in place of $x_{i}$: its value, the same under every assignment, is a set lying in $A$ by hypothesis, so $c$ is a term under $\gamma$; and $\psi$ is the formula $(\gamma\wedge z=c)$, where $z$ is not $c$ since it does not occur in $c$.

Clause value. By Functions, Values of a Function, and Functions from One Class to Another §map, $F$ is a function with domain $\operatorname{dom}F=A$ and range $\operatorname{ran}F\subseteq B$, with $\subseteq$ as in Subclasses and Subsets §subclass.

First part. Consider an assignment satisfying $\gamma$. Since $t$ is of type $A$, the value of $t$ is a set lying in $A=\operatorname{dom}F$ by Terms and Typed Terms under a Guard §type-defined; so by Functions, Values of a Function, and Functions from One Class to Another §value exactly one set $v$ satisfies $(t,v)\in F$, and this set is the value $F(t)$ of $F$ at $t$, the value of $F(t)$ under the assignment. It is determined by the value of $t$ and the value of the parameter $F$, and the value of $t$ is determined by the sets assigned to $x_{1},\dots,x_{k}$ and the values of the parameters by Terms and Typed Terms under a Guard §term; so $F(t)$ is a term under $\gamma$ by Terms and Typed Terms under a Guard §term. As $(t,F(t))\in F$, the set $F(t)$ lies in $\operatorname{ran}F$ by Relations, Domain, Range, Inverse and Composition §range and Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, hence in $B$ by Subclasses and Subsets §subclass.

Second part. Let $z$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $F(t)$; so $z$ does not occur in $t$ and is not $F$. Choose distinct fresh set variables $w$ and $p'$ for $\gamma$, $t$, $F$ and $z$. Then $w$ is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $t$, so $\psi_{t}^{w}$ is defined. Let $\chi$ be the formula $\exists p'\,(p'=(w,z)\wedge p'\in F)$, with the pair formula $p'=(w,z)$, that is, $\omega(p',w,z)$. By the pair formulas fact and the compound formulas fact, $\chi$ is predicative and its free variables are among $w$, $z$ and $F$. Let $\psi$ be the formula $\exists w\,(\psi_{t}^{w}\wedge\chi)$. By the compound formulas fact, $\psi$ is predicative, and its free variables are among $x_{1},\dots,x_{k}$, $z$, the parameters of $\gamma$ and $t$, and $F$, that is, among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$ and $F(t)$. The variable $z$ is not free in $\psi_{t}^{w}$, being none of $x_{1},\dots,x_{k}$, not $w$, not free in $\gamma$ and not occurring in $t$, hence not a parameter of $\gamma$ or $t$.

Consider an assignment of sets to $x_{1},\dots,x_{k}$ and $z$, and let $w$ be a set. By the reading fact and the pair formulas fact, $\chi$ holds if and only if there is a set $p'$ with $p'=(w,z)$ and $p'\in F$, that is, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §pair-membership, if and only if $(w,z)\in F$. As the value of $F$ is a function, by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols §value this is the case if and only if $w\in\operatorname{dom}F$ and $z=F(w)$. By the reading fact and the property of $\psi_{t}^{w}$, $\psi$ holds if and only if there is a set $w$ such that $\gamma$ holds, $w$ is the set $t$, $w\in\operatorname{dom}F$ and $z=F(w)$. If $\gamma$ holds, $t$ is a set lying in $A=\operatorname{dom}F$ by the first part, and taking $w$ to be it shows that this holds if and only if $z=F(t)$. So $\psi$ holds if and only if $\gamma$ holds and $z$ is the set $F(t)$.

Clause pair. First part. Consider an assignment satisfying $\gamma$. Since $s$ is of type $A$ and $t$ of type $B$, the values of $s$ and $t$ are sets with $s\in A$ and $t\in B$ by Terms and Typed Terms under a Guard §type-defined. So exactly one set is the ordered pair of $s$ and $t$ of The Ordered Pair of Two Sets and Nested Tuples §pair, which is the value of $(s,t)$ under the assignment. It is determined by the values of $s$ and $t$, which are determined by the sets assigned to $x_{1},\dots,x_{k}$ and the values of the parameters by Terms and Typed Terms under a Guard §term, so $(s,t)$ is a term under $\gamma$ by Terms and Typed Terms under a Guard §term; and $(s,t)\in A\times B$ by Membership in a Cartesian Product, and the Cartesian Product of Two Sets Is a Set §membership.

Second part. Let $z$ be a set variable that is none of $x_{1},\dots,x_{k}$, is not free in $\gamma$ and does not occur in $(s,t)$, so it occurs in neither $s$ nor $t$. Choose distinct fresh set variables $u$ and $v$ for $\gamma$, $s$, $t$ and $z$. Then $\psi_{s}^{u}$ and $\psi_{t}^{v}$ are defined; let $\psi$ be the formula $\exists u\,\exists v\,(\psi_{s}^{u}\wedge(\psi_{t}^{v}\wedge z=(u,v)))$, with the pair formula $z=(u,v)$. By the compound formulas fact and the pair formulas fact, $\psi$ is predicative, with free variables among $x_{1},\dots,x_{k}$, $z$ and the parameters of $\gamma$, $s$ and $t$, which are those of $\gamma$ and $(s,t)$. The free variables of $\psi_{s}^{u}$ are among $x_{1},\dots,x_{k}$, $u$ and the parameters of $\gamma$ and $s$, so neither $v$ nor $z$ is free in it; likewise neither $u$ nor $z$ is free in $\psi_{t}^{v}$.

Consider an assignment of sets to $x_{1},\dots,x_{k}$ and $z$. By the reading fact, the properties of $\psi_{s}^{u}$ and $\psi_{t}^{v}$ and the pair formulas fact, $\psi$ holds if and only if there are sets $u$ and $v$ such that $\gamma$ holds, $u$ is the set $s$, $v$ is the set $t$, and $z$ is the ordered pair of $u$ and $v$. If $\gamma$ holds, $s$ and $t$ are sets by the first part, and taking $u$ and $v$ to be them shows that this holds if and only if $z$ is the ordered pair $(s,t)$. So $\psi$ holds if and only if $\gamma$ holds and $z$ is the set $(s,t)$.

Clause equation. Choose a fresh set variable $u$ for $\gamma$, $s$ and $t$. Then $\psi_{s}^{u}$ and $\psi_{t}^{u}$ are defined; let $\psi$ be the formula $\exists u\,(\psi_{s}^{u}\wedge\psi_{t}^{u})$. By the compound formulas fact it is predicative, with free variables among $x_{1},\dots,x_{k}$ and the parameters of $\gamma$, $s$ and $t$. Under an assignment of sets to $x_{1},\dots,x_{k}$, by the reading fact and the properties of $\psi_{s}^{u}$ and $\psi_{t}^{u}$, $\psi$ holds if and only if there is a set $u$ such that $\gamma$ holds and $u$ is both the set $s$ and the set $t$. If $\gamma$ holds, $s$ and $t$ are sets by Terms and Typed Terms under a Guard §type-defined, and there is a set $u$ with $u=s$ and $u=t$ if and only if $s=t$. So $\psi$ holds if and only if $\gamma$ holds and $s=t$.

Clause membership. Choose a fresh set variable $u$ for $\gamma$, $t$ and $C$, and let $\psi$ be the formula $\exists u\,(\psi_{t}^{u}\wedge u\in C)$. By the compound formulas fact it is predicative, with free variables among $x_{1},\dots,x_{k}$ and the parameters of $\gamma$, $t$ and $C$. Under an assignment of sets to $x_{1},\dots,x_{k}$, by the reading fact and the property of $\psi_{t}^{u}$, $\psi$ holds if and only if there is a set $u$ such that $\gamma$ holds, $u$ is the set $t$, and $u\in C$. If $\gamma$ holds, $t$ is a set by Terms and Typed Terms under a Guard §type-defined, and taking $u$ to be $t$ shows that this holds if and only if $t\in C$. So $\psi$ holds if and only if $\gamma$ holds and $t\in C$.

Clause set-builder. The formula $x\in D$ is atomic, hence predicative by the compound formulas fact, and its free variables are $x$ and the parameter $D$, so it is a guard by Conditions Expressed by a Predicative Formula, and Guards §guard. By the clauses equation and membership, formulas $\psi_{=}$ and $\psi_{\in}$ as in the statement exist; by Conditions Expressed by a Predicative Formula, and Guards §expressed their free variables are among $x$ and the parameters of $\gamma$, $s$, $t$ and $C$, all different from $x$. Since $\psi_{=}$ is predicative, Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted gives the class $\{x\in D:\psi_{=}\}$, which is the class $\{x:x\in D\wedge\psi_{=}\}$. Let $a$ be a set. By Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §abstraction, $a$ is an element of this class if and only if $a\in D$ and $\psi_{=}$ holds with $a$ assigned to $x$; since $\psi_{=}$ expresses $\gamma\wedge s=t$ and $\gamma$ is $x\in D$, this is the case if and only if $a\in D$ and $s=t$ with $a$ assigned to $x$. In particular every element of $\{x\in D:\psi_{=}\}$ lies in $D$, so it is a subclass of the set $D$ by Subclasses and Subsets §subclass, and hence a set 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 §subclass. Its elements do not depend on the choice of $\psi_{=}$, so two choices give the same class by Axiom of Extensionality for Classes. The same argument, with $\psi_{\in}$ and the condition $t\in C$, applies to $\{x\in D:\psi_{\in}\}$.