ONT Re: Propositional Equation Reasoning Systems
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PERS. Note 8
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
CAST (cont.)
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 seeking for a more proper formulation.
o-----------------------------------------------------------o
| Precept L1. Indifference |
o-----------------------------------------------------------o
| |
| a |
| o |
| a | |
| o---o |
| \ / |
| @ = @ |
| |
o-----------------------------------------------------------o
| |
| (a, (a)) = |
| |
o-----------------------------------------------------------o
| Split <---- | ----> Merge |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
| Precept L2. Equality. The Following Are Equivalent: |
o-----------------------------------------------------------o
| |
| b a b a |
| o o---o o |
| a | \ / | b |
| o---o o o---o |
| \ / | \ / |
| @ = @ = @ |
| |
o-----------------------------------------------------------o
| |
| (a, (b)) = ((a , b)) = ((a), b) |
| |
o-----------------------------------------------------------o
o-----------------------------------------------------------o
| Precept L3. Dispersion |
o-----------------------------------------------------------o
| |
| For k > 1, the following equation holds: |
| |
| y_1 y_2 ... y_k x y_1 x y_2 ... x y_k |
| o------o-...-o------o o------o-...-o------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| x @ = @ |
| |
| x (y_1, ..., y_k) = (x y_1, ..., x y_k) |
| |
o-----------------------------------------------------------o
| Distill <---- | ----> Disperse |
o-----------------------------------------------------------o
To see why the Dispersion Rule holds, look at it this way:
If x is true, then the presence of "x" makes no difference
on either side of the equation, but if x is false, then both
sides of the equation are false.
Here is a proof sketch for the "Case Analysis-Synthesis Theorem" (CAST):
o-----------------------------------------------------------o
| Case Analysis-Synthesis Theorem. Proof Sketch. |
o-----------------------------------------------------------o
| |
| Q |
| @ |
| |
o=============================< L1. Split " " >=============o
| |
| x |
| o |
| x | |
| o---o |
| \ / |
| Q @ |
| |
o=============================< L3. Disperse "Q" >==========o
| |
| x |
| o |
| x | |
| Q o---o Q |
| \ / |
| @ |
| |
o=============================< C1. Reflect "x" >===========o
| |
| x |
| o |
| x | |
| Q o---o Q[((x))/x] |
| \ / |
| @ |
| |
o=============================< C2. Weed "x", "(x)" >=======o
| |
| x |
| o |
| x | |
| Q[o/x] o---o Q[|/x] |
| \ / |
| @ |
| |
o=============================< QES >=======================o
Nota Bene. QES = "Quod Erat Sketchum".
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o