| Line 6: |
Line 6: |
| | | | |
| | =====1.3.12.1. Syntactic Transformation Rules===== | | =====1.3.12.1. Syntactic Transformation Rules===== |
| − |
| |
| − | 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 in U.
| |
| − |
| |
| − | <pre>
| |
| − | o-------------------------------------------------o---------o
| |
| − | | Rule 3 | |
| |
| − | o-------------------------------------------------o---------o
| |
| − | | | |
| |
| − | | If X c U | |
| |
| − | | | |
| |
| − | | and u in U, | |
| |
| − | | | |
| |
| − | | then the following are equivalent: | |
| |
| − | | | |
| |
| − | o-------------------------------------------------o---------o
| |
| − | | | |
| |
| − | | R3a. u in X. | : R1a |
| |
| − | | | :: |
| |
| − | | R3b. -{X}-(u). | : R1b |
| |
| − | | | : R2a |
| |
| − | | | :: |
| |
| − | | R3c. -{X}-(u) = 1. | : R2b |
| |
| − | | | |
| |
| − | o-------------------------------------------------o---------o
| |
| − | </pre>
| |
| − |
| |
| − | A large stock of rules can be derived in this way, by chaining together segments that are selected from a stock of previous rules, with perhaps the whole process of derivation leading back to an axial body or a core stock of rules, with all recurring to and relying on an axiomatic basis. In order to keep track of their derivations, as their pedigrees help to remember the reasons for trusting their use in the first place, derived rules can be annotated by citing the rules from which they are derived.
| |
| − |
| |
| − | In the present discussion, I am using a particular style of annotation for rule derivations, one that is called "proof by grammatical paradigm" or "proof by syntactic analogy". The annotations in the right margin of the Rule box can be read as the "denominators" of the paradigm that is being employed, in other words, as the alternating terms of comparison in a sequence of analogies. This can be illustrated by considering the derivation Rule 3 in detail. Taking the steps marked in the box one at a time, one can interweave the applications in the central body of the box with the annotations in the right margin of the box, reading "is to" for the ":" sign and "as" for the "::" sign, in the following fashion:
| |
| − |
| |
| − | <pre>
| |
| − | R3a. "u in X" is to R1a, namely, "u in X",
| |
| − |
| |
| − | as
| |
| − |
| |
| − | R3b. "{X}(u)" is to R1b, namely, "{X}(u)",
| |
| − |
| |
| − | and
| |
| − |
| |
| − | "{X}(u)" is to R2a, namely, "f(u)",
| |
| − |
| |
| − | as
| |
| − |
| |
| − | R3c. "{X}(u) = 1" is to R2b, namely, "f(u) = 1".
| |
| − | </pre>
| |
| − |
| |
| − | Notice how the sequence of analogies pivots on the item R3b, viewing it first under the aegis of R1b, as the second term of the first analogy, and then turning to view it again under the guise of R2a, as the first term of the second analogy.
| |
| − |
| |
| − | By way of convention, rules that are tailored to a particular application, case, or subject, and rules that are adapted to a particular goal, object, or purpose, I frequently refer to as "Facts".
| |
| | | | |
| | Besides linking rules together into extended sequences of equivalents, there is one other way that is commonly used to get new rules from old. Novel starting points for rules can be obtained by extracting pairs of equivalent expressions from a sequence that falls under an established rule, and then by stating their equality in the proper form of equation. For example, by extracting the equivalent expressions that are annotated as "R3a" and "R3c" in Rule 3 and by explictly stating their equivalence, one obtains the specialized result that is recorded in Corollary 1. | | Besides linking rules together into extended sequences of equivalents, there is one other way that is commonly used to get new rules from old. Novel starting points for rules can be obtained by extracting pairs of equivalent expressions from a sequence that falls under an established rule, and then by stating their equality in the proper form of equation. For example, by extracting the equivalent expressions that are annotated as "R3a" and "R3c" in Rule 3 and by explictly stating their equivalence, one obtains the specialized result that is recorded in Corollary 1. |