MyWikiBiz

Changes

Directory:Jon Awbrey/MathJax Problems (view source)

Revision as of 18:15, 6 November 2016

17,534 bytes added ,  18:15, 6 November 2016
add problem section
Line 1: Line 1: −
*
+
{{DISPLAYTITLE:Propositional Equation Reasoning Systems}}
 +
* '''Note.''' The MathJax parser is not rendering this page properly.<br>Until it can be fixed please see the [http://intersci.ss.uci.edu/wiki/index.php/Propositional_Equation_Reasoning_Systems InterSciWiki version].
 +
 
 +
'''Author: [[User:Jon Awbrey|Jon Awbrey]]'''
 +
 
 +
This article develops elementary facts about a family of formal calculi described as '''propositional equation reasoning systems''' ('''PERS''').  This work follows 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 &ldquo;[[Logical Graphs]]&rdquo; 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" cellpadding="10"
 +
| [[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'' <math>(\mathrm{En}).\!</math>  Under <math>\mathrm{En},\!</math> the axioms read as follows:
 +
 
 +
{| align="center" cellpadding="10"
 +
|
 +
<math>\begin{matrix}
 +
I_1
 +
& : &
 +
\mathrm{true} ~\mathrm{or}~ \mathrm{true}
 +
& = &
 +
\mathrm{true}
 +
\\
 +
I_2
 +
& : &
 +
\mathrm{not}~ \mathrm{true}
 +
& = &
 +
\mathrm{false}
 +
\\
 +
J_1
 +
& : &
 +
a ~\mathrm{or}~ \mathrm{not}~ a
 +
& = &
 +
\mathrm{true}
 +
\\
 +
J_2
 +
& : &
 +
(a ~\mathrm{or}~ b) ~\mathrm{and}~ (a ~\mathrm{or}~ c)
 +
& = &
 +
a ~\mathrm{or}~ (b ~\mathrm{and}~ c)
 +
\end{matrix}</math>
 +
|}
 +
 
 +
Another way of assigning logical meaning to the initial equations is known as the ''existential interpretation'' <math>(\mathrm{Ex}).\!</math>  Under <math>\mathrm{Ex},\!</math> the axioms read as follows:
 +
 
 +
{| align="center" cellpadding="10"
 +
|
 +
<math>\begin{matrix}
 +
I_1
 +
& : &
 +
\mathrm{false} ~\mathrm{and}~ \mathrm{false}
 +
& = &
 +
\mathrm{false}
 +
\\
 +
I_2
 +
& : &
 +
\mathrm{not}~ \mathrm{false}
 +
& = &
 +
\mathrm{true}
 +
\\
 +
J_1
 +
& : &
 +
a ~\mathrm{and}~ \mathrm{not}~ a
 +
& = &
 +
\mathrm{false}
 +
\\
 +
J_2
 +
& : &
 +
(a ~\mathrm{and}~ b) ~\mathrm{or}~ (a ~\mathrm{and}~ c)
 +
& = &
 +
a ~\mathrm{and}~ (b ~\mathrm{or}~ c)
 +
\end{matrix}</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 &#9552;&#9552;&#9552;&#9552;&#9552; 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 <math>\mathrm{En}\!</math> and <math>\mathrm{Ex},\!</math> respectively.  The early CSP, as in his essay on &ldquo;Qualitative Logic&rdquo;, and also GSB, emphasized the <math>\mathrm{En}\!</math> interpretation, while the later CSP developed mostly the <math>\mathrm{Ex}\!</math> interpretation.
 +
 
 +
===Frequently used theorems===
 +
 
 +
====C<sub>1</sub>.  Double negation====
 +
 
 +
The first theorem goes under the names of ''Consequence&nbsp;1'' <math>(C_1),\!</math> the ''double negation theorem'' (DNT), or ''Reflection''.
 +
 
 +
{| align="center" cellpadding="10"
 +
| [[Image:Double Negation 1.0 Splash Page.png|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" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Double Negation 1.0 Marquee Title.png|500px]]
 +
|-
 +
| [[Image:Double Negation 1.0 Storyboard 1.png|500px]]
 +
|-
 +
| [[Image:Equational Inference I2 Elicit (( )).png|500px]]
 +
|-
 +
| [[Image:Double Negation 1.0 Storyboard 2.png|500px]]
 +
|-
 +
| [[Image:Equational Inference J1 Insert (a).png|500px]]
 +
|-
 +
| [[Image:Double Negation 1.0 Storyboard 3.png|500px]]
 +
|-
 +
| [[Image:Equational Inference J2 Distribute ((a)).png|500px]]
 +
|-
 +
| [[Image:Double Negation 1.0 Storyboard 4.png|500px]]
 +
|-
 +
| [[Image:Equational Inference J1 Delete (a).png|500px]]
 +
|-
 +
| [[Image:Double Negation 1.0 Storyboard 5.png|500px]]
 +
|-
 +
| [[Image:Equational Inference J1 Insert a.png|500px]]
 +
|-
 +
| [[Image:Double Negation 1.0 Storyboard 6.png|500px]]
 +
|-
 +
| [[Image:Equational Inference J2 Collect a.png|500px]]
 +
|-
 +
| [[Image:Double Negation 1.0 Storyboard 7.png|500px]]
 +
|-
 +
| [[Image:Equational Inference J1 Delete ((a)).png|500px]]
 +
|-
 +
| [[Image:Double Negation 1.0 Storyboard 8.png|500px]]
 +
|-
 +
| [[Image:Equational Inference I2 Cancel (( )).png|500px]]
 +
|-
 +
| [[Image:Double Negation 1.0 Storyboard 9.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Marquee QED.png|500px]]
 +
|}
 +
| (6)
 +
|}
 +
 
 +
The steps of this proof are replayed in the following animation.
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Double Negation 2.0 Animation.gif]]
 +
|}
 +
| (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&nbsp;2'' <math>(C_2)\!</math> or ''Generation''.
 +
 
 +
{| align="center" cellpadding="10"
 +
| [[Image:Generation Theorem 1.0 Splash Page.png|500px]] || (8)
 +
|}
 +
 
 +
Here is a proof of the Generation Theorem.
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Generation Theorem 1.0 Marquee Title.png|500px]]
 +
|-
 +
| [[Image:Generation Theorem 1.0 Storyboard 1.png|500px]]
 +
|-
 +
| [[Image:Equational Inference C1 Reflect a(b).png|500px]]
 +
|-
 +
| [[Image:Generation Theorem 1.0 Storyboard 2.png|500px]]
 +
|-
 +
| [[Image:Equational Inference I2 Elicit (( )).png|500px]]
 +
|-
 +
| [[Image:Generation Theorem 1.0 Storyboard 3.png|500px]]
 +
|-
 +
| [[Image:Equational Inference J1 Insert a.png|500px]]
 +
|-
 +
| [[Image:Generation Theorem 1.0 Storyboard 4.png|500px]]
 +
|-
 +
| [[Image:Equational Inference J2 Collect a.png|500px]]
 +
|-
 +
| [[Image:Generation Theorem 1.0 Storyboard 5.png|500px]]
 +
|-
 +
| [[Image:Equational Inference C1 Reflect a, b.png|500px]]
 +
|-
 +
| [[Image:Generation Theorem 1.0 Storyboard 6.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Marquee QED.png|500px]]
 +
|}
 +
| (9)
 +
|}
 +
 
 +
The steps of this proof are replayed in the following animation.
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Generation Theorem 2.0 Animation.gif]]
 +
|}
 +
| (10)
 +
|}
 +
 
 +
====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&nbsp;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" cellpadding="10"
 +
| [[Image:Dominant Form 1.0 Splash Page.png|500px]] || (11)
 +
|}
 +
 
 +
Here is a proof of the Dominant Form Theorem.
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Dominant Form 1.0 Marquee Title.png|500px]]
 +
|-
 +
| [[Image:Dominant Form 1.0 Storyboard 1.png|500px]]
 +
|-
 +
| [[Image:Equational Inference C2 Regenerate a.png|500px]]
 +
|-
 +
| [[Image:Dominant Form 1.0 Storyboard 2.png|500px]]
 +
|-
 +
| [[Image:Equational Inference J1 Delete a.png|500px]]
 +
|-
 +
| [[Image:Dominant Form 1.0 Storyboard 3.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Marquee QED.png|500px]]
 +
|}
 +
| (12)
 +
|}
 +
 
 +
The following animation provides an instant re*play.
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Dominant Form 2.0 Animation.gif]]
 +
|}
 +
| (13)
 +
|}
 +
 
 +
===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:
 +
 
 +
{| align="center" cellpadding="10"
 +
| <math>((p \Rightarrow q) \Rightarrow p) \Rightarrow p\!</math>
 +
|}
 +
 
 +
The existential graph representation of Peirce's law is shown below.
 +
 
 +
{| align="center" cellpadding="10"
 +
| [[Image:Peirce's Law 1.0 Splash Page.png|500px]] || (14)
 +
|}
 +
 
 +
A graphical proof of Peirce's law is shown next.
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Peirce's Law 1.0 Marquee Title.png|500px]]
 +
|-
 +
| [[Image:Peirce's Law 1.0 Storyboard 1.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Band Collect p.png|500px]]
 +
|-
 +
| [[Image:Peirce's Law 1.0 Storyboard 2.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Band Quit ((q)).png|500px]]
 +
|-
 +
| [[Image:Peirce's Law 1.0 Storyboard 3.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Band Cancel (( )).png|500px]]
 +
|-
 +
| [[Image:Peirce's Law 1.0 Storyboard 4.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Band Delete p.png|500px]]
 +
|-
 +
| [[Image:Peirce's Law 1.0 Storyboard 5.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Band Cancel (( )).png|500px]]
 +
|-
 +
| [[Image:Peirce's Law 1.0 Storyboard 6.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Marquee QED.png|500px]]
 +
|}
 +
| (15)
 +
|}
 +
 
 +
The following animation replays the steps of the proof.
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Peirce's Law 2.0 Animation.gif]]
 +
|}
 +
| (16)
 +
|}
 +
 
 +
====Praeclarum theorema====
 +
 
 +
An illustrious example of a propositional theorem is the ''praeclarum theorema'', the ''admirable'', ''shining'', or ''splendid'' theorem of Leibniz.
 +
 
 +
{| align="center" cellpadding="10" width="90%"
 +
|
 +
<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>
 +
|}
 +
 
 +
Under the existential interpretation, the praeclarum theorema is represented by means of the following logical graph.
 +
 
 +
{| align="center" cellpadding="10"
 +
| [[Image:Praeclarum Theorema 1.0 Splash Page.png|500px]] || (17)
 +
|}
 +
 
 +
And here's a neat proof of that nice theorem.
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Praeclarum Theorema 1.0 Marquee Title.png|500px]]
 +
|-
 +
| [[Image:Praeclarum Theorema 1.0 Storyboard 1.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Rule Reflect ad(bc).png|500px]]
 +
|-
 +
| [[Image:Praeclarum Theorema 1.0 Storyboard 2.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Rule Weed a, d.png|500px]]
 +
|-
 +
| [[Image:Praeclarum Theorema 1.0 Storyboard 3.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Rule Reflect b, c.png|500px]]
 +
|-
 +
| [[Image:Praeclarum Theorema 1.0 Storyboard 4.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Rule Weed bc.png|500px]]
 +
|-
 +
| [[Image:Praeclarum Theorema 1.0 Storyboard 5.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Rule Quit abcd.png|500px]]
 +
|-
 +
| [[Image:Praeclarum Theorema 1.0 Storyboard 6.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Rule Cancel (( )).png|500px]]
 +
|-
 +
| [[Image:Praeclarum Theorema 1.0 Storyboard 7.png|500px]]
 +
|-
 +
| [[Image:Equational Inference Marquee QED.png|500px]]
 +
|}
 +
| (18)
 +
|}
 +
 
 +
The steps of the proof are replayed in the following animation.
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Praeclarum Theorema 2.0 Animation.gif]]
 +
|}
 +
| (19)
 +
|}
 +
 
 +
====Two-thirds majority function====
 +
 
 +
Consider the following equation in boolean algebra, posted as a [http://mathoverflow.net/questions/9292/newbie-boolean-algebra-question problem for proof] at [http://mathoverflow.net/ MathOverFlow].
 +
 
 +
{| align="center" cellpadding="20"
 +
| <math>\begin{matrix} a b \bar{c} + a \bar{b} c + \bar{a} b c + a b c \\[6pt] \iff \\[6pt] a b + a c + b c \end{matrix}</math>
 +
| (20)
 +
|}
 +
 
 +
The required equation can be proven in the medium of logical graphs as shown in the following Figure.
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Majority Function Example Proof 1 Title.jpg|500px]]
 +
|-
 +
| [[Image:Majority Function Example 2.0 Proof 1 Frame 1.jpg|500px]]
 +
|-
 +
| [[Image:Equational Inference Reflect ab, ac, bc ISW.jpg|500px]]
 +
|-
 +
| [[Image:Majority Function Example 2.0 Proof 1 Frame 2.jpg|500px]]
 +
|-
 +
| [[Image:Equational Inference Distribute (abc).jpg|500px]]
 +
|-
 +
| [[Image:Majority Function Example 2.0 Proof 1 Frame 3.jpg|500px]]
 +
|-
 +
| [[Image:Equational Inference Collect ab, ac, bc ISW.jpg|500px]]
 +
|-
 +
| [[Image:Majority Function Example 2.0 Proof 1 Frame 4.jpg|500px]]
 +
|-
 +
| [[Image:Equational Inference Quit (a), (b), (c).jpg|500px]]
 +
|-
 +
| [[Image:Majority Function Example 2.0 Proof 1 Frame 5.jpg|500px]]
 +
|-
 +
| [[Image:Equational Inference Cancel (( )).jpg|500px]]
 +
|-
 +
| [[Image:Majority Function Example 2.0 Proof 1 Frame 6.jpg|500px]]
 +
|-
 +
| [[Image:Equational Inference Weed ab, ac, bc.jpg|500px]]
 +
|-
 +
| [[Image:Majority Function Example 2.0 Proof 1 Frame 7.jpg|500px]]
 +
|-
 +
| [[Image:Equational Inference Delete a, b, c ISW.jpg|500px]]
 +
|-
 +
| [[Image:Majority Function Example 2.0 Proof 1 Frame 8.jpg|500px]]
 +
|-
 +
| [[Image:Equational Inference Cancel (( )).jpg|500px]]
 +
|-
 +
| [[Image:Majority Function Example 2.0 Proof 1 Frame 9.jpg|500px]]
 +
|-
 +
| [[Image:Equational Inference QED.jpg|500px]]
 +
|}
 +
| (21)
 +
|}
 +
 
 +
Here's an animated recap of the graphical transformations that occur in the above proof:
 +
 
 +
{| align="center" cellpadding="8"
 +
|
 +
{| align="center" cellpadding="0" cellspacing="0" style="border-left:1px solid black; border-top:1px solid black; border-right:1px solid black; border-bottom:1px solid black; text-align:center"
 +
|-
 +
| [[Image:Two-Thirds Majority Function 500 x 250 Animation.gif]]
 +
|}
 +
| (22)
 +
|}
 +
 
 +
==Formal extension : Cactus calculus==
 +
 
 +
Let us now extend the CSP&ndash;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>\texttt{(\_)}\!</math> in a particular manner, treating <math>\texttt{(\_)}\!</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>\texttt{(\_)},\!</math>&nbsp; <math>\texttt{(\_, \_)},\!</math>&nbsp; <math>\texttt{(\_, \_, \_)},\!</math>&nbsp; and so on, where the number of argument slots is the order of the reflective negation operator in question.
Jon Awbrey
12,080

edits

Retrieved from "https://mywikibiz.com/Special:MobileDiff/467459"