From NAND Rod to 0 Axiom

From NAND Rod to 0 Axiom
Armahedi Mahzar (c) 2016

This morning I have a little enlightenment alias makio of the Zen meditator. It turned out that a rod can symbolize the fundamental NAND operation of logic. The proposition a NAND b is equivalent to NOT (a AND b). It is said to be fundamental since all other logic operations can be defined by just using it.

To condense the writing, NAND is written as a rod so a NAND b is written as a|b following Sheffer. Bertrand Russell once admired Sheffer because he could reduce his five axioms base of the propositional calculus using three operations to a three axioms base using a single operation: NAND.
-
Nicod actually simplified the axiom base to the extreme. It is enough to have one axiom with one operation. Unfortunately, Nicod axiom is a very long string of characters (11 NAND and 5 variables).

(A|(B|C))|((D|(D|D))|((E|B)|((A|E)|(A|E)))

So many people were trying to abbreviate it. Finally, Stephen Wolfram could replace it with a NAND formulated logical identity which is quite short with 6 NANDs and 3 variables:

((x|z)|y)|((x|(x|y))|x) = y.

To get such a short single axiom, Wolfram needs a computer to do the search. But can we simplify the Wofram axiom? This is the question that haunted my mind for a long time. Can we?

Pictorial Notation of Logic

The operation of the computer seems to be complicated. But human is better than the computer because it can only read a string of characters. Man has two eyes that can read images. Therefore, we need a pictorial symbolization of logic.

By describing a|b as a and b in a box as [ab], then we can simplify the axiom Wolfram to the axiom Kauffman with 5 NANDs and 2 variables which basically can be read as the formulation of symbolic Reductio ad Absurdum that is

[[a]b] [[a][b]] = a

Linear literal Thinking

Actually the Kauffman axiom is nothing but the Huntington axiom in the 30s of the last century. However, Huntington declared it as part of an axiom trio together with the axioms of commutation and association. In the pictorial symbolism the last two axioms are not necessary anymore, because it's too obvious.

Huntington had a student named Robbins who proposed to replace the Huntington formula with a shorter formula containing only 4 NANDs and 2 variables

[[ab][a[b]]]=a,

but still requires the axioms of commutation and association. Unfortunately, he could not prove that Boolean algebra could be derived from the new axiom trio.

For decades, no mathematician could manually prove the adequacy of the three Robbins axioms. Eventually, in 1997, McCune can prove it with the help of computers that run for seven days continuously.

Planar Pictorial Thinking
-
However, later on, Louis Kauffman had proven it manually as many as 14 steps.
Thanks God, I could manually prove Huntington axiom from the Robbins axiom in just three steps.
-
I reported my proof was on eGroup Lawsofform@yahoogroups.com. They protest by saying that I smuggle an unproven proposition: the contraposition. However, I just think of it as one of the rules of inference, not as an axiom.

From there I concluded that humans are far more powerful than a computer, because it could not use a rule that has not be inputted. Because we are human, we can see that the Robbins axiom as a single axiom of Boolean algebra in pictorial symbolism that is non-linear. So, I was proud to be human who has a nonlinear intuition in addition to the lineal capability of the computers.

The Shortest Axiom: 0

However, if the axiom Robbins is the shortest single axiom Boolean algebra? It was not. Peirce in the early last century to make use of pictorial symbolism, which is called the method of existential graphs, can prove all boolean identities from a single axiom, namely 0. So Robbins axiom can be derived from TRUE or VOID.

Unfortunately, Peirce has to use 5 inference rules for proving it. Fortunately, I could reduce it to only one inference rule, as long as we replace TRUE axiom with the consistency or identity formula p -> p which, in pictorial symbolism, is [p[p]].

This is the small epiphany. I found the simplest axiom system (one axiom, one operation, one variable and one rule of inference) of Boolean algebra: the axiom is IDENTITY or POSITION. 

I thought I can reformulate the Simple Existential Graph System by replacing VOID axiom with  POSITION [a[a]]=   as the single axiom. By doing it, we need only one rule of inference: GENERATION [ab]b=[a]b. In pictorial notation with rod symbolism, 0 became VOID. It is summarized in the following picture:

.