Cross-Derivation of Boundary Logic Axiomatizations

On this page, three axiomatizations of boundary logic from Spencer-Brown, Bricken, and Kauffman are shown to be equivalent. For each system the original source is given, followed by the axiomatization and derivations of the other rules.

Spencer-Brown

Source: Spencer-Brown, G. (1969). Laws of Form. Allen and Unwin, London.

Axioms

J1. Position J2. Transposition

( ( A ) A ) ( ( A B ) ( A C ) )

= =

A ( ( B ) ( C ) )

Theorems

C1. ( ( A ) ) = A

                          ((a))     Given
(((a)     )(a     )      )((a))     J1, A=(a)
(((a)((a)))(a((a)))      )          J2, A=((a))
(          (a((a)))      )          J1, A=(a)
(          (a((a)))((a)a))          J1, A=a
(          ( ((a)))((a) ))  a       J2, A=a
                            a       J1, A=((a))

C2. A ( A B ) = A ( B )

a(   a     b  )     Given
a(   a  ( (b)))     C1, A=b
a(( (a))( (b)))     C1, A=a
 ((a(a))(a(b)))     J2, A=a
 (      (a(b)))     J1, A=a
         a(b)       C1, A=a(b)

C3. A ( ) = ( )

  a( )       Given
  a(a)       C2, A=a
((a(a)))     C1, A=a(a)
(      )     J1, A=a

CX. ( ( A B ) ( A ( B ) ) ) = A

((ab   )(a( b)))     Given
((ab   )(a(ab)))     C2, A=a
((ab   )(a    ))     C2, A=(ab)
((ab(a))(a    ))     C2, A=(a)
((ab( ))(a    ))     C2, A=a
((  ( ))(a    ))     C3, A=ab
(       (a    ))     C1, A=
         a           C1, A=a

Bricken

Source: Bricken, W. (1986). A deductive mathematics for efficient reasoning. Technical Report HITL-R-86-2, Human Interface Technology Laboratory of the Washington Technology Center, University of Washington, Seattle, WA.

Axioms

Dominion Involution Pervasion

A ( ) ( ( A ) ) A ( A B )

= = =

( ) A A ( B )

Theorems

Position ( ( A ) A ) =

((a)a)     Given
(( )a)     Pervasion, A=a
(( ) )     Dominion, A=a
           Involution, A=

Deep Pervasion A ( B ( A C ) ) = A ( B ( C ) ) any depth!

a( b(ac))     Given
a(ab(ac))     Pervasion, A=a
a(ab( c))     Pervasion, A=a
a( b( c))     Pervasion, A=a

Transposition ( ( A B ) ( A C ) ) = ( ( B ) ( C ) ) A

                     ((ab)(ac))     Given
(   (              ))((ab)(ac))     Involution, A=
((a)(              ))((ab)(ac))     Dominion, A=(a)
((a)((  ( ))(  ( ))))((ab)(ac))     Involution (2x), A=
((a)((ab( ))(ac( ))))((ab)(ac))     Dominion (2x), A=ab, A=ac
((a)((ab(a))(ac(a))))((ab)(ac))     Pervasion (2x), A=a
((a)((ab   )(ac   )))((ab)(ac))     Deep Pervasion (2x), A=(a)
((a)                )((ab)(ac))     Pervasion, A=((ab)(ac))
  a                  ((ab)(ac))     Involution
  a                  (( b)( c))     Deep Pervasion, A=a

Huntington ( ( A ) B ) ( ( A ) ( B ) ) = A

((a)b) ((a)(   b))     Given
((a)b) ((a)((a)b))     Pervasion, A=(a)
((a)b) ((a)      )     Pervasion, A=((a)b)
((a)b)   a             Involution, A=a
(( )b)   a             Pervasion, A=a
(( ) )   a             Dominion, A=b
         a             Involution, A=

Kauffman

Source: Kauffman, L. H. (1990). Robbins algebra. In Proceedings of the 20th International Symposium on Multiple-Valued Logic, pages 54-60, Charlotte, NC. IEEE Computer Society Press.

Axiom

Huntington ( ( A ) B ) ( ( A ) ( B ) ) = A

Theorems

Lemma 1. A ( A ) = B ( B )

  a                 (a)                      Given
((a)(b))((a)((b)))  (a)                      Huntington, A=a, B=(b)
((a)(b))((a)((b)))(((a))(b))(((a))((b)))     Huntington, A=(a), B=(b)
     b  ((a)((b)))          (((a))((b)))     Huntington, A=b, B=(a)
     b       (b)                             Huntington, A=(b), B=(a)

Lemma 2. ( ( A ) ) = A

  ((a))                         Given
((((a)))(a)) ((((a)))((a)))     Huntington, A=((a)), B=(a)
((((a)))(a)) (( (a) ) (a) )     Lemma 1, A=((a)), B=(a)
         a                      Huntington, A=a, B=((a))

Lemma 3. A ( A ) = ( )

a(a)       Given
 ( )       Lemma 1, A=a, B=

Lemma 4. ( A ( A ) ) =

(a(a))     Given
( ( ))     Lemma 3, A=a
           Lemma 2, A=

Lemma 5. A A = A

              a  a
(          (  a  a))     Lemma 2, A=aa
((  a  (a))(  a  a))     Lemma 4, A=a
((((a))(a))(((a))a))     Lemma 2, A=a
(  (a)             )     Huntington, A=(a), B=a
    a                    Lemma 2, A=a

Lemma 6. ( ( A ) B ) A = A

((a)b)  a                Given
((a)b)((a)b)((a)(b))     Huntington, A=a, B=b
      ((a)b)((a)(b))     Lemma 5, A=((a)b)
        a                Huntington, A=a, B=b

Lemma 7. ( A ) B = ( A B ) B

  (a)             b     Given
(((a))b)(((a))(b))b     Huntington, A=(a), B=b
(((a))b)          b     Lemma 6, A=b, B=((a))
(  a  b)          b     Lemma 2, A=a

Lemma 8. ( ( A C ) ( B C ) ) = ( ( A ) ( B ) ) C

  ((ac)(bc))
((((ac)(bc)))c)((((a  c  )(b  c  )))(c))     Huntington, A=((ac)(bc)), B=c
(  (ac)(bc)  c)(  (a  c  )(b  c  )  (c))     Lemma 2 (2x)
(  (a )(b )  c)(  (a  c  )(b  c  )  (c))     Lemma 7 (2x)
(  (a )(b )  c)(  (a((c)))(b((c)))  (c))     Lemma 2 (2x)
(  (a )(b )  c)(                    (c))     Lemma 6 (2x)
(  (a )(b )  c)                      c       Lemma 2
(  (a )(b )   )                      c       Lemma 7

Lemma X. A ( ) = ( )   [not given in Kauffman (1990)]

 a( )     Given
 a(a)     Lemma 7
  ( )     Lemma 3