ONT Re: Propositional Equation Reasoning Systems
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PERS. Note 5
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Now to take up a more interesting example,
here is the statement and a proof of the
Splendid Theorem from Leibniz that was
brought to my attention by John Sowa.
| If 'a' is 'b' and 'd' is 'c', then 'ad' will be 'bc'.
| This is a fine theorem, which is proved in this way:
|
| 'a' is 'b', therefore 'ad' is 'bd' (by what precedes),
|
| 'd' is 'c', therefore 'bd' is 'bc' (again by what precedes),
|
| 'ad' is 'bd', and 'bd' is 'bc', therefore 'ad' is 'bc'. Q.E.D.
|
| Leibniz, 'Logical Papers', page 41.
|
| Leibniz, G.W., 'Addenda to the Specimen of the Universal Calculus',
| pages 40-46 in Parkinson, G.H.R. (ed.), 'Leibniz: Logical Papers',
| Oxford University Press, London, UK, 1966. (Gerhardt, 7, p. 223).
o-----------------------------------------------------------o
| Praeclarum Theorema (Leibniz) |
o-----------------------------------------------------------o
| |
| b o o c o bc |
| | | | |
| a o o d o ad |
| \ / | |
| o---------o |
| | |
| | |
| @ = @ |
| |
o-----------------------------------------------------------o
| |
| ((a(b))(d(c))((ad(bc)))) = |
| |
o-----------------------------------------------------------o
And here's a neat proof of that nice theorem.
o-----------------------------------------------------------o
| Praeclarum Theorema (Leibniz). Proof. |
o-----------------------------------------------------------o
| |
| b o o c o bc |
| | | | |
| a o o d o ad |
| \ / | |
| o---------o |
| | |
| | |
| @ |
| |
o=============================< C1. Reflect "ad(bc)" >======o
| |
| b o o c |
| | | |
| a o o d |
| \ / |
| ad o---------o bc |
| | |
| | |
| @ |
| |
o=============================< Weed "a", "d" >=============o
| |
| b o o c |
| | | |
| o o |
| \ / |
| ad o---------o bc |
| | |
| | |
| @ |
| |
o=============================< C1. Reflect "b", "c" >======o
| |
| abcd o---------o bc |
| | |
| | |
| @ |
| |
o=============================< Weed "bc" >=================o
| |
| abcd o---------o |
| | |
| | |
| @ |
| |
o=============================< C3. Recess "abcd" >=========o
| |
| o---------o |
| | |
| | |
| @ |
| |
o=============================< I2. Refold "(())" >=========o
| |
| @ |
| |
o=============================< QED >=======================o
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o