|
|
| (8 intermediate revisions by the same user not shown) |
| Line 6: |
Line 6: |
| | | | |
| | =====1.3.12.1. Syntactic Transformation Rules===== | | =====1.3.12.1. Syntactic Transformation Rules===== |
| − |
| |
| − | <pre>
| |
| − | Logical Translation Rule 1
| |
| − |
| |
| − | If S is a sentence
| |
| − |
| |
| − | about things in the universe U
| |
| − |
| |
| − | and P is a proposition : U -> B, such that:
| |
| − |
| |
| − | L1a. [S] = P,
| |
| − |
| |
| − | then the following equations hold:
| |
| − |
| |
| − | L1b00. [False] = () = 0 : U->B.
| |
| − |
| |
| − | L1b01. [Not S] = ([S]) = (P) : U->B.
| |
| − |
| |
| − | L1b10. [S] = [S] = P : U->B.
| |
| − |
| |
| − | L1b11. [True] = (()) = 1 : U->B.
| |
| − | </pre>
| |
| − |
| |
| − | <pre>
| |
| − | Geometric Translation Rule 1
| |
| − |
| |
| − | If X c U
| |
| − |
| |
| − | and P : U -> B, such that:
| |
| − |
| |
| − | G1a. {X} = P,
| |
| − |
| |
| − | then the following equations hold:
| |
| − |
| |
| − | G1b00. {{}} = () = 0 : U->B.
| |
| − |
| |
| − | G1b10. {~X} = ({X}) = (P) : U->B.
| |
| − |
| |
| − | G1b01. {X} = {X} = P : U->B.
| |
| − |
| |
| − | G1b11. {U} = (()) = 1 : U->B.
| |
| − | </pre>
| |
| − |
| |
| − | <pre>
| |
| − | Logical Translation Rule 2
| |
| − |
| |
| − | If S, T are sentences
| |
| − |
| |
| − | about things in the universe U
| |
| − |
| |
| − | and P, Q are propositions: U -> B, such that:
| |
| − |
| |
| − | L2a. [S] = P and [T] = Q,
| |
| − |
| |
| − | then the following equations hold:
| |
| − |
| |
| − | L2b00. [False] = () = 0 : U->B.
| |
| − |
| |
| − | L2b01. [Neither S nor T] = ([S])([T]) = (P)(Q).
| |
| − |
| |
| − | L2b02. [Not S, but T] = ([S])[T] = (P) Q.
| |
| − |
| |
| − | L2b03. [Not S] = ([S]) = (P).
| |
| − |
| |
| − | L2b04. [S and not T] = [S]([T]) = P (Q).
| |
| − |
| |
| − | L2b05. [Not T] = ([T]) = (Q).
| |
| − |
| |
| − | L2b06. [S or T, not both] = ([S], [T]) = (P, Q).
| |
| − |
| |
| − | L2b07. [Not both S and T] = ([S].[T]) = (P Q).
| |
| − |
| |
| − | L2b08. [S and T] = [S].[T] = P.Q.
| |
| − |
| |
| − | L2b09. [S <=> T] = (([S], [T])) = ((P, Q)).
| |
| − |
| |
| − | L2b10. [T] = [T] = Q.
| |
| − |
| |
| − | L2b11. [S => T] = ([S]([T])) = (P (Q)).
| |
| − |
| |
| − | L2b12. [S] = [S] = P.
| |
| − |
| |
| − | L2b13. [S <= T] = (([S]) [T]) = ((P) Q).
| |
| − |
| |
| − | L2b14. [S or T] = (([S])([T])) = ((P)(Q)).
| |
| − |
| |
| − | L2b15. [True] = (()) = 1 : U->B.
| |
| − | </pre>
| |
| − |
| |
| − | <pre>
| |
| − | Geometric Translation Rule 2
| |
| − |
| |
| − | If X, Y c U
| |
| − |
| |
| − | and P, Q U -> B, such that:
| |
| − |
| |
| − | G2a. {X} = P and {Y} = Q,
| |
| − |
| |
| − | then the following equations hold:
| |
| − |
| |
| − | G2b00. {{}} = () = 0 : U->B.
| |
| − |
| |
| − | G2b01. {~X n ~Y} = ({X})({Y}) = (P)(Q).
| |
| − |
| |
| − | G2b02. {~X n Y} = ({X}){Y} = (P) Q.
| |
| − |
| |
| − | G2b03. {~X} = ({X}) = (P).
| |
| − |
| |
| − | G2b04. {X n ~Y} = {X}({Y}) = P (Q).
| |
| − |
| |
| − | G2b05. {~Y} = ({Y}) = (Q).
| |
| − |
| |
| − | G2b06. {X + Y} = ({X}, {Y}) = (P, Q).
| |
| − |
| |
| − | G2b07. {~(X n Y)} = ({X}.{Y}) = (P Q).
| |
| − |
| |
| − | G2b08. {X n Y} = {X}.{Y} = P.Q.
| |
| − |
| |
| − | G2b09. {~(X + Y)} = (({X}, {Y})) = ((P, Q)).
| |
| − |
| |
| − | G2b10. {Y} = {Y} = Q.
| |
| − |
| |
| − | G2b11. {~(X n ~Y)} = ({X}({Y})) = (P (Q)).
| |
| − |
| |
| − | G2b12. {X} = {X} = P.
| |
| − |
| |
| − | G2b13. {~(~X n Y)} = (({X}) {Y}) = ((P) Q).
| |
| − |
| |
| − | G2b14. {X u Y} = (({X})({Y})) = ((P)(Q)).
| |
| − |
| |
| − | G2b15. {U} = (()) = 1 : U->B.
| |
| − | </pre>
| |
| | | | |
| | <pre> | | <pre> |
| Line 277: |
Line 145: |
| | </pre> | | </pre> |
| | | | |
| − | <pre>
| + | =====1.3.12.2. Derived Equivalence Relations <big>✔</big>===== |
| − | Definition 2
| |
| − | | |
| − | If X, Y c U,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | D2a. X = Y.
| |
| − | | |
| − | D2b. u C X <=> u C Y, for all u C U.
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Definition 3
| |
| − | | |
| − | If f, g : U -> V,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | D3a. f = g.
| |
| − | | |
| − | D3b. f(u) = g(u), for all u C U.
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Definition 4
| |
| − | | |
| − | If X c U,
| |
| − | | |
| − | then the following are identical subsets of UxB:
| |
| − | | |
| − | D4a. {X}
| |
| − | | |
| − | D4b. {< u, v> C UxB : v = [u C X]}
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Definition 5
| |
| − | | |
| − | If X c U,
| |
| − | | |
| − | then the following are identical propositions:
| |
| − | | |
| − | D5a. {X}.
| |
| − | | |
| − | D5b. f : U -> B
| |
| − | | |
| − | : 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.
| |
| − | | |
| − | <pre>
| |
| − | Definition 6
| |
| − | | |
| − | If Sj is a sentence
| |
| − | | |
| − | about things in the universe U,
| |
| − | | |
| − | for all j C J,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | D6a. Sj, for all j C J.
| |
| − | | |
| − | D6b. For all j C J, Sj.
| |
| − | | |
| − | D6c. Conj(j C J) Sj.
| |
| − | | |
| − | D6d. ConjJ,j Sj.
| |
| − | | |
| − | D6e. ConjJj Sj.
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Definition 7
| |
| − | | |
| − | If S, T are sentences
| |
| − | | |
| − | about things in the universe U,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | D7a. S <=> T.
| |
| − | | |
| − | D7b. [S] = [T].
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Rule 5
| |
| − | | |
| − | If X, Y c U,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | R5a. X = Y. :D2a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R5b. u C X <=> u C Y, for all u C U. :D2b
| |
| − | | |
| − | :D7a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R5c. [u C X] = [u C Y], for all u C U. :D7b
| |
| − | | |
| − | :???
| |
| − | | |
| − | ::
| |
| − | | |
| − | R5d. {< u, v> C UxB : v = [u C X]}
| |
| − | | |
| − | =
| |
| − | | |
| − | {< u, v> C UxB : v = [u C Y]}. :???
| |
| − | | |
| − | :D5b
| |
| − | | |
| − | ::
| |
| − | | |
| − | R5e. {X} = {Y}. :D5a
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Rule 6
| |
| − | | |
| − | If f, g : U -> V,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | R6a. f = g. :D3a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R6b. f(u) = g(u), for all u C U. :D3b
| |
| − | | |
| − | :D6a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R6c. ConjUu (f(u) = g(u)). :D6e
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Rule 7
| |
| − | | |
| − | If P, Q : U -> B,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | R7a. P = Q. :R6a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R7b. P(u) = Q(u), for all u C U. :R6b
| |
| − | | |
| − | ::
| |
| − | | |
| − | R7c. ConjUu (P(u) = Q(u)). :R6c
| |
| − | | |
| − | :P1a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R7d. ConjUu (P(u) <=> Q(u)). :P1b
| |
| − | | |
| − | ::
| |
| − | | |
| − | R7e. ConjUu (( P(u) , Q(u) )). :P1c
| |
| − | | |
| − | :$1a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R7f. ConjUu (( P , Q ))$(u). :$1b
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Rule 8
| |
| − | | |
| − | If S, T are sentences
| |
| − | | |
| − | about things in the universe U,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | R8a. S <=> T. :D7a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R8b. [S] = [T]. :D7b
| |
| − | | |
| − | :R7a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R8c. [S](u) = [T](u), for all u C U. :R7b
| |
| − | | |
| − | ::
| |
| − | | |
| − | R8d. ConjUu ( [S](u) = [T](u) ). :R7c
| |
| − | | |
| − | ::
| |
| − | | |
| − | R8e. ConjUu ( [S](u) <=> [T](u) ). :R7d
| |
| − | | |
| − | ::
| |
| − | | |
| − | R8f. ConjUu (( [S](u) , [T](u) )). :R7e
| |
| − | | |
| − | ::
| |
| − | | |
| − | 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".
| |
| − | | |
| − | <pre>
| |
| − | Rule 9
| |
| − | | |
| − | If X, Y c U,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | R9a. X = Y. :R5a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R9b. {X} = {Y}. :R5e
| |
| − | | |
| − | :R7a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R9c. {X}(u) = {Y}(u), for all u C U. :R7b
| |
| − | | |
| − | ::
| |
| − | | |
| − | R9d. ConjUu ( {X}(u) = {Y}(u) ). :R7c
| |
| − | | |
| − | ::
| |
| − | | |
| − | R9e. ConjUu ( {X}(u) <=> {Y}(u) ). :R7d
| |
| − | | |
| − | ::
| |
| − | | |
| − | R9f. ConjUu (( {X}(u) , {Y}(u) )). :R7e
| |
| − | | |
| − | ::
| |
| − | | |
| − | R9g. ConjUu (( {X} , {Y} ))$(u). :R7f
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Rule 10
| |
| − | | |
| − | If X, Y c U,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | R10a. X = Y. :D2a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R10b. u C X <=> u C Y, for all u C U. :D2b
| |
| − | | |
| − | :R8a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R10c. [u C X] = [u C Y]. :R8b
| |
| − | | |
| − | ::
| |
| − | | |
| − | R10d. For all u C U,
| |
| − | | |
| − | [u C X](u) = [u C Y](u). :R8c
| |
| − | | |
| − | ::
| |
| − | | |
| − | R10e. ConjUu ( [u C X](u) = [u C Y](u) ). :R8d
| |
| − | | |
| − | ::
| |
| − | | |
| − | R10f. ConjUu ( [u C X](u) <=> [u C Y](u) ). :R8e
| |
| − | | |
| − | ::
| |
| − | | |
| − | R10g. ConjUu (( [u C X](u) , [u C Y](u) )). :R8f
| |
| − | | |
| − | ::
| |
| − | | |
| − | R10h. ConjUu (( [u C X] , [u C Y] ))$(u). :R8g
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Rule 11
| |
| − | | |
| − | If X c U
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | R11a. X = {u C U : S}. :R5a
| |
| − | | |
| − | ::
| |
| − | | |
| − | R11b. {X} = { {u C U : S} }. :R5e
| |
| − | | |
| − | ::
| |
| − | | |
| − | R11c. {X} c UxB
| |
| − | | |
| − | : {X} = {< u, v> C UxB : v = [S](u)}. :R
| |
| − | | |
| − | ::
| |
| − | | |
| − | R11d. {X} : U -> B
| |
| − | | |
| − | : {X}(u) = [S](u), for all u C U. :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:
| |
| − | | |
| − | a. R11a marks the usual starting place for an application of the Rule, that is, the standard form of antecedent condition that is likely to lead to an invocation of the Rule.
| |
| − | | |
| − | b. R11b records the trivial consequence of applying the spiny braces to both sides of the initial equation.
| |
| − | | |
| − | c. R11c gives a version of the indicator function with {X} c UxB, called its "extensional form".
| |
| − | | |
| − | d. R11d gives a version of the indicator function with {X} : U->B, called its "functional form".
| |
| − | | |
| − | 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
| |
| − | | |
| − | If X,Y c U,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | F1a. S <=> X = Y. :R9a
| |
| − | | |
| − | ::
| |
| − | | |
| − | F1b. S <=> {X} = {Y}. :R9b
| |
| − | | |
| − | ::
| |
| − | | |
| − | F1c. S <=> {X}(u) = {Y}(u), for all u C U. :R9c
| |
| − | | |
| − | ::
| |
| − | | |
| − | F1d. S <=> ConjUu ( {X}(u) = {Y}(u) ). :R9d
| |
| − | | |
| − | :R8a
| |
| − | | |
| − | ::
| |
| − | | |
| − | F1e. [S] = [ ConjUu ( {X}(u) = {Y}(u) ) ]. :R8b
| |
| − | | |
| − | :???
| |
| − | | |
| − | ::
| |
| − | | |
| − | F1f. [S] = ConjUu [ {X}(u) = {Y}(u) ]. :???
| |
| − | | |
| − | ::
| |
| − | | |
| − | F1g. [S] = ConjUu (( {X}(u) , {Y}(u) )). :$1a
| |
| − | | |
| − | ::
| |
| − | | |
| − | F1h. [S] = ConjUu (( {X} , {Y} ))$(u). :$1b
| |
| − | | |
| − | ///
| |
| − | | |
| − | {u C U : (f, g)$(u)}
| |
| − | | |
| − | = {u C U : (f(u), g(u))}
| |
| − | | |
| − | = {u C
| |
| − | | |
| − | ///
| |
| − | </pre>
| |
| − | | |
| − | =====1.3.12.2. Derived Equivalence Relations===== | |
| − | | |
| − | The uses of the equal sign for denoting equations or equivalences are recalled and extended in the following ways:
| |
| − | | |
| − | 1. If E is an arbitrary equivalence relation,
| |
| − | | |
| − | then the equation "x =E y" means that <x, y> C E.
| |
| − | | |
| − | 2. If R is a sign relation such that RSI is a SER on S = I,
| |
| − | | |
| − | then the semiotic equation "x =R y" means that <x, y> C RSI.
| |
| − | | |
| − | 3. If R is a sign relation such that F is its DER on S = I,
| |
| − | | |
| − | then the denotative equation "x =R y" means that <x, y> C F,
| |
| − | | |
| − | in other words, that Den(R, x) = Den(R, y).
| |
| − | | |
| − | The uses of square brackets for denoting equivalence classes are recalled and extended in the following ways:
| |
| − | | |
| − | 1. If E is an arbitrary equivalence relation,
| |
| − | | |
| − | then "[x]E" denotes the equivalence class of x under E.
| |
| − | | |
| − | 2. If R is a sign relation such that Con(R) is a SER on S = I,
| |
| − | | |
| − | then "[x]R" denotes the SEC of x under Con(R).
| |
| − | | |
| − | 3. If R is a sign relation such that Der(R) is a DER on S = I,
| |
| − | | |
| − | then "[x]R" denotes the DEC of x under Der(R).
| |
| − | | |
| − | By applying the form of Fact 1 to the special case where X = Den(R, x) and Y = Den(R, y), one obtains the following facts.
| |
| − | | |
| − | <pre>
| |
| − | Fact 2.1
| |
| − | | |
| − | If R c OxSxI,
| |
| − | | |
| − | then the following are identical subsets of SxI:
| |
| − | | |
| − | F2.1a. DerR :D13a
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.1b. Der(R) :D13b
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.1c. {<x, y> C SxI :
| |
| − | | |
| − | Den(R, x) = Den(R, y)
| |
| − | | |
| − | } :D13c
| |
| − | | |
| − | :R9a
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.1d. {<x, y> C SxI :
| |
| − | | |
| − | {Den(R, x)} = {Den(R, y)}
| |
| − | | |
| − | } :R9b
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.1e. {<x, y> C SxI :
| |
| − | | |
| − | for all o C O
| |
| − | | |
| − | {Den(R, x)}(o) = {Den(R, y)}(o)
| |
| − | | |
| − | } :R9c
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.1f. {<x, y> C SxI :
| |
| − | | |
| − | Conj(o C O)
| |
| − | | |
| − | {Den(R, x)}(o) = {Den(R, y)}(o)
| |
| − | | |
| − | } :R9d
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.1g. {<x, y> C SxI :
| |
| − | | |
| − | Conj(o C O)
| |
| − | | |
| − | (( {Den(R, x)}(o) , {Den(R, y)}(o) ))
| |
| − | | |
| − | } :R9e
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.1h. {<x, y> C SxI :
| |
| − | | |
| − | Conj(o C O)
| |
| − | | |
| − | (( {Den(R, x)} , {Den(R, y)} ))$(o)
| |
| − | | |
| − | } :R9f
| |
| − | | |
| − | :D12e
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.1i. {<x, y> C SxI :
| |
| − | | |
| − | Conj(o C O)
| |
| − | | |
| − | (( {ROS.x} , {ROS.y} ))$(o)
| |
| − | | |
| − | } :D12a
| |
| − | </pre> | |
| − | | |
| − | <pre>
| |
| − | Fact 2.2
| |
| − | | |
| − | If R c OxSxI,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | F2.2a. DerR = {<x, y> C SxI :
| |
| − | | |
| − | Conj(o C O)
| |
| − | | |
| − | {Den(R, x)}(o) =
| |
| − | | |
| − | {Den(R, y)}(o)
| |
| − | | |
| − | } :R11a
| |
| − | ::
| |
| − | | |
| − | F2.2b. {DerR} = { {<x, y> C SxI :
| |
| − | | |
| − | Conj(o C O)
| |
| − | | |
| − | {Den(R, x)}(o) =
| |
| − | | |
| − | {Den(R, y)}(o)
| |
| − | | |
| − | }
| |
| − | | |
| − | } :R11b
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.2c. {DerR} c SxIxB
| |
| − | | |
| − | :
| |
| − | | |
| − | {DerR} = {<x, y, v> C SxIxB :
| |
| − | | |
| − | v =
| |
| − | | |
| − | [ Conj(o C O)
| |
| − | | |
| − | {Den(R, x)}(o) =
| |
| − | | |
| − | {Den(R, y)}(o)
| |
| − | | |
| − | ]
| |
| − | | |
| − | } :R11c
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.2d. {DerR} = {<x, y, v> C SxIxB :
| |
| − | | |
| − | v =
| |
| − | | |
| − | Conj(o C O)
| |
| − | | |
| − | [ {Den(R, x)}(o) =
| |
| − | | |
| − | {Den(R, y)}(o)
| |
| − | | |
| − | ]
| |
| − | | |
| − | } :Log
| |
| − | | |
| − | F2.2e. {DerR} = {<x, y, v> C SxIxB :
| |
| − | | |
| − | v =
| |
| − | | |
| − | Conj(o C O)
| |
| − | | |
| − | (( {Den(R, x)}(o),
| |
| − | | |
| − | {Den(R, y)}(o)
| |
| − | | |
| − | ))
| |
| − | | |
| − | } :Log
| |
| − | | |
| − | F2.2f. {DerR} = {<x, y, v> C SxIxB :
| |
| − | | |
| − | v =
| |
| − | | |
| − | Conj(o C O)
| |
| − | | |
| − | (( {Den(R, x)},
| |
| − | | |
| − | {Den(R, y)}
| |
| − | | |
| − | ))$(o)
| |
| − | | |
| − | } :$
| |
| − | </pre>
| |
| − | | |
| − | <pre>
| |
| − | Fact 2.3
| |
| − | | |
| − | If R c OxSxI,
| |
| − | | |
| − | then the following are equivalent:
| |
| − | | |
| − | F2.3a. DerR = {<x, y> C SxI :
| |
| − | | |
| − | Conj(o C O)
| |
| − | | |
| − | {Den(R, x)}(o) =
| |
| − | | |
| − | {Den(R, y)}(o)
| |
| − | | |
| − | } :R11a
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.3b. {DerR} : SxI -> B
| |
| − | | |
| − | :
| |
| − | | |
| − | {DerR}(x, y) = [ Conj(o C O)
| |
| − | | |
| − | {Den(R, x)}(o) =
| |
| − | | |
| − | {Den(R, y)}(o)
| |
| − | | |
| − | ] :R11d
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.3c. {DerR}(x, y) = Conj(o C O)
| |
| − | | |
| − | [ {Den(R, x)}(o) =
| |
| − | | |
| − | {Den(R, y)}(o)
| |
| − | | |
| − | ] :Log
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.3d. {DerR}(x, y) = Conj(o C O)
| |
| − | | |
| − | [ {DenR}(o, x) =
| |
| − | | |
| − | {DenR}(o, y)
| |
| − | | |
| − | ] :Def
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.3e. {DerR}(x, y) = Conj(o C O)
| |
| − | | |
| − | (( {DenR}(o, x),
| |
| − | | |
| − | {DenR}(o, y)
| |
| − | | |
| − | )) :Log
| |
| − | | |
| − | :D10b
| |
| − | | |
| − | ::
| |
| − | | |
| − | F2.3f. {DerR}(x, y) = Conj(o C O)
| |
| − | | |
| − | (( {ROS}(o, x),
| |
| − | | |
| − | {ROS}(o, y)
| |
| − | | |
| − | )) :D10a
| |
| − | </pre>
| |
| | | | |
| | =====1.3.12.3. Digression on Derived Relations <big>✔</big>===== | | =====1.3.12.3. Digression on Derived Relations <big>✔</big>===== |
Alternate Version : Needs To Be Reconciled
1.3.12. Syntactic Transformations ✔
1.3.12.1. Syntactic Transformation Rules
Value Rule 1
If v, w C B
then "v = w" is a sentence about <v, w> C B2,
[v = w] is a proposition : B2 -> B,
and the following are identical values in B:
V1a. [ v = w ](v, w)
V1b. [ v <=> w ](v, w)
V1c. ((v , w))
Value Rule 1
If v, w C B,
then the following are equivalent:
V1a. v = w.
V1b. v <=> w.
V1c. (( v , w )).
A rule that allows one to turn equivalent sentences into identical propositions:
- (S <=> T) <=> ([S] = [T])
Consider [ v = w ](v, w) and [ v(u) = w(u) ](u)
Value Rule 1
If v, w C B,
then the following are identical values in B:
V1a. [ v = w ]
V1b. [ v <=> w ]
V1c. (( v , w ))
Value Rule 1
If f, g : U -> B,
and u C U
then the following are identical values in B:
V1a. [ f(u) = g(u) ]
V1b. [ f(u) <=> g(u) ]
V1c. (( f(u) , g(u) ))
Value Rule 1
If f, g : U -> B,
then the following are identical propositions on U:
V1a. [ f = g ]
V1b. [ f <=> g ]
V1c. (( f , g ))$
Evaluation Rule 1
If f, g : U -> B
and u C U,
then the following are equivalent:
E1a. f(u) = g(u). :V1a
::
E1b. f(u) <=> g(u). :V1b
::
E1c. (( f(u) , g(u) )). :V1c
:$1a
::
E1d. (( f , g ))$(u). :$1b
Evaluation Rule 1
If S, T are sentences
about things in the universe U,
f, g are propositions: U -> B,
and u C U,
then the following are equivalent:
E1a. f(u) = g(u). :V1a
::
E1b. f(u) <=> g(u). :V1b
::
E1c. (( f(u) , g(u) )). :V1c
:$1a
::
E1d. (( f , g ))$(u). :$1b
1.3.12.2. Derived Equivalence Relations ✔
1.3.12.3. Digression on Derived Relations ✔
