12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 19:34, 3 November 2008
, 19:34, 3 November 2008Revert Some Sort Of Screw-Up : Undo revision 72582 by Jon Awbrey (Talk)
==Analysis of contingent propositions==
{{DISPLAYTITLE:Propositional Equation Reasoning Systems}}
This article develops elementary facts about the formal calculi that we describe as '''propositional equation reasoning systems''' ('''PERS'''). This work follows up on the ''[[alpha graphs]]'' that [[Charles Sanders Peirce]] devised as a graphical syntax for [[propositional calculus]] and also on the ''calculus of indications'' that [[George Spencer Brown]] presented in his ''[[Laws of Form]]''.
==Formal development==
The first order of business is to give the exact forms of the axioms that we use, devolving from Peirce's "[[Logical Graphs]]" via Spencer-Brown's ''[[Laws of Form]]'' (LOF). In formal proofs, we use a variation of the annotation scheme from LOF to mark each step of the proof according to which axiom, or ''initial'', is being invoked to justify the corresponding step of syntactic transformation, whether it applies to graphs or to strings.
===Axioms===
The axioms are just four in number, divided into the ''arithmetic initials'', <math>I_1\!</math> and <math>I_2,\!</math> and the ''algebraic initials'', <math>J_1\!</math> and <math>J_2.\!</math>
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_01.jpg|500px]] || (1)
|-
| [[Image:PERS_Figure_02.jpg|500px]] || (2)
|-
| [[Image:PERS_Figure_03.jpg|500px]] || (3)
|-
| [[Image:PERS_Figure_04.jpg|500px]] || (4)
|}
One way of assigning logical meaning to the initial equations is known as the ''entitative interpretation'' (EN). Under EN, the axioms read as follows:
{| align="center" border="0" cellpadding="10"
|
<math>\begin{array}{ccccc}
I_1 & : &
\operatorname{true}\ \operatorname{or}\ \operatorname{true} & = &
\operatorname{true} \\
I_2 & : &
\operatorname{not}\ \operatorname{true}\ & = &
\operatorname{false} \\
J_1 & : &
a\ \operatorname{or}\ \operatorname{not}\ a & = &
\operatorname{true} \\
J_2 & : &
(a\ \operatorname{or}\ b)\ \operatorname{and}\ (a\ \operatorname{or}\ c) & = &
a\ \operatorname{or}\ (b\ \operatorname{and}\ c) \\
\end{array}</math>
|}
Another way of assigning logical meaning to the initial equations is known as the ''existential interpretation'' (EX). Under EX, the axioms read as follows:
{| align="center" border="0" cellpadding="10"
|
<math>\begin{array}{ccccc}
I_1 & : &
\operatorname{false}\ \operatorname{and}\ \operatorname{false} & = &
\operatorname{false} \\
I_2 & : &
\operatorname{not}\ \operatorname{false} & = &
\operatorname{true} \\
J_1 & : &
a\ \operatorname{and}\ \operatorname{not}\ a & = &
\operatorname{false} \\
J_2 & : &
(a\ \operatorname{and}\ b)\ \operatorname{or}\ (a\ \operatorname{and}\ c) & = &
a\ \operatorname{and}\ (b\ \operatorname{or}\ c) \\
\end{array}</math>
|}
All of the axioms in this set have the form of equations. This means that all of the inference licensed by them are reversible. The proof annotation scheme employed below makes use of a double bar <math>\overline{\underline{~~~~~~}}</math> to mark this fact, but it will often be left to the reader to decide which of the two possible ways of applying the axiom is the one that is called for in a particular case.
Peirce introduced these formal equations at a level of abstraction that is one step higher than their customary interpretations as propositional calculi, which two readings he called the ''Entitative'' and the ''Existential'' interpretations, here referred to as "EN" and "EX", respectively. The early CSP, as in his essay on "Qualitative Logic", and also GSB, emphasized the EN interpretation, while the later CSP developed mostly the EX interpretation.
===Frequently used theorems===
====C<sub>1</sub>. Double negation theorem====
The first theorem goes under the names of ''Consequence 1'' <math>(C_1)\!</math>, the ''double negation theorem'' (DNT), or ''Reflection''.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_05.jpg|500px]] || (5)
|}
The proof that follows is adapted from the one that was given by [[George Spencer Brown]] in his book ''Laws of Form'' (LOF) and credited to two of his students, John Dawes and D.A. Utting.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_06.jpg|500px]] || (6)
|}
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_07.jpg|500px]] || (7)
|}
====C<sub>2</sub>. Generation theorem====
One theorem of frequent use goes under the nickname of the ''weed and seed theorem'' (WAST). The proof is just an exercise in mathematical induction, once a suitable basis is laid down, and it will be left as an exercise for the reader. What the WAST says is that a label can be freely distributed or freely erased anywhere in a subtree whose root is labeled with that label. The second in our list of frequently used theorems is in fact the base case of this weed and seed theorem. In LOF, it goes by the names of ''Consequence 2'' <math>(C_2)\!</math> or ''Generation''.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_08.jpg|500px]] || (8)
|}
Here is a proof of the Generation Theorem.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_09.jpg|500px]] || (9)
|}
====C<sub>3</sub>. Dominant form theorem====
The third of the frequently used theorems of service to this survey is one that Spencer-Brown annotates as ''Consequence 3'' <math>(C_3)\!</math> or ''Integration''. A better mnemonic might be ''dominance and recession theorem'' (DART), but perhaps the brevity of ''dominant form theorem'' (DFT) is sufficient reminder of its double-edged role in proofs.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_10.jpg|500px]] || (10)
|}
Here is a proof of the Dominant Form Theorem.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_11.jpg|500px]] || (11)
|}
===Exemplary proofs===
Based on the axioms given at the outest, and aided by the theorems recorded so far, it is possible to prove a multitude of much more complex theorems. A couple of all-time favorites are given next.
====Peirce's law====
: ''Main article : [[Peirce's law]]
Peirce's law is commonly written in the following form:
<center>
<p><math>((p \Rightarrow q) \Rightarrow p) \Rightarrow p</math></p>
</center>
The existential graph representation of Peirce's law is shown in Figure 12.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_12.jpg|500px]] || (12)
|}
A graphical proof of Peirce's law is shown in Figure 13.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_13.jpg|500px]] || (13)
|}
====Praeclarum theorema====
An illustrious example of a propositional theorem is the ''praeclarum theorema'', the ''admirable'', ''shining'', or ''splendid'' theorem of [[Leibniz]].
<blockquote>
<p>If ''a'' is ''b'' and ''d'' is ''c'', then ''ad'' will be ''bc''.</p>
<p>This is a fine theorem, which is proved in this way:</p>
<p>''a'' is ''b'', therefore ''ad'' is ''bd'' (by what precedes),</p>
<p>''d'' is ''c'', therefore ''bd'' is ''bc'' (again by what precedes),</p>
<p>''ad'' is ''bd'', and ''bd'' is ''bc'', therefore ''ad'' is ''bc''. Q.E.D.</p>
<p>([[Leibniz]], ''Logical Papers'', p. 41).</p>
</blockquote>
Under the existential interpretation, the praeclarum theorema is represented by means of the following logical graph.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_14.jpg|500px]] || (14)
|}
And here's a neat proof of that nice theorem.
{| align="center" border="0" cellpadding="10" cellspacing="0"
| [[Image:PERS_Figure_15.jpg|500px]] || (15)
|}
==Formal extension : Cactus calculus==
Let us now extend the CSP–GSB calculus in the following way:
The first extension is the ''reflective extension of logical graphs'', or what may be described as the ''cactus language'', after its principal graph-theoretic data structure. It is generated by generalizing the negation operator <math>(\_)\!</math> in a particular manner, treating <math>(\_)\!</math> as the ''[[minimal negation operator]]'' of order 1, and adding another such operator for each integer parameter greater than 1. Taken in series, the minimal negation operators are symbolized by parenthesized argument lists of the following shapes: <math>(\_),\!</math> <math>(\_, \_),\!</math> <math>(\_, \_, \_),\!</math> and so on, where the number of argument slots is the order of the reflective negation operator in question.
The formal rule of evaluation for a <math>k\!</math>''-lobe'' or <math>k\!</math>-operator may be summarized as follows:
<pre>
o-----------------------------------------------------------o
| Evaluation Rule ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` x_1 `x_2` `...` x_k ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` `o----o-...-o----o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` = ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ( x_1, x_2, ..., x_k )` ` = ` ` ` ` ` <space> ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` IF AND ONLY IF` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` ` |
| ` Just one of the x_1, x_2, ..., x_k` `=` `|` `=` `( )` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
</pre>
The interpretation of these operators, read as assertions about the values of their listed arguments, is as follows:
<pre>
o-----------------------------------------------------------o
| Interpretation Rule ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` x_1 `x_2` `...` x_k ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o----o-...-o----o` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| A "k-lobe operator" of the form "(x_1, ..., x_k)" ` ` ` ` |
| enjoys two commonly employed interpretations for` ` ` ` ` |
| propositional logic, in other words, two ways of` ` ` ` ` |
| taking it as an assertion about, or a constraint` ` ` ` ` |
| upon, the logical values of the listed arguments, ` ` ` ` |
| the mentioned variables x_j, for j = 1 through k. ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| Existential Interpretation: ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` `"Just one of the k arguments is not true." ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| Entitative `Interpretation: ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` `"Not just one of the k arguments is true." ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
</pre>
==Case analysis-synthesis theorem==
The task at hand is to lay out what I think of as the pontoon bridge between the model-theoretic and the proof-theoretic shores, and thus between their diverging perspectives on logical procedure, even if I can construct it at a point but so close to their common source that it may not seem like it's worth the candle.
The substance of this principle was known to Boole in the 1850's, tantamount to what we now call the ''boolean expansion'' of a propositional expression. The only novelty here resides in a certain manner of presentation, in which we will prove the basic principle from the axioms given before. One name for this rule is the ''Case Analysis-Synthesis Theorem'' (CAST).
I am going to revert to my customarily sloppy workshop manners and refer to propositions and proposition expressions on rough analogy with functions and function expressions, which implies that a proposition will be regarded as the chief formal object of discussion, enjoying many proposition expressions, formulas, or sentences that express it, but worst of all I will probably just go ahead and use any and all of these terms as loosely as I see fit, taking a bit of extra care only when I see the need.
Let <math>Q\!</math> be a propositional expression with an unspecified, but context-appropriate number of variables, say, none, or <math>x,\!</math> or <math>x_1, \ldots, x_k,\!</math> as the case may be.
:* Strings and graphs that have no labels are called ''bare''.
:* A bare terminal node, symbolized by a small circle <math>\circ</math> in text, is known as a ''stone''.
:* A bare terminal edge, symbolized by a vertical bar <math>\vert</math> in text, is known as a ''stick''.
Let the ''replacement expression'' of the form <math>Q[\circ /x]</math> denote the proposition that results from <math>Q\!</math> by replacing every token of the variable <math>x\!</math> with a blank, that is to say, by erasing <math>x.\!</math>
Let the ''replacement expression'' of the form <math>Q[\,\vert /x]</math> denote the proposition that results from <math>Q\!</math> by replacing every token of the variable <math>x\!</math> with a stick stemming from the site of <math>x.\!</math>
In the case of a propositional expression <math>Q\!</math> that has no token of the designated variable <math>x,\!</math> let it be stipulated that <math>Q[\circ /x] = Q = Q[\,\vert /x].</math>
I think that I am at long last ready to state the following:
<pre>
o-----------------------------------------------------------o
| Case Analysis-Synthesis Theorem (CAST)` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `x` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `o` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `x` `|` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` Q[o/x] o---o Q[|/x] ` ` |
| ` ` ` ` ` ` `Q` ` ` ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` = ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `Q` ` ` ` ` ` ` = ` ( Q[o/x] x , Q[|/x] (x) ) |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
</pre>
In order to think of tackling even the roughest sketch toward a proof of this theorem, we need to add a number of axioms and axiom schemata. Because I abandoned proof-theoretic purity somewhere in the middle of grinding this calculus into computational form, I never got around to finding the most elegant and minimal, or anything near a complete set of axioms for the ''cactus language'', so what I list here are just the slimmest rudiments of the hodge-podge of ''rules of thumb'' that I have found over time to be necessary and useful in most working settings. Some of these special precepts are probably provable from genuine axioms, but I have yet to go looking for a more proper formulation.
<pre>
o-----------------------------------------------------------o
| Precept L_1.` Indifference` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` a ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` a ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` o---o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` @ ` ` ` ` = ` ` ` ` @ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `(a, (a)) ` ` = ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` Split <---- | ----> Merge ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
</pre>
<pre>
o-----------------------------------------------------------o
| Precept L_2.` Equality. `The Following Are Equivalent:` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` b ` ` ` ` ` ` ` a ` b ` ` ` ` ` ` ` a ` ` ` ` ` |
| ` ` ` ` ` o ` ` ` ` ` ` ` o---o ` ` ` ` ` ` ` o ` ` ` ` ` |
| ` ` ` a ` | ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` | ` b ` ` ` |
| ` ` ` o---o ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` o---o ` ` ` |
| ` ` ` `\ /` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` `\ /` ` ` ` |
| ` ` ` ` @ ` ` ` ` = ` ` ` ` @ ` ` ` ` = ` ` ` ` @ ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` `(a, (b)) ` ` = ` ` ((a , b)) ` ` = ` ` ((a), b)` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
</pre>
<pre>
o-----------------------------------------------------------o
| Precept L_3.` Dispersion` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| For k > 1, the following equation holds:` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` y_1 ` `y_2` `...` ` y_k ` ` x y_1 `x y_2` `...` x y_k ` |
| ` `o------o-...-o------o` ` ` ` `o------o-...-o------o` ` |
| ` ` \ ` ` ` ` ` ` ` ` / ` ` ` ` ` \ ` ` ` ` ` ` ` ` / ` ` |
| ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` |
| ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` |
| ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` |
| ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` \ ` ` ` ` / ` ` ` ` |
| ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` |
| ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` ` \ ` ` / ` ` ` ` ` |
| ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` |
| ` ` ` ` ` `x @` ` ` ` ` ` ` = ` ` ` ` ` ` `@` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` x (y_1, ..., y_k) ` ` ` = ` ` (x y_1, ..., x y_k) ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` Distill ` ` <---- | ----> ` ` Disperse` ` ` ` ` |
o-----------------------------------------------------------o
</pre>
To see why the ''Dispersion Rule'' holds, look at it this way: If <math>x\!</math> is true, then the presence of <math>x\!</math> makes no difference on either side of the equation, but if <math>x\!</math> is false, then both sides of the equation are false.
Here is a proof sketch for the ''Case Analysis-Synthesis Theorem'' (CAST):
<pre>
o-----------------------------------------------------------o
| Case Analysis-Synthesis Theorem.` Proof Sketch. ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `Q` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< L1. Split " " >=============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `x` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `x` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `o---o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `Q @` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< L3. Disperse "Q" >==========o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `x` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `x` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `Q o---o Q` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< C1. Reflect "x" >===========o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `x` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `x` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `Q o---o Q[((x))/x] ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< C2. Weed "x", "(x)" >=======o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `x` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `x ` |` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` Q[o/x] o---o Q[|/x] ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< QES >=======================o
</pre>
NB. QES = "Quod Erat Sketchiendum".
Some of the jobs that the CAST can be usefully put to work on are proving propositional theorems and establishing equations between propositions. Once again, let us turn to the example of Leibniz's ''Praeclarum Theorema'' as a way of illustrating how.
<pre>
o-----------------------------------------------------------o
| Praeclarum Theorema.` Proof by CAST.` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` a o ` o d ` ` o ad` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o---------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "a" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `bc ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` b o ` o c ` o o ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` | ` | ` ` |/` ` ` ` ` |
| ` ` ` o ` o d ` o d ` ` ` ` ` ` `o--o ` o d ` o d ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` a o-----------------------------o---o a ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` o c ` ` o ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` | ` ` `/` ` ` ` ` |
| ` ` ` o ` o d ` o d ` ` ` ` ` ` `o--o ` o d ` o ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` a o-----------------------------o---o a ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` o c ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` |
| ` ` ` o ` o d ` o d ` ` ` ` ` ` ` ` ` ` o d ` ` ` ` ` ` ` |
| ` ` ` `\ / ` ` `| ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` a o-----------------------------o---o a ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o d ` o d ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` a o-----------------------------o---o a ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o d ` o d ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` a o-----------------------------o---o a ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "d" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` b ` c ` `bc ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` o ` o o ` o o ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` | ` |/` ` |/` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` o ` ` ` ` ` ` ` o ` o ` ` o ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` d o-------------------------o---o d ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` b ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` o ` ` o ` ` o ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` | ` `/` ` `/` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` o ` ` ` ` ` ` ` o ` o ` ` o ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` d o-------------------------o---o d ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` b ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` o ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` d o-------------------------o---o d ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` d o-------------------------o---o d ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` o ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` d o-------------------------o---o d ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "b" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` o ` ` ` ` o ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` |
| ` ` o ` o c ` o c ` ` ` ` ` ` o ` o c ` o c ` ` ` ` ` ` ` |
| ` ` | ` | ` ` | ` ` ` ` ` ` ` | ` | ` ` | ` ` ` ` ` ` ` ` |
| ` ` o ` o ` ` o ` ` ` ` ` ` ` o ` o ` ` o ` ` ` ` ` ` ` ` |
| ` ` `\ /` ` ` | ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` |
| ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o-------------------------o---o b ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` |
| ` ` ` ` o c ` o c ` ` ` ` ` ` ` ` o c ` o c ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` |
| ` ` ` ` o ` ` o ` ` ` ` ` ` ` o ` o ` ` o ` ` ` ` ` ` ` ` |
| ` ` ` `/` ` ` | ` ` ` ` ` ` ` `\ /` ` ` | ` ` ` ` ` ` ` ` |
| ` ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o-------------------------o---o b ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Domination >================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o c ` o c ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o ` ` o ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `/` ` ` | ` ` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o-------o ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o-------------------------o---o b ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o c ` o c ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `/` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` o-------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o-------------------------o---o b ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< CAST "c" >==================o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` | ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` |
| ` ` `/` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` |
| ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` c o-------------------------o---o c ` ` ` ` ` ` ` ` ` ` |
| ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `b o---o---o b` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` o ` ` o ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` o-------o ` ` ` ` ` ` ` ` o-------o ` ` ` ` ` ` ` ` ` |
| ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` | ` ` ` ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` c o-------------------------o---o c ` ` ` ` ` ` ` ` ` ` |
| ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` ` ` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `b o---o---o b` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< Cancellation >==============o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `c o---o---o c` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `b o---o---o b` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o=============================< QED >=======================o
</pre>
What we have harvested is the succulent equivalent of a ''disjunctive normal form'' (DNF) for the proposition with which we started. Remembering that a blank node is the graphical equivalent of a logical value ''true'', we can read this brand of DNF in the following manner:
<pre>
<pre>
o-----------------------------------------------------------o
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` q o ` o r ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `c o---o---o c` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` | ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` p o ` o p ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `b o---o---o b` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `d o---o---o d` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `a o---o---o a` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `@` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `(p (q)) (p (r))` ` ` ` ` ` ` ` ` ` ` |
| Either not 'a' and thus 'true'` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` Or ` ` 'a' and thus ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `Either not 'd' and thus 'true' ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `Or ` ` 'd' and thus` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` Either not 'b' and thus 'true'` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` Or ` ` 'b' and thus ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `Either not 'c' and thus 'true' ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` `Or ` ` 'c' and thus true.` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
</pre>
</pre>
That is tantamount to saying that the proposition being submitted for analysis is true in each case. Ergo we are justly entitled to title it a ''Theorem''.
==Logic as sign transformation==
We have been looking at various ways of transforming propositional expressions, expressed in the parallel formats of character strings and graphical structures, all the while preserving certain aspects of their "meaning" — and here I risk using that vaguest of all possible words, but only as a promissory note, hopefully to be cached out in a more meaningful species of currency as the discussion develops.
I cannot pretend to be acquainted with or to comprehend every form of intension that others might find of interest in a given form of expression, nor can I speak for every form of meaning that another might find in a given form of syntax. The best that I can hope to do is to specify what my object is in using these expressions, and to say what aspects of their syntax are meant to serve this object, lending these properties the interest I have in preserving them as I put the expressions through the paces of their transformations.
On behalf of this object I have been spinning in the form of this thread a developing example base of propositional expressions, in the data structures of graphs and strings, along with many examples of step-wise transformations on these expressions that preserve something of significant logical import, something that might be referred to as their ''logical equivalence class'' (LEC), and that we could as well call the ''constraint information'' or the ''denotative object'' of the expression in view.
To focus still more, let us return to that ''Splendid Theorem'' noted by Leibniz, and let us look more carefully at the two distinct ways of transforming its initial expression that we just used to arrive at an equivalent expression, one that made its tautologous character or its theorematic nature as evident as it could be.
Just to remind you, here is the ''Splendid Theorem'' again:
o-----------------------------------------------------------o
| Praeclarum Theorema (PT)` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` b o ` o c ` ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` | ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` a o ` o d ` ` o ad` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\ /` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` o---------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` @ ` ` ` ` ` ` ` ` ` = ` ` ` ` ` ` ` ` ` @ ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| `((a(b))(d(c))((ad(bc)))) ` = ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
The first way of transforming the expression that appears on the left hand side of the equation can be described as ''proof-theoretic'' in character. That was given in Note 5.
* PERS 5. http://forum.wolframscience.com/showthread.php?postid=957#post957
The other way of transforming the expression that appears on the left hand side of the equation can be described as ''model-theoretic'' in character. That was given in Note 9.
* PERS 9. http://forum.wolframscience.com/showthread.php?postid=962#post962
What we have here amounts to a couple of different styles of ''communicational conduct'', or ''conductive communication'', if you prefer, that is to say, two sequences of signs of the form ''e''<sub>1</sub>, ''e''<sub>2</sub>, …, ''e''<sub>''n''</sub>, each one beginning with a problematic expression and eventually ending with a clear expression of the appropriate ''logical equivalence class'' (LEC) to which each and every sign or expression in the sequence belongs.
Ordinarily, any orbit through a locus of signs can be taken to reflect an underlying sign-process, a case of ''semiosis''. So what we have here are two very special cases of semiosis, and what we might just find it useful to contemplate is how to characterize them as two species of a very general class.
We are starting to delve into some fairly picayune details of a particular sign system, non-trivial enough in its own right but still rather simple compared to the types of our ultimate interest, and though I believe that this exercise will be worth the effort in prospect of understanding more complicated sign systems, I feel that I ought to say a few words about the larger reasons for going through this work.
My broader interest lies in the theory of inquiry as a special application or a special case of the theory of signs. Another name for the theory of inquiry is ''logic'' and another name for the theory of signs is ''semiotics''. So I might as well have said that I am interested in logic as a special application or a special case of semiotics. But what sort of a special application? What sort of a special case? Well, I think of logic as ''formal semiotics'' — though, of course, I am not the first to have said such a thing — and by ''formal'' we say, in our etymological way, that logic is concerned with the ''form'', indeed, with the ''animate beauty'' and the very ''life force'' of signs and sign actions. Yes, perhaps that is far too Latin a way of understanding logic, but it's all I've got.
Now, if you think about these things just a little more, I know that you will find them just a little suspicious, for what besides logic would I use to do this theory of signs that I would apply to this theory of inquiry that I'm also calling ''logic''? But that is precisely one of the things signified by the word ''formal'', for what I'd be required to use would have to be some brand of logic, that is, some sort of innate or inured skill at inquiry, but a style of logic that is casual, catch-as-catch-can, formative, incipient, inchoate, unformalized, a work in progress, partially built into our natural language and partially more primitive than our most artless language. In so far as I use it more than mention it, mention it more than describe it, and describe it more than fully formalize it, then to that extent it must be consigned to the realm of unformalized and unreflective logic, where some say "there be oracles", but I don't know.
Still, one of the aims of formalizing what acts of reasoning that we can is to draw them into an arena where we can examine them more carefully, perhaps to get better at their performance than we can unreflectively, and thus to live, to formalize again another day. Formalization is not the be-all end-all of human life, not by a long shot, but it has its uses on that behalf.
This looks like a good place to pause and take stock. The question arises: What is really going on here? We have all these signs, but what is the object?
One object worth the candle is simply to study a non-trivial example of a syntactic system, simple in design but not entirely a toy, just to see how these systems tick.
More than that, we would like to understand how sign systems come to exist or can be placed in relation to object systems, in the likes of which we possess some compelling independent reason to take an interest.
What is the utility of setting up sets of strings and sets of graphs, and sorting them according to their ''semiotic equivalence class'' (SEC) based on this or that abstract notion of transformational equivalence?
Good questions.
I can but begin to address these questions in the present frame of work, but I can't hope to answer them in anything like a satisfactory fashion. Nevertheless, I will not mind one bit if you keep them in mind as we go.
==Analysis of contingent propositions==
For all of the reasons mentioned above, and for the sake of a more compact illustration of the in and outs of a typical propositional equation reasoning system (PERS), let's now take up a much simpler example of a contingent proposition:
o-----------------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` q o ` o r ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` | ` | ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` p o ` o p ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `(p (q)) (p (r))` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-----------------------------------------------------------o
For the sake of simplicity in discussing this example, I will revert to the existential interpretation (''Ex'') of logical graphs and their corresponding parse strings.
For the sake of simplicity in discussing this example, I will revert to the existential interpretation (''Ex'') of logical graphs and their corresponding parse strings.
Under ''Ex'' the expression "<math>(p\ (q))(p\ (r))\!</math>" interprets as the vernacular expression "<math>p\ \operatorname{implies}\ q\ \operatorname{and}\ p\ \operatorname{implies}\ r</math>", in symbols, <math>\{ p \Rightarrow q \} \land \{ p \Rightarrow r \},</math> so this is the reading that we'll want to keep in mind for the present.
Under ''Ex'' the expression "(p (q))(p (r))" interprets as the vernacular expression "''p'' implies ''q'' and ''p'' implies ''r''", in symbols, {''p'' ⇒ ''q''} ∧ ''p'' ⇒ ''r'', so this is the reading that we'll want to keep in mind for the present.
Where brevity is required, and it occasionally is, we may invoke the propositional expression "(p (q))(p (r))" under the name "''f''" by making use of the following definition: "f = (p (q))(p (r))".
Where brevity is required, and it occasionally is, we may invoke the propositional expression "(p (q))(p (r))" under the name "''f''" by making use of the following definition: "f = (p (q))(p (r))".
And that, of course, is the DNF of a theorem.
And that, of course, is the DNF of a theorem.
==Proof as semiosis==
We have been looking at several different ways of proving one particular example of a propositional equation, and along the way we have been exemplifying the species of sign transforming process that is commonly known as a ''proof'', more specifically, an equational proof of the propositional equation at issue.
Let us now draw out these semiotic features of the business of proof and place them in relief.
Our syntactic domain ''S'' contains an infinite number of signs or expressions, which we may choose to view in either their text or their graphic forms, glossing over for now the many details of their parsicular correspondence.
Here are some of the expressions that we find salient enough to single out and confer an epithetic nickname on:
: ''e''<sub>0</sub> = "( )"
: ''e''<sub>1</sub> = " "
: ''e''<sub>2</sub> = "(p (q))(p (r))"
: ''e''<sub>3</sub> = "(p (q r))"
: ''e''<sub>4</sub> = "(p q r, (p))"
: ''e''<sub>5</sub> = "(( (p (q))(p (r)) , (p (q r)) ))"
Under ''Ex'' we have the following interpretations:
: ''e''<sub>0</sub> expresses the logical constant "false"
: ''e''<sub>1</sub> expresses the logical constant "true"
: ''e''<sub>2</sub> says "not p without q, and not p without r"
: ''e''<sub>3</sub> says "not p without q and r"
: ''e''<sub>4</sub> says "p and q and r, or else not p"
: ''e''<sub>5</sub> says that ''e''<sub>2</sub> and ''e''<sub>3</sub> say the same thing
We took up the Equation ''E''<sub>1</sub> that reads as follows:
: (p (q))(p (r)) = (p (q r)).
Each of our proofs is a finite sequence of signs, and thus, for a finite integer n, takes the form:
: ''s''<sub>1</sub>, ''s''<sub>2</sub>, ''s''<sub>3</sub>, …, ''s''<sub>''n''</sub>.
Proof 1 proceeded by the ''straightforward approach'', starting with ''e''<sub>2</sub> as ''s''<sub>1</sub> and ending with ''e''<sub>3</sub> as ''s''<sub>''n''</sub>. That is, it commenced from the sign "(p (q))(p (r))" and ended up at the sign "(p (q r))" by legal moves.
Proof 2 lit on by ''burning the candle at both ends'', changing ''e''<sub>2</sub> into a normal form that reduced to ''e''<sub>4</sub>, and changing ''e''<sub>3</sub> into a normal form that also reduced to ''e''<sub>4</sub>, in this way tethering ''e''<sub>2</sub> and ''e''<sub>3</sub> to a common stake. In more detail, one route went from "(p (q))(p (r))" to "(p q r, (p))", and another went from "(p (q r))" to "(p q r, (p))", thus equating the two points of departure.
Proof 3 took the path of reflection, expressing the met-equation between ''e''<sub>2</sub> and ''e''<sub>3</sub> in the naturalized equation ''e''<sub>5</sub>, then taking ''e''<sub>5</sub> as ''s''<sub>1</sub> and exchanging it by dint of value preserving steps for ''e''<sub>1</sub> as ''s''<sub>''n''</sub>. Thus we went from "(( (p (q))(p (r)) , (p (q r)) ))" to the blank expression that ''Ex'' recognizes as the value ''true''.
Review:
* Pf 1. PERS 14. http://forum.wolframscience.com/showthread.php?postid=973#post973
* Pf 2a. PERS 15. http://forum.wolframscience.com/showthread.php?postid=976#post976
* Pf 2b. PERS 16. http://forum.wolframscience.com/showthread.php?postid=977#post977
* Pf 3. PERS 18. http://forum.wolframscience.com/showthread.php?postid=988#post988
==Computation and inference as semiosis==
Equational reasoning, as distinguished from implicational reasoning, is well-evolved in mathematics today but grievously short-schrifted in contemporary logic textbooks. Consequently, it may be advisable for me to draw out and place in relief some of the more distinctive characters of equational inference that may have passed beneath the notice of a casual reading of these notes.
By way of a very preliminary orientation, let us consider the distinction between an ''information maintaining process'' (IMP) and an ''information reducing process'' (IRP). To conform with prudent practice, let's make our first acquaintance with this difference in the medium of some concrete and simple examples.
* Example 1. Modus Ponens
: IRP Version:
: ''p'' ⇒ ''q''
: ''p''
: ––––––––
: ''q''
: IMP Version:
: ''p'' ⇒ ''q''
: ''p''
: ========
: ''p q''
Let us examine these two types of inference in a little more detail. A display of the form:
: ''Expression''<sub>1</sub>
: ''Expression''<sub>2</sub>
: ––––––––––––
: ''Expression''<sub>3</sub>
is used to state a ''rule of inference'' (ROI). The expressions above the line of inference are called ''premisses'' and the expression below the line is called a ''conclusion'', (also ''outcome'', ''result'', or ''upshot'').
If the ROI in question is succinct enough, one may write it in-line, as ''Premiss''<sub>1</sub>, ''Premiss''<sub>2</sub> |– ''Conclusion'', where the symbol "|–" is called the ''(proof-theoretic) turnstile''.
Either way, one reads such a ROI in the following manner: "From ''Expression''<sub>1</sub> and ''Expression''<sub>2</sub>, infer ''Expression''<sub>3</sub>".
Looking to our first Example, the ROI that is classically known as ''modus ponens'' says the following: If one has that ''p'' implies ''q'', and one has that ''p'' is true, then one has a ''way of putting it forward'' that q is true.
Modus ponens is an ''illative'' or ''implicational'' rule. Passage through its turnstile incurs the toll of some information loss, and thus from a fact of ''q'' alone one cannot infer with any degree of certainty that ''p'' ⇒ ''q'' and ''p'' are the reasons why ''q'' happens to be true.
Further considerations along these lines may lead us to appreciate the difference between ''implicational rules of inference'' (IROI's) and ''equational rules of inference'' (EROI's), the latter indicated by an ''equational line of inference'' (ELOI) or 2-way turnstile "|–|".
==Variations on a theme of transitivity==
The next Example is extremely important, and for reasons that reach well beyond the level of propositional calculus as it is ordinarily conceived. But it's slightly tricky to get all of the details right, so it will be worth taking the trouble to look at it from several different angles and as it appears in diverse frames, genres, or styles of representation.
In discussing this Example, it is convenient to observe that the implication relation that is ordinarily indicated by the propositional form ''x'' ⇒ ''y'' is equivalent to an order relation ''x'' ≤ ''y'' on boolean values, where 0 is taken to be less than 1.
* Example 2. Transitivity
: IRP Version:
: ''p'' ≤ ''q''
: ''q'' ≤ ''r''
: ––––––––
: ''p'' ≤ ''r''
: IMP Version:
: ''p'' ≤ ''q''
: ''q'' ≤ ''r''
: ============
: ''p'' ≤ ''q'' ≤ ''r''
In stating the IMP analogue of transitivity, I have taken advantage of a common idiom in the use of order relation symbols, one that represents their logical conjunction by way of a catenated syntax. Thus, ''p'' ≤ ''q'' ≤ ''r'' means that ''p'' ≤ ''q'' and that ''q'' ≤ ''r''. The claim that this 3-adic relation holds among the 3 propositions ''p'', ''q'', ''r'' is a stronger claim — contains more information — than the claim that the 2-adic relation ''p'' ≤ ''r'' holds between the 2 propositions ''p'' and ''r''.
To study the differences between these two versions of transitivity within what is locally a familiar context, let's view the propositional forms involved as if they were elementary cellular automaton rules, resulting in the following Table.
Table 21. Composite and Compiled Order Relations
o---------o------------o-----------------o----------------o-------------o
| L_1 ` ` | L_2 ` ` ` `| L_3 ` ` ` ` ` ` | L_4 ` ` ` ` ` `| L_5 ` ` ` ` |
| ` ` ` ` | ` ` ` ` ` `| ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` `| ` ` ` ` ` ` |
| Decimal | Binary` ` `| Vector` ` ` ` ` | Cactus` ` ` ` `| Order ` ` ` |
o---------o------------o-----------------o----------------o-------------o
| ` ` ` ` | ` ` ` ` `p : 1 1 1 1 0 0 0 0 | ` ` ` ` ` ` ` `| ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` `q : 1 1 0 0 1 1 0 0 | ` ` ` ` ` ` ` `| ` ` ` ` ` ` |
| ` ` ` ` | ` ` ` ` `r : 1 0 1 0 1 0 1 0 | ` ` ` ` ` ` ` `| ` ` ` ` ` ` |
o---------o------------o-----------------o----------------o-------------o
| ` ` ` ` | ` ` ` ` ` `| ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` `| ` ` ` ` ` ` |
| q_207 ` | q_11001111 | 1 1 0 0 1 1 1 1 | (p` `(q)) ` ` `| p =< q` ` ` |
| ` ` ` ` | ` ` ` ` ` `| ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` `| ` ` ` ` ` ` |
| q_187 ` | q_10111011 | 1 0 1 1 1 0 1 1 | ` ` `(q ` (r)) | q =< r` ` ` |
| ` ` ` ` | ` ` ` ` ` `| ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` `| ` ` ` ` ` ` |
| q_175 ` | q_10101111 | 1 0 1 0 1 1 1 1 | (p` ` ` ` (r)) | p =< r` ` ` |
| ` ` ` ` | ` ` ` ` ` `| ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` `| ` ` ` ` ` ` |
| q_139 ` | q_10001011 | 1 0 0 0 1 0 1 1 | (p (q))(q (r)) | p =< q =< r |
| ` ` ` ` | ` ` ` ` ` `| ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` `| ` ` ` ` ` ` |
o---------o------------o-----------------o----------------o-------------o
Taking up another angle of incidence by way of extra perspective, let us now reflect on the venn diagrams of our four propositions.
o-----------------------------------------------------------o
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^o-------------o^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^/` ` ` ` ` ` ` ` `\^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^/` ` ` ` ` ` ` ` ` ` `\^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^o` ` ` ` ` ` ` ` ` ` ` ` `o^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` P ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ o--o----------o ` o----------o--o ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^/^ ^ \ ^ ^ ^ ^ ^\`/` ` ` ` ` / ^ ^\^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ / ^ ^ ^\^ ^ ^ ^ ^ o ` ` ` ` `/^ ^ ^ \ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^/^ ^ ^ ^ \ ^ ^ ^ ^/^\` ` ` ` / ^ ^ ^ ^\^ ^ ^ ^ ^ |
| ^ ^ ^ ^ / ^ ^ ^ ^ ^\^ ^ ^ / ^ \ ` ` `/^ ^ ^ ^ ^ \ ^ ^ ^ ^ |
| ^ ^ ^ ^/^ ^ ^ ^ ^ ^ \ ^ ^/^ ^ ^\` ` / ^ ^ ^ ^ ^ ^\^ ^ ^ ^ |
| ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^o--o-------o--o^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ Q ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ R ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ |
| ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^ ^\^ ^ ^/^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ |
| ^ ^ ^ ^ \ ^ ^ ^ ^ ^ ^ ^ ^ \ ^ / ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ |
| ^ ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^ ^\^/^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ \ ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^/^\^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ o-------------o ^ o-------------o ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
o-----------------------------------------------------------o
q_207. (p (q))
o-----------------------------------------------------------o
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^o-------------o^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ ^ ^ ^ \ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ ^ ^ ^ ^ ^ \ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ \ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^o^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^o^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|^ ^ ^ ^ ^ ^ P ^ ^ ^ ^ ^ ^|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ o--o----------o ^ o----------o--o ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^/` ` \ ` ` ` ` `\^/^ ^ ^ ^ ^ / ^ ^\^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ / ` ` `\` ` ` ` ` o ^ ^ ^ ^ ^/^ ^ ^ \ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^/` ` ` ` \ ` ` ` `/^\^ ^ ^ ^ / ^ ^ ^ ^\^ ^ ^ ^ ^ |
| ^ ^ ^ ^ / ` ` ` ` `\` ` ` / ^ \ ^ ^ ^/^ ^ ^ ^ ^ \ ^ ^ ^ ^ |
| ^ ^ ^ ^/` ` ` ` ` ` \ ` `/^ ^ ^\^ ^ / ^ ^ ^ ^ ^ ^\^ ^ ^ ^ |
| ^ ^ ^ o ` ` ` ` ` ` `o--o-------o--o^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ |
| ^ ^ ^ | ` ` ` ` ` ` ` ` | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ` ` ` ` ` ` ` ` | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ` ` ` ` ` ` ` ` | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ` ` ` Q ` ` ` ` | ^ ^ ^ | ^ ^ ^ ^ R ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ` ` ` ` ` ` ` ` | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ o ` ` ` ` ` ` ` ` o ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ |
| ^ ^ ^ ^\` ` ` ` ` ` ` ` `\^ ^ ^/^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ |
| ^ ^ ^ ^ \ ` ` ` ` ` ` ` ` \ ^ / ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ |
| ^ ^ ^ ^ ^\` ` ` ` ` ` ` ` `\^/^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ \ ` ` ` ` ` ` ` ` o ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^\` ` ` ` ` ` ` `/^\^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ o-------------o ^ o-------------o ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
o-----------------------------------------------------------o
q_187. (q (r))
o-----------------------------------------------------------o
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^o-------------o^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^/` ` ` ` ` ` ` ` `\^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^/` ` ` ` ` ` ` ` ` ` `\^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^o` ` ` ` ` ` ` ` ` ` ` ` `o^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` P ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ o--o----------o ` o----------o--o ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^/^ ^ \ ` ` ` ` `\`/^ ^ ^ ^ ^ / ^ ^\^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ / ^ ^ ^\` ` ` ` ` o ^ ^ ^ ^ ^/^ ^ ^ \ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^/^ ^ ^ ^ \ ` ` ` `/^\^ ^ ^ ^ / ^ ^ ^ ^\^ ^ ^ ^ ^ |
| ^ ^ ^ ^ / ^ ^ ^ ^ ^\` ` ` / ^ \ ^ ^ ^/^ ^ ^ ^ ^ \ ^ ^ ^ ^ |
| ^ ^ ^ ^/^ ^ ^ ^ ^ ^ \ ` `/^ ^ ^\^ ^ / ^ ^ ^ ^ ^ ^\^ ^ ^ ^ |
| ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^o--o-------o--o^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ Q ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ R ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ |
| ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^ ^\^ ^ ^/^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ |
| ^ ^ ^ ^ \ ^ ^ ^ ^ ^ ^ ^ ^ \ ^ / ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ |
| ^ ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^ ^\^/^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ \ ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^\^ ^ ^ ^ ^ ^ ^ ^/^\^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ o-------------o ^ o-------------o ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
o-----------------------------------------------------------o
q_175. (p (r))
o-----------------------------------------------------------o
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^o-------------o^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^/` ` ` ` ` ` ` ` `\^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^/` ` ` ` ` ` ` ` ` ` `\^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ / ` ` ` ` ` ` ` ` ` ` ` \ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^o` ` ` ` ` ` ` ` ` ` ` ` `o^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` P ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^|` ` ` ` ` ` ` ` ` ` ` ` `|^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ o--o----------o ` o----------o--o ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^/` ` \ ` ` ` ` `\`/` ` ` ` ` / ^ ^\^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ / ` ` `\` ` ` ` ` o ` ` ` ` `/^ ^ ^ \ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^/` ` ` ` \ ` ` ` `/^\` ` ` ` / ^ ^ ^ ^\^ ^ ^ ^ ^ |
| ^ ^ ^ ^ / ` ` ` ` `\` ` ` / ^ \ ` ` `/^ ^ ^ ^ ^ \ ^ ^ ^ ^ |
| ^ ^ ^ ^/` ` ` ` ` ` \ ` `/^ ^ ^\` ` / ^ ^ ^ ^ ^ ^\^ ^ ^ ^ |
| ^ ^ ^ o ` ` ` ` ` ` `o--o-------o--o^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ |
| ^ ^ ^ | ` ` ` ` ` ` ` ` | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ` ` ` ` ` ` ` ` | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ` ` ` ` ` ` ` ` | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ` ` ` Q ` ` ` ` | ^ ^ ^ | ^ ^ ^ ^ R ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ | ` ` ` ` ` ` ` ` | ^ ^ ^ | ^ ^ ^ ^ ^ ^ ^ ^ | ^ ^ ^ |
| ^ ^ ^ o ` ` ` ` ` ` ` ` o ^ ^ ^ o ^ ^ ^ ^ ^ ^ ^ ^ o ^ ^ ^ |
| ^ ^ ^ ^\` ` ` ` ` ` ` ` `\^ ^ ^/^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ |
| ^ ^ ^ ^ \ ` ` ` ` ` ` ` ` \ ^ / ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ |
| ^ ^ ^ ^ ^\` ` ` ` ` ` ` ` `\^/^ ^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ \ ` ` ` ` ` ` ` ` o ^ ^ ^ ^ ^ ^ ^ ^ / ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^\` ` ` ` ` ` ` `/^\^ ^ ^ ^ ^ ^ ^ ^/^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ o-------------o ^ o-------------o ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
| ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ ^ |
o-----------------------------------------------------------o
q_139. (p (q))(q (r))
Among other things, these images make it visually obvious that the constraint on the three boolean variables ''p'', ''q'', ''r'' that we indicate by asserting either of the forms "(p (q))(q (r))" or "''p'' ≤ ''q'' ≤ ''r''" is one that implies a constraint on the two boolean variables ''p'', ''r'' that we indicate by either of the forms "(p (r))" or "''p'' ≤ ''r''", but that it imposes additional constraints on these variables that are not captured by the illative conclusion.
One way to view a proposition ''f'' : '''B'''<sup>''k''</sup> → '''B''' is to consider its ''fiber of truth'', ''f''<sup>−1</sup>(1) ⊆ '''B'''<sup>''k''</sup>, and to regard it as a ''k''-adic relation ''L'' ⊆ '''B'''<sup>''k''</sup>.
By way of general definition, the ''fiber'' of a function ''f'' : ''X'' → ''Y'' at a given value ''y'' of its co-domain ''Y'' is the ''antecedent'' (pre-image or inverse image) of ''y'' under ''f''. This is a subset, possibly empty, of the domain ''X'', notated as ''f''<sup>−1</sup>(''y'') ⊆ ''X''.
In particular, if ''f'' is a proposition ''f'' : ''X'' → '''B''', then we think of ''f''<sup>−1</sup>(''y'') as the subset of ''X'' that is ''indicated'' by the proposition ''f''. Whenever we ''assert'' a proposition ''f'' : ''X'' → '''B''', we are saying that what it indicates is all that happens to be the case in the relevant universe of discourse ''X''. Because the special case of the fiber of truth is used so often in logical contexts, we will sometimes use the notation <nowiki>[|</nowiki>''f''<nowiki>|]</nowiki> = ''f''<sup>−1</sup>(1).
Using this panoply of notions and notations, we may treat the fiber of truth of each proposition ''f'' : '''B'''<sup>3</sup> → '''B''' as if it were a relational data table of the shape {(''p'', ''q'', ''r'')} ⊆ '''B'''<sup>3</sup>, where the (''p'', ''q'', ''r'') are bit vectors indicated by the proposition ''f''.
Thus we obtain the following four relational data tables for the propositions that we are looking at in Example 2.
[| q_207 |] = [| p =< q |]
o---------o---------o---------o
|` ` p ` `|` ` q ` `|` ` r ` `|
o---------o---------o---------o
|` ` 0 ` ` ` ` 0 ` ` ` ` 0 ` `|
|` ` 0 ` ` ` ` 0 ` ` ` ` 1 ` `|
|` ` 0 ` ` ` ` 1 ` ` ` ` 0 ` `|
|` ` 0 ` ` ` ` 1 ` ` ` ` 1 ` `|
|` ` 1 ` ` ` ` 1 ` ` ` ` 0 ` `|
|` ` 1 ` ` ` ` 1 ` ` ` ` 1 ` `|
o-----------------------------o
[| q_187 |] = [| q =< r |]
o---------o---------o---------o
|` ` p ` `|` ` q ` `|` ` r ` `|
o---------o---------o---------o
|` ` 0 ` ` ` ` 0 ` ` ` ` 0 ` `|
|` ` 0 ` ` ` ` 0 ` ` ` ` 1 ` `|
|` ` 0 ` ` ` ` 1 ` ` ` ` 1 ` `|
|` ` 1 ` ` ` ` 0 ` ` ` ` 0 ` `|
|` ` 1 ` ` ` ` 0 ` ` ` ` 1 ` `|
|` ` 1 ` ` ` ` 1 ` ` ` ` 1 ` `|
o-----------------------------o
[| q_175 |] = [| p =< r |]
o---------o---------o---------o
|` ` p ` `|` ` q ` `|` ` r ` `|
o---------o---------o---------o
|` ` 0 ` ` ` ` 0 ` ` ` ` 0 ` `|
|` ` 0 ` ` ` ` 0 ` ` ` ` 1 ` `|
|` ` 0 ` ` ` ` 1 ` ` ` ` 0 ` `|
|` ` 0 ` ` ` ` 1 ` ` ` ` 1 ` `|
|` ` 1 ` ` ` ` 0 ` ` ` ` 1 ` `|
|` ` 1 ` ` ` ` 1 ` ` ` ` 1 ` `|
o-----------------------------o
[| q_139 |] = [| p =< q =< r |]
o---------o---------o---------o
|` ` p ` `|` ` q ` `|` ` r ` `|
o---------o---------o---------o
|` ` 0 ` ` ` ` 0 ` ` ` ` 0 ` `|
|` ` 0 ` ` ` ` 0 ` ` ` ` 1 ` `|
|` ` 0 ` ` ` ` 1 ` ` ` ` 1 ` `|
|` ` 1 ` ` ` ` 1 ` ` ` ` 1 ` `|
o-----------------------------o
In the medium of these unassuming examples, we begin to see the activities of logical inference and methodical inquiry as ''information clarifying operations'' (ICO's).
First, we drew a distinction between information maintaining and information reducing processes and we noted the related distinction between equational and implicational inferences. I will use the acronyms EROI and IROI, respectively, for the equational and implicational analogues of the various rules of inference.
For example, we considered the brands of ''information fusion'' that are involved in a couple of standard rules of inference, taken in both their equational and their illative variants.
In particular, let us assume that we begin from a state of uncertainty about the universe of discourse ''X'' = '''B'''<sup>3</sup> that is standardly represented by a uniform distribution ''u'' : ''X'' → '''B''' such that ''u''(''x'') = 1 for all ''x'' in ''X'', in short, by the constant proposition 1 : ''X'' → '''B'''. This amounts to the ''maximum entropy sign state'' (MESS). As a measure of uncertainty, let us use either the multiplicative measure given by the cardinality of ''X'', commonly notated as |''X''|, or else the additive measure given by log |X|. In this frame we have |''X''| = 8 and log |''X''| = 3, to wit, 3 bits of doubt.
Let us now consider the various rules of inference for transitivity in the light of their performance as information-developing actions.
* Transitive Law (IROI)
: ''p'' ≤ ''q''
: ''q'' ≤ ''r''
: ––––––––
: ''p'' ≤ ''r''
* By itself, the information ''p'' ≤ ''q'' would reduce our uncertainty from log 8 bits to log 6 bits.
* By itself, the information ''q'' ≤ ''r'' would reduce our uncertainty from log 8 bits to log 6 bits.
* By itself, the information ''p'' ≤ ''r'' would reduce our uncertainty from log 8 bits to log 6 bits.
In this situation, the application of the IROI for transitivity to the information ''p'' ≤ ''q'' and the information ''q'' ≤ ''r'' to get the information ''p'' ≤ ''r'' does not increase the measure of information beyond what any one of the three propositions has independently of the other two. In a sense, then, this IROI operates only to move the information around without changing its measure in the slightest bit.
* Transitive Law (EROI)
: ''p'' ≤ ''q''
: ''q'' ≤ ''r''
: ============
: ''p'' ≤ ''q'' ≤ ''r''
The contents and the measures of information that are associated with the propositions ''p'' ≤ ''q'' and ''q'' ≤ ''r'' are the same as before.
On its own, the information ''p'' ≤ ''q'' ≤ ''r'' would reduce our uncertainty from log(8) = 3 bits to log(4) = 2 bits, a reduction of 1 bit.
These are just some of the initial observations that can be made about the dimensions of information and uncertainty in the conduct of logical inference, and there are many issues to be taken up as we get to the thick of it. In particular, we are taking propositions far too literally at the outset, reading their spots at face value, as it were, without yet considering their species character as fallible signs.
For ease of reference during the rest of this discussion, let us refer to the propositional form ''f'' : '''B'''<sup>3</sup> → '''B''' such that ''f''(''p'', ''q'', ''r'') = ''q''<sub>139</sub>(''p'', ''q'', ''r'') = (p (q))(q (r)) as the ''syllogism mapping'', written as ''syll'' : '''B'''<sup>3</sup> → '''B''', and let us refer to the fiber ''syll''<sup>−1</sup>(1) ⊆ '''B'''<sup>3</sup> as the ''syllogism relation'', written as ''Syll'' ⊆ '''B'''<sup>3</sup>. Table 25-a shows ''Syll'' as a relational dataset.
Table 25-a. Syllogism Relation
o---------o---------o---------o
|` ` p ` `|` ` q ` `|` ` r ` `|
o---------o---------o---------o
|` ` 0 ` ` ` ` 0 ` ` ` ` 0 ` `|
|` ` 0 ` ` ` ` 0 ` ` ` ` 1 ` `|
|` ` 0 ` ` ` ` 1 ` ` ` ` 1 ` `|
|` ` 1 ` ` ` ` 1 ` ` ` ` 1 ` `|
o-----------------------------o
One of the first questions that we might ask about a 3-adic relation, in this case ''Syll'', is whether it is ''determined by'' its 2-adic projections. I will illustrate what this means in the present case.
Table 25-b repeats the relation ''Syll'' in the first column, listing its 3-tuples in bit-string form, followed by the 2-adic or ''planar'' projections of ''Syll'' in the next three columns. For instance, ''Syll''<sub>''pq''</sub> is the 2-adic projection of ''Syll'' on the ''pq'' plane that is arrived at by deleting the ''r'' column and counting each 2-tuple that results just one time. Likewise, ''Syll''<sub>''pr''</sub> is obtained by deleting the ''q'' column and ''Syll''<sub>''qr''</sub> is derived by deleting the p column, ignoring whatever duplicate pairs may result. The final row of the right three columns gives the propositions of the form ''f'' : '''B'''<sup>2</sup> → '''B''' that indicate the 2-adic relations that result from these projections.
Table 25-b. Dyadic Projections of the Syllogism Relation
o-------------o-------------o-------------o-------------o
| ` `Syll ` ` | ` Syll_pq ` | ` Syll_pr ` | ` Syll_qr ` |
o-------------o-------------o-------------o-------------o
| ` ` 000 ` ` | ` ` 00 ` ` `| ` ` 00 ` ` `| ` ` 00 ` ` `|
| ` ` 001 ` ` | ` ` 00 ` ` `| ` ` 01 ` ` `| ` ` 01 ` ` `|
| ` ` 011 ` ` | ` ` 01 ` ` `| ` ` 01 ` ` `| ` ` 11 ` ` `|
| ` ` 111 ` ` | ` ` 11 ` ` `| ` ` 11 ` ` `| ` ` 11 ` ` `|
o-------------o-------------o-------------o-------------o
| p =< q =< r | ` (p (q)) ` | ` (p (r)) ` | ` (q (r)) ` |
o-------------o-------------o-------------o-------------o
Let us make the simple observation that taking a projection, in our framework, deleting a column from a relational table, is like taking a derivative in differential calculus. What it means is that our attempt to return to the integral from whence the derivative was derived will in general encounter an indefinite variation on account of the circumstance that real information may have been destroyed by the derivation.
One will find that some relations can be reconstructed from various types of derivatives and projections, others cannot. The reconstuctible relations are said to be ''reducible'' to the types of reductive data in question, while the others are said to be ''irreducible'' with respect to those means.
The analogies between derivation, differentiation, implication, projection, and others sorts of information reducing operation will undergo extensive development in the remainder and sequel of the present discussion.
We were in the middle of discussing the relationships between information preserving rules of inference and information destroying rules of inference — folks of a 3-basket philosophical bent will no doubt be asking, "And what of information creating rules of inference?", but there I must wait for some signs of enlightenment, desiring not to tread on the rules of that succession.
The contrast between the information destroying and the information preserving versions of the transitive rule of inference led us to examine the relationships among several boolean functions, namely, those that qualify locally as the elementary cellular automata rules ''q''<sub>139</sub>, ''q''<sub>175</sub>, ''q''<sub>187</sub>, ''q''<sub>207</sub>.
The function ''q''<sub>139</sub> : '''B'''<sup>3</sup> → '''B''' and its fiber <nowiki>[|</nowiki> ''q''<sub>139</sub> <nowiki>|]</nowiki> ⊆ '''B'''<sup>3</sup> appeared to be key to many structures in this setting, and so I singled them out under the new names of ''syll'' : '''B'''<sup>3</sup> → '''B''' and ''Syll'' ⊆ '''B'''<sup>3</sup>, respectively.
Managing the conceptual complexity of our considerations at this juncture put us in need of some conceptual tools that I broke off to develop in my notes on "Reductions Among Relations". The main items that we need right away from that thread are the definitions of relational projections and their inverses, the tacit extensions.
But the more I survey the problem setting the more it looks like we need better ways to bring our visual intuitions to play on the scene, and so I want next to lay out some visual schemata that are designed to facilitate that.
Figure 28-a shows the familiar picture of a boolean 3-cube, wherein the points of '''B'''<sup>3</sup> are coordinated as bit strings of length three. Looking at the functions ''f'' : '''B'''<sup>3</sup> → '''B''' and the relations ''L'' ⊆ '''B'''<sup>3</sup> on this pattern, one views the construction of either type of object as a matter of coloring the nodes of the 3-cube with choices from a pair of colors that stipulate which points are in the relation ''L'' = <nowiki>[|</nowiki>''f''<nowiki>|]</nowiki> and which points are out of it. Bowing to common convention, we may use the color "1" for points that are "in" a given relation and the color "0" for points that are "out" of that same relation. However, it will be more convenient here to indicate the former case by writing the coordinates in the place of the node and to indicate the latter case by plotting the point as an unlabeled node "o".
o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 111 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` /|\ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `/`|`\` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` / `|` \ ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `/` `|` `\` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` / ` `|` ` \ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `/` ` `|` ` `\` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` / ` ` `|` ` ` \ ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` 110 ` ` 101 ` ` 011 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|\ ` ` / \ ` ` /|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`\` `/` `\` `/`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` \ / ` ` \ / `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` `\` ` ` `/` `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` / \ ` ` / \ `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`/` `\` `/` `\`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|/ ` ` \ / ` ` \|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` 100 ` ` 010 ` ` 001 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` `|` ` ` / ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` `|` ` `/` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ ` `|` ` / ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `|` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ `|` / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\`|`/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \|/ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 000 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
Figure 28-a. Boolean 3-Cube B^3
Table 28-b shows the 3-adic relation ''Syll'' ⊆ '''B'''<sup>3</sup> again, and Figure 28-c shows it plotted on a 3-cube template.
Table 28-b. Syll c B^3
o-----------------------o
| ` p ` ` ` q ` ` ` r ` |
o-----------------------o
| ` 0 ` ` ` 0 ` ` ` 0 ` |
| ` 0 ` ` ` 0 ` ` ` 1 ` |
| ` 0 ` ` ` 1 ` ` ` 1 ` |
| ` 1 ` ` ` 1 ` ` ` 1 ` |
o-----------------------o
o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 111 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` /|\ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `/`|`\` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` / `|` \ ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `/` `|` `\` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` / ` `|` ` \ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `/` ` `|` ` `\` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` / ` ` `|` ` ` \ ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` `o` ` ` 011 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|\ ` ` / \ ` ` /|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`\` `/` `\` `/`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` \ / ` ` \ / `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` `\` ` ` `/` `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` / \ ` ` / \ `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`/` `\` `/` `\`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|/ ` ` \ / ` ` \|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` `o` ` ` 001 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` `|` ` ` / ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` `|` ` `/` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ ` `|` ` / ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `|` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ `|` / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\`|`/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \|/ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 000 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
Figure 28-c. Triadic Relation Syll c B^3
We return once more to the plane projections of ''Syll'' ⊆ '''B'''<sup>3</sup>.
Table 29-a. Syll c B^3
o-----------------------o
| ` p ` ` ` q ` ` ` r ` |
o-----------------------o
| ` 0 ` ` ` 0 ` ` ` 0 ` |
| ` 0 ` ` ` 0 ` ` ` 1 ` |
| ` 0 ` ` ` 1 ` ` ` 1 ` |
| ` 1 ` ` ` 1 ` ` ` 1 ` |
o-----------------------o
Table 29-b. Dyadic Projections of Syll
o-----------o o-----------o o-----------o
| `Syll_12` | | `Syll_13` | | `Syll_23` |
o-----------o o-----------o o-----------o
| ` p ` q ` | | ` p ` r ` | | ` q ` r ` |
o-----------o o-----------o o-----------o
| ` 0 ` 0 ` | | ` 0 ` 0 ` | | ` 0 ` 0 ` |
| ` 0 ` 1 ` | | ` 0 ` 1 ` | | ` 0 ` 1 ` |
| ` 1 ` 1 ` | | ` 1 ` 1 ` | | ` 1 ` 1 ` |
o-----------o o-----------o o-----------o
| `(p (q))` | | `(p (r))` | | `(q (r))` |
o-----------o o-----------o o-----------o
In showing the 2-adic projections of a 3-adic relation ''L'' ⊆ '''B'''<sup>3</sup>, I will translate the coordinates of the points in each relation to the plane of the projection, there dotting out with a dot "." the bit of the bit string that is out of place on that plane.
Figure 29-c shows ''Syll'' and its three 2-adic projections:
o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 111 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` /|\ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `/`|`\` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` / `|` \ ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `/` `|` `\` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` / ` `|` ` \ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `/` ` `|` ` `\` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` / ` ` `|` ` ` \ ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` `o` ` ` 011 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|\ ` ` / \ ` ` /|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`\` `/` `\` `/`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` \ / ` ` \ / `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` `\` ` ` `/` `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` / \ ` ` / \ `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`/` `\` `/` `\`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|/ ` ` \ / ` ` \|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` `o` ` ` 001 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` `|` ` ` / ` ` ` ` ` ` ` ` |
| ` ` 11. ` ` ` ` `\` ` `|` ` `/` ` ` ` ` .11 ` ` |
| ` ` `|\ ` ` ` ` ` \ ` `|` ` / ` ` ` ` ` /|` ` ` |
| ` ` `|`\` ` ` ` ` `\` `|` `/` ` ` ` ` `/`|` ` ` |
| ` ` `|` \ ` ` ` ` ` \ `|` / ` ` ` ` ` / `|` ` ` |
| ` ` `|` `\` ` ` ` ` `\`|`/` ` ` ` ` `/` `|` ` ` |
| ` ` `|` ` \ ` ` ` ` ` \|/ ` ` ` ` ` / ` `|` ` ` |
| ` ` `|` ` `\` ` ` ` ` 000 ` ` ` ` `/` ` `|` ` ` |
| ` ` `|` ` ` \ ` ` ` ` ` ` ` ` ` ` / ` ` `|` ` ` |
| ` ` `o` ` ` 01. ` ` ` ` ` ` ` ` `o` ` ` .01 ` ` |
| ` ` ` \ ` ` `|` ` ` ` ` ` ` ` ` `|` ` ` / ` ` ` |
| ` ` ` `\` ` `|` ` ` ` ` ` ` ` ` `|` ` `/` ` ` ` |
| ` ` ` ` \ ` `|` ` ` ` ` ` ` ` ` `|` ` / ` ` ` ` |
| ` ` ` ` `\` `|` ` ` ` 1.1 ` ` ` `|` `/` ` ` ` ` |
| ` ` ` ` ` \ `|` ` ` ` / \ ` ` ` `|` / ` ` ` ` ` |
| ` ` ` ` ` `\`|` ` ` `/` `\` ` ` `|`/` ` ` ` ` ` |
| ` ` ` ` ` ` \|` ` ` / ` ` \ ` ` `|/ ` ` ` ` ` ` |
| ` ` ` ` ` ` 00. ` `/` ` ` `\` ` .00 ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` / ` ` ` ` \ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `/` ` ` ` ` `\` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` / ` ` ` ` ` ` \ ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` 0.1 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 0.0 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
Figure 29-c. Syll c B^3 and its Dyadic Projections
We now compute the tacit extensions of the 2-adic projections of ''Syll'', alias ''q''<sub>139</sub>, and this makes manifest its relationship to the other functions and fibers, namely, ''q''<sub>175</sub>, ''q''<sub>187</sub>, ''q''<sub>207</sub>.
Table 30-a. Syll c B^3
o-----------------------o
| ` p ` ` ` q ` ` ` r ` |
o-----------------------o
| ` 0 ` ` ` 0 ` ` ` 0 ` |
| ` 0 ` ` ` 0 ` ` ` 1 ` |
| ` 0 ` ` ` 1 ` ` ` 1 ` |
| ` 1 ` ` ` 1 ` ` ` 1 ` |
o-----------------------o
Table 30-b. Dyadic Projections of Syll
o-----------o o-----------o o-----------o
| `Syll_12` | | `Syll_13` | | `Syll_23` |
o-----------o o-----------o o-----------o
| ` p ` q ` | | ` p ` r ` | | ` q ` r ` |
o-----------o o-----------o o-----------o
| ` 0 ` 0 ` | | ` 0 ` 0 ` | | ` 0 ` 0 ` |
| ` 0 ` 1 ` | | ` 0 ` 1 ` | | ` 0 ` 1 ` |
| ` 1 ` 1 ` | | ` 1 ` 1 ` | | ` 1 ` 1 ` |
o-----------o o-----------o o-----------o
| `(p (q))` | | `(p (r))` | | `(q (r))` |
o-----------o o-----------o o-----------o
Table 30-c. Tacit Extensions of Projections of Syll
o---------------o o---------------o o---------------o
| `TE(Syll_12)` | | `TE(Syll_13)` | | `TE(Syll_23)` |
o---------------o o---------------o o---------------o
| ` p ` q ` r ` | | ` p ` q ` r ` | | ` p ` q ` r ` |
o---------------o o---------------o o---------------o
| ` 0 ` 0 ` 0 ` | | ` 0 ` 0 ` 0 ` | | ` 0 ` 0 ` 0 ` |
| ` 0 ` 0 ` 1 ` | | ` 0 ` 1 ` 0 ` | | ` 1 ` 0 ` 0 ` |
| ` 0 ` 1 ` 0 ` | | ` 0 ` 0 ` 1 ` | | ` 0 ` 0 ` 1 ` |
| ` 0 ` 1 ` 1 ` | | ` 0 ` 1 ` 1 ` | | ` 1 ` 0 ` 1 ` |
| ` 1 ` 1 ` 0 ` | | ` 1 ` 0 ` 1 ` | | ` 0 ` 1 ` 1 ` |
| ` 1 ` 1 ` 1 ` | | ` 1 ` 1 ` 1 ` | | ` 1 ` 1 ` 1 ` |
o---------------o o---------------o o---------------o
| [| (p (q)) |] | | [| (p (r)) |] | | [| (q (r)) |] |
o---------------o o---------------o o---------------o
| [| `q_207` |] | | [| `q_175` |] | | [| `q_187` |] |
o---------------o o---------------o o---------------o
o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 111 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` /|\ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `/`|`\` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` / `|` \ ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `/` `|` `\` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` / ` `|` ` \ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `/` ` `|` ` `\` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` / ` ` `|` ` ` \ ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` 110 ` ` `o` ` ` 011 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|\ ` ` / \ ` ` /|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`\` `/` `\` `/`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` \ / ` ` \ / `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` `\` ` ` `/` `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` / \ ` ` / \ `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`/` `\` `/` `\`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|/ ` ` \ / ` ` \|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` 010 ` ` 001 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` `|` ` ` / ` ` ` ` ` ` ` ` |
| ` ` 11. ` ` ` ` `\` ` `|` ` `/` ` ` ` ` ` ` ` ` |
| ` ` `|\ ` ` ` ` ` \ ` `|` ` / ` ` ` ` ` ` ` ` ` |
| ` ` `|`\` ` ` ` ` `\` `|` `/` ` ` ` ` ` ` ` ` ` |
| ` ` `|` \ ` ` ` ` ` \ `|` / ` ` ` ` ` ` ` ` ` ` |
| ` ` `|` `\` ` ` ` ` `\`|`/` ` ` ` ` ` ` ` ` ` ` |
| ` ` `|` ` \ ` ` ` ` ` \|/ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` `|` ` `\` ` ` ` ` 000 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` `|` ` ` \ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` `o` ` ` 01. ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` \ ` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` `\` ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` \ ` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` `\` `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` \ `|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` `\`|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` \|` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` 00. ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
Figure 30-d. Tacit Extension TE_12_3 (Syll_12)
o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 111 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` /|\ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `/`|`\` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` / `|` \ ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `/` `|` `\` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` / ` `|` ` \ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `/` ` `|` ` `\` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` / ` ` `|` ` ` \ ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` 101 ` ` 011 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|\ ` ` / \ ` ` /|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`\` `/` `\` `/`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` \ / ` ` \ / `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` `\` ` ` `/` `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` / \ ` ` / \ `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`/` `\` `/` `\`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|/ ` ` \ / ` ` \|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` 010 ` ` 001 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` `|` ` ` / ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` `|` ` `/` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ ` `|` ` / ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `|` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ `|` / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\`|`/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \|/ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 000 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 1.1 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` / \ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `/` `\` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` / ` ` \ ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `/` ` ` `\` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` / ` ` ` ` \ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `/` ` ` ` ` `\` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` / ` ` ` ` ` ` \ ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` 0.1 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 0.0 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
Figure 30-e. Tacit Extension TE_13_2 (Syll_13)
o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 111 ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` /|\ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `/`|`\` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` / `|` \ ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `/` `|` `\` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` / ` `|` ` \ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `/` ` `|` ` `\` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` / ` ` `|` ` ` \ ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` 101 ` ` 011 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|\ ` ` / \ ` ` /|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`\` `/` `\` `/`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` \ / ` ` \ / `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` `\` ` ` `/` `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|` / \ ` ` / \ `|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|`/` `\` `/` `\`|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `|/ ` ` \ / ` ` \|` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` 100 ` ` `o` ` ` 001 ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` `|` ` ` / ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` `|` ` `/` ` ` ` ` .11 ` ` |
| ` ` ` ` ` ` ` ` ` \ ` `|` ` / ` ` ` ` ` /|` ` ` |
| ` ` ` ` ` ` ` ` ` `\` `|` `/` ` ` ` ` `/`|` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ `|` / ` ` ` ` ` / `|` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\`|`/` ` ` ` ` `/` `|` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \|/ ` ` ` ` ` / ` `|` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` 000 ` ` ` ` `/` ` `|` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` / ` ` `|` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `o` ` ` .01 ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` / ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` `/` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `|` ` / ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `|` `/` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `|` / ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `|`/` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `|/ ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` .00 ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
Figure 30-f. Tacit Extension TE_23_1 (Syll_23)
The reader may wish to contemplate Figure 31 and use it to verify the following two facts:
: ''Syll'' = ''TE''(''Syll''<sub>12</sub>) ∩ ''TE''(''Syll''<sub>23</sub>)
: ''Syll''<sub>13</sub> = ''Syll''<sub>12</sub> ο ''Syll''<sub>23</sub>
o-------------------------------------------------o
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `*` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` /|\ ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `/`|`\` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` / `|` \ ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `/` `|` `\` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` / ` `|` ` \ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `/` ` `|` ` `\` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` / ` ` `|` ` ` \ ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` `o` ` ` `*` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` /|\ ` ` / \ ` ` /|\ ` ` ` ` ` ` ` |
| ` ` ` ` ` ` `/`|`\` `/` `\` `/`|`\` ` ` ` ` ` ` |
| ` ` ` ` ` ` / `|` \ / ` ` \ / `|` \ ` ` ` ` ` ` |
| ` ` ` ` ` `/` `|` `\` ` ` `/` `|` `\` ` ` ` ` ` |
| ` ` ` ` ` / ` `|` / \ ` ` / \ `|` ` \ ` ` ` ` ` |
| ` ` ` ` `/` ` `|`/` `\` `/` `\`|` ` `\` ` ` ` ` |
| ` ` ` ` / ` ` `|/ ` ` \ / ` ` \|` ` ` \ ` ` ` ` |
| ` ` ` `/` ` ` `o` ` ` `o` ` ` `*` ` ` `\` ` ` ` |
| ` ` ` / ` ` ` ` \ ` ` /|` ` ` / \ ` ` ` \ ` ` ` |
| ` ` `*` ` ` ` ` `\` `/`|` ` `/` `\` ` ` `*` ` ` |
| ` ` `|\ ` ` ` ` ` \ / `|` ` / ` ` \ ` ` /|` ` ` |
| ` ` `|`\` ` ` ` ` `/` `|` `/` ` ` `\` `/`|` ` ` |
| ` ` `|` \ ` ` ` ` / \ `|` / ` ` ` ` \ / `|` ` ` |
| ` ` `|` `\` ` ` `/` `\`|`/` ` ` ` ` `/` `|` ` ` |
| ` ` `|` ` \ ` ` / ` ` \|/ ` ` ` ` ` / \ `|` ` ` |
| ` ` `|` ` `\` `/` ` ` `*` ` ` ` ` `/` `\`|` ` ` |
| ` ` `|` ` ` \ / ` ` ` / \ ` ` ` ` / ` ` \|` ` ` |
| ` ` `o` ` ` `*` ` ` `/` `\` ` ` `o` ` ` `*` ` ` |
| ` ` ` \ ` ` `|` ` ` / ` ` \ ` ` `|` ` ` / ` ` ` |
| ` ` ` `\` ` `|` ` `/` ` ` `\` ` `|` ` `/` ` ` ` |
| ` ` ` ` \ ` `|` ` / ` ` ` ` \ ` `|` ` / ` ` ` ` |
| ` ` ` ` `\` `|` `/` ` `*` ` `\` `|` `/` ` ` ` ` |
| ` ` ` ` ` \ `|` / ` ` / \ ` ` \ `|` / ` ` ` ` ` |
| ` ` ` ` ` `\`|`/` ` `/` `\` ` `\`|`/` ` ` ` ` ` |
| ` ` ` ` ` ` \|/ ` ` / ` ` \ ` ` \|/ ` ` ` ` ` ` |
| ` ` ` ` ` ` `*` ` `/` ` ` `\` ` `*` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` / ` ` ` ` \ ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `/` ` ` ` ` `\` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` / ` ` ` ` ` ` \ ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` `o` ` ` ` ` ` ` `*` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` `\` ` ` ` ` `/` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` \ ` ` ` ` / ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` `\` ` ` `/` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` \ ` ` / ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` `\` `/` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` \ / ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` `*` ` ` ` ` ` ` ` ` ` ` ` |
| ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
o-------------------------------------------------o
Figure 31. Syll = TE(Syll_12) |^| TE(Syll_23)
I don't know about you, but I am still puzzled by all of thus stuff, that is to say, by the entanglements of composition and projection and their relationship to the information processing properties of logical inference rules. What I lack is a single picture that could show me all of the pieces and make the pattern of their informational relationships clear.
In accord with my experimental way, I will stick with the case of transitive inference until I have pinned it down thoroughly, but of course the real interest is much more general than that.
At first or maybe second sight, the relationships seem easy enough to write out. Figure 32 shows how the various logical expressions are related to each other: The expressions "(p (q))" and "(q (r))" are conjoined in a purely syntactic fashion — much in the way that one might compile a theory from axioms without knowing what either the theory or the axioms were about — and the best way to sum up the state of information implicit in taking them together is just the expression "(p (q)) (q (r))" that would the canonical result of an equational or reversible rule of inference. From that equational inference, one might arrive at the implicational inference "(p (r))" by the most conventional implication.
o-------------------o ` ` ` ` o-------------------o
| ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` ` q ` ` ` ` | ` ` ` ` | ` ` ` ` r ` ` ` ` |
| ` ` ` ` o ` ` ` ` | ` ` ` ` | ` ` ` ` o ` ` ` ` |
| ` ` ` ` | ` ` ` ` | ` ` ` ` | ` ` ` ` | ` ` ` ` |
| ` ` ` p o ` ` ` ` | ` ` ` ` | ` ` ` q o ` ` ` ` |
| ` ` ` ` | ` ` ` ` | ` ` ` ` | ` ` ` ` | ` ` ` ` |
| ` ` ` ` @ ` ` ` ` | ` ` ` ` | ` ` ` ` @ ` ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` ` |
o-------------------o ` ` ` ` o-------------------o
| ` ` `(p (q))` ` ` | ` ` ` ` | ` ` `(q (r))` ` ` |
o-------------------o ` ` ` ` o-------------------o
| ` ` ` q_207 ` ` ` | ` ` ` ` | ` ` ` q_187 ` ` ` |
o---------o---------o ` ` ` ` o---------o---------o
` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` `
` ` ` ` ` ` \ ` ` ` Conjunction ` ` ` / ` ` ` ` ` `
` ` ` ` ` ` `\` ` ` ` ` ` ` ` ` ` ` `/` ` ` ` ` ` `
` ` ` ` ` ` ` v ` ` ` ` ` ` ` ` ` ` v ` ` ` ` ` ` `
` ` ` ` ` ` ` `o-------------------o` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` q ` r ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` o ` o ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` | ` | ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` p o ` o q ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` `\`/` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` @ ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `o-------------------o` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| `(p (q)) (q (r))` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `o-------------------o` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` q_139 ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `o---------o---------o` ` ` ` ` ` ` `
` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` `
` ` ` ` ` ` ` ` ` ` Implication ` ` ` ` ` ` ` ` ` `
` ` ` ` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` ` ` ` `
` ` ` ` ` ` ` ` ` ` ` ` `v` ` ` ` ` ` ` ` ` ` ` ` `
` ` ` ` ` ` ` `o---------o---------o` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` r ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` o ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` | ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` p o ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` | ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` @ ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `o-------------------o` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` `(p (r))` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `o-------------------o` ` ` ` ` ` ` `
` ` ` ` ` ` ` `| ` ` ` q_175 ` ` ` |` ` ` ` ` ` ` `
` ` ` ` ` ` ` `o-------------------o` ` ` ` ` ` ` `
` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` `
Figure 32. Expressive Aspects of Transitive Inference
Most of the customary names for this type of process have turned out to have misleading connotations, and so I will experiment with calling it the ''expressive'' aspect of the various rules for transitive inference, simply to emphasize the fact that rules can be given for it that operate solely on signs and expressions, without necessarily needing to look at the objects that are denoted by these signs and expressions.
In the way of many experiments, the word ''expressive'' does not seem to work for what I wanted to say here, since we too often use it to suggest something that expresses an object or a purpose, and I wanted it to imply what is purely a matter of expression, shorn of consideration for anything objective. Aside from coining a word like ''ennotative'', some other options would be ''connotative'', ''hermeneutic'', ''semiotic'', ''syntactic'' — each of which works in some range of interpretation but fails in others. Trial 2. Let's try ''formulaic''.
Despite how simple the formulaic aspects of transitive inference might appear on the surface, there are problems that wait for us just beneath the syntactic surface, as we quickly discover if we turn to considering the kinds of objects, abstract and concrete, that these formulas are meant to denote, and all the more so if we try to do this in a context of computational implementations, where the "interpreters" to be addressed take nothing on faith. Thus we engage the ''denotative semantics'' or the ''model theory'' of these extremely simple programs that we call ''propositions''.
Table 33 is an attempt to outline the model-theoretic relationships that are involved in our study of transitive inference. In it I use a number of abbreviated notations:
# I use the forms ''X''<b>:</b>''Y''<b>:</b>''Z'' and ''x''<b>:</b>''y''<b>:</b>''z'' as alternative notations for the cartesian product ''X'' × ''Y'' × ''Z'' and the tuple (''x'', ''y'', ''z''), respectively.
# In situations where we have products like ''X''''':'''''Y''''':'''''Z'' with ''X'' = ''Y'' = ''Z'' = '''B''', and relations like ''L'' ⊆ ''X''<b>:</b>''Y'', ''M'' ⊆ ''X''<b>:</b>''Z'', ''N'' ⊆ ''Y''<b>:</b>''Z'', I will use forms like ''L'' ⊆ '''B:B:~''', ''M'' ⊆ '''B:~:B''', ''N'' ⊆ '''~:B:B''' to remind us that we are considering particular ways of situating ''L'', ''M'', ''N'' within the product space ''X''<b>:</b>''Y''<b>:</b>''Z''.
o-------------------o ` ` ` ` o-------------------o
| ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` 0:0:0 ` ` ` | ` ` ` ` | ` ` ` 0:0:0 ` ` ` |
| ` ` ` 0:0:1 ` ` ` | ` ` ` ` | ` ` ` 0:0:1 ` ` ` |
| ` ` ` 0:1:0 ` ` ` | ` ` ` ` | ` ` ` 0:1:1 ` ` ` |
| ` ` ` 0:1:1 ` ` ` | ` ` ` ` | ` ` ` 1:0:0 ` ` ` |
| ` ` ` 1:1:0 ` ` ` | ` ` ` ` | ` ` ` 1:0:1 ` ` ` |
| ` ` ` 1:1:1 ` ` ` | ` ` ` ` | ` ` ` 1:1:1 ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` ` |
o-------------------o ` ` ` ` o-------------------o
|TE(Syll_12) c B:B:B| ` ` ` ` |TE(Syll_23) c B:B:B|
o-------------------o ` ` ` ` o-------------------o
| ` `[| q_207 |]` ` | ` ` ` ` | ` `[| q_187 |]` ` |
o----o---------o----o ` ` ` ` o----o---------o----o
` ` `^` ` ` ` ` \ ` ` ` ` ` ` ` ` / ` ` ` ` `^` ` `
` ` `|` ` ` ` ` `\`Intersection `/` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` `v` ` ` ` ` `v` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` `o-------------------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` 0:0:0 ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` 0:0:1 ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` 0:1:1 ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` 1:1:1 ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o-------------------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` `Syll c B:B:B ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o-------------------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` `[| q_139 |]` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o---------o---------o` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` ` Projection` ` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` ` ` ` `v` ` ` ` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` `o---------o---------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` `0:0` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` `0:1` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` `1:1` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o-------------------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| `Syll_13 c B:~:B` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o-------------------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` [| (p (r)) |] ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o----o---------o----o` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` `^` ` ` ` ` `^` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` / ` ` ` ` ` ` \ ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` `/` Composition `\` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` / ` ` ` ` ` ` ` ` \ ` ` ` ` `|` ` `
o----o---------o----o ` ` ` ` o----o---------o----o
| ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` ` `0:0` ` ` ` | ` ` ` ` | ` ` ` `0:0` ` ` ` |
| ` ` ` `0:1` ` ` ` | ` ` ` ` | ` ` ` `0:1` ` ` ` |
| ` ` ` `1:1` ` ` ` | ` ` ` ` | ` ` ` `1:1` ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` ` |
o-------------------o ` ` ` ` o-------------------o
| `Syll_12 c B:B:~` | ` ` ` ` | `Syll_23 c ~:B:B` |
o-------------------o ` ` ` ` o-------------------o
| ` [| (p (q)) |] ` | ` ` ` ` | ` [| (q (r)) |] ` |
o---------o---------o ` ` ` ` o---------o---------o
Figure 33. Denotative Aspects of Transitive Inference
A piece of syntax like "(p (q))" or "''p'' ⇒ ''q''" is an abstract description, and abstraction is a process that loses information about the objects described. So when we go to reverse the abstraction, as we do when we look for models of that description, there is a degree of indefiniteness that comes into play.
For example, the proposition (p (q)) is typically assigned the functional type '''B'''<sup>2</sup> → '''B''', but that is only its canonical or its minimal abstract type. No sooner do we use it in a context that invokes additional variables, as we do when we next consider the proposition (q (r)), than its type is tacitly adjusted to fit the new context, for instance, acquiring the extended type '''B'''<sup>3</sup> → '''B'''. This is one of those things that most people eventually learn to do without blinking an eye, that is to say, unreflectively, and this is precisely what makes the same facility so much trouble to implement properly in computational form.
Both the fibering operation, that takes us from the function (p (q)) to the relation <nowiki>[|</nowiki> (p (q)) <nowiki>|]</nowiki>, and the tacit extension operation, that takes us from the relation <nowiki>[|</nowiki> (p (q)) <nowiki>|]</nowiki> ⊆ '''B:B''' to the relation <nowiki>[|</nowiki> ''q''<sub>207</sub> <nowiki>|]</nowiki> ⊆ '''B:B:B''' have this same character of abstraction-undoing or modelling operations that require us to re-interpret the same pieces of syntax under different types. This accounts for a large part of the apparent ambiguities.
Up till now I've concentrated mostly on the abstract types of domains and propositions, things like '''B'''<sup>''k''</sup> and '''B'''<sup>''k''</sup> → '''B''', respectively. This is a little like trying to do physics all in dimensionless quantities without keeping track of the qualitative physical units. So much abstraction has its obvious limits, not to mention its hidden dangers.
To remedy this situation I will start to introduce the concrete types of domains and propositions, once again as they pertain to our current collection of examples.
We have been using the lower case letters ''p'', ''q'', ''r'' for the basic propositions of abstract type '''B'''<sup>3</sup> → '''B''' and the upper case letters ''P'', ''Q'', ''R'' for the basic regions of the universe of discourse where ''p'', ''q'', ''r'' hold true, respectively.
The set of signs <font face=calligrapher>X</font> = {"''p''", "''q''", "''r''"} is the ''alphabet'' for the universe of discourse that is notated as ''X''<sup> •</sup> = [<font face=calligrapher>X</font>] = [''p'', ''q'', ''r''], already getting sloppy about quotation marks to single out the signs.
The universe ''X''<sup> •</sup> is composed of two different spaces of objects. The first is the space of positions ''X'' = <font face=symbol>á</font>''p'', ''q'', ''r''<font face=symbol>ñ</font> = {<''p'', ''q'', ''r''>}. The second is the space of propositions ''X''↑ = (''X'' → '''B''').
Let us make the following definitions:
: ''P''‡ = ''X''<sub>''p''</sub> = {(''p''), ''p''},
: ''Q''‡ = ''X''<sub>''q''</sub> = {(''q''), ''q''},
: ''R''‡ = ''X''<sub>''r''</sub> = {(''r''), ''r''}.
These are three sets of two abstract signs each, altogether staking out the qualitative dimensions of the universe of discourse ''X''<sup> •</sup>.
Given this framework, the concrete type of the space ''X'' is ''P''‡ × ''Q''‡ × ''R''‡ <u>≈</u> '''B'''<sup>3</sup> and the concrete type of each proposition in ''X''↑ = (''X'' → '''B''') is ''P''‡ × ''Q''‡ × ''R''‡ → '''B'''. Given the length of the type markers, we will often omit the cartesian product symbols and write just ''P''‡ ''Q''‡ ''R''‡.
An abstract reference to a point of ''X'' is a triple in '''B'''<sup>3</sup>. A concrete reference to a point of ''X'' is a conjunction of signs from the dimensions ''P''‡, ''Q''‡, ''R''‡, picking exactly one sign from each dimension.
To illustrate the use of concrete coordinates for points and concrete types for spaces and propositions, Figure 35 translates the contents of Figure 33 into the new language.
o-------------------o ` ` ` ` o-------------------o
| ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` (p)(q)(r) ` ` | ` ` ` ` | ` ` (p)(q)(r) ` ` |
| ` ` (p)(q)`r` ` ` | ` ` ` ` | ` ` (p)(q)`r` ` ` |
| ` ` (p) q (r) ` ` | ` ` ` ` | ` ` (p) q `r` ` ` |
| ` ` (p) q `r` ` ` | ` ` ` ` | ` ` `p`(q)(r) ` ` |
| ` ` `p` q (r) ` ` | ` ` ` ` | ` ` `p`(q)`r` ` ` |
| ` ` `p` q `r` ` ` | ` ` ` ` | ` ` `p` q `r` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` ` |
o-------------------o ` ` ` ` o-------------------o
|TE(Syll_12) c B:B:B| ` ` ` ` |TE(Syll_23) c B:B:B|
o-------------------o ` ` ` ` o-------------------o
| ` `[| q_207 |]` ` | ` ` ` ` | ` `[| q_187 |]` ` |
o----o---------o----o ` ` ` ` o----o---------o----o
` ` `^` ` ` ` ` \ ` ` ` ` ` ` ` ` / ` ` ` ` `^` ` `
` ` `|` ` ` ` ` `\`Intersection `/` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` \ ` ` ` ` ` ` / ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` `v` ` ` ` ` `v` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` `o-------------------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` (p)(q)(r) ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` (p)(q)`r` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` (p) q `r` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` `p` q `r` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o-------------------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| `Syll c P‡ Q‡ R‡` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o-------------------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` `[| q_139 |]` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o---------o---------o` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` ` Projection` ` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` ` ` ` `|` ` ` ` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` ` ` ` `v` ` ` ` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` `o---------o---------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` `(p) (r)` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` `(p)` r ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` p ` r ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` ` ` ` ` ` ` ` ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o-------------------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| `Syll_13 c P‡ R‡` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o-------------------o` ` ` ` `|` ` `
` ` `|` ` ` ` `| ` [| (p (r)) |] ` |` ` ` ` `|` ` `
` ` `|` ` ` ` `o----o---------o----o` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` `^` ` ` ` ` `^` ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` ` / ` ` ` ` ` ` \ ` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` `/` Composition `\` ` ` ` ` `|` ` `
` ` `|` ` ` ` ` / ` ` ` ` ` ` ` ` \ ` ` ` ` `|` ` `
o----o---------o----o ` ` ` ` o----o---------o----o
| ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| ` ` `(p) (q)` ` ` | ` ` ` ` | ` ` `(q) (r)` ` ` |
| ` ` `(p)` q ` ` ` | ` ` ` ` | ` ` `(q)` r ` ` ` |
| ` ` ` p ` q ` ` ` | ` ` ` ` | ` ` ` q ` r ` ` ` |
| ` ` ` ` ` ` ` ` ` | ` ` ` ` | ` ` ` ` ` ` ` ` ` |
o-------------------o ` ` ` ` o-------------------o
| `Syll_12 c P‡ Q‡` | ` ` ` ` | `Syll_23 c Q‡ R‡` |
o-------------------o ` ` ` ` o-------------------o
| ` [| (p (q)) |] ` | ` ` ` ` | ` [| (q (r)) |] ` |
o---------o---------o ` ` ` ` o---------o---------o
Figure 35. Denotative Aspects of Transitive Inference
==References==
* [[Gottfried Leibniz|Leibniz, G.W.]] (1679–1686 ?), "Addenda to the Specimen of the Universal Calculus", pp. 40–46 in Parkinson, G.H.R. (ed.), ''Leibniz : Logical Papers'', Oxford University Press, London, UK, 1966. (Cf. Gerhardt, 7, p. 223).
* [[Charles Peirce (Bibliography)|Peirce, C.S., Bibliography]].
* [[Charles Peirce|Peirce, C.S.]] (1931–1935, 1958), ''Collected Papers of Charles Sanders Peirce'', vols. 1–6, [[Charles Hartshorne]] and [[Paul Weiss (philosopher)|Paul Weiss]] (eds.), vols. 7–8, [[Arthur W. Burks]] (ed.), Harvard University Press, Cambridge, MA. Cited as CP volume.paragraph.
* Peirce, C.S. (1981–), ''Writings of Charles S. Peirce: A Chronological Edition'', [[Peirce Edition Project]] (eds.), Indiana University Press, Bloomington and Indianoplis, IN. Cited as CE volume, page.
* Peirce, C.S. (1885), "On the Algebra of Logic: A Contribution to the Philosophy of Notation", ''American Journal of Mathematics'' 7 (1885), 180–202. Reprinted as CP 3.359–403 and CE 5, 162–190.
* Peirce, C.S. (c. 1886), "Qualitative Logic", MS 736. Published as pp. 101–115 in Carolyn Eisele (ed., 1976), ''The New Elements of Mathematics by Charles S. Peirce, Volume 4, Mathematical Philosophy'', Mouton, The Hague.
* Peirce, C.S. (1886 a), "Qualitative Logic", MS 582. Published as pp. 323–371 in ''Writings of Charles S. Peirce: A Chronological Edition, Volume 5, 1884–1886'', Peirce Edition Project (eds.), Indiana University Press, Bloomington, IN, 1993.
* Peirce, C.S. (1886 b), "The Logic of Relatives: Qualitative and Quantitative", MS 584. Published as pp. 372–378 in ''Writings of Charles S. Peirce: A Chronological Edition, Volume 5, 1884–1886'', Peirce Edition Project (eds.), Indiana University Press, Bloomington, IN, 1993.
* [[George Spencer Brown|Spencer Brown, George]] (1969), ''[[Laws of Form]]'', George Allen and Unwin, London, UK.
==See also==
===Related essays and projects===
* [[Futures Of Logical Graphs]]
* [[Information = Comprehension × Extension]]
* [[Inquiry Driven Systems]]
* [[Introduction to Inquiry Driven Systems]]
* [[Peirce's Logic Of Information]]
* [[Semiotic Theory Of Information]]
===Related concepts and topics===
{{col-begin}}
{{col-break}}
* [[Ampheck]]
* [[Boolean algebra]]
* [[Boolean domain]]
* [[Boolean function]]
* [[Boolean logic]]
* [[Boolean-valued function]]
* [[Dynamics of inquiry]]
* [[Entitative graph]]
* [[Existential graph]]
{{col-break}}
* [[Graph (mathematics)|Graph]]
* [[Graph theory]]
* [[Laws of Form]]
* [[Logic of relatives]]
* [[Logic of information]]
* [[Logical graph]]
* [[Logical matrix]]
* [[Logical NAND]]
* [[Logical NNOR]]
{{col-break}}
* [[Minimal negation operator]]
* [[Multigrade operator]]
* [[Parametric operator]]
* [[Peirce's law]]
* [[Peirce's logic of information]]
* [[Propositional calculus]]
* [[Semiotic information theory]]
* [[Truth table]]
* [[Zeroth order logic]]
{{col-end}}
==External links==
* [http://www.lawsofform.org/ ''Laws of Form'' Web Site].
* [http://www.lawsofform.org/aum/session1.html Spencer-Brown's talks at Esalen 1973] — Self-referential forms are introduced in the section entitled "Degree of Equations and the Theory of Types".
* [http://www.math.uic.edu/~kauffman/ Louis H. Kauffman] — ''[http://www.math.uic.edu/~kauffman/Arithmetic.htm Box Algebra, Boundary Mathematics, Logic, and Laws of Form]''.
==Document history==
...
{{aficionados}}<sharethis />
<!--semantic tags-->
[[Author:=Jon Awbrey| ]]
[[Paper Name:=Propositional Equation Reasoning Systems| ]]
[[Paper Of::Directory:Jon Awbrey| ]]