Changes

'''Author: Jon Awbrey'''
Line 1: Line 1:  
{{DISPLAYTITLE:Syntactic Transformations}}
 
{{DISPLAYTITLE:Syntactic Transformations}}
 +
'''Author: [[User:Jon Awbrey|Jon Awbrey]]'''
    
<div class="nonumtoc">__TOC__</div>
 
<div class="nonumtoc">__TOC__</div>
   −
==Syntactic Transformations==
+
====1.3.12.  Syntactic Transformations====
   −
To discuss the import of the above definitions in greater depth, it serves to establish a number of logical relations and set-theoretic identities that can be found to hold among this array of conceptions and constructions.  Facilitating this task requires in turn a number of auxiliary concepts and notations.
+
We have been examining several distinct but closely related notions of ''indication''.  To discuss the import of these ideas in greater depth, it serves to establish a number of logical relations and set-theoretic identities that can be found to hold among their roughly parallel arrays of conceptions and constructions.  Facilitating this task requires in turn a number of auxiliary concepts and notations. The notions of indication in question are expressed in a variety of different notations, enumerated as follows:
   −
The diverse notions of ''indication'' under discussion are expressed in a variety of different notations, in particular, the logical language of sentences, the functional language of propositions, and the geometric language of sets.  Thus, one way to explain the relationships that exist among these concepts is to describe the ''translations'' that they induce among the allied families of notation.
+
# The functional language of propositions
 +
# The logical language of sentences
 +
# The geometric language of sets
   −
===Syntactic Transformation Rules===
+
Thus, one way to explain the relationships that hold among these concepts is to describe the ''translations'' that are induced among their allied families of notation.
 +
 
 +
=====1.3.12.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.  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:
Line 432: Line 437:  
'''Editing Note.'''  Need a transition here.  Give a brief description of the Tables of Translation Rules that have now been moved to the Appendices, and then move on to the rest of the Definitions and Proof Schemata.
 
'''Editing Note.'''  Need a transition here.  Give a brief description of the Tables of Translation Rules that have now been moved to the Appendices, and then move on to the rest of the Definitions and Proof Schemata.
   −
<br>
+
A rule that allows one to turn equivalent sentences into identical propositions:
   −
<pre>
+
{| align="center" cellpadding="8" width="90%"
Value Rule 1
+
| <math>(S \Leftrightarrow T) \quad \Leftrightarrow \quad (\downharpoonleft S \downharpoonright = \downharpoonleft T \downharpoonright)</math>
 +
|}
   −
If v, w C B
+
Compare:
   −
then "v = w" is a sentence about <v, w> C B2,
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\downharpoonleft v = w \downharpoonright (v, w)</math>
 +
|-
 +
| <math>\downharpoonleft v(u) = w(u) \downharpoonright (u)</math>
 +
|}
   −
[v = w] is a proposition : B2 -> B,
+
'''Editing Note.'''  The last draft I can find has 5 variants for the next box, "Value&nbsp;Rule&nbsp;1", and I can't tell right off which I meant to use.  Until I can get back to this, here's a link to the collection of variants:
   −
and the following are identical values in B:
+
* [http://mywikibiz.com/User:Jon_Awbrey/SCRATCHPAD#Value_Rule_1 Value Rule 1]  
 
  −
V1a. [ v = w ](v, w)
  −
 
  −
V1b. [ v <=> w ](v, w)
  −
 
  −
V1c. ((v , w))
  −
</pre>
      
<br>
 
<br>
   −
<pre>
+
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
Value Rule 1
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
If v, w C B,
+
|- style="height:50px; text-align:right"
 
+
| width="98%" | <math>\operatorname{Evaluation~Rule~1}</math>
then the following are equivalent:
+
| width="2%"  | &nbsp;
 
+
|}
V1a. v = w.
+
|-
 
+
|
V1b. v <=> w.
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:50px"
V1c. (( v , w )).
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
</pre>
+
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
+
| width="84%" style="border-top:1px solid black" | <math>f, g ~:~ X \to \underline\mathbb{B}</math>
<br>
+
|- style="height:50px"
 
+
| &nbsp;
<pre>
+
| <math>\text{and}\!</math>
A rule that allows one to turn equivalent sentences into identical propositions:
+
| <math>x ~\in~ X</math>
 
+
|- style="height:50px"
(S <=> T) <=> ([S] = [T])
+
| &nbsp;
 
+
| <math>\text{then}\!</math>
Consider [ v = w ](v, w) and [ v(u) = w(u) ](u)
+
| <math>\text{the following are equivalent:}\!</math>
 
+
|}
Value Rule 1
+
|-
 
+
|
If v, w C B,
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:10px"
then the following are identical values in B:
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
+
| width="14%" style="border-top:1px solid black" | &nbsp;
V1a. [ v = w ]
+
| width="64%" style="border-top:1px solid black" | &nbsp;
 
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
V1b. [ v <=> w ]
+
|- style="height:40px"
 
+
| &nbsp;
V1c. (( v , w ))
+
| <math>\operatorname{E1a.}</math>
</pre>
+
| <math>f(x) ~=~ g(x)</math>
 
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{E1a~:~V1a}</math>
<br>
+
|- style="height:20px"
 
+
| colspan="3" | &nbsp;
<pre>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
Value Rule 1
+
|- style="height:40px"
 
+
| &nbsp;
If f, g : U -> B,
+
| <math>\operatorname{E1b.}</math>
 
+
| <math>f(x) ~\Leftrightarrow~ g(x)</math>
and u C U
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{E1b~:~V1b}</math>
 
+
|- style="height:20px"
then the following are identical values in B:
+
| colspan="3" | &nbsp;
 
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
V1a. [ f(u) = g(u) ]
+
|- style="height:60px"
 
+
| &nbsp;
V1b. [ f(u) <=> g(u) ]
+
| <math>\operatorname{E1c.}</math>
 
+
| <math>\underline{((}~ f(x) ~,~ g(x) ~\underline{))}</math>
V1c. (( f(u) , g(u) ))
+
| style="border-left:1px solid black; text-align:center" |
</pre>
+
<p><math>\operatorname{E1c~:~V1c}</math></p>
 +
<p><math>\operatorname{E1c~:~$1a}</math></p>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{E1d.}</math>
 +
| <math>\underline{((}~ f ~,~ g ~\underline{))}^\$ (x)</math>
 +
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{E1d~:~$1b}</math>
 +
|- style="height:10px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black" | &nbsp;
 +
|}
 +
|}
    
<br>
 
<br>
   −
<pre>
+
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
Value Rule 1
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
If f, g : U -> B,
+
|- style="height:40px; text-align:center"
 
+
| width="80%" | &nbsp;
then the following are identical propositions on U:
+
| width="20%" | <math>\operatorname{Definition~2}</math>
 
  −
V1a. [ f = g ]
  −
 
  −
V1b. [ f <=> g ]
  −
 
  −
V1c. (( f , g ))$
  −
</pre>
  −
 
  −
<br>
  −
 
  −
<pre>
  −
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
  −
</pre>
  −
 
  −
<br>
  −
 
  −
<pre>
  −
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
  −
</pre>
  −
 
  −
<br>
  −
 
  −
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:40px; text-align:center"
  −
| width="80%" | &nbsp;
  −
| width="20%" | <math>\operatorname{Definition~2}</math>
   
|}
 
|}
 
|-
 
|-
Line 1,563: Line 1,519:  
<br>
 
<br>
   −
===Derived Equivalence Relations===
+
=====1.3.12.2.  Derived Equivalence Relations=====
    
One seeks a method of general application for approaching the individual sign relation, a way to select an aspect of its form, to analyze it with regard to its intrinsic structure, and to classify it in comparison with other sign relations.  With respect to a particular sign relation, one approach that presents itself is to examine the relation between signs and interpretants that is given directly by its connotative component and to compare it with the various forms of derived, indirect, mediate, or peripheral relationships that can be found to exist among signs and interpretants by way of secondary considerations or subsequent studies.  Of especial interest are the relationships among signs and interpretants that can be obtained by working through the collections of objects that they commonly or severally denote.
 
One seeks a method of general application for approaching the individual sign relation, a way to select an aspect of its form, to analyze it with regard to its intrinsic structure, and to classify it in comparison with other sign relations.  With respect to a particular sign relation, one approach that presents itself is to examine the relation between signs and interpretants that is given directly by its connotative component and to compare it with the various forms of derived, indirect, mediate, or peripheral relationships that can be found to exist among signs and interpretants by way of secondary considerations or subsequent studies.  Of especial interest are the relationships among signs and interpretants that can be obtained by working through the collections of objects that they commonly or severally denote.
Line 1,599: Line 1,555:  
<br>
 
<br>
   −
<pre>
+
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
Definition 8
+
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:40px; text-align:center"
 +
| width="80%" | &nbsp;
 +
| width="20%" | <math>\operatorname{Definition~8}</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:40px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 +
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\text{then}\!</math>
 +
| <math>\text{the following are identical subsets of}~ S \times I \, :</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:40px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D8a.}</math>
 +
| width="80%" style="border-top:1px solid black" | <math>L_{SI}\!</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D8b.}</math>
 +
| <math>\operatorname{Con}^L</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D8c.}</math>
 +
| <math>\operatorname{Con}(L)</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D8d.}</math>
 +
| <math>\operatorname{proj}_{SI}(L)</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D8e.}</math>
 +
| <math>\{ (s, i) \in S \times I ~:~ (o, s, i) \in L ~\operatorname{for~some}~ o \in O \}</math>
 +
|}
 +
|}
   −
If R c OxSxI,
+
<br>
   −
then the following are identical subsets of SxI:
+
'''Editing Note.'''  Need a discussion of converse relations here.  Perhaps it would work to introduce the operators that Peirce used for the converse of a dyadic relative <math>\ell,</math> namely, <math>K\ell ~=~ k\!\cdot\!\ell ~=~ \breve\ell.</math>
   −
D8a. RSI
+
The dyadic relation <math>L_{IS}\!</math> that is the converse of the connotative relation <math>L_{SI}\!</math> can be defined directly in the following fashion:
   −
D8b. ConR
+
{| align="center" cellpadding="8" width="90%"
 
  −
D8c. Con(R)
  −
 
  −
D8d. PrSI(R)
  −
 
  −
D8e. {<s, i> C SxI : <o, s, i> C R for some o C O}
  −
</pre>
  −
 
  −
<br>
  −
 
  −
'''Editing Note.'''  Need a discussion of converse relations here.  Perhaps it would work to introduce the operators that Peirce used for the converse of a dyadic relative <math>\ell,</math> namely, <math>K\ell ~=~ k\!\cdot\!\ell ~=~ \breve\ell.</math>
  −
 
  −
The dyadic relation <math>L_{IS}\!</math> that is the converse of the connotative relation <math>L_{SI}\!</math> can be defined directly in the following fashion:
  −
 
  −
{| align="center" cellpadding="8" width="90%"
   
| <math>\overset{\smile}{\operatorname{Con}(L)} ~=~ L_{IS} ~=~ \{ (i, s) \in I \times S ~:~ (o, s, i) \in L ~\text{for some}~ o \in O \}.</math>
 
| <math>\overset{\smile}{\operatorname{Con}(L)} ~=~ L_{IS} ~=~ \{ (i, s) \in I \times S ~:~ (o, s, i) \in L ~\text{for some}~ o \in O \}.</math>
 
|}
 
|}
Line 1,631: Line 1,614:  
<br>
 
<br>
   −
<pre>
+
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
Definition 9
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
If R c OxSxI,
+
|- style="height:40px; text-align:center"
 
+
| width="80%" | &nbsp;
then the following are identical subsets of IxS:
+
| width="20%" | <math>\operatorname{Definition~9}</math>
 
+
|}
D9a. RIS
+
|-
 
+
|
D9b. RSI^
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:40px"
D9c. ConR^
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
+
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
D9d. Con(R)^
+
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
+
|- style="height:40px"
D9e. PrIS(R)
+
| &nbsp;
 
+
| <math>\text{then}\!</math>
D9f. Conv(Con(R))
+
| <math>\text{the following are identical subsets of}~ I \times S \, :</math>
 
+
|}
D9g. {<i, s> C IxS : <o, s, i> C R for some o C O}
+
|-
</pre>
+
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:50px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D9a.}</math>
 +
| width="80%" style="border-top:1px solid black" | <math>L_{IS}\!</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D9b.}</math>
 +
| <math>\overset{\smile}{L_{SI}}</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D9c.}</math>
 +
| <math>\overset{\smile}{\operatorname{Con}^L}</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D9d.}</math>
 +
| <math>\overset{\smile}{\operatorname{Con}(L)}</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D9e.}</math>
 +
| <math>\operatorname{proj}_{IS}(L)</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D9f.}</math>
 +
| <math>\operatorname{Conv}(\operatorname{Con}(L))</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D9g.}</math>
 +
| <math>\{ (i, s) \in I \times S ~:~ (o, s, i) \in L ~\operatorname{for~some}~ o \in O \}</math>
 +
|}
 +
|}
    
<br>
 
<br>
Line 1,665: Line 1,679:  
<br>
 
<br>
   −
<pre>
+
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
Definition 10
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
If R c OxSxI,
+
|- style="height:40px; text-align:center"
 
+
| width="80%" | &nbsp;
then the following are identical subsets of OxS:
+
| width="20%" | <math>\operatorname{Definition~10}</math>
 
+
|}
D10a. ROS
+
|-
 
+
|
D10b. DenR
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:40px"
D10c. Den(R)
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
+
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
D10d. PrOS(R)
+
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
+
|- style="height:40px"
D10e. {<o, s> C OxS : <o, s, i> C R for some i C I}
+
| &nbsp;
</pre>
+
| <math>\text{then}\!</math>
 +
| <math>\text{the following are identical subsets of}~ O \times S \, :</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:40px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D10a.}</math>
 +
| width="80%" style="border-top:1px solid black" | <math>L_{OS}\!</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D10b.}</math>
 +
| <math>\operatorname{Den}^L</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D10c.}</math>
 +
| <math>\operatorname{Den}(L)</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D10d.}</math>
 +
| <math>\operatorname{proj}_{OS}(L)</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D10e.}</math>
 +
| <math>\{ (o, s) \in O \times S ~:~ (o, s, i) \in L ~\operatorname{for~some}~ i \in I \}</math>
 +
|}
 +
|}
    
<br>
 
<br>
Line 1,691: Line 1,732:  
|}
 
|}
   −
A few of the many different expressions for this concept are recorded in Definition 11.
+
A few of the many different expressions for this concept are recorded in Definition&nbsp;11.
    
<br>
 
<br>
   −
<pre>
+
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
Definition 11
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
If R c OxSxI,
+
|- style="height:40px; text-align:center"
 
+
| width="80%" | &nbsp;
then the following are identical subsets of SxO:
+
| width="20%" | <math>\operatorname{Definition~11}</math>
 
+
|}
D11a. RSO
+
|-
 
+
|
D11b. ROS^
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:40px"
D11c. DenR^
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
+
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
D11d. Den(R)^
+
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
+
|- style="height:40px"
D11e. PrSO(R)
+
| &nbsp;
 
+
| <math>\text{then}\!</math>
D11f. Conv(Den(R))
+
| <math>\text{the following are identical subsets of}~ S \times O \, :</math>
 
+
|}
D11g. {<s, o> C SxO : <o, s, i> C R for some i C I}
+
|-
</pre>
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
<br>
+
|- style="height:50px"
 
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
The ''denotation of <math>x\!</math> in <math>L,\!</math>'' written <math>\operatorname{Den}(L, x),</math> is defined as follows:
+
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D11a.}</math>
 
+
| width="80%" style="border-top:1px solid black" | <math>L_{SO}\!</math>
{| align="center" cellpadding="8" width="90%"
+
|- style="height:50px"
| <math>\operatorname{Den}(L, x) ~=~ \{ o \in O ~:~ (o, x) \in \operatorname{Den}(L) \}.</math>
+
| &nbsp;
 +
| <math>\operatorname{D11b.}</math>
 +
| <math>\overset{\smile}{L_{OS}}</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D11c.}</math>
 +
| <math>\overset{\smile}{\operatorname{Den}^L}</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D11d.}</math>
 +
| <math>\overset{\smile}{\operatorname{Den}(L)}</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D11e.}</math>
 +
| <math>\operatorname{proj}_{SO}(L)</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D11f.}</math>
 +
| <math>\operatorname{Conv}(\operatorname{Den}(L))</math>
 +
|- style="height:50px"
 +
| &nbsp;
 +
| <math>\operatorname{D11g.}</math>
 +
| <math>\{ (s, o) \in S \times O ~:~ (o, s, i) \in L ~\operatorname{for~some}~ i \in I \}</math>
 
|}
 
|}
  −
In other words:
  −
  −
{| align="center" cellpadding="8" width="90%"
  −
| <math>\operatorname{Den}(L, x) ~=~ \{ o \in O ~:~ (o, x, i) \in L ~\text{for some}~ i \in I \}.</math>
   
|}
 
|}
  −
Equivalent expressions for this concept are recorded in Definition&nbsp;12.
      
<br>
 
<br>
   −
<pre>
+
The ''denotation of <math>x\!</math> in <math>L,\!</math>'' written <math>\operatorname{Den}(L, x),</math> is defined as follows:
Definition 12
     −
If R c OxSxI,
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\operatorname{Den}(L, x) ~=~ \{ o \in O ~:~ (o, x) \in \operatorname{Den}(L) \}.</math>
 +
|}
   −
and x C S,
+
In other words:
   −
then the following are identical subsets of O:
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\operatorname{Den}(L, x) ~=~ \{ o \in O ~:~ (o, x, i) \in L ~\text{for some}~ i \in I \}.</math>
 +
|}
   −
D12a. ROS.x
+
Equivalent expressions for this concept are recorded in Definition&nbsp;12.
 
  −
D12b. DenR.x
  −
 
  −
D12c. DenR|x
  −
 
  −
D12d. DenR(, x)
  −
 
  −
D12e. Den(R, x)
  −
 
  −
D12f. Den(R).x
  −
 
  −
D12g. {o C O : <o, x> C Den(R)}
  −
 
  −
D12h. {o C O : <o, x, i> C R for some i C I}
  −
</pre>
      
<br>
 
<br>
   −
Signs are ''equiferent'' if they refer to all and only the same objects, that is, if they have exactly the same denotations.  In other language for the same relation, signs are said to be ''denotatively equivalent'' or ''referentially equivalent'', but it is probably best to check whether the extension of this concept over the syntactic domain is really a genuine equivalence relation before jumping to the conclusions that are implied by these latter terms.
+
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
 
+
|
<pre>
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
To define the "equiference" of signs in terms of their denotations, one says that "x is equiferent to y under R", and writes "x =R y", to mean that Den(R, x) = Den(R, y).  Taken in extension, this notion of a relation between signs induces an "equiference relation" on the syntactic domain.
+
|- style="height:40px; text-align:center"
 
+
| width="80%" | &nbsp;
For each sign relation R, this yields a binary relation Der(R) c SxI that is defined as follows:
+
| width="20%" | <math>\operatorname{Definition~12}</math>
 
+
|}
Der(R)  =  DerR  =  {<x, y> C SxI : Den(R, x) = Den(R, y)}.
+
|-
 
+
|
These definitions and notations are recorded in the following display.
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:40px"
Definition 13
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
+
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
If R c OxSxI,
+
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 
+
|- style="height:40px"
then the following are identical subsets of SxI:
+
| &nbsp;
 
+
| <math>\text{and}\!</math>
D13a. DerR
+
| <math>x ~\in~ S</math>
 
+
|- style="height:40px"
D13b. Der(R)
+
| &nbsp;
 +
| <math>\text{then}\!</math>
 +
| <math>\text{the following are identical subsets of}~ O \, :</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:40px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D12a.}</math>
 +
| width="80%" style="border-top:1px solid black" | <math>L_{OS} \cdot x</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D12b.}</math>
 +
| <math>\operatorname{Den}^L \cdot x</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D12c.}</math>
 +
| <math>\operatorname{Den}^L |_x</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D12d.}</math>
 +
| <math>\operatorname{Den}^L (-, x)</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D12e.}</math>
 +
| <math>\operatorname{Den}(L, x)</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D12f.}</math>
 +
| <math>\operatorname{Den}(L) \cdot x</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D12g.}</math>
 +
| <math>\{ o \in O ~:~ (o, x) \in \operatorname{Den}(L) \}</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D12h.}</math>
 +
| <math>\{ o \in O ~:~ (o, x, i) \in L ~\operatorname{for~some}~ i \in I \}</math>
 +
|}
 +
|}
   −
D13c. {<x,y> C SxI : DenR|x = DenR|y}
+
<br>
   −
D13d. {<x,y> C SxI : Den(R, x) = Den(R, y)}
+
Signs are ''equiferent'' if they refer to all and only the same objects, that is, if they have exactly the same denotations. In other language for the same relation, signs are said to be ''denotatively equivalent'' or ''referentially equivalent'', but it is probably best to check whether the extension of this concept over the syntactic domain is really a genuine equivalence relation before jumping to the conclusions that are implied by these latter terms.
   −
The relation Der(R) is defined and the notation "x =R y" is meaningful in every situation where Den(-,-) makes sense, but it remains to check whether this relation enjoys the properties of an equivalence relation.
+
To define the ''equiference'' of signs in terms of their denotations, one says that ''<math>x\!</math> is equiferent to <math>y\!</math> under <math>L,\!</math>'' and writes <math>x ~\overset{L}{=}~ y,\!</math> to mean that <math>\operatorname{Den}(L, x) = \operatorname{Den}(L, y).</math>  Taken in extension, this notion of a relation between signs induces an ''equiference relation'' on the syntactic domain.
   −
1. Reflexive property.  Is it true that  x =R x  for every x C S = I?  By definition, x =R x if and only if Den(R, x) = Den(R, x).  Thus, the reflexive property holds in any setting where the denotations Den(R, x) are defined for all signs x in the syntactic domain of R.
+
For each sign relation <math>L,\!</math> this yields a binary relation <math>\operatorname{Der}(L) \subseteq S \times I</math> that is defined as follows:
   −
2. Symmetric property.  Does  x =R y  => y =R x  for all x, y C S?  In effect, does Den(R, x) = Den(R, y) imply Den(R, y) = Den(R, x) for all signs x and y in the syntactic domain S?  Yes, so long as the sets Den(R, x) and Den(R, y) are well�defined, a fact which is already being assumed.
+
{| align="center" cellpadding="8" width="90%"
 +
| <math>\operatorname{Der}(L) ~=~ Der^L ~=~ \{ (x, y) \in S \times I ~:~ \operatorname{Den}(L, x) = \operatorname{Den}(L, y) \}.</math>
 +
|}
   −
3. Transitive property.  Does  x =R y  &  y =R z  =>  x =R z  for all x, y, z C S?  To belabor the point, does Den(R, x) = Den(R, y) and Den(R, y) = Den(R, z) imply Den(R, x) = Den(R, z) for all x, y, z in S?  Yes, again, under the stated conditions.
+
These definitions and notations are recorded in the following display.
   −
It should be clear at this point that any question about the equiference of signs reduces to a question about the equality of sets, specifically, the sets that are indexed by these signs.  As a result, so long as these sets are well�defined, the issue of whether equiference relations induce equivalence relations on their syntactic domains is almost as trivial as it initially appears.
+
<br>
   −
Taken in its set�theoretic extension, a relation of equiference induces a "denotative equivalence relation" (DER) on its syntactic domain S = I. This leads to the formation of "denotative equivalence classes" (DEC's), "denotative partitions" (DEP's), and "denotative equations" (DEQ's) on the syntactic domain.  But what does it mean for signs to be equiferent?
+
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:40px; text-align:center"
 +
| width="80%" | &nbsp;
 +
| width="20%" | <math>\operatorname{Definition~13}</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:40px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 +
| width="80%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\text{then}\!</math>
 +
| <math>\text{the following are identical subsets of}~ S \times I \, :</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:40px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D13a.}</math>
 +
| width="80%" style="border-top:1px solid black" | <math>\operatorname{Der}^L</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D13b.}</math>
 +
| <math>\operatorname{Der}(L)</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D13c.}</math>
 +
| <math>\{ (x, y) \in S \times I ~:~ \operatorname{Den}^L|_x = \operatorname{Den}^L|_y \}</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{D13d.}</math>
 +
| <math>\{ (x, y) \in S \times I ~:~ \operatorname{Den}(L, x) = \operatorname{Den}(L, y) \}</math>
 +
|}
 +
|}
   −
Notice that this is not the same thing as being "semiotically equivalent", in the sense of belonging to a single "semiotic equivalence class" (SEC), falling into the same part of a "semiotic partition" (SEP), or having a "semiotic equation" (SEQ) between them.  It is only when very felicitous conditions obtain, establishing a concord between the denotative and the connotative components of a sign relation, that these two ideas coalesce.
+
<br>
   −
In general, there is no necessity that the equiference of signs, that is, their denotational equivalence or their referential equivalence, induces the same equivalence relation on the syntactic domain as that defined by their semiotic equivalence, even though this state of accord seems like an especially desirable situation.  This makes it necessary to find a distinctive nomenclature for these structures, for which I adopt the term "denotative equivalence relations" (DER's).  In their train they bring the allied structures of "denotative equivalence classes" (DEC's) and "denotative partitions" (DEP's), while the corresponding statements of "denotative equations" (DEQ's) are expressible in the form "x =R y".
+
The relation <math>\operatorname{Der}(L)</math> is defined and the notation <math>x ~\overset{L}{=}~ y</math> is meaningful in every situation where the corresponding denotation operator <math>\operatorname{Den}(-,-)</math> makes sense, but it remains to check whether this relation enjoys the properties of an equivalence relation.
   −
The uses of the equal sign for denoting equations or equivalences are recalled and extended in the following ways:
+
<ol style="list-style-type:decimal">
   −
1. If E is an arbitrary equivalence relation,
+
<li>
then the equation "x =E y" means that <x, y> C E.
+
<p>'''Reflexive property.'''</p>
   −
2. If R is a sign relation such that RSI is a SER on S = I,
+
<p>Is it true that <math>x ~\overset{L}{=}~ x</math> for every <math>x \in S = I</math>?</p>
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,
+
<p> By definition, <math>x ~\overset{L}{=}~ x</math> if and only if <math>\operatorname{Den}(L, x) = \operatorname{Den}(L, x).</math></p>
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:
+
<p>Thus, the reflexive property holds in any setting where the denotations <math>\operatorname{Den}(L, x)</math> are defined for all signs <math>x\!</math> in the syntactic domain of <math>R.\!</math></p></li>
   −
1. If E is an arbitrary equivalence relation,
+
<li>
then "[x]E" denotes the equivalence class of x under E.
+
<p>'''Symmetric property.'''</p>
   −
2. If R is a sign relation such that Con(R) is a SER on S = I,
+
<p>Does <math>x ~\overset{L}{=}~ y</math> imply <math>y ~\overset{L}{=}~ x</math> for all <math>x, y \in S</math>?</p>
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,
+
<p>In effect, does <math>\operatorname{Den}(L, x) = \operatorname{Den}(L, y)</math> imply <math>\operatorname{Den}(L, y) = \operatorname{Den}(L, x)</math> for all signs <math>x\!</math> and <math>y\!</math> in the syntactic domain <math>S\!</math>?</p>
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.
+
<p>Yes, so long as the sets <math>\operatorname{Den}(L, x)</math> and <math>\operatorname{Den}(L, y)</math> are well-defined, a fact which is already being assumed.</p></li>
   −
Fact 2.1
+
<li>
 +
<p>'''Transitive property.'''</p>
   −
If R c OxSxI,
+
<p>Does <math>x ~\overset{L}{=}~ y</math> and <math>y ~\overset{L}{=}~ z</math> imply <math>x ~\overset{L}{=}~ z</math> for all <math>x, y, z \in S</math>?</p>
   −
then the following are identical subsets of SxI:
+
<p>To belabor the point, does <math>\operatorname{Den}(L, x) = \operatorname{Den}(L, y)</math> and <math>\operatorname{Den}(L, y) = \operatorname{Den}(L, z)</math> imply <math>\operatorname{Den}(L, x) = \operatorname{Den}(L, z)</math> for all <math>x, y, z \in S</math>?</p>
   −
F2.1a. DerR :D13a
+
<p>Yes, once again, under the stated conditions.</p></li>
::
  −
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
      +
</ol>
   −
Fact 2.2
+
It should be clear at this point that any question about the equiference of signs reduces to a question about the equality of sets, specifically, the sets that are indexed by these signs.  As a result, so long as these sets are well-defined, the issue of whether equiference relations induce equivalence relations on their syntactic domains is almost as trivial as it initially appears.
   −
If R c OxSxI,
+
Taken in its set-theoretic extension, a relation of equiference induces a ''denotative equivalence relation'' (DER) on its syntactic domain <math>S = I.\!</math>  This leads to the formation of ''denotative equivalence classes'' (DECs), ''denotative partitions'' (DEPs), and ''denotative equations'' (DEQs) on the syntactic domain.  But what does it mean for signs to be equiferent?
   −
then the following are equivalent:
+
Notice that this is not the same thing as being ''semiotically equivalent'', in the sense of belonging to a single ''semiotic equivalence class'' (SEC), falling into the same part of a ''semiotic partition'' (SEP), or having a ''semiotic equation'' (SEQ) between them.  It is only when very felicitous conditions obtain, establishing a concord between the denotative and the connotative components of a sign relation, that these two ideas coalesce.
   −
F2.2a. DerR = {<x, y> C SxI :
+
In general, there is no necessity that the equiference of signs, that is, their denotational equivalence or their referential equivalence, induces the same equivalence relation on the syntactic domain as that defined by their semiotic equivalence, even though this state of accord seems like an especially desirable situation. This makes it necessary to find a distinctive nomenclature for these structures, for which I adopt the term ''denotative equivalence relations'' (DERs).  In their train they bring the allied structures of ''denotative equivalence classes'' (DECs) and ''denotative partitions'' (DEPs), while the corresponding statements of ''denotative equations'' (DEQs) are expressible in the form <math>x ~\overset{L}{=}~ y.</math>
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 :
+
The uses of the equal sign for denoting equations or equivalences are recalled and extended in the following ways:
v =
  −
Conj(o C O)
  −
(( {Den(R, x)}(o),
  −
{Den(R, y)}(o)
  −
))
  −
} :Log
     −
F2.2f. {DerR} = {<x, y, v> C SxIxB :
+
# If <math>E\!</math> is an arbitrary equivalence relation, then the equation <math>x =_E y\!</math> means that <math>(x, y) \in E.</math>
v =
+
# If <math>L\!</math> is a sign relation such that <math>L_{SI}\!</math> is a SER on <math>S = I,\!</math> then the semiotic equation <math>x =_L y\!</math> means that <math>(x, y) \in L_{SI}.</math>
Conj(o C O)
+
# If <math>L\!</math> is a sign relation such that <math>F\!</math> is its DER on <math>S = I,\!</math> then the denotative equation <math>x ~\overset{L}{=}~ y</math> means that <math>(x, y) \in F,</math> in other words, that <math>\operatorname{Den}(L, x) = \operatorname{Den}(L, y).</math>
(( {Den(R, x)},
  −
{Den(R, y)}
  −
))$(o)
  −
} :$
      +
The use of square brackets for denoting equivalence classes is recalled and extended in the following ways:
   −
Fact 2.3
+
# If <math>E\!</math> is an arbitrary equivalence relation, then <math>[x]_E\!</math> is the equivalence class of <math>x\!</math> under <math>E.\!</math>
 +
# If <math>L\!</math> is a sign relation such that <math>\operatorname{Con}(L)</math> is a SER on <math>S = I,\!</math> then <math>[x]_L\!</math> is the SEC of <math>x\!</math> under <math>\operatorname{Con}(L).</math>
 +
# If <math>L\!</math> is a sign relation such that <math>\operatorname{Der}(L)</math> is a DER on <math>S = I,\!</math> then <math>[x]^L\!</math> is the DEC of <math>x\!</math> under <math>\operatorname{Der}(L).</math>
   −
If R c OxSxI,
+
By applying the form of Fact&nbsp;1 to the special case where <math>X = \operatorname{Den}(L, x)</math> and <math>Y = \operatorname{Den}(L, y),</math> one obtains the following facts.
 
  −
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>
  −
 
  −
===Digression on Derived Relations===
  −
 
  −
<pre>
  −
A better understanding of derived equivalence relations (DER's) can be achieved by placing their constructions within a more general context, and thus comparing the associated type of derivation operation, namely, the one that takes a triadic relation R into a dyadic relation Der(R), with other types of operations on triadic relations.  The proper setting would permit a comparative study of all their constructions from a basic set of projections and a full array of compositions on dyadic relations.
  −
 
  −
To that end, let the derivation Der(R) be expressed in the following way:
  −
 
  −
{DerR}(x, y)  =  Conj(o C O) (( {RSO}(x, o) , {ROS}(o, y) )).
  −
 
  −
From this abstract a form of composition, temporarily notated as "P#Q", where P c XxM and Q c MxY are otherwise arbitrary dyadic relations, and where P#Q c XxY is defined as follows:
  −
 
  −
{P#Q}(x, y) = Conj(m C M) (( {P}(x, m) , {Q}(m, y) )).
  −
 
  −
Compare this with the usual form of composition, typically notated as "P.Q" and defined as follows:
  −
 
  −
{P.Q}(x, y) = Disj(m C M) ( {P}(x, m) . {Q}(m, y) ).
  −
</pre>
  −
 
  −
==Appendices==
  −
 
  −
===Logical Translation Rule 1===
      
<br>
 
<br>
Line 1,997: Line 1,987:  
|
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:48px; text-align:right"
+
|- style="height:50px; text-align:center"
| width="98%" | <math>\text{Logical Translation Rule 1}\!</math>
+
| style="width:80%" | &nbsp;
| width="2%"  | &nbsp;
+
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~2.1}</math>
 
|}
 
|}
 
|-
 
|-
 
|
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:48px"
+
|- style="height:50px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
+
| width="10%" style="border-top:1px solid black" | <math>\text{If}\!</math>
| width="80%" style="border-top:1px solid black" |
+
| width="68%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
<math>s ~\text{is a sentence about things in the universe X}</math>
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
|- style="height:48px"
+
|- style="height:50px"
 
| &nbsp;
 
| &nbsp;
| <math>\text{and}\!</math>
+
| <math>\text{then}\!</math>
| <math>p ~\text{is a proposition} ~:~ X \to \underline\mathbb{B}</math>
+
| <math>\text{the following are identical subsets of}~ S \times I :</math>
|- style="height:48px"
+
| style="border-left:1px solid black" | &nbsp;
| &nbsp;
  −
| <math>\text{such that:}\!</math>
  −
| &nbsp;
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{L1a.}\!</math>
  −
| <math>\downharpoonleft s \downharpoonright ~=~ p</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following equations hold:}\!</math>
   
|}
 
|}
 
|-
 
|-
 
|
 
|
{| align="center" cellpadding="0" cellspacing="0" style="text-align:center" width="100%"
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:52px"
+
|- style="height:60px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
| width="18%" style="border-top:1px solid black" align="left" | <math>\text{L1b}_{00}.\!</math>
+
| width="10%" style="border-top:1px solid black" | <math>\operatorname{F2.1a.}</math>
| width="20%" style="border-top:1px solid black" |
+
| width="68%" style="border-top:1px solid black" | <math>\operatorname{Der}^L</math>
<math>\downharpoonleft \operatorname{false} \downharpoonright</math>
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{F2.1a~:~D13a}</math>
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
+
|- style="height:20px"
| width="20%" style="border-top:1px solid black" | <math>(~)</math>
+
| &nbsp;
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
+
| &nbsp;
| width="30%" style="border-top:1px solid black" |
  −
<math>\underline{0} ~:~ X \to \underline\mathbb{B}</math>
  −
|- style="height:52px"
   
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L1b}_{01}.\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\downharpoonleft \operatorname{not}~ s \downharpoonright</math>
+
|- style="height:40px"
| <math>=\!</math>
+
| &nbsp;
| <math>(\downharpoonleft s \downharpoonright)</math>
+
| valign="top" | <math>\operatorname{F2.1b.}</math>
| <math>=\!</math>
+
| valign="top" | <math>\operatorname{Der}(L)</math>
| <math>(p) ~:~ X \to \underline\mathbb{B}</math>
+
| style="border-left:1px solid black; text-align:center" |
|- style="height:52px"
+
<math>\operatorname{F2.1b~:~D13b}</math>
 +
|- style="height:20px"
 +
| &nbsp;
 +
| &nbsp;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:60px"
 +
| &nbsp;
 +
| valign="top" | <math>\operatorname{F2.1c.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ll}
 +
\{ & (x, y) \in S \times I ~: \\
 +
  & \operatorname{Den}(L, x) ~=~ \operatorname{Den}(L, y) \\
 +
\} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<p><math>\operatorname{F2.1c~:~D13c}</math></p>
 +
<p><math>\operatorname{F2.1c~:~R9a}</math></p>
 +
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L1b}_{10}.\!</math>
  −
| <math>\downharpoonleft s \downharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>\downharpoonleft s \downharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>p ~:~ X \to \underline\mathbb{B}</math>
  −
|- style="height:52px"
   
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L1b}_{11}.\!</math>
  −
| <math>\downharpoonleft \operatorname{true} \downharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>((~))</math>
  −
| <math>=\!</math>
  −
| <math>\underline{1} ~:~ X \to \underline\mathbb{B}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Geometric Translation Rule 1===
  −
  −
<br>
  −
  −
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:48px; text-align:right"
  −
| width="98%" | <math>\text{Geometric Translation Rule 1}\!</math>
  −
| width="2%"  | &nbsp;
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:48px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
  −
| width="80%" style="border-top:1px solid black" | <math>Q \subseteq X</math>
  −
|- style="height:48px"
   
| &nbsp;
 
| &nbsp;
| <math>\text{and}\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>p ~:~ X \to \underline\mathbb{B}</math>
+
|- style="height:60px"
|- style="height:48px"
+
| &nbsp;
 +
| valign="top" | <math>\operatorname{F2.1d.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ll}
 +
\{ & (x, y) \in S \times I ~: \\
 +
  & \upharpoonleft \operatorname{Den}(L, x) \upharpoonright ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright \\
 +
\} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F2.1d~:~R9b}</math>
 +
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
| <math>\text{such that:}\!</math>
   
| &nbsp;
 
| &nbsp;
|- style="height:48px"
   
| &nbsp;
 
| &nbsp;
| <math>\text{G1a.}\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\upharpoonleft Q \upharpoonright ~=~ p</math>
+
|- style="height:60px"
|- style="height:48px"
+
| &nbsp;
 +
| valign="top" | <math>\operatorname{F2.1e.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ll}
 +
\{ & (x, y) \in S \times I ~: \\
 +
  & \overset{O}{\underset{o}{\forall}}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) \\
 +
\} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F2.1e~:~R9c}</math>
 +
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
| <math>\text{then}\!</math>
  −
| <math>\text{the following equations hold:}\!</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" style="text-align:center" width="100%"
  −
|- style="height:52px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" align="left" | <math>\text{G1b}_{00}.\!</math>
  −
| width="20%" style="border-top:1px solid black" |
  −
<math>\upharpoonleft \varnothing \upharpoonright</math>
  −
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
  −
| width="20%" style="border-top:1px solid black" | <math>(~)</math>
  −
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
  −
| width="30%" style="border-top:1px solid black" |
  −
<math>\underline{0} ~:~ X \to \underline\mathbb{B}</math>
  −
|- style="height:52px"
   
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G1b}_{01}.\!</math>
  −
| <math>\upharpoonleft {}^{_\sim} Q \upharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>(\upharpoonleft Q \upharpoonright)</math>
  −
| <math>=\!</math>
  −
| <math>(p) ~:~ X \to \underline\mathbb{B}</math>
  −
|- style="height:52px"
   
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G1b}_{10}.\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\upharpoonleft Q \upharpoonright</math>
+
|- style="height:60px"
| <math>=\!</math>
+
| &nbsp;
| <math>\upharpoonleft Q \upharpoonright</math>
+
| valign="top" | <math>\operatorname{F2.1f.}</math>
| <math>=\!</math>
+
| valign="top" |
| <math>p ~:~ X \to \underline\mathbb{B}</math>
+
<math>\begin{array}{ll}
|- style="height:52px"
+
\{ & (x, y) \in S \times I ~: \\
 +
  & \underset{o \in O}{\operatorname{Conj}}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) \\
 +
\} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F2.1f~:~R9d}</math>
 +
|- style="height:20px"
 +
| &nbsp;
 +
| &nbsp;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:60px"
 +
| &nbsp;
 +
| valign="top" | <math>\operatorname{F2.1g.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ll}
 +
\{ & (x, y) \in S \times I ~: \\
 +
  & \underset{o \in O}{\operatorname{Conj}}~ \underline{((}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright (o) ~,~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright (o) ~\underline{))} \\
 +
\} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F2.1g~:~R9e}</math>
 +
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G1b}_{11}.\!</math>
+
| &nbsp;
| <math>\upharpoonleft X \upharpoonright</math>
+
| &nbsp;
| <math>=\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>((~))</math>
+
|- style="height:60px"
| <math>=\!</math>
+
| &nbsp;
| <math>\underline{1} ~:~ X \to \underline\mathbb{B}</math>
+
| valign="top" | <math>\operatorname{F2.1h.}</math>
|}
+
| valign="top" |
|}
+
<math>\begin{array}{ll}
 
+
\{ & (x, y) \in S \times I ~: \\
<br>
+
  & \underset{o \in O}{\operatorname{Conj}}~ \underline{((}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright ~,~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright ~\underline{))}^\$ (o) \\
 
+
\} & \\
===Logical Translation Rule 2===
+
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<p><math>\operatorname{F2.1h~:~R9f}</math></p>
 +
<p><math>\operatorname{F2.1h~:~D12e}</math></p>
 +
|- style="height:20px"
 +
| &nbsp;
 +
| &nbsp;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:60px"
 +
| &nbsp;
 +
| valign="top" | <math>\operatorname{F2.1i.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ll}
 +
\{ & (x, y) \in S \times I ~: \\
 +
  & \underset{o \in O}{\operatorname{Conj}}~ \underline{((}~ \upharpoonleft L_{OS} \cdot x \upharpoonright ~,~ \upharpoonleft L_{OS} \cdot y \upharpoonright ~\underline{))}^\$ (o) \\
 +
\} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F2.1i~:~D12a}</math>
 +
|}
 +
|}
    
<br>
 
<br>
Line 2,152: Line 2,146:  
|
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:48px; text-align:right"
+
|- style="height:50px; text-align:center"
| width="98%" | <math>\text{Logical Translation Rule 2}\!</math>
+
| style="width:80%" | &nbsp;
| width="2%"  | &nbsp;
+
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~2.2}</math>
 
|}
 
|}
 
|-
 
|-
 
|
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:48px"
+
|- style="height:50px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
+
| width="12%" style="border-top:1px solid black" | <math>\text{If}\!</math>
| width="84%" style="border-top:1px solid black" |
+
| width="66%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
<math>s, t ~\text{are sentences about things in the universe}~ X</math>
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
|- style="height:48px"
+
|- style="height:50px"
 
| &nbsp;
 
| &nbsp;
| <math>\text{and}\!</math>
+
| <math>\text{then}\!</math>
| <math>p, q ~\text{are propositions} ~:~ X \to \underline\mathbb{B}</math>
+
| <math>\text{the following are equivalent:}\!</math>
|- style="height:48px"
+
| style="border-left:1px solid black" | &nbsp;
| &nbsp;
  −
| <math>\text{such that:}\!</math>
  −
| &nbsp;
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{L2a.}\!</math>
  −
| <math>\downharpoonleft s \downharpoonright ~=~ p \quad \operatorname{and} \quad \downharpoonleft t \downharpoonright ~=~ q</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following equations hold:}\!</math>
   
|}
 
|}
 
|-
 
|-
 
|
 
|
{| align="center" cellpadding="0" cellspacing="0" style="text-align:center" width="100%"
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:52px"
+
|- style="height:10px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
| width="14%" style="border-top:1px solid black" align="left" | <math>\text{L2b}_{0}.\!</math>
+
| width="12%" style="border-top:1px solid black" | &nbsp;
| width="32%" style="border-top:1px solid black" |
+
| width="66%" style="border-top:1px solid black" | &nbsp;
<math>\downharpoonleft \operatorname{false} \downharpoonright</math>
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
| width="4%" style="border-top:1px solid black" | <math>=\!</math>
+
|- style="height:100px"
| width="28%" style="border-top:1px solid black" | <math>(~)</math>
  −
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
  −
| width="16%" style="border-top:1px solid black" | <math>(~)</math>
  −
|- style="height:52px"
   
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{1}.\!</math>
+
| valign="top" | <math>\operatorname{F2.2a.}</math>
| <math>\downharpoonleft \operatorname{neither}~ s ~\operatorname{nor}~ t \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{cccl}
| <math>(\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright)</math>
+
\operatorname{Der}^L
| <math>=\!</math>
+
& = & \{ & (x, y) \in S \times I ~: \\
| <math>(p)(q)\!</math>
+
&  &    & \begin{array}{ccl}
|- style="height:52px"
+
          \underset{o \in O}{\operatorname{Conj}} \\
 +
          & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 +
          & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 +
          & ) & \\
 +
          \end{array} \\
 +
&  & \} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.2a~:~R11a}</math>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{2}.\!</math>
+
| valign="top" | <math>\operatorname{F2.2b.}</math>
| <math>\downharpoonleft \operatorname{not}~ s ~\operatorname{but}~ t \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{ccccl}
| <math>(\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright</math>
+
\upharpoonleft \operatorname{Der}^L \upharpoonright
| <math>=\!</math>
+
& = & \upharpoonleft  & \{ & (x, y) \in S \times I ~: \\
| <math>(p) q\!</math>
+
&  &                &    & \begin{array}{ccl}
|- style="height:52px"
+
                            \underset{o \in O}{\operatorname{Conj}} \\
 +
                            & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 +
                            & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 +
                            & ) & \\
 +
                            \end{array} \\
 +
&  &                & \} & \\
 +
&  & \upharpoonright &    & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F2.2b~:~R11b}</math>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{3}.\!</math>
+
| valign="top" | <math>\operatorname{F2.2c.}</math>
| <math>\downharpoonleft \operatorname{not}~ s \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{cccl}
| <math>(\downharpoonleft s \downharpoonright)</math>
+
\upharpoonleft \operatorname{Der}^L \upharpoonright
| <math>=\!</math>
+
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
| <math>(p)\!</math>
+
&  &    & \begin{array}{cccl}
|- style="height:52px"
+
          \downharpoonleft & \underset{o \in O}{\operatorname{Conj}} \\
 +
          &                & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 +
          &                & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 +
          &                & ) & \\
 +
          \downharpoonright &  & \\
 +
          \end{array} \\
 +
&  & \} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F2.2c~:~R11c}</math></p>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{4}.\!</math>
+
| valign="top" | <math>\operatorname{F2.2d.}</math>
| <math>\downharpoonleft s ~\operatorname{and~not}~ t \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{cccl}
| <math>\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright)</math>
+
\upharpoonleft \operatorname{Der}^L \upharpoonright
| <math>=\!</math>
+
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
| <math>p (q)\!</math>
+
&  &    & \begin{array}{cccl}
|- style="height:52px"
+
          \underset{o \in O}{\operatorname{Conj}} \\
 +
          & \downharpoonleft & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 +
          &                  & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 +
          &                  & ) & \\
 +
          & \downharpoonright &  & \\
 +
          \end{array} \\
 +
&  & \} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F2.2d~:~Log}</math>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{5}.\!</math>
+
| valign="top" | <math>\operatorname{F2.2e.}</math>
| <math>\downharpoonleft \operatorname{not}~ t \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{cccl}
| <math>(\downharpoonleft t \downharpoonright)</math>
+
\upharpoonleft \operatorname{Der}^L \upharpoonright
| <math>=\!</math>
+
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
| <math>(q)\!</math>
+
&  &    & \begin{array}{ccl}
|- style="height:52px"
+
          \underset{o \in O}{\operatorname{Conj}} \\
 +
          & \underline{((} & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 +
          & ,              & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 +
          & \underline{))} & \\
 +
          \end{array} \\
 +
&  & \} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F2.2e~:~Log}</math>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{6}.\!</math>
+
| valign="top" | <math>\operatorname{F2.2f.}</math>
| <math>\downharpoonleft s ~\operatorname{or}~ t, ~\operatorname{not~both} \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{cccl}
| <math>(\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright)</math>
+
\upharpoonleft \operatorname{Der}^L \upharpoonright
| <math>=\!</math>
+
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
| <math>(p, q)\!</math>
+
&  &    & \begin{array}{cll}
|- style="height:52px"
+
          \underset{o \in O}{\operatorname{Conj}} \\
| &nbsp;
+
          & \underline{((}    & \upharpoonleft \operatorname{Den}^L x \upharpoonright \\
| align="left" | <math>\text{L2b}_{7}.\!</math>
+
          & ,                 & \upharpoonleft \operatorname{Den}^L y \upharpoonright \\
| <math>\downharpoonleft \operatorname{not~both}~ s ~\operatorname{and}~ t \downharpoonright</math>
+
          & \underline{))}^\$ & (o) \\
| <math>=\!</math>
+
          \end{array} \\
| <math>(\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright)</math>
+
&  & \} & \\
| <math>=\!</math>
+
\end{array}</math>
| <math>(p q)\!</math>
+
| style="border-left:1px solid black; text-align:center" |
|- style="height:52px"
+
<math>\operatorname{F2.2f~:~$~}</math>
 +
|}
 +
|}
 +
 
 +
<br>
 +
 
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:50px; text-align:center"
 +
| style="width:80%" | &nbsp;
 +
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~2.3}</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:50px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="12%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 +
| width="66%" style="border-top:1px solid black" | <math>L ~\subseteq~ O \times S \times I</math>
 +
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 +
|- style="height:50px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{8}.\!</math>
+
| <math>\text{then}\!</math>
| <math>\downharpoonleft s ~\operatorname{and}~ t \downharpoonright</math>
+
| <math>\text{the following are equivalent:}\!</math>
| <math>=\!</math>
+
| style="border-left:1px solid black" | &nbsp;
| <math>\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright</math>
+
|}
| <math>=\!</math>
+
|-
| <math>p q\!</math>
+
|
|- style="height:52px"
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:10px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="12%" style="border-top:1px solid black" | &nbsp;
 +
| width="66%" style="border-top:1px solid black" | &nbsp;
 +
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{9}.\!</math>
+
| valign="top" | <math>\operatorname{F2.3a.}</math>
| <math>\downharpoonleft s ~\operatorname{is~equivalent~to}~ t \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{cccl}
| <math>((\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright))</math>
+
\operatorname{Der}^L
| <math>=\!</math>
+
& = & \{ & (x, y) \in S \times I ~: \\
| <math>((p, q))\!</math>
+
&  &    & \begin{array}{ccl}
|- style="height:52px"
+
          \underset{o \in O}{\operatorname{Conj}} \\
 +
          & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 +
          & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 +
          & ) & \\
 +
          \end{array} \\
 +
&  & \} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3a~:~R11a}</math>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{10}.\!</math>
+
| valign="top" | <math>\operatorname{F2.3b.}</math>
| <math>\downharpoonleft t \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{ccccl}
| <math>\downharpoonleft t \downharpoonright</math>
+
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
| <math>=\!</math>
+
& = & \downharpoonleft & \underset{o \in O}{\operatorname{Conj}} \\
| <math>q\!</math>
+
&  &                  & & \begin{array}{cl}
|- style="height:52px"
+
                            ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 +
                            = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 +
                            ) & \\
 +
                            \end{array} \\
 +
&  & \downharpoonright & & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3b~:~R11d}</math>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{11}.\!</math>
+
| valign="top" | <math>\operatorname{F2.3c.}</math>
| <math>\downharpoonleft s ~\operatorname{implies}~ t \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{ccccl}
| <math>(\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright))</math>
+
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
| <math>=\!</math>
+
& = & \underset{o \in O}{\operatorname{Conj}} \\
| <math>(p (q))\!</math>
+
&  & & \begin{array}{ccl}
|- style="height:52px"
+
        \downharpoonleft  & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\
 +
                          & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\
 +
                          & ) & \\
 +
        \downharpoonright &  & \\
 +
        \end{array} \\
 +
&  & & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3c~:~Log}</math></p>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{12}.\!</math>
+
| valign="top" | <math>\operatorname{F2.3d.}</math>
| <math>\downharpoonleft s \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{ccccl}
| <math>\downharpoonleft s \downharpoonright</math>
+
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
| <math>=\!</math>
+
& = & \underset{o \in O}{\operatorname{Conj}} \\
| <math>p\!</math>
+
&  & & \begin{array}{ccl}
|- style="height:52px"
+
        \downharpoonleft & ( & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, x) \\
 +
                          & = & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, y) \\
 +
                          & ) & \\
 +
        \downharpoonright &  & \\
 +
        \end{array} \\
 +
&  & & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3d~:~Def}</math>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{13}.\!</math>
+
| valign="top" | <math>\operatorname{F2.3e.}</math>
| <math>\downharpoonleft s ~\operatorname{is~implied~by}~ t \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{ccccl}
| <math>((\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright)</math>
+
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
| <math>=\!</math>
+
& = & \underset{o \in O}{\operatorname{Conj}} \\
| <math>((p) q)\!</math>
+
&  & & \begin{array}{cl}
|- style="height:52px"
+
        \underline{((} & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, x) \\
 +
        ,              & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, y) \\
 +
        \underline{))} & \\
 +
        \end{array} \\
 +
&  & & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<p><math>\operatorname{F2.3e~:~Log}</math></p>
 +
<p><math>\operatorname{F2.3e~:~D10b}</math></p>
 +
|- style="height:20px"
 +
| colspan="3" | &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:100px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{14}.\!</math>
+
| valign="top" | <math>\operatorname{F2.3f.}</math>
| <math>\downharpoonleft s ~\operatorname{or}~ t \downharpoonright</math>
+
| valign="top" |
| <math>=\!</math>
+
<math>\begin{array}{ccccl}
| <math>((\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright))</math>
+
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
| <math>=\!</math>
+
& = & \underset{o \in O}{\operatorname{Conj}} \\
| <math>((p)(q))\!</math>
+
&  & & \begin{array}{cl}
|- style="height:52px"
+
        \underline{((} & \upharpoonleft L_{OS} \upharpoonright (o, x) \\
| &nbsp;
+
        ,              & \upharpoonleft L_{OS} \upharpoonright (o, y) \\
| align="left" | <math>\text{L2b}_{15}.\!</math>
+
        \underline{))} & \\
| <math>\downharpoonleft \operatorname{true} \downharpoonright</math>
+
        \end{array} \\
| <math>=\!</math>
+
&  & & \\
| <math>((~))</math>
+
\end{array}</math>
| <math>=\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3f~:~D10a}</math>
| <math>((~))</math>
+
|}
 +
|}
 +
 
 +
<br>
 +
 
 +
=====1.3.12.3.  Digression on Derived Relations=====
 +
 
 +
A better understanding of derived equivalence relations (DERs) can be achieved by placing their constructions within a more general context and thus comparing the associated type of derivation operation, namely, the one that takes a triadic relation <math>L\!</math> into a dyadic relation <math>\operatorname{Der}(L),</math> with other types of operations on triadic relations.  The proper setting would permit a comparative study of all their constructions from a basic set of projections and a full array of compositions on dyadic relations.
 +
 
 +
To that end, let the derivation <math>\operatorname{Der}(L)</math> be expressed in the following way:
 +
 
 +
{| align="center" cellpadding="8" width="90%"
 +
| <math>\upharpoonleft \operatorname{Der}(L) \upharpoonright (x, y) \quad = \quad \underset{o \in O}{\operatorname{Conj}} ~\underline{((}~ \upharpoonleft L_{SO} \upharpoonright (x, o) ~,~ \upharpoonleft L_{OS} \upharpoonright (o, y) ~\underline{))}~.</math>
 +
|}
 +
 
 +
From this may be abstracted a way of composing two dyadic relations that have a domain in common.  For example, let <math>P \subseteq X \times M</math> and <math>Q \subseteq M \times Y</math> be dyadic relations that have the middle domain <math>M\!</math> in common.  Then we may define a form of composition, notated <math>P \circeq Q,</math> where <math>P \circeq Q ~\subseteq~ X \times Y</math> is defined as follows:
 +
 
 +
{| align="center" cellpadding="8" width="90%"
 +
| <math>\upharpoonleft P \circeq Q \upharpoonright (x, y) \quad = \quad \underset{m \in M}{\operatorname{Conj}} ~\underline{((}~ \upharpoonleft P \upharpoonright (x, m) ~,~ \upharpoonleft Q \upharpoonright (m, y) ~\underline{))}~.</math>
 
|}
 
|}
 +
 +
Compare this with the usual form of composition, typically notated <math>P \circ Q</math> and defined as follows:
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
| <math>\upharpoonleft P \circ Q \upharpoonright (x, y) \quad = \quad \underset{m \in M}{\operatorname{Disj}} ~\upharpoonleft P \upharpoonright (x, m) ~\cdot~ \upharpoonleft Q \upharpoonright (m, y)~.</math>
 
|}
 
|}
   −
<br>
+
==Appendices==
   −
===Geometric Translation Rule 2===
+
===Logical Translation Rule 1===
    
<br>
 
<br>
Line 2,326: Line 2,472:  
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
|- style="height:48px; text-align:right"
 
|- style="height:48px; text-align:right"
| width="98%" | <math>\text{Geometric Translation Rule 2}\!</math>
+
| width="98%" | <math>\text{Logical Translation Rule 1}\!</math>
 
| width="2%"  | &nbsp;
 
| width="2%"  | &nbsp;
 
|}
 
|}
Line 2,334: Line 2,480:  
|- style="height:48px"
 
|- style="height:48px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
+
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
| width="84%" style="border-top:1px solid black" | <math>P, Q \subseteq X</math>
+
| width="80%" style="border-top:1px solid black" |
 +
<math>s ~\text{is a sentence about things in the universe X}</math>
 
|- style="height:48px"
 
|- style="height:48px"
 
| &nbsp;
 
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>\text{and}\!</math>
| <math>p, q ~:~ X \to \underline\mathbb{B}</math>
+
| <math>p ~\text{is a proposition} ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:48px"
 
|- style="height:48px"
 
| &nbsp;
 
| &nbsp;
Line 2,346: Line 2,493:  
|- style="height:48px"
 
|- style="height:48px"
 
| &nbsp;
 
| &nbsp;
| <math>\text{G2a.}\!</math>
+
| <math>\text{L1a.}\!</math>
| <math>\upharpoonleft P \upharpoonright ~=~ p \quad \operatorname{and} \quad \upharpoonleft Q \upharpoonright ~=~ q</math>
+
| <math>\downharpoonleft s \downharpoonright ~=~ p</math>
 
|- style="height:48px"
 
|- style="height:48px"
 
| &nbsp;
 
| &nbsp;
Line 2,358: Line 2,505:  
|- style="height:52px"
 
|- style="height:52px"
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
| width="2%"  style="border-top:1px solid black" | &nbsp;
| width="14%" style="border-top:1px solid black" align="left" | <math>\text{G2b}_{0}.\!</math>
+
| width="18%" style="border-top:1px solid black" align="left" | <math>\text{L1b}_{00}.\!</math>
| width="32%" style="border-top:1px solid black" |
+
| width="20%" style="border-top:1px solid black" |
<math>\upharpoonleft \varnothing \upharpoonright</math>
+
<math>\downharpoonleft \operatorname{false} \downharpoonright</math>
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
+
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
| width="28%" style="border-top:1px solid black" | <math>(~)</math>
+
| width="20%" style="border-top:1px solid black" | <math>(~)</math>
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
+
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
| width="16%" style="border-top:1px solid black" | <math>(~)</math>
+
| width="30%" style="border-top:1px solid black" |
 +
<math>\underline{0} ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
|- style="height:52px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{1}.\!</math>
+
| align="left" | <math>\text{L1b}_{01}.\!</math>
| <math>\upharpoonleft \overline{P} ~\cap~ \overline{Q} \upharpoonright</math>
+
| <math>\downharpoonleft \operatorname{not}~ s \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>(\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright)</math>
+
| <math>(\downharpoonleft s \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>(p)(q)\!</math>
+
| <math>(p) ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
|- style="height:52px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{2}.\!</math>
+
| align="left" | <math>\text{L1b}_{10}.\!</math>
| <math>\upharpoonleft \overline{P} ~\cap~ Q \upharpoonright</math>
+
| <math>\downharpoonleft s \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>(\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright</math>
+
| <math>\downharpoonleft s \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>(p) q\!</math>
+
| <math>p ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
|- style="height:52px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{3}.\!</math>
+
| align="left" | <math>\text{L1b}_{11}.\!</math>
| <math>\upharpoonleft \overline{P} \upharpoonright</math>
+
| <math>\downharpoonleft \operatorname{true} \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>(\upharpoonleft P \upharpoonright)</math>
+
| <math>((~))</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>(p)\!</math>
+
| <math>\underline{1} ~:~ X \to \underline\mathbb{B}</math>
|- style="height:52px"
+
|}
| &nbsp;
+
|}
| align="left" | <math>\text{G2b}_{4}.\!</math>
+
 
| <math>\upharpoonleft P ~\cap~ \overline{Q} \upharpoonright</math>
+
<br>
| <math>=\!</math>
+
 
| <math>\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright)</math>
+
===Geometric Translation Rule 1===
| <math>=\!</math>
+
 
| <math>p (q)\!</math>
+
<br>
|- style="height:52px"
+
 
| &nbsp;
+
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
| align="left" | <math>\text{G2b}_{5}.\!</math>
+
|
| <math>\upharpoonleft \overline{Q} \upharpoonright</math>
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
| <math>=\!</math>
+
|- style="height:48px; text-align:right"
| <math>(\upharpoonleft Q \upharpoonright)</math>
+
| width="98%" | <math>\text{Geometric Translation Rule 1}\!</math>
| <math>=\!</math>
+
| width="2%"  | &nbsp;
| <math>(q)\!</math>
+
|}
|- style="height:52px"
+
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:48px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 +
| width="80%" style="border-top:1px solid black" | <math>Q \subseteq X</math>
 +
|- style="height:48px"
 +
| &nbsp;
 +
| <math>\text{and}\!</math>
 +
| <math>p ~:~ X \to \underline\mathbb{B}</math>
 +
|- style="height:48px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{6}.\!</math>
+
| <math>\text{such that:}\!</math>
| <math>\upharpoonleft P ~+~ Q \upharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>(\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright)</math>
  −
| <math>=\!</math>
  −
| <math>(p, q)\!</math>
  −
|- style="height:52px"
   
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{7}.\!</math>
+
|- style="height:48px"
| <math>\upharpoonleft \overline{P ~\cap~ Q} \upharpoonright</math>
+
| &nbsp;
 +
| <math>\text{G1a.}\!</math>
 +
| <math>\upharpoonleft Q \upharpoonright ~=~ p</math>
 +
|- style="height:48px"
 +
| &nbsp;
 +
| <math>\text{then}\!</math>
 +
| <math>\text{the following equations hold:}\!</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="text-align:center" width="100%"
 +
|- style="height:52px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="18%" style="border-top:1px solid black" align="left" | <math>\text{G1b}_{00}.\!</math>
 +
| width="20%" style="border-top:1px solid black" |
 +
<math>\upharpoonleft \varnothing \upharpoonright</math>
 +
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
 +
| width="20%" style="border-top:1px solid black" | <math>(~)</math>
 +
| width="5%"  style="border-top:1px solid black" | <math>=\!</math>
 +
| width="30%" style="border-top:1px solid black" |
 +
<math>\underline{0} ~:~ X \to \underline\mathbb{B}</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G1b}_{01}.\!</math>
 +
| <math>\upharpoonleft {}^{_\sim} Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>(\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright)</math>
+
| <math>(\upharpoonleft Q \upharpoonright)</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>(p q)\!</math>
+
| <math>(p) ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
|- style="height:52px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{8}.\!</math>
+
| align="left" | <math>\text{G1b}_{10}.\!</math>
| <math>\upharpoonleft P ~\cap~ Q \upharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>p q\!</math>
  −
|- style="height:52px"
  −
| &nbsp;
  −
| align="left" | <math>\text{G2b}_{9}.\!</math>
  −
| <math>\upharpoonleft \overline{P ~+~ Q} \upharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>((\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright))</math>
  −
| <math>=\!</math>
  −
| <math>((p, q))\!</math>
  −
|- style="height:52px"
  −
| &nbsp;
  −
| align="left" | <math>\text{G2b}_{10}.\!</math>
   
| <math>\upharpoonleft Q \upharpoonright</math>
 
| <math>\upharpoonleft Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
 
| <math>\upharpoonleft Q \upharpoonright</math>
 
| <math>\upharpoonleft Q \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>q\!</math>
+
| <math>p ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:52px"
 
|- style="height:52px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{11}.\!</math>
+
| align="left" | <math>\text{G1b}_{11}.\!</math>
| <math>\upharpoonleft \overline{P ~\cap~ \overline{Q}} \upharpoonright</math>
+
| <math>\upharpoonleft X \upharpoonright</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>(\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright))</math>
+
| <math>((~))</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
| <math>(p (q))\!</math>
+
| <math>\underline{1} ~:~ X \to \underline\mathbb{B}</math>
|- style="height:52px"
+
|}
| &nbsp;
+
|}
| align="left" | <math>\text{G2b}_{12}.\!</math>
+
 
| <math>\upharpoonleft P \upharpoonright</math>
+
<br>
| <math>=\!</math>
+
 
| <math>\upharpoonleft P \upharpoonright</math>
+
===Logical Translation Rule 2===
| <math>=\!</math>
+
 
| <math>p\!</math>
+
<br>
|- style="height:52px"
+
 
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:48px; text-align:right"
 +
| width="98%" | <math>\text{Logical Translation Rule 2}\!</math>
 +
| width="2%"  | &nbsp;
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:48px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 +
| width="84%" style="border-top:1px solid black" |
 +
<math>s, t ~\text{are sentences about things in the universe}~ X</math>
 +
|- style="height:48px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{13}.\!</math>
+
| <math>\text{and}\!</math>
| <math>\upharpoonleft \overline{\overline{P} ~\cap~ Q} \upharpoonright</math>
+
| <math>p, q ~\text{are propositions} ~:~ X \to \underline\mathbb{B}</math>
| <math>=\!</math>
+
|- style="height:48px"
| <math>((\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright)</math>
+
| &nbsp;
 +
| <math>\text{such that:}\!</math>
 +
| &nbsp;
 +
|- style="height:48px"
 +
| &nbsp;
 +
| <math>\text{L2a.}\!</math>
 +
| <math>\downharpoonleft s \downharpoonright ~=~ p \quad \operatorname{and} \quad \downharpoonleft t \downharpoonright ~=~ q</math>
 +
|- style="height:48px"
 +
| &nbsp;
 +
| <math>\text{then}\!</math>
 +
| <math>\text{the following equations hold:}\!</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="text-align:center" width="100%"
 +
|- style="height:52px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="14%" style="border-top:1px solid black" align="left" | <math>\text{L2b}_{0}.\!</math>
 +
| width="32%" style="border-top:1px solid black" |
 +
<math>\downharpoonleft \operatorname{false} \downharpoonright</math>
 +
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
 +
| width="28%" style="border-top:1px solid black" | <math>(~)</math>
 +
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
 +
| width="16%" style="border-top:1px solid black" | <math>(~)</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{1}.\!</math>
 +
| <math>\downharpoonleft \operatorname{neither}~ s ~\operatorname{nor}~ t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(p)(q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{2}.\!</math>
 +
| <math>\downharpoonleft \operatorname{not}~ s ~\operatorname{but}~ t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(p) q\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{3}.\!</math>
 +
| <math>\downharpoonleft \operatorname{not}~ s \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\downharpoonleft s \downharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(p)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{4}.\!</math>
 +
| <math>\downharpoonleft s ~\operatorname{and~not}~ t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>p (q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{5}.\!</math>
 +
| <math>\downharpoonleft \operatorname{not}~ t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\downharpoonleft t \downharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{6}.\!</math>
 +
| <math>\downharpoonleft s ~\operatorname{or}~ t, ~\operatorname{not~both} \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(p, q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{7}.\!</math>
 +
| <math>\downharpoonleft \operatorname{not~both}~ s ~\operatorname{and}~ t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(p q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{8}.\!</math>
 +
| <math>\downharpoonleft s ~\operatorname{and}~ t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>p q\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{9}.\!</math>
 +
| <math>\downharpoonleft s ~\operatorname{is~equivalent~to}~ t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>((\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright))</math>
 +
| <math>=\!</math>
 +
| <math>((p, q))\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{10}.\!</math>
 +
| <math>\downharpoonleft t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>\downharpoonleft t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>q\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{11}.\!</math>
 +
| <math>\downharpoonleft s ~\operatorname{implies}~ t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright))</math>
 +
| <math>=\!</math>
 +
| <math>(p (q))\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{12}.\!</math>
 +
| <math>\downharpoonleft s \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>\downharpoonleft s \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>p\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{13}.\!</math>
 +
| <math>\downharpoonleft s ~\operatorname{is~implied~by}~ t \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>((\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>=\!</math>
 
| <math>((p) q)\!</math>
 
| <math>((p) q)\!</math>
|- style="height:52px"
+
|- style="height:52px"
| &nbsp;
+
| &nbsp;
| align="left" | <math>\text{G2b}_{14}.\!</math>
+
| align="left" | <math>\text{L2b}_{14}.\!</math>
| <math>\upharpoonleft P ~\cup~ Q \upharpoonright</math>
+
| <math>\downharpoonleft s ~\operatorname{or}~ t \downharpoonright</math>
| <math>=\!</math>
+
| <math>=\!</math>
| <math>((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright))</math>
+
| <math>((\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright))</math>
| <math>=\!</math>
+
| <math>=\!</math>
| <math>((p)(q))\!</math>
+
| <math>((p)(q))\!</math>
|- style="height:52px"
+
|- style="height:52px"
| &nbsp;
+
| &nbsp;
| align="left" | <math>\text{G2b}_{15}.\!</math>
+
| align="left" | <math>\text{L2b}_{15}.\!</math>
| <math>\upharpoonleft X \upharpoonright</math>
+
| <math>\downharpoonleft \operatorname{true} \downharpoonright</math>
| <math>=\!</math>
+
| <math>=\!</math>
| <math>((~))</math>
+
| <math>((~))</math>
| <math>=\!</math>
+
| <math>=\!</math>
| <math>((~))</math>
+
| <math>((~))</math>
|}
+
|}
|}
+
|}
 
+
 
<br>
+
<br>
 
+
 
==Document History==
+
===Geometric Translation Rule 2===
 +
 
 +
<br>
 +
 
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black" width="90%"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:48px; text-align:right"
 +
| width="98%" | <math>\text{Geometric Translation Rule 2}\!</math>
 +
| width="2%"  | &nbsp;
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:48px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 +
| width="84%" style="border-top:1px solid black" | <math>P, Q \subseteq X</math>
 +
|- style="height:48px"
 +
| &nbsp;
 +
| <math>\text{and}\!</math>
 +
| <math>p, q ~:~ X \to \underline\mathbb{B}</math>
 +
|- style="height:48px"
 +
| &nbsp;
 +
| <math>\text{such that:}\!</math>
 +
| &nbsp;
 +
|- style="height:48px"
 +
| &nbsp;
 +
| <math>\text{G2a.}\!</math>
 +
| <math>\upharpoonleft P \upharpoonright ~=~ p \quad \operatorname{and} \quad \upharpoonleft Q \upharpoonright ~=~ q</math>
 +
|- style="height:48px"
 +
| &nbsp;
 +
| <math>\text{then}\!</math>
 +
| <math>\text{the following equations hold:}\!</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="text-align:center" width="100%"
 +
|- style="height:52px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="14%" style="border-top:1px solid black" align="left" | <math>\text{G2b}_{0}.\!</math>
 +
| width="32%" style="border-top:1px solid black" |
 +
<math>\upharpoonleft \varnothing \upharpoonright</math>
 +
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
 +
| width="28%" style="border-top:1px solid black" | <math>(~)</math>
 +
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
 +
| width="16%" style="border-top:1px solid black" | <math>(~)</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{1}.\!</math>
 +
| <math>\upharpoonleft \overline{P} ~\cap~ \overline{Q} \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(p)(q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{2}.\!</math>
 +
| <math>\upharpoonleft \overline{P} ~\cap~ Q \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(p) q\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{3}.\!</math>
 +
| <math>\upharpoonleft \overline{P} \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\upharpoonleft P \upharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(p)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{4}.\!</math>
 +
| <math>\upharpoonleft P ~\cap~ \overline{Q} \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>p (q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{5}.\!</math>
 +
| <math>\upharpoonleft \overline{Q} \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\upharpoonleft Q \upharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{6}.\!</math>
 +
| <math>\upharpoonleft P ~+~ Q \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(p, q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{7}.\!</math>
 +
| <math>\upharpoonleft \overline{P ~\cap~ Q} \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(p q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{8}.\!</math>
 +
| <math>\upharpoonleft P ~\cap~ Q \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>p q\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{9}.\!</math>
 +
| <math>\upharpoonleft \overline{P ~+~ Q} \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>((\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright))</math>
 +
| <math>=\!</math>
 +
| <math>((p, q))\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{10}.\!</math>
 +
| <math>\upharpoonleft Q \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>\upharpoonleft Q \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>q\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{11}.\!</math>
 +
| <math>\upharpoonleft \overline{P ~\cap~ \overline{Q}} \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright))</math>
 +
| <math>=\!</math>
 +
| <math>(p (q))\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{12}.\!</math>
 +
| <math>\upharpoonleft P \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>\upharpoonleft P \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>p\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{13}.\!</math>
 +
| <math>\upharpoonleft \overline{\overline{P} ~\cap~ Q} \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>((\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>((p) q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{14}.\!</math>
 +
| <math>\upharpoonleft P ~\cup~ Q \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright))</math>
 +
| <math>=\!</math>
 +
| <math>((p)(q))\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G2b}_{15}.\!</math>
 +
| <math>\upharpoonleft X \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>((~))</math>
 +
| <math>=\!</math>
 +
| <math>((~))</math>
 +
|}
 +
|}
 +
 
 +
<br>
 +
 
 +
==Document History==
 +
 
 +
<pre>
 +
| Subject:  Inquiry Driven Systems : An Inquiry Into Inquiry
 +
| Contact:  Jon Awbrey
 +
| Version:  Draft 8.70
 +
| Created:  23 Jun 1996
 +
| Revised:  06 Jan 2002
 +
| Advisor:  M.A. Zohdy
 +
| Setting:  Oakland University, Rochester, Michigan, USA
 +
| Excerpt:  Section 1.3.10 (Recurring Themes)
 +
| Excerpt:  Subsections 1.3.10.8 - 1.3.10.13
 +
</pre>
   −
<pre>
+
***
| Subject:  Inquiry Driven Systems : An Inquiry Into Inquiry
  −
| Contact:  Jon Awbrey
  −
| Version:  Draft 8.70
  −
| Created:  23 Jun 1996
  −
| Revised:  06 Jan 2002
  −
| Advisor:  M.A. Zohdy
  −
| Setting:  Oakland University, Rochester, Michigan, USA
  −
| Excerpt:  Section 1.3.10 (Recurring Themes)
  −
| Excerpt:  Subsections 1.3.10.8 - 1.3.10.13
  −
</pre>
 
12,080

edits