Changes

Line 271: Line 271:  
I think that I am at long last ready to state the following:
 
I think that I am at long last ready to state the following:
    +
{| align="center" cellpadding="10" style="text-align:center; width:90%"
 +
|
 
<pre>
 
<pre>
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
Line 289: Line 291:  
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
</pre>
 
</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.
 
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.
    +
{| align="center" cellpadding="10" style="text-align:center; width:90%"
 +
|
 
<pre>
 
<pre>
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
Line 312: Line 317:  
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
</pre>
 
</pre>
&nbsp;
+
|-
 +
|
 
<pre>  
 
<pre>  
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
Line 331: Line 337:  
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
</pre>
 
</pre>
&nbsp;
+
|-
 +
|
 
<pre>  
 
<pre>  
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
Line 358: Line 365:  
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
 
</pre>
 
</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.
 
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.
Line 363: Line 371:  
Here is a proof sketch for the ''Case Analysis-Synthesis Theorem'' (CAST):
 
Here is a proof sketch for the ''Case Analysis-Synthesis Theorem'' (CAST):
    +
{| align="center" cellpadding="10" style="text-align:center; width:90%"
 +
|
 
<pre>
 
<pre>
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
Line 409: Line 419:  
o=============================< QES >=======================o
 
o=============================< QES >=======================o
 
</pre>
 
</pre>
 +
|}
    
NB.  QES = "Quod Erat Sketchiendum".
 
NB.  QES = "Quod Erat Sketchiendum".
Line 414: Line 425:  
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.
 
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.
    +
{| align="center" cellpadding="10" style="text-align:center; width:90%"
 +
|
 
<pre>
 
<pre>
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
Line 797: Line 810:  
o=============================< QED >=======================o
 
o=============================< QED >=======================o
 
</pre>
 
</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:
 
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:
    +
{| align="center" cellpadding="10" style="text-align:center; width:90%"
 +
|
 
<pre>
 
<pre>
 
o-----------------------------------------------------------o
 
o-----------------------------------------------------------o
Line 826: Line 842:  
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''.
 
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''.
12,080

edits