Laws of Form in Metamath

Metamath derivations of the Primary Algebra from G. Spencer-Brown’s Laws of Form.

———————————————————————————–

1. Introduction

lof.mm presents metamath derivations of the Primary Algebra from Spencer-Brown, 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¹ and sentential logic, so it may be of some interest to logicians. From the perspective of metamath, it is a non-trivial 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 2-dimensional 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 Spencer-Brown 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.²

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 31-Dec-2020          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

1. void    Empty space is a form.

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

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

Common notions

4. ax-euc    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).

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

6. ax-sub    Juxtaposing the same form with equal forms leaves equal forms:   p = q  implies  p v = q v.

Commutativity of LoF

7. ax-cmm    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 self-dual. 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’.

Spencer-Brown 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. 28-35]:

	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. 50-52].

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 Spencer-Brown’s original numbering scheme for cross-referencing, 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₀

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₀:

	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₁

Although System₀ is the only one demonstrated by Spencer-Brown, 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₁ is any more complicated than System₀. The virtue of this basis, as noted by Spencer-Brown, 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₁

	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 ax-sub)
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 ax-sub)
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₀, 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 ) )	(ax-cmm)
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 ax-beq)
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	(ax-cmm)
2	q ( p ) = ( p ) q	(ax-cmm)
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 41-step 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₀, J2. This completes the proof that Basis₁ is at least as powerful as Basis₀.

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 ax-beq)
7	( ( p ) ( q ) ) r = ( ( p r ) ( q r ) )	(1,6 eucr)

System₂

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₂ is at least as powerful as Basis₁.

Basis₂

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³ 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 ) )	(ax-cmm)
2	( ( ( p ) ) ) ( p ) = ( p ) ( ( ( p ) ) )	(ax-cmm)
3	( ( ( p ) ) ( p ) ) ( ( ( ( p ) ) ) ( p ) )
	= ( ( ( ( p ) ) ) ( p ) ) ( ( ( p ) ) ( p ) )	(ax-cmm)
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 ax-beq)
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₂ is at least as strong as Basis₁.

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₃

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 ax-beq)
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 ax-beq)
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	(ax-cmm)
2	( p ( ( p ) ) ) = ( ( ( p ) ) p )	(1 ax-beq)
3	( ( p ( ( p ) ) ) ) = ( ( ( ( p ) ) p ) )	(2 ax-beq)
4	( ( ( p ) ) ( p ) ) =	(robbins)
5	( p ) ( ( p ) ) = ( ( p ) ) ( p )	(ax-cmm)
6	( ( p ) ( ( p ) ) ) = ( ( ( p ) ) ( p ) )	(5 ax-beq)
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 ax-beq)
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 proof-display 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.

conj-assc

( ( ( ( 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.

	bicond-assc	( ( ( ( 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]

---

1. “…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). ↩

2. 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 Near-Boolean Algebra Boolean”, J. Automated Reasoning 6(4), 465–489 (1990) and “Absorption and idempotency criteria for a problem in near-Boolean algebras”, J. Algebra 153(2), 414–423 (1992)). See http://homepages.math.uic.edu/~kauffman/Robbins.htm for a LoF-inspired derivation by Louis Kauffman that does not take the void as given. ↩

3. 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 . ↩