Richard Suchenwirth 2005-04-12 - Boolean functions, in which arguments and result are in the domain {true, false}, or {1, 0} as expr has it, and operators are e.g. {AND, OR, NOT} resp. {&&, ||, !}, can be represented by their truth table, which for example for {$a && $b} looks like:

 a b  a&&b
 0 0  0
 1 0  0
 0 1  0
 1 1  1

As all but the last column just enumerate all possible combinations of the arguments, first column least-significant, the full representation of a&&b is the last column, a sequence of 0s and 1s which can be seen as binary integer, reading from bottom up: 1 0 0 0 == 8. So 8 is the associated integer of a&&b, but not only of this - we get the same integer for !(!a || !b), but then again, these functions are equivalent.

To try this in Tcl, here's a truth table generator that I borrowed from a little proving engine, but without the lsort used there - the order of cases delivered makes best sense when the first bit is least significant:

 proc truthtable n {
    # make a list of 2**n lists, each with n truth values 0|1
    set res {}
    for {set i 0} {$i < (1<<$n)} {incr i} {
        set case {}
        for {set j  0} {$j <$n} {incr j } {
            lappend case [expr {($i & (1<<$j)) != 0}]
        }
        lappend res $case
    }
    set res
 }

Now we can write n(f), which, given a Boolean function of one or more arguments, returns its characteristic number, by iterating over all cases in the truth table, and setting a bit where appropriate:

 proc n(f) expression {
    set vars [lsort -unique [regsub -all {[^a-zA-Z]} $expression " "]]
    set res 0
    set bit 1
    foreach case [truthtable [llength $vars]] {
        foreach $vars $case break
        set res [expr $res | ((($expression)!=0)*$bit)]
        incr bit $bit ;#-- <<1, or *2
    }
    set res
 }

Experimenting:

 % n(f) {$a && !$a} ;#-- contradiction is always false
 0
 % n(f) {$a || !$a} ;#-- tautology is always true
 3
 % n(f) {$a}        ;#-- identity is boring
 2
 % n(f) {!$a}       ;#-- NOT
 1
 % n(f) {$a && $b}  ;#-- AND
 8
 % n(f) {$a || $b}  ;#-- OR
 14
 % n(f) {!($a && $b)} ;#-- de Morgan's laws:
 7
 % n(f) {!$a || !$b}  ;#-- same value = equivalent
 7

So the characteristic integer is not the same as the Goedel number of a function, which would encode the structure of operators used there.

 % n(f) {!($a || $b)} ;#-- interesting: same as unary NOT
 1
 % n(f) {!$a && !$b}
 1

Getting more daring, let's try a distributive law:

 % n(f) {$p && ($q || $r)}
 168
 % n(f) {($p && $q) || ($p && $r)}
 168

Daring more: what if we postulate the equivalence?

 % n(f) {(($p && $q) || ($p && $r)) == ($p && ($q || $r))}
 255

Without proof, I just claim that every function of n arguments whose characteristic integer is 2^(2^n) - 1 is a tautology (or a true statement - all bits are 1). Conversely, postulating non-equivalence turns out to be false in all cases, hence a contradiction:

 % n(f) {(($p && $q) || ($p && $r)) != ($p && ($q || $r))}
 0

So again, we have a little proving engine, and simpler than last time.

In the opposite direction, we can call a Boolean function by its number and provide one or more arguments - if we give more than the function can make sense of, non-false excess arguments lead to constant falsity, as the integer can be considered zero-extended:

 proc f(n) {n args} {
    set row 0
    set bit 1
    foreach arg $args {
        set row [expr {$row | ($arg != 0)*$bit}]
        incr bit $bit
    }
    expr !!($n &(1<<$row))
 }

Trying again, starting at OR (14):

 % f(n) 14 0 0
 0
 % f(n) 14 0 1
 1
 % f(n) 14 1 0
 1
 % f(n) 14 1 1
 1

So f(n) 14 indeed behaves like the OR function - little surprise, as its truth table (the results of the four calls), read bottom-up, 1110, is decimal 14 (8 + 4 + 2). Another test, inequality:

 % n(f) {$a != $b}
 6
 % f(n) 6 0 0
 0
 % f(n) 6 0 1
 1
 % f(n) 6 1 0
 1
 % f(n) 6 1 1
 0

Trying to call 14 (OR) with more than two args:

 % f(n) 14 0 0 1
 0
 % f(n) 14 0 1 1
 0
 53 % f(n) 14 1 1 1
 0

The constant 0 result is a subtle indication that we did something wrong :)

Implication (if a then b, a -> b) can in expr be expressed as $a <= $b - just note that the "arrow" seems to point the wrong way. Let's try to prove "Modus Barbara" - "if a implies b and b implies c, then a implies c":

 % n(f) {(($a <= $b) && ($b <= $c)) <= ($a <= $c)}
 255

With less abstract variable names, one might as well write

 % n(f) {(($Socrates <= $human) && ($human <= $mortal)) <= ($Socrates <= $mortal)}
 255

But this has been verified long ago, by Socrates' death :^)

---

Lars H: A remark concerning the use of the word "proof" above. Strictly speaking, the above doesn't prove any implications; it verifies that the given formula is a tautology (evaluates to true for any assignment of true/false to its variables). While from one point of view these things are the same -- a formula is a theorem of standard propositional logic if and only if it is a tautology -- they are also quite different, because "proof" is a concept that has meaning only in relation to a particular theory, whereas "tautology" is defined with respect to a particular model. It is possible to deduce from the fact that a formula is a tautology that there is a proof of it, but that deduction relies on a result in the metatheory of propositional logic.

More formally, a proof in a theory T is defined to be a sequence of formulae where each formula is (i) a premise, (ii) an axiom of the theory T, or (iii) a formula that follows (using one of the rules of inference of T) from some previous formulae in the proof. If there is a proof in the theory under consideration that ends with B and has premises A1,...,An, then one writes A1,...,An|-B (this |- is really a \u22A2). A formula B is a theorem in a theory if |-B, i.e., if there is a proof of it without any additional assumptions.

CL applauds Lars' exposition of the distinction between model and theory.

---

The way back from an integer to a logical expression is shown on Disjunctive Normal Form.

---

See also Parsing Polish notation - A little proving engine - NAND - Boolean Functions and Cellular Automata

---