Laws of Form in Metamath
Metamath derivations of the Primary Algebra from G. SpencerBrown’s Laws of Form.
———————————————————————————–
1. Introduction
lof.mm presents metamath derivations of the Primary Algebra from SpencerBrown, G. (1969) Laws of Form (Allen & Unwin, London), hereafter cited as LoF.
The algebra of LoF has a number of models, most significantly Boolean algebra^{1} and sentential logic, so it may be of some interest to logicians. From the perspective of metamath, it is a nontrivial example of a system that requires, indeed is based on, the empty substitution.
Access to the empty substitution, in conjunction with metamath’s radical formalism, allows a representation that closely matches LoF’s actual expressions.
LoF is a 2dimensional notation in which closed curves (boundaries) are the symbols under investigation, and in which the only property of interest is whether a given boundary is inside or outside of another boundary, intersecting boundaries not being allowed. Variables p q r … will range over possible arrangements of boundaries (which we call forms). It is now common to call LoF a boundary algebra. In LoF all boundaries are considered equivalent.
The topology of LoF implicitly imposes commutativity on its operations and transferring this to a linear notation involves compromises. To better understand the compromises and see the formal cost of linearity was a major motivation of this exercise.
As has become standard, I use matching parentheses (…) to represent boundaries. And I need to explicitly state the commutative property. The ramifications of this last point are felt throughout the ensuing derivations, as properties that are obvious in the 2D notation have to be spelled out case by case in auxiliary theorems. The system as formulated is simply unable to prove general statements of commutativity.
———————————————————————————–
2. Synopsis
Since my derivation of the Primary Algebra (PA) follows SpencerBrown rather closely, I spend little time on it here. I do provide a full demonstration that an alternate basis of C5 and C6 is equivalent to PA. I then show that C6 alone is adequate. Finally, I show that C6 is derivable from the Robbins axiom, implying that a Robbins algebra is a Boolean algebra.^{2}
If metamath is installed on your system, you can confirm the correctness of the formal derivations in lof.mm by starting the program, reading in the file, and verifying the steps:
$ metamath
Metamath  Version 0.196 31Dec2020 Type HELP for help, EXIT to exit.
MM> read lof.mm
Reading source file "lof.mm"... 26646 bytes
26646 bytes were read into the source buffer.
The source has 123 statements; 13 are $a and 52 are $p.
SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database.
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
if you want to check them.
MM> verify proof *
0 10% 20% 30% 40% 50% 60% 70% 80% 90% 100%
..................................................
All proofs in the database were verified in 0.01 s.
To see the actual steps in the proof of a particular proposition, for example c3.0, execute:
MM> show proof c3.0 /lemmon /renumber /no_repeated_steps
———————————————————————————–
3. Axioms
In keeping with the spirit of LoF’s austerity, I aimed for the most minimal formalism possible. I start with five constant symbols:
( ) =  form
and seven basic axioms – three to provide a recursive definition of ‘form’, three common notions (so to speak) to power symbol manipulation, and a commutativity axiom. Metamath does not distinguish definitions from proper axioms.
Recursive definition of form

void Empty space is a form.

encl If p is a form, enclosing it in parentheses ( p ) is a form.

juxt If p and q are forms, juxtaposing them as p q is a form.
Common notions

axeuc Two things equal to the same thing are equal to each other. This is Euclid’s first Common Notion and, in an equational logic, this and its sibling, transitivity, are the main engine of derivation. Formally, p = q and r = q implies p = r.
Euclid’s second and third Common Notions are specific to quantity, so not exactly common. We can rephrase them as: doing the same thing (e.g., applying the same operation) to equal things leaves equal things. Applying this to LoF’s two operations, enclosure and juxtaposition, leads to the next two axioms (looked at differently, these can also be seen as substitution/replacement rules).

axbeq Enclosing equal forms leaves equal forms. We can consider this a definition of boundary equality: p = q implies ( p ) = ( q ).

axsub Juxtaposing the same form with equal forms leaves equal forms: p = q implies p v = q v.
Commutativity of LoF
 axcmm p q = q p
———————————————————————————–
4. Theorems
The symbol ‘=’ is never defined but it will turn out to obey the expected laws of an equivalence relation. Specifically, from the common notion that two things equal to the same thing are equal to each other and from the commutativity of LoF, we derive the reflexivity, symmetry, and transitivity of ‘=’. Note that such a derivation is not possible in a traditional formal system without additional axioms – it is the ability to reference the empty (or void) form that allows it here. For the actual derivations, see the source file.
id  p = p  
sym  p = q implies q = p  
trans  p = q and q = r implies p = r 
The axioms and theorems so far have been transparent, succinct, and
powerful (they embody Boolean algebra, after all), but applying them
would be impractical without further theorems. While this is no different
from any other formal system, here these auxiliary theorems have a
peculiar feeling of inconsequence: they are often tiresome (and sometimes
ugly) commutative elaborations of previous statements, whose only adhoc
utility is to ease the derivation of particular propositions.
I state these below without further comment.
eucr  p = q and p = r implies q = r  
subr  p = q implies u p = u q  
subst  p = q implies u p v = u q v  
substr  p = q implies u p v = v q u  
subb1  p = q implies w ( u p v ) x = w ( u q v ) x  
subb3  p = q implies w ( u p v ) x = w ( v q u ) x  
rep  p = q and u p v = y implies u q v = y  
repbx  p = q and w ( u p v ) x = y implies w ( u q v ) x = y  
quad  p = q and r = s implies p r = q s  
ins  p q = r s implies p v q = r v s  
cmmx  u p v q w = u q v p w  
cmmbx  x ( u p v q w ) y = x ( u q v p w ) y  
quadbx  p = q and r = s implies x ( u p v r w ) y = x ( u q v s w ) y 
It’s hard to know where to stop with auxiliary theorems. Had we chosen
to prove the two additional statements:
p = q and r = q implies x ( v p u ) w = w ( u r v ) x
p = q and p = r implies x ( v q u ) w = w ( u r v ) x
we could have reduced significantly the proof of theorem c9.0.
———————————————————————————–
5. Laws of Form
LoF can be considered a prolonged deduction from two initial ‘arithmetic’ equations [LoF, p. 12]:
I1. Number  ( ) ( )  =  ( )  
I2. Order  ( ( ) )  = 
As mentioned, one of the models of LoF is sentential logic:
T  ≡  ( )  
F  ≡  
¬ p  ≡  ( p )  
p ∨ q  ≡  p q  
p ∧ q  ≡  ( ( p ) ( q ) )  
p > q  ≡  ( p ) q  
p ↔ q  ≡  ( ( p ) ( q ) ) ( p q ) 
The algebra is selfdual. If we interchange T and F, the algebraic laws
continue to hold, with juxtaposition now interpreted as conjunction:
T  ≡  
F  ≡  ( )  
¬ p  ≡  ( p )  
p ∨ q  ≡  ( ( p ) ( q ) )  
p ∧ q  ≡  p q  
p > q  ≡  ( p ( q ) )  
p ↔ q  ≡  ( ( ( p ) ( q ) ) ( p q ) ) 
In keeping with standard practice, I use the first interpretation
(juxtaposition as disjunction). When refering to the second interpretation,
I call it the ‘dual interpretation’.
SpencerBrown begins with the two axioms:
J1. Position  ( ( p ) p ) =  
J2. Transposition  ( ( p r ) ( q r ) ) = ( ( p ) ( q ) ) r 
and deduces the following consequences [LoF, pp. 2835]:
C1. Reflexion  ( ( a ) ) = a  
C2. Generation  ( a b ) b = ( a ) b  
C3. Integration  ( ) a = ( )  
C4. Occultation  ( ( a ) b ) a = a  
C5. Iteration  a a = a  
C6. Extension  ( ( a ) ( b ) ) ( ( a ) b ) = a  
C7. Echelon  ( ( ( a ) b ) c ) = ( a c ) ( ( b ) c )  
C8. Modified transposition  ( ( a ) ( b r ) ( c r ) ) = ( ( a ) ( b ) ( c ) ) ( ( a ) ( r ) )  
C9. Crosstransposition  ( ( ( b ) ( r ) ) ( ( a ) ( r ) ) ( ( x ) r ) ( ( y ) r ) ) =  
( ( r ) a b ) ( r x y ) 
To see that J1 and J2 constitute a complete set of axioms, refer to
chapter 9 of LoF [pp. 5052].
One of the goals of lof.mm was to establish different bases (initial axioms) for the algebra. To do this in one file, I need a way to reference the same theorems in the different bases. Retaining SpencerBrown’s original numbering scheme for crossreferencing, I label the theorems as ck.n (or jk.n), where ck (jk) refers to LoF’s Ck (Jk) and n refers to the basis under consideration. In other words, ck.n = ck.m (jk.n = jk.m) for all n, m. LoF’s system is n = 0.
———————————————————————————–
6. Summary of results
System_{0}
This version essentially follows LoF, so not much more needs to be said. There is one difference – theorem C5 is derived before C4 – and so for those interested, I show the derivation below, as expressed by metamath.
First the axioms, i.e., Basis_{0}:
j1.0  ( ( p ) p ) =  
j2.0  ( ( p r ) ( q r ) ) = ( ( p ) ( q ) ) r 
Proof of c5.0
1  ( ( p ) p ) p = ( ( p ) ) p  (c2.0) 
2  ( ( p ) ) = p  (c1.0) 
3  ( ( p ) ) p = p p  (2,subst) 
4  ( ( p ) p ) p = p p  (1,3,trans) 
5  ( ( p ) p ) =  (j1.0) 
6  ( ( p ) p ) p = p  (5,subst) 
7  p p = p  (4,6,eucr) 
System_{1}
Although System_{0} is the only one demonstrated by SpencerBrown, and so can be considered canonical, he mentions in his notes an alternate basis of C5 and C6, but suggests the derivation is ‘both difficult and tedious’ [LoF, p.89]. Readers can decide for themselves whether System_{1} is any more complicated than System_{0}. The virtue of this basis, as noted by SpencerBrown, is the need for only two distinct variables.
The derivation below ends at the point where both j1.1 and j2.1 are proved, since that establishes c5.1 and c6.1 as a complete basis.
Basis_{1}
c5.1  p p = p  
c6.1  ( ( p ) ( q ) ) ( ( p ) q ) = p 
The following lemma is crucial for the proof of c1.1 Under the dual
interpretation, it is mildly reminiscent of modus ponens:
(p ∧ (p > q)) ↔ (p ∧ q)
lem1.1  p ( ( q ) p ) = p q 
Proof of lem1.1
1  ( ( q ) ( p ) ) = ( ( p ) ( q ) )  (cmmbx) 
2  ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) ( p ) ) ( ( q ) p )  
= ( ( p ) ( q ) ) ( ( p ) q ) ( ( p ) ( q ) ) ( ( q ) p )  (1 subst)  
3  ( ( p ) ( q ) ) ( ( p ) q ) ( ( p ) ( q ) ) ( ( q ) p )  
= ( ( p ) ( q ) ) ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) p )  (cmmx)  
4  ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) ( p ) ) ( ( q ) p )  
= ( ( p ) ( q ) ) ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) p )  (2,3 trans)  
5  ( ( p ) ( q ) ) ( ( p ) ( q ) ) = ( ( p ) ( q ) )  (c5.1) 
6  ( ( p ) ( q ) ) ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) p )  
= ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) p )  (5 axsub)  
7  ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) ( p ) ) ( ( q ) p )  
= ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) p )  (4,6 trans)  
8  ( ( p ) ( q ) ) ( ( p ) q ) = p  (c6.1) 
9  ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) p ) = p ( ( q ) p )  (8 axsub) 
10  ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) ( p ) ) ( ( q ) p )  
= p ( ( q ) p )  (7,9 trans)  
11  ( ( q ) ( p ) ) ( ( q ) p ) = q  (c6.1) 
12  ( ( p ) ( q ) ) ( ( p ) q ) ( ( q ) ( p ) ) ( ( q ) p )  
= p q  (8,11 quad)  
13  p ( ( q ) p ) = p q  (10,12 eucr) 
If we now plug void values into lem1.1’s p variable, we
immediately prove:
c1.1  ( ( p ) ) = p 
And plugging void values into c1.1’s p variable immediately
proves the I2 arithmetic initial:
i2.1  ( ( ) ) = 
I2 is also directly derivable from the basis by plugging void values
into c6.1, followed by two applications of c5.1. We now prove one of
the two equations from Basis_{0}, J1.
j1.1  ( ( p ) p ) = 
Proof of j1.1
1  ( ( p ) ) = p  (c1.1) 
2  ( p ) ( ( p ) ) = ( p ) p  (1 subr) 
3  ( ( p ) ) ( p ) = ( p ) ( ( p ) )  (axcmm) 
4  ( ( ) ) =  (i2.1) 
5  ( ( ( ) ) ( p ) ) = ( ( p ) )  (4 subb1) 
6  ( ( ( ) ) p ) = ( p )  (4 subb1) 
7  ( ( ( ) ) ( p ) ) ( ( ( ) ) p ) = ( ( p ) ) ( p )  (5,6 quad) 
8  ( ( ( ) ) ( p ) ) ( ( ( ) ) p ) = ( )  (c6.1) 
9  ( ( p ) ) ( p ) = ( )  (7,8 eucr) 
10  ( p ) ( ( p ) ) = ( )  (3,9 eucr) 
11  ( p ) p = ( )  (2,10 eucr) 
12  ( ( p ) p ) = ( ( ) )  (11 axbeq) 
13  ( ( p ) p ) =  (12,4 trans) 
We now prove C4.
c4.1  ( ( p ) q ) p = p 
Proof of c4.1
1  ( ( p ) ( q ) ) ( ( p ) q ) = p  (c6.1) 
2  ( ( p ) ( q ) ) ( ( p ) q ) ( ( p ) q ) = ( ( p ) q ) p  (1 substr) 
3  ( ( p ) q ) ( ( p ) q ) = ( ( p ) q )  (c5.1) 
4  ( ( p ) ( q ) ) ( ( p ) q ) ( ( p ) q )  
= ( ( p ) ( q ) ) ( ( p ) q )  (3 subr)  
5  ( ( p ) q ) p = ( ( p ) ( q ) ) ( ( p ) q )  (2,4 eucr) 
6  ( ( p ) q ) p = p  (5,1 trans) 
We will need this corollary of c4.1:
c4cor.1  ( p q ) ( p ) = ( p ) 
Proof of c4cor.1
1  ( ( p ) ) = p  (c1.1) 
2  ( ( ( p ) ) q ) ( p ) = ( p q ) ( p )  (1 subb1) 
3  ( ( ( p ) ) q ) ( p ) = ( p )  (c4.1) 
4  ( p q ) ( p ) = ( p )  (2,3 eucr) 
And this corollary of c6.1:
c6cor.1  ( ( p ) q ) ( p q ) = ( q ) 
Proof of c6cor.1
1  q p = p q  (axcmm) 
2  q ( p ) = ( p ) q  (axcmm) 
3  ( ( q ) ) = q  (c1.1) 
4  ( ( ( q ) ) ( p ) ) ( ( ( q ) ) p ) = ( q )  (c6.1) 
5  ( q ( p ) ) ( ( ( q ) ) p ) = ( q )  (3,4 repbx) 
6  ( q ( p ) ) ( q p ) = ( q )  (3,5 repbx) 
7  ( ( p ) q ) ( q p ) = ( q )  (2,6 repbx) 
8  ( ( p ) q ) ( p q ) = ( q )  (1,7 repbx) 
We prove C7.
c7.1  ( ( ( p ) q ) r ) = ( p r ) ( ( q ) r ) 
Beyond a certain length, proofs become dominated by commutations and
substitutions of equal forms, making them practically unreadable. The full
41step version of c7.1 is an example (have metamath execute show proof c7.1
/lemmon /renumber /no_repeated_steps
to see all the steps). Below is a much
condensed version where rearrangement of terms and substitution of equals go
unmentioned.
Condensed proof of c7.1
1  ( ( ( ( ( p ) q ) r ) ) ( p q ) ) ( ( ( ( ( p ) q ) r ) ) p q )  
= ( ( ( p ) q ) r )  (c6.1)  
2  ( ( ( p ) q ) r ( p q ) ) ( ( ( p ) q ) p r q )  
= ( ( ( p ) q ) r )  (c1.1 twice)  
3  ( ( q ) r ) ( ( ( p ) q ) p r q ) = ( ( ( p ) q ) r )  (c6cor.1) 
4  ( ( q ) r ) ( p r q ) = ( ( ( p ) q ) r )  (c4.1) 
5  ( ( ( ( ( p ) q ) r ) ) ( ( p ) ( q ) ) ) ( ( ( ( ( p ) q ) r ) ) ( p ) ( q ) )  
= ( ( ( p ) q ) r )  (c6.1)  
6  ( ( ( p ) q ) r ( ( p ) ( q ) ) ) ( ( ( p ) q ) r ( p ) ( q ) )  
= ( ( ( p ) q ) r )  (c1.1 twice)  
7  ( p r ) ( ( ( p ) q ) r ( p ) ( q ) ) = ( ( ( p ) q ) r )  (c6.1) 
8  ( p r ) ( ( p ) ( q ) r ) = ( ( ( p ) q ) r )  (c4cor.1) 
9  ( p r ) ( p r q ) ( ( q ) r ) ( ( p ) ( q ) r )  
= ( ( ( p ) q ) r ) ( ( ( p ) q ) r )  (4,8 quad)  
10  ( p r ) ( p r q ) ( ( q ) r ) ( ( p ) ( q ) r )  
= ( ( ( p ) q ) r )  (c5.1)  
11  ( ( ( p ) q ) r ) = ( p r ) ( ( q ) r )  (c4.1 twice) 
We can now prove the second of the two equations from Basis_{0}, J2.
This completes the proof that Basis_{1} is at least as powerful as
Basis_{0}.
j2.1  ( ( p ) ( q ) ) r = ( ( p r ) ( q r ) ) 
Proof of j2.1
1  ( ( ( ( p ) ( q ) ) r ) ) = ( ( p ) ( q ) ) r  (c1.1) 
2  ( ( ( p ) ( q ) ) r ) = ( p r ) ( ( ( q ) ) r )  (c7.1) 
3  ( ( q ) ) = q  (c1.1) 
4  ( p r ) ( ( ( q ) ) r ) = ( p r ) ( q r )  (3 subb1) 
5  ( ( ( p ) ( q ) ) r ) = ( p r ) ( q r )  (2,4 trans) 
6  ( ( ( ( p ) ( q ) ) r ) ) = ( ( p r ) ( q r ) )  (5 axbeq) 
7  ( ( p ) ( q ) ) r = ( ( p r ) ( q r ) )  (1,6 eucr) 
System_{2}
Having shown that C5 and C6 form a basis, I now show that C6 alone suffices. The derivation ends at the point where c5.2 is proved, since that establishes that Basis_{2} is at least as powerful as Basis_{1}.
Basis_{2}
c6.2  ( ( p ) ( q ) ) ( ( p ) q ) = p 
An important lemma used in the proof of c1.2:
lem2.2  ( p ) p = ( q ) q 
This is a condensed proof of lem2.2.
1  ( ( ( p ) ) ( ( q ) ) ) ( ( ( p ) ) ( q ) ) = ( p )  (c6.2) 
2  ( ( p ) ( ( q ) ) ) ( ( p ) ( q ) ) = p  (c6.2) 
3  ( ( ( q ) ) ( ( p ) ) ) ( ( ( q ) ) ( p ) ) = ( q )  (c6.2) 
4  ( ( q ) ( ( p ) ) ) ( ( q ) ( p ) ) = q  (c6.2) 
5  ( ( ( p ) ) ( ( q ) ) ) ( ( ( p ) ) ( q ) )  
( ( p ) ( ( q ) ) ) ( ( p ) ( q ) ) = ( p ) p  (1,2 quad)  
6  ( ( ( p ) ) ( ( q ) ) ) ( ( ( p ) ) ( q ) )  
( ( p ) ( ( q ) ) ) ( ( q ) ( p ) ) = ( q ) q  (3,4 quad)  
7  ( p ) p = ( q ) q  (5,6 euc) 
Axiom B3 from Meguire^{3} follows immediately from
lem2.2 by plugging void values into q.
b3.2  ( p ) p = ( ) 
Now we prove c1.2.
c1.2  ( ( p ) ) = p 
Proof of c1.2
1  ( ( p ) ) ( p ) = ( p ) ( ( p ) )  (axcmm) 
2  ( ( ( p ) ) ) ( p ) = ( p ) ( ( ( p ) ) )  (axcmm) 
3  ( ( ( p ) ) ( p ) ) ( ( ( ( p ) ) ) ( p ) )  
= ( ( ( ( p ) ) ) ( p ) ) ( ( ( p ) ) ( p ) )  (axcmm)  
4  ( ( ( p ) ) ) ( ( p ) ) = ( ( p ) ) ( p )  (lem2.2) 
5  ( ( ( ( p ) ) ) ( ( p ) ) ) ( ( ( ( p ) ) ) ( p ) )  
= ( ( p ) )  (c6.2)  
6  ( ( ( p ) ) ( p ) ) ( ( ( ( p ) ) ) ( p ) ) = ( ( p ) )  (4,5 repbx) 
7  ( ( ( ( p ) ) ) ( p ) ) ( ( ( p ) ) ( p ) ) = ( ( p ) )  (3,6 rep) 
8  ( ( p ) ( ( ( p ) ) ) ) ( ( ( p ) ) ( p ) ) = ( ( p ) )  (2,7 repbx) 
9  ( ( p ) ( ( ( p ) ) ) ) ( ( p ) ( ( p ) ) ) = ( ( p ) )  (1,8 repbx) 
10  ( ( p ) ( ( ( p ) ) ) ) ( ( p ) ( ( p ) ) ) = p  (c6.2) 
11  ( ( p ) ) = p  (9,10 eucr) 
Next we prove J1.
j1.2  ( ( p ) p ) = 
Proof of j1.2
1  ( p ) p = ( )  (b3.2) 
2  ( ( p ) p ) = ( ( ) )  (1 axbeq) 
3  ( ( ) ) =  (c1.2) 
4  ( ( p ) p ) =  (2,3 trans) 
Another lemma.
lem3.2  ( p p ) = ( ( ( p ) ) ( ( p ) ) 
Proof of lem3.2
1  ( ( p ) ) = p  (c1.2) 
2  p = ( ( p ) )  (1 sym) 
3  ( p p ) = ( p p )  (id) 
4  ( ( ( p ) ) p ) = ( p p )  (2,3 repbx) 
5  ( ( ( p ) ) ( ( p ) ) ) = ( p p )  (2,4 repbx) 
6  ( p p ) = ( ( ( p ) ) ( ( p ) ) )  (5 sym) 
We can finally prove C5, which demonstrates that Basis_{2} is at least
as strong as Basis_{1}.
c5.2  p p = p 
Proof of c5.2
1  ( ( ( p ) ) ( ( p ) ) ) ( ( ( p ) ) ( p ) ) = ( p )  (c6.2) 
2  ( p p ) = ( ( ( p ) ) ( ( p ) ) )  (lem3.2) 
3  ( ( ( p ) ) ( p ) ) =  (j1.2) 
4  = ( ( ( p ) ) ( p ) )  (3 sym) 
5  ( ( p p ) ) = p p  (c1.2) 
6  ( ( p p ) ( ( ( p ) ) ( p ) ) ) = p p  (4,5 repbx) 
7  ( ( ( ( p ) ) ( ( p ) ) ) ( ( ( p ) ) ( p ) ) ) = p p  (2,6 repbx) 
8  ( ( p ) ) = p p  (1,7 repbx) 
9  ( ( p ) ) = p  (c1.2) 
10  p p = p  (8,9 eucr) 
System_{3}
Here we derive C6 from the Robbins equation, demonstrating that a Robbins algebra is a Boolean algebra. The more familiar form of the Robbins equation is ( ( p q ) ( p ( q ) ) ) = p, but for this exercise I’ll be using the equivalent form:
robbins  ( ( ( p ) q ) ( p q ) ) = q 
First we prove J1.
j1.3  ( ( p ) p ) = 
Proof of j1.3
1  ( ( ( q ) p ) ( q p ) ) = p  (robbins) 
2  p = ( ( ( q ) p ) ( q p ) )  (1 sym) 
3  ( p ) = ( ( ( ( q ) p ) ( q p ) ) )  (2 axbeq) 
4  ( p ) p  
= ( ( ( ( q ) p ) ( q p ) ) ) ( ( ( q ) p ) ( q p ) )  (3,2 quad)  
5  ( ( p ) p )  
= ( ( ( ( ( q ) p ) ( q p ) ) ) ( ( ( q ) p ) ( q p ) ) )  (4 axbeq)  
6  ( ( ( ( ( q ) p ) ( q p ) ) ) ( ( ( q ) p ) ( q p ) ) ) =  (robbins) 
7  ( ( p ) p ) =  (5,6 trans) 
Next we prove C1.
c1.3  ( ( p ) ) = p 
Proof of c1.3
1  p ( ( p ) ) = ( ( p ) ) p  (axcmm) 
2  ( p ( ( p ) ) ) = ( ( ( p ) ) p )  (1 axbeq) 
3  ( ( p ( ( p ) ) ) ) = ( ( ( ( p ) ) p ) )  (2 axbeq) 
4  ( ( ( p ) ) ( p ) ) =  (robbins) 
5  ( p ) ( ( p ) ) = ( ( p ) ) ( p )  (axcmm) 
6  ( ( p ) ( ( p ) ) ) = ( ( ( p ) ) ( p ) )  (5 axbeq) 
7  ( ( ( p ) ( ( p ) ) ) ( p ( ( p ) ) ) ) = ( ( p ) )  (robbins) 
8  ( ( ( ( p ) ) ( p ) ) ( p ( ( p ) ) ) ) = ( ( p ) )  (6,7 repbx) 
9  ( ( p ( ( p ) ) ) ) = ( ( p ) )  (4,8 repbx) 
10  ( ( ( ( p ) ) p ) ) = ( ( p ) )  (3,9 rep) 
11  ( ( p ) p ) =  (j1.3) 
12  ( ( ( ( p ) ) p ) ( ( p ) p ) ) = p  (robbins) 
13  ( ( ( ( p ) ) p ) ) = p  (11,12 repbx) 
14  ( ( p ) ) = p  (10,13 eucr) 
We now prove C6, demonstrating that the Robbins algebra is at least as
powerful as Boolean algebra. The original proof was simplified according to
suggestions by Armahedi Mahzar.
c6.3  ( ( p ) ( q ) ) ( ( p ) q ) = p 
Proof of c6.3
1  ( ( p ) ( q ) ) ( q ( p ) ) = ( ( p ) ( q ) ) ( ( p ) q )  (cmmbx) 
2  ( ( q ) ( p ) ) ( q ( p ) ) = ( ( p ) ( q ) ) ( q ( p ) )  (cmmbx) 
3  ( ( ( ( q ) ( p ) ) ( q ( p ) ) ) ) = ( ( q ) ( p ) ) ( q ( p ) )  (c1.3) 
4  ( ( ( q ) ( p ) ) ( q ( p ) ) ) = ( p )  (robbins) 
5  ( ( ( ( q ) ( p ) ) ( q ( p ) ) ) ) = ( ( p ) )  (4 axbeq) 
6  ( ( p ) ) = p  (c1.3) 
7  ( ( ( ( q ) ( p ) ) ( q ( p ) ) ) ) = p  (5,6 trans) 
8  ( ( q ) ( p ) ) ( q ( p ) ) = p  (3,7 eucr) 
9  ( ( p ) ( q ) ) ( q ( p ) ) = p  (2,8 eucr) 
10  ( ( p ) ( q ) ) ( ( p ) q ) = p  (1,9 eucr) 
———————————————————————————–
7. Topics in Laws of Form
Associativity of logical connectives
Although LoF lacks the concept of associativity, proving that a model of LoF has associative connectives is straightforward. For example, the proof of (p ∨ q) ∨ r = p ∨ (q ∨ r) corresponds to proving the LoF equation p q r = p q r , which follows immediately from theorems quad or ins. Under the dual interpretation this also proves the associativity of conjunction, but we can prove the latter more directly. Since p ∧ q corresponds to ( ( p ) ( q ) ), we need to show that ( ( ( ( p ) ( q ) ) ) ( r ) ) = ( ( p ) ( ( ( q ) ( r ) ) ) ). Consider the left side of that equation – it evaluates to a form symmetric in the three variables:
conj3  ( ( ( ( p ) ( q ) ) ) ( r ) ) = ( ( p ) ( q ) ( r ) ) 
[This and subsequent proofs will be omitted. See the source file or
utilize metamath’s proofdisplay capabilities.]
This shows that a permutation of variables in the LHS leaves the result unchanged. Specifically, ( ( ( ( q ) ( r ) ) ) ( p ) ), which is equal to ( ( p ) ( ( ( q ) ( r ) ) ) ) by commutation, will evaluate to the same form as ( ( ( ( p ) ( q ) ) ) ( r ) ) This completes the proof. See the source for a full formal proof.
conjassc  ( ( ( ( p ) ( q ) ) ) ( r ) ) = ( ( p ) ( ( ( q ) ( r ) ) ) ) 
Now I turn to proving the associativity of the biconditional,
(p ↔ q) ↔ r = p ↔ (q ↔ r).
I had earlier taken for granted that
p ↔ q, transcribed as
( ( ( p ) q ) ( ( q ) p ) ),
was equivalent to
( ( p ) ( q ) ) ( p q ).
Here I prove it (see the source).
bicond  ( ( ( p ) q ) ( ( q ) p ) ) = ( ( p ) ( q ) ) ( p q ) 
Let A = p ↔ q = ( ( p ) ( q ) ) ( p q )
and B = q ↔ r = ( ( q ) ( r ) ) ( q r ).
Proving that the biconditional associates amounts to proving:
( ( A ) ( r ) ) ( A r ) = ( ( p ) ( B ) ) ( p B ),
in other words,
( ( ( ( p ) ( q ) ) ( p q ) ) ( r ) ) ( ( ( p ) ( q ) ) ( p q ) r ) =
( ( p ) ( ( ( q ) ( r ) ) ( q r ) ) ) ( p ( ( q ) ( r ) ) ( q r ) ).
Consider the left side of that equation – as in the case of conjunction,
it evaluates to a form symmetric in the three variables:
bic3  ( ( ( ( p ) ( q ) ) ( p q ) ) ( r ) ) ( ( ( p ) ( q ) ) ( p q ) r )  
= ( ( p ) ( q ) ( r ) ) ( p q ( r ) ) ( p ( q ) r ) ( ( p ) q r ) 
This completes the informal proof that the biconditional associates. See
the source for the full proof.
bicondassc  ( ( ( ( p ) ( q ) ) ( p q ) ) ( r ) ) ( ( ( p ) ( q ) ) ( p q ) r )  
= ( ( p ) ( ( ( q ) ( r ) ) ( q r ) ) ) ( p ( ( q ) ( r ) ) ( q r ) 
[Note: this post was updated in April 2021]

“…we consider Brown’s algebraic axioms and show that they are synonymous with the axioms for Boolean algebra.” Paul Cull & William Frank, “Flaws of Form”, International Journal of General Systems, 5:4, 201–211 (1979). ↩

To be clear, this is not an alternative to the 1996 computer proof that Robbins algebras are Boolean (W. McCune, “Solution of the Robbins Problem”, JAR 19(3), 263–276 (1997)). LoF has a natural identity element, the void, and Steven Winkler showed in the early 1990s that the existence of such an element sufficed to turn a Robbins algebra into a Boolean algebra (S. Winker, “Robbins Algebra: Conditions That Make a NearBoolean Algebra Boolean”, J. Automated Reasoning 6(4), 465–489 (1990) and “Absorption and idempotency criteria for a problem in nearBoolean algebras”, J. Algebra 153(2), 414–423 (1992)). See http://homepages.math.uic.edu/~kauffman/Robbins.htm for a LoFinspired derivation by Louis Kauffman that does not take the void as given. ↩

P. Meguire, “Boundary Algebra: A Simple Notation for Boolean Algebra and the Truth Functors” (2007), http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.143.8171 . ↩