Changes

MyWikiBiz, Author Your Legacy — Sunday June 16, 2024
Jump to navigationJump to search

Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)

Revision as of 16:21, 18 August 2009

1,594 bytes removed ,  16:21, 18 August 2009
del redun & renum figs
Line 1,092: Line 1,092:  
|}
 
|}
   −
The reader can probably finish the second half of the proof with a few scribbles on paper faster than I can asciify it on my own, so at least there's that entertainment to occupy the interval.
+
It remains to show that the right hand side of the equation <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))}</math> is logically equivalent to the DNF just obtained.  The remainder of the needed chain of equations is as follows:  
−
 
  −
We are still in the middle of contemplating a particular example of a propositional equation, namely, <math>\texttt{(} p \texttt{(} q \texttt{))(} p \texttt{(} r \texttt{))} = \texttt{(} p \texttt{(} q r \texttt{))},</math> and we are still considering the second of three formal methods that are illustrated in the process of thrice-over establishing it.
  −
 
  −
{| align="center" cellpadding="8" style="text-align:center; width:90%"
  −
|
  −
<pre>
  −
o-----------------------------------------------------------o
  −
| Equation E_1                                              |
  −
o-----------------------------------------------------------o
  −
|                                                          |
  −
|                                          q r            |
  −
|          q o  o r                        o              |
  −
|            |  |                          |              |
  −
|          p o  o p                      p o              |
  −
|            \ /                            |              |
  −
|              @              =              @              |
  −
|                                                          |
  −
|      (p (q)) (p (r))      =          (p  (q r))        |
  −
|                                                          |
  −
|      [p=>q] & [p=>r]      =          [p=>[q&r]]        |
  −
|                                                          |
  −
o-----------------------------------------------------------o
  −
</pre>
  −
| (33)
  −
|}
  −
 
  −
We probably ought to go ahead and carry out the second half of this model-theoretic strategy, just so we'll have the security of this concrete experience to call on in future discussions.  The remainder of the needed chain of equations is as follows:
      
{| align="center" cellpadding="8" style="text-align:center; width:90%"
 
{| align="center" cellpadding="8" style="text-align:center; width:90%"
Line 1,268: Line 1,241:  
o=============================< DNF >=======================o
 
o=============================< DNF >=======================o
 
</pre>
 
</pre>
−
| (34)
+
| (33)
 
|}
 
|}
   Line 1,288: Line 1,261:  
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
</pre>
 
</pre>
−
| (35)
+
| (34)
 
|}
 
|}
   Line 1,312: Line 1,285:  
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
</pre>
 
</pre>
−
| (36)
+
| (35)
 
|}
 
|}
   Line 1,332: Line 1,305:  
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
</pre>
 
</pre>
−
| (37)
+
| (36)
 
|}
 
|}
   Line 1,351: Line 1,324:  
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
</pre>
 
</pre>
−
| (38)
+
| (37)
 
|}
 
|}
   Line 1,382: Line 1,355:  
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
</pre>
 
</pre>
−
| (39)
+
| (38)
 
|}
 
|}
   Line 1,444: Line 1,417:  
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
</pre>
 
</pre>
−
| (40)
+
| (39)
 
|}
 
|}
   Line 1,883: Line 1,856:  
o==================================< QED >==================o
 
o==================================< QED >==================o
 
</pre>
 
</pre>
−
| (41)
+
| (40)
 
|}
 
|}
   Line 2,174: Line 2,147:     
{| align="center" cellpadding="6" style="text-align:center"
 
{| align="center" cellpadding="6" style="text-align:center"
−
| [[Image:Venn Diagram (P (Q)).jpg|500px]] || (43)
+
| [[Image:Venn Diagram (P (Q)).jpg|500px]] || (42)
 
|-
 
|-
 
| <math>f_{207}(p, q, r) ~=~ \texttt{(} p \texttt{~(} q \texttt{))}</math>
 
| <math>f_{207}(p, q, r) ~=~ \texttt{(} p \texttt{~(} q \texttt{))}</math>
Line 2,180: Line 2,153:  
| &nbsp;
 
| &nbsp;
 
|-
 
|-
−
| [[Image:Venn Diagram (Q (R)).jpg|500px]] || (44)
+
| [[Image:Venn Diagram (Q (R)).jpg|500px]] || (43)
 
|-
 
|-
 
| <math>f_{187}(p, q, r) ~=~ \texttt{(} q \texttt{~(} r \texttt{))}</math>
 
| <math>f_{187}(p, q, r) ~=~ \texttt{(} q \texttt{~(} r \texttt{))}</math>
Line 2,186: Line 2,159:  
| &nbsp;
 
| &nbsp;
 
|-
 
|-
−
| [[Image:Venn Diagram (P (R)).jpg|500px]] || (45)
+
| [[Image:Venn Diagram (P (R)).jpg|500px]] || (44)
 
|-
 
|-
 
| <math>f_{175}(p, q, r) ~=~ \texttt{(} p \texttt{~(} r \texttt{))}</math>
 
| <math>f_{175}(p, q, r) ~=~ \texttt{(} p \texttt{~(} r \texttt{))}</math>
Line 2,192: Line 2,165:  
| &nbsp;
 
| &nbsp;
 
|-
 
|-
−
| [[Image:Venn Diagram (P (Q)) (Q (R)).jpg|500px]] || (46)
+
| [[Image:Venn Diagram (P (Q)) (Q (R)).jpg|500px]] || (45)
 
|-
 
|-
 
| <math>f_{139}(p, q, r) ~=~ \texttt{(} p \texttt{~(} q \texttt{))~(} q \texttt{~(} r \texttt{))}</math>
 
| <math>f_{139}(p, q, r) ~=~ \texttt{(} p \texttt{~(} q \texttt{))~(} q \texttt{~(} r \texttt{))}</math>
Line 2,437: Line 2,410:  
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 let us next lay out some visual schemata that are designed to facilitate that.
 
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 let us next lay out some visual schemata that are designed to facilitate that.
   −
Figure&nbsp;28-a shows the familiar picture of a boolean 3-cube, where the points of <math>\mathbb{B}^3</math> are coordinated as bit strings of length three.  Looking at the functions <math>f : \mathbb{B}^3 \to \mathbb{B}</math> and the relations <math>L \subseteq \mathbb{B}^3</math> 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 <math>L = [| f |]\!</math> and which points are out of it.  Bowing to common convention, we may use the color <math>1\!</math> for points that are ''in'' a given relation and the color <math>0\!</math> for points that are ''out'' of the 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".
+
Figure&nbsp;52 shows the familiar picture of a boolean 3-cube, where the points of <math>\mathbb{B}^3</math> are coordinated as bit strings of length three.  Looking at the functions <math>f : \mathbb{B}^3 \to \mathbb{B}</math> and the relations <math>L \subseteq \mathbb{B}^3</math> 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 <math>L = [| f |]\!</math> and which points are out of it.  Bowing to common convention, we may use the color <math>1\!</math> for points that are ''in'' a given relation and the color <math>0\!</math> for points that are ''out'' of the 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".
    
{| align="center" cellpadding="10" style="text-align:center; width:90%"
 
{| align="center" cellpadding="10" style="text-align:center; width:90%"
Line 2,471: Line 2,444:  
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
−
Figure 28-a.  Boolean 3-Cube B^3
+
Figure 52.  Boolean 3-Cube B^3
 
</pre>
 
</pre>
−
| (53)
+
| (52)
 
|}
 
|}
   −
Table&nbsp;54 shows the 3-adic relation <math>\operatorname{Syll} \subseteq \mathbb{B}^3</math> again, and Figure&nbsp;55 shows it plotted on a 3-cube template.
+
Table&nbsp;53 shows the 3-adic relation <math>\operatorname{Syll} \subseteq \mathbb{B}^3</math> again, and Figure&nbsp;54 shows it plotted on a 3-cube template.
    
{| align="center" cellpadding="10" style="text-align:center; width:90%"
 
{| align="center" cellpadding="10" style="text-align:center; width:90%"
 
|
 
|
 
<pre>
 
<pre>
−
Table 54.  Syll c B^3
+
Table 53.  Syll c B^3
 
o-----------------------o
 
o-----------------------o
 
|  p      q      r  |
 
|  p      q      r  |
Line 2,491: Line 2,464:  
o-----------------------o
 
o-----------------------o
 
</pre>
 
</pre>
−
| (54)
+
| (53)
 
|-
 
|-
 
|
 
|
Line 2,524: Line 2,497:  
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
−
Figure 55.  Triadic Relation Syll c B^3
+
Figure 54.  Triadic Relation Syll c B^3
 
</pre>
 
</pre>
−
| (55)
+
| (54)
 
|}
 
|}
   Line 2,534: Line 2,507:  
|
 
|
 
<pre>
 
<pre>
−
Table 56.  Syll c B^3
+
Table 55.  Syll c B^3
 
o-----------------------o
 
o-----------------------o
 
|  p      q      r  |
 
|  p      q      r  |
Line 2,544: Line 2,517:  
o-----------------------o
 
o-----------------------o
 
</pre>
 
</pre>
−
| (56)
+
| (55)
 
|-
 
|-
 
|
 
|
 
<pre>
 
<pre>
−
Table 57.  Dyadic Projections of Syll
+
Table 56.  Dyadic Projections of Syll
 
o-----------o o-----------o o-----------o
 
o-----------o o-----------o o-----------o
 
|  Syll_12  | |  Syll_13  | |  Syll_23  |
 
|  Syll_12  | |  Syll_13  | |  Syll_23  |
Line 2,561: Line 2,534:  
o-----------o o-----------o o-----------o
 
o-----------o o-----------o o-----------o
 
</pre>
 
</pre>
−
| (57)
+
| (56)
 
|}
 
|}
    
In showing the 2-adic projections of a 3-adic relation <math>L \subseteq \mathbb{B}^3,</math> 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.
 
In showing the 2-adic projections of a 3-adic relation <math>L \subseteq \mathbb{B}^3,</math> 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&nbsp;58 shows <math>\operatorname{Syll}</math> and its three 2-adic projections:
+
Figure&nbsp;57 shows <math>\operatorname{Syll}</math> and its three 2-adic projections:
    
{| align="center" cellpadding="10" style="text-align:center; width:90%"
 
{| align="center" cellpadding="10" style="text-align:center; width:90%"
Line 2,622: Line 2,595:  
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
−
Figure 58.  Syll c B^3 and its Dyadic Projections
+
Figure 57.  Syll c B^3 and its Dyadic Projections
 
</pre>
 
</pre>
−
| (58)
+
| (57)
 
|}
 
|}
   Line 2,632: Line 2,605:  
|
 
|
 
<pre>
 
<pre>
−
Table 59.  Syll c B^3
+
Table 58.  Syll c B^3
 
o-----------------------o
 
o-----------------------o
 
|  p      q      r  |
 
|  p      q      r  |
Line 2,642: Line 2,615:  
o-----------------------o
 
o-----------------------o
 
</pre>
 
</pre>
−
| (59)
+
| (58)
 
|-
 
|-
 
|
 
|
 
<pre>
 
<pre>
−
Table 60.  Dyadic Projections of Syll
+
Table 59.  Dyadic Projections of Syll
 
o-----------o o-----------o o-----------o
 
o-----------o o-----------o o-----------o
 
|  Syll_12  | |  Syll_13  | |  Syll_23  |
 
|  Syll_12  | |  Syll_13  | |  Syll_23  |
Line 2,659: Line 2,632:  
o-----------o o-----------o o-----------o
 
o-----------o o-----------o o-----------o
 
</pre>
 
</pre>
−
| (60)
+
| (59)
 
|-
 
|-
 
|
 
|
 
<pre>
 
<pre>
−
Table 61.  Tacit Extensions of Projections of Syll
+
Table 60.  Tacit Extensions of Projections of Syll
 
o---------------o o---------------o o---------------o
 
o---------------o o---------------o o---------------o
 
|  te(Syll_12)  | |  te(Syll_13)  | |  te(Syll_23)  |
 
|  te(Syll_12)  | |  te(Syll_13)  | |  te(Syll_23)  |
Line 2,681: Line 2,654:  
o---------------o o---------------o o---------------o
 
o---------------o o---------------o o---------------o
 
</pre>
 
</pre>
−
| (61)
+
| (60)
 
|-
 
|-
 
|
 
|
Line 2,724: Line 2,697:  
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
−
Figure 62.  Tacit Extension te_12_3 (Syll_12)
+
Figure 61.  Tacit Extension te_12_3 (Syll_12)
 
</pre>
 
</pre>
−
| (62)
+
| (61)
 
|-
 
|-
 
|
 
|
Line 2,778: Line 2,751:  
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
−
Figure 63.  Tacit Extension te_13_2 (Syll_13)
+
Figure 62.  Tacit Extension te_13_2 (Syll_13)
 
</pre>
 
</pre>
−
| (63)
+
| (62)
 
|-
 
|-
 
|
 
|
Line 2,823: Line 2,796:  
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
−
Figure 64.  Tacit Extension te_23_1 (Syll_23)
+
Figure 63.  Tacit Extension te_23_1 (Syll_23)
 
</pre>
 
</pre>
−
| (64)
+
| (63)
 
|}
 
|}
   −
The reader may wish to contemplate Figure&nbsp;31 and use it to verify the following two facts:
+
The reader may wish to contemplate Figure&nbsp;64 and use it to verify the following two facts:
    
{| align="center" cellpadding="8" width="90%"
 
{| align="center" cellpadding="8" width="90%"
Line 2,901: Line 2,874:  
|                                                |
 
|                                                |
 
o-------------------------------------------------o
 
o-------------------------------------------------o
−
Figure 65.  Syll = te(Syll_12) |^| te(Syll_23)
+
Figure 64.  Syll = te(Syll_12) |^| te(Syll_23)
 
</pre>
 
</pre>
−
| (65)
+
| (64)
 
|}
 
|}
   Line 2,910: Line 2,883:  
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.
 
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&nbsp;66 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 &mdash; much in the way that one might compile a theory from axioms without knowing what either the theory or the axioms were about &mdash; 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.
+
At first or maybe second sight, the relationships seem easy enough to write out.  Figure&nbsp;65 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 &mdash; much in the way that one might compile a theory from axioms without knowing what either the theory or the axioms were about &mdash; 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.
    
<pre>
 
<pre>
Line 2,966: Line 2,939:  
               o-------------------o               
 
               o-------------------o               
 
                                                    
 
                                                    
−
Figure 66.  Expressive Aspects of Transitive Inference
+
Figure 65.  Expressive Aspects of Transitive Inference
 
</pre>
 
</pre>
   Line 2,975: Line 2,948:  
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''.
 
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&nbsp;67 is an attempt to outline the model-theoretic relationships that are involved in our study of transitive inference.  A couple of alternative notations are introduced in this Table:
+
Figure&nbsp;66 is an attempt to outline the model-theoretic relationships that are involved in our study of transitive inference.  A couple of alternative notations are introduced in this Table:
    
{| align="center" cellpadding="8" width="90%"
 
{| align="center" cellpadding="8" width="90%"
Line 3,045: Line 3,018:  
o---------o---------o        o---------o---------o
 
o---------o---------o        o---------o---------o
 
                                                    
 
                                                    
−
Figure 67.  Denotative Aspects of Transitive Inference
+
Figure 66.  Denotative Aspects of Transitive Inference
 
</pre>
 
</pre>
   Line 3,083: Line 3,056:  
An abstract reference to a point of <math>X\!</math> is a triple in <math>\mathbb{B}^3.</math>  A concrete reference to a point of <math>X\!</math> is a conjunction of signs from the dimensions <math>P^\ddagger, Q^\ddagger, R^\ddagger,</math> picking exactly one sign from each dimension.
 
An abstract reference to a point of <math>X\!</math> is a triple in <math>\mathbb{B}^3.</math>  A concrete reference to a point of <math>X\!</math> is a conjunction of signs from the dimensions <math>P^\ddagger, Q^\ddagger, R^\ddagger,</math> picking exactly one sign from each dimension.
   −
To illustrate the use of concrete coordinates for points and concrete types for spaces and propositions, Figure&nbsp;68 translates the contents of Figure 33 into the new language.
+
To illustrate the use of concrete coordinates for points and concrete types for spaces and propositions, Figure&nbsp;67 translates the contents of Figure&nbsp;66 into the new language.
    
<pre>
 
<pre>
Line 3,147: Line 3,120:  
o---------o---------o        o---------o---------o
 
o---------o---------o        o---------o---------o
 
                                                      
 
                                                      
−
Figure 68.  Denotative Aspects of Transitive Inference
+
Figure 67.  Denotative Aspects of Transitive Inference
 
</pre>
 
</pre>
  
Jon Awbrey
12,080

edits

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

Navigation menu