[FOM] Animated Proofs : Praeclarum Theorema

[Jon Awbrey]

More fun with proof animations ...

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 what graph
theorists call "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

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