MyWikiBiz

Changes

Directory talk:Jon Awbrey/Papers/Differential Logic : Introduction (view source)

Revision as of 21:30, 29 June 2009

27,651 bytes added ,  21:30, 29 June 2009
→‎Logical Cacti: copy partial markup
Line 11: Line 11:  
: http://stderr.org/pipermail/inquiry/2005-February/002360.html
 
: http://stderr.org/pipermail/inquiry/2005-February/002360.html
 
: http://stderr.org/pipermail/inquiry/2005-February/002361.html
 
: http://stderr.org/pipermail/inquiry/2005-February/002361.html
 +
 +
====Original Version====
    
<pre>
 
<pre>
Line 358: Line 360:  
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
 
</pre>
 
</pre>
 +
 +
====Partial Markup====
 +
 +
Table&nbsp;13 illustrates the ''existential interpretation'' of cactus graphs and cactus expressions by providing English translations for a few of the most basic and commonly occurring forms.
 +
 +
Even though I do most of my thinking in the existential interpretation, I will continue to speak of these forms as ''logical graphs'', because I think it is an important fact about them that the formal validity of the axioms and theorems is not dependent on the choice between the entitative and the existential interpretations.
 +
 +
The first extension is the ''reflective extension of logical graphs'' (RefLog).  It is obtained by generalizing the negation operator "<math>\texttt{(~)}</math>" in a certain way, calling "<math>\texttt{(~)}</math>" the ''controlled'', ''moderated'', or ''reflective'' negation operator of order 1, then adding another such operator for each finite <math>k = 2, 3, \ldots .</math>
 +
 +
In sum, these operators are symbolized by bracketed argument lists as follows:  "<math>\texttt{(~)}</math>", "<math>\texttt{(~,~)}</math>", "<math>\texttt{(~,~,~)}</math>", &hellip;, where the number of slots is the order of the reflective negation operator in question.
 +
             
 +
The cactus graph and the cactus expression shown here are both described as a ''spike''.
 +
 +
{| align="center" cellpadding="6" width="90%"
 +
| align="center" |
 +
<pre>
 +
o---------------------------------------o
 +
|                                      |
 +
|                  o                  |
 +
|                  |                  |
 +
|                  @                  |
 +
|                                      |
 +
o---------------------------------------o
 +
|                  ( )                  |
 +
o---------------------------------------o
 +
</pre>
 +
|}
 +
 +
The rule of reduction for a lobe is:
 +
 +
{| align="center" cellpadding="6" width="90%"
 +
| align="center" |
 +
<pre>
 +
o---------------------------------------o
 +
|                                      |
 +
|  x_1  x_2  ...  x_k                |
 +
|  o-----o--- ... ---o                |
 +
|    \              /                  |
 +
|    \            /                  |
 +
|      \          /                    |
 +
|      \        /                    |
 +
|        \      /                      |
 +
|        \    /                      |
 +
|          \  /                        |
 +
|          \ /                        |
 +
|            @      =      @            |
 +
|                                      |
 +
o---------------------------------------o
 +
</pre>
 +
|}
 +
 +
if and only if exactly one of the <math>x_j\!</math> is a spike.
 +
 +
In Ref Log, an expression of the form <math>\texttt{((}~ e_1 ~\texttt{),(}~ e_2 ~\texttt{),(}~ \ldots ~\texttt{),(}~ e_k ~\texttt{))}</math>
 +
expresses the fact that ''exactly one of the <math>e_j\!</math> is true''.  Expressions of this form are called ''universal partition'' expressions, and
 +
they parse into a type of graph called a ''painted and rooted cactus'' (PARC):
 +
 +
{| align="center" cellpadding="6" width="90%"
 +
| align="center" |
 +
<pre>
 +
o---------------------------------------o
 +
|                                      |
 +
|  e_1  e_2  ...  e_k                |
 +
|  o    o          o                |
 +
|  |    |          |                |
 +
|  o-----o--- ... ---o                |
 +
|    \              /                  |
 +
|    \            /                  |
 +
|      \          /                    |
 +
|      \        /                    |
 +
|        \      /                      |
 +
|        \    /                      |
 +
|          \  /                        |
 +
|          \ /                        |
 +
|            @                          |
 +
|                                      |
 +
o---------------------------------------o
 +
</pre>
 +
|}
 +
 +
{| align="center" cellpadding="6" width="90%"
 +
| align="center" |
 +
<pre>
 +
o---------------------------------------o
 +
|                                      |
 +
| ( x1, x2, ..., xk )  =  [blank]      |
 +
|                                      |
 +
| iff                                  |
 +
|                                      |
 +
| Just one of the arguments            |
 +
| x1, x2, ..., xk  =  ()                |
 +
|                                      |
 +
o---------------------------------------o
 +
</pre>
 +
|}
 +
 +
The interpretation of these operators, read as assertions about the values of their listed arguments, is as follows:
 +
 +
{| align="center" cellpadding="6" width="90%"
 +
| Existential Interpretation:
 +
| Just one of the k argument is false.
 +
|-
 +
| Entitative  Interpretation:
 +
| Not just one of the k arguments is true.
 +
|}
 +
 +
{| align="center" cellpadding="6" width="90%"
 +
| align="center" |
 +
<pre>
 +
o-------------------o-------------------o-------------------o
 +
|      Graph      |      String      |    Translation    |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        @        |        " "        |      true.      |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        o        |                  |                  |
 +
|        |        |                  |                  |
 +
|        @        |        ( )        |      untrue.      |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        r        |                  |                  |
 +
|        @        |        r        |        r.        |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        r        |                  |                  |
 +
|        o        |                  |                  |
 +
|        |        |                  |                  |
 +
|        @        |        (r)        |      not r.      |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      r s t      |                  |                  |
 +
|        @        |      r s t      |  r and s and t.  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      r s t      |                  |                  |
 +
|      o o o      |                  |                  |
 +
|        \|/        |                  |                  |
 +
|        o        |                  |                  |
 +
|        |        |                  |                  |
 +
|        @        |    ((r)(s)(t))    |    r or s or t.  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |    r implies s.  |
 +
|        r  s    |                  |                  |
 +
|        o---o    |                  |    if r then s.  |
 +
|        |        |                  |                  |
 +
|        @        |      (r (s))      |    no r sans s.  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      r  s      |                  |                  |
 +
|      o---o      |                  | r exclusive-or s. |
 +
|        \ /        |                  |                  |
 +
|        @        |      (r , s)      | r not equal to s. |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      r  s      |                  |                  |
 +
|      o---o      |                  |                  |
 +
|        \ /        |                  |                  |
 +
|        o        |                  | r if & only if s. |
 +
|        |        |                  |                  |
 +
|        @        |    ((r , s))    | r equates with s. |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      r  s  t      |                  |                  |
 +
|      o--o--o      |                  |                  |
 +
|      \  /      |                  |                  |
 +
|        \ /        |                  |  just one false  |
 +
|        @        |    (r , s , t)    |  out of r, s, t.  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      r  s  t      |                  |                  |
 +
|      o  o  o      |                  |                  |
 +
|      |  |  |      |                  |                  |
 +
|      o--o--o      |                  |                  |
 +
|      \  /      |                  |                  |
 +
|        \ /        |                  |  just one true  |
 +
|        @        |  ((r),(s),(t))  |  among r, s, t.  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |  genus t over    |
 +
|        r  s      |                  |  species r, s.  |
 +
|        o  o      |                  |                  |
 +
|      t  |  |      |                  |  partition t    |
 +
|      o--o--o      |                  |  among r & s.    |
 +
|      \  /      |                  |                  |
 +
|        \ /        |                  |  whole pie t:    |
 +
|        @        |  ( t ,(r),(s))  |  slices r, s.    |
 +
o-------------------o-------------------o-------------------o
 +
</pre>
 +
|}
 +
 +
{| align="center" cellpadding="6" width="90%"
 +
| align="center" |
 +
<pre>
 +
Table 13.  The Existential Interpretation
 +
o-------------------o-------------------o-------------------o
 +
|  Cactus Graph    | Cactus Expression |    Existential    |
 +
|                  |                  |  Interpretation  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        @        |        " "        |      true.      |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        o        |                  |                  |
 +
|        |        |                  |                  |
 +
|        @        |        ( )        |      untrue.      |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        a        |                  |                  |
 +
|        @        |        a        |        a.        |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        a        |                  |                  |
 +
|        o        |                  |                  |
 +
|        |        |                  |                  |
 +
|        @        |        (a)        |      not a.      |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a b c      |                  |                  |
 +
|        @        |      a b c      |  a and b and c.  |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a b c      |                  |                  |
 +
|      o o o      |                  |                  |
 +
|        \|/        |                  |                  |
 +
|        o        |                  |                  |
 +
|        |        |                  |                  |
 +
|        @        |    ((a)(b)(c))    |    a or b or c.  |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|                  |                  |    a implies b.  |
 +
|        a  b    |                  |                  |
 +
|        o---o    |                  |    if a then b.  |
 +
|        |        |                  |                  |
 +
|        @        |      (a (b))      |    no a sans b.  |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a  b      |                  |                  |
 +
|      o---o      |                  | a exclusive-or b. |
 +
|        \ /        |                  |                  |
 +
|        @        |      (a , b)      | a not equal to b. |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a  b      |                  |                  |
 +
|      o---o      |                  |                  |
 +
|        \ /        |                  |                  |
 +
|        o        |                  | a if & only if b. |
 +
|        |        |                  |                  |
 +
|        @        |    ((a , b))    | a equates with b. |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a  b  c      |                  |                  |
 +
|      o--o--o      |                  |                  |
 +
|      \  /      |                  |                  |
 +
|        \ /        |                  |  just one false  |
 +
|        @        |    (a , b , c)    |  out of a, b, c.  |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a  b  c      |                  |                  |
 +
|      o  o  o      |                  |                  |
 +
|      |  |  |      |                  |                  |
 +
|      o--o--o      |                  |                  |
 +
|      \  /      |                  |                  |
 +
|        \ /        |                  |  just one true  |
 +
|        @        |  ((a),(b),(c))  |  among a, b, c.  |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|                  |                  |  genus a over    |
 +
|        b  c      |                  |  species b, c.  |
 +
|        o  o      |                  |                  |
 +
|      a  |  |      |                  |  partition a    |
 +
|      o--o--o      |                  |  among b & c.    |
 +
|      \  /      |                  |                  |
 +
|        \ /        |                  |  whole pie a:    |
 +
|        @        |  ( a ,(b),(c))  |  slices b, c.    |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
</pre>
 +
|}
 +
 +
{| align="center" cellpadding="6" width="90%"
 +
| align="center" |
 +
<pre>
 +
Table 14.  The Entitative Interpretation
 +
o-------------------o-------------------o-------------------o
 +
|  Cactus Graph    | Cactus Expression |    Entitative    |
 +
|                  |                  |  Interpretation  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        @        |        " "        |      untrue.      |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        o        |                  |                  |
 +
|        |        |                  |                  |
 +
|        @        |        ( )        |      true.      |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        a        |                  |                  |
 +
|        @        |        a        |        a.        |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|        a        |                  |                  |
 +
|        o        |                  |                  |
 +
|        |        |                  |                  |
 +
|        @        |        (a)        |      not a.      |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a b c      |                  |                  |
 +
|        @        |      a b c      |    a or b or c.  |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a b c      |                  |                  |
 +
|      o o o      |                  |                  |
 +
|        \|/        |                  |                  |
 +
|        o        |                  |                  |
 +
|        |        |                  |                  |
 +
|        @        |    ((a)(b)(c))    |  a and b and c.  |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|                  |                  |    a implies b.  |
 +
|                  |                  |                  |
 +
|        o a      |                  |    if a then b.  |
 +
|        |        |                  |                  |
 +
|        @ b      |      (a) b        |    not a, or b.  |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a  b      |                  |                  |
 +
|      o---o      |                  | a if & only if b. |
 +
|        \ /        |                  |                  |
 +
|        @        |      (a , b)      | a equates with b. |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a  b      |                  |                  |
 +
|      o---o      |                  |                  |
 +
|        \ /        |                  |                  |
 +
|        o        |                  | a exclusive-or b. |
 +
|        |        |                  |                  |
 +
|        @        |    ((a , b))    | a not equal to b. |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a  b  c      |                  |                  |
 +
|      o--o--o      |                  |                  |
 +
|      \  /      |                  |                  |
 +
|        \ /        |                  | not just one true |
 +
|        @        |    (a , b , c)    | out of a, b, c.  |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a  b  c      |                  |                  |
 +
|      o--o--o      |                  |                  |
 +
|      \  /      |                  |                  |
 +
|        \ /        |                  |                  |
 +
|        o        |                  |                  |
 +
|        |        |                  |  just one true  |
 +
|        @        |  ((a , b , c))  |  among a, b, c.  |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
|                  |                  |                  |
 +
|      a            |                  |                  |
 +
|      o            |                  |  genus a over    |
 +
|      |  b  c      |                  |  species b, c.  |
 +
|      o--o--o      |                  |                  |
 +
|      \  /      |                  |  partition a    |
 +
|        \ /        |                  |  among b & c.    |
 +
|        o        |                  |                  |
 +
|        |        |                  |  whole pie a:    |
 +
|        @        |  ( a ,(b),(c))  |  slices b, c.    |
 +
|                  |                  |                  |
 +
o-------------------o-------------------o-------------------o
 +
</pre>
 +
|}
 +
 +
{| align="center" cellpadding="6" width="90%"
 +
| align="center" |
 +
<pre>
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|      Graph      |    String      |  Entitative    |  Existential  |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |                |
 +
|        @        |      " "      |    untrue.    |      true.      |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |                |
 +
|        o        |                |                |                |
 +
|        |        |                |                |                |
 +
|        @        |      ( )      |      true.      |    untrue.    |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |                |
 +
|        r        |                |                |                |
 +
|        @        |        r        |        r.      |        r.      |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |                |
 +
|        r        |                |                |                |
 +
|        o        |                |                |                |
 +
|        |        |                |                |                |
 +
|        @        |      (r)      |      not r.    |      not r.    |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |                |
 +
|      r s t      |                |                |                |
 +
|        @        |      r s t      |  r or s or t.  |  r and s and t. |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |                |
 +
|      r s t      |                |                |                |
 +
|      o o o      |                |                |                |
 +
|      \|/      |                |                |                |
 +
|        o        |                |                |                |
 +
|        |        |                |                |                |
 +
|        @        |  ((r)(s)(t))  |  r and s and t. |  r or s or t.  |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |  r implies s.  |
 +
|                |                |                |                |
 +
|        o r      |                |                |  if r then s.  |
 +
|        |        |                |                |                |
 +
|        @ s      |      (r) s      |  not r, or s    |  no r sans s.  |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |  r implies s.  |
 +
|        r  s    |                |                |                |
 +
|        o---o    |                |                |  if r then s.  |
 +
|        |        |                |                |                |
 +
|        @        |    (r (s))    |                |  no r sans s.  |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |                |
 +
|      r  s      |                |                |                |
 +
|      o---o      |                |                |r exclusive-or s.|
 +
|      \ /      |                |                |                |
 +
|        @        |    (r , s)    |                |r not equal to s.|
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |                |
 +
|      r  s      |                |                |                |
 +
|      o---o      |                |                |                |
 +
|      \ /      |                |                |                |
 +
|        o        |                |                |r if & only if s.|
 +
|        |        |                |                |                |
 +
|        @        |    ((r , s))    |                |r equates with s.|
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |                |
 +
|    r  s  t    |                |                |                |
 +
|    o--o--o    |                |                |                |
 +
|      \  /      |                |                |                |
 +
|      \ /      |                |                | just one false  |
 +
|        @        |  (r , s , t)  |                | out of r, s, t. |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |                |
 +
|    r  s  t    |                |                |                |
 +
|    o  o  o    |                |                |                |
 +
|    |  |  |    |                |                |                |
 +
|    o--o--o    |                |                |                |
 +
|      \  /      |                |                |                |
 +
|      \ /      |                |                |  just one true  |
 +
|        @        |  ((r),(s),(t))  |                |  among r, s, t. |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
|                |                |                |  genus t over  |
 +
|        r  s    |                |                |  species r, s.  |
 +
|        o  o    |                |                |                |
 +
|    t  |  |    |                |                |  partition t    |
 +
|    o--o--o    |                |                |  among r & s.  |
 +
|      \  /      |                |                |                |
 +
|      \ /      |                |                |  whole pie t:  |
 +
|        @        |  ( t ,(r),(s))  |                |  slices r, s.  |
 +
o-----------------o-----------------o-----------------o-----------------o
 +
</pre>
 +
|}
Jon Awbrey
12,080

edits

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