Difference between revisions of "Directory:Jon Awbrey/Papers/Syntactic Transformations"

MyWikiBiz, Author Your Legacy — Friday November 22, 2024
Jump to navigationJump to search
(→‎Syntactic Transformation Rules: format definition box)
('''Author: Jon Awbrey''')
 
(54 intermediate revisions by the same user not shown)
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>
[v = w] is a proposition : B2 -> B,
+
|-
 
+
| <math>\downharpoonleft v(u) = w(u) \downharpoonright (u)</math>
and the following are identical values in B:
+
|}
  
V1a. [ v = w ](v, w)
+
'''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:
  
V1b. [ v <=> w ](v, w)
+
* [http://mywikibiz.com/User:Jon_Awbrey/SCRATCHPAD#Value_Rule_1 Value Rule 1]
 
 
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
 
 
 
If f, g : U -> B,
 
 
 
then the following are identical propositions on U:
 
 
 
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%"
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
Line 789: Line 745:
 
<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%"
Rule 5
+
|
If X, Y c U,
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:40px; text-align:center"
then the following are equivalent:
+
| width="80%" | &nbsp;
 
+
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~5}</math>
R5a. X = Y. :D2a
+
|}
::
+
|-
R5b. u C X  <=>  u C Y, for all u C U. :D2b
+
|
:D7a
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
::
+
|- style="height:40px"
R5c. [u C X] = [u C Y], for all u C U. :D7b
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
:???
+
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
::
+
| width="60%" style="border-top:1px solid black" | <math>P, Q ~\subseteq~ X</math>
R5d. {<u, v> C UxB : v = [u C X]}
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
=
+
|- style="height:40px"
{<u, v> C UxB : v = [u C Y]}. :???
+
| &nbsp;
:D5b
+
| <math>\text{then}\!</math>
::
+
| <math>\text{the following are equivalent:}\!</math>
R5e. {X} = {Y}. :D5a
+
| style="border-left:1px solid black" | &nbsp;
</pre>
+
|}
 
+
|-
<br>
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
<pre>
+
|- style="height:40px"
Rule 6
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
+
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R5a.}</math>
If f, g : U -> V,
+
| width="60%" style="border-top:1px solid black" | <math>P ~=~ Q</math>
 
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R5a~:~D2a}</math>
then the following are equivalent:
+
|- style="height:20px"
 
+
| &nbsp;
R6a. f = g. :D3a
+
| &nbsp;
::
+
| &nbsp;
R6b. f(u) = g(u), for all u C U. :D3b
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
:D6a
+
|- style="height:60px"
::
+
| &nbsp;
R6c. ConjUu (f(u) = g(u)). :D6e
+
| <math>\operatorname{R5b.}</math>
</pre>
+
| <math>\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)</math>
 
+
| style="border-left:1px solid black; text-align:center" |
<br>
+
<p><math>\operatorname{R5b~:~D2b}</math></p>
 
+
<p><math>\operatorname{R5b~:~D7a}</math></p>
<pre>
+
|- style="height:20px"
Rule 7
+
| &nbsp;
 
+
| &nbsp;
If P, Q : U -> B,
+
| &nbsp;
 
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
then the following are equivalent:
+
|- style="height:60px"
 
+
| &nbsp;
R7a. P = Q. :R6a
+
| <math>\operatorname{R5c.}</math>
::
+
| <math>\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright)</math>
R7b. P(u) = Q(u), for all u C U. :R6b
+
| style="border-left:1px solid black; text-align:center" |
::
+
<p><math>\operatorname{R5c~:~D7b}</math></p>
R7c. ConjUu (P(u)  = Q(u)). :R6c
+
<p><math>\operatorname{R5c~:~\_\_?\_\_}</math></p>
:P1a
+
|- style="height:20px"
::
+
| &nbsp;
R7d. ConjUu (P(u) <=> Q(u)). :P1b
+
| &nbsp;
::
+
| &nbsp;
R7e. ConjUu (( P(u) , Q(u) )). :P1c
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
:$1a
+
|- style="height:80px"
::
+
| &nbsp;
R7f. ConjUu (( P , Q ))$(u). :$1b
+
| <math>\operatorname{R5d.}</math>
</pre>
+
|
 
+
<math>\begin{matrix}
<br>
+
\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in P \downharpoonright
 
+
\\
<pre>
+
=
Rule 8
+
\\
 
+
\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in Q \downharpoonright
If S, T are sentences
+
\end{matrix}</math>
about things in the universe U,
+
| style="border-left:1px solid black; text-align:center" |
 
+
<p><math>\operatorname{R5d~:~\_\_?\_\_}</math></p>
then the following are equivalent:
+
<p><math>\operatorname{R5d~:~D5b}</math></p>
 
+
|- style="height:20px"
R8a. S <=> T. :D7a
+
| &nbsp;
::
+
| &nbsp;
R8b. [S] = [T]. :D7b
+
| &nbsp;
:R7a
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
::
+
|- style="height:40px"
R8c. [S](u) = [T](u), for all u C U. :R7b
+
| &nbsp;
::
+
| <math>\operatorname{R5e.}</math>
R8d. ConjUu ( [S](u)  = [T](u) ). :R7c
+
| <math>\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright</math>
::
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R5e~:~D5a}</math>
R8e. ConjUu ( [S](u) <=> [T](u) ). :R7d
+
|}
::
+
|}
R8f. ConjUu (( [S](u) , [T](u) )). :R7e
 
::
 
R8g. ConjUu (( [S] , [T] ))$(u). :R7f
 
 
 
For instance, the observation that expresses the equality of sets in terms of their indicator functions can be formalized according to the pattern in Rule 9, namely, at lines (a, b, c), and these components of Rule 9 can be cited in future uses as "R9a", "R9b", "R9c", respectively. Using Rule 7, annotated as "R7", to adduce a few properties of indicator functions to the account, it is possible to extend Rule 9 by another few steps, referenced as "R9d", "R9e", "R9f", "R9g".
 
</pre>
 
  
 
<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%"
Rule 9
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
If X, Y c U,
+
|- style="height:40px; text-align:center"
 
+
| width="80%" | &nbsp;
then the following are equivalent:
+
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~6}</math>
 
+
|}
R9a. X = Y. :R5a
+
|-
::
+
|
R9b. {X} = {Y}. :R5e
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
:R7a
+
|- style="height:40px"
::
+
| width="2%" style="border-top:1px solid black" | &nbsp;
R9c. {X}(u) = {Y}(u), for all u C U. :R7b
+
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
::
+
| width="60%" style="border-top:1px solid black" | <math>f, g ~:~ X \to Y</math>
R9d. ConjUu ( {X}(u) = {Y}(u) ). :R7c
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
::
+
|- style="height:40px"
R9e. ConjUu ( {X}(u) <=> {Y}(u) ). :R7d
+
| &nbsp;
::
+
| <math>\text{then}\!</math>
R9f. ConjUu (( {X}(u) , {Y}(u) )). :R7e
+
| <math>\text{the following are equivalent:}\!</math>
::
+
| style="border-left:1px solid black" | &nbsp;
R9g. ConjUu (( {X} , {Y} ))$(u). :R7f
+
|}
</pre>
+
|-
 
+
|
<br>
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:40px"
<pre>
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
Rule 10
+
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R6a.}</math>
 
+
| width="60%" style="border-top:1px solid black" | <math>f ~=~ g</math>
If X, Y c U,
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R6a~:~D3a}</math>
 
+
|- style="height:20px"
then the following are equivalent:
+
| &nbsp;
 
+
| &nbsp;
R10a. X = Y. :D2a
+
| &nbsp;
::
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
R10b. u C X  <=> u C Y, for all u C U. :D2b
+
|- style="height:60px"
:R8a
+
| &nbsp;
::
+
| <math>\operatorname{R6b.}</math>
R10c. [u C X] = [u C Y]. :R8b
+
| <math>\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))</math>
::
+
| style="border-left:1px solid black; text-align:center" |
R10d. For all u C U,
+
<p><math>\operatorname{R6b~:~D3b}</math></p>
[u C X](u) = [u C Y](u). :R8c
+
<p><math>\operatorname{R6b~:~D6a}</math></p>
::
+
|- style="height:20px"
R10e. ConjUu ( [u C X](u)  = [u C Y](u) ). :R8d
+
| &nbsp;
::
+
| &nbsp;
R10f. ConjUu ( [u C X](u) <=> [u C Y](u) ). :R8e
+
| &nbsp;
::
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
R10g. ConjUu (( [u C X](u) , [u C Y](u) )). :R8f
+
|- style="height:40px"
::
+
| &nbsp;
R10h. ConjUu (( [u C X] , [u C Y] ))$(u). :R8g
+
| <math>\operatorname{R6c.}</math>
</pre>
+
| <math>\operatorname{Conj_x^X}~ (f(x) ~=~ g(x))</math>
 
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R6c~:~D6b}</math>
 +
|}
 +
|}
 +
 
 
<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%"
Rule 11
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
If X c U
+
|- style="height:40px; text-align:center"
 
+
| width="80%" | &nbsp;
then the following are equivalent:
+
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~7}</math>
 
+
|}
R11a. X = {u C U : S}. :R5a
+
|-
::
+
|
R11b. {X} = { {u C U : S} }. :R5e
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
::
+
|- style="height:40px"
R11c. {X} c UxB
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
+
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
: {X} = {<u, v> C UxB : v = [S](u)}. :R
+
| width="60%" style="border-top:1px solid black" | <math>p, q ~:~ X \to \underline\mathbb{B}</math>
::
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
R11d. {X} : U -> B
+
|- style="height:40px"
 
+
| &nbsp;
: {X}(u) = [S](u), for all u C U. :R
+
| <math>\text{then}\!</math>
::
+
| <math>\text{the following are equivalent:}\!</math>
R11e. {X} = [S]. :R
+
| style="border-left:1px solid black" | &nbsp;
 
+
|}
An application of Rule 11 involves the recognition of an antecedent condition as a case under the Rule, that is, as a condition that matches one of the sentences in the Rule's chain of equivalents, and it requires the relegation of the other expressions to the production of a result.  Thus, there is the choice of an initial expression that has to be checked on input for whether it fits the antecedent condition, and there is the choice of three types of output that are generated as a consequence, only one of which is generally needed at any given time.  More often than not, though, a rule is applied in only a few of its possible ways.  The usual antecedent and the usual consequents for Rule 11 can be distinguished in form and specialized in practice as follows:
+
|-
 
+
|
a. R11a marks the usual starting place for an application of the Rule, that is, the standard form of antecedent condition that is likely to lead to an invocation of the Rule.
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:40px"
b. R11b records the trivial consequence of applying the spiny braces to both sides of the initial equation.
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
 
+
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R7a.}</math>
c. R11c gives a version of the indicator function with {X} c UxB, called its "extensional form".
+
| width="60%" style="border-top:1px solid black" | <math>p ~=~ q</math>
 
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R7a~:~R6a}</math>
d. R11d gives a version of the indicator function with {X} : U->B, called its "functional form".
+
|- style="height:20px"
 
+
| &nbsp;
Applying Rule 9, Rule 8, and the Logical Rules to the special case where S <=> (X = Y), one obtains the following general fact.
+
| &nbsp;
</pre>
+
| &nbsp;
 
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
<br>
+
|- style="height:60px"
 
+
| &nbsp;
<pre>
+
| <math>\operatorname{R7b.}</math>
Fact 1
+
| <math>\overset{X}{\underset{x}{\forall}}~ (p(x) ~=~ q(x))</math>
 
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7b~:~R6b}</math>
If X,Y c U,
+
|- style="height:20px"
 
+
| &nbsp;
then the following are equivalent:
+
| &nbsp;
 
+
| &nbsp;
F1a. S <=> X = Y. :R9a
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
::
+
|- style="height:60px"
F1b. S <=> {X} = {Y}. :R9b
+
| &nbsp;
::
+
| <math>\operatorname{R7c.}</math>
F1c. S <=> {X}(u) = {Y}(u), for all u C U. :R9c
+
| <math>\operatorname{Conj_x^X}~ (p(x) ~=~ q(x))</math>
::
+
| style="border-left:1px solid black; text-align:center" |
F1d. S <=> ConjUu ( {X}(u) = {Y}(u) ). :R9d
+
<p><math>\operatorname{R7c~:~R6c}</math></p>
:R8a
+
<p><math>\operatorname{R7c~:~P1a}</math></p>
::
+
|- style="height:20px"
F1e. [S] = [ ConjUu ( {X}(u) = {Y}(u) ) ]. :R8b
+
| &nbsp;
:???
+
| &nbsp;
::
+
| &nbsp;
F1f. [S] = ConjUu [ {X}(u) = {Y}(u) ]. :???
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
::
+
|- style="height:40px"
F1g. [S] = ConjUu (( {X}(u) , {Y}(u) )). :$1a
+
| &nbsp;
::
+
| <math>\operatorname{R7d.}</math>
F1h. [S] = ConjUu (( {X} , {Y} ))$(u). :$1b
+
| <math>\operatorname{Conj_x^X}~ (p(x) ~\Leftrightarrow~ q(x))</math>
 
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7d~:~P1b}</math>
///
+
|- style="height:20px"
{u C U : (f, g)$(u)}
+
| &nbsp;
= {u C U : (f(u), g(u))}
+
| &nbsp;
= {u C
+
| &nbsp;
///
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
</pre>
+
|- style="height:60px"
 
+
| &nbsp;
===Derived Equivalence Relations===
+
| <math>\operatorname{R7e.}</math>
 
+
| <math>\operatorname{Conj_x^X}~ \underline{((}~ p(x) ~,~ q(x) ~\underline{))}</math>
<pre>
+
| style="border-left:1px solid black; text-align:center" |
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.
+
<p><math>\operatorname{R7e~:~P1c}</math></p>
 
+
<p><math>\operatorname{R7e~:~$1a}</math></p>
A classic way of showing that two sets are equal is to show that every element of the first belongs to the second and that every element of the second belongs to the first.  The problem with this strategy is that one can exhaust a considerable amount of time trying to prove that two sets are equal before it occurs to one to look for a counterexample, that is, an element of the first that does not belong to the second or an element of the second that does not belong to the first, in cases where that is precisely what one ought to be seeking.  It would be nice if there were a more balanced, impartial, neutral, or nonchalant way to go about this task, one that did not require such an undue commitment to either side, a technique that helps to pinpoint the counterexamples when they exist, and a method that keeps in mind the original relation of "proving that" and "showing that" to probing, testing, and seeing "whether".
+
|- style="height:20px"
 
+
| &nbsp;
A different way of seeing that two sets are equal, or of seeing whether two sets are equal, is based on the following observation:
+
| &nbsp;
 
+
| &nbsp;
Two sets are equal as sets
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
<=> the indicator functions of these sets are equal as functions
+
|- style="height:40px"
<=> the values of these functions are equal on all domain elements.
+
| &nbsp;
 
+
| <math>\operatorname{R7f.}</math>
It is important to notice the hidden quantifier, of a universal kind, that lurks in all three equivalent statements but is only revealed in the last.
+
| <math>\operatorname{Conj_x^X}~ \underline{((}~ p ~,~ q ~\underline{))}^\$ (x)</math>
 
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R7f~:~$1b}</math>
In making the next set of definitions and in using the corresponding terminology it is taken for granted that all of the references of signs are relative to a particular sign relation R c OxSxI that either remains to be specified or is already understood.  Further, I continue to assume that S = I, in which case this set is called the "syntactic domain" of R.
+
|}
 
+
|}
In the following definitions let R c OxSxI, let S = I, and let x, y C S.
 
 
 
Recall the definition of Con(R), the connotative component of R, in the following form:
 
 
 
Con(R) = RSI  =  {<s, i> C SxI : <o, s, i> C R for some o C O}.
 
 
 
Equivalent expressions for this concept are recorded in Definition 8.
 
 
 
Definition 8
 
 
 
If R c OxSxI,
 
 
 
then the following are identical subsets of SxI:
 
 
 
D8a. RSI
 
 
 
D8b. ConR
 
  
D8c. Con(R)
+
<br>
  
D8d. PrSI(R)
+
'''Editing Note.'''  Check earlier and later drafts to see where <math>\text{P1a, P1b, P1c}~</math> came from.  Are these just placeholders for the Value or Evaluation Rules?
  
D8e. {<s, i> C SxI : <o, s, i> C R for some o C O}
+
<br>
  
The dyadic relation RIS that constitutes the converse of the connotative relation RSI can be defined directly in the following fashion:
+
{| 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%"
 
+
|
Con(R)^  = RIS  = {<i, s> C IxS : <o, s, i> C R for some o C O}.
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:40px; text-align:center"
A few of the many different expressions for this concept are recorded in Definition 9.
+
| width="80%" | &nbsp;
 
+
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~8}</math>
Definition 9
+
|}
 
+
|-
If R c OxSxI,
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
then the following are identical subsets of IxS:
+
|- style="height:40px"
 
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
D9a. RIS
+
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
+
| width="60%" style="border-top:1px solid black" | <math>s, t ~\text{are sentences about things in}~ X</math>
D9b. RSI^
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
+
|- style="height:40px"
D9c. ConR^
+
| &nbsp;
 
+
| <math>\text{then}\!</math>
D9d. Con(R)^
+
| <math>\text{the following are equivalent:}\!</math>
 
+
| style="border-left:1px solid black" | &nbsp;
D9e. PrIS(R)
+
|}
 
+
|-
D9f. Conv(Con(R))
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
D9g. {<i, s> C IxS : <o, s, i> C R for some o C O}
+
|- style="height:40px"
 
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
Recall the definition of Den(R), the denotative component of R, in the following form:
+
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R8a.}</math>
Den(R)  =  ROS  =  {<o, s> C OxS : <o, s, i> C R for some i C I}.
+
| width="60%" style="border-top:1px solid black" | <math>s ~\Leftrightarrow~ t</math>
 
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" |
Equivalent expressions for this concept are recorded in Definition 10.
+
<math>\operatorname{R8a~:~D7a}</math>
 
+
|- style="height:20px"
Definition 10
+
| &nbsp;
 
+
| &nbsp;
If R c OxSxI,
+
| &nbsp;
 
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
then the following are identical subsets of OxS:
+
|- style="height:60px"
 
+
| &nbsp;
D10a. ROS
+
| <math>\operatorname{R8b.}</math>
 
+
| <math>\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright</math>
D10b. DenR
+
| style="border-left:1px solid black; text-align:center" |
 
+
<p><math>\operatorname{R8b~:~D7b}</math></p>
D10c. Den(R)
+
<p><math>\operatorname{R8b~:~R7a}</math></p>
 
+
|- style="height:20px"
D10d. PrOS(R)
+
| &nbsp;
 
+
| &nbsp;
D10e. {<o, s> C OxS : <o, s, i> C R for some i C I}
+
| &nbsp;
 
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
The dyadic relation RSO that constitutes the converse of the denotative relation ROS can be defined directly in the following fashion:
+
|- style="height:60px"
 
+
| &nbsp;
Den(R)= RSO  = {<s, o> C SxO : <o, s, i> C R for some i C I}.
+
| <math>\operatorname{R8c.}</math>
 
+
| <math>\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))</math>
A few of the many different expressions for this concept are recorded in Definition 11.
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8c~:~R7b}</math>
 
+
|- style="height:20px"
Definition 11
+
| &nbsp;
 
+
| &nbsp;
If R c OxSxI,
+
| &nbsp;
 
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
then the following are identical subsets of SxO:
+
|- style="height:40px"
 
+
| &nbsp;
D11a. RSO
+
| <math>\operatorname{R8d.}</math>
 
+
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))</math>
D11b. ROS^
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8d~:~R7c}</math>
 
+
|- style="height:20px"
D11c. DenR^
+
| &nbsp;
 
+
| &nbsp;
D11d. Den(R)^
+
| &nbsp;
 
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
D11e. PrSO(R)
+
|- style="height:40px"
 
+
| &nbsp;
D11f. Conv(Den(R))
+
| <math>\operatorname{R8e.}</math>
 
+
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft t \downharpoonright (x))</math>
D11g. {<s, o> C SxO : <o, s, i> C R for some i C I}
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8e~:~R7d}</math>
 
+
|- style="height:20px"
The "denotation of x in R", written "Den(R, x)", is defined as follows:
+
| &nbsp;
Den(R, x)  = {o C O : <o, x> C Den(R)}.
+
| &nbsp;
 
+
| &nbsp;
In other words:
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
+
|- style="height:60px"
Den(R, x) = {o C O : <o, x, i> C R for some i C I}.
+
| &nbsp;
Equivalent expressions for this concept are recorded in Definition 12.
+
| <math>\operatorname{R8f.}</math>
 
+
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright (x) ~,~ \downharpoonleft t \downharpoonright (x) ~\underline{))}</math>
Definition 12
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8f~:~R7e}</math>
 
+
|- style="height:20px"
If R c OxSxI,
+
| &nbsp;
 
+
| &nbsp;
and x C S,
+
| &nbsp;
 
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
then the following are identical subsets of O:
+
|- style="height:40px"
 
+
| &nbsp;
D12a. ROS.x
+
| <math>\operatorname{R8g.}</math>
 
+
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright ~\underline{))}^\$ (x)</math>
D12b. DenR.x
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8g~:~R7f}</math>
 
+
|}
D12c. DenR|x
+
|}
 
 
D12d. DenR(, x)
 
  
D12e. Den(R, x)
+
<br>
  
D12f. Den(R).x
+
For instance, the observation that expresses the equality of sets in terms of their indicator functions can be formalized according to the pattern in Rule&nbsp;9, namely, at lines R9a, R9b, and R9c, and these components of Rule&nbsp;9 can be cited in future uses by their indices in this list. Using Rule&nbsp;7, annotated as R7, to adduce a few properties of indicator functions to the account, it is possible to extend Rule&nbsp;9 by another few steps, referenced as R9d, R9e, R9f, and R9g.
  
D12g. {o C O : <o, x> C Den(R)}
+
<br>
  
D12h. {o C O : <o, x, i> C R for some i C I}
+
{| 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%"
 
+
|
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 jumpimg to the conclusions that are implied by these latter terms.
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
+
|- style="height:40px; text-align:center"
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.
+
| width="80%" | &nbsp;
 
+
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~9}</math>
For each sign relation R, this yields a binary relation Der(R) c SxI that is defined as follows:
+
|}
 
+
|-
Der(R)  = DerR  = {<x, y> C SxI : Den(R, x) = Den(R, y)}.
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
These definitions and notations are recorded in the following display.
+
|- style="height:40px"
 
+
| width="2%"  style="border-top:1px solid black" | &nbsp;
Definition 13
+
| width="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 
+
| width="60%" style="border-top:1px solid black" | <math>P, Q ~\subseteq~ X</math>
If R c OxSxI,
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
 
+
|- style="height:40px"
then the following are identical subsets of SxI:
+
| &nbsp;
 
+
| <math>\text{then}\!</math>
D13a. DerR
+
| <math>\text{the following are equivalent:}\!</math>
 
+
| style="border-left:1px solid black" | &nbsp;
D13b. Der(R)
+
|}
 
+
|-
D13c. {<x,y> C SxI : DenR|x = DenR|y}
+
|
 
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
D13d. {<x,y> C SxI : Den(R, x) = Den(R, y)}
+
|- style="height:40px"
 
+
| width="2%style="border-top:1px solid black" | &nbsp;
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.
+
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R9a.}</math>
 
+
| width="60%" style="border-top:1px solid black" | <math>P ~=~ Q</math>
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.
+
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R9a~:~R5a}</math>
 
+
|- style="height:20px"
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.
+
| &nbsp;
 
+
| &nbsp;
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.
+
| &nbsp;
 
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
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.
+
|- style="height:60px"
 
+
| &nbsp;
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?
+
| <math>\operatorname{R9b.}</math>
 
+
| <math>\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright</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.
+
| style="border-left:1px solid black; text-align:center" |
 
+
<p><math>\operatorname{R9b~:~R5e}</math></p>
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".
+
<p><math>\operatorname{R9b~:~R7a}</math></p>
 
+
|- style="height:20px"
The uses of the equal sign for denoting equations or equivalences are recalled and extended in the following ways:
+
| &nbsp;
 
+
| &nbsp;
1. If E is an arbitrary equivalence relation,
+
| &nbsp;
then the equation "x =E y" means that <x, y> C E.
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
+
|- style="height:60px"
2. If R is a sign relation such that RSI is a SER on S = I,
+
| &nbsp;
then the semiotic equation "x =R y" means that <x, y> C RSI.
+
| <math>\operatorname{R9c.}</math>
 
+
| <math>\overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
3. If R is a sign relation such that F is its DER on S = I,
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9c~:~R7b}</math>
then the denotative equation "x =R y" means that <x, y> C F,
+
|- style="height:20px"
in other words, that Den(R, x) = Den(R, y).
+
| &nbsp;
 
+
| &nbsp;
The uses of square brackets for denoting equivalence classes are recalled and extended in the following ways:
+
| &nbsp;
 
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
1. If E is an arbitrary equivalence relation,
+
|- style="height:40px"
then "[x]E" denotes the equivalence class of x under E.
+
| &nbsp;
 
+
| <math>\operatorname{R9d.}</math>
2. If R is a sign relation such that Con(R) is a SER on S = I,
+
| <math>\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
then "[x]R" denotes the SEC of x under Con(R).
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9d~:~R7c}</math>
 
+
|- style="height:20px"
3. If R is a sign relation such that Der(R) is a DER on S = I,
+
| &nbsp;
then "[x]R" denotes the DEC of x under Der(R).
+
| &nbsp;
 
+
| &nbsp;
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.
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 
+
|- style="height:40px"
Fact 2.1
+
| &nbsp;
 
+
| <math>\operatorname{R9e.}</math>
If R c OxSxI,
+
| <math>\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x))</math>
 
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9e~:~R7d}</math>
then the following are identical subsets of SxI:
+
|- style="height:20px"
 
+
| &nbsp;
F2.1a. DerR :D13a
+
| &nbsp;
::
+
| &nbsp;
F2.1b. Der(R) :D13b
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
::
+
|- style="height:60px"
F2.1c. {<x, y> C SxI :
+
| &nbsp;
Den(R, x) = Den(R, y)
+
| <math>\operatorname{R9f.}</math>
} :D13c
+
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}</math>
:R9a
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9f~:~R7e}</math>
::
+
|- style="height:20px"
F2.1d. {<x, y> C SxI :
+
| &nbsp;
{Den(R, x)} = {Den(R, y)}
+
| &nbsp;
} :R9b
+
| &nbsp;
::
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
F2.1e. {<x, y> C SxI :
+
|- style="height:40px"
for all o C O
+
| &nbsp;
{Den(R, x)}(o) = {Den(R, y)}(o)
+
| <math>\operatorname{R9g.}</math>
} :R9c
+
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\$ (x)</math>
::
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9g~:~R7f}</math>
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
 
 
 
 
 
Fact 2.2
 
 
 
If R c OxSxI,
 
 
 
then the following are equivalent:
 
 
 
F2.2a. DerR = {<x, y> C SxI :
 
Conj(o C O)
 
{Den(R, x)}(o) =
 
{Den(R, y)}(o)
 
} :R11a
 
::
 
F2.2b. {DerR} = { {<x, y> C SxI :
 
Conj(o C O)
 
{Den(R, x)}(o) =
 
{Den(R, y)}(o)
 
}
 
} :R11b
 
::
 
F2.2c. {DerR} c SxIxB
 
:
 
{DerR} = {<x, y, v> C SxIxB :
 
v =
 
[ Conj(o C O)
 
{Den(R, x)}(o) =
 
{Den(R, y)}(o)
 
]
 
} :R11c
 
::
 
F2.2d. {DerR} = {<x, y, v> C SxIxB :
 
v =
 
Conj(o C O)
 
[ {Den(R, x)}(o) =
 
{Den(R, y)}(o)
 
]
 
} :Log
 
 
 
F2.2e. {DerR} = {<x, y, v> C SxIxB :
 
v =
 
Conj(o C O)
 
(( {Den(R, x)}(o),
 
{Den(R, y)}(o)
 
))
 
} :Log
 
 
 
F2.2f. {DerR} = {<x, y, v> C SxIxB :
 
v =
 
Conj(o C O)
 
(( {Den(R, x)},
 
{Den(R, y)}
 
))$(o)
 
} :$
 
 
 
 
 
Fact 2.3
 
 
 
If R c OxSxI,
 
  
then the following are equivalent:
+
<br>
  
F2.3a. DerR = {<x, y> C SxI :
+
{| 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%"
Conj(o C O)
+
|
{Den(R, x)}(o) =
+
{| align="center" cellpadding="0" cellspacing="0" width="100%"
{Den(R, y)}(o)
+
|- style="height:40px; text-align:center"
} :R11a
+
| width="80%" | &nbsp;
::
+
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~10}</math>
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>
 
 
 
{| 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 1}\!</math>
 
| width="2%"  | &nbsp;
 
 
|}
 
|}
 
|-
 
|-
 
|
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:48px"
+
|- style="height:40px"
 
| 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="18%" style="border-top:1px solid black" | <math>\text{If}\!</math>
| width="80%" style="border-top:1px solid black" |
+
| width="60%" style="border-top:1px solid black" | <math>P, Q ~\subseteq~ X</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:40px"
 
| &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 equivalent:}\!</math>
|- style="height:48px"
+
| style="border-left:1px solid black" | &nbsp;
 +
|}
 +
|-
 +
|
 +
{| 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{R10a.}</math>
 +
| width="60%" style="border-top:1px solid black" | <math>P ~=~ Q</math>
 +
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R10a~:~D2a}</math>
 +
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
| <math>\text{such that:}\!</math>
 
 
| &nbsp;
 
| &nbsp;
|- style="height:48px"
 
 
| &nbsp;
 
| &nbsp;
| <math>\text{L1a.}\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\downharpoonleft s \downharpoonright ~=~ p</math>
+
|- style="height:60px"
|- style="height:48px"
+
| &nbsp;
 +
| <math>\operatorname{R10b.}</math>
 +
| <math>\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<p><math>\operatorname{R10b~:~D2b}</math></p>
 +
<p><math>\operatorname{R10b~:~R8a}</math></p>
 +
|- 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{L1b}_{00}.\!</math>
 
| width="20%" style="border-top:1px solid black" |
 
<math>\downharpoonleft \operatorname{false} \downharpoonright</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{L1b}_{01}.\!</math>
 
| <math>\downharpoonleft \operatorname{not}~ 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}_{10}.\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\downharpoonleft s \downharpoonright</math>
+
|- style="height:40px"
| <math>=\!</math>
+
| &nbsp;
| <math>\downharpoonleft s \downharpoonright</math>
+
| <math>\operatorname{R10c.}</math>
| <math>=\!</math>
+
| <math>\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright</math>
| <math>p ~:~ X \to \underline\mathbb{B}</math>
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10c~:~R8b}</math>
|- style="height:52px"
+
|- style="height:20px"
 
| &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>
 
| <math>p ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:48px"
 
 
| &nbsp;
 
| &nbsp;
| <math>\text{such that:}\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:40px"
 
| &nbsp;
 
| &nbsp;
|- style="height:48px"
+
| <math>\operatorname{R10d.}</math>
 +
| <math>\overset{X}{\underset{x}{\forall}}~ \downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x)</math>
 +
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10d~:~R8c}</math>
 +
|- style="height:20px"
 
| &nbsp;
 
| &nbsp;
| <math>\text{G1a.}\!</math>
 
| <math>\upharpoonleft Q \upharpoonright ~=~ p</math>
 
|- style="height:48px"
 
 
| &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>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\upharpoonleft {}^{_\sim} Q \upharpoonright</math>
+
|- style="height:40px"
| <math>=\!</math>
+
| &nbsp;
| <math>(\upharpoonleft Q \upharpoonright)</math>
+
| <math>\operatorname{R10e.}</math>
| <math>=\!</math>
+
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x))</math>
| <math>(p) ~:~ X \to \underline\mathbb{B}</math>
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10e~:~R8d}</math>
|- style="height:52px"
+
|- style="height:20px"
 +
| &nbsp;
 +
| &nbsp;
 
| &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:40px"
| <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}_{11}.\!</math>
+
| <math>\operatorname{R10f.}</math>
| <math>\upharpoonleft X \upharpoonright</math>
+
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft x \in Q \downharpoonright (x))</math>
| <math>=\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10f~:~R8e}</math>
| <math>((~))</math>
+
|- style="height:20px"
| <math>=\!</math>
+
| &nbsp;
| <math>\underline{1} ~:~ X \to \underline\mathbb{B}</math>
+
| &nbsp;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{R10g.}</math>
 +
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft x \in P \downharpoonright (x) ~,~ \downharpoonleft x \in Q \downharpoonright (x) ~\underline{))}</math>
 +
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10g~:~R8f}</math>
 +
|- style="height:20px"
 +
| &nbsp;
 +
| &nbsp;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{R10h.}</math>
 +
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft x \in P \downharpoonright ~,~ \downharpoonleft x \in Q \downharpoonright ~\underline{))}^\$ (x)</math>
 +
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10h~:~R8g}</math>
 
|}
 
|}
 
|}
 
|}
 
<br>
 
 
===Logical Translation Rule 2===
 
  
 
<br>
 
<br>
Line 1,537: Line 1,286:
 
|
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:48px; text-align:right"
+
|- style="height:40px; text-align:center"
| width="98%" | <math>\text{Logical Translation Rule 2}\!</math>
+
| width="80%" | &nbsp;
| width="2%"  | &nbsp;
+
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~11}</math>
 
|}
 
|}
 
|-
 
|-
 
|
 
|
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 
{| align="center" cellpadding="0" cellspacing="0" width="100%"
|- style="height:48px"
+
|- style="height:40px"
 
| 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" |
+
| width="60%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</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:40px"
| &nbsp;
 
| <math>\text{and}\!</math>
 
| <math>p, q ~\text{are propositions} ~:~ X \to \underline\mathbb{B}</math>
 
|- style="height:48px"
 
| &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;
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{then}\!</math>
| <math>\text{the following equations hold:}\!</math>
+
| <math>\text{the following are equivalent:}\!</math>
 +
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|}
 
|-
 
|-
 
|
 
|
{| 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:40px"
 
| 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="18%" style="border-top:1px solid black" | <math>\operatorname{R11a.}</math>
| width="32%" style="border-top:1px solid black" |
+
| width="60%" style="border-top:1px solid black" | <math>Q ~=~ \{ x \in X ~:~ s \}</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{R11a~:~R5a}</math>
| width="4%" style="border-top:1px solid black" | <math>=\!</math>
+
|- style="height:20px"
| width="28%" style="border-top:1px solid black" | <math>(~)</math>
+
| &nbsp;
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
+
| &nbsp;
| width="16%" style="border-top:1px solid black" | <math>(~)</math>
+
| &nbsp;
|- style="height:52px"
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:40px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{1}.\!</math>
+
| <math>\operatorname{R11b.}</math>
| <math>\downharpoonleft \operatorname{neither}~ s ~\operatorname{nor}~ t \downharpoonright</math>
+
| <math>\upharpoonleft Q \upharpoonright ~=~ \upharpoonleft \{ x \in X ~:~ s \} \upharpoonright</math>
| <math>=\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11b~:~R5e}</math>
| <math>(\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright)</math>
+
|- style="height:20px"
| <math>=\!</math>
 
| <math>(p)(q)\!</math>
 
|- style="height:52px"
 
 
| &nbsp;
 
| &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;
 
| &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;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{4}.\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\downharpoonleft s ~\operatorname{and~not}~ t \downharpoonright</math>
+
|- style="height:60px"
| <math>=\!</math>
+
| &nbsp;
| <math>\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright)</math>
+
| <math>\operatorname{R11c.}</math>
| <math>=\!</math>
+
|
| <math>p (q)\!</math>
+
<math>\begin{array}{lcl}
|- style="height:52px"
+
\upharpoonleft Q \upharpoonright
 +
& \subseteq &
 +
X \times \underline\mathbb{B}
 +
\\
 +
\upharpoonleft Q \upharpoonright
 +
& = &
 +
\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y  = \, \downharpoonleft s \downharpoonright (x) \}
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<p><math>\operatorname{R11c~:~\_\_?\_\_}</math></p>
 +
<p><math>\operatorname{R11c~:~\_\_?\_\_}</math></p>
 +
|- style="height:20px"
 
| &nbsp;
 
| &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;
 
| &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;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{7}.\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\downharpoonleft \operatorname{not~both}~ s ~\operatorname{and}~ t \downharpoonright</math>
+
|- style="height:60px"
| <math>=\!</math>
+
| &nbsp;
| <math>(\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright)</math>
+
| <math>\operatorname{R11d.}</math>
| <math>=\!</math>
+
|
| <math>(p q)\!</math>
+
<math>\begin{array}{ccccl}
|- style="height:52px"
+
\upharpoonleft Q \upharpoonright & : & X & \to    & \underline\mathbb{B}
 +
\\
 +
\upharpoonleft Q \upharpoonright & : & x & \mapsto & \downharpoonleft s \downharpoonright (x)
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<p><math>\operatorname{R11d~:~\_\_?\_\_}</math></p>
 +
<p><math>\operatorname{R11d~:~\_\_?\_\_}</math></p>
 +
|- style="height:20px"
 
| &nbsp;
 
| &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;
 
| &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;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{10}.\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\downharpoonleft t \downharpoonright</math>
+
|- style="height:60px"
| <math>=\!</math>
+
| &nbsp;
| <math>\downharpoonleft t \downharpoonright</math>
+
| <math>\operatorname{R11e.}</math>
| <math>=\!</math>
+
| <math>\overset{X}{\underset{x}{\forall}}~ \upharpoonleft Q \upharpoonright (x) ~=~ \downharpoonleft s \downharpoonright (x)</math>
| <math>q\!</math>
+
| style="border-left:1px solid black; text-align:center" |
|- style="height:52px"
+
<p><math>\operatorname{R11e~:~\_\_?\_\_}</math></p>
 +
<p><math>\operatorname{R11e~:~\_\_?\_\_}</math></p>
 +
|- style="height:20px"
 
| &nbsp;
 
| &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;
 
| &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;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{13}.\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\downharpoonleft s ~\operatorname{is~implied~by}~ t \downharpoonright</math>
+
|- style="height:40px"
| <math>=\!</math>
 
| <math>((\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright)</math>
 
| <math>=\!</math>
 
| <math>((p) q)\!</math>
 
|- style="height:52px"
 
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{L2b}_{14}.\!</math>
+
| <math>\operatorname{R11f.}</math>
| <math>\downharpoonleft s ~\operatorname{or}~ t \downharpoonright</math>
+
| <math>\upharpoonleft Q \upharpoonright ~=~ \downharpoonleft s \downharpoonright</math>
| <math>=\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11f~:~\_\_?\_\_}</math>
| <math>((\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright))</math>
 
| <math>=\!</math>
 
| <math>((p)(q))\!</math>
 
|- style="height:52px"
 
| &nbsp;
 
| align="left" | <math>\text{L2b}_{15}.\!</math>
 
| <math>\downharpoonleft \operatorname{true} \downharpoonright</math>
 
| <math>=\!</math>
 
| <math>((~))</math>
 
| <math>=\!</math>
 
| <math>((~))</math>
 
 
|}
 
|}
 
|}
 
|}
Line 1,703: Line 1,387:
 
<br>
 
<br>
  
===Geometric Translation Rule 2===
+
An application of Rule&nbsp;11 involves the recognition of an antecedent condition as a case under the Rule, that is, as a condition that matches one of the sentences in the Rule's chain of equivalents, and it requires the relegation of the other expressions to the production of a result.  Thus, there is the choice of an initial expression that has to be checked on input for whether it fits the antecedent condition, and there is the choice of three types of output that are generated as a consequence, only one of which is generally needed at any given time.  More often than not, though, a rule is applied in only a few of its possible ways.  The usual antecedent and the usual consequents for Rule&nbsp;11 can be distinguished in form and specialized in practice as follows:
 +
 
 +
{| align="center" cellpadding="8" width="90%"
 +
| <math>\operatorname{R11a}</math> marks the usual starting place for an application of the Rule, that is, the standard form of antecedent condition that is likely to lead to an invocation of the Rule.
 +
|-
 +
| <math>\operatorname{R11b}</math> records the trivial consequence of applying the ''up-spar operator'' <math>\upharpoonleft \cdots \upharpoonright</math> to both sides of the initial equation.
 +
|-
 +
| <math>\operatorname{R11c}</math> gives a version of the indicator function with <math>\upharpoonleft X \upharpoonright ~\subseteq~ X \times \underline\mathbb{B},</math> called the ''extensional'' or ''relational'' form of the indicator function.
 +
|-
 +
| <math>\operatorname{R11d}</math> gives a version of the indicator function with <math>\upharpoonleft X \upharpoonright ~:~ X \to \underline\mathbb{B},</math> called its ''functional form''.
 +
|}
 +
 
 +
Applying Rule&nbsp;9, Rule&nbsp;8, and the Logical Rules to the special case where <math>s \Leftrightarrow (X = Y),</math> one obtains the following general Fact:
  
 
<br>
 
<br>
Line 1,710: Line 1,406:
 
|
 
|
 
{| 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{Geometric Translation Rule 2}\!</math>
+
| style="width:80%" | &nbsp;
| width="2%"  | &nbsp;
+
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~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;
+
| style="border-top:1px solid black; width:2%" | &nbsp;
| width="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
+
| style="border-top:1px solid black; width:18%" | <math>\text{If}\!</math>
| width="84%" style="border-top:1px solid black" | <math>P, Q \subseteq X</math>
+
| style="border-top:1px solid black; width:60%" | <math>P, Q ~\subseteq~ X</math>
|- style="height:48px"
+
| style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
| &nbsp;
+
|- style="height:50px"
| <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;
 
| &nbsp;
 
| <math>\text{then}\!</math>
 
| <math>\text{then}\!</math>
| <math>\text{the following equations hold:}\!</math>
+
| <math>\text{the following are equivalent:}\!</math>
 +
| style="border-left:1px solid black" | &nbsp;
 
|}
 
|}
 
|-
 
|-
 
|
 
|
{| 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;
+
| style="width:2%; border-top:1px solid black" | &nbsp;
| width="14%" style="border-top:1px solid black" align="left" | <math>\text{G2b}_{0}.\!</math>
+
| style="width:14%; border-top:1px solid black" | <math>\operatorname{F1a.}</math>
| width="32%" style="border-top:1px solid black" |
+
| style="width:64%; border-top:1px solid black" | <math>s \quad \Leftrightarrow \quad (P ~=~ Q)</math>
<math>\upharpoonleft \varnothing \upharpoonright</math>
+
| style="width:20%; border-top:1px solid black; border-left:1px solid black; text-align:center" |
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
+
<math>\operatorname{F1a~:~R9a}</math>
| width="28%" style="border-top:1px solid black" | <math>(~)</math>
+
|- style="height:20px"
| width="4%"  style="border-top:1px solid black" | <math>=\!</math>
+
| &nbsp;
| width="16%" style="border-top:1px solid black" | <math>(~)</math>
+
| &nbsp;
|- style="height:52px"
+
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| <math>\operatorname{F1b.}</math>
 +
| <math>s \quad \Leftrightarrow \quad (\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright)</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F1b~:~R9b}</math>
 +
|- style="height:20px"
 
| &nbsp;
 
| &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;
 
| &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;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{3}.\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\upharpoonleft \overline{P} \upharpoonright</math>
+
|- style="height:60px"
| <math>=\!</math>
+
| &nbsp;
| <math>(\upharpoonleft P \upharpoonright)</math>
+
| <math>\operatorname{F1c.}</math>
| <math>=\!</math>
+
| <math>s \quad \Leftrightarrow \quad \overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
| <math>(p)\!</math>
+
| style="border-left:1px solid black; text-align:center" |
|- style="height:52px"
+
<math>\operatorname{F1c~:~R9c}</math>
 +
|- style="height:20px"
 
| &nbsp;
 
| &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;
 
| &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;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{6}.\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\upharpoonleft P ~+~ Q \upharpoonright</math>
+
|- style="height:60px"
| <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>
+
| <math>\operatorname{F1d.}</math>
| <math>\upharpoonleft \overline{P ~\cap~ Q} \upharpoonright</math>
+
| <math>s \quad \Leftrightarrow \quad \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
| <math>=\!</math>
+
| style="border-left:1px solid black; text-align:center" |
| <math>(\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright)</math>
+
<p><math>\operatorname{F1d~:~R9d}</math></p>
| <math>=\!</math>
+
<p><math>\operatorname{F1d~:~R8a}</math></p>
| <math>(p q)\!</math>
+
|- style="height:20px"
|- style="height:52px"
 
 
| &nbsp;
 
| &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;
 
| &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;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{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>
+
| <math>\operatorname{F1e.}</math>
| <math>=\!</math>
+
| <math>\downharpoonleft s \downharpoonright \quad = \quad \downharpoonleft \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright</math>
| <math>q\!</math>
+
| style="border-left:1px solid black; text-align:center" |
|- style="height:52px"
+
<p><math>\operatorname{F1e~:~R8b}</math></p>
 +
<p><math>\operatorname{F1e~:~\_\_?\_\_}</math></p>
 +
|- style="height:20px"
 
| &nbsp;
 
| &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;
 
| &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;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{13}.\!</math>
+
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
| <math>\upharpoonleft \overline{\overline{P} ~\cap~ Q} \upharpoonright</math>
+
|- style="height:60px"
| <math>=\!</math>
+
| &nbsp;
| <math>((\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright)</math>
+
| <math>\operatorname{F1f.}</math>
| <math>=\!</math>
+
| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \downharpoonleft (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright</math>
| <math>((p) q)\!</math>
+
| style="border-left:1px solid black; text-align:center" |
|- style="height:52px"
+
<p><math>\operatorname{F1f~:~\_\_?\_\_}</math></p>
 +
<p><math>\operatorname{F1f~:~\_\_?\_\_}</math></p>
 +
|- style="height:20px"
 +
| &nbsp;
 +
| &nbsp;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:60px"
 +
| &nbsp;
 +
| <math>\operatorname{F1g.}</math>
 +
| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<p><math>\operatorname{F1g~:~\_\_?\_\_}</math></p>
 +
<p><math>\operatorname{F1g~:~\_\_?\_\_}</math></p>
 +
|- style="height:20px"
 +
| &nbsp;
 +
| &nbsp;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:40px"
 
| &nbsp;
 
| &nbsp;
| align="left" | <math>\text{G2b}_{14}.\!</math>
+
| <math>\operatorname{F1h.}</math>
 +
| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\$ (x)</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<math>\operatorname{F1h~:~~\_\_?\_\_}</math>
 +
|}
 +
|}
 +
 
 +
<br>
 +
 
 +
=====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.
 +
 
 +
A classic way of showing that two sets are equal is to show that every element of the first belongs to the second and that every element of the second belongs to the first.  The problem with this strategy is that one can exhaust a considerable amount of time trying to prove that two sets are equal before it occurs to one to look for a counterexample, that is, an element of the first that does not belong to the second or an element of the second that does not belong to the first, in cases where that is precisely what one ought to be seeking.  It would be nice if there were a more balanced, impartial, or neutral way to go about this task, one that did not require such an undue commitment to either side, a technique that helps to pinpoint the counterexamples when they exist, and a method that keeps in mind the original relation of ''proving that'' and ''showing that'' to probing, testing, and seeing ''whether''.
 +
 
 +
A different way of seeing that two sets are equal, or of seeing whether two sets are equal, is based on the following observation:
 +
 
 +
{| align="center" cellpadding="8" style="text-align:center" width="90%"
 +
| Two sets are equal as sets
 +
|-
 +
| <math>\iff</math>
 +
|-
 +
| The indicator functions of the two sets are equal as functions
 +
|-
 +
| <math>\iff</math>
 +
|-
 +
| The values of the two indicator functions are equal to each other on all domain elements.
 +
|}
 +
 
 +
It is important to notice the hidden quantifier, of a universal kind, that lurks in all three equivalent statements but is only revealed in the last.
 +
 
 +
In making the next set of definitions and in using the corresponding terminology it is taken for granted that all of the references of signs are relative to a particular sign relation <math>L \subseteq O \times S \times I</math> that either remains to be specified or is already understood.  Further, I continue to assume that <math>S = I,\!</math> in which case this set is called the ''syntactic domain'' of <math>L.\!</math>
 +
 
 +
In the following definitions, let <math>L \subseteq O \times S \times I,</math> let <math>S = I,\!</math> and let <math>x, y \in S.\!</math>
 +
 
 +
Recall the definition of <math>\operatorname{Con} (L),</math> the connotative component of a sign relation <math>L,\!</math> in the following form:
 +
 
 +
{| align="center" cellpadding="8" width="90%"
 +
| <math>\operatorname{Con} (L) ~=~ L_{SI} ~=~ \{ (s, i) \in S \times I ~:~ (o, s, i) \in L ~\text{for some}~ o \in O \}.</math>
 +
|}
 +
 
 +
Equivalent expressions for this concept are recorded in Definition&nbsp;8.
 +
 
 +
<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~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>
 +
|}
 +
|}
 +
 
 +
<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>
 +
|}
 +
 
 +
A few of the many different expressions for this concept are recorded in Definition&nbsp;9.
 +
 
 +
<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~9}</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}~ I \times S \, :</math>
 +
|}
 +
|-
 +
|
 +
{| 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>
 +
 
 +
Recall the definition of <math>\operatorname{Den} (L),</math> the denotative component of <math>L,\!</math> in the following form:
 +
 
 +
{| align="center" cellpadding="8" width="90%"
 +
| <math>\operatorname{Den} (L) ~=~ L_{OS} ~=~ \{ (o, s) \in O \times S ~:~ (o, s, i) \in L ~\text{for some}~ i \in I \}.</math>
 +
|}
 +
 
 +
Equivalent expressions for this concept are recorded in Definition&nbsp;10.
 +
 
 +
<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~10}</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}~ 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>
 +
 
 +
The dyadic relation <math>L_{SO}\!</math> that is the converse of the denotative relation <math>L_{OS}\!</math> can be defined directly in the following fashion:
 +
 
 +
{| align="center" cellpadding="8" width="90%"
 +
| <math>\overset{\smile}{\operatorname{Den}(L)} ~=~ L_{SO} ~=~ \{ (s, o) \in S \times O ~:~ (o, s, i) \in L ~\text{for some}~ i \in I \}.</math>
 +
|}
 +
 
 +
A few of the many different expressions for this concept are recorded in Definition&nbsp;11.
 +
 
 +
<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~11}</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 O \, :</math>
 +
|}
 +
|-
 +
|
 +
{| 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{D11a.}</math>
 +
| width="80%" style="border-top:1px solid black" | <math>L_{SO}\!</math>
 +
|- style="height:50px"
 +
| &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>
 +
|}
 +
|}
 +
 
 +
<br>
 +
 
 +
The ''denotation of <math>x\!</math> in <math>L,\!</math>'' written <math>\operatorname{Den}(L, x),</math> is defined as follows:
 +
 
 +
{| align="center" cellpadding="8" width="90%"
 +
| <math>\operatorname{Den}(L, x) ~=~ \{ o \in O ~:~ (o, x) \in \operatorname{Den}(L) \}.</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>
 +
 
 +
{| 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~12}</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{and}\!</math>
 +
| <math>x ~\in~ S</math>
 +
|- style="height:40px"
 +
| &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>
 +
|}
 +
|}
 +
 
 +
<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.
 +
 
 +
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.
 +
 
 +
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:
 +
 
 +
{| 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>
 +
|}
 +
 
 +
These definitions and notations are recorded in the following display.
 +
 
 +
<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~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>
 +
|}
 +
|}
 +
 
 +
<br>
 +
 
 +
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.
 +
 
 +
<ol style="list-style-type:decimal">
 +
 
 +
<li>
 +
<p>'''Reflexive property.'''</p>
 +
 
 +
<p>Is it true that <math>x ~\overset{L}{=}~ x</math> for every <math>x \in S = I</math>?</p>
 +
 
 +
<p> By definition, <math>x ~\overset{L}{=}~ x</math> if and only if <math>\operatorname{Den}(L, x) = \operatorname{Den}(L, x).</math></p>
 +
 
 +
<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>
 +
 
 +
<li>
 +
<p>'''Symmetric property.'''</p>
 +
 
 +
<p>Does <math>x ~\overset{L}{=}~ y</math> imply <math>y ~\overset{L}{=}~ x</math> for all <math>x, y \in S</math>?</p>
 +
 
 +
<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>
 +
 
 +
<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>
 +
 
 +
<li>
 +
<p>'''Transitive property.'''</p>
 +
 
 +
<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>
 +
 
 +
<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>
 +
 
 +
<p>Yes, once again, under the stated conditions.</p></li>
 +
 
 +
</ol>
 +
 
 +
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.
 +
 
 +
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?
 +
 
 +
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.
 +
 
 +
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>
 +
 
 +
The uses of the equal sign for denoting equations or equivalences are recalled and extended in the following ways:
 +
 
 +
# 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>
 +
# 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>
 +
# 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>
 +
 
 +
The use of square brackets for denoting equivalence classes is recalled and extended in the following ways:
 +
 
 +
# 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>
 +
 
 +
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.
 +
 
 +
<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.1}</math>
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:50px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="10%" style="border-top:1px solid black" | <math>\text{If}\!</math>
 +
| width="68%" 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;
 +
| <math>\text{then}\!</math>
 +
| <math>\text{the following are identical subsets of}~ S \times I :</math>
 +
| style="border-left:1px solid black" | &nbsp;
 +
|}
 +
|-
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" width="100%"
 +
|- style="height:60px"
 +
| width="2%"  style="border-top:1px solid black" | &nbsp;
 +
| width="10%" style="border-top:1px solid black" | <math>\operatorname{F2.1a.}</math>
 +
| width="68%" style="border-top:1px solid black" | <math>\operatorname{Der}^L</math>
 +
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{F2.1a~:~D13a}</math>
 +
|- style="height:20px"
 +
| &nbsp;
 +
| &nbsp;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:40px"
 +
| &nbsp;
 +
| valign="top" | <math>\operatorname{F2.1b.}</math>
 +
| valign="top" | <math>\operatorname{Der}(L)</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<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;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:60px"
 +
| &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;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:60px"
 +
| &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;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:60px"
 +
| &nbsp;
 +
| valign="top" | <math>\operatorname{F2.1f.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ll}
 +
\{ & (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;
 +
| &nbsp;
 +
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
 +
|- style="height:60px"
 +
| &nbsp;
 +
| valign="top" | <math>\operatorname{F2.1h.}</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 ~,~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright ~\underline{))}^\$ (o) \\
 +
\} & \\
 +
\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>
 +
 
 +
{| 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.2}</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;
 +
| <math>\text{then}\!</math>
 +
| <math>\text{the following are equivalent:}\!</math>
 +
| style="border-left:1px solid black" | &nbsp;
 +
|}
 +
|-
 +
|
 +
{| 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;
 +
| valign="top" | <math>\operatorname{F2.2a.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{cccl}
 +
\operatorname{Der}^L
 +
& = & \{ & (x, y) \in S \times I ~: \\
 +
&  &    & \begin{array}{ccl}
 +
          \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;
 +
| valign="top" | <math>\operatorname{F2.2b.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ccccl}
 +
\upharpoonleft \operatorname{Der}^L \upharpoonright
 +
& = & \upharpoonleft  & \{ & (x, y) \in S \times I ~: \\
 +
&  &                &    & \begin{array}{ccl}
 +
                            \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;
 +
| valign="top" | <math>\operatorname{F2.2c.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{cccl}
 +
\upharpoonleft \operatorname{Der}^L \upharpoonright
 +
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
 +
&  &    & \begin{array}{cccl}
 +
          \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;
 +
| valign="top" | <math>\operatorname{F2.2d.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{cccl}
 +
\upharpoonleft \operatorname{Der}^L \upharpoonright
 +
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
 +
&  &    & \begin{array}{cccl}
 +
          \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;
 +
| valign="top" | <math>\operatorname{F2.2e.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{cccl}
 +
\upharpoonleft \operatorname{Der}^L \upharpoonright
 +
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
 +
&  &    & \begin{array}{ccl}
 +
          \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;
 +
| valign="top" | <math>\operatorname{F2.2f.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{cccl}
 +
\upharpoonleft \operatorname{Der}^L \upharpoonright
 +
& = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\
 +
&  &    & \begin{array}{cll}
 +
          \underset{o \in O}{\operatorname{Conj}} \\
 +
          & \underline{((}    & \upharpoonleft \operatorname{Den}^L x \upharpoonright \\
 +
          & ,                & \upharpoonleft \operatorname{Den}^L y \upharpoonright \\
 +
          & \underline{))}^\$ & (o) \\
 +
          \end{array} \\
 +
&  & \} & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" |
 +
<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;
 +
| <math>\text{then}\!</math>
 +
| <math>\text{the following are equivalent:}\!</math>
 +
| style="border-left:1px solid black" | &nbsp;
 +
|}
 +
|-
 +
|
 +
{| 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;
 +
| valign="top" | <math>\operatorname{F2.3a.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{cccl}
 +
\operatorname{Der}^L
 +
& = & \{ & (x, y) \in S \times I ~: \\
 +
&  &    & \begin{array}{ccl}
 +
          \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;
 +
| valign="top" | <math>\operatorname{F2.3b.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ccccl}
 +
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
 +
& = & \downharpoonleft  & \underset{o \in O}{\operatorname{Conj}} \\
 +
&  &                  & & \begin{array}{cl}
 +
                            ( & \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;
 +
| valign="top" | <math>\operatorname{F2.3c.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ccccl}
 +
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
 +
& = & \underset{o \in O}{\operatorname{Conj}} \\
 +
&  & & \begin{array}{ccl}
 +
        \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;
 +
| valign="top" | <math>\operatorname{F2.3d.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ccccl}
 +
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
 +
& = & \underset{o \in O}{\operatorname{Conj}} \\
 +
&  & & \begin{array}{ccl}
 +
        \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;
 +
| valign="top" | <math>\operatorname{F2.3e.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ccccl}
 +
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
 +
& = & \underset{o \in O}{\operatorname{Conj}} \\
 +
&  & & \begin{array}{cl}
 +
        \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;
 +
| valign="top" | <math>\operatorname{F2.3f.}</math>
 +
| valign="top" |
 +
<math>\begin{array}{ccccl}
 +
\upharpoonleft \operatorname{Der}^L \upharpoonright (x, y)
 +
& = & \underset{o \in O}{\operatorname{Conj}} \\
 +
&  & & \begin{array}{cl}
 +
        \underline{((} & \upharpoonleft L_{OS} \upharpoonright (o, x) \\
 +
        ,              & \upharpoonleft L_{OS} \upharpoonright (o, y) \\
 +
        \underline{))} & \\
 +
        \end{array} \\
 +
&  & & \\
 +
\end{array}</math>
 +
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{F2.3f~:~D10a}</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>
 +
|}
 +
 
 +
==Appendices==
 +
 
 +
===Logical 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{Logical 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>s ~\text{is a sentence about things in the universe X}</math>
 +
|- style="height:48px"
 +
| &nbsp;
 +
| <math>\text{and}\!</math>
 +
| <math>p ~\text{is a proposition} ~:~ X \to \underline\mathbb{B}</math>
 +
|- style="height:48px"
 +
| &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%"
 +
|- style="height:52px"
 +
| 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="20%" style="border-top:1px solid black" |
 +
<math>\downharpoonleft \operatorname{false} \downharpoonright</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{L1b}_{01}.\!</math>
 +
| <math>\downharpoonleft \operatorname{not}~ s \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>(\downharpoonleft s \downharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(p) ~:~ X \to \underline\mathbb{B}</math>
 +
|- style="height:52px"
 +
| &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;
 +
| 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;
 +
| <math>\text{and}\!</math>
 +
| <math>p ~:~ X \to \underline\mathbb{B}</math>
 +
|- style="height:48px"
 +
| &nbsp;
 +
| <math>\text{such that:}\!</math>
 +
| &nbsp;
 +
|- style="height:48px"
 +
| &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>(\upharpoonleft Q \upharpoonright)</math>
 +
| <math>=\!</math>
 +
| <math>(p) ~:~ X \to \underline\mathbb{B}</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G1b}_{10}.\!</math>
 +
| <math>\upharpoonleft Q \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>\upharpoonleft Q \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>p ~:~ X \to \underline\mathbb{B}</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{G1b}_{11}.\!</math>
 +
| <math>\upharpoonleft X \upharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>((~))</math>
 +
| <math>=\!</math>
 +
| <math>\underline{1} ~:~ X \to \underline\mathbb{B}</math>
 +
|}
 +
|}
 +
 
 +
<br>
 +
 
 +
===Logical 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{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;
 +
| <math>\text{and}\!</math>
 +
| <math>p, q ~\text{are propositions} ~:~ X \to \underline\mathbb{B}</math>
 +
|- style="height:48px"
 +
| &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>((p) q)\!</math>
 +
|- style="height:52px"
 +
| &nbsp;
 +
| align="left" | <math>\text{L2b}_{14}.\!</math>
 +
| <math>\downharpoonleft s ~\operatorname{or}~ 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}_{15}.\!</math>
 +
| <math>\downharpoonleft \operatorname{true} \downharpoonright</math>
 +
| <math>=\!</math>
 +
| <math>((~))</math>
 +
| <math>=\!</math>
 +
| <math>((~))</math>
 +
|}
 +
|}
 +
 
 +
<br>
 +
 
 +
===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>\upharpoonleft P ~\cup~ Q \upharpoonright</math>
| <math>=\!</math>
+
| <math>=\!</math>
| <math>((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright))</math>
+
| <math>((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright))</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{G2b}_{15}.\!</math>
| <math>\upharpoonleft X \upharpoonright</math>
+
| <math>\upharpoonleft X \upharpoonright</math>
| <math>=\!</math>
+
| <math>=\!</math>
| <math>((~))</math>
+
| <math>((~))</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>
  
<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>
 

Latest revision as of 22:14, 9 December 2015

Author: Jon Awbrey

1.3.12. Syntactic Transformations

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:

  1. The functional language of propositions
  2. The logical language of sentences
  3. The geometric language of sets

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:


  \(\text{Definition 1}\!\)
  \(\text{If}\!\) \(Q ~\subseteq~ X\)
  \(\text{then}\!\) \(\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}\)
  \(\text{such that:}\!\)  
  \(\operatorname{D1a.}\) \(\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q\) \(\forall x \in X\)


In practice, a definition like this is commonly used to substitute one logically equivalent expression or sentence for another in a context where the conditions of using the definition this way are satisfied and where the change is perceived to advance a proof. This employment of a definition can be expressed in the form of a STR that allows one to exchange two expressions of logically equivalent forms for one another in every context where their logical values are the only consideration. To be specific, the logical value of an expression is the value in the boolean domain \(\underline\mathbb{B} = \{ \underline{0}, \underline{1} \} = \{ \operatorname{false}, \operatorname{true} \}\) that the expression stands for in its context or represents to its interpreter.

In the case of Definition 1, the corresponding STR permits one to exchange a sentence of the form \(x \in Q\) with an expression of the form \(\upharpoonleft Q \upharpoonright (x)\) in any context that satisfies the conditions of its use, namely, the conditions of the definition that lead up to the stated equivalence. The relevant STR is recorded in Rule 1. By way of convention, I list the items that fall under a rule roughly in order of their ascending conceptual subtlety or their increasing syntactic complexity, without regard to their normal or typical orders of exchange, since this can vary widely from case to case.


      \(\text{Rule 1}\!\)
  \(\text{If}\!\) \(Q \subseteq X\)  
  \(\text{then}\!\) \(\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}\)  
  \(\text{and if}\!\) \(x \in X\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\text{R1a.}\!\) \(x \in Q\)  
  \(\text{R1b.}\!\) \(\upharpoonleft Q \upharpoonright (x)\)  


Conversely, any rule of this sort, properly qualified by the conditions under which it applies, can be turned back into a summary statement of the logical equivalence that is involved in its application. This mode of conversion a static principle and a transformational rule, that is, between a statement of equivalence and an equivalence of statements, is so automatic that it is usually not necessary to make a separate note of the "horizontal" versus the "vertical" versions.

As another example of a STR, consider the following logical equivalence, that holds for any \(Q \subseteq X\) and for all \(x \in X.\)

\(\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x) = \underline{1}.\)

In practice, this logical equivalence is used to exchange an expression of the form \(\upharpoonleft Q \upharpoonright (x)\) with a sentence of the form \(\upharpoonleft Q \upharpoonright (x) = \underline{1}\) in any context where one has a relatively fixed \(Q \subseteq X\) in mind and where one is conceiving \(x \in X\) to vary over its whole domain, namely, the universe \(X.\!\) This leads to the STR that is given in Rule 2.


      \(\text{Rule 2}\!\)
  \(\text{If}\!\) \(f : X \to \underline\mathbb{B}\)  
  \(\text{and}\!\) \(x \in X\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\text{R2a.}\!\) \(f(x)\!\)  
  \(\text{R2b.}\!\) \(f(x) = \underline{1}\)  


Rules like these can be chained together to establish extended rules, just so long as their antecedent conditions are compatible. For example, Rules 1 and 2 combine to give the equivalents that are listed in Rule 3. This follows from a recognition that the function \(\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}\) that is introduced in Rule 1 is an instance of the function \(f : X \to \underline\mathbb{B}\) that is mentioned in Rule 2. By the time one arrives in the "consequence box" of either Rule, then, one has in mind a comparatively fixed \(Q \subseteq X,\) a proposition \(f\!\) or \(\upharpoonleft Q \upharpoonright\) about things in \(X,\!\) and a variable argument \(x \in X.\)


  \(\operatorname{Rule~3}\)
  \(\text{If}\!\) \(Q ~\subseteq~ X\)  
  \(\text{and}\!\) \(x ~\in~ X\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\operatorname{R3a.}\) \(x ~\in~ Q\) \(\operatorname{R3a~:~R1a}\)
      \(::\!\)
  \(\operatorname{R3b.}\) \(\upharpoonleft Q \upharpoonright (x)\)

\(\operatorname{R3b~:~R1b}\)

\(\operatorname{R3b~:~R2a}\)

      \(::\!\)
  \(\operatorname{R3c.}\) \(\upharpoonleft Q \upharpoonright (x) ~=~ \underline{1}\) \(\operatorname{R3c~:~R2b}\)


A large stock of rules can be derived in this way, by chaining together segments that are selected from a stock of previous rules, with perhaps the whole process of derivation leading back to an axial body or a core stock of rules, with all recurring to and relying on an axiomatic basis. In order to keep track of their derivations, as their pedigrees help to remember the reasons for trusting their use in the first place, derived rules can be annotated by citing the rules from which they are derived.

In the present discussion, I am using a particular style of annotation for rule derivations, one that is called proof by grammatical paradigm or proof by syntactic analogy. The annotations in the right hand margin of the Rule Box interweave the numerators and the denominators of the paradigm being employed, in other words, the alternating terms of comparison in a sequence of analogies. Taking the syntactic transformations marked in the Rule Box one at a time, each step is licensed by its formal analogy to a previously established rule.

For example, the annnotation \(X_1 : A_1 :: X_2 : A_2\!\) may be read to say that \(X_1\!\) is to \(A_1\!\) as \(X_2\!\) is to \(A_2,\!\) where the step from \(A_1\!\) to \(A_2\!\) is permitted by a previously accepted rule.

This can be illustrated by considering the derivation of Rule 3 in the augmented form that follows:

\(\begin{array}{lcclc} \text{R3a.} & x \in Q & \text{is to} & \text{R1a.} & x \in Q \\[6pt] & & \text{as} & & \\[6pt] \text{R3b.} & \upharpoonleft Q \upharpoonright (x) & \text{is to} & \text{R1b.} & \upharpoonleft Q \upharpoonright (x) \\[6pt] & & \text{and} & & \\[6pt] \text{R3b.} & \upharpoonleft Q \upharpoonright (x) & \text{is to} & \text{R2a.} & f(x) \\[6pt] & & \text{as} & & \\[6pt] \text{R3c.} & \upharpoonleft Q \upharpoonright (x) = \underline{1} & \text{is to} & \text{R2b.} & f(x) = \underline{1} \end{array}\)

Notice how the sequence of analogies pivots on the term \(\text{R3b},\!\) viewing it first under the aegis of \(\text{R1b},\!\) as the second term of the first analogy, and then turning to view it again under the guise of \(\text{R2a},\!\) as the first term of the second analogy.

By way of convention, rules that are tailored to a particular application, case, or subject, and rules that are adapted to a particular goal, object, or purpose, I frequently refer to as Facts.

Besides linking rules together into extended sequences of equivalents, there is one other way that is commonly used to get new rules from old. Novel starting points for rules can be obtained by extracting pairs of equivalent expressions from a sequence that falls under an established rule and then stating their equality in the appropriate form of equation.

For example, extracting the expressions \(\text{R3a}\!\) and \(\text{R3c}\!\) that are given as equivalents in Rule 3 and explicitly stating their equivalence produces the equation recorded in Corollary 1.


     

\(\text{Corollary 1}\!\)

  \(\text{If}\!\) \(Q \subseteq X\)  
  \(\text{and}\!\) \(x \in X\)  
  \(\text{then}\!\) \(\text{the following statement is true:}\!\)  
  \(\text{C1a.}\!\)

\(x \in Q ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x) = \underline{1}\)

\(\text{R3a} \Leftrightarrow \text{R3c}\)


There are a number of issues, that arise especially in establishing the proper use of STRs, that are appropriate to discuss at this juncture. The notation \(\downharpoonleft s \downharpoonright\) is intended to represent the proposition denoted by the sentence \(s.\!\) There is only one problem with the use of this form. There is, in general, no such thing as "the" proposition denoted by \(s.\!\) Generally speaking, if a sentence is taken out of context and considered across a variety of different contexts, there is no unique proposition that it can be said to denote. But one is seldom ever speaking at the maximum level of generality, or even found to be thinking of it, and so this notation is usually meaningful and readily understandable whenever it is read in the proper frame of mind. Still, once the issue is raised, the question of how these meanings and understandings are possible has to be addressed, especially if one desires to express the regulations of their syntax in a partially computational form. This requires a closer examination of the very notion of context, and it involves engaging in enough reflection on the contextual evaluation of sentences that the relevant principles of its successful operation can be discerned and rationalized in explicit terms.

A sentence that is written in a context where it represents a value of \(\underline{1}\) or \(\underline{0}\) as a function of things in the universe \(X,\!\) where it stands for a value of \(\operatorname{truth}\) or \(\operatorname{falsehood},\) depending on how the signs that constitute its proper syntactic arguments are interpreted as denoting objects in \(X,\!\) in other words, where it is bound to lead its interpreter to view its own truth or falsity as determined by a choice of objects in \(X,\!\) is a sentence that might as well be written in the context \(\downharpoonleft \ldots \downharpoonright,\) whether this frame is explicitly marked around it or not.

More often than not, the context of interpretation fixes the denotations of most of the signs that make up a sentence, and so it is safe to adopt the convention that only those signs whose objects are not already fixed are free to vary in their denotations. Thus, only the signs that remain in default of prior specification are subject to treatment as variables, with a decree of functional abstraction hanging over all of their heads.

\(\downharpoonleft x \in Q \downharpoonright ~=~ \lambda (x, \in, Q).(x \in Q).\)

Going back to Rule 1, we see that it lists a pair of concrete sentences and authorizes exchanges in either direction between the syntactic structures that have these two forms. But a sentence is any sign that denotes a proposition, and so there are any number of less obvious sentences that can be added to this list, extending the number of items that are licensed to be exchanged. For example, a larger collection of equivalent sentences is recorded in Rule 4.


      \(\text{Rule 4}\!\)
  \(\text{If}\!\) \(Q \subseteq X ~\text{is fixed}\)  
  \(\text{and}\!\) \(x \in X ~\text{is varied}\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\text{R4a.}\!\) \(x \in Q\)  
  \(\text{R4b.}\!\) \(\downharpoonleft x \in Q \downharpoonright\)  
  \(\text{R4c.}\!\) \(\downharpoonleft x \in Q \downharpoonright (x)\)  
  \(\text{R4d.}\!\) \(\upharpoonleft Q \upharpoonright (x)\)  
  \(\text{R4e.}\!\) \(\upharpoonleft Q \upharpoonright (x) = \underline{1}\)  


The first and last items on this list, namely, the sentence \(\text{R4a}\!\) stating \(x \in Q\) and the sentence \(\text{R4e}\!\) stating \(\upharpoonleft Q \upharpoonright (x) = \underline{1},\) are just the pair of sentences from Rule 3 whose equivalence for all \(x \in X\) is usually taken to define the idea of an indicator function \(\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}.\) At first sight, the inclusion of the other items appears to involve a category confusion, in other words, to mix the modes of interpretation and to create an array of mismatches between their ostensible types and the ruling type of a sentence. On reflection, and taken in context, these problems are not as serious as they initially seem. For example, the expression \(^{\backprime\backprime} \downharpoonleft x \in Q \downharpoonright \, ^{\prime\prime}\) ostensibly denotes a proposition, but if it does, then it evidently can be recognized, by virtue of this very fact, to be a genuine sentence. As a general rule, if one can see it on the page, then it cannot be a proposition but can at most be a sign of one.

The use of the basic logical connectives can be expressed in the form of a STR as follows:


\(\text{Logical Translation Rule 0}\!\)  
  \(\text{If}\!\)

\(s_j ~\text{is a sentence about things in the universe X}\)

  \(\text{and}\!\) \(p_j ~\text{is a proposition about things in the universe X}\)
  \(\text{such that:}\!\)  
  \(\text{L0a.}\!\) \(\downharpoonleft s_j \downharpoonright ~=~ p_j, ~\text{for all}~ j \in J,\)
  \(\text{then}\!\) \(\text{the following equations are true:}\!\)
  \(\text{L0b.}\!\)

\(\downharpoonleft \operatorname{Conc}_j^J s_j \downharpoonright\)

\(=\!\)

\(\operatorname{Conj}_j^J \downharpoonleft s_j \downharpoonright\)

\(=\!\)

\(\operatorname{Conj}_j^J p_j\)

  \(\text{L0c.}\!\) \(\downharpoonleft \operatorname{Surc}_j^J s_j \downharpoonright\) \(=\!\) \(\operatorname{Surj}_j^J \downharpoonleft s_j \downharpoonright\) \(=\!\) \(\operatorname{Surj}_j^J p_j\)


As a general rule, the application of a STR involves the recognition of an antecedent condition and the facilitation of a consequent condition. The antecedent condition is a state whose initial expression presents a match, in a formal sense, to one of the sentences that are listed in the STR, and the consequent condition is achieved by taking its suggestions seriously, in other words, by following its sequence of equivalents and implicants to some other link in its chain.

Generally speaking, the application of a rule involves the recognition of an antecedent condition as a case that falls under a clause of the rule. This means that the antecedent condition is able to be captured in the form, conceived in the guise, expressed in the manner, grasped in the pattern, or recognized in the shape of one of the sentences in a list of equivalents or a chain of implicants.

A condition is amenable to a rule if any of its conceivable expressions formally match any of the expressions that are enumerated by the rule. Further, it requires the relegation of the other expressions to the production of a result. Thus, there is the choice of an initial expression that needs to be checked on input for whether it fits the antecedent condition and there are several types of output that are generated as a consequence, only a few of which are usually needed at any given time.

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.

A rule that allows one to turn equivalent sentences into identical propositions:

\((S \Leftrightarrow T) \quad \Leftrightarrow \quad (\downharpoonleft S \downharpoonright = \downharpoonleft T \downharpoonright)\)

Compare:

\(\downharpoonleft v = w \downharpoonright (v, w)\)
\(\downharpoonleft v(u) = w(u) \downharpoonright (u)\)

Editing Note. The last draft I can find has 5 variants for the next box, "Value Rule 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:


\(\operatorname{Evaluation~Rule~1}\)  
  \(\text{If}\!\) \(f, g ~:~ X \to \underline\mathbb{B}\)
  \(\text{and}\!\) \(x ~\in~ X\)
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)
       
  \(\operatorname{E1a.}\) \(f(x) ~=~ g(x)\) \(\operatorname{E1a~:~V1a}\)
  \(::\!\)
  \(\operatorname{E1b.}\) \(f(x) ~\Leftrightarrow~ g(x)\) \(\operatorname{E1b~:~V1b}\)
  \(::\!\)
  \(\operatorname{E1c.}\) \(\underline{((}~ f(x) ~,~ g(x) ~\underline{))}\)

\(\operatorname{E1c~:~V1c}\)

\(\operatorname{E1c~:~$1a}\)

  \(::\!\)
  \(\operatorname{E1d.}\) \(\underline{((}~ f ~,~ g ~\underline{))}^\$ (x)\) \(\operatorname{E1d~:~$1b}\)
   


  \(\operatorname{Definition~2}\)
  \(\text{If}\!\) \(P, Q ~\subseteq~ X\)
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)
  \(\operatorname{D2a.}\) \(P ~=~ Q\)
  \(\operatorname{D2b.}\) \(\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)\)


  \(\operatorname{Definition~3}\)
  \(\text{If}\!\) \(f, g ~:~ X \to Y\)
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)
  \(\operatorname{D3a.}\) \(f ~=~ g\)
  \(\operatorname{D3b.}\) \(\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))\)


  \(\operatorname{Definition~4}\)
  \(\text{If}\!\) \(Q ~\subseteq~ X\)
  \(\text{then}\!\) \(\text{the following are identical subsets of}~ X \times \underline\mathbb{B}:\)
  \(\operatorname{D4a.}\) \(\upharpoonleft Q \upharpoonright\)
  \(\operatorname{D4b.}\) \(\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in Q \downharpoonright\)


  \(\operatorname{Definition~5}\)
  \(\text{If}\!\) \(Q ~\subseteq~ X\)
  \(\text{then}\!\) \(\text{the following are identical propositions} ~:~ X \to \underline\mathbb{B}\)
  \(\operatorname{D5a.}\) \(\upharpoonleft Q \upharpoonright\)
  \(\operatorname{D5b.}\) \(\downharpoonleft x \in Q \downharpoonright\)


Given an indexed set of sentences, \(s_j\!\) for \(j \in J,\) it is possible to consider the logical conjunction of the corresponding propositions. Various notations for this concept are be useful in various contexts, a sufficient sample of which are recorded in Definition 6.


  \(\operatorname{Definition~6}\)
  \(\text{If}\!\) \(\text{each string}~ s_j, ~\text{as}~ j ~\text{ranges over the set}~ J,\)
    \(\text{is a sentence about things in the universe}~ X~\)
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)
  \(\operatorname{D6a.}\) \(\overset{J}{\underset{j}{\forall}}~ s_j\)
  \(\operatorname{D6b.}\) \(\operatorname{Conj}_j^J s_j\)


  \(\operatorname{Definition~7}\)
  \(\text{If}\!\) \(s, t ~\text{are sentences about things in the universe}~ X\)
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)
  \(\operatorname{D7a.}\) \(s ~\Leftrightarrow~ t\)
  \(\operatorname{D7b.}\) \(\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright\)


  \(\operatorname{Rule~5}\)
  \(\text{If}\!\) \(P, Q ~\subseteq~ X\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\operatorname{R5a.}\) \(P ~=~ Q\) \(\operatorname{R5a~:~D2a}\)
      \(::\!\)
  \(\operatorname{R5b.}\) \(\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)\)

\(\operatorname{R5b~:~D2b}\)

\(\operatorname{R5b~:~D7a}\)

      \(::\!\)
  \(\operatorname{R5c.}\) \(\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright)\)

\(\operatorname{R5c~:~D7b}\)

\(\operatorname{R5c~:~\_\_?\_\_}\)

      \(::\!\)
  \(\operatorname{R5d.}\)

\(\begin{matrix} \{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in P \downharpoonright \\ = \\ \{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in Q \downharpoonright \end{matrix}\)

\(\operatorname{R5d~:~\_\_?\_\_}\)

\(\operatorname{R5d~:~D5b}\)

      \(::\!\)
  \(\operatorname{R5e.}\) \(\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright\) \(\operatorname{R5e~:~D5a}\)


  \(\operatorname{Rule~6}\)
  \(\text{If}\!\) \(f, g ~:~ X \to Y\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\operatorname{R6a.}\) \(f ~=~ g\) \(\operatorname{R6a~:~D3a}\)
      \(::\!\)
  \(\operatorname{R6b.}\) \(\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))\)

\(\operatorname{R6b~:~D3b}\)

\(\operatorname{R6b~:~D6a}\)

      \(::\!\)
  \(\operatorname{R6c.}\) \(\operatorname{Conj_x^X}~ (f(x) ~=~ g(x))\) \(\operatorname{R6c~:~D6b}\)


  \(\operatorname{Rule~7}\)
  \(\text{If}\!\) \(p, q ~:~ X \to \underline\mathbb{B}\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\operatorname{R7a.}\) \(p ~=~ q\) \(\operatorname{R7a~:~R6a}\)
      \(::\!\)
  \(\operatorname{R7b.}\) \(\overset{X}{\underset{x}{\forall}}~ (p(x) ~=~ q(x))\) \(\operatorname{R7b~:~R6b}\)
      \(::\!\)
  \(\operatorname{R7c.}\) \(\operatorname{Conj_x^X}~ (p(x) ~=~ q(x))\)

\(\operatorname{R7c~:~R6c}\)

\(\operatorname{R7c~:~P1a}\)

      \(::\!\)
  \(\operatorname{R7d.}\) \(\operatorname{Conj_x^X}~ (p(x) ~\Leftrightarrow~ q(x))\) \(\operatorname{R7d~:~P1b}\)
      \(::\!\)
  \(\operatorname{R7e.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ p(x) ~,~ q(x) ~\underline{))}\)

\(\operatorname{R7e~:~P1c}\)

\(\operatorname{R7e~:~$1a}\)

      \(::\!\)
  \(\operatorname{R7f.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ p ~,~ q ~\underline{))}^\$ (x)\) \(\operatorname{R7f~:~$1b}\)


Editing Note. Check earlier and later drafts to see where \(\text{P1a, P1b, P1c}~\) came from. Are these just placeholders for the Value or Evaluation Rules?


  \(\operatorname{Rule~8}\)
  \(\text{If}\!\) \(s, t ~\text{are sentences about things in}~ X\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\operatorname{R8a.}\) \(s ~\Leftrightarrow~ t\)

\(\operatorname{R8a~:~D7a}\)

      \(::\!\)
  \(\operatorname{R8b.}\) \(\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright\)

\(\operatorname{R8b~:~D7b}\)

\(\operatorname{R8b~:~R7a}\)

      \(::\!\)
  \(\operatorname{R8c.}\) \(\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))\) \(\operatorname{R8c~:~R7b}\)
      \(::\!\)
  \(\operatorname{R8d.}\) \(\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))\) \(\operatorname{R8d~:~R7c}\)
      \(::\!\)
  \(\operatorname{R8e.}\) \(\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft t \downharpoonright (x))\) \(\operatorname{R8e~:~R7d}\)
      \(::\!\)
  \(\operatorname{R8f.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright (x) ~,~ \downharpoonleft t \downharpoonright (x) ~\underline{))}\) \(\operatorname{R8f~:~R7e}\)
      \(::\!\)
  \(\operatorname{R8g.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright ~\underline{))}^\$ (x)\) \(\operatorname{R8g~:~R7f}\)


For instance, the observation that expresses the equality of sets in terms of their indicator functions can be formalized according to the pattern in Rule 9, namely, at lines R9a, R9b, and R9c, and these components of Rule 9 can be cited in future uses by their indices in this list. Using Rule 7, annotated as R7, to adduce a few properties of indicator functions to the account, it is possible to extend Rule 9 by another few steps, referenced as R9d, R9e, R9f, and R9g.


  \(\operatorname{Rule~9}\)
  \(\text{If}\!\) \(P, Q ~\subseteq~ X\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\operatorname{R9a.}\) \(P ~=~ Q\) \(\operatorname{R9a~:~R5a}\)
      \(::\!\)
  \(\operatorname{R9b.}\) \(\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright\)

\(\operatorname{R9b~:~R5e}\)

\(\operatorname{R9b~:~R7a}\)

      \(::\!\)
  \(\operatorname{R9c.}\) \(\overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))\) \(\operatorname{R9c~:~R7b}\)
      \(::\!\)
  \(\operatorname{R9d.}\) \(\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))\) \(\operatorname{R9d~:~R7c}\)
      \(::\!\)
  \(\operatorname{R9e.}\) \(\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x))\) \(\operatorname{R9e~:~R7d}\)
      \(::\!\)
  \(\operatorname{R9f.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}\) \(\operatorname{R9f~:~R7e}\)
      \(::\!\)
  \(\operatorname{R9g.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\$ (x)\) \(\operatorname{R9g~:~R7f}\)


  \(\operatorname{Rule~10}\)
  \(\text{If}\!\) \(P, Q ~\subseteq~ X\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\operatorname{R10a.}\) \(P ~=~ Q\) \(\operatorname{R10a~:~D2a}\)
      \(::\!\)
  \(\operatorname{R10b.}\) \(\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)\)

\(\operatorname{R10b~:~D2b}\)

\(\operatorname{R10b~:~R8a}\)

      \(::\!\)
  \(\operatorname{R10c.}\) \(\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright\) \(\operatorname{R10c~:~R8b}\)
      \(::\!\)
  \(\operatorname{R10d.}\) \(\overset{X}{\underset{x}{\forall}}~ \downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x)\) \(\operatorname{R10d~:~R8c}\)
      \(::\!\)
  \(\operatorname{R10e.}\) \(\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x))\) \(\operatorname{R10e~:~R8d}\)
      \(::\!\)
  \(\operatorname{R10f.}\) \(\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft x \in Q \downharpoonright (x))\) \(\operatorname{R10f~:~R8e}\)
      \(::\!\)
  \(\operatorname{R10g.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft x \in P \downharpoonright (x) ~,~ \downharpoonleft x \in Q \downharpoonright (x) ~\underline{))}\) \(\operatorname{R10g~:~R8f}\)
      \(::\!\)
  \(\operatorname{R10h.}\) \(\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft x \in P \downharpoonright ~,~ \downharpoonleft x \in Q \downharpoonright ~\underline{))}^\$ (x)\) \(\operatorname{R10h~:~R8g}\)


  \(\operatorname{Rule~11}\)
  \(\text{If}\!\) \(Q ~\subseteq~ X\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\operatorname{R11a.}\) \(Q ~=~ \{ x \in X ~:~ s \}\) \(\operatorname{R11a~:~R5a}\)
      \(::\!\)
  \(\operatorname{R11b.}\) \(\upharpoonleft Q \upharpoonright ~=~ \upharpoonleft \{ x \in X ~:~ s \} \upharpoonright\) \(\operatorname{R11b~:~R5e}\)
      \(::\!\)
  \(\operatorname{R11c.}\)

\(\begin{array}{lcl} \upharpoonleft Q \upharpoonright & \subseteq & X \times \underline\mathbb{B} \\ \upharpoonleft Q \upharpoonright & = & \{ (x, y) \in X \times \underline\mathbb{B} ~:~ y = \, \downharpoonleft s \downharpoonright (x) \} \end{array}\)

\(\operatorname{R11c~:~\_\_?\_\_}\)

\(\operatorname{R11c~:~\_\_?\_\_}\)

      \(::\!\)
  \(\operatorname{R11d.}\)

\(\begin{array}{ccccl} \upharpoonleft Q \upharpoonright & : & X & \to & \underline\mathbb{B} \\ \upharpoonleft Q \upharpoonright & : & x & \mapsto & \downharpoonleft s \downharpoonright (x) \end{array}\)

\(\operatorname{R11d~:~\_\_?\_\_}\)

\(\operatorname{R11d~:~\_\_?\_\_}\)

      \(::\!\)
  \(\operatorname{R11e.}\) \(\overset{X}{\underset{x}{\forall}}~ \upharpoonleft Q \upharpoonright (x) ~=~ \downharpoonleft s \downharpoonright (x)\)

\(\operatorname{R11e~:~\_\_?\_\_}\)

\(\operatorname{R11e~:~\_\_?\_\_}\)

      \(::\!\)
  \(\operatorname{R11f.}\) \(\upharpoonleft Q \upharpoonright ~=~ \downharpoonleft s \downharpoonright\) \(\operatorname{R11f~:~\_\_?\_\_}\)


An application of Rule 11 involves the recognition of an antecedent condition as a case under the Rule, that is, as a condition that matches one of the sentences in the Rule's chain of equivalents, and it requires the relegation of the other expressions to the production of a result. Thus, there is the choice of an initial expression that has to be checked on input for whether it fits the antecedent condition, and there is the choice of three types of output that are generated as a consequence, only one of which is generally needed at any given time. More often than not, though, a rule is applied in only a few of its possible ways. The usual antecedent and the usual consequents for Rule 11 can be distinguished in form and specialized in practice as follows:

\(\operatorname{R11a}\) marks the usual starting place for an application of the Rule, that is, the standard form of antecedent condition that is likely to lead to an invocation of the Rule.
\(\operatorname{R11b}\) records the trivial consequence of applying the up-spar operator \(\upharpoonleft \cdots \upharpoonright\) to both sides of the initial equation.
\(\operatorname{R11c}\) gives a version of the indicator function with \(\upharpoonleft X \upharpoonright ~\subseteq~ X \times \underline\mathbb{B},\) called the extensional or relational form of the indicator function.
\(\operatorname{R11d}\) gives a version of the indicator function with \(\upharpoonleft X \upharpoonright ~:~ X \to \underline\mathbb{B},\) called its functional form.

Applying Rule 9, Rule 8, and the Logical Rules to the special case where \(s \Leftrightarrow (X = Y),\) one obtains the following general Fact:


  \(\operatorname{Fact~1}\)
  \(\text{If}\!\) \(P, Q ~\subseteq~ X\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
  \(\operatorname{F1a.}\) \(s \quad \Leftrightarrow \quad (P ~=~ Q)\)

\(\operatorname{F1a~:~R9a}\)

      \(::\!\)
  \(\operatorname{F1b.}\) \(s \quad \Leftrightarrow \quad (\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright)\)

\(\operatorname{F1b~:~R9b}\)

      \(::\!\)
  \(\operatorname{F1c.}\) \(s \quad \Leftrightarrow \quad \overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))\)

\(\operatorname{F1c~:~R9c}\)

      \(::\!\)
  \(\operatorname{F1d.}\) \(s \quad \Leftrightarrow \quad \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))\)

\(\operatorname{F1d~:~R9d}\)

\(\operatorname{F1d~:~R8a}\)

      \(::\!\)
  \(\operatorname{F1e.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \downharpoonleft \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright\)

\(\operatorname{F1e~:~R8b}\)

\(\operatorname{F1e~:~\_\_?\_\_}\)

      \(::\!\)
  \(\operatorname{F1f.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \downharpoonleft (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright\)

\(\operatorname{F1f~:~\_\_?\_\_}\)

\(\operatorname{F1f~:~\_\_?\_\_}\)

      \(::\!\)
  \(\operatorname{F1g.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}\)

\(\operatorname{F1g~:~\_\_?\_\_}\)

\(\operatorname{F1g~:~\_\_?\_\_}\)

      \(::\!\)
  \(\operatorname{F1h.}\) \(\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright ~\underline{))}^\$ (x)\)

\(\operatorname{F1h~:~~\_\_?\_\_}\)


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.

A classic way of showing that two sets are equal is to show that every element of the first belongs to the second and that every element of the second belongs to the first. The problem with this strategy is that one can exhaust a considerable amount of time trying to prove that two sets are equal before it occurs to one to look for a counterexample, that is, an element of the first that does not belong to the second or an element of the second that does not belong to the first, in cases where that is precisely what one ought to be seeking. It would be nice if there were a more balanced, impartial, or neutral way to go about this task, one that did not require such an undue commitment to either side, a technique that helps to pinpoint the counterexamples when they exist, and a method that keeps in mind the original relation of proving that and showing that to probing, testing, and seeing whether.

A different way of seeing that two sets are equal, or of seeing whether two sets are equal, is based on the following observation:

Two sets are equal as sets
\(\iff\)
The indicator functions of the two sets are equal as functions
\(\iff\)
The values of the two indicator functions are equal to each other on all domain elements.

It is important to notice the hidden quantifier, of a universal kind, that lurks in all three equivalent statements but is only revealed in the last.

In making the next set of definitions and in using the corresponding terminology it is taken for granted that all of the references of signs are relative to a particular sign relation \(L \subseteq O \times S \times I\) that either remains to be specified or is already understood. Further, I continue to assume that \(S = I,\!\) in which case this set is called the syntactic domain of \(L.\!\)

In the following definitions, let \(L \subseteq O \times S \times I,\) let \(S = I,\!\) and let \(x, y \in S.\!\)

Recall the definition of \(\operatorname{Con} (L),\) the connotative component of a sign relation \(L,\!\) in the following form:

\(\operatorname{Con} (L) ~=~ L_{SI} ~=~ \{ (s, i) \in S \times I ~:~ (o, s, i) \in L ~\text{for some}~ o \in O \}.\)

Equivalent expressions for this concept are recorded in Definition 8.


  \(\operatorname{Definition~8}\)
  \(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)
  \(\text{then}\!\) \(\text{the following are identical subsets of}~ S \times I \, :\)
  \(\operatorname{D8a.}\) \(L_{SI}\!\)
  \(\operatorname{D8b.}\) \(\operatorname{Con}^L\)
  \(\operatorname{D8c.}\) \(\operatorname{Con}(L)\)
  \(\operatorname{D8d.}\) \(\operatorname{proj}_{SI}(L)\)
  \(\operatorname{D8e.}\) \(\{ (s, i) \in S \times I ~:~ (o, s, i) \in L ~\operatorname{for~some}~ o \in O \}\)


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 \(\ell,\) namely, \(K\ell ~=~ k\!\cdot\!\ell ~=~ \breve\ell.\)

The dyadic relation \(L_{IS}\!\) that is the converse of the connotative relation \(L_{SI}\!\) can be defined directly in the following fashion:

\(\overset{\smile}{\operatorname{Con}(L)} ~=~ L_{IS} ~=~ \{ (i, s) \in I \times S ~:~ (o, s, i) \in L ~\text{for some}~ o \in O \}.\)

A few of the many different expressions for this concept are recorded in Definition 9.


  \(\operatorname{Definition~9}\)
  \(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)
  \(\text{then}\!\) \(\text{the following are identical subsets of}~ I \times S \, :\)
  \(\operatorname{D9a.}\) \(L_{IS}\!\)
  \(\operatorname{D9b.}\) \(\overset{\smile}{L_{SI}}\)
  \(\operatorname{D9c.}\) \(\overset{\smile}{\operatorname{Con}^L}\)
  \(\operatorname{D9d.}\) \(\overset{\smile}{\operatorname{Con}(L)}\)
  \(\operatorname{D9e.}\) \(\operatorname{proj}_{IS}(L)\)
  \(\operatorname{D9f.}\) \(\operatorname{Conv}(\operatorname{Con}(L))\)
  \(\operatorname{D9g.}\) \(\{ (i, s) \in I \times S ~:~ (o, s, i) \in L ~\operatorname{for~some}~ o \in O \}\)


Recall the definition of \(\operatorname{Den} (L),\) the denotative component of \(L,\!\) in the following form:

\(\operatorname{Den} (L) ~=~ L_{OS} ~=~ \{ (o, s) \in O \times S ~:~ (o, s, i) \in L ~\text{for some}~ i \in I \}.\)

Equivalent expressions for this concept are recorded in Definition 10.


  \(\operatorname{Definition~10}\)
  \(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)
  \(\text{then}\!\) \(\text{the following are identical subsets of}~ O \times S \, :\)
  \(\operatorname{D10a.}\) \(L_{OS}\!\)
  \(\operatorname{D10b.}\) \(\operatorname{Den}^L\)
  \(\operatorname{D10c.}\) \(\operatorname{Den}(L)\)
  \(\operatorname{D10d.}\) \(\operatorname{proj}_{OS}(L)\)
  \(\operatorname{D10e.}\) \(\{ (o, s) \in O \times S ~:~ (o, s, i) \in L ~\operatorname{for~some}~ i \in I \}\)


The dyadic relation \(L_{SO}\!\) that is the converse of the denotative relation \(L_{OS}\!\) can be defined directly in the following fashion:

\(\overset{\smile}{\operatorname{Den}(L)} ~=~ L_{SO} ~=~ \{ (s, o) \in S \times O ~:~ (o, s, i) \in L ~\text{for some}~ i \in I \}.\)

A few of the many different expressions for this concept are recorded in Definition 11.


  \(\operatorname{Definition~11}\)
  \(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)
  \(\text{then}\!\) \(\text{the following are identical subsets of}~ S \times O \, :\)
  \(\operatorname{D11a.}\) \(L_{SO}\!\)
  \(\operatorname{D11b.}\) \(\overset{\smile}{L_{OS}}\)
  \(\operatorname{D11c.}\) \(\overset{\smile}{\operatorname{Den}^L}\)
  \(\operatorname{D11d.}\) \(\overset{\smile}{\operatorname{Den}(L)}\)
  \(\operatorname{D11e.}\) \(\operatorname{proj}_{SO}(L)\)
  \(\operatorname{D11f.}\) \(\operatorname{Conv}(\operatorname{Den}(L))\)
  \(\operatorname{D11g.}\) \(\{ (s, o) \in S \times O ~:~ (o, s, i) \in L ~\operatorname{for~some}~ i \in I \}\)


The denotation of \(x\!\) in \(L,\!\) written \(\operatorname{Den}(L, x),\) is defined as follows:

\(\operatorname{Den}(L, x) ~=~ \{ o \in O ~:~ (o, x) \in \operatorname{Den}(L) \}.\)

In other words:

\(\operatorname{Den}(L, x) ~=~ \{ o \in O ~:~ (o, x, i) \in L ~\text{for some}~ i \in I \}.\)

Equivalent expressions for this concept are recorded in Definition 12.


  \(\operatorname{Definition~12}\)
  \(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)
  \(\text{and}\!\) \(x ~\in~ S\)
  \(\text{then}\!\) \(\text{the following are identical subsets of}~ O \, :\)
  \(\operatorname{D12a.}\) \(L_{OS} \cdot x\)
  \(\operatorname{D12b.}\) \(\operatorname{Den}^L \cdot x\)
  \(\operatorname{D12c.}\) \(\operatorname{Den}^L |_x\)
  \(\operatorname{D12d.}\) \(\operatorname{Den}^L (-, x)\)
  \(\operatorname{D12e.}\) \(\operatorname{Den}(L, x)\)
  \(\operatorname{D12f.}\) \(\operatorname{Den}(L) \cdot x\)
  \(\operatorname{D12g.}\) \(\{ o \in O ~:~ (o, x) \in \operatorname{Den}(L) \}\)
  \(\operatorname{D12h.}\) \(\{ o \in O ~:~ (o, x, i) \in L ~\operatorname{for~some}~ i \in I \}\)


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.

To define the equiference of signs in terms of their denotations, one says that \(x\!\) is equiferent to \(y\!\) under \(L,\!\) and writes \(x ~\overset{L}{=}~ y,\!\) to mean that \(\operatorname{Den}(L, x) = \operatorname{Den}(L, y).\) Taken in extension, this notion of a relation between signs induces an equiference relation on the syntactic domain.

For each sign relation \(L,\!\) this yields a binary relation \(\operatorname{Der}(L) \subseteq S \times I\) that is defined as follows:

\(\operatorname{Der}(L) ~=~ Der^L ~=~ \{ (x, y) \in S \times I ~:~ \operatorname{Den}(L, x) = \operatorname{Den}(L, y) \}.\)

These definitions and notations are recorded in the following display.


  \(\operatorname{Definition~13}\)
  \(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)
  \(\text{then}\!\) \(\text{the following are identical subsets of}~ S \times I \, :\)
  \(\operatorname{D13a.}\) \(\operatorname{Der}^L\)
  \(\operatorname{D13b.}\) \(\operatorname{Der}(L)\)
  \(\operatorname{D13c.}\) \(\{ (x, y) \in S \times I ~:~ \operatorname{Den}^L|_x = \operatorname{Den}^L|_y \}\)
  \(\operatorname{D13d.}\) \(\{ (x, y) \in S \times I ~:~ \operatorname{Den}(L, x) = \operatorname{Den}(L, y) \}\)


The relation \(\operatorname{Der}(L)\) is defined and the notation \(x ~\overset{L}{=}~ y\) is meaningful in every situation where the corresponding denotation operator \(\operatorname{Den}(-,-)\) makes sense, but it remains to check whether this relation enjoys the properties of an equivalence relation.

  1. Reflexive property.

    Is it true that \(x ~\overset{L}{=}~ x\) for every \(x \in S = I\)?

    By definition, \(x ~\overset{L}{=}~ x\) if and only if \(\operatorname{Den}(L, x) = \operatorname{Den}(L, x).\)

    Thus, the reflexive property holds in any setting where the denotations \(\operatorname{Den}(L, x)\) are defined for all signs \(x\!\) in the syntactic domain of \(R.\!\)

  2. Symmetric property.

    Does \(x ~\overset{L}{=}~ y\) imply \(y ~\overset{L}{=}~ x\) for all \(x, y \in S\)?

    In effect, does \(\operatorname{Den}(L, x) = \operatorname{Den}(L, y)\) imply \(\operatorname{Den}(L, y) = \operatorname{Den}(L, x)\) for all signs \(x\!\) and \(y\!\) in the syntactic domain \(S\!\)?

    Yes, so long as the sets \(\operatorname{Den}(L, x)\) and \(\operatorname{Den}(L, y)\) are well-defined, a fact which is already being assumed.

  3. Transitive property.

    Does \(x ~\overset{L}{=}~ y\) and \(y ~\overset{L}{=}~ z\) imply \(x ~\overset{L}{=}~ z\) for all \(x, y, z \in S\)?

    To belabor the point, does \(\operatorname{Den}(L, x) = \operatorname{Den}(L, y)\) and \(\operatorname{Den}(L, y) = \operatorname{Den}(L, z)\) imply \(\operatorname{Den}(L, x) = \operatorname{Den}(L, z)\) for all \(x, y, z \in S\)?

    Yes, once again, under the stated conditions.

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.

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 (DECs), denotative partitions (DEPs), and denotative equations (DEQs) on the syntactic domain. But what does it mean for signs to be equiferent?

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.

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 \(x ~\overset{L}{=}~ y.\)

The uses of the equal sign for denoting equations or equivalences are recalled and extended in the following ways:

  1. If \(E\!\) is an arbitrary equivalence relation, then the equation \(x =_E y\!\) means that \((x, y) \in E.\)
  2. If \(L\!\) is a sign relation such that \(L_{SI}\!\) is a SER on \(S = I,\!\) then the semiotic equation \(x =_L y\!\) means that \((x, y) \in L_{SI}.\)
  3. If \(L\!\) is a sign relation such that \(F\!\) is its DER on \(S = I,\!\) then the denotative equation \(x ~\overset{L}{=}~ y\) means that \((x, y) \in F,\) in other words, that \(\operatorname{Den}(L, x) = \operatorname{Den}(L, y).\)

The use of square brackets for denoting equivalence classes is recalled and extended in the following ways:

  1. If \(E\!\) is an arbitrary equivalence relation, then \([x]_E\!\) is the equivalence class of \(x\!\) under \(E.\!\)
  2. If \(L\!\) is a sign relation such that \(\operatorname{Con}(L)\) is a SER on \(S = I,\!\) then \([x]_L\!\) is the SEC of \(x\!\) under \(\operatorname{Con}(L).\)
  3. If \(L\!\) is a sign relation such that \(\operatorname{Der}(L)\) is a DER on \(S = I,\!\) then \([x]^L\!\) is the DEC of \(x\!\) under \(\operatorname{Der}(L).\)

By applying the form of Fact 1 to the special case where \(X = \operatorname{Den}(L, x)\) and \(Y = \operatorname{Den}(L, y),\) one obtains the following facts.


  \(\operatorname{Fact~2.1}\)
  \(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)  
  \(\text{then}\!\) \(\text{the following are identical subsets of}~ S \times I :\)  
  \(\operatorname{F2.1a.}\) \(\operatorname{Der}^L\) \(\operatorname{F2.1a~:~D13a}\)
      \(::\!\)
  \(\operatorname{F2.1b.}\) \(\operatorname{Der}(L)\)

\(\operatorname{F2.1b~:~D13b}\)

      \(::\!\)
  \(\operatorname{F2.1c.}\)

\(\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \operatorname{Den}(L, x) ~=~ \operatorname{Den}(L, y) \\ \} & \\ \end{array}\)

\(\operatorname{F2.1c~:~D13c}\)

\(\operatorname{F2.1c~:~R9a}\)

      \(::\!\)
  \(\operatorname{F2.1d.}\)

\(\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \upharpoonleft \operatorname{Den}(L, x) \upharpoonright ~=~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright \\ \} & \\ \end{array}\)

\(\operatorname{F2.1d~:~R9b}\)

      \(::\!\)
  \(\operatorname{F2.1e.}\)

\(\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}\)

\(\operatorname{F2.1e~:~R9c}\)

      \(::\!\)
  \(\operatorname{F2.1f.}\)

\(\begin{array}{ll} \{ & (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}\)

\(\operatorname{F2.1f~:~R9d}\)

      \(::\!\)
  \(\operatorname{F2.1g.}\)

\(\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}\)

\(\operatorname{F2.1g~:~R9e}\)

      \(::\!\)
  \(\operatorname{F2.1h.}\)

\(\begin{array}{ll} \{ & (x, y) \in S \times I ~: \\ & \underset{o \in O}{\operatorname{Conj}}~ \underline{((}~ \upharpoonleft \operatorname{Den}(L, x) \upharpoonright ~,~ \upharpoonleft \operatorname{Den}(L, y) \upharpoonright ~\underline{))}^\$ (o) \\ \} & \\ \end{array}\)

\(\operatorname{F2.1h~:~R9f}\)

\(\operatorname{F2.1h~:~D12e}\)

      \(::\!\)
  \(\operatorname{F2.1i.}\)

\(\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}\)

\(\operatorname{F2.1i~:~D12a}\)


  \(\operatorname{Fact~2.2}\)
  \(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
       
  \(\operatorname{F2.2a.}\)

\(\begin{array}{cccl} \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \begin{array}{ccl} \underset{o \in O}{\operatorname{Conj}} \\ & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ & ) & \\ \end{array} \\ & & \} & \\ \end{array}\)

\(\operatorname{F2.2a~:~R11a}\)
  \(::\!\)
  \(\operatorname{F2.2b.}\)

\(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright & = & \upharpoonleft & \{ & (x, y) \in S \times I ~: \\ & & & & \begin{array}{ccl} \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}\)

\(\operatorname{F2.2b~:~R11b}\)

  \(::\!\)
  \(\operatorname{F2.2c.}\)

\(\begin{array}{cccl} \upharpoonleft \operatorname{Der}^L \upharpoonright & = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\ & & & \begin{array}{cccl} \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}\)

\(\operatorname{F2.2c~:~R11c}\)

  \(::\!\)
  \(\operatorname{F2.2d.}\)

\(\begin{array}{cccl} \upharpoonleft \operatorname{Der}^L \upharpoonright & = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\ & & & \begin{array}{cccl} \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}\)

\(\operatorname{F2.2d~:~Log}\)

  \(::\!\)
  \(\operatorname{F2.2e.}\)

\(\begin{array}{cccl} \upharpoonleft \operatorname{Der}^L \upharpoonright & = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\ & & & \begin{array}{ccl} \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}\)

\(\operatorname{F2.2e~:~Log}\)

  \(::\!\)
  \(\operatorname{F2.2f.}\)

\(\begin{array}{cccl} \upharpoonleft \operatorname{Der}^L \upharpoonright & = & \{ & (x, y, z) \in S \times I \times \underline\mathbb{B} ~:~ z = \\ & & & \begin{array}{cll} \underset{o \in O}{\operatorname{Conj}} \\ & \underline{((} & \upharpoonleft \operatorname{Den}^L x \upharpoonright \\ & , & \upharpoonleft \operatorname{Den}^L y \upharpoonright \\ & \underline{))}^\$ & (o) \\ \end{array} \\ & & \} & \\ \end{array}\)

\(\operatorname{F2.2f~:~$~}\)


  \(\operatorname{Fact~2.3}\)
  \(\text{If}\!\) \(L ~\subseteq~ O \times S \times I\)  
  \(\text{then}\!\) \(\text{the following are equivalent:}\!\)  
       
  \(\operatorname{F2.3a.}\)

\(\begin{array}{cccl} \operatorname{Der}^L & = & \{ & (x, y) \in S \times I ~: \\ & & & \begin{array}{ccl} \underset{o \in O}{\operatorname{Conj}} \\ & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ & ) & \\ \end{array} \\ & & \} & \\ \end{array}\)

\(\operatorname{F2.3a~:~R11a}\)
  \(::\!\)
  \(\operatorname{F2.3b.}\)

\(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright (x, y) & = & \downharpoonleft & \underset{o \in O}{\operatorname{Conj}} \\ & & & & \begin{array}{cl} ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ ) & \\ \end{array} \\ & & \downharpoonright & & \\ \end{array}\)

\(\operatorname{F2.3b~:~R11d}\)
  \(::\!\)
  \(\operatorname{F2.3c.}\)

\(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright (x, y) & = & \underset{o \in O}{\operatorname{Conj}} \\ & & & \begin{array}{ccl} \downharpoonleft & ( & \upharpoonleft \operatorname{Den}^L x \upharpoonright (o) \\ & = & \upharpoonleft \operatorname{Den}^L y \upharpoonright (o) \\ & ) & \\ \downharpoonright & & \\ \end{array} \\ & & & \\ \end{array}\)

\(\operatorname{F2.3c~:~Log}\)

  \(::\!\)
  \(\operatorname{F2.3d.}\)

\(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright (x, y) & = & \underset{o \in O}{\operatorname{Conj}} \\ & & & \begin{array}{ccl} \downharpoonleft & ( & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, x) \\ & = & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, y) \\ & ) & \\ \downharpoonright & & \\ \end{array} \\ & & & \\ \end{array}\)

\(\operatorname{F2.3d~:~Def}\)
  \(::\!\)
  \(\operatorname{F2.3e.}\)

\(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright (x, y) & = & \underset{o \in O}{\operatorname{Conj}} \\ & & & \begin{array}{cl} \underline{((} & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, x) \\ , & \upharpoonleft \operatorname{Den}^L \upharpoonright (o, y) \\ \underline{))} & \\ \end{array} \\ & & & \\ \end{array}\)

\(\operatorname{F2.3e~:~Log}\)

\(\operatorname{F2.3e~:~D10b}\)

  \(::\!\)
  \(\operatorname{F2.3f.}\)

\(\begin{array}{ccccl} \upharpoonleft \operatorname{Der}^L \upharpoonright (x, y) & = & \underset{o \in O}{\operatorname{Conj}} \\ & & & \begin{array}{cl} \underline{((} & \upharpoonleft L_{OS} \upharpoonright (o, x) \\ , & \upharpoonleft L_{OS} \upharpoonright (o, y) \\ \underline{))} & \\ \end{array} \\ & & & \\ \end{array}\)

\(\operatorname{F2.3f~:~D10a}\)


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 \(L\!\) into a dyadic relation \(\operatorname{Der}(L),\) 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 \(\operatorname{Der}(L)\) be expressed in the following way:

\(\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{))}~.\)

From this may be abstracted a way of composing two dyadic relations that have a domain in common. For example, let \(P \subseteq X \times M\) and \(Q \subseteq M \times Y\) be dyadic relations that have the middle domain \(M\!\) in common. Then we may define a form of composition, notated \(P \circeq Q,\) where \(P \circeq Q ~\subseteq~ X \times Y\) is defined as follows:

\(\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{))}~.\)

Compare this with the usual form of composition, typically notated \(P \circ Q\) and defined as follows:

\(\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)~.\)

Appendices

Logical Translation Rule 1


\(\text{Logical Translation Rule 1}\!\)  
  \(\text{If}\!\)

\(s ~\text{is a sentence about things in the universe X}\)

  \(\text{and}\!\) \(p ~\text{is a proposition} ~:~ X \to \underline\mathbb{B}\)
  \(\text{such that:}\!\)  
  \(\text{L1a.}\!\) \(\downharpoonleft s \downharpoonright ~=~ p\)
  \(\text{then}\!\) \(\text{the following equations hold:}\!\)
  \(\text{L1b}_{00}.\!\)

\(\downharpoonleft \operatorname{false} \downharpoonright\)

\(=\!\) \((~)\) \(=\!\)

\(\underline{0} ~:~ X \to \underline\mathbb{B}\)

  \(\text{L1b}_{01}.\!\) \(\downharpoonleft \operatorname{not}~ s \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright)\) \(=\!\) \((p) ~:~ X \to \underline\mathbb{B}\)
  \(\text{L1b}_{10}.\!\) \(\downharpoonleft s \downharpoonright\) \(=\!\) \(\downharpoonleft s \downharpoonright\) \(=\!\) \(p ~:~ X \to \underline\mathbb{B}\)
  \(\text{L1b}_{11}.\!\) \(\downharpoonleft \operatorname{true} \downharpoonright\) \(=\!\) \(((~))\) \(=\!\) \(\underline{1} ~:~ X \to \underline\mathbb{B}\)


Geometric Translation Rule 1


\(\text{Geometric Translation Rule 1}\!\)  
  \(\text{If}\!\) \(Q \subseteq X\)
  \(\text{and}\!\) \(p ~:~ X \to \underline\mathbb{B}\)
  \(\text{such that:}\!\)  
  \(\text{G1a.}\!\) \(\upharpoonleft Q \upharpoonright ~=~ p\)
  \(\text{then}\!\) \(\text{the following equations hold:}\!\)
  \(\text{G1b}_{00}.\!\)

\(\upharpoonleft \varnothing \upharpoonright\)

\(=\!\) \((~)\) \(=\!\)

\(\underline{0} ~:~ X \to \underline\mathbb{B}\)

  \(\text{G1b}_{01}.\!\) \(\upharpoonleft {}^{_\sim} Q \upharpoonright\) \(=\!\) \((\upharpoonleft Q \upharpoonright)\) \(=\!\) \((p) ~:~ X \to \underline\mathbb{B}\)
  \(\text{G1b}_{10}.\!\) \(\upharpoonleft Q \upharpoonright\) \(=\!\) \(\upharpoonleft Q \upharpoonright\) \(=\!\) \(p ~:~ X \to \underline\mathbb{B}\)
  \(\text{G1b}_{11}.\!\) \(\upharpoonleft X \upharpoonright\) \(=\!\) \(((~))\) \(=\!\) \(\underline{1} ~:~ X \to \underline\mathbb{B}\)


Logical Translation Rule 2


\(\text{Logical Translation Rule 2}\!\)  
  \(\text{If}\!\)

\(s, t ~\text{are sentences about things in the universe}~ X\)

  \(\text{and}\!\) \(p, q ~\text{are propositions} ~:~ X \to \underline\mathbb{B}\)
  \(\text{such that:}\!\)  
  \(\text{L2a.}\!\) \(\downharpoonleft s \downharpoonright ~=~ p \quad \operatorname{and} \quad \downharpoonleft t \downharpoonright ~=~ q\)
  \(\text{then}\!\) \(\text{the following equations hold:}\!\)
  \(\text{L2b}_{0}.\!\)

\(\downharpoonleft \operatorname{false} \downharpoonright\)

\(=\!\) \((~)\) \(=\!\) \((~)\)
  \(\text{L2b}_{1}.\!\) \(\downharpoonleft \operatorname{neither}~ s ~\operatorname{nor}~ t \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright)\) \(=\!\) \((p)(q)\!\)
  \(\text{L2b}_{2}.\!\) \(\downharpoonleft \operatorname{not}~ s ~\operatorname{but}~ t \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright\) \(=\!\) \((p) q\!\)
  \(\text{L2b}_{3}.\!\) \(\downharpoonleft \operatorname{not}~ s \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright)\) \(=\!\) \((p)\!\)
  \(\text{L2b}_{4}.\!\) \(\downharpoonleft s ~\operatorname{and~not}~ t \downharpoonright\) \(=\!\) \(\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright)\) \(=\!\) \(p (q)\!\)
  \(\text{L2b}_{5}.\!\) \(\downharpoonleft \operatorname{not}~ t \downharpoonright\) \(=\!\) \((\downharpoonleft t \downharpoonright)\) \(=\!\) \((q)\!\)
  \(\text{L2b}_{6}.\!\) \(\downharpoonleft s ~\operatorname{or}~ t, ~\operatorname{not~both} \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright)\) \(=\!\) \((p, q)\!\)
  \(\text{L2b}_{7}.\!\) \(\downharpoonleft \operatorname{not~both}~ s ~\operatorname{and}~ t \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright)\) \(=\!\) \((p q)\!\)
  \(\text{L2b}_{8}.\!\) \(\downharpoonleft s ~\operatorname{and}~ t \downharpoonright\) \(=\!\) \(\downharpoonleft s \downharpoonright ~ \downharpoonleft t \downharpoonright\) \(=\!\) \(p q\!\)
  \(\text{L2b}_{9}.\!\) \(\downharpoonleft s ~\operatorname{is~equivalent~to}~ t \downharpoonright\) \(=\!\) \(((\downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright))\) \(=\!\) \(((p, q))\!\)
  \(\text{L2b}_{10}.\!\) \(\downharpoonleft t \downharpoonright\) \(=\!\) \(\downharpoonleft t \downharpoonright\) \(=\!\) \(q\!\)
  \(\text{L2b}_{11}.\!\) \(\downharpoonleft s ~\operatorname{implies}~ t \downharpoonright\) \(=\!\) \((\downharpoonleft s \downharpoonright (\downharpoonleft t \downharpoonright))\) \(=\!\) \((p (q))\!\)
  \(\text{L2b}_{12}.\!\) \(\downharpoonleft s \downharpoonright\) \(=\!\) \(\downharpoonleft s \downharpoonright\) \(=\!\) \(p\!\)
  \(\text{L2b}_{13}.\!\) \(\downharpoonleft s ~\operatorname{is~implied~by}~ t \downharpoonright\) \(=\!\) \(((\downharpoonleft s \downharpoonright) \downharpoonleft t \downharpoonright)\) \(=\!\) \(((p) q)\!\)
  \(\text{L2b}_{14}.\!\) \(\downharpoonleft s ~\operatorname{or}~ t \downharpoonright\) \(=\!\) \(((\downharpoonleft s \downharpoonright)(\downharpoonleft t \downharpoonright))\) \(=\!\) \(((p)(q))\!\)
  \(\text{L2b}_{15}.\!\) \(\downharpoonleft \operatorname{true} \downharpoonright\) \(=\!\) \(((~))\) \(=\!\) \(((~))\)


Geometric Translation Rule 2


\(\text{Geometric Translation Rule 2}\!\)  
  \(\text{If}\!\) \(P, Q \subseteq X\)
  \(\text{and}\!\) \(p, q ~:~ X \to \underline\mathbb{B}\)
  \(\text{such that:}\!\)  
  \(\text{G2a.}\!\) \(\upharpoonleft P \upharpoonright ~=~ p \quad \operatorname{and} \quad \upharpoonleft Q \upharpoonright ~=~ q\)
  \(\text{then}\!\) \(\text{the following equations hold:}\!\)
  \(\text{G2b}_{0}.\!\)

\(\upharpoonleft \varnothing \upharpoonright\)

\(=\!\) \((~)\) \(=\!\) \((~)\)
  \(\text{G2b}_{1}.\!\) \(\upharpoonleft \overline{P} ~\cap~ \overline{Q} \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright)\) \(=\!\) \((p)(q)\!\)
  \(\text{G2b}_{2}.\!\) \(\upharpoonleft \overline{P} ~\cap~ Q \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright\) \(=\!\) \((p) q\!\)
  \(\text{G2b}_{3}.\!\) \(\upharpoonleft \overline{P} \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright)\) \(=\!\) \((p)\!\)
  \(\text{G2b}_{4}.\!\) \(\upharpoonleft P ~\cap~ \overline{Q} \upharpoonright\) \(=\!\) \(\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright)\) \(=\!\) \(p (q)\!\)
  \(\text{G2b}_{5}.\!\) \(\upharpoonleft \overline{Q} \upharpoonright\) \(=\!\) \((\upharpoonleft Q \upharpoonright)\) \(=\!\) \((q)\!\)
  \(\text{G2b}_{6}.\!\) \(\upharpoonleft P ~+~ Q \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright)\) \(=\!\) \((p, q)\!\)
  \(\text{G2b}_{7}.\!\) \(\upharpoonleft \overline{P ~\cap~ Q} \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright)\) \(=\!\) \((p q)\!\)
  \(\text{G2b}_{8}.\!\) \(\upharpoonleft P ~\cap~ Q \upharpoonright\) \(=\!\) \(\upharpoonleft P \upharpoonright ~ \upharpoonleft Q \upharpoonright\) \(=\!\) \(p q\!\)
  \(\text{G2b}_{9}.\!\) \(\upharpoonleft \overline{P ~+~ Q} \upharpoonright\) \(=\!\) \(((\upharpoonleft P \upharpoonright ~,~ \upharpoonleft Q \upharpoonright))\) \(=\!\) \(((p, q))\!\)
  \(\text{G2b}_{10}.\!\) \(\upharpoonleft Q \upharpoonright\) \(=\!\) \(\upharpoonleft Q \upharpoonright\) \(=\!\) \(q\!\)
  \(\text{G2b}_{11}.\!\) \(\upharpoonleft \overline{P ~\cap~ \overline{Q}} \upharpoonright\) \(=\!\) \((\upharpoonleft P \upharpoonright (\upharpoonleft Q \upharpoonright))\) \(=\!\) \((p (q))\!\)
  \(\text{G2b}_{12}.\!\) \(\upharpoonleft P \upharpoonright\) \(=\!\) \(\upharpoonleft P \upharpoonright\) \(=\!\) \(p\!\)
  \(\text{G2b}_{13}.\!\) \(\upharpoonleft \overline{\overline{P} ~\cap~ Q} \upharpoonright\) \(=\!\) \(((\upharpoonleft P \upharpoonright) \upharpoonleft Q \upharpoonright)\) \(=\!\) \(((p) q)\!\)
  \(\text{G2b}_{14}.\!\) \(\upharpoonleft P ~\cup~ Q \upharpoonright\) \(=\!\) \(((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright))\) \(=\!\) \(((p)(q))\!\)
  \(\text{G2b}_{15}.\!\) \(\upharpoonleft X \upharpoonright\) \(=\!\) \(((~))\) \(=\!\) \(((~))\)


Document History

| 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