ONT Re: Propositional Equation Reasoning Systems
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PERS. Note 9
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
CAST (cont.)
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.
o-----------------------------------------------------------o
| Praeclarum Theorema. Proof by CAST. |
o-----------------------------------------------------------o
| |
| b o o c o bc |
| | | | |
| a o o d o ad |
| \ / | |
| o---------o |
| | |
| | |
| @ |
| |
o=============================< CAST "a" >==================o
| |
| bc |
| b o o c o bc b o o c o o |
| | | | | | |/ |
| o o d o d o--o o d o d |
| \ / | \ / | |
| o-------o o-------o |
| | | |
| | | |
| a o-----------------------------o---o a |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o=============================< Domination >================o
| |
| b o o c o bc o c o |
| | | | | / |
| o o d o d o--o o d o |
| \ / | \ / | |
| o-------o o-------o |
| | | |
| | | |
| a o-----------------------------o---o a |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o=============================< Cancellation >==============o
| |
| b o o c o bc o c |
| | | | | |
| o o d o d o d |
| \ / | / |
| o-------o o-------o |
| | | |
| | | |
| a o-----------------------------o---o a |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o=============================< Domination >================o
| |
| b o o c o bc |
| | | | |
| o o d o d |
| \ / | |
| o-------o o-------o |
| | | |
| | | |
| a o-----------------------------o---o a |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o=============================< Cancellation >==============o
| |
| b o o c o bc |
| | | | |
| o o d o d |
| \ / | |
| o-------o |
| | |
| | |
| a o-----------------------------o---o a |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o=============================< CAST "d" >==================o
| |
| b c bc |
| b o o c o bc o o o o o |
| | | | | |/ |/ |
| o o o o o o |
| \ / | \ / | |
| o-------o o-------o |
| | | |
| | | |
| d o-------------------------o---o d |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< Domination >================o
| |
| b |
| b o o c o bc o o o |
| | | | | / / |
| o o o o o o |
| \ / | \ / | |
| o-------o o-------o |
| | | |
| | | |
| d o-------------------------o---o d |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< Cancellation >==============o
| |
| b |
| b o o c o bc o |
| | | | | |
| o o o o |
| \ / | \ |
| o-------o o-------o |
| | | |
| | | |
| d o-------------------------o---o d |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< Domination >================o
| |
| b o o c o bc |
| | | | |
| o o o |
| \ / | |
| o-------o o-------o |
| | | |
| | | |
| d o-------------------------o---o d |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< Cancellation >==============o
| |
| b o o c o bc |
| | | | |
| o o o |
| \ / | |
| o-------o |
| | |
| | |
| d o-------------------------o---o d |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< CAST "b" >==================o
| |
| o o |
| | | |
| o o c o c o o c o c |
| | | | | | | |
| o o o o o o |
| \ / | \ / | |
| o-------o o-------o |
| | | |
| | | |
| b o-------------------------o---o b |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| d o---o---o d |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< Cancellation >==============o
| |
| o |
| | |
| o c o c o c o c |
| | | | | |
| o o o o o |
| / | \ / | |
| o-------o o-------o |
| | | |
| | | |
| b o-------------------------o---o b |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| d o---o---o d |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< Domination >================o
| |
| o c o c |
| | | |
| o o o |
| / | \ |
| o-------o o |
| | | |
| | | |
| b o-------------------------o---o b |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| d o---o---o d |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< Cancellation >==============o
| |
| o c o c |
| | | |
| o o |
| / | |
| o-------o |
| | |
| | |
| b o-------------------------o---o b |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| d o---o---o d |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< CAST "c" >==================o
| |
| o o |
| | | |
| o o o o |
| | | | | |
| o o o o |
| / | / | |
| o-------o o-------o |
| | | |
| | | |
| c o-------------------------o---o c |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| b o---o---o b |
| \ / |
| d o---o---o d |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< Cancellation >==============o
| |
| o o |
| / | |
| o-------o o-------o |
| | | |
| | | |
| c o-------------------------o---o c |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| b o---o---o b |
| \ / |
| d o---o---o d |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< Cancellation >==============o
| |
| c o---o---o c |
| \ / |
| b o---o---o b |
| \ / |
| d o---o---o d |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o=============================< QED >=======================o
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:
o-----------------------------------------------------------o
| |
| c o---o---o c |
| \ / |
| b o---o---o b |
| \ / |
| d o---o---o d |
| \ / |
| a o---o---o a |
| \ / |
| @ |
| |
o-----------------------------------------------------------o
| |
| Either not 'a' and thus 'true' |
| Or 'a' and thus |
| Either not 'd' and thus 'true' |
| Or 'd' and thus |
| Either not 'b' and thus 'true' |
| Or 'b' and thus |
| Either not 'c' and thus 'true' |
| Or 'c' and thus 'true'. |
| |
o-----------------------------------------------------------o
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 "Theorem".
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o