[Inquiry] Peirce's Rules Of Inference

[Jon Awbrey]

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.