[seqfan] Animated Proofs & Cactus Logic
Jon Awbrey
jawbrey at att.net
Tue Mar 23 16:22:56 CET 2010
Hi SeqFans --
I finally got around to doing something I've
been thinking about doing since the late 60's,
animating proofs in Peirce's logical graphs.
Here's a rough cut where all I did was flip through
a sequence of images that I had already made up
in storyboard form:
http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Propositional_Equation_Reasoning_Systems#Majority_function_example
Background:
There's an extension of Peirce's logical graphs for propositional calculus
that uses "minimal negation operators" -- the family of connectives that
assert "just one false" of the propositions in their argument lists.
This generalizes the corresponding syntactical trees to cacti and
represents a minimal negation operator of k arguments by means
of a cactus lobe of k+1 nodes.
For instance, XOR(x, y) is graphed as follows, where * is the root node:
x y
o---o
\ /
*
This provides us with a nice way of representing boolean expansions
and using them as disjunctive normal forms to establish results.
For example, here's a graphical DNF way of proving Leibniz's
Praeclarum Theorema -- with a proof animation at the end:
http://mywikibiz.com/Directory:Jon_Awbrey/Papers/Propositional_Equation_Reasoning_Systems#Praeclarum_theorema_:_Proof_by_CAST
The species of cacti that arises is known as "painted and rooted cacti" --
this means that you can assign any set of labels ("paints") from
a given finite set of boolean variable names to each node.
I remember that enumerating cacti was one of my favorite problems in Harary & Palmer,
and I've always thought that there ought to be some nice counting problems here,
but I fear that exceeds my current powers, so maybe someone else can see one.
Cheers,
Jon Awbrey
--
inquiry list: http://stderr.org/pipermail/inquiry/
mwb: http://www.mywikibiz.com/Directory:Jon_Awbrey
knol: http://knol.google.com/k/-/-/3fkwvf69kridz/1
oeiswiki: http://www.oeis.org/wiki/User:Jon_Awbrey
More information about the SeqFan
mailing list