Laws of Form

Richard Suchenwirth 2005-04-10 - After many years, I re-read

 G. Spencer-Brown, "Laws of Form". New York: E.P. Dutton 1979

which is sort of a mathematical thriller, if you will. Bertrand Russell commented that the author "has revealed a new calculus, of great power and simplicity" (somehow sounds like Tcl ;^). In a very radical simplification, a whole world is built up by two operators, the empty string "" (which could be likened to or) and a overbar-hook (with the meaning of not) that I can't type here - it's a horizontal stroke over zero or more operands, continued at right by a vertical stroke going down to the baseline. In these Tcl experiments, I use "" for "" and angle-brackets <> for the overbar-hook (with zero or more operands in between).

Lars H: Speaking of "the empty string operator" like this is rather confusing. The normal terminology would be to say that juxtaposition (writing things next to each other) is one of the operations. Then of course the empty string should be considered to denote the neutral element for the operation denoted by juxtaposition.

One point that was new for me is that the distinction between operators and operands is not cast in stone. Especially constants (like "true" and "false" in Boolean algebras) can be equally well expressed as neutral elements of operators, if these are considered variadic, and having zero arguments. This makes sense, even in Tcl, where one might implement them as

 proc and args {
    foreach arg $args {if {![uplevel 1 expr $arg]} {return 0}}
    return 1
 }
 proc or args {
    foreach arg $args {if {[uplevel 1 expr $arg]} {return 1}}
    return 0
 }

which, when called with no arguments, return 1 or 0, respectively. So [or] == 0 and [and] == 1. In Spencer-Brown's terms, [] (which is "", the empty string with no arguments) is false ("nil" in LISP), and [<>] is the negation of "", i.e. true. His two axioms are:

 <><> == <> "to recall is to call       -- (1 || 1) == 1"
 <<>> ==    "to recross is not to cross -- !!0 == 0"

and these can be implemented by a string map that is repeated as long as it makes any difference (sort of a trampoline) to simplify any expression consisting only of operators and constants (which are operators with zero arguments):

 proc lf'simplify expression {
    while 1 {
        set res [string map {<><> <> <<>> ""} $expression]
        if {$res eq $expression} {return $res}
        set expression $res
    }
 }

Testing:

 % lf'simplify <<><>><>
 <>

which maps <><> to <>, <<>> to "", and returns <> for "true".

 % lf'simplify <a>a
 <a>a

In the algebra introduced here, with a variable "a", no further simplification was so far possible. Let's change that - "a" can have only two values, "" or <>, so we might try to solve the expression by assuming all possible values for a, and see if they differ. If they don't, we have found a fact that isn't dependent on the variable's value, and the resulting constant is returned, otherwise the unsolved expression:

 proc lf'solve {expression var} {
    set results {}
    foreach value {"" <>} {
        set res [lf'simplify [string map [list $var $value] $expression]]
        if {![in $results $res]} {lappend results $res}
        if {[llength $results] > 1} {return $expression}
    }
    set results
 }

#-- with a helper function in that reports containment of an element in a list:

 proc in {list element} {expr {[lsearch -exact $list $element] >= 0}}

Testing:

 % lf'solve <a>a a
 <>

which means, in expr terms, {(!$a || $a) == 1}, for all values of a. In other words, a tautology. All of Boole's algebra can be expressed in this calculus:

 (1) not a       == !$a       == <a>
 (2) a or b      == $a || $b  == ab
 (3) a and b     == $a && $b  == <<a><b>>
 (4) a implies b == $a <= $b  == <a>b

We can test it with the classic "ex contradictione quodlibet" (ECQ) example - "if p and not p, then q" for any q:

 % lf'solve <<p><<p>>>q p
 q

So formally, q is true, whatever it is :) If this sounds overly theoretic, here's a tricky practical example in puzzle solving, Lewis Carroll's last sorites (pp. 123f.). The task is to conclude something from the following premises:

The only animals in this house are cats
Every animal is suitable for a pet, that loves to gaze at the moon
When I detest an animal, I avoid it
No animals are carnivorous, unless they prowl at night
No cat fail to kill mice
No animals ever take to me, except what are in this house
Kangaroos are not suitable for pets
None but carnivora kill mice
I detest animals that do not take to me
Animals that prowl at night always love to gaze at the moon

These are encoded to the following one-letter predicates:

a - avoided by me
c - cat
d - detested by me
h - house, in this
k - kill mice
m - moon, love to gaze at
n - night, prowl at
p - pet, suitable for
r - (kanga)roo
t - take to me
v - (carni)vorous

So the problem set can be restated, in Spencer-Brown's terms, as

 <h>c <m>p <d>a <v>n <c>k <t>h <r><p> <k>v td <n>m

I first don't understand why all premises can be just written in a row, which amounts to implicit "or", but it seems to work out well. As we've seen that <x>x is true for any x, we can cancel out such tautologies. For this, we reformat the expression to a list of values of type x or !x, that is in turn dumped into a local array for existence checking. And when both x and !x exist, they are removed from the expression:

 proc lf'cancel expression {
    set e2 [string map {"< " ! "> " ""} [split $expression ""]]
    foreach term $e2 {if {$term ne ""} {set a($term) ""}}
    foreach var [array names a ?] {
        if [info exists a(!$var)] {
            set expression [string map [list <$var> "" $var ""] $expression]
        }
    }
    set expression
 }
 puts [lf'cancel {<h>c <m>p <d>a <v>n <c>k <t>h <r><p> <k>v td <n>m}]

which results in:

 a   <r>

translated back: "I avoid it, or it's not a kangaroo", or, reordered, "<r> a" which by (4) means, "All kangaroos are avoided by me".

Afterthought: See also NAND for how all Boolean operations can be constructed out of the single NAND ("not-and") operator.