Conditions Expressed by a Predicative Formula, and Guards

This definition adopts the setting of Sets and Maps: Ordinary Notation and belongs to the metatheory: it describes formulas and expressions. Set variables, class variables, formulas and free variables are as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §symbols, Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §formula and Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §free, and a formula is predicative as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §predicative. An expression written with abbreviations as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §defined-symbols may be given for a formula; it stands for the formula obtained by eliminating them.

¶ Let $k\ge0$ be a metatheoretic number and let $x_{1},\dots,x_{k}$ be distinct set variables. A condition considered below is on $x_{1},\dots,x_{k}$ and on finitely many further set variables displayed with them, its displayed set variables, such as $y_{1},\dots,y_{m}$ in the clause expressed. The parameters of a formula are its free variables other than $x_{1},\dots,x_{k}$ and the displayed variables; of a term, that is, of an expression built from variables and defined set symbols, the variables occurring in it other than $x_{1},\dots,x_{k}$; of a condition stated by formulas and terms, those of these formulas and terms. The parameters have fixed values, given before anything else: a set for a parameter that is a set variable and a class for one that is a class variable, as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading, and a letter used for a parameter also denotes its value. Every notion below, and every statement using these notions, is relative to these values. Such a statement holds for all values of its parameters satisfying its hypotheses, and each of its hypotheses and conclusions, including those stating that a term has a type or that a condition is expressed by a predicative formula, refers to the same fixed values. Formulas are read as in Formulas of the Language of Class Theory, Free Variables, Predicative Formulas and Abbreviations §reading, with the parameters at their values, under assignments of sets to $x_{1},\dots,x_{k}$ and to the displayed set variables.

¶ Let $m\ge0$ be a metatheoretic number. A condition on $x_{1},\dots,x_{k}$, on displayed set variables $y_{1},\dots,y_{m}$ and on parameters is expressed by a predicative formula if there is a predicative formula $\psi$, whose free variables are among $x_{1},\dots,x_{k}$, $y_{1},\dots,y_{m}$ and the parameters of the condition, such that, the parameters having their values, under every assignment of sets to $x_{1},\dots,x_{k}$ and $y_{1},\dots,y_{m}$, $\psi$ holds if and only if the condition holds. Such a $\psi$ is said to express the condition.

¶ A guard is a predicative formula $\gamma$ whose free variables are among $x_{1},\dots,x_{k}$ and the parameters. An assignment of sets to $x_{1},\dots,x_{k}$ satisfies $\gamma$ if $\gamma$ holds under it.