Re: Peirce's Rules Of Inference

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

Responding to messages by John Sowa and Frithjof Dau:

I started writing theorem-provers for Alpha Graphs during
the last half of the 1970s, and the first prover that I was
moderately happy with proved it first theorem sometime in 1985.
In the meantime I had taken a few courses on general resolution
theorem provers, but none of that was very helpful with Peirce's
way of doing things.  Along the way I was forced by a convergent
host of conceptual elegance and computational efficiency factors
to generalize from tree-like data structures to cactus-like forms.
These days, of course, speed of computation makes up for all sorts
of inelegance in concept, but still, the latter factors have a big
impact on the humane understanding of what's going on in the proofs.

One of these issues had to with a conceptual inefficiency in the
representation of logical equality (logical equivalence, iff, <=>).

If you look at the topological dual form of Peirce's graph for x <=> y,
you get this:

y o   o x
  |   |
x o   o y
   \ /
    @

In other words, (x => y) & (y => x).

The fact that each variable is mentioned twice turned out
to be an efficiency boondoggle under the constraints that
I was working, and it remains a conceptual ineffficiency
under any conditions.

The way that I eventually solved this was by introducing
the following cactus form:

x   y
o---o
 \ /
  @

Under the analogous existential interpretation,
this has the meaning x =/= y, that is, x XOR y.

From that we get x = y (or x <=> y if you prefer)
by negating it, yielding the following cactus form:

x   y
o---o
 \ /
  o
  |
  @

Thus, a change in the language results in easier proofs.

Jon Awbrey

CC: Inquiry <[email protected]>

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
¢iare: http://www.centiare.com/Directory:Jon_Awbrey
getwiki: http://www.getwiki.net/-User_talk:Jon_Awbrey
zhongwen wp: http://zh.wikipedia.org/wiki/User:Jon_Awbrey
http://www.altheim.com/ceryle/wiki/Wiki.jsp?page=JonAwbrey
wp review: http://wikipediareview.com/index.php?showuser=398
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o