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

This helper adopts the setting of Sets and Maps: Ordinary Notation; it is a statement of the metatheory about formulas and expressions. Let $k\ge0$, the distinct set variables $x_{1},\dots,x_{k}$, the parameters and their values, and assignments be as in Conditions Expressed by a Predicative Formula, and Guards §data; let $\gamma$ be a guard; let terms and their values be as in Terms and Typed Terms under a Guard §term, terms of type $A$ under $\gamma$ as in Terms and Typed Terms under a Guard §typed-term, and conditions expressed by a predicative formula as in Conditions Expressed by a Predicative Formula, and Guards §expressed. Throughout, the parameters have fixed values, as in Conditions Expressed by a Predicative Formula, and Guards §data.

¶ Let $1\le i\le k$ and let $A$ be a class such that $x_{i}\in A$ under every assignment satisfying $\gamma$. Then $x_{i}$ is a term of type $A$ under $\gamma$.

¶ Let $A$ be a class and let $c$ be a variable other than $x_{1},\dots,x_{k}$ whose value is a set with $c\in A$. Then $c$ is a term of type $A$ under $\gamma$.

¶ Let $A$ and $B$ be classes, let $F$ be a variable other than $x_{1},\dots,x_{k}$ whose value is a map $F:A\to B$, and let $t$ be a term of type $A$ under $\gamma$. Then the term $F(t)$, the value of $F$ at $t$, is a term of type $B$ under $\gamma$.

¶ Let $A$ and $B$ be classes, let $s$ be a term of type $A$ under $\gamma$, and let $t$ be a term of type $B$ under $\gamma$. Then the ordered pair $(s,t)$ is a term of type $A\times B$ under $\gamma$, where $A\times B$ is the Cartesian product.

¶ Let $A$ and $B$ be classes, let $s$ be a term of type $A$ under $\gamma$, and let $t$ be a term of type $B$ under $\gamma$. Then the condition $\gamma\wedge s=t$ on $x_{1},\dots,x_{k}$, that is, "$\gamma$ holds and the sets $s$ and $t$ are equal", is expressed by a predicative formula.

¶ Let $A$ be a class, let $t$ be a term of type $A$ under $\gamma$, and let $C$ be a variable other than $x_{1},\dots,x_{k}$. Then the condition $\gamma\wedge t\in C$ on $x_{1},\dots,x_{k}$, that is, "$\gamma$ holds and the set $t$ is an element of $C$", is expressed by a predicative formula.

¶ In this clause, $k=1$ and $\gamma$ is $x\in D$, where $x$ is $x_{1}$ and $D$ is a variable other than $x$ whose value is a set. Let $s$ and $t$ be terms each of some type under $\gamma$, let $C$ be a variable other than $x$, and let $\psi_{=}$ and $\psi_{\in}$ be predicative formulas expressing the conditions $\gamma\wedge s=t$ and $\gamma\wedge t\in C$, as provided by the clauses equation and membership. Then the classes $\{x\in D:\psi_{=}\}$ and $\{x\in D:\psi_{\in}\}$ of Class Abstraction: the Class of All Sets Satisfying a Predicative Formula §restricted are sets, which do not depend on the choice of $\psi_{=}$ and $\psi_{\in}$ and are written $\{x\in D:s=t\}$ and $\{x\in D:t\in C\}$. For every set $a$: $a\in\{x\in D:s=t\}$ if and only if $a\in D$ and $s=t$ with $a$ assigned to $x$; and $a\in\{x\in D:t\in C\}$ if and only if $a\in D$ and $t\in C$ with $a$ assigned to $x$.