Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

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