Difference between revisions of "User:Jon Awbrey/SCRATCHPAD"

MyWikiBiz, Author Your Legacy — Monday November 25, 2024
Jump to navigationJump to search
 
(36 intermediate revisions by the same user not shown)
Line 101: Line 101:
 
| align="right" | — Rousseau, ''Emile, or On Education'', [Rou-1, 34–35]
 
| align="right" | — Rousseau, ''Emile, or On Education'', [Rou-1, 34–35]
 
|}
 
|}
 +
 +
<br>
 +
 +
==Division Styles==
 +
 +
<br>
 +
 +
<div class="references-small">
 +
# Able
 +
# Baker
 +
# Charlie
 +
</div>
 +
 +
<br>
 +
 +
<font face="georgia">
 +
# Able
 +
# Baker
 +
# Charlie
 +
</font>
  
 
<br>
 
<br>
Line 108: 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 190: 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 216: 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 235: 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 240: 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 277: Line 586:
  
 
{| align="center" cellpadding="8" width="90%"
 
{| 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>
+
| <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>
 
|}
 
|}
  
Line 347: 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 497: 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>

Latest revision as of 01:36, 4 December 2011

Greek

  ἐν ἀρχῇ

  Ἐν ἀρχῇ ἦν ὁ λόγος  

Template:Polytonic

Πάτερ ἡμῶν ὁ ἐν τοῖς οὐρανοῖς· ἁγιασθήτω τὸ ὄνομά σου·

Template:Polytonic

ἐλθέτω ἡ βασιλεία σου·

LOGOS

Epigraph Formats


 

'Tis a derivative from me to mine,
And only that I stand for.

  Winter's Tale, 3.2.43–44


 

Out of the dimness opposite equals advance . . . .
     Always substance and increase,
Always a knit of identity . . . . always distinction . . . .
     always a breed of life.

  — Walt Whitman, Leaves of Grass, [Whi, 28]


On either side the river lie
Long fields of barley and of rye,
That clothe the wold and meet the sky;
And thro' the field the road runs by
  To many-tower'd Camelot;
And up and down the people go,
Gazing where the lilies blow
Round an island there below,
  The island of Shalott.
    — Tennyson, The Lady of Shalott, [Ten, 17]


The most valuable insights are arrived at last; but the most valuable insights are methods.

— Nietzsche, The Will to Power, [Nie, S469, 261]


The power of form, the will to give form to oneself. "Happiness" admitted as a goal. Much strength and energy behind the emphasis on forms. The delight in looking at a life that seems so easy. — To the French, the Greeks looked like children.

— Nietzsche, The Will to Power, [Nie, S94, 58]


          In every sort of project there are two things to consider: first, the absolute goodness of the project; in the second place, the facility of execution.

          In the first respect it suffices that the project be acceptable and practicable in itself, that what is good in it be in the nature of the thing; here, for example, that the proposed education be suitable for man and well adapted to the human heart.

          The second consideration depends on relations given in certain situations — relations accidental to the thing, which consequently are not necessary and admit of infinite variety.

— Rousseau, Emile, or On Education, [Rou-1, 34–35]


Division Styles


  1. Able
  2. Baker
  3. Charlie


  1. Able
  2. Baker
  3. Charlie


Blockquote Formats


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 — whether reflected on or not — 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).


          The information of a term is the measure of its superfluous comprehension. That is to say that the proper office of the comprehension is to determine the extension of the term. …

          Every addition to the comprehension of a term, lessens its extension up to a certain point, after that further additions increase the information instead. …

          And therefore as every term must have information, every term has superfluous comprehension. And, hence, whenever we make a symbol to express any thing or any attribute we cannot make it so empty that it shall have no superfluous comprehension.

          I am going, next, to show that inference is symbolization and that the puzzle of the validity of scientific inference lies merely in this superfluous comprehension and is therefore entirely removed by a consideration of the laws of information.

(Peirce, CE 1, 467).


a. The theories of the soul (psyche) handed down by our predecessors have been sufficiently discussed; now let us start afresh, as it were, and try to determine (diorisai) what the soul is, and what definition (logos) of it will be most comprehensive (koinotatos).
b. We describe one class of existing things as substance (ousia), and this we subdivide into three: (1) matter (hyle), which in itself is not an individual thing, (2) shape (morphe) or form (eidos), in virtue of which individuality is directly attributed, and (3) the compound of the two.
c. Matter is potentiality (dynamis), while form is realization or actuality (entelecheia), and the word actuality is used in two senses, illustrated by the possession of knowledge (episteme) and the exercise of it (theorein).
d. Bodies (somata) seem to be pre-eminently substances, and most particularly those which are of natural origin (physica), for these are the sources (archai) from which the rest are derived.
e. But of natural bodies some have life (zoe) and some have not; by life we mean the capacity for self-sustenance, growth, and decay.
f. Every natural body (soma physikon), then, which possesses life must be substance, and substance of the compound type (synthete).
g. But since it is a body of a definite kind, viz., having life, the body (soma) cannot be soul (psyche), for the body is not something predicated of a subject, but rather is itself to be regarded as a subject, i.e., as matter.
h. So the soul must be substance in the sense of being the form of a natural body, which potentially has life. And substance in this sense is actuality.
i. The soul, then, is the actuality of the kind of body we have described. But actuality has two senses, analogous to the possession of knowledge and the exercise of it.
j. Clearly (phaneron) actuality in our present sense is analogous to the possession of knowledge; for both sleep (hypnos) and waking (egregorsis) depend upon the presence of the soul, and waking is analogous to the exercise of knowledge, sleep to its possession (echein) but not its exercise (energein).
k. Now in one and the same person the possession of knowledge comes first.
l. The soul may therefore be defined as the first actuality of a natural body potentially possessing life; and such will be any body which possesses organs (organikon).
m. (The parts of plants are organs too, though very simple ones: e.g., the leaf protects the pericarp, and the pericarp protects the seed; the roots are analogous to the mouth, for both these absorb food.)
n. If then one is to find a definition which will apply to every soul, it will be "the first actuality of a natural body possessed of organs".
o. So one need no more ask (zetein) whether body and soul are one than whether the wax (keros) and the impression (schema) it receives are one, or in general whether the matter of each thing is the same as that of which it is the matter; for admitting that the terms unity and being are used in many senses, the paramount (kyrios) sense is that of actuality.
p. We have, then, given a general definition of what the soul is: it is substance in the sense of formula (logos), i.e., the essence of such-and-such a body.
q. Suppose that an implement (organon), e.g. an axe, were a natural body; the substance of the axe would be that which makes it an axe, and this would be its soul; suppose this removed, and it would no longer be an axe, except equivocally. As it is, it remains an axe, because it is not of this kind of body that the soul is the essence or formula, but only of a certain kind of natural body which has in itself a principle of movement and rest.
r. We must, however, investigate our definition in relation to the parts of the body.
s. If the eye were a living creature, its soul would be its vision; for this is the substance in the sense of formula of the eye. But the eye is the matter of vision, and if vision fails there is no eye, except in an equivocal sense, as for instance a stone or painted eye.
t. Now we must apply what we have found true of the part to the whole living body. For the same relation must hold good of the whole of sensation to the whole sentient body qua sentient as obtains between their respective parts.
u. That which has the capacity to live is not the body which has lost its soul, but that which possesses its soul; so seed and fruit are potentially bodies of this kind.
v. The waking state is actuality in the same sense as the cutting of the axe or the seeing of the eye, while the soul is actuality in the same sense as the faculty of the eye for seeing, or of the implement for doing its work.
w. The body is that which exists potentially; but just as the pupil and the faculty of seeing make an eye, so in the other case the soul and body make a living creature.
x. It is quite clear, then, that neither the soul nor certain parts of it, if it has parts, can be separated from the body; for in some cases the actuality belongs to the parts themselves. Not but what there is nothing to prevent some parts being separated, because they are not actualities of any body.
y. It is also uncertain (adelon) whether the soul as an actuality bears the same relation to the body as the sailor (ploter) to the ship (ploion).
z. This must suffice as an attempt to determine in rough outline the nature of the soul.
  (Aristotle, On the Soul, 2.1)


Ordered List Formats

Simple

  1. Item 1
    1. Item a
    2. Item b
    3. Item c
  2. Item 2
    1. Item a
    2. Item b
    3. Item c
  3. Item 3

Complex

  1. Item 1
    1. Item a
      1. Item i
      2. Item ii
      3. Item iii
    2. Item b
    3. Item c
  2. Item 2
    1. Item a
      1. Item i
      2. Item ii
      3. Item iii
    2. Item b
    3. Item c
  3. Item 3

Examples

Example 1

In the present case, one can observe the possibility that the author is suggesting the following analogies:

  1. One analogy says that authoring a text is like piloting a vehicle. This can be written in either one of two ways.

    1. Poet / Poem = Pilot / Boat.

    2. Poet / Pilot = Poem / Boat.

    3. Pilot / Poet = Boat / Poem.

Example 2

In this way, an epitext can serve a couple of functions within a text:

  1. 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 ???]

  2. 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:

    1. 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.

    2. 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.

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:

  1. 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.

  2. 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:

    1. 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.

    2. 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.

Example 4

In the pragmatic theory of signs it is often said, “The question of the interpreter reduces to the question of the interpretant.” 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:

  1. 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:

    1. What may be: the "prospective" or the "imaginative";
      also: the contingent, inquisitive, interrogative, optional, provisional, speculative, or "possible on some condition".

    2. What is: the "descriptive" or the "indicative";
      also: the actual, apparent, definite, empirical, existential, experiential, factual, phenomenal, or "evident at some time".

    3. What must be: the "prescriptive" or the "imperative";
      also: the injunctive, intentional, normative, obligatory, optative, prerequisite, or "necessary to some purpose".

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.

  1. 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.

  2. 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.

Outline Formats


Example 1. Modus Ponens
    Information Reducing Inference
     

\(\begin{array}{l} ~ p \Rightarrow q \\ ~ p \\ \overline{~~~~~~~~~~~~~~~} \\ ~ q \end{array}\)

    Information Preserving Inference
     

\(\begin{array}{l} ~ p \Rightarrow q \\ ~ p \\ ='"`UNIQ--h-13--QINU`"'\!=\!=\!=\!=\!=\!=\!= \\ ~ p ~ q \end{array}\)


Example 2. Transitivity
    Information Reducing Inference
     

\(\begin{array}{l} ~ p \le q \\ ~ q \le r \\ \overline{~~~~~~~~~~~~~~~} \\ ~ p \le r \end{array}\)

    Information Preserving Inference
     

\(\begin{array}{l} ~ p \le q \\ ~ q \le r \\ ='"`UNIQ--h-14--QINU`"'\!=\!=\!=\!=\!=\!=\!= \\ ~ p \le q \le r \end{array}\)


Transitive Law (Implicational Inference)
   

\(\begin{array}{l} ~ p \le q \\ ~ q \le r \\ \overline{~~~~~~~~~~~~~~~} \\ ~ p \le r \end{array}\)

By itself, the information \(p \le q\) would reduce our uncertainty from \(\log 8\!\) bits to \(\log 6\!\) bits.
By itself, the information \(q \le r\) would reduce our uncertainty from \(\log 8\!\) bits to \(\log 6\!\) bits.
By itself, the information \(p \le r\) would reduce our uncertainty from \(\log 8\!\) bits to \(\log 6\!\) bits.


Transitive Law (Equational Inference)
   

\(\begin{array}{l} ~ p \le q \\ ~ q \le r \\ ='"`UNIQ--h-15--QINU`"'\!=\!=\!=\!=\!=\!=\!= \\ ~ p \le q \le r \end{array}\)

The contents and the measures of information that are associated with the propositions \(p \le q\) and \(q \le r\) are the same as before.
On its own, the information \(p \le q \le r\) would reduce our uncertainty from log(8) = 3 bits to log(4) = 2 bits, a reduction of 1 bit.


Mathematical Symbols

\(-<\!\) -<
\(-\!<\) -\!<
\(-\!\!<\) -\!\!<
\(-\!\!\!<\) -\!\!\!<
\(\curlyvee\) \curlyvee
\(\curlywedge\) \curlywedge
\(\lessdot\) \lessdot
\(\gtrdot\) \gtrdot
\(:\!\lessdot\) :\!\lessdot
\(:\!\gtrdot\) :\!\gtrdot
\(\colon\!\lessdot\) \colon\!\lessdot
\(\colon\!\gtrdot\) \colon\!\gtrdot
\(\And\) \And
\(\dagger\) \dagger
\(\ddagger\) \ddagger
\(\lVert\) \lVert
\(\rVert\) \rVert
\(\parallel\) \parallel
\(\P\) \P
\(\S\) \S
\($\) $ NB. Idiosyntax of WikiTeX
\($\!\) $\! NB. Idiosyntax of WikiTeX
\(\$\) \$ NB. Standard Syntax in LaTeX
\(\mathfrak{g}_{\dagger\ddagger} \, ^\dagger\mathit{l}_\parallel \, ^\parallel\mathrm{w} \, ^\ddagger\mathrm{h}\)
\(\mathfrak{g}_{\dagger\ddagger} {}^\dagger\mathit{l}_\parallel {}^\parallel\mathrm{w} {}^\ddagger\mathrm{h}\)
\(\mathfrak{g}_{\dagger\ddagger} {}^\dagger\!\mathit{l}_\parallel {}^\parallel\!\mathrm{w} {}^\ddagger\!\mathrm{h}\)

Cactus TeX


\(\begin{array}{l} \texttt{ } \\ \texttt{~} \\ \texttt{()} \\ \texttt{(~)} \\ \texttt{(( ))} \\ \texttt{( )( )} \\ \texttt{a b c} \\ \texttt{a~b~c} \\ \texttt{a(a)~=~(~)} \\ \texttt{a((b)(c))~=~((ab)(ac))} \\ \end{array}\)


\(\begin{array}{l} \texttt{d}^2 \texttt{x} \\ \texttt{d}^\text{2} \texttt{x} \\ \texttt{d}^\texttt{2} \texttt{x} \\ \end{array}\)


\(\texttt{uv~(du~dv) ~+~ u(v)~(du (dv)) ~+~ (u)v~((du) dv) ~+~ (u)(v)~((du)(dv))}\)


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


\(\begin{matrix} \bar{(} \ldots \bar{)} & \bar{|} \ldots \bar{|} \\ \\ \dot{(} \ldots \dot{)} & \dot{|} \ldots \dot{|} \\ \\ \hat{(} \ldots \hat{)} & \hat{|} \ldots \hat{|} \\ \\ \check{(} \ldots \check{)} & \check{|} \ldots \check{|} \\ \\ \tilde{(} \ldots \tilde{)} & \tilde{|} \ldots \tilde{|} \\ \\ \downharpoonleft \ldots \downharpoonright & \upharpoonleft \ldots \upharpoonright \\ \\ \overline{(} \ldots \overline{)} & \overline{|} \ldots \overline{|} \\ \\ \underline{(} \ldots \underline{)} & \underline{|} \ldots \underline{|} \\ \\ \overline{\underline{(}} \ldots \overline{\underline{)}} & \overline{\underline{|}} \ldots \overline{\underline{|}} \\ \\ \end{matrix}\)

\(\begin{array}{lllll} {}^{_\sim}\!X & = & U - X & = & \{ \, u \in U : \underline{(} u \in X \underline{)} \, \}. \end{array}\)

\(\begin{array}{lllll} {}^{_\sim}\!X & = & U - X & = & \{ \, u \in U : \tilde{(} u \in X \tilde{)} \, \}. \end{array}\)

\[X = \{\ (\!|u|\!)(\!|v|\!),\ (\!|u|\!) v,\ u (\!|v|\!),\ u v\ \} \cong \mathbb{B}^2.\]
\[X = \{\ \underline{(u)(v)},\ \underline{(u)~v},\ \underline{u~(v)},\ \underline{u~v}\ \} \cong \mathbb{B}^2.\]
\[X = \{\!\] (u)(v)\(,\) (u)v\(,\) u(v)\(,\) uv \(\} \cong \mathbb{B}^2.\)
\[X = \{\!\] (u)(v) \(,\) (u)v \(,\) u(v) \(,\) uv \(\} \cong \mathbb{B}^2.\)
\(X = \{\!\) (u)(v) \(,\) (u)v \(,\) u(v) \(,\) uv \(\} \cong \mathbb{B}^2.\)
\(X = \{\!\) (u)(v) , (u)v ,  u(v) , uv \(\} \cong \mathbb{B}^2.\)


Examples of Logical Orbits

Version 1

\(\begin{array}{ccc} \texttt{u}' & = & \texttt{((u)(v))} \\ \texttt{v}' & = & \texttt{((u,~v))} \end{array}\)

\(\begin{matrix} \text{Orbit 1} \\ \text{Initial Point :}~ (u, v) = (1, 1) \end{matrix}\)

\(\begin{array}{c|cc} t & u & v \\ \\ 0 & 1 & 1 \\ 1 & 1 & 1 \\ 2 & '' & '' \\ \end{array}\)

\(\begin{matrix} \text{Orbit 2} \\ \text{Initial Point :}~ (u, v) = (0, 0) \end{matrix}\)

\(\begin{array}{c|cc} t & u & v \\ \\ 0 & 0 & 0 \\ 1 & 0 & 1 \\ 2 & 1 & 0 \\ 3 & 1 & 0 \\ 4 & '' & '' \\ \end{array}\)

Version 2

\(\text{Orbit 1. Intitial Point :}~ (u, v) = (1, 1)\)

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

\(\text{Orbit 2. Intitial Point :}~ (u, v) = (0, 0)\)

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

Version 3

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

\(\begin{array}{c|cc|cc|} t & u & v & du & dv \\[8pt] 0 & 1 & 1 & 0 & 0 \\ 1 & '' & '' & '' & '' \\ \end{array}\)

 
\(\text{Orbit 2}\!\)

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

Type Markers

Composer P

\(\begin{array}{l} ((x \underset{A}{:} ~y \overset{B}{\underset{A}{:}}) \underset{B}{:} ~z \overset{C}{\underset{B}{:}}) \underset{C}{:} \end{array}\)

\(\begin{array}{l} ((x \overset{A}{:} ~y \overset{B}{\underset{A}{:}}) \overset{B}{:} ~z \overset{C}{\underset{B}{:}}) \overset{C}{:} \end{array}\)

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

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

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

Transposer T

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

Proof Example

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

Over And Under Setting

  1. The conjunction \(\overset{J}{\underset{j}{\operatorname{Conj}}}\ q_j\) of a set of propositions, \(\{ q_j : j \in J \},\) is a proposition that is true if and only if every one of the \(q_j\!\) is true.

    \(\overset{J}{\underset{j}{\operatorname{Conj}}}\ q_j\) is true  \(\Leftrightarrow\)  \(q_j\!\) is true for every \(j \in J.\)

  2. The surjunction \(\overset{J}{\underset{j}{\operatorname{Surj}}}\ q_j\) of a set of propositions, \(\{ q_j : j \in J \},\) is a proposition that is true if and only if exactly one of the \(q_j\!\) is untrue.

    \(\overset{J}{\underset{j}{\operatorname{Surj}}}\ q_j\) is true  \(\Leftrightarrow\)  \(q_j\!\) is untrue for unique \(j \in J.\)

Equation Sequences

\(\begin{array}{lll} [| \downharpoonleft s \downharpoonright |] & = & [| F |] \\[6pt] & = & F^{-1} (\underline{1}) \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ s ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ F(x, y) = \underline{1} ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ F(x, y) ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \underline{(}~x~,~y~\underline{)} = \underline{1} ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \underline{(}~x~,~y~\underline{)} ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x ~\operatorname{exclusive~or}~ y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ \operatorname{just~one~true~of}~ x, y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x ~\operatorname{not~equal~to}~ y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x \nLeftrightarrow y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x \neq y ~\} \\[6pt] & = & \{~ (x, y) \in \underline\mathbb{B}^2 ~:~ x + y ~\}. \end{array}\)

\(\begin{array}{lll} [| F^\$ (p, q) |] & = & [| \underline{(}~p~,~q~\underline{)}^\$ |] \\[6pt] & = & (F^\$ (p, q))^{-1} (\underline{1}) \\[6pt] & = & \{~ x \in X ~:~ F^\$ (p, q)(x) ~\} \\[6pt] & = & \{~ x \in X ~:~ \underline{(}~p~,~q~\underline{)}^\$ (x) ~\} \\[6pt] & = & \{~ x \in X ~:~ \underline{(}~p(x)~,~q(x)~\underline{)} ~\} \\[6pt] & = & \{~ x \in X ~:~ p(x) + q(x) ~\} \\[6pt] & = & \{~ x \in X ~:~ p(x) \neq q(x) ~\} \\[6pt] & = & \{~ x \in X ~:~ \upharpoonleft P \upharpoonright (x) ~\neq~ \upharpoonleft Q \upharpoonright (x) ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P ~\nLeftrightarrow~ x \in Q ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P\!-\!Q ~\operatorname{or}~ x \in Q\!-\!P ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P\!-\!Q ~\cup~ Q\!-\!P ~\} \\[6pt] & = & \{~ x \in X ~:~ x \in P + Q ~\} \\[6pt] & = & P + Q ~\subseteq~ X \\[6pt] & = & [|p|] + [|q|] ~\subseteq~ X \end{array}\)

Multiline TeX Formats


\( \begin{cases} a \\ b \\ c \\ \begin{cases} d \\ e \\ f \\ \end{cases} \\ g \\ h \\ i \\ \end{cases} \)


\(\begin{alignat}{2} x & = (y - z)(y + z) \\ & = y^2 - z^2 \\ \end{alignat}\)


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


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


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


\(\begin{array}{lllll} \operatorname{F2.2a.} & \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{array}\)