MyWikiBiz

Changes

User:Jon Awbrey/SCRATCHPAD (view source)

Revision as of 01:36, 4 December 2011

115,761 bytes removed ,  01:36, 4 December 2011
→‎Examples
Line 16: Line 16:     
==Epigraph Formats==
 
==Epigraph Formats==
 +
 +
<br>
 +
 +
{| cellpadding="2" cellspacing="2" width="100%"
 +
| width="60%" | &nbsp;
 +
| width="40%" |
 +
'Tis a derivative from me to mine,<br>
 +
And only that I stand for.
 +
|-
 +
| height="50px" | &nbsp;
 +
| valign="top"  | &mdash; ''Winter's Tale'', 3.2.43&ndash;44
 +
|}
    
<br>
 
<br>
Line 89: Line 101:  
| align="right" | &mdash; Rousseau, ''Emile, or On Education'', [Rou-1, 34&ndash;35]
 
| align="right" | &mdash; Rousseau, ''Emile, or On Education'', [Rou-1, 34&ndash;35]
 
|}
 
|}
 +
 +
<br>
 +
 +
==Division Styles==
 +
 +
<br>
 +
 +
<div class="references-small">
 +
# Able
 +
# Baker
 +
# Charlie
 +
</div>
 +
 +
<br>
 +
 +
<font face="georgia">
 +
# Able
 +
# Baker
 +
# Charlie
 +
</font>
    
<br>
 
<br>
Line 96: Line 128:  
<br>
 
<br>
   −
{| align="center" cellpadding="0" cellspacing="0" width="90%"
+
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
 
|
 
|
 
<p>Now, I ask, how is it that anything can be done with a symbol, without reflecting upon the conception, much less imagining the object that belongs to it?  It is simply because the symbol has acquired a nature, which may be described thus, that when it is brought before the mind certain principles of its use &mdash; whether reflected on or not &mdash; by association immediately regulate the action of the mind;  and these may be regarded as laws of the symbol itself which it cannot ''as a symbol'' transgress.  (Peirce, CE 1, 173).</p>
 
<p>Now, I ask, how is it that anything can be done with a symbol, without reflecting upon the conception, much less imagining the object that belongs to it?  It is simply because the symbol has acquired a nature, which may be described thus, that when it is brought before the mind certain principles of its use &mdash; whether reflected on or not &mdash; by association immediately regulate the action of the mind;  and these may be regarded as laws of the symbol itself which it cannot ''as a symbol'' transgress.  (Peirce, CE 1, 173).</p>
Line 178: Line 210:     
==Ordered List Formats==
 
==Ordered List Formats==
 +
 +
===Simple===
 +
 +
<ol style="list-style-type:decimal">
 +
  <li>Item 1</li>
 +
    <ol style="list-style-type:lower-alpha">
 +
      <li>Item a</li>
 +
      <li>Item b</li>
 +
      <li>Item c</li>
 +
    </ol>
 +
  <li>Item 2</li>
 +
    <ol style="list-style-type:lower-latin">
 +
      <li>Item a</li>
 +
      <li>Item b</li>
 +
      <li>Item c</li>
 +
    </ol>
 +
  <li>Item 3</li>
 +
</ol>
 +
 +
===Complex===
    
<ol style="list-style-type:decimal">
 
<ol style="list-style-type:decimal">
Line 204: Line 256:  
   <li>Item 3</li>
 
   <li>Item 3</li>
 
</ol>
 
</ol>
 +
 +
===Examples===
 +
 +
====Example 1====
 +
 +
In the present case, one can observe the possibility that the author is suggesting the following analogies:
 +
 +
<ol style="list-style-type:decimal">
 +
 +
<li><p>One analogy says that authoring a text is like piloting a vehicle.  This can be written in either one of two ways.</p></li>
 +
 +
<ol style="list-style-type:lower-alpha">
 +
 +
<li><p>Poet / Poem  =  Pilot / Boat.</p></li>
 +
<li><p>Poet / Pilot  =  Poem / Boat.</p></li>
 +
<li><p>Pilot / Poet  =  Boat / Poem.</p></li>
 +
 +
</ol>
 +
 +
<li>&hellip;</li>
 +
 +
</ol>
 +
 +
====Example 2====
 +
 +
In this way, an epitext can serve a couple of functions within a text:
 +
 +
<ol style="list-style-type:decimal">
 +
 +
<li><p>The epitext maintains an internal model of the informal context, the actual, intended, or likely "context of interpretation" (COI), or the typical "situation of communication" (SOC) that prevails in a given society of interpretive agents.  It does this by preserving a constant but gentle reminder of the type of text that ultimately demands to be understood within this social context.  In other words, it represents its social context in terms of its ideals, [??? the expectation that contains it dialogue between the epitext helps to provides an image of the dialogue that ???]</p></li>
 +
 +
<li><p>The epitext and the text are in a relation, analogous to a dialogue, that mirrors the relation of the text itself to its casual, informal, or social context.  In general, the analogy can be set up in either one of two ways, and can shift its sense from moment to moment:</p></li>
 +
 +
<ol style="list-style-type:lower-latin">
 +
 +
<li><p>Epitext : Text :: Context : Text.  Here, the epitext plays the part of common expectations, generic ideals, or social norms that are invoked in the process of communication.</p></li>
 +
 +
<li><p>Epitext : Text :: Text : Context.  Here, the epitext gives vent to the individual conceits, idiosyncratic caprices, or whims of the moment that are stirred up by the process of communication.</p></li>
 +
 +
</ol></ol>
 +
 +
====Example 3====
 +
 +
The pragmatic idea about phenomena is that all phenomena are signs of significant objects, except for the ones that are not.  In effect, all phenomena are meant to appear before the court of significance and are deemed by their very nature to be judged as signs of potential objects.  Depending on how one chooses to say it, the results of this evaluation can be rendered in one of the following ways:
 +
 +
<ol style="list-style-type:decimal">
 +
 +
<li><p>Some phenomena are in fact signs of significant objects.  That is, they turn out to exist in a certain relation, one that is formally identical to a sign relation, wherein they denote objects that are important to the agent in question, an agent that thereby becomes the interpreter of these signs.</p></li>
 +
 +
<li><p>Some phenomena fail to be signs of significant objects, however much they initially appear to be.  In this event, the failure can be accounted for in either one of two ways:</p></li>
 +
 +
<ol style="list-style-type:lower-latin">
 +
 +
<li><p>Some phenomena can fail to be signs of any objects at all.  This amounts to saying that what appears is not really a sign at all, not really a sign of any object at all.</p></li>
 +
 +
<li><p>All phenomena are signs in some sense, even if only granted a default, nominal, or token designation as signs, but some signs still fail to qualify as signs of significant objects, because the objects they signify are not important to the agents in question.</p></li>
 +
 +
</ol></ol>
 +
 +
====Example 4====
 +
 +
In the pragmatic theory of signs it is often said, &ldquo;The question of the interpreter reduces to the question of the interpretant.&rdquo;  If this is true then it means that questions about the special interpreters that are designated to serve as the writer and the reader of a text are reducible to questions about the particular sign relations that independently and jointly define these two interpreters and their process of communication.  The assumptions and the implications that are involved in this maxim are best explained by retracing the analysis that leads to this reduction, setting it out in the following stages:
 +
 +
<ol style="list-style-type:decimal">
 +
 +
<li><p>By way of setting up the question of the interpreter, it needs to be noted that it can be asked in any one of several modalities.  These are commonly referred to under a variety of different names, for instance:</p></li>
 +
 +
<ol style="list-style-type:lower-alpha">
 +
 +
<li><p>What may be:  the "prospective" or the "imaginative";<br>
 +
also:  the contingent, inquisitive, interrogative, optional, provisional, speculative, or "possible on some condition".</p></li>
 +
 +
<li><p>What is:  the "descriptive" or the "indicative";<br>
 +
also:  the actual, apparent, definite, empirical, existential, experiential, factual, phenomenal, or "evident at some time".</p></li>
 +
 +
<li><p>What must be:  the "prescriptive" or the "imperative";<br>
 +
also:  the injunctive, intentional, normative, obligatory, optative, prerequisite, or "necessary to some purpose".</p></li>
 +
 +
</ol></ol>
 +
 +
It is important to recognize that these lists refer to modes of judgment, not the results of the judgments themselves.  Accordingly, they conflate under single headings the particular issues that remain to be sorted out through the performance of the appropriate judgments, for instance, the difference between an apparent fact and a genuine fact.  In general, it is a difficult question what sorts of relationships exist among these modalities and what sorts of orderings are logically or naturally the best for organizing them in the mind.  Here, they are given in one of the possible types of logical ordering, based on the idea that a thing must be possible before it can become actual, and that it must become actual (at some point in time) in order to qualify as being necessary.  That is, being necessary implies being actual at some time or another, and being actual implies being possible in the first place.  This amounts to thinking that something must be added to a condition of possibility in order to achieve a state of actuality, and that something must be added to a state of actuality in order to acquire a status of necessity.
 +
 +
All of this notwithstanding, it needs to be recognized that other types of logical arrangement can be motivated on other grounds.  For example, there are good reasons to think that all of one's notions of possibility are in fact abstracted from one's actual experiences, making actuality prior in some empirically natural sense to the predicates of possibility.  Since a plausible heuristic organization is all that is needed for now, this is one of those questions that can be left open until a later time.
 +
 +
<ol style="list-style-type:decimal" start="2">
 +
 +
<li><p>Taking this setting as sufficiently well understood and keeping these modalities of inquiry in mind, the analysis proper can begin.  Any question about the character of the interpreter that is acting in a situation can be identified with a question about the nature of the process of interpretation that is taking place under the corresponding conditions.</p></li>
 +
 +
<li><p>Any question about the nature of the process of interpretation that is taking place can be identified with a question about the properties of the interpretant that follows on a given sign.  This is a question about the interpretant that is associated with a sign, in one of several modalities and as contingent on the total context.</p></li>
 +
 +
</ol>
 +
 +
==Outline Formats==
 +
 +
<br>
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
| width="1%" | <big>&bull;</big>
 +
| colspan="3" | '''Example 1.  Modus Ponens'''
 +
|-
 +
| &nbsp;
 +
| width="1%" | &nbsp;
 +
| colspan="2" | ''Information Reducing Inference''
 +
|-
 +
| &nbsp;
 +
| &nbsp;
 +
| width="1%" | &nbsp;
 +
|
 +
<math>\begin{array}{l}
 +
~ p \Rightarrow q
 +
\\
 +
~ p
 +
\\
 +
\overline{~~~~~~~~~~~~~~~}
 +
\\
 +
~ q
 +
\end{array}</math>
 +
|-
 +
| &nbsp;
 +
| &nbsp;
 +
| colspan="2" | ''Information Preserving Inference''
 +
|-
 +
| &nbsp;
 +
| &nbsp;
 +
| &nbsp;
 +
|
 +
<math>\begin{array}{l}
 +
~ p \Rightarrow q
 +
\\
 +
~ p
 +
\\
 +
=\!=\!=\!=\!=\!=\!=\!=
 +
\\
 +
~ p ~ q
 +
\end{array}</math>
 +
|}
 +
 +
<br>
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
| width="1%" | <big>&bull;</big>
 +
| colspan="3" | '''Example 2.  Transitivity'''
 +
|-
 +
| &nbsp;
 +
| width="1%" | &nbsp;
 +
| colspan="2" | ''Information Reducing Inference''
 +
|-
 +
| &nbsp;
 +
| &nbsp;
 +
| width="1%" | &nbsp;
 +
|
 +
<math>\begin{array}{l}
 +
~ p \le q
 +
\\
 +
~ q \le r
 +
\\
 +
\overline{~~~~~~~~~~~~~~~}
 +
\\
 +
~ p \le r
 +
\end{array}</math>
 +
|-
 +
| &nbsp;
 +
| &nbsp;
 +
| colspan="2" | ''Information Preserving Inference''
 +
|-
 +
| &nbsp;
 +
| &nbsp;
 +
| &nbsp;
 +
|
 +
<math>\begin{array}{l}
 +
~ p \le q
 +
\\
 +
~ q \le r
 +
\\
 +
=\!=\!=\!=\!=\!=\!=\!=
 +
\\
 +
~ p \le q \le r
 +
\end{array}</math>
 +
|}
 +
 +
<br>
 +
 +
{| align="center" cellpadding="4" width="90%"
 +
| <big>&bull;</big>
 +
| colspan="3" | '''Transitive Law''' (Implicational Inference)
 +
|-
 +
| width="1%" | &nbsp;
 +
| width="1%" | &nbsp;
 +
| colspan="2" |
 +
<math>\begin{array}{l}
 +
~ p \le q
 +
\\
 +
~ q \le r
 +
\\
 +
\overline{~~~~~~~~~~~~~~~}
 +
\\
 +
~ p \le r
 +
\end{array}</math>
 +
|-
 +
| valign="top" | <big>&bull;</big>
 +
| colspan="3" | By itself, the information <math>p \le q</math> would reduce our uncertainty from <math>\log 8\!</math> bits to <math>\log 6\!</math> bits.
 +
|-
 +
| valign="top" | <big>&bull;</big>
 +
| colspan="3" | By itself, the information <math>q \le r</math> would reduce our uncertainty from <math>\log 8\!</math> bits to <math>\log 6\!</math> bits.
 +
|-
 +
| valign="top" | <big>&bull;</big>
 +
| colspan="3" | By itself, the information <math>p \le r</math> would reduce our uncertainty from <math>\log 8\!</math> bits to <math>\log 6\!</math> bits.
 +
|}
 +
 +
<br>
 +
 +
{| align="center" cellpadding="4" width="90%"
 +
| <big>&bull;</big>
 +
| colspan="3" | '''Transitive Law''' (Equational Inference)
 +
|-
 +
| width="1%" | &nbsp;
 +
| width="1%" | &nbsp;
 +
| colspan="2" |
 +
<math>\begin{array}{l}
 +
~ p \le q
 +
\\
 +
~ q \le r
 +
\\
 +
=\!=\!=\!=\!=\!=\!=\!=
 +
\\
 +
~ p \le q \le r
 +
\end{array}</math>
 +
|-
 +
| valign="top" | <big>&bull;</big>
 +
| colspan="3" | The contents and the measures of information that are associated with the propositions <math>p \le q</math> and <math>q \le r</math> are the same as before.
 +
|-
 +
| valign="top" | <big>&bull;</big>
 +
| colspan="3" | On its own, the information <math>p \le q \le r</math> would reduce our uncertainty from log(8) = 3 bits to log(4) = 2 bits, a reduction of 1 bit.
 +
|}
 +
 +
<br>
    
==Mathematical Symbols==
 
==Mathematical Symbols==
   −
{| cellpadding="4"
+
{| cellpadding="8"
 +
| <math>-<\!</math> || <code>-<</code>
 +
|-
 +
| <math>-\!<</math> || <code>-\!<</code>
 +
|-
 +
| <math>-\!\!<</math> || <code>-\!\!<</code>
 +
|-
 +
| <math>-\!\!\!<</math> || <code>-\!\!\!<</code>
 +
|-
 
| <math>\curlyvee</math> || <code>\curlyvee</code>
 
| <math>\curlyvee</math> || <code>\curlyvee</code>
 
|-
 
|-
Line 223: Line 519:  
|-
 
|-
 
| <math>\colon\!\gtrdot</math>  || <code>\colon\!\gtrdot</code>
 
| <math>\colon\!\gtrdot</math>  || <code>\colon\!\gtrdot</code>
 +
|-
 +
| <math>\And</math> || <code>\And</code>
 +
|-
 +
| <math>\dagger</math> || <code>\dagger</code>
 +
|-
 +
| <math>\ddagger</math> || <code>\ddagger</code>
 +
|-
 +
| <math>\lVert</math> || <code>\lVert</code>
 +
|-
 +
| <math>\rVert</math> || <code>\rVert</code>
 +
|-
 +
| <math>\parallel</math> || <code>\parallel</code>
 +
|-
 +
| <math>\P</math> || <code>\P</code>
 +
|-
 +
| <math>\S</math> || <code>\S</code>
 
|-
 
|-
 
| <math>$</math> || <code>$</code> || NB.  Idiosyntax of WikiTeX
 
| <math>$</math> || <code>$</code> || NB.  Idiosyntax of WikiTeX
Line 228: Line 540:  
| <math>$\!</math> || <code>$\!</code> || NB.  Idiosyntax of WikiTeX
 
| <math>$\!</math> || <code>$\!</code> || NB.  Idiosyntax of WikiTeX
 
|-
 
|-
−
| <math>\$</math> || <code>\$</code>
+
| <math>\$</math> || <code>\$</code> || NB.  Standard Syntax in LaTeX
 +
|-
 +
|}
 +
 
 +
{| cellpadding="8"
 +
| <math>\mathfrak{g}_{\dagger\ddagger} \, ^\dagger\mathit{l}_\parallel \, ^\parallel\mathrm{w} \, ^\ddagger\mathrm{h}</math>
 +
|-
 +
| <math>\mathfrak{g}_{\dagger\ddagger} {}^\dagger\mathit{l}_\parallel {}^\parallel\mathrm{w} {}^\ddagger\mathrm{h}</math>
 +
|-
 +
| <math>\mathfrak{g}_{\dagger\ddagger} {}^\dagger\!\mathit{l}_\parallel {}^\parallel\!\mathrm{w} {}^\ddagger\!\mathrm{h}</math>
 
|}
 
|}
   Line 255: Line 576:  
\texttt{d}^\texttt{2} \texttt{x}  \\
 
\texttt{d}^\texttt{2} \texttt{x}  \\
 
\end{array}</math>
 
\end{array}</math>
 +
 +
<br>
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
| <math>\texttt{uv~(du~dv) ~+~ u(v)~(du (dv)) ~+~ (u)v~((du) dv) ~+~ (u)(v)~((du)(dv))}</math>
 +
|}
 +
 +
<br>
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
| <math>\texttt{uv} \cdot \texttt{(du~dv)} + \texttt{u(v)} \cdot \texttt{(du (dv))} + \texttt{(u)v} \cdot \texttt{((du) dv)} + \texttt{(u)(v)} \cdot \texttt{((du)(dv))}</math>
 +
|}
    
<br>
 
<br>
Line 323: Line 656:     
<br>
 
<br>
 +
 +
==Examples of Logical Orbits==
 +
 +
===Version 1===
 +
 +
{| align="center" cellpadding="8" style="text-align:center"
 +
|
 +
<math>\begin{array}{ccc}
 +
\texttt{u}' & = & \texttt{((u)(v))}
 +
\\
 +
\texttt{v}' & = & \texttt{((u,~v))}
 +
\end{array}</math>
 +
|-
 +
|
 +
<math>\begin{matrix}
 +
\text{Orbit 1}
 +
\\
 +
\text{Initial Point :}~ (u, v) = (1, 1)
 +
\end{matrix}</math>
 +
|-
 +
|
 +
<math>\begin{array}{c|cc}
 +
t &  u &  v \\
 +
\\
 +
0 &  1 &  1 \\
 +
1 &  1 &  1 \\
 +
2 & '' & '' \\
 +
\end{array}</math>
 +
|-
 +
|
 +
<math>\begin{matrix}
 +
\text{Orbit 2}
 +
\\
 +
\text{Initial Point :}~ (u, v) = (0, 0)
 +
\end{matrix}</math>
 +
|-
 +
|
 +
<math>\begin{array}{c|cc}
 +
t &  u &  v \\
 +
\\
 +
0 &  0 &  0 \\
 +
1 &  0 &  1 \\
 +
2 &  1 &  0 \\
 +
3 &  1 &  0 \\
 +
4 & '' & '' \\
 +
\end{array}</math>
 +
|}
 +
 +
===Version 2===
 +
 +
{| align="center" cellpadding="8" style="text-align:center"
 +
|-
 +
| <math>\text{Orbit 1. Intitial Point :}~ (u, v) = (1, 1)</math>
 +
|-
 +
|
 +
<math>\begin{array}{c|cc|cc|cc|cc|cc|c}
 +
t &  u &  v & du & dv & d^2 u & d^2 v & d^3 u & d^3 v & d^4 u & d^4 v & \ldots \\
 +
\\
 +
0 &  1 &  1 &  0 &  0 &    0 &    0 &    0 &    0 &    0 &    0 & \ldots \\
 +
1 &  1 &  1 &  0 &  0 &    0 &    0 &    0 &    0 &    0 &    0 & \ldots \\
 +
4 & '' & '' & '' & '' &    '' &    '' &    '' &    '' &    '' &    '' & \ldots \\
 +
\end{array}</math>
 +
|-
 +
| <math>\text{Orbit 2. Intitial Point :}~ (u, v) = (0, 0)</math>
 +
|-
 +
|
 +
<math>\begin{array}{c|cc|cc|cc|cc|cc|c}
 +
t &  u &  v & du & dv & d^2 u & d^2 v & d^3 u & d^3 v & d^4 u & d^4 v & \ldots \\
 +
\\
 +
0 &  0 &  0 &  0 &  1 &    1 &    0 &    0 &    1 &    1 &    0 & \ldots \\
 +
1 &  0 &  1 &  1 &  1 &    1 &    1 &    1 &    1 &    1 &    1 & \ldots \\
 +
2 &  1 &  0 &  0 &  0 &    0 &    0 &    0 &    0 &    0 &    0 & \ldots \\
 +
3 &  1 &  0 &  0 &  0 &    0 &    0 &    0 &    0 &    0 &    0 & \ldots \\
 +
4 & '' & '' & '' & '' &    '' &    '' &    '' &    '' &    '' &    '' & \ldots \\
 +
\end{array}</math>
 +
|}
 +
 +
===Version 3===
 +
 +
{| align="center" cellpadding="8" style="text-align:center"
 +
| <math>\text{Orbit 1}\!</math>
 +
|-
 +
|
 +
<math>\begin{array}{c|cc|cc|}
 +
t &  u &  v & du & dv \\[8pt]
 +
0 &  1 &  1 &  0 &  0 \\
 +
1 & '' & '' & '' & '' \\
 +
\end{array}</math>
 +
|-
 +
| &nbsp;
 +
|-
 +
| <math>\text{Orbit 2}\!</math>
 +
|-
 +
|
 +
<math>\begin{array}{c|cc|cc|cc|}
 +
t &  u &  v & du & dv & d^2 u & d^2 v \\[8pt]
 +
0 &  0 &  0 &  0 &  1 &    1 &    0 \\
 +
1 &  0 &  1 &  1 &  1 &    1 &    1 \\
 +
2 &  1 &  0 &  0 &  0 &    0 &    0 \\
 +
3 & '' & '' & '' & '' &    '' &    '' \\
 +
\end{array}</math>
 +
|}
 +
 +
==Type Markers==
 +
 +
===Composer P===
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{l}
 +
((x \underset{A}{:} ~y \overset{B}{\underset{A}{:}}) \underset{B}{:} ~z \overset{C}{\underset{B}{:}}) \underset{C}{:}
 +
\end{array}</math>
 +
|}
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{l}
 +
((x \overset{A}{:} ~y \overset{B}{\underset{A}{:}}) \overset{B}{:} ~z \overset{C}{\underset{B}{:}}) \overset{C}{:}
 +
\end{array}</math>
 +
|}
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{l}
 +
((x \overset{A}{\Uparrow} ~y \overset{B}{\underset{A}{\Uparrow}}) \overset{B}{\Uparrow} ~z \overset{C}{\underset{B}{\Uparrow}}) \overset{C}{\Uparrow}
 +
\end{array}</math>
 +
|}
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{l}
 +
((x \underset{A}{\Downarrow} ~y \overset{A}{\underset{B}{\Downarrow}}) \underset{B}{\Downarrow} ~z \overset{B}{\underset{C}{\Downarrow}}) \underset{C}{\Downarrow}
 +
\end{array}</math>
 +
|}
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{l}
 +
((x \overset{ }{\underset{A}{\Downarrow}} ~
 +
  y \overset{A}{\underset{B}{\Downarrow}}
 +
  ) \overset{ }{\underset{B}{\Downarrow}} ~
 +
  z \overset{B}{\underset{C}{\Downarrow}}
 +
  ) \overset{ }{\underset{C}{\Downarrow}}
 +
\\ \\
 +
=
 +
\\ \\
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
(y \overset{A}{\underset{B}{\Downarrow}} ~
 +
(z \overset{B}{\underset{C}{\Downarrow}} ~
 +
P \overset{B \Rightarrow C}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}}
 +
) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}}
 +
) \overset{A}{\underset{C}{\Downarrow}}
 +
) \overset{ }{\underset{C}{\Downarrow}}
 +
\end{array}</math>
 +
|}
 +
 +
===Transposer T===
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{l}
 +
(y \overset{ }{\underset{B}{\Downarrow}} ~
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}
 +
) \overset{B}{\underset{C}{\Downarrow}}
 +
) \overset{ }{\underset{C}{\Downarrow}}
 +
\\ \\
 +
=
 +
\\ \\
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
(y \overset{ }{\underset{B}{\Downarrow}} ~
 +
(z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~
 +
T \overset{A \Rightarrow (B \Rightarrow C)}{\underset{B \Rightarrow (A \Rightarrow C)}{\Downarrow}}
 +
) \overset{B}{\underset{A \Rightarrow C}{\Downarrow}}
 +
) \overset{A}{\underset{C}{\Downarrow}}
 +
) \overset{ }{\underset{C}{\Downarrow}}
 +
\end{array}</math>
 +
|}
 +
 +
===Proof Example===
 +
 +
{| align="center" cellpadding="8" width="90%"
 +
|
 +
<math>\begin{array}{l}
 +
(y \overset{ }{\underset{B}{\Downarrow}} ~
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}
 +
) \overset{B}{\underset{C}{\Downarrow}}
 +
) \overset{ }{\underset{C}{\Downarrow}}
 +
\\ \\
 +
=
 +
\\ \\
 +
((x \overset{ }{\underset{A}{\Downarrow}} ~
 +
(y \overset{ }{\underset{B}{\Downarrow}} ~
 +
  K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}}
 +
  ) \overset{A}{\underset{B}{\Downarrow}}
 +
  ) \overset{ }{\underset{B}{\Downarrow}} ~
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
  z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}}
 +
  ) \overset{B}{\underset{C}{\Downarrow}}
 +
  ) \overset{ }{\underset{C}{\Downarrow}}
 +
\\ \\
 +
=
 +
\\ \\
 +
(x \overset{ }{\underset{A}{\Downarrow}} ~
 +
((y \overset{ }{\underset{B}{\Downarrow}} ~
 +
  K \overset{B}{\underset{A \Rightarrow B}{\Downarrow}}
 +
  ) \overset{A}{\underset{B}{\Downarrow}} ~
 +
(z \overset{A}{\underset{B \Rightarrow C}{\Downarrow}} ~
 +
  S \overset{A \Rightarrow (B \Rightarrow C)}{\underset{(A \Rightarrow B) \Rightarrow (A \Rightarrow C)}{\Downarrow}}
 +
  ) \overset{A \Rightarrow B}{\underset{A \Rightarrow C}{\Downarrow}}
 +
  ) \overset{A}{\underset{C}{\Downarrow}}
 +
  ) \overset{ }{\underset{C}{\Downarrow}}
 +
\\ \\
 +
=
 +
\\ \\
 +
\ldots
 +
\end{array}</math>
 +
|}
    
==Over And Under Setting==
 
==Over And Under Setting==
Line 473: Line 1,025:  
                       &                      &  & \} & \\
 
                       &                      &  & \} & \\
 
\end{array}</math>
 
\end{array}</math>
−
  −
<br>
  −
  −
==Box Displays==
  −
  −
===Formal Grammars===
  −
  −
<br>
  −
  −
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
  −
| align="left"  style="border-left:1px solid black;"  width="50%" |
  −
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 1}\!</math>
  −
| align="right" style="border-right:1px solid black;" width="50%" |
  −
<math>\mathfrak{Q} = \varnothing</math>
  −
|-
  −
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
  −
<math>\begin{array}{rcll}
  −
1.
  −
& S
  −
& :>
  −
& m_1 \ = \ ^{\backprime\backprime} \operatorname{~} ^{\prime\prime}
  −
\\
  −
2.
  −
& S
  −
& :>
  −
& p_j, \, \text{for each} \, j \in J
  −
\\
  −
3.
  −
& S
  −
& :>
  −
& \operatorname{Conc}^0 \ = \ ^{\backprime\backprime\prime\prime}
  −
\\
  −
4.
  −
& S
  −
& :>
  −
& \operatorname{Surc}^0 \ = \ ^{\backprime\backprime} \, \operatorname{()} \, ^{\prime\prime}
  −
\\
  −
5.
  −
& S
  −
& :>
  −
& S^*
  −
\\
  −
6.
  −
& S
  −
& :>
  −
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, S \, \cdot \, ( \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S \, )^* \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
  −
\\
  −
\end{array}</math>
  −
|}
  −
  −
<br>
  −
  −
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
  −
| align="left"  style="border-left:1px solid black;"  width="50%" |
  −
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 2}\!</math>
  −
| align="right" style="border-right:1px solid black;" width="50%" |
  −
<math>\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}</math>
  −
|-
  −
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
  −
<math>\begin{array}{rcll}
  −
1.
  −
& S
  −
& :>
  −
& \varepsilon
  −
\\
  −
2.
  −
& S
  −
& :>
  −
& m_1
  −
\\
  −
3.
  −
& S
  −
& :>
  −
& p_j, \, \text{for each} \, j \in J
  −
\\
  −
4.
  −
& S
  −
& :>
  −
& S \, \cdot \, S
  −
\\
  −
5.
  −
& S
  −
& :>
  −
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
  −
\\
  −
6.
  −
& T
  −
& :>
  −
& S
  −
\\
  −
7.
  −
& T
  −
& :>
  −
& T \, \cdot \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S
  −
\\
  −
\end{array}</math>
  −
|}
  −
  −
<br>
  −
  −
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
  −
| align="left"  style="border-left:1px solid black;"  width="50%" |
  −
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 3}\!</math>
  −
| align="right" style="border-right:1px solid black;" width="50%" |
  −
<math>\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, F \, ^{\prime\prime}, \, ^{\backprime\backprime} \, R \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}</math>
  −
|-
  −
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
  −
<math>\begin{array}{rcll}
  −
1.
  −
& S
  −
& :>
  −
& R
  −
\\
  −
2.
  −
& S
  −
& :>
  −
& F
  −
\\
  −
3.
  −
& S
  −
& :>
  −
& S \, \cdot \, S
  −
\\
  −
4.
  −
& R
  −
& :>
  −
& \varepsilon
  −
\\
  −
5.
  −
& R
  −
& :>
  −
& m_1
  −
\\
  −
6.
  −
& R
  −
& :>
  −
& p_j, \, \text{for each} \, j \in J
  −
\\
  −
7.
  −
& R
  −
& :>
  −
& R \, \cdot \, R
  −
\\
  −
8.
  −
& F
  −
& :>
  −
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
  −
\\
  −
9.
  −
& T
  −
& :>
  −
& S
  −
\\
  −
10.
  −
& T
  −
& :>
  −
& T \, \cdot \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S
  −
\\
  −
\end{array}</math>
  −
|}
  −
  −
<br>
  −
  −
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
  −
| align="left"  style="border-left:1px solid black;"  width="50%" |
  −
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 4}\!</math>
  −
| align="right" style="border-right:1px solid black;" width="50%" |
  −
<math>\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T' \, ^{\prime\prime} \, \}</math>
  −
|-
  −
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
  −
<math>\begin{array}{rcll}
  −
1.
  −
& S
  −
& :>
  −
& \varepsilon
  −
\\
  −
2.
  −
& S
  −
& :>
  −
& S'
  −
\\
  −
3.
  −
& S'
  −
& :>
  −
& m_1
  −
\\
  −
4.
  −
& S'
  −
& :>
  −
& p_j, \, \text{for each} \, j \in J
  −
\\
  −
5.
  −
& S'
  −
& :>
  −
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
  −
\\
  −
6.
  −
& S'
  −
& :>
  −
& S' \, \cdot \, S'
  −
\\
  −
7.
  −
& T
  −
& :>
  −
& \varepsilon
  −
\\
  −
8.
  −
& T
  −
& :>
  −
& T'
  −
\\
  −
9.
  −
& T'
  −
& :>
  −
& T \, \cdot \, ^{\backprime\backprime} \operatorname{,} ^{\prime\prime} \, \cdot \, S
  −
\\
  −
\end{array}</math>
  −
|}
  −
  −
<br>
  −
  −
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
  −
| align="left"  style="border-left:1px solid black;"  width="50%" |
  −
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 5}\!</math>
  −
| align="right" style="border-right:1px solid black;" width="50%" |
  −
<math>\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}</math>
  −
|-
  −
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
  −
<math>\begin{array}{rcll}
  −
1.
  −
& S
  −
& :>
  −
& \varepsilon
  −
\\
  −
2.
  −
& S
  −
& :>
  −
& S'
  −
\\
  −
3.
  −
& S'
  −
& :>
  −
& m_1
  −
\\
  −
4.
  −
& S'
  −
& :>
  −
& p_j, \, \text{for each} \, j \in J
  −
\\
  −
5.
  −
& S'
  −
& :>
  −
& S' \, \cdot \, S'
  −
\\
  −
6.
  −
& S'
  −
& :>
  −
& ^{\backprime\backprime} \, \operatorname{()} \, ^{\prime\prime}
  −
\\
  −
7.
  −
& S'
  −
& :>
  −
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
  −
\\
  −
8.
  −
& T
  −
& :>
  −
& ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime}
  −
\\
  −
9.
  −
& T
  −
& :>
  −
& S'
  −
\\
  −
10.
  −
& T
  −
& :>
  −
& T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime}
  −
\\
  −
11.
  −
& T
  −
& :>
  −
& T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime} \, \cdot \, S'
  −
\\
  −
\end{array}</math>
  −
|}
  −
  −
<br>
  −
  −
{| align="center" cellpadding="12" cellspacing="0" style="border-top:1px solid black" width="90%"
  −
| align="left"  style="border-left:1px solid black;"  width="50%" |
  −
<math>\mathfrak{C} (\mathfrak{P}) : \text{Grammar 6}\!</math>
  −
| align="right" style="border-right:1px solid black;" width="50%" |
  −
<math>\mathfrak{Q} = \{ \, ^{\backprime\backprime} \, S' \, ^{\prime\prime}, \, ^{\backprime\backprime} \, F \, ^{\prime\prime}, \, ^{\backprime\backprime} \, R \, ^{\prime\prime}, \, ^{\backprime\backprime} \, T \, ^{\prime\prime} \, \}</math>
  −
|-
  −
| colspan="2" style="border-top:1px solid black; border-bottom:1px solid black; border-left:1px solid black; border-right:1px solid black" |
  −
<math>\begin{array}{rcll}
  −
1.
  −
& S
  −
& :>
  −
& \varepsilon
  −
\\
  −
2.
  −
& S
  −
& :>
  −
& S'
  −
\\
  −
3.
  −
& S'
  −
& :>
  −
& R
  −
\\
  −
4.
  −
& S'
  −
& :>
  −
& F
  −
\\
  −
5.
  −
& S'
  −
& :>
  −
& S' \, \cdot \, S'
  −
\\
  −
6.
  −
& R
  −
& :>
  −
& m_1
  −
\\
  −
7.
  −
& R
  −
& :>
  −
& p_j, \, \text{for each} \, j \in J
  −
\\
  −
8.
  −
& R
  −
& :>
  −
& R \, \cdot \, R
  −
\\
  −
9.
  −
& F
  −
& :>
  −
& ^{\backprime\backprime} \, \operatorname{()} \, ^{\prime\prime}
  −
\\
  −
10.
  −
& F
  −
& :>
  −
& ^{\backprime\backprime} \, \operatorname{(} \, ^{\prime\prime} \, \cdot \, T \, \cdot \, ^{\backprime\backprime} \, \operatorname{)} \, ^{\prime\prime}
  −
\\
  −
11.
  −
& T
  −
& :>
  −
& ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime}
  −
\\
  −
12.
  −
& T
  −
& :>
  −
& S'
  −
\\
  −
13.
  −
& T
  −
& :>
  −
& T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime}
  −
\\
  −
14.
  −
& T
  −
& :>
  −
& T \, \cdot \, ^{\backprime\backprime} \, \operatorname{,} \, ^{\prime\prime} \, \cdot \, S'
  −
\\
  −
\end{array}</math>
  −
|}
  −
  −
<br>
  −
  −
===Proof Schemata===
  −
  −
====Definition 1====
  −
  −
=====Variant 1=====
  −
  −
<br>
  −
  −
{| align="center" cellpadding="2" 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%"
  −
|- style="height:40px"
  −
| width="2%"  | &nbsp;
  −
| width="18%" | &nbsp;
  −
| width="60%" | &nbsp;
  −
| align="center" width="20%" | <math>\text{Definition 1}\!</math>
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{If}\!</math>
  −
| style="border-top:1px solid black" | <math>Q \subseteq X</math>
  −
| style="border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{such that:}\!</math>
  −
| &nbsp;
  −
| &nbsp;
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{D1a.}\!</math>
  −
| style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q</math>
  −
| align="center" style="border-top:1px solid black" | <math>\forall x \in X</math>
  −
|}
  −
  −
<br>
  −
  −
=====Variant 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:40px; text-align:center"
  −
| width="80%" | &nbsp;
  −
| width="20%" | <math>\text{Definition 1}\!</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>Q ~\subseteq~ X</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{such that:}\!</math>
  −
| &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{D1a.}</math>
  −
| width="60%" style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright (x) ~\Leftrightarrow~ x \in Q</math>
  −
| width="20%" style="border-top:1px solid black; text-align:center" | <math>\forall x \in X</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Rule 1====
  −
  −
<br>
  −
  −
{| align="center" cellpadding="2" 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%"
  −
|- style="height:40px"
  −
| width="2%"  | &nbsp;
  −
| width="18%" | &nbsp;
  −
| width="60%" | &nbsp;
  −
| align="center" width="20%" | <math>\text{Rule 1}\!</math>
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{If}\!</math>
  −
| style="border-top:1px solid black" | <math>Q \subseteq X</math>
  −
| style="border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\upharpoonleft Q \upharpoonright ~:~ X \to \underline\mathbb{B}</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{and if}\!</math>
  −
| <math>x \in X</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{R1a.}\!</math>
  −
| style="border-top:1px solid black" | <math>x \in Q</math>
  −
| style="border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{R1b.}\!</math>
  −
| <math>\upharpoonleft Q \upharpoonright (x)</math>
  −
| &nbsp;
  −
|}
  −
  −
<br>
  −
  −
====Rule 2====
  −
  −
<br>
  −
  −
{| align="center" cellpadding="2" 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%"
  −
|- style="height:40px"
  −
| width="2%"  | &nbsp;
  −
| width="18%" | &nbsp;
  −
| width="60%" | &nbsp;
  −
| align="center" width="20%" | <math>\text{Rule 2}\!</math>
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{If}\!</math>
  −
| style="border-top:1px solid black" | <math>f : X \to \underline\mathbb{B}</math>
  −
| style="border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{and}\!</math>
  −
| <math>x \in X</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{R2a.}\!</math>
  −
| style="border-top:1px solid black" | <math>f(x)\!</math>
  −
| style="border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{R2b.}\!</math>
  −
| <math>f(x) = \underline{1}</math>
  −
| &nbsp;
  −
|}
  −
  −
<br>
  −
  −
====Rule 3====
  −
  −
=====Variant 1=====
  −
  −
<br>
  −
  −
{| align="center" cellpadding="2" 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%"
  −
|- style="height:40px"
  −
| width="2%"  | &nbsp;
  −
| width="18%" | &nbsp;
  −
| width="60%" | &nbsp;
  −
| align="center" style="border-left:1px solid black" width="20%" | <math>\text{Rule 3}\!</math>
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{If}\!</math>
  −
| style="border-top:1px solid black" | <math>Q \subseteq X</math>
  −
| style="border-left:1px solid black; border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{and}\!</math>
  −
| <math>x \in X</math>
  −
| style="border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</math>
  −
| style="border-left:1px solid black" | &nbsp;
  −
|- style="height:36px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{R3a.}\!</math>
  −
| style="border-top:1px solid black" | <math>x \in Q</math>
  −
| style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\text{R3a : R1a}\!</math>
  −
|- style="height:24px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:36px"
  −
| &nbsp;
  −
| <math>\text{R3b.}\!</math>
  −
| <math>\upharpoonleft Q \upharpoonright (x)</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\text{R3b : R1b}\!</math></p>
  −
<p><math>\text{R3b : R2a}\!</math></p>
  −
|- style="height:24px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:36px"
  −
| &nbsp;
  −
| <math>\text{R3c.}\!</math>
  −
| <math>\upharpoonleft Q \upharpoonright (x) = \underline{1}</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\text{R3c : R2b}\!</math>
  −
|}
  −
  −
<br>
  −
  −
=====Variant 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:40px; text-align:center"
  −
| width="80%" | &nbsp;
  −
| width="20%" style="border-left:1px solid black" | <math>\operatorname{Rule~3}</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="60%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{and}\!</math>
  −
| <math>x ~\in~ X</math>
  −
| style="border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &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:40px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R3a.}</math>
  −
| width="60%" style="border-top:1px solid black" | <math>x ~\in~ Q</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R3a~:~R1a}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R3b.}</math>
  −
| <math>\upharpoonleft Q \upharpoonright (x)</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{R3b~:~R1b}</math></p>
  −
<p><math>\operatorname{R3b~:~R2a}</math></p>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R3c.}</math>
  −
| <math>\upharpoonleft Q \upharpoonright (x) ~=~ \underline{1}</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R3c~:~R2b}</math></p>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Corollary 1====
  −
  −
<br>
  −
  −
{| align="center" cellpadding="2" 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%"
  −
|- style="height:40px"
  −
| width="2%"  | &nbsp;
  −
| width="18%" | &nbsp;
  −
| width="60%" | &nbsp;
  −
| align="center" style="border-left:1px solid black" width="20%" |
  −
<math>\text{Corollary 1}\!</math>
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{If}\!</math>
  −
| style="border-top:1px solid black" | <math>Q \subseteq X</math>
  −
| style="border-left:1px solid black; border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{and}\!</math>
  −
| <math>x \in X</math>
  −
| style="border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following statement is true:}\!</math>
  −
| style="border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{C1a.}\!</math>
  −
| style="border-top:1px solid black" |
  −
<math>x \in Q ~\Leftrightarrow~ \upharpoonleft Q \upharpoonright (x) = \underline{1}</math>
  −
| align="center" style="border-left:1px solid black; border-top:1px solid black" |
  −
<math>\text{R3a} \Leftrightarrow \text{R3c}</math>
  −
|}
  −
  −
<br>
  −
  −
====Rule 4====
  −
  −
<br>
  −
  −
{| align="center" cellpadding="2" 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%"
  −
|- style="height:40px"
  −
| width="2%"  | &nbsp;
  −
| width="18%" | &nbsp;
  −
| width="60%" | &nbsp;
  −
| align="center" width="20%" | <math>\text{Rule 4}\!</math>
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{If}\!</math>
  −
| style="border-top:1px solid black" | <math>Q \subseteq X ~\text{is fixed}</math>
  −
| style="border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{and}\!</math>
  −
| <math>x \in X ~\text{is varied}</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| style="border-top:1px solid black" | &nbsp;
  −
| style="border-top:1px solid black" | <math>\text{R4a.}\!</math>
  −
| style="border-top:1px solid black" | <math>x \in Q</math>
  −
| style="border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{R4b.}\!</math>
  −
| <math>\downharpoonleft x \in Q \downharpoonright</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{R4c.}\!</math>
  −
| <math>\downharpoonleft x \in Q \downharpoonright (x)</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{R4d.}\!</math>
  −
| <math>\upharpoonleft Q \upharpoonright (x)</math>
  −
| &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{R4e.}\!</math>
  −
| <math>\upharpoonleft Q \upharpoonright (x) = \underline{1}</math>
  −
| &nbsp;
  −
|}
  −
  −
<br>
  −
  −
===Logical Translation Rule 0===
  −
  −
<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 0}\!</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_j ~\text{is a sentence about things in the universe X}</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{and}\!</math>
  −
| <math>p_j ~\text{is a proposition about things in the universe X}</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{such that:}\!</math>
  −
| &nbsp;
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{L0a.}\!</math>
  −
| <math>\downharpoonleft s_j \downharpoonright ~=~ p_j, ~\text{for all}~ j \in J,</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following equations are true:}\!</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:56px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" | <math>\text{L0b.}\!</math>
  −
| width="20%" style="border-top:1px solid black" |
  −
<math>\downharpoonleft \operatorname{Conc}_j^J s_j \downharpoonright</math>
  −
| width="10%" style="border-top:1px solid black" | <math>=\!</math>
  −
| width="20%" style="border-top:1px solid black" |
  −
<math>\operatorname{Conj}_j^J \downharpoonleft s_j \downharpoonright</math>
  −
| width="10%" style="border-top:1px solid black" | <math>=\!</math>
  −
| width="20%" style="border-top:1px solid black" |
  −
<math>\operatorname{Conj}_j^J p_j</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{L0c.}\!</math>
  −
| <math>\downharpoonleft \operatorname{Surc}_j^J s_j \downharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>\operatorname{Surj}_j^J \downharpoonleft s_j \downharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>\operatorname{Surj}_j^J p_j</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===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>=\!</math>
  −
| <math>((\upharpoonleft P \upharpoonright)(\upharpoonleft Q \upharpoonright))</math>
  −
| <math>=\!</math>
  −
| <math>((p)(q))\!</math>
  −
|- style="height:52px"
  −
| &nbsp;
  −
| align="left" | <math>\text{G2b}_{15}.\!</math>
  −
| <math>\upharpoonleft X \upharpoonright</math>
  −
| <math>=\!</math>
  −
| <math>((~))</math>
  −
| <math>=\!</math>
  −
| <math>((~))</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Value Rule 1===
  −
  −
'''Editing Note.'''  There are several versions of this Rule in the last couple of drafts I can find.  I will try to figure out what's at issue here as I mark them up.
  −
  −
====Variant 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{Value 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="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
  −
| width="84%" style="border-top:1px solid black" | <math>v, w ~\in~ \underline\mathbb{B}</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>^{\backprime\backprime} v = w \, ^{\prime\prime} ~\text{is a sentence about pairs of values}~ (v, w) \in \underline\mathbb{B}^2,</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| &nbsp;
  −
| <math>\downharpoonleft v = w \downharpoonright ~\text{is a proposition} ~:~ \underline\mathbb{B}^2 \to \underline\mathbb{B},</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{and}\!</math>
  −
| <math>\text{the following are identical values in}~ \underline\mathbb{B}:</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:56px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="14%" style="border-top:1px solid black" | <math>\text{V1a.}\!</math>
  −
| width="84%" style="border-top:1px solid black" | <math>\downharpoonleft v = w \downharpoonright (v, w)</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{V1b.}\!</math>
  −
| <math>\downharpoonleft v \Leftrightarrow w \downharpoonright (v, w)</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{V1c.}\!</math>
  −
| <math>\underline{((}~ v ~,~ w ~\underline{))}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Variant 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{Value 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="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
  −
| width="84%" style="border-top:1px solid black" | <math>v, w ~\in~ \underline\mathbb{B}</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:56px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="14%" style="border-top:1px solid black" | <math>\text{V1a.}\!</math>
  −
| width="84%" style="border-top:1px solid black" | <math>v = w\!</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{V1b.}\!</math>
  −
| <math>v \Leftrightarrow w</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{V1c.}\!</math>
  −
| <math>\underline{((}~ v ~,~ w ~\underline{))}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Variant 3====
  −
  −
A rule that allows one to turn equivalent sentences into identical propositions:
  −
  −
{| align="center" cellpadding="8" width="90%"
  −
| <math>(s ~\Leftrightarrow~ t) \quad \Leftrightarrow \quad (\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright)</math>
  −
|}
  −
  −
Consider the following pair of expressions:
  −
  −
{| align="center" cellpadding="8" width="90%"
  −
| <math>\downharpoonleft v ~=~ w \downharpoonright (v, w)</math>
  −
|-
  −
| <math>\downharpoonleft v(x) ~=~ w(x) \downharpoonright (x)</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:48px; text-align:right"
  −
| width="98%" | <math>\text{Value 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="14%" style="border-top:1px solid black" | <math>\text{If}\!</math>
  −
| width="84%" style="border-top:1px solid black" | <math>v, w ~\in~ \underline\mathbb{B}</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are identical values in}~ \underline\mathbb{B}:</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:56px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="14%" style="border-top:1px solid black" | <math>\text{V1a.}\!</math>
  −
| width="84%" style="border-top:1px solid black" | <math>\downharpoonleft v = w \downharpoonright</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{V1b.}\!</math>
  −
| <math>\downharpoonleft v \Leftrightarrow w \downharpoonright</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{V1c.}\!</math>
  −
| <math>\underline{((}~ v ~,~ w ~\underline{))}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Variant 4====
  −
  −
<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{Value 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="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>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{and}\!</math>
  −
| <math>x ~\in~ X</math>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are identical values in}~ \underline\mathbb{B}:</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:56px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="14%" style="border-top:1px solid black" | <math>\text{V1a.}\!</math>
  −
| width="84%" style="border-top:1px solid black" | <math>\downharpoonleft f(x) ~=~ g(x) \downharpoonright</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{V1b.}\!</math>
  −
| <math>\downharpoonleft f(x) ~\Leftrightarrow~ g(x) \downharpoonright</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{V1c.}\!</math>
  −
| <math>\underline{((}~ f(x) ~,~ g(x) ~\underline{))}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Variant 5====
  −
  −
<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{Value 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="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>
  −
|- style="height:48px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are identical propositions on}~ X:</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:56px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="14%" style="border-top:1px solid black" | <math>\text{V1a.}\!</math>
  −
| width="84%" style="border-top:1px solid black" | <math>\downharpoonleft f ~=~ g \downharpoonright</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{V1b.}\!</math>
  −
| <math>\downharpoonleft f ~\Leftrightarrow~ g \downharpoonright</math>
  −
|- style="height:56px"
  −
| &nbsp;
  −
| <math>\text{V1c.}\!</math>
  −
| <math>\underline{((}~ f ~,~ g ~\underline{))}^\$</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Evaluation 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:50px; text-align:right"
  −
| width="98%" | <math>\operatorname{Evaluation~Rule~1}</math>
  −
| width="2%"  | &nbsp;
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:50px"
  −
| 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>f, g ~:~ X \to \underline\mathbb{B}</math>
  −
|- style="height:50px"
  −
| &nbsp;
  −
| <math>\text{and}\!</math>
  −
| <math>x ~\in~ X</math>
  −
|- style="height:50px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:10px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="14%" style="border-top:1px solid black" | &nbsp;
  −
| width="64%" style="border-top:1px solid black" | &nbsp;
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{E1a.}</math>
  −
| <math>f(x) ~=~ g(x)</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{E1a~:~V1a}</math>
  −
|- style="height:20px"
  −
| colspan="3" | &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{E1b.}</math>
  −
| <math>f(x) ~\Leftrightarrow~ g(x)</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{E1b~:~V1b}</math>
  −
|- style="height:20px"
  −
| colspan="3" | &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{E1c.}</math>
  −
| <math>\underline{((}~ f(x) ~,~ g(x) ~\underline{))}</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<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>
  −
  −
===Definition 2===
  −
  −
====Variant 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:40px; text-align:center"
  −
| width="80%" | &nbsp;
  −
| width="20%" | <math>\operatorname{Definition~2}</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>P, Q ~\subseteq~ X</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</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{D2a.}</math>
  −
| width="60%" style="border-top:1px solid black" | <math>P ~=~ Q</math>
  −
| width="20%" style="border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{D2b.}</math>
  −
| <math>x \in P ~\Leftrightarrow~ x \in Q</math>
  −
| align="center" | <math>\forall x \in X</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Variant 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:40px; text-align:center"
  −
| width="80%" | &nbsp;
  −
| width="20%" | <math>\operatorname{Definition~2}</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>P, Q ~\subseteq~ X</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</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{D2a.}</math>
  −
| width="80%" style="border-top:1px solid black" | <math>P ~=~ Q</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{D2b.}</math>
  −
| <math>\overset{X}{\underset{x}{\forall}}~ (x \in P ~\Leftrightarrow~ x \in Q)</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Definition 3===
  −
  −
====Variant 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:40px; text-align:center"
  −
| width="80%" | &nbsp;
  −
| width="20%" | <math>\operatorname{Definition~3}</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>f, g ~:~ X \to Y</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</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{D3a.}</math>
  −
| width="60%" style="border-top:1px solid black" | <math>f ~=~ g</math>
  −
| width="20%" style="border-top:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{D3b.}</math>
  −
| <math>f(x) ~=~ g(x)</math>
  −
| align="center" | <math>\forall x \in X</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Variant 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:40px; text-align:center"
  −
| width="80%" | &nbsp;
  −
| width="20%" | <math>\operatorname{Definition~3}</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>f, g ~:~ X \to Y</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</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{D3a.}</math>
  −
| width="80%" style="border-top:1px solid black" | <math>f ~=~ g</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{D3b.}</math>
  −
| <math>\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Variant 3====
  −
  −
<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~3}</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>f, g ~:~ X \to Y</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</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{D3a.}</math>
  −
| width="80%" style="border-top:1px solid black" | <math>f ~=~ g</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{D3b.}</math>
  −
| <math>\prod_x^X~ (f(x) ~=~ g(x))</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Definition 4===
  −
  −
<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~4}</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>Q ~\subseteq~ X</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are identical subsets of}~ X \times \underline\mathbb{B}:</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{D4a.}</math>
  −
| width="80%" style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{D4b.}</math>
  −
| <math>\{ (x, y) \in X \times \underline\mathbb{B} ~:~ y ~=~ \downharpoonleft x \in Q \downharpoonright</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Definition 5===
  −
  −
====Variant 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:40px; text-align:center"
  −
| width="80%" | &nbsp;
  −
| width="20%" | <math>\operatorname{Definition~5}</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>Q ~\subseteq~ X</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are identical propositions:}\!</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{D5a.}</math>
  −
| width="80%" style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{D5b.}</math>
  −
|
  −
<math>\begin{array}{lcl}
  −
f    & : & X \to \underline\mathbb{B}
  −
\\
  −
f(x) & = & \downharpoonleft x \in Q \downharpoonright \quad (\forall x \in X)
  −
\end{array}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Variant 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:40px; text-align:center"
  −
| width="80%" | &nbsp;
  −
| width="20%" | <math>\operatorname{Definition~5}</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>Q ~\subseteq~ X</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are identical propositions:}\!</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{D5a.}</math>
  −
| width="80%" style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{D5b.}</math>
  −
|
  −
<math>\begin{array}{ccccl}
  −
f & : & X & \to    & \underline\mathbb{B}
  −
\\
  −
f & : & x & \mapsto & \downharpoonleft x \in Q \downharpoonright
  −
\end{array}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
====Variant 3====
  −
  −
<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~5}</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>Q ~\subseteq~ X</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are identical propositions} ~:~ X \to \underline\mathbb{B}</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{D5a.}</math>
  −
| width="80%" style="border-top:1px solid black" | <math>\upharpoonleft Q \upharpoonright</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{D5b.}</math>
  −
| <math>\downharpoonleft x \in Q \downharpoonright</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Definition 6===
  −
  −
<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~6}</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>\text{each string}~ s_j, ~\text{as}~ j ~\text{ranges over the set}~ J,</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| <math>\text{is a sentence about things in the universe}~ X~</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:60px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" | <math>\operatorname{D6a.}</math>
  −
| width="80%" style="border-top:1px solid black" | <math>\overset{J}{\underset{j}{\forall}}~ s_j</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{D6b.}</math>
  −
| <math>\operatorname{Conj}_j^J s_j</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Definition 7===
  −
  −
<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~7}</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>s, t ~\text{are sentences about things in the universe}~ X</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\text{then}\!</math>
  −
| <math>\text{the following are equivalent:}\!</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{D7a.}</math>
  −
| width="80%" style="border-top:1px solid black" | <math>s ~\Leftrightarrow~ t</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{D7b.}</math>
  −
| <math>\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Rule 5===
  −
  −
<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%" style="border-left:1px solid black" | <math>\operatorname{Rule~5}</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="60%" style="border-top:1px solid black" | <math>P, Q ~\subseteq~ X</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &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:40px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R5a.}</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{R5a~:~D2a}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R5b.}</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{R5b~:~D2b}</math></p>
  −
<p><math>\operatorname{R5b~:~D7a}</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{R5c.}</math>
  −
| <math>\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright)</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{R5c~:~D7b}</math></p>
  −
<p><math>\operatorname{R5c~:~\_\_?\_\_}</math></p>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:80px"
  −
| &nbsp;
  −
| <math>\operatorname{R5d.}</math>
  −
|
  −
<math>\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}</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{R5d~:~\_\_?\_\_}</math></p>
  −
<p><math>\operatorname{R5d~:~D5b}</math></p>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R5e.}</math>
  −
| <math>\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R5e~:~D5a}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Rule 6===
  −
  −
<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%" style="border-left:1px solid black" | <math>\operatorname{Rule~6}</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="60%" style="border-top:1px solid black" | <math>f, g ~:~ X \to Y</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &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:40px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R6a.}</math>
  −
| width="60%" style="border-top:1px solid black" | <math>f ~=~ g</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R6a~:~D3a}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R6b.}</math>
  −
| <math>\overset{X}{\underset{x}{\forall}}~ (f(x) ~=~ g(x))</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{R6b~:~D3b}</math></p>
  −
<p><math>\operatorname{R6b~:~D6a}</math></p>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R6c.}</math>
  −
| <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>
  −
  −
===Rule 7===
  −
  −
<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%" style="border-left:1px solid black" | <math>\operatorname{Rule~7}</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="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;
  −
|- style="height:40px"
  −
| &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:40px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R7a.}</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{R7a~:~R6a}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R7b.}</math>
  −
| <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>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R7c.}</math>
  −
| <math>\operatorname{Conj_x^X}~ (p(x) ~=~ q(x))</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{R7c~:~R6c}</math></p>
  −
<p><math>\operatorname{R7c~:~P1a}</math></p>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R7d.}</math>
  −
| <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"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R7e.}</math>
  −
| <math>\operatorname{Conj_x^X}~ \underline{((}~ p(x) ~,~ q(x) ~\underline{))}</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{R7e~:~P1c}</math></p>
  −
<p><math>\operatorname{R7e~:~$1a}</math></p>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R7f.}</math>
  −
| <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>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Rule 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%" style="border-left:1px solid black" | <math>\operatorname{Rule~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="60%" style="border-top:1px solid black" | <math>s, t ~\text{are sentences about things in}~ X</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &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:40px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R8a.}</math>
  −
| 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" |
  −
<math>\operatorname{R8a~:~D7a}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R8b.}</math>
  −
| <math>\downharpoonleft s \downharpoonright ~=~ \downharpoonleft t \downharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{R8b~:~D7b}</math></p>
  −
<p><math>\operatorname{R8b~:~R7a}</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{R8c.}</math>
  −
| <math>\overset{X}{\underset{x}{\forall}}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8c~:~R7b}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R8d.}</math>
  −
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~=~ \downharpoonleft t \downharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8d~:~R7c}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R8e.}</math>
  −
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft s \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft t \downharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8e~:~R7d}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R8f.}</math>
  −
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright (x) ~,~ \downharpoonleft t \downharpoonright (x) ~\underline{))}</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8f~:~R7e}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R8g.}</math>
  −
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \downharpoonleft s \downharpoonright ~,~ \downharpoonleft t \downharpoonright ~\underline{))}^\$ (x)</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R8g~:~R7f}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Rule 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%" style="border-left:1px solid black" | <math>\operatorname{Rule~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="60%" style="border-top:1px solid black" | <math>P, Q ~\subseteq~ X</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &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:40px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R9a.}</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{R9a~:~R5a}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R9b.}</math>
  −
| <math>\upharpoonleft P \upharpoonright ~=~ \upharpoonleft Q \upharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{R9b~:~R5e}</math></p>
  −
<p><math>\operatorname{R9b~:~R7a}</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{R9c.}</math>
  −
| <math>\overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9c~:~R7b}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R9d.}</math>
  −
| <math>\operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9d~:~R7c}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R9e.}</math>
  −
| <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>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R9f.}</math>
  −
| <math>\operatorname{Conj_x^X}~ \underline{((}~ \upharpoonleft P \upharpoonright (x) ~,~ \upharpoonleft Q \upharpoonright (x) ~\underline{))}</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R9f~:~R7e}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R9g.}</math>
  −
| <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>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Rule 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%" style="border-left:1px solid black" | <math>\operatorname{Rule~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="60%" style="border-top:1px solid black" | <math>P, Q ~\subseteq~ X</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &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: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;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &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;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R10c.}</math>
  −
| <math>\downharpoonleft x \in P \downharpoonright ~=~ \downharpoonleft x \in Q \downharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10c~:~R8b}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <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;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R10e.}</math>
  −
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~=~ \downharpoonleft x \in Q \downharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10e~:~R8d}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R10f.}</math>
  −
| <math>\operatorname{Conj_x^X}~ (\downharpoonleft x \in P \downharpoonright (x) ~\Leftrightarrow~ \downharpoonleft x \in Q \downharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R10f~:~R8e}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &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>
  −
  −
===Rule 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%" style="border-left:1px solid black" | <math>\operatorname{Rule~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="60%" style="border-top:1px solid black" | <math>Q ~\subseteq~ X</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black" | &nbsp;
  −
|- style="height:40px"
  −
| &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:40px"
  −
| width="2%"  style="border-top:1px solid black" | &nbsp;
  −
| width="18%" style="border-top:1px solid black" | <math>\operatorname{R11a.}</math>
  −
| width="60%" style="border-top:1px solid black" | <math>Q ~=~ \{ x \in X ~:~ s \}</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{R11a~:~R5a}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R11b.}</math>
  −
| <math>\upharpoonleft Q \upharpoonright ~=~ \upharpoonleft \{ x \in X ~:~ s \} \upharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11b~:~R5e}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R11c.}</math>
  −
|
  −
<math>\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}</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;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R11d.}</math>
  −
|
  −
<math>\begin{array}{ccccl}
  −
\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;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{R11e.}</math>
  −
| <math>\overset{X}{\underset{x}{\forall}}~ \upharpoonleft Q \upharpoonright (x) ~=~ \downharpoonleft s \downharpoonright (x)</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{R11e~:~\_\_?\_\_}</math></p>
  −
<p><math>\operatorname{R11e~:~\_\_?\_\_}</math></p>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{R11f.}</math>
  −
| <math>\upharpoonleft Q \upharpoonright ~=~ \downharpoonleft s \downharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" | <math>\operatorname{R11f~:~\_\_?\_\_}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Fact 1===
  −
  −
====Variant 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:50px; text-align:center"
  −
| style="width:80%" | &nbsp;
  −
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~1}</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:50px"
  −
| style="border-top:1px solid black; width:2%"  | &nbsp;
  −
| style="border-top:1px solid black; width:18%" | <math>\text{If}\!</math>
  −
| style="border-top:1px solid black; width:60%" | <math>P, Q ~\subseteq~ X</math>
  −
| 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:60px"
  −
| style="width:2%;  border-top:1px solid black" | &nbsp;
  −
| style="width:14%; border-top:1px solid black" | <math>\operatorname{F1a.}</math>
  −
| style="width:64%; border-top:1px solid black" | <math>s \quad \Leftrightarrow \quad (P ~=~ Q)</math>
  −
| style="width:20%; border-top:1px solid black; border-left:1px solid black; text-align:center" |
  −
<math>\operatorname{F1a~:~R9a}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &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;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{F1c.}</math>
  −
| <math>s \quad \Leftrightarrow \quad \overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<math>\operatorname{F1c~:~R9c}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{F1d.}</math>
  −
| <math>s \quad \Leftrightarrow \quad \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{F1d~:~R9d}</math></p>
  −
<p><math>\operatorname{F1d~:~R8a}</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{F1e.}</math>
  −
| <math>\downharpoonleft s \downharpoonright \quad = \quad \downharpoonleft \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{F1e~:~R8b}</math></p>
  −
<p><math>\operatorname{F1e~:~\_\_?\_\_}</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{F1f.}</math>
  −
| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \downharpoonleft (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<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;
  −
| <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>
  −
  −
====Variant 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:50px; text-align:center"
  −
| style="width:80%" | &nbsp;
  −
| style="width:20%; border-left:1px solid black" | <math>\operatorname{Fact~1}</math>
  −
|}
  −
|-
  −
|
  −
{| align="center" cellpadding="0" cellspacing="0" width="100%"
  −
|- style="height:50px"
  −
| style="border-top:1px solid black; width:2%"  | &nbsp;
  −
| style="border-top:1px solid black; width:18%" | <math>\text{If}\!</math>
  −
| style="border-top:1px solid black; width:60%" | <math>P, Q ~\subseteq~ X</math>
  −
| 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:60px"
  −
| style="width:2%;  border-top:1px solid black" | &nbsp;
  −
| style="width:14%; border-top:1px solid black" | <math>\operatorname{F1a.}</math>
  −
| style="width:64%; border-top:1px solid black" | <math>s \quad \Leftrightarrow \quad (P ~=~ Q)</math>
  −
| style="width:20%; border-top:1px solid black; border-left:1px solid black; text-align:center" |
  −
<math>\operatorname{F1a~:~R9a}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &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;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{F1c.}</math>
  −
| <math>s \quad \Leftrightarrow \quad \overset{X}{\underset{x}{\forall}}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<math>\operatorname{F1c~:~R9c}</math>
  −
|- style="height:20px"
  −
| &nbsp;
  −
| &nbsp;
  −
| &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{F1d.}</math>
  −
| <math>s \quad \Leftrightarrow \quad \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x))</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{F1d~:~R9d}</math></p>
  −
<p><math>\operatorname{F1d~:~R8a}</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{F1e.}</math>
  −
| <math>\downharpoonleft s \downharpoonright \quad = \quad \downharpoonleft \operatorname{Conj_x^X}~ (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<p><math>\operatorname{F1e~:~R8b}</math></p>
  −
<p><math>\operatorname{F1e~:~\_\_?\_\_}</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{F1f.}</math>
  −
| <math>\downharpoonleft s \downharpoonright \quad = \quad \operatorname{Conj_x^X}~ \downharpoonleft (\upharpoonleft P \upharpoonright (x) ~=~ \upharpoonleft Q \upharpoonright (x)) \downharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<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;
  −
| <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>
  −
  −
===Definition 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>
  −
  −
===Definition 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>
  −
  −
===Definition 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>
  −
  −
===Definition 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>
  −
  −
===Definition 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>
  −
  −
===Definition 13===
  −
  −
<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>
  −
  −
===Fact 2.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: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>
  −
  −
===Fact 2.2===
  −
  −
====Variant 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: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>
  −
  −
====Variant 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: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="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 equivalent:}\!</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="78%" style="border-top:1px solid black" |
  −
<math>\begin{align}
  −
\operatorname{F2.2a.} \quad \operatorname{Der}^L
  −
& = & \{ & (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{align}</math>
  −
| width="20%" style="border-top:1px solid black; border-left:1px solid black; text-align:center" | <math>\operatorname{F2.2a~:~R11a}</math>
  −
|- style="height:20px"
  −
| colspan="2" | &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:40px"
  −
| &nbsp;
  −
| <math>\operatorname{F2.2b.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<math>\operatorname{F2.2b~:~R11b}</math>
  −
|- style="height:20px"
  −
| colspan="2" | &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{F2.2c.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<math>\operatorname{F2.2c~:~R11c}</math></p>
  −
|- style="height:20px"
  −
| colspan="2" | &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{F2.2d.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<math>\operatorname{F2.2d~:~Log}</math>
  −
|- style="height:20px"
  −
| colspan="2" | &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{F2.2e.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<math>\operatorname{F2.2e~:~Log}</math>
  −
|- style="height:20px"
  −
| colspan="2" | &nbsp;
  −
| style="border-left:1px solid black; text-align:center" | <math>::\!</math>
  −
|- style="height:60px"
  −
| &nbsp;
  −
| <math>\operatorname{F2.2f.} \quad \upharpoonleft \operatorname{Der}^L \upharpoonright</math>
  −
| style="border-left:1px solid black; text-align:center" |
  −
<math>\operatorname{F2.2f~:~$~}</math>
  −
|}
  −
|}
  −
  −
<br>
  −
  −
===Fact 2.3===
  −
  −
<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>
 
<br>
Jon Awbrey
12,080

edits

Retrieved from "https://mywikibiz.com/Special:MobileDiff/80747...147172"