Laws of Form in Metamath
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 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.
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.131 10Jun2016 Type HELP for help, EXIT to exit. MM> read lof.mm Reading source file "lof.mm"... 592 lines (22102 characters) were read from "lof.mm". The source has 114 statements; 13 are $a and 43 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
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.
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. 
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, 
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: 
axsub 
Juxtaposing the same form with equal forms leaves equal forms: 
axcmm 
p q = q p 
Associativity is found to hold despite our system lacking the means to even state it.
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 → q=p 
trans 
p=q & q=r → 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 & p=r → q=r 
subr 
p=q → u p = u q 
subst 
p=q → u p v = u q v 
substr 
p=q → u p v = v q u 
subb1 
p=q → w ( u p v ) x = w ( u q v ) x 
subb3 
p=q → w ( u p v ) x = w ( v q u ) x 
rep 
p=q & u p v = y → u q v = y 
repbx 
p=q & w (u p v) x = y → w (u q v) x = y 
quad 
p=q & r=s → p r = q s 
ins 
p q = r s → 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 & r=s → 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 & r=q → x ( v p u ) w = w ( u r v ) x

p=q & p=r → x ( v q u ) w = w ( u r v ) x
we could have reduced significantly the proof of theorem c9.0.
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 (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.
Summary of Results
System_{0}
This version follows LoF and was the original proof of concept, 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:
j1.0 
( ( p ) p ) 
= 

j2.0 
( ( p r ) ( q r ) ) 
= 
( ( p ) ( q ) ) r 
and the first two theorems:
c1.0 
( ( p ) ) 
= 
p 
c2.0 
( p q ) q 
= 
( p ) q 
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.
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 
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 ) 
= 
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 
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 ) 
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 ) 
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.
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 ) ) 
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}.
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.
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 
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 ) 
= 
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 ) ) ) 
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 
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 ) 
= 
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 
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 
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) 
Topics in Laws of Form
Associativity of logical connectives
Since LoF lacks the concept of associativity, proving that a model of LoF has associative connectives may involve metareasoning. For example, the proof of (p ∨ q) ∨ r = p ∨ (q ∨ r) corresponds to the equation p q r = p q r , which is easy to prove in LoF! Under the dual interpretation this also proves the associativity of conjunction, but here I will prove that 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. I call this metareasoning because we’re using an undefined, intuitive notion of symmetry. 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) , i.e.,
((((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 ) ) 