12,089
edits
Changes
Directory:Jon Awbrey/Papers/Cactus Language (view source)
Revision as of 17:09, 25 January 2009
, 17:09, 25 January 2009→Syntactic Transformations: set box display
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 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:
<pre>
<br>
If X c U,
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black; border-bottom:1px solid black" width="90%"
|-
| align="left" style="border-left:1px solid black;" width="50%" |
| align="right" style="border-right:1px solid black;" width="50%" | <math>\text{Definition 1}\!</math>
|-
| colspan="2" style="border-left:1px solid black; border-right:1px solid black; border-top:1px solid black" |
<math>\begin{array}{ll}
\text{If} & Q \subseteq X
\\
\\
\text{then} & \upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}
\\
\\
\text{such that:}
\end{array}</math>
|-
| align="left" style="border-left:1px solid black; border-top:1px solid black" width="50%" |
<math>\begin{array}{ll}
\text{D1a.} & \upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q
\end{array}</math>
| align="right" style="border-right:1px solid black; border-top:1px solid black" width="50%" |
<math>\forall x \in X</math>
|}
<br>
<pre>
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 B = {false, true} = {0, 1} that the expression represents to its context or that it stands for in its context.
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 B = {false, true} = {0, 1} that the expression represents to its context or that it stands for in its context.