ONT Re: Propositional Equation Reasoning Systems
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PERS. Note 15
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
To continue with the beating of this still kicking horse that is
known as the propositional equation "(p (q))(p (r)) = (p (q r))",
let's now take up the "third way" that I mentioned for examining
propositional equations, but I believe that you will be relieved
to know that it is literally a third way only at the very outset,
almost immediately breaking up according to whether one proceeds
model-wise or proof-wise thereafter.
Let's metamorphose our propositional equation:
(p (q))(p (r)) = (p (q r)),
into the corresponding equational proposition:
(( (p (q))(p (r)) , (p (q r)) )).
I am sure that you would rather see the movie:
o-----------------------------------------------------------o
| Equation E1, as Expressed in the Cactus Language |
o-----------------------------------------------------------o
| |
| q o o r q o r |
| | | | |
| p o o p p o |
| \ / | |
| o---------o |
| \ / |
| \ / |
| \ / |
| \ / |
| o |
| | |
| | |
| | |
| | |
| @ |
| |
| (( (p (q)) (p (r)) , (p (q r)) )) |
| |
| [[p=>q] & [p=>r]] <=> [p=>[q&r]] |
| |
o-----------------------------------------------------------o
Let us now interrogate the alleged theorem that was lined up last time.
I will proceed quasi modo the "Case Analysis-Synthesis Theorem" (CAST),
that is to say, start out in a way that is model-wise if proof-foolish,
just because this is the manner that requires the least foresight, and
I am not feeling very Promethean today. One lemma that I can see just
far ahead enough to see that we'll need to provision ourselves with is
this principle here, that a bare lobe expression like "( , ... )" with
any number places for arguments but nothing but blanks to fill them up
is logically tantamount to the proto-typical expression of its species,
to wit, the constant expression "()" that an existentialist interprets
as denoting the logical value "false". To depict it in graphical form:
o-----------------------------------------------------------o
| Emptiness Rule |
o-----------------------------------------------------------o
| |
| o o---o o-o-o |
| | \ / \ / |
| @ = @ = @ = ... |
| |
o-----------------------------------------------------------o
Let us for the nonce dub this the "emptiness rule"
and worry later how to enscounce it in our system.
Yet another rule that we'll need is the following:
o-----------------------------------------------------------o
| Indistinctness Rule |
o-----------------------------------------------------------o
| |
| a a a a a |
| o o---o o-o-o |
| | \ / \ / |
| @ = @ = @ = ... |
| |
o-----------------------------------------------------------o
This one is easy enough to derive from rules that are
already known, but call it the "indistinctness rule"
just on behalf of ready reference and employment.
Finally, let me introduce a rule-of-thumb that is a bit
more suited to routine computation, and that will serve
to replace the indistinctness rule in many of the cases
where we actually have to call on it. This is actually
just a special case of the evaluation rule listed above:
o-----------------------------------------------------------o
| Evaluation Rule |
o-----------------------------------------------------------o
| |
| o |
| | x_2 ... x_k |
| o---o-...-o---o |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / x_2 ... x_k |
| @ = @ |
| |
o-----------------------------------------------------------o
| |
| ((), x_2, ..., x_k) = x_2 ... x_k |
| |
o-----------------------------------------------------------o
| Setup <---- | ----> Spike |
o-----------------------------------------------------------o
I believe that this will be enough of a grubstake for us
prospectors of proof and truth to see what pans out here:
o-----------------------------------------------------------o
| Equation E1. Proof 3. |
o-----------------------------------------------------------o
| |
| q o o r q o r |
| | | | |
| p o o p p o |
| \ / | |
| o---------o |
| \ / |
| \ / |
| \ / |
| \ / |
| o |
| | |
| | |
| | |
| | |
| @ |
| |
o==================================< CAST "p" >=============o
| |
| q r q r q r qr |
| o o o o o o o o o |
| | | | |/ |/ |/ |
| o o o o o o |
| \ / | \ / | |
| o-------o o-------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| o o |
| | | |
| | | |
| | | |
| p o---------------o---o p |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Domination >===========o
| |
| q r q r |
| o o o o o o |
| | | | / / / |
| o o o o o o |
| \ / | \ / | |
| o-------o o-------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| o o |
| | | |
| | | |
| | | |
| p o---------------o---o p |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Cancellation >=========o
| |
| q r q r |
| o o o |
| | | | |
| o o o |
| \ / | |
| o-------o o-------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| o o |
| | | |
| | | |
| | | |
| p o---------------o---o p |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Emptiness >============o
| |
| q r q r |
| o o o |
| | | | |
| o o o |
| \ / | |
| o-------o o |
| \ / | |
| \ / | |
| \ / | |
| o o |
| | | |
| | | |
| | | |
| p o---------------o---o p |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Cancellation >=========o
| |
| q r q r |
| o o o |
| | | | |
| o o o |
| \ / | |
| o-------o |
| \ / |
| \ / |
| \ / |
| o |
| | |
| | |
| | |
| p o---------------o---o p |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< CAST "q" >=============o
| |
| o o |
| r r | r | |
| o o o o o o r |
| | | | | | | |
| o o o o o o |
| \ / | \ / | |
| o-------o o-------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| o o |
| | | |
| | | |
| | | |
| q o---------------o---o q |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Domination >===========o
| |
| o o |
| r r | r | |
| o o o o o o |
| | | | | | | |
| o o o o o o |
| \ / | \ / | |
| o-------o o-------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| o o |
| | | |
| | | |
| | | |
| q o---------------o---o q |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Cancellation >=========o
| |
| r r r |
| o o o |
| | | | |
| o o o o o |
| / | \ / | |
| o-------o o-------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| o o |
| | | |
| | | |
| | | |
| q o---------------o---o q |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Domination >===========o
| |
| r r |
| o o |
| | | |
| o o o o |
| / | \ | |
| o-------o o-------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| o o |
| | | |
| | | |
| | | |
| q o---------------o---o q |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Spike >================o
| |
| r r |
| o o |
| | | |
| o o |
| / | |
| o-------o o |
| \ / | |
| \ / | |
| \ / | |
| o o |
| | | |
| | | |
| | | |
| q o---------------o---o q |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Cancellation >=========o
| |
| r r |
| o o |
| | | |
| o o |
| / | |
| o-------o |
| \ / |
| \ / |
| \ / |
| o |
| | |
| | |
| | |
| q o---------------o---o q |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< CAST "r" >=============o
| |
| o o |
| | | |
| o o o o |
| | | | | |
| o o o o |
| / | / | |
| o-------o o-------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| o o |
| | | |
| | | |
| | | |
| r o---------------o---o r |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| q o-------o---o q |
| \ / |
| \ / |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Cancellation >=========o
| |
| o o |
| / | |
| o-------o o-------o |
| \ / \ / |
| \ / \ / |
| \ / \ / |
| o o |
| | | |
| | | |
| | | |
| r o---------------o---o r |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| q o-------o---o q |
| \ / |
| \ / |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Emptiness & Spike >====o
| |
| o o |
| | | |
| | | |
| | | |
| o o |
| | | |
| | | |
| | | |
| r o---------------o---o r |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| \ / |
| q o-------o---o q |
| \ / |
| \ / |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< Cancellation >=========o
| |
| r o-------o---o r |
| \ / |
| \ / |
| \ / |
| q o-------o---o q |
| \ / |
| \ / |
| \ / |
| p o-------o---o p |
| \ / |
| \ / |
| \ / |
| @ |
| |
o==================================< QED >==================o
And that, of course, is the DNF of a theorem.
Jon Awbrey
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o