Changes

Conversely, any rule of this sort, properly qualified by the conditions under which it applies, can be turned back into a summary statement of the logical equivalence that is involved in its application.  This mode of conversion a static principle and a transformational rule, that is, between a statement of equivalence and an equivalence of statements, is so automatic that it is usually not necessary to make a separate note of the "horizontal" versus the "vertical" versions.

Conversely, any rule of this sort, properly qualified by the conditions under which it applies, can be turned back into a summary statement of the logical equivalence that is involved in its application.  This mode of conversion a static principle and a transformational rule, that is, between a statement of equivalence and an equivalence of statements, is so automatic that it is usually not necessary to make a separate note of the "horizontal" versus the "vertical" versions.

As another example of a STR, consider the following logical equivalence, that holds for any <math>Q \subseteq X</math> and for all <math>x \in X.</math>

As another example of a STR, consider the following logical equivalence, that holds for any X c U and for all u C U:

{X}(u) <=>  {X}(u) = 1.

{| align="center" cellpadding="8" width="90%"

| <math>\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x) = \underline{1}.</math>

In practice, this logical equivalence is used to exchange an expression of the form "{X}(u)" with a sentence of the form "{X}(u) = 1" in any context where one has a relatively fixed X c U in mind and where one is conceiving u C U to vary over its whole domain, namely, the universe U.  This leads to the STR that is given in Rule 2.

In practice, this logical equivalence is used to exchange an expression of the form <math>\upharpoonleft Q \upharpoonright (x)</math> with a sentence of the form <math>\upharpoonleft Q \upharpoonright (x) = \underline{1}</math> in any context where one has a relatively fixed <math>Q \subseteq X</math> in mind and where one is conceiving <math>x \in X</math> to vary over its whole domain, namely, the universe <math>X.\!</math> This leads to the STR that is given in Rule&nbsp;2.

Rule 2

Rule 2

If f : U �> B

If f : U -> B

and u C U,

and u C U,

R2b. f(u) = 1.

R2b. f(u) = 1.

Rules like these can be chained together to establish extended rules, just so long as their antecedent conditions are compatible.  For example, Rules 1 and 2 combine to give the equivalents that are listed in Rule 3.  This follows from a recognition that the function {X} : U �> B that is introduced in Rule 1 is an instance of the function f : U �> B that is mentioned in Rule 2.  By the time one arrives in the "consequence box" of either Rule, then, one has in mind a comparatively fixed X c U, a proposition f or {X} about things in U, and a variable argument u C U.

Rules like these can be chained together to establish extended rules, just so long as their antecedent conditions are compatible.  For example, Rules 1 and 2 combine to give the equivalents that are listed in Rule 3.  This follows from a recognition that the function {X} : U -> B that is introduced in Rule 1 is an instance of the function f : U -> B that is mentioned in Rule 2.  By the time one arrives in the "consequence box" of either Rule, then, one has in mind a comparatively fixed X c U, a proposition f or {X} about things in U, and a variable argument u C U.

Rule 3

Rule 3