SUO: Re: Propositional Equation Reasoning Systems (PERS)
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
We are in the midst of examining the propositional equation:
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
|
| q r
| q o o r o
| | | |
| p o o p p o
| \ / |
| @ = @
|
| (p (q)) (p (r)) = (p (q r))
|
| [p=>q] & [p=>r] = [p=>[q&r]]
|
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
We have seen what we would probably consider an informal way
of seeing the validity of this equation, and then we took up
a rather more formal path, blazing our proof-theoretic trek*
from the sinister charge to the dexter emblem, working under
the aegis -- like Odysseus and his cohorts escaping from the
cave of the Cyclops under the skins of some hapless sheep --
somehow that image just popped into my mind -- of principles
that I, in deference to long-cherished custom, call "axioms",
though others, more cautious than customary, have elected to
invoke as pure "initials", and if we are satisfied, at least,
for the moment or the sake of the argument, that these rules
preserve the logical equivalence class of the expressions to
which they are aptly applied, then, proceeding on the chancy
presumption that our application of the givens is apt enough,
we can reckon ourselves to be in the possession of a genuine
demonstration that the distaff is well-matched for the spear.
By the way, for knowing blazoneers, my shield is transparent.
The second way of establishing the truth of this equation is
one that I called, rather loosely, "model-theoretic", for no
better reason than the sense of its ending with a pattern of
expression, a variant on the "disjunctive normal form" (DNF),
which is commonly recognized to be that which one can derive
from a truth table by pulling out the rows of the table that
evaluate to true and constructing the disjunctive expression
that sums up the senses of the corresponding interpretations.
In order to apply this "model-theoretic" method to an equation
between a couple of contingent expressions, one must transform
each expression into its associated DNF and then compare those
to see if they are equal. In the current setting, these DNF's
may indeed end up as identical expressions, but it is possible,
also, for them to turn out slightly off-kilter from each other,
and so the ultimate comparison may not be absolutely immediate.
The explanation of this is that, for the sake of computational
efficiency, it is useful to tailor the DNF that gets developed
as the output of a DNF algorithm to the particular form of the
propositional expression that is given as input. So, let's go!
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
|
| q r
| q o o r o
| | | |
| p o o p p o
| \ / |
| @ = @
|
| (p (q)) (p (r)) = (p (q r))
|
| [p=>q] & [p=>r] = [p=>[q&r]]
|
¤~~~~~~~~~¤~~~~~~~~~¤~~~FEQ~~~¤~~~~~~~~~¤~~~~~~~~~¤
|
| q o o r
| | |
| p o o p
| \ /
| @
|
=================================================== CAST [p]
|
| q r
| q o o r o o o o
| | | \| |/
| o o o o
| \ / \ /
| p o-----------o---o p
| \ /
| \ /
| \ /
| \ /
| \ /
| @
|
=================================================== Domination
|
| q o o r o o
| | | \ /
| o o o o
| \ / \ /
| p o-----------o---o p
| \ /
| \ /
| \ /
| \ /
| \ /
| @
|
=================================================== Cancellation
|
| q o o r
| | |
| o o
| \ /
| p o-----------o---o p
| \ /
| \ /
| \ /
| \ /
| \ /
| @
|
=================================================== CAST [q]
|
| o
| |
| o o r o o r
| | | | |
| o o o o
| \ / \ /
| q o-----------o---o q
| \ /
| \ /
| \ /
| \ /
| \ /
| p o-------o---o p
| \ /
| \ /
| \ /
| @
|
=================================================== Cancellation
|
| o r o r
| | |
| o o o
| / \ /
| q o-----------o---o q
| \ /
| \ /
| \ /
| \ /
| \ /
| p o-------o---o p
| \ /
| \ /
| \ /
| @
|
=================================================== Domination
|
| o r
| |
| o o
| / \
| q o-----------o---o q
| \ /
| \ /
| \ /
| \ /
| \ /
| p o-------o---o p
| \ /
| \ /
| \ /
| @
|
=================================================== CAST [r]
|
| o
| |
| o o
| | |
| o o
| / /
| r o-----------o---o r
| \ /
| \ /
| \ /
| \ / o
| \ / |
| q o-------o---o q
| \ /
| \ /
| \ /
| p o-------o---o p
| \ /
| \ /
| \ /
| @
|
=================================================== Cancellation
|
| o
| |
| r o-------o---o r
| \ /
| \ / o
| \ / |
| q o-------o---o q
| \ /
| \ /
| \ /
| p o-------o---o p
| \ /
| \ /
| \ /
| @
|
¤~~~~~~~~~¤~~~~~~~~~¤~~~QEF~~~¤~~~~~~~~~¤~~~~~~~~~¤
What we have arrived at is the arboreal 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",
and taking the abbreviation "iwc" for "in which case",
we can read this brand of DNF in the following manner:
| either [not p] iwc [true]
| orelse [p] iwc
| either [not q] iwc [false]
| orelse [q] iwc
| either [not r] iwc [false]
| orelse [r] iwc [true]
I think that I will leave the other half of the equation
as an "exercise for the reader" (EFTR), since it is much
easier to do this sort of stuff with a few scribbles on
paper than it is for me to lay it out in ASCII-glyphics.
At any rate, I do not think that the reader will be too
shocked to learn that it all works out, and that if one
cases the variables in the usual "leftmost shallowest"
order that one will even get an identical DNF for each.
To be continued ...
Jon Awbrey
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤