Terms and Typed Terms under a Guard

This definition, which adopts the setting of Sets and Maps: Ordinary Notation and belongs to the metatheory, describing expressions, takes $k$, the distinct set variables $x_{1},\dots,x_{k}$, displayed set variables, parameters with their fixed values, and assignments as in Conditions Expressed by a Predicative Formula, and Guards §data, guards as in Conditions Expressed by a Predicative Formula, and Guards §guard, and conditions expressed by a predicative formula as in Conditions Expressed by a Predicative Formula, and Guards §expressed. Set variables and class variables are as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols.

¶ The terms are the expressions obtained by finitely many applications of the following rules. Each set variable $x_{i}$, $1\le i\le k$, is a term, and so is each other variable, of either kind. If $f(v_{1},\dots,v_{m})$ is a defined set symbol, introduced as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols by a predicative formula $\theta(z,v_{1},\dots,v_{m})$ as an abbreviation in the sense of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols, and $t_{1},\dots,t_{m}$ are terms, then $f(t_{1},\dots,t_{m})$ is a term; examples are the ordered pair $(s,t)$ and the value $F(t)$ of a function $F$ (for $F(t)$, the symbol with the two arguments $F$ and $t$, $\theta(z,F,u)$ being $(u,z)\in F$, as in Functions, Values of a Function, and Functions from One Class to Another §value). Under an assignment of sets to $x_{1},\dots,x_{k}$, the value of a term is given, where defined, by the same recursion: the value of $x_{i}$ is the set assigned to $x_{i}$; the value of a parameter is its value; and the value of $f(t_{1},\dots,t_{m})$ is defined when the values of $t_{1},\dots,t_{m}$ are defined and are of the kinds that Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols requires of the arguments $v_{1},\dots,v_{m}$ of $f$, a set for each set variable among them, and exactly one set $z$ satisfies $\theta(z,v_{1},\dots,v_{m})$ when these values are assigned to $v_{1},\dots,v_{m}$; it is then that set $z$ (so the value depends only on the values of $x_{1},\dots,x_{k}$ and of the parameters). The defined set symbols of a term $t$ are said to be used properly under the assignment, in the sense of Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-set-symbols, when the value of $t$ is defined; this value is then also written $t$. A class variable is a term whatever its value, a proper class included.

¶ Let $\gamma$ be a guard and $A$ a class. A term $t$ is a term of type $A$ under $\gamma$ if ¶(a) under every assignment of sets to $x_{1},\dots,x_{k}$ satisfying $\gamma$, the value of $t$ is defined and is a set lying in $A$; and ¶(b) for every set variable $z$ other than $x_{1},\dots,x_{k}$ occurring neither in $\gamma$ nor in $t$, the condition $\gamma\wedge z=t$ on $x_{1},\dots,x_{k}$ and the displayed set variable $z$, that is, "$\gamma$ holds and $z$ is the set $t$", is expressed by a predicative formula, as in Conditions Expressed by a Predicative Formula, and Guards §expressed.