ONT Re: Propositional Equation Reasoning Systems
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PERS. Note 4
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
The third theorem to be proved here is one that GSB
annotates as "Integration", but I tend to regard it
as a matter of "Dominance or Recession" among forms.
o-----------------------------------------------------------o
| C3. Dominant Form Theorem |
o-----------------------------------------------------------o
| |
| o o |
| | | |
| a @ = @ |
| |
o-----------------------------------------------------------o
| |
| a( ) = ( ) |
| |
o-----------------------------------------------------------o
| Remark <---- | ----> Recess |
o-----------------------------------------------------------o
Here is a proof of the Dominant Form Theorem.
o-----------------------------------------------------------o
| C3. Dominant Form Theorem. Proof. |
o-----------------------------------------------------------o
| |
| o |
| | |
| a @ |
| |
o=============================< C2. Regenerate "a" >========o
| |
| a o |
| | |
| a @ |
| |
o=============================< J1. Delete "a" >============o
| |
| o |
| | |
| @ |
| |
o=============================< QED >=======================o
If you scan the elementary steps that lead up to this point,
you will notice two distinct qualities to the proofs so far:
One brand of proof has that "falling off a log and rolling downhill"
sort of quality that is earnestly to be wished for but seldom to be
seen, at least, never so often as we'd wish.
The other kind, more kith o' death than kind, has a quality strained
past mercy, with a "how in the heck did anybody ever think of that?"
sort of subtlety that all too unfortunately rules the roost whenever
we begin to extend out practice to more and more compelling theories.
This is, to me, at least, a surprising observation,
and though I have no grand conclusion to draw from
it at the moment, it occurs to me that it might be
a useful measure to keep in mind as we essay forth.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o