ONT Extensions Of Logical Graphs
¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤~~~~~~~~~¤
John, Mishtu, ...
Here's my idea of what I hope will be a potentially more productive exercise for us --
seeing as how we three appear to share a delectation for "zeroth order logic" (ZOL),
and seeing as how this is such a rarely acquired taste in these days of no argument,
or very little on the plate of effective argument, anyway, I propose to serve up or
toss out these tidbits of what all I have learned about ZOL, propositional calculus,
sentential logic, or whatever it pleases you to call it, beginning as I began with
the Alpha Order of Peirce's Logical Graphs (AlpLog), in their dual interpretations
as "entitative logical graphs" (EnLog) and "existential logical graphs" (ExLog).
The proposed discussion would supply a modicum of concrete material
for illustrating several different issues of current interest to us:
1. It would introject an actual substance and a few novel turns to the discussion
of "formally abstract calculi" (FAC's), notoriouly AKA "The Ininterpretables".
2. When we weary of that impoverished POV that I am using to relate the "Story of A and B",
this work will have served to plow and to sow for us a significantly more fertile field,
one in which the syntactic domain S = I is a non-trivial formal language that comprises
a denumerable infinity of signs, here called "propositional expressions" or "sentences".
3. There is, of Peirce, another reason. Just give me time to think of one.
But first, a bit of apology and a note of potential caution. Those of you who believe --
and you know who you are -- that we Persean camp-followers are more of a religious cult
than a viable "community of inquiry" (COI) may be shocked to find that one among us has
dared to impart of number of innovations to the liturgy of the fateful, namely me, and
tuit in the form of several mild extensions of Peirce's Initial LogoGriphs, ones that
I found were critically necessary in order to preserve the very spirit of these laws.
In particular, all in good time I hope, we will take up extensions of AlphaLog that
I call the "reflective", the "differential", and the "higher order propositional"
extensions, or RefLog, DifLog, and HopLog, respectively. The last will bring us
to the verge of that integration among inference, information, and inquiry that
Peirce foresaw in the 1860's, and the same on which I have worked so earnestly,
albeit intermittently, since the 1960's.
To begin as lazily as I possibly can, without yet the effort of any new thought,
I can take advantage of this earlier note to the SUO Work Group, that addressed
a particular question that arose there in regard to Peirce's Existential Graphs:
¤~~~~~~~~~¤~~~~~~~~~¤~EADEM~MUTATA~RESURGO~¤~~~~~~~~~¤~~~~~~~~~¤
FYE (For Your Edification):
Concerning the ExGraph example from Rob Kremer's website on
Software Engineering, Reqs Engineering, Concept Mapping at:
http://sern.ucalgary.ca/courses/SENG/611/F99/ConceptMaps/ConceptMaps.html
The equivalence in question is:
[A & B => C] <=> [A => [B => C]].
This is a pretty important equivalence in computer science and math generally.
There is an analogy between two very fundamental formal systems, one known as
the "intuitionistic positive implicational calculus" (IPIC) and another known
as the "combinator calculus" (CC), which has roughly the same kind of generic
computational power as lambda calculus, but was actually discovered before it.
The abstract formal equivalence between these two systems
is officially called the "Curry-Howard Isomorphism" (CHI),
but more often, the "Propositions As Types" (PAT) analogy.
For example, PAT gives a correspondence
between the propositional equivalence
[A & B => C] <=> [A => [B => C]]
and the functional-type isomorphism
[A x B -> C] <-> [A -> [B -> C]].
In the latter statement, the letters "A", "B", "C"
signify category "objects", domains, sets, spaces,
or whatever you prefer to call them, "x" signifies
the "cartesian product" of these kinds of domains,
and the expression of the form "[X -> Y]" denotes
the "function space" [X -> Y] that contains "all",
suitably restricted, functions from X to Y. Also,
the sign "<->" is written to read "isomorphic to".
¤~~~~~~~~~¤~~~~~~~~~¤~CITATION~¤~~~~~~~~~¤~~~~~~~~~¤
"A proof in standard first order logic":
| (A ^ B) -> C
|------------------
| | A
| |---------------
| | | B
| | |------------
| | | A ^ B
| | | C
| | B -> C
| A -> (B -> C)
"The same proof in Peirce's Existential Graphs":
( A B ( C )) [<=>] ( A ( ( B ( C )) ))
¤~~~~~~~~~¤~~~~~~~~~¤~NOITATIC~¤~~~~~~~~~¤~~~~~~~~~¤
In RefLog syntax for Peirce's Alpha, this looks like so:
| B C
| o---o
| AB C A |
| o---o o---o
| | |
| @ = @
|
| ( A B ( C )) = ( A ( ( B ( C )) ))
It would be fudging a bit, however, to call this equivalence "one-step".
That is, the "one-step-ness" of the above proof is qualified by the fact
that one first has to prove the prior theorem of "Double Negation" (DN).
Strictly speaking, DN is a theorem, and one that requires quite a bit of
ingenuity to prove, because it says something more than the simple axiom:
| o
| |
| o
| |
| @ = @
|
| (( )) = <blank>
The "Double Negation Theorem" (DNT) is the logical equivalence:
| A
| o
| |
| o
| | A
| @ = @
|
| ((A)) = A
There is nothing in the axioms or principles that says you
can do the same stuff to a filled frame of the form "(())"
as you can with the version that has no label at depth two.
¤~~~~~~~~~¤~~~~~~~~~¤~OGRUSER~ATATUM~MEDAE~¤~~~~~~~~~¤~~~~~~~~~¤
I will now give a proof of the "Double Negation Theorem" (DNT).
This is the proof that was given by George Spencer-Brown in his
book 'Laws of Form', and therein credited to two of his students,
John Dawes and D.A. Utting.
Just to be clear about the basis of this proof, I will record here
the exact forms of the axioms that I will be using, devolving from
Peirce's "Logical Graphs" via Spencer-Brown's "Laws of Form" (LOF).
I will use the annotation scheme from LOF to mark the steps of the
proof according to which axiom (or "initial") is being invoked to
justify the corresponding step of the graphical transformation.
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 following axioms are equations.
Thus, the inference steps that they permit are always
reversible. In the proof annotation scheme below,
I will use a double bar "===" to mark this fact,
and I leave it to the reader to decide in which
direction the indicated axiom is being applied.
-------------------------
Axiom I1
-------------------------
o o o
\ / |
@ = @
( ) ( ) = ( )
-------------------------
Axiom I2
-------------------------
o
|
o
|
@ = @
(( )) =
-------------------------
Axiom J1
-------------------------
xo o
| |
x@ = @
x(x) = ( )
-------------------------
Axiom J2
-------------------------
y z xy xz
o o o o
\ / \ /
o o
| |
x@ = @
x((y)(z)) = ((xy)(xz))
-------------------------
Here is the proof of the Double Negation Theorem,
marked as "Reflection" or "Consequence 1" in LOF:
¤~~~~~~~~~¤~~~~~~~~~¤~~~DEQ~~~¤~~~~~~~~~¤~~~~~~~~~¤
xo
\
o
\
@
===================== I2 [Unfold "(())"]
xo o
\ /
o o
\ /
@
===================== J1 [Insert "(x)"]
xo
\
xo xo o
\ \ /
o o
\ /
@
===================== J2 [Distribute "((x))"]
xo xo
\ /
o xo o
\ \ /
xo o
\ /
o
/
@
===================== J1 [Delete "(x)"]
xo
\
o o
\ /
xo o
\ /
o
/
@
===================== J1 [Insert "x"]
xo
\
o xo
\ /
xo xo
\ /
o
/
@
===================== J2 [Collect "x"]
xo
\
o xo
\ /
o o
\ /
o
/
x@
===================== J1 [Delete "((x))"]
o
\
o
/
x@
===================== I2 [Refold "(())"]
x
@
¤~~~~~~~~~¤~~~~~~~~~¤~~~QED~~~¤~~~~~~~~~¤~~~~~~~~~¤