Changes

====2.4.1.  Syntactic Transformation Rules====

====2.4.1.  Syntactic Transformation Rules====

A good way to summarize these translations and to organize their use in practice is by means of the ''syntactic transformation rules'' (STRs) that partially formalize them.  A rudimentary example of a STR is readily mined from the raw materials that are already available in this area of discussion.  To begin, let the definition of an indicator function be recorded in the following form:

A good way to summarize these translations and to organize their use in practice is by means of the ''syntactic transformation rules'' (STRs) that partially formalize them.  Rudimentary examples of STRs are readily mined from the raw materials that are already available in this area of discussion.  To begin, let the definition of an indicator function be recorded in the following form:

<br>

<br>

<br>

<br>

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 of two logically equivalent expressions or sentences for the other in a context where the conditions of using the definition in this way are satisfied and where the change is perceived as potentially advancing a proof.  The employment of a definition in this way can be expressed in the form of an 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&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 for their normal or typical orders of exchange, since this can vary widely from case to case.

<br>

<br>