Rigorous proofs of the theorems in chapter 7 of Laws of Form.

A pdf version is available.

$\require{enclose}$ $ \newcommand{\CR}[1]{\enclose{actuarial}{#1}} \newcommand{\st}[1]{\small{\text{#1}}} \newcommand{\v}[1]{\vphantom{#1}} \newcommand{\b}[1]{\vphantom{#1}\hphantom{#1}} $ —————————————————————

Introduction

In chapter 7 of Laws of Form, Spencer-Brown extends the scope of his basic equations to expressions involving any finite number of variables. Some of his arguments, when he provides them, are rigorous; others are mere sketches, and some possible generalizations are left unmentioned. This post will present fully rigorous proofs of the propositions.

Below is a list of axioms and theorems referenced in subsequent proofs:

\[\begin{align*} &\CR{\CR{pr}\;\CR{qr}}\, = \CR{\CR{p}\;\CR{q}}\,r \tag{J2}\\ &\CR{pr}\;\CR{qr} \,= \CR{\CR{\CR{p}\;\CR{q}}\,r} \tag{J2.1}\\ & \CR{\CR{a}} \,= a \tag{C1}\\ &\CR{ab}\,b \,= \CR{a\v{b}}\, b \tag{C2}\\ & \CR{\CR{\CR{a}\, b}\,c} \,= \CR{ac\v{b}}\; \CR{\CR{b}\,c} \tag{C7}\\ & \CR{\CR{a\v{b}}\;\CR{br}\;\CR{cr\v{b}}} \,= \CR{\CR{a\v{b}}\;\CR{b}\;\CR{c\v{b}}}\; \CR{\v{\CR{b}}\CR{a\v{b}}\;\CR{r\v{b}}} \tag{C8}\\ &\CR{ \CR{\CR{a\v{b}}\;\CR{r\v{b}}}\; \CR{\CR{b}\;\CR{r\v{b}}}\; \CR{\CR{x\v{b}}\,r}\; \CR{\CR{y\v{b}}\,r} } \,= \CR{\CR{r}\, ab}\; \CR{rxy} \tag{C9}\\ &\CR{\CR{\CR{a}\;\CR{r}} \CR{\CR{x}\,r}} \,= \CR{\CR{r}\,a}\; \CR{rx} \tag{C9.1} \end{align*}\]

General theorems

Spencer-Brown begins the chapter by sketching an inductive generalization of J2. Here is the proof in full.

Theorem (J2*). $\quad \CR{\CR{a_1}\;\CR{a_2}\dots \CR{a_n}}\,r\,=\CR{\CR{a_1r}\;\CR{a_2r}\dots \CR{a_nr}}$

Proof. The proof proceeds by induction on $n$. The base case is J2, where n=2. Let the induction hypothesis (J2h) be: $\CR{\CR{a_1}\;\CR{a_2}\dots \CR{a_n}}\,r\,=\CR{\CR{a_1r}\;\CR{a_2r}\dots \CR{a_nr}}$

The induction step:

\[\begin{align*} &\; \CR{\CR{a_1}\;\CR{a_2}\dots \CR{a_n}\;\CR{a_{n+1}}}\,r \\ &= \; \CR{\CR{\CR{\CR{a_1}\;\CR{a_2}\dots \CR{a_n}}}\;\CR{a_{n+1}}}\,r \tag{C1}\\ &=\; \CR{\CR{\CR{\CR{a_1}\;\CR{a_2}\dots \CR{a_n}}\,r}\;\CR{a_{n+1}r}} \tag{J2} \\ &= \; \CR{\CR{\CR{\CR{a_1r}\;\CR{a_2r}\dots \CR{a_nr}}}\;\CR{a_{n+1}r}} \tag{J2h} \\ &=\; \CR{\CR{a_1r}\;\CR{a_2r}\dots \CR{a_nr}\;\CR{a_{n+1}r}} \tag{C1} \end{align*}\]

Alternate proof. A very similar and equally short proof, using the same induction hypothesis as above.

The induction step:

\[\begin{align*} &\; \CR{\CR{a_1}\;\CR{a_2}\dots \CR{a_n}\;\CR{a_{n+1}}}\,r \\ &=\; \CR{\CR{a_1}\;\CR{a_2}\dots \CR{\CR{\CR{a_n}\;\CR{a_{n+1}}}}}\,r \tag{C1}\\ &=\; \CR{\CR{a_1r}\;\CR{a_2r}\dots \CR{\CR{\CR{a_n}\;\CR{a_{n+1}}}\,r}} \tag{J2h} \\ &=\; \CR{\CR{a_1r}\;\CR{a_2r}\dots \CR{\CR{\CR{a_nr}\;\CR{a_{n+1}r}}}} \tag{J2} \\ &=\; \CR{\CR{a_1r}\;\CR{a_2r}\dots \CR{a_nr}\;\CR{a_{n+1}r}} \tag{C1} \end{align*}\]

Before continuing, I prove a useful generalization of corollary J2.1.

Theorem (J2.1*). $\quad \CR{a_{1}r}\;\CR{a_{2}r}\dots \CR{a_{n}r}\, = \CR{\CR{\CR{a_1}\;\CR{a_2}\dots \CR{a_n}}\,r}$

Proof.

\[\begin{align*} &\; \CR{a_{1}r}\;\CR{a_{2}r}\dots \CR{a_{n}r} \\ &=\;\CR{ \CR{\CR{a_{1}r}\;\CR{a_{2}r}\dots \CR{a_{n}r}}} \tag{C1}\\ &=\; \CR{\CR{\CR{a_1}\;\CR{a_2}\dots \CR{a_n}}\,r} \tag{J2*} \end{align*}\]

Spencer-Brown states the generalizations of C8 and C9 but omits the proofs, merely noting that they are similar to J2*.

Theorem (C8*). $\quad \CR{\CR{a\v{b_1}}\;\CR{b_1r}\;\CR{b_2r}\dots \CR{b_nr}}\,= \CR{\CR{a\v{b_1}}\;\CR{b_1}\;\CR{b_2}\dots \CR{b_n}}\;\CR{\CR{a\v{b_1}}\;\CR{r\v{b_1}}}$

Proof. The proof proceeds by induction on n. The base case is C8, where n=2. Let the induction hypothesis (C8h) be: $\CR{\CR{a\v{b_1}}\;\CR{b_1r}\;\CR{b_2r}\dots \CR{b_nr}}\,= \CR{\CR{a\v{b_1}}\;\CR{b_1}\;\CR{b_2}\dots \CR{b_n}}\;\CR{\CR{a\v{b_1}}\;\CR{r\v{b_1}}}$

The induction step:

\[\begin{align*} &\;\CR{\CR{a\v{b_1}}\;\CR{b_1r}\;\CR{b_2r}\dots \CR{b_nr}\;\CR{b_{n+1}r}} \\ &=\; \CR{\CR{\CR{\CR{a\v{b_1}}\;\CR{b_1r}}}\;\CR{b_2r}\dots \CR{b_nr}\;\CR{b_{n+1}r}} \tag{C1}\\ &=\; \CR{\CR{\CR{\CR{a\v{b_1}}\;\CR{b_1r}}}\;\CR{b_2}\dots \CR{b_n}\;\CR{b_{n+1}}} \;\CR{\CR{\CR{\CR{a\v{b_1}}\;\CR{b_1r}}}\;\CR{r\v{b_1}}} \tag{C8h}\\ &=\; \CR{\CR{\CR{\CR{b_2}\dots \CR{b_n}\;\CR{b_{n+1}}}\; \CR{\CR{r\v{b_1}}}}\;\CR{\CR{\CR{a\v{b_1}}\;\CR{b_1r}}}} \tag{J2.1}\\ &=\; \CR{\CR{\CR{\CR{b_2}\dots \CR{b_n}\;\CR{b_{n+1}}}\,r}\;\CR{a\v{b_1}}\;\CR{b_1r}} \tag{C1 twice}\\ &=\; \CR{\CR{\CR{\CR{\CR{\CR{b_2}\dots \CR{b_n}\;\CR{b_{n+1}}}}\; \CR{b_1}}\,r}\; \CR{a\v{b_1}} } \tag{J2.1}\\ &=\; \CR{\CR{\CR{\CR{b_1}\;\CR{b_2}\dots \CR{b_n}\;\CR{b_{n+1}} }\,r}\; \CR{a\v{b_1}} } \tag{C1}\\ &=\; \CR{ \CR{\CR{\CR{b_1}\;\CR{b_2}\dots \CR{b_n}\;\CR{b_{n+1}} }\;\CR{\CR{r\v{b_1}}}}\; \CR{a\v{b_1}} } \tag{C1}\\ &=\;\CR{\CR{ \CR{\CR{a\v{b_1}}\;\CR{b_1}\;\CR{b_2}\dots \CR{b_n}\;\CR{b_{n+1}}}\; \CR{\CR{a\v{b_1}}\;\CR{r\v{b_1}}}}} \tag{J2}\\ &=\; \CR{\CR{a\v{b_1}}\;\CR{b_1}\;\CR{b_2}\dots \CR{b_n}\; \CR{b_{n+1}}}\; \CR{\CR{a\v{b_1}}\;\CR{r\v{b_1}}}\tag{C1} \end{align*}\]

J2.1* allows for a quicker direct proof:

\[\begin{align*} &\;\CR{\CR{a\v{b_1}}\;\CR{b_1r}\;\CR{b_2r}\dots\CR{b_nr}}\\ &=\;\CR{\CR{a\v{b_1}}\; \CR{\CR{\CR{b_1}\;\CR{b_2}\dots\CR{b_n}}\, r}} \tag{J2.1*}\\ &=\;\CR{ \CR{a\v{b_1}}\; \CR{\CR{\CR{b_1}\;\CR{b_2}\dots\CR{b_n}}\; \CR{\CR{r\v{b_1}}}}} \tag{C1}\\ &=\;\CR{\CR{\CR{\CR{a\v{b_1}}\;\CR{b_1}\;\CR{b_2}\dots\CR{b_n}}\;\CR{\CR{a\v{b_1}}\;\CR{r\v{b_1}}}}}\tag{J2}\\ &=\;\CR{\CR{a\v{b_1}}\;\CR{b_1}\;\CR{b_2}\dots\CR{b_n}}\;\CR{\CR{a\v{b_1}}\;\CR{r\v{b_1}}} \tag{C1} \end{align*}\]

Theorem (C9*). $\; \CR{ \CR{\CR{a_1}\;\CR{r}}\; \CR{\CR{a_2}\;\CR{r}}\dots\CR{\CR{a_n}\;\CR{r}} \; \CR{\CR{x_1}\,r} \;\CR{\CR{x_2}\,r} \dots\CR{\CR{x_m}\,r} }\,= \CR{\CR{r}\, a_1a_2\dots a_n}\; \CR{rx_1x_2\dots x_m}$

Proof.

\[\begin{align*} &\;\CR{ \CR{\CR{a_1}\;\CR{r}} \CR{\CR{a_2}\;\CR{r}}\dots \CR{\CR{a_n}\;\CR{r}} \; \CR{\CR{x_1}\,r}\; \CR{\CR{x_2}\,r} \dots \CR{\CR{x_m}\,r} } \\ &=\;\CR{\CR{\CR{ \CR{\CR{a_1}} \;\CR{\CR{a_2}}\dots \CR{\CR{a_n}}}\;\CR{r}} \CR{\CR{\CR{\CR{x_1}}\; \CR{\CR{x_2}} \dots \CR{\CR{x_m}}}\,r} } \tag{J2.1* twice}\\ &=\;\CR{\CR{\CR{a_1a_2\dots a_n}\;\CR{r}}\;\CR{\CR{x_1 x_2 \dots x_m}\,r} } \tag{C1 $n\!+\!m$ times}\\ &=\; \CR{\CR{r}\, a_1a_2\dots a_n} \;\CR{rx_1x_2\dots x_m}\tag{C9.1} \end{align*}\]

Next we prove a generalizion of C2.

Theorem (C2*). $\quad \CR{\CR{\CR{\CR{a_nb}\dots}\, a_2}\,a_1}\,b = \CR{\CR{\CR{\CR{a_n}\dots}\, a_2}\,a_1}\,b$

Proof. The proof proceeds by induction on n. The base case is C2, where n=1. Let the induction hypothesis (C2h) be: $\CR{\CR{\CR{\CR{a_nb}\dots}\, a_2}\,a_1}\,b = \CR{\CR{\CR{\CR{a_n}\dots}\, a_2}\,a_1}\,b$

Substitute $\CR{a_{n+1}\,b}\,a_n$ for $a_n$ . The induction step then follows immediately:

\[\begin{align*} &\;\CR{\CR{\CR{\CR{\CR{a_{n+1}\,b}\, a_nb}\dots}\, a_2}\,a_1}\,b \tag{sub}\\ &=\; \CR{\CR{\CR{\CR{\CR{a_{n+1}\,b}\, a_n}\dots}\, a_2}\,a_1}\,b \tag{C2h} \end{align*}\]

Spencer-Brown does not mention a generalized C7. Here is one possible version.

Theorem (C7*). $\;$ Let $n$ be a positive even number. Then for all such $n$ the following pair of equations holds:

\[\begin{align*} \CR{\CR{\CR{\CR{a_n}\dots}\, a_2}\,a_1} &=\; \CR{\CR{a_n}\, a_{n-1}\dots a_3 a_1} \dots\,\CR{\CR{a_4}\, a_3 a_1}\;\CR{\CR{a_2}\, a_1}\tag{i}\\ \CR{\CR{\CR{\CR{\CR{a_{n+1}}\, a_n}\dots}\, a_2}\,a_1} &=\, \CR{ a_{n+1}\,a_{n-1}\dots a_3 a_1}\; \CR{\CR{a_n}\, a_{n-1}\dots\,a_3 a_1} \dots \CR{\CR{a_4}\, a_3 a_1}\;\CR{\CR{a_2}\, a_1}\tag{ii} \end{align*}\]

Proof. Let equation (i) be the induction hypothesis. The base case is the identity $\CR{\CR{a_2}\, a_1}=\CR{\CR{a_2}\, a_1}$, where n=2. Now substitute $\CR{a_{n+1}}\,a_n$ for $a_n$. Then, \(\begin{align*} &\; \CR{\CR{\CR{\CR{\CR{a_{n+1}}\, a_n}\dots}\, a_2}\,a_1}\\ &=\; \CR{\CR{\CR{a_{n+1}}\, a_n}\, a_{n-1}\dots a_3 a_1} \dots \CR{\CR{a_4}\, a_3 a_1}\;\CR{\CR{a_2}\, a_1}\tag{i}\\ &=\; \CR{ a_{n+1}a_{n-1}\dots a_3 a_1} \;\CR{\CR{a_n}\, a_{n-1}\dots a_3 a_1} \dots \CR{\CR{a_4}\, a_3 a_1}\;\CR{\CR{a_2}\, a_1}\tag{C7} \end{align*}\)

proving the implication from (i) to (ii). In equation (ii) substitute $\CR{a_{n+2}}\,a_{n+1}$ for $a_{n+1}$. Then,

\[\begin{align*} &\; \CR{\CR{\CR{\CR{\CR{a_{n+2}}\, a_{n+1}}\dots}\, a_2}a_1} =\; \CR{\CR{a_{n+2}}\, a_{n+1}\dots a_3 a_1} \dots \CR{\CR{a_4}\, a_3 a_1}\;\CR{\CR{a_2}\, a_1} \tag{ii} \end{align*}\]

proving (i) for the succeeding even number. This proves the proposition for all $n\ge2$, and hence for all echelons of depth greater than or equal to 2.

Theorem (T14). $\;$ Any expression can be reduced to an equivalent expression not more than two crosses deep. Specifically, any expression $E$ is equivalent to $\CR{\CR{a_1}\,b_1}\;\CR{\CR{a_2}\,b_2}\dots \CR{\CR{a_n}\,b_n}\;\CR{c_1}\;\CR{c_2}\dots \CR{c_m}\,d$, where $a_i, b_i, c_i, d$ are composed (at most) of juxtapositions of variables and the two constants, $\CR{\b{a}}$ and $\quad$.

Proof. Repeated applications of C7* to any expression demonstrates the theorem. Spencer-Brown uses C7 (not having proven a generalization), but it comes to the same thing.

The final theorem follows Spencer-Brown closely.

Theorem (T15). $\;$ Given any expression $E$ and any variable $v$, $E$ can be reduced to an equivalent expression containing not more than two appearances of $v$.

Proof. In the case where $v$ is not in $E$, the theorem is trivially true, since $E= \CR{\CR{v}\,v}\, E$ by J1. So let us suppose that $v$ appears in $E$. Using C7* as many times as necessary, we rewrite $E$:

\[\begin{equation*} E= \CR{\CR{va_1}\,b_1}\;\CR{\CR{va_2}\,b_2}\dots \CR{\CR{va_n}\,b_n}\;\CR{vc_1}\;\CR{vc_2}\dots \CR{vc_m}\,d \end{equation*}\]

where $a_i ,b_i, c_i,$ and $d$ are expressions free of $v$. Then, by n applications of C8.1,

\[\begin{align*} E &= \CR{\CR{v}\,b_1}\;\CR{\CR{a_1}\,b_1}\;\CR{\CR{v}\,b_2}\;\CR{\CR{a_2}\,b_2}\dots \CR{\CR{v}\,b_n}\; \CR{\CR{a_n}\,b_n}\;\CR{vc_1}\;\CR{vc_2}\dots \CR{vc_m}\,d \\ &=\CR{\CR{v}\,b_1}\;\CR{\CR{v}\,b_2}\dots \CR{\CR{v}\,b_n}\;\CR{vc_1}\;\CR{vc_2}\dots \CR{vc_m}\,f \\ &\quad\quad\quad\text{(where $f=\CR{\CR{a_1}\,b_1}\;\CR{\CR{a_2}\,b_2}\dots \CR{\CR{a_n}\,b_n}\, d$ is free of $v$.) }\\ &= \CR{\CR{\CR{b_1}\;\CR{b_2}\dots \CR{b_n}}\;\CR{v\v{b_1}}}\; \CR{\CR{\CR{c_1\v{b_1}}\;\CR{c_2\v{b_1}}\dots \CR{c_m\v{b_1}}}\,v\v{b_1}}\, f \tag{J2.1* twice} \end{align*}\]