[Inquiry] Peirce's Rules Of Inference

[Jon Awbrey]

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

PROI.  Note 1

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

Responding to messages by John Sowa and Frithjof Dau on the CG List:

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 do 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 inefficiency
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.

Negating that gives us the cactus expression
for x = y (or x <=> y if you prefer), namely:

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

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

Jon Awbrey

CC: Inquiry <inquiry at stderr.org>

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