[Inquiry] Propositional Equation Reasoning Systems

[Jon Awbrey]

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

PERS.  Note 1

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

| Ergo in numero quo numeramus repetitio unitatum facit pluralitatem;
| in rerum vero numero non facit pluralitatem unitatum repetitio,
| vel si de eodem dicam "gladius unus mucro unus ensis unus".
|
| Therefore in the case of that number by which we number,
| the repetition of ones makes a plurality;
|
| but in the number consisting in things
| the repetition of ones does not make a plurality,
|
| as, for example, if I say of one and the same
| thing, "one sword, one brand, one blade".
|
| Boethius (Anicius Manlius Severinus Boetius, c.480-524 A.D.),
|'De Trinitate' ('The Trinity Is One God Not Three Gods'), in:
|'The Theological Tractates', Trans. H.F. Stewart & E.K. Rand,
| New Edition, Loeb Classical Library, Harvard/Heinemann, 1973.

Here is a reference version of the CSP-GSB axioms and
first few theorems for the abstract calculus formally
knowable in a couple of senses as propositional logic.

For ease of future reference, I list here the exact forms of the axioms that I use,
devolving from Peirce's "Logical Graphs" via Spencer-Brown's "Laws of Form" (LOF).
In formal proofs, I will use the annotation scheme from LOF to mark each step of
the proof according to which axiom (or "initial") is being invoked to justify
the corresponding step of syntactic transformation, on graphs or on strings.

The axioms are just four in number,
divided into two types, as follows:
the "Arithmetic Initials" I1 and I2,
the "Algebraic  Initials" J1 and J2.

I use a trivially different J1 here.

Notice that all of the axioms in this set have the form of equations.
This means that all of the inference steps they allow are reversible.
In the proof annotation scheme below, I will use a double bar "====="
to mark this fact, but I may at times leave it to the reader to pick
which direction is the one required for applying the indicated axiom.

As you are undoubtedly aware, Peirce introduced these formal equations
at a level of abstraction that is one step higher than their customary
interpretations as propositional calculi, which two readings for logic
he called the "Entitative" and the "Existential" interpretations, and
so I will refer to the interpreted systems of graphs as "EnG" & "ExG",
respectively.  The early CSP, as in his essay on "Qualitative Logic",
and also GSB, emphasized the EnG interpretation, while the later CSP
developed mostly the ExG interpretation.  When it comes down to this
very primitive level of formal structure, I find it important to note
and I even tend to stress the formal significance of the circumstance
that this formal system is a "very abstract calculus" (VAC), devoid of
meaning in the usual logical sense.  I cannot speak for how this works
out or what it might mean beyond this point, on the next levels of form.

o-----------------------------------------------------------o
|                                                           |
|                 o   o                 o                   |
|                  \ /                  |                   |
|                   @         =         @                   |
|                                                           |
o-----------------------------------------------------------o
|                                                           |
|                ( ) ( )      =        ( )                  |
|                                                           |
o-----------------------------------------------------------o
| Axiom I1.    Distract <---- | ----> Condense              |
o-----------------------------------------------------------o

o-----------------------------------------------------------o
|                                                           |
|                   o                                       |
|                   |                                       |
|                   o                                       |
|                   |                                       |
|                   @         =         @                   |
|                                                           |
o-----------------------------------------------------------o
|                                                           |
|                 (( ))       =                             |
|                                                           |
o-----------------------------------------------------------o
| Axiom I2.      Unfold <---- | ----> Refold                |
o-----------------------------------------------------------o

o-----------------------------------------------------------o
|                                                           |
|                 a o                   o                   |
|                   |                   |                   |
|                 a @         =         @                   |
|                                                           |
o-----------------------------------------------------------o
|                                                           |
|                 a(a)        =        ( )                  |
|                                                           |
o-----------------------------------------------------------o
| Axiom J1.      Insert <---- | ----> Delete                |
o-----------------------------------------------------------o

o-----------------------------------------------------------o
|                                                           |
|                ab   ac              b   c                 |
|                 o   o               o   o                 |
|                  \ /                 \ /                  |
|                   o                   o                   |
|                   |                   |                   |
|                   @         =       a @                   |
|                                                           |
o-----------------------------------------------------------o
|                                                           |
|              ((ab)(ac))     =     a((b)(c))               |
|                                                           |
o-----------------------------------------------------------o
| Axiom J2.  Distribute <---- | ----> Collect               |
o-----------------------------------------------------------o

Jon Awbrey

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