Changes

In practice, a definition like this is commonly used to substitute one logically equivalent expression or sentence for another in a context where the conditions of using the definition this way are satisfied and where the change is perceived to advance a proof.  This employment of a definition can be expressed in the form of a STR that allows one to exchange two expressions of logically equivalent forms for one another in every context where their logical values are the only consideration.  To be specific, the ''logical value'' of an expression is the value in the boolean domain <math>\underline\mathbb{B} = \{ \underline{0}, \underline{1} \} = \{ \operatorname{false}, \operatorname{true} \}</math> that the expression stands for in its context or represents to its interpreter.

In practice, a definition like this is commonly used to substitute one logically equivalent expression or sentence for another in a context where the conditions of using the definition this way are satisfied and where the change is perceived to advance a proof.  This employment of a definition can be expressed in the form of a STR that allows one to exchange two expressions of logically equivalent forms for one another in every context where their logical values are the only consideration.  To be specific, the ''logical value'' of an expression is the value in the boolean domain <math>\underline\mathbb{B} = \{ \underline{0}, \underline{1} \} = \{ \operatorname{false}, \operatorname{true} \}</math> that the expression stands for in its context or represents to its interpreter.

In the case of Definition&nbsp;1, the corresponding STR permits one to exchange a sentence of the form <math>x \in Q</math> with an expression of the form <math>\upharpoonleft Q \upharpoonright (x)</math> in any context that satisfies the conditions of its use, namely, the conditions of the definition that lead up to the stated equivalence.  The relevant STR is recorded in Rule&nbsp;1.  By way of convention, I list the items that fall under a rule roughly in order of their ascending conceptual subtlety or their increasing syntactic complexity, without regard to their normal or typical orders of exchange, since this can vary widely from case to case.

In the case of Definition 1, the corresponding STR permits one to exchange a sentence of the form "u C X" with an expression of the form "{X}(u)" in any context that satisfies the conditions of its use, namely, the conditions of the definition that lead up to the stated equivalence.  The relevant STR is recorded in Rule 1.  By way of convention, I list the items that fall under a rule roughly in order of their ascending conceptual subtlety or their increasing syntactic complexity, without regard to their normal or typical orders of exchange, since this can vary from widely from case to case.

 

 

 

then the following are equivalent:

| style="border-left:1px solid black" | <math>\text{then}\!</math>

| <math>\text{the following are equivalent:}\!</math>

 

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 X c U and for all u C U:

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