Line 10,209: |
Line 10,209: |
| 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 between a static principle and a transformational rule, in other words, 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 of what amounts to the same abstract principle. | | 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 between a static principle and a transformational rule, in other words, 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 of what amounts to the same abstract principle. |
| | | |
− | <pre>
| + | As another example of a ROST, consider the following logical equivalence, that holds for any <math>X \subseteq U\!</math> and for all <math>u \in U.</math> |
− | As another example of a ROST, consider the | |
− | following logical equivalence, that holds | |
− | for any X c U and for all u in U: | |
| | | |
− | -{X}-(u) <=> -{X}-(u) = 1.
| + | : -{X}-(u) <=> -{X}-(u) = 1. |
| | | |
− | In practice, this logical equivalence is used to exchange | + | 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 in U to vary over its whole domain, namely, the universe U. This leads to the ROST that is given in Rule 2. |
− | 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 in U to vary | |
− | over its whole domain, namely, the universe U. This leads to | |
− | the ROST that is given in Rule 2. | |
| | | |
| + | <pre> |
| o-------------------------------------------------o | | o-------------------------------------------------o |
| | Rule 2 | | | | Rule 2 | |
Line 10,240: |
Line 10,233: |
| | | | | | | |
| o-------------------------------------------------o | | o-------------------------------------------------o |
| + | </pre> |
| | | |
− | Rules like these can be chained together to establish extended | + | 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. |
− | 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 | | o-------------------------------------------------o---------o |
| | Rule 3 | | | | | Rule 3 | | |
Line 10,271: |
Line 10,258: |
| | | | | | | | | |
| o-------------------------------------------------o---------o | | o-------------------------------------------------o---------o |
| + | </pre> |
| | | |
− | A large stock of rules can be derived in this way, by chaining together | + | 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. |
− | 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 | + | 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: |
− | 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", | | R3a. "u in X" is to R1a, namely, "u in X", |
| | | |
Line 10,304: |
Line 10,278: |
| | | |
| R3c. "{X}(u) = 1" is to R2b, namely, "f(u) = 1". | | 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. |
| | | |
− | Notice how the sequence of analogies pivots on the item R3b,
| + | 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". |
− | 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
| + | 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. |
− | application, case, or subject, and rules that are adapted to
| |
− | a particular goal, object, or purpose, I frequently refer to
| |
− | as "Facts". | |
− | </pre>
| |
| | | |
| <pre> | | <pre> |
− | 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.
| |
− |
| |
| Corollary 1 | | Corollary 1 |
| | | |
Line 10,335: |
Line 10,296: |
| | | |
| C1a. u C X <=> {X}(u) = 1. R3a=R3c | | C1a. u C X <=> {X}(u) = 1. R3a=R3c |
| + | </pre> |
| | | |
− | There are a number of issues, that arise especially in establishing the proper use of STR's, that are appropriate to discuss at this juncture. The notation "[S]" is intended to represent "the proposition denoted by the sentence S". There is only one problem with the use of this form. There is, in general, no such thing as "the" proposition denoted by S. Generally speaking, if a sentence is taken out of context and considered across a variety of different contexts, there is no unique proposition that it can be said to denote. But one is seldom ever speaking at the maximum level of generality, or even found to be thinking of it, and so this notation is usually meaningful and readily understandable whenever it is read in the proper frame of mind. Still, once the issue is raised, the question of how these meanings and understandings are possible has to be addressed, especially if one desires to express the regulations of their syntax in a partially computational form. This requires a closer examination of the very notion of "context", and it involves engaging in enough reflection on the "contextual evaluation" of sentences that the relevant principles of its successful operation can be discerned and rationalized in explicit terms. | + | There are a number of issues, that arise especially in establishing the proper use of ROSTs, that are appropriate to discuss at this juncture. The notation "[S]" is intended to represent "the proposition denoted by the sentence S". There is only one problem with the use of this form. There is, in general, no such thing as "the" proposition denoted by S. Generally speaking, if a sentence is taken out of context and considered across a variety of different contexts, there is no unique proposition that it can be said to denote. But one is seldom ever speaking at the maximum level of generality, or even found to be thinking of it, and so this notation is usually meaningful and readily understandable whenever it is read in the proper frame of mind. Still, once the issue is raised, the question of how these meanings and understandings are possible has to be addressed, especially if one desires to express the regulations of their syntax in a partially computational form. This requires a closer examination of the very notion of "context", and it involves engaging in enough reflection on the "contextual evaluation" of sentences that the relevant principles of its successful operation can be discerned and rationalized in explicit terms. |
| | | |
| A sentence that is written in a context where it represents a value of 1 or 0 as a function of things in the universe U, where it stands for a value of "true" or "false", depending on how the signs that constitute its proper syntactic arguments are interpreted as denoting objects in U, in other words, where it is bound to lead its interpreter to view its own truth or falsity as determined by a choice of objects in U, is a sentence that might as well be written in the context "[ ... ]", whether or not this frame is explicitly marked around it. | | A sentence that is written in a context where it represents a value of 1 or 0 as a function of things in the universe U, where it stands for a value of "true" or "false", depending on how the signs that constitute its proper syntactic arguments are interpreted as denoting objects in U, in other words, where it is bound to lead its interpreter to view its own truth or falsity as determined by a choice of objects in U, is a sentence that might as well be written in the context "[ ... ]", whether or not this frame is explicitly marked around it. |
Line 10,342: |
Line 10,304: |
| More often than not, the context of interpretation fixes the denotations of most of the signs that make up a sentence, and so it is safe to adopt the convention that only those signs whose objects are not already fixed are free to vary in their denotations. Thus, only the signs that remain in default of prior specification are subject to treatment as variables, with a decree of functional abstraction hanging over all of their heads. | | More often than not, the context of interpretation fixes the denotations of most of the signs that make up a sentence, and so it is safe to adopt the convention that only those signs whose objects are not already fixed are free to vary in their denotations. Thus, only the signs that remain in default of prior specification are subject to treatment as variables, with a decree of functional abstraction hanging over all of their heads. |
| | | |
− | [u C X] = Lambda (u, C, X).(u C X). | + | : [u C X] = Lambda (u, C, X).(u C X). |
| | | |
| As it is presently stated, Rule 1 lists a couple of manifest sentences, and it authorizes one to make exchanges in either direction between the syntactic items that have these two forms. But a sentence is any sign that denotes a proposition, and thus there are a number of less obvious sentences that can be added to this list, extending the number of items that are licensed to be exchanged. Consider the sense of equivalence among sentences that is recorded in Rule 4. | | As it is presently stated, Rule 1 lists a couple of manifest sentences, and it authorizes one to make exchanges in either direction between the syntactic items that have these two forms. But a sentence is any sign that denotes a proposition, and thus there are a number of less obvious sentences that can be added to this list, extending the number of items that are licensed to be exchanged. Consider the sense of equivalence among sentences that is recorded in Rule 4. |
| | | |
| + | <pre> |
| Rule 4 | | Rule 4 |
| | | |
Line 10,363: |
Line 10,326: |
| | | |
| R4e. {X}(u) = 1. | | R4e. {X}(u) = 1. |
| + | </pre> |
| | | |
| The first and last items on this list, namely, the sentences "u C X" and "{X}(u) = 1" that are annotated as "R4a" and "R4e", respectively, are just the pair of sentences from Rule 3 whose equivalence for all u C U is usually taken to define the idea of an indicator function {X} : U -> B. At first sight, the inclusion of the other items appears to involve a category confusion, in other words, to mix the modes of interpretation and to create an array of mismatches between their own ostensible types and the ruling type of a sentence. On reflection, and taken in context, these problems are not as serious as they initially seem. For instance, the expression "[u C X]" ostensibly denotes a proposition, but if it does, then it evidently can be recognized, by virtue of this very fact, to be a genuine sentence. As a general rule, if one can see it on the page, then it cannot be a proposition, but can be, at best, a sign of one. | | The first and last items on this list, namely, the sentences "u C X" and "{X}(u) = 1" that are annotated as "R4a" and "R4e", respectively, are just the pair of sentences from Rule 3 whose equivalence for all u C U is usually taken to define the idea of an indicator function {X} : U -> B. At first sight, the inclusion of the other items appears to involve a category confusion, in other words, to mix the modes of interpretation and to create an array of mismatches between their own ostensible types and the ruling type of a sentence. On reflection, and taken in context, these problems are not as serious as they initially seem. For instance, the expression "[u C X]" ostensibly denotes a proposition, but if it does, then it evidently can be recognized, by virtue of this very fact, to be a genuine sentence. As a general rule, if one can see it on the page, then it cannot be a proposition, but can be, at best, a sign of one. |
| | | |
− | The use of the basic connectives can be expressed in the form of a STR as follows: | + | The use of the basic connectives can be expressed in the form of a ROST as follows: |
| | | |
| + | <pre> |
| Logical Translation Rule 0 | | Logical Translation Rule 0 |
| | | |
Line 10,387: |
Line 10,352: |
| | | |
| L0c. [SurcJj Sj] = SurjJj [Sj] = SurjJj Pj. | | L0c. [SurcJj Sj] = SurjJj [Sj] = SurjJj Pj. |
| + | </pre> |
| | | |
− | As a general rule, the application of a STR involves the recognition of an antecedent condition and the facilitation of a consequent condition. The antecedent condition is a state whose initial expression presents a match, in a formal sense, to one of the sentences that are listed in the STR, and the consequent condition is achieved by taking its suggestions seriously, in other words, by following its sequence of equivalents and implicants to some other link in its chain. | + | As a general rule, the application of a ROST involves the recognition of an antecedent condition and the facilitation of a consequent condition. The antecedent condition is a state whose initial expression presents a match, in a formal sense, to one of the sentences that are listed in the STR, and the consequent condition is achieved by taking its suggestions seriously, in other words, by following its sequence of equivalents and implicants to some other link in its chain. |
| | | |
| Generally speaking, the application of a rule involves the recognition of an antecedent condition as a case that falls under a clause of the rule. This means that the antecedent condition is able to be captured in the form, conceived in the guise, expressed in the manner, grasped in the pattern, or recognized in the shape of one of the sentences in a list of equivalents or a chain of implicants. | | Generally speaking, the application of a rule involves the recognition of an antecedent condition as a case that falls under a clause of the rule. This means that the antecedent condition is able to be captured in the form, conceived in the guise, expressed in the manner, grasped in the pattern, or recognized in the shape of one of the sentences in a list of equivalents or a chain of implicants. |
Line 10,394: |
Line 10,360: |
| A condition is "amenable" to a rule if any of its conceivable expressions formally match any of the expressions that are enumerated by the rule. Further, it requires the relegation of the other expressions to the production of a result. Thus, there is the choice of an initial expression that needs to be checked on input for whether it fits the antecedent condition and there are several types of output that are generated as a consequence, only a few of which are usually needed at any given time. | | A condition is "amenable" to a rule if any of its conceivable expressions formally match any of the expressions that are enumerated by the rule. Further, it requires the relegation of the other expressions to the production of a result. Thus, there is the choice of an initial expression that needs to be checked on input for whether it fits the antecedent condition and there are several types of output that are generated as a consequence, only a few of which are usually needed at any given time. |
| | | |
| + | <pre> |
| Logical Translation Rule 1 | | Logical Translation Rule 1 |
| | | |
Line 10,413: |
Line 10,380: |
| | | |
| L1b11. [True] = (()) = 1 : U->B. | | L1b11. [True] = (()) = 1 : U->B. |
| + | </pre> |
| | | |
| + | <pre> |
| Geometric Translation Rule 1 | | Geometric Translation Rule 1 |
| | | |
Line 10,431: |
Line 10,400: |
| | | |
| G1b11. {U} = (()) = 1 : U->B. | | G1b11. {U} = (()) = 1 : U->B. |
| + | </pre> |
| | | |
| + | <pre> |
| Logical Translation Rule 2 | | Logical Translation Rule 2 |
| | | |
Line 10,475: |
Line 10,446: |
| | | |
| L2b15. [True] = (()) = 1 : U->B. | | L2b15. [True] = (()) = 1 : U->B. |
| + | </pre> |
| | | |
| + | <pre> |
| Geometric Translation Rule 2 | | Geometric Translation Rule 2 |
| | | |
Line 10,517: |
Line 10,490: |
| | | |
| G2b15. {U} = (()) = 1 : U->B. | | G2b15. {U} = (()) = 1 : U->B. |
| + | </pre> |
| | | |
− | | + | <pre> |
| Value Rule 1 | | Value Rule 1 |
| | | |
Line 10,534: |
Line 10,508: |
| | | |
| V1c. ((v , w)) | | V1c. ((v , w)) |
| + | </pre> |
| | | |
− | | + | <pre> |
| Value Rule 1 | | Value Rule 1 |
| | | |
Line 10,547: |
Line 10,522: |
| | | |
| V1c. (( v , w )). | | V1c. (( v , w )). |
| + | </pre> |
| | | |
| A rule that allows one to turn equivalent sentences into identical propositions: | | A rule that allows one to turn equivalent sentences into identical propositions: |
| | | |
− | (S <=> T) <=> ([S] = [T]) | + | : (S <=> T) <=> ([S] = [T]) |
| | | |
| Consider [ v = w ](v, w) and [ v(u) = w(u) ](u) | | Consider [ v = w ](v, w) and [ v(u) = w(u) ](u) |
| | | |
| + | <pre> |
| Value Rule 1 | | Value Rule 1 |
| | | |
Line 10,565: |
Line 10,542: |
| | | |
| V1c. (( v , w )) | | V1c. (( v , w )) |
| + | </pre> |
| | | |
| + | <pre> |
| Value Rule 1 | | Value Rule 1 |
| | | |
Line 10,579: |
Line 10,558: |
| | | |
| V1c. (( f(u) , g(u) )) | | V1c. (( f(u) , g(u) )) |
| + | </pre> |
| | | |
| + | <pre> |
| Value Rule 1 | | Value Rule 1 |
| | | |
Line 10,591: |
Line 10,572: |
| | | |
| V1c. (( f , g ))$ | | V1c. (( f , g ))$ |
| + | </pre> |
| | | |
| + | <pre> |
| Evaluation Rule 1 | | Evaluation Rule 1 |
| | | |
Line 10,615: |
Line 10,598: |
| | | |
| E1d. (( f , g ))$(u). :$1b | | E1d. (( f , g ))$(u). :$1b |
| + | </pre> |
| | | |
| + | <pre> |
| Evaluation Rule 1 | | Evaluation Rule 1 |
| | | |
Line 10,643: |
Line 10,628: |
| | | |
| E1d. (( f , g ))$(u). :$1b | | E1d. (( f , g ))$(u). :$1b |
| + | </pre> |
| | | |
− | | + | <pre> |
| Definition 2 | | Definition 2 |
| | | |
Line 10,654: |
Line 10,640: |
| | | |
| D2b. u C X <=> u C Y, for all u C U. | | D2b. u C X <=> u C Y, for all u C U. |
| + | </pre> |
| | | |
| + | <pre> |
| Definition 3 | | Definition 3 |
| | | |
Line 10,664: |
Line 10,652: |
| | | |
| D3b. f(u) = g(u), for all u C U. | | D3b. f(u) = g(u), for all u C U. |
| + | </pre> |
| | | |
| + | <pre> |
| Definition 4 | | Definition 4 |
| | | |
Line 10,674: |
Line 10,664: |
| | | |
| D4b. {< u, v> C UxB : v = [u C X]} | | D4b. {< u, v> C UxB : v = [u C X]} |
| + | </pre> |
| | | |
| + | <pre> |
| Definition 5 | | Definition 5 |
| | | |
Line 10,686: |
Line 10,678: |
| | | |
| : f(u) = [u C X], for all u C U. | | : f(u) = [u C X], for all u C U. |
| + | </pre> |
| | | |
| Given an indexed set of sentences, Sj for j C J, it is possible to consider the logical conjunction of the corresponding propositions. Various notations for this concept are be useful in various contexts, a sufficient sample of which are recorded in Definition 6. | | Given an indexed set of sentences, Sj for j C J, it is possible to consider the logical conjunction of the corresponding propositions. Various notations for this concept are be useful in various contexts, a sufficient sample of which are recorded in Definition 6. |
| | | |
| + | <pre> |
| Definition 6 | | Definition 6 |
| | | |
Line 10,708: |
Line 10,702: |
| | | |
| D6e. ConjJj Sj. | | D6e. ConjJj Sj. |
| + | </pre> |
| | | |
| + | <pre> |
| Definition 7 | | Definition 7 |
| | | |
Line 10,720: |
Line 10,716: |
| | | |
| D7b. [S] = [T]. | | D7b. [S] = [T]. |
| + | </pre> |
| | | |
| + | <pre> |
| Rule 5 | | Rule 5 |
| | | |
Line 10,754: |
Line 10,752: |
| | | |
| R5e. {X} = {Y}. :D5a | | R5e. {X} = {Y}. :D5a |
| + | </pre> |
| | | |
| + | <pre> |
| Rule 6 | | Rule 6 |
| | | |
Line 10,772: |
Line 10,772: |
| | | |
| R6c. ConjUu (f(u) = g(u)). :D6e | | R6c. ConjUu (f(u) = g(u)). :D6e |
| + | </pre> |
| | | |
| + | <pre> |
| Rule 7 | | Rule 7 |
| | | |
Line 10,804: |
Line 10,806: |
| | | |
| R7f. ConjUu (( P , Q ))$(u). :$1b | | R7f. ConjUu (( P , Q ))$(u). :$1b |
| + | </pre> |
| | | |
| + | <pre> |
| Rule 8 | | Rule 8 |
| | | |
Line 10,840: |
Line 10,844: |
| | | |
| R8g. ConjUu (( [S] , [T] ))$(u). :R7f | | R8g. ConjUu (( [S] , [T] ))$(u). :R7f |
| + | </pre> |
| | | |
| For instance, the observation that expresses the equality of sets in terms of their indicator functions can be formalized according to the pattern in Rule 9, namely, at lines (a, b, c), and these components of Rule 9 can be cited in future uses as "R9a", "R9b", "R9c", respectively. Using Rule 7, annotated as "R7", to adduce a few properties of indicator functions to the account, it is possible to extend Rule 9 by another few steps, referenced as "R9d", "R9e", "R9f", "R9g". | | For instance, the observation that expresses the equality of sets in terms of their indicator functions can be formalized according to the pattern in Rule 9, namely, at lines (a, b, c), and these components of Rule 9 can be cited in future uses as "R9a", "R9b", "R9c", respectively. Using Rule 7, annotated as "R7", to adduce a few properties of indicator functions to the account, it is possible to extend Rule 9 by another few steps, referenced as "R9d", "R9e", "R9f", "R9g". |
| | | |
| + | <pre> |
| Rule 9 | | Rule 9 |
| | | |
Line 10,876: |
Line 10,882: |
| | | |
| R9g. ConjUu (( {X} , {Y} ))$(u). :R7f | | R9g. ConjUu (( {X} , {Y} ))$(u). :R7f |
| + | </pre> |
| | | |
| + | <pre> |
| Rule 10 | | Rule 10 |
| | | |
Line 10,916: |
Line 10,924: |
| | | |
| R10h. ConjUu (( [u C X] , [u C Y] ))$(u). :R8g | | R10h. ConjUu (( [u C X] , [u C Y] ))$(u). :R8g |
| + | </pre> |
| | | |
| + | <pre> |
| Rule 11 | | Rule 11 |
| | | |
Line 10,932: |
Line 10,942: |
| | | |
| R11c. {X} c UxB | | R11c. {X} c UxB |
− |
| |
− |
| |
| | | |
| : {X} = {< u, v> C UxB : v = [S](u)}. :R | | : {X} = {< u, v> C UxB : v = [S](u)}. :R |
Line 10,940: |
Line 10,948: |
| | | |
| R11d. {X} : U -> B | | R11d. {X} : U -> B |
− |
| |
− |
| |
| | | |
| : {X}(u) = [S](u), for all u C U. :R | | : {X}(u) = [S](u), for all u C U. :R |
Line 10,948: |
Line 10,954: |
| | | |
| R11e. {X} = [S]. :R | | R11e. {X} = [S]. :R |
| + | </pre> |
| | | |
| An application of Rule 11 involves the recognition of an antecedent condition as a case under the Rule, that is, as a condition that matches one of the sentences in the Rule's chain of equivalents, and it requires the relegation of the other expressions to the production of a result. Thus, there is the choice of an initial expression that has to be checked on input for whether it fits the antecedent condition, and there is the choice of three types of output that are generated as a consequence, only one of which is generally needed at any given time. More often than not, though, a rule is applied in only a few of its possible ways. The usual antecedent and the usual consequents for Rule 11 can be distinguished in form and specialized in practice as follows: | | An application of Rule 11 involves the recognition of an antecedent condition as a case under the Rule, that is, as a condition that matches one of the sentences in the Rule's chain of equivalents, and it requires the relegation of the other expressions to the production of a result. Thus, there is the choice of an initial expression that has to be checked on input for whether it fits the antecedent condition, and there is the choice of three types of output that are generated as a consequence, only one of which is generally needed at any given time. More often than not, though, a rule is applied in only a few of its possible ways. The usual antecedent and the usual consequents for Rule 11 can be distinguished in form and specialized in practice as follows: |
Line 10,961: |
Line 10,968: |
| Applying Rule 9, Rule 8, and the Logical Rules to the special case where S <=> (X = Y), one obtains the following general fact. | | Applying Rule 9, Rule 8, and the Logical Rules to the special case where S <=> (X = Y), one obtains the following general fact. |
| | | |
| + | <pre> |
| Fact 1 | | Fact 1 |
| | | |