Laws of Form in Metamath

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 [1] 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 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 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 [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 10-Jun-2016          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.

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
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 & r = q     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).

ax-beq

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

ax-sub

Juxtaposing the same form with equal forms leaves equal forms:
p = q     p v = q v.

Commutativity of LoF
ax-cmm

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.

Auxiliary theorems
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 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 (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

System0

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:

Basis0

j1.0

( ( p ) p )

=

j2.0

( ( p r ) ( q r ) )

=

( ( p ) ( q ) ) r

and the first two theorems:

Theorems0

c1.0

( ( p ) )

=

p

c2.0

( p q ) q

=

( p ) q

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)

System1

Although System0 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 System1 is any more complicated than System0. 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.

Basis1

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 Basis0, 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 Basis0, J2. This completes the proof that Basis1 is at least as powerful as Basis0.

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)

System2

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 Basis2 is at least as powerful as Basis1.

Basis2

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.

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 ) )

(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 Basis2 is at least as strong as Basis1.

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)

System3

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)

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 meta-reasoning. 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 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. I call this meta-reasoning because we’re using an undefined, intuitive notion of symmetry. See the source for a full formal proof.

Associativity of conjunction

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

Normal form of the biconditional

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:

Associativity of the biconditional

bicond-assc

( ( ( ( p ) ( q ) ) ( p q ) ) ( r ) ) ( ( ( p ) ( q ) ) ( p q ) r ) = ( ( p ) ( ( ( q ) ( r ) ) ( q r ) ) ) ( p ( ( q ) ( r ) ) ( q r ) )

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 .