Changes

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:

<pre>

<pre>

o-----------------------------------------------------------o

o-----------------------------------------------------------o

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.

<pre>

<pre>

o-----------------------------------------------------------o

o-----------------------------------------------------------o

o-----------------------------------------------------------o

o-----------------------------------------------------------o

</pre>

</pre>

<pre>  

<pre>  

o-----------------------------------------------------------o

o-----------------------------------------------------------o

o-----------------------------------------------------------o

o-----------------------------------------------------------o

</pre>

</pre>

<pre>  

<pre>  

o-----------------------------------------------------------o

o-----------------------------------------------------------o

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.

Here is a proof sketch for the ''Case Analysis-Synthesis Theorem'' (CAST):

Here is a proof sketch for the ''Case Analysis-Synthesis Theorem'' (CAST):

<pre>

<pre>

o-----------------------------------------------------------o

o-----------------------------------------------------------o

o=============================< QES >=======================o

o=============================< QES >=======================o

</pre>

</pre>

NB.  QES = "Quod Erat Sketchiendum".

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.

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>

<pre>

o-----------------------------------------------------------o

o-----------------------------------------------------------o

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:

<pre>

<pre>

o-----------------------------------------------------------o

o-----------------------------------------------------------o

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''.