Consider the Boolean algebra (Power-set of two elements) with elements $0,1,a,b$. Define $p \implies q$ as $\neg p \lor q$. Then by "brute force computation" (see the attached sage script) we get: The boolean algebra satisfies:

1) Law of the excluded middle ($A \lor \neg A$)

2) Law of contraposition $(A\rightarrow B) \iff (\neg B \rightarrow \neg A)$

3) Reductio ad absurdum: $((\neg A \rightarrow B) \land (\neg A \rightarrow \neg B)) \rightarrow A$

4) de Morgan's law: $\neg(A \land B) \iff (\neg A \lor \neg B)$

5) Syllogism: $((A \rightarrow B) \land (B \rightarrow C)) \rightarrow (A \rightarrow C)$

Why do we use in "mainstream mathematical proofs" 2-valued logic (True / False) instead of for example the 4-valued logic (Boolean Algebra) if both logics seem to satisfy "useful" axioms. What would change if one uses the 4-valued logic (Boolean Algebra) in proofs?

Thanks for your help!

Attached Sage script:

from sage.all import *

o = set([]) 
a = set([0]) 
b = set([1]) 
l = set([0,1]) 

ba = [o,a,b,l]

def nicht(x):
    return l.difference(x)

def und(x,y):
    return x.intersection(y)

def oder(x,y):
    return x.union(y)

def implies(x,y):
    return oder(nicht(x),y)

def equal(x,y):
    return oder(und(x,y),und(nicht(x),nicht(y)))

# law of excluded middle:
for A in ba:
    print A, oder(A,nicht(A))==l

# law of contraposition:
for x in ba:
    for y in ba:
        print x, y, implies(x,y)==implies(nicht(y),nicht(x))

# reductio ad absurdum
for A in ba:
    for B in ba:
        print A,B, implies(und(implies(nicht(A),B),implies(nicht(A),nicht(B))),A) == l

# de morgans law
for A in ba:
    for B in ba:
        print A,B, nicht(und(A,B))==oder(nicht(A),nicht(B))

# syllogism:
for A in ba:
    for B in ba:
        for C in ba:
            print A,B,C, implies(und(implies(A,B),implies(B,C)),implies(A,C))==l
  • $\begingroup$ What do you hope to get by using 4-value logic? How would you interpret a truth value of $a$? $\endgroup$ Commented Jun 8, 2019 at 8:12
  • 1
    $\begingroup$ What would there be to be gained? This is equivalent to classically investigating an $a$-theory, where $1$ and $a$ are true and $0$ and $b$ are false, and a $b$-theory where $1$ and $b$ are true and $0$ and $a$ are false. So could we perhaps investigate the theory of abelian and non-abelian groups in parallel? Sure, just the same way as we do now: We prove statements about all groups, and prove additional statement under the additional hypothesis that our group is abelian ... $\endgroup$ Commented Jun 8, 2019 at 8:18
  • $\begingroup$ @MarkKamsma: I am not sure. I thought of for example $0=$ provable false, $1=$ provable true, $a=$ not provable but false, $b=$ not provable but true? I am not sure however, if this would be of any use. $\endgroup$
    – user276611
    Commented Jun 8, 2019 at 8:32
  • $\begingroup$ @HagenvonEitzen: I don't know, this question is out of curiosity. See my comment to markkamsma, for a possible truth-value assigment to $a$ and $b$ $\endgroup$
    – user276611
    Commented Jun 8, 2019 at 8:34
  • 1
    $\begingroup$ Provable/nonprovable and true/false shouldn't me mixed. The former is syntax and the latter is semantics. We do want theorems that relate the two, like soundness and completeness, if possible. $\endgroup$
    – Ennar
    Commented Jun 8, 2019 at 9:21

1 Answer 1


You can interpret classical propositional logic (CPL) into any Boolean algebra. We also have soundness and completeness with respect to this interpretation. That is, a theorem of CPL is provable (with respect to some typical proof system, e.g. the propositional fragment of the sequent calculus LK) if and only if it evaluates to the unit/top element of any Boolean algebra. You can actually prove completeness from soundness and the Lindenbaum-Tarski algebra with this approach to semantics.

That said, it is much harder to (directly) show that that some formula interprets to the top element for every Boolean algebra than it is to show it for some particular Boolean algebra. In particular, the Boolean algebra on a two element set is extremely simple. It also turns out that CPL with usual proof systems is complete with respect to it too. In other words, instead of checking all Boolean algebras, it suffices to check this one extremely simple one.

And that's pretty much it. It is definitely useful to know that you can interpret CPL into any Boolean algebra, but, for the purposes of logic, no (closed) CPL formula can distinguish amongst them. If all you care about is establishing provability/validity, there's no reason to consider anything other than the two element Boolean algebra.

(As a matter of terminology, we don't use $2$-valued logic in proofs1, we use proof systems that don't care what the semantics are at all. You could say we use classical logic, but as you've just illustrated, that doesn't depend on being $2$-valued.)

1 Also, as a fairly subtle point, you can have a $2$-valued logic that isn't classical.

  • $\begingroup$ Ok, thanks for your answer (+1). But why do proofs by contradiction start with assume $A$ is false, then get a contradiction, so $A$ must be true (law of excluded middle), if $A$ could be assigned more than two truth values. I don't understand that. Of course you could argue, that the two valued Boolean Algebra is the most simple, but this does not exclude the possibility of having more than two truth-values assigned to a variable. $\endgroup$
    – user276611
    Commented Jun 8, 2019 at 8:45
  • 1
    $\begingroup$ That's not what proofs by contradiction do. They assume $\neg A$, show that that leads to a contradiction, and hence conclude $A$. Again, proofs say nothing about semantics. There is no "$A$ is false" or "$A$ is true" as far as proofs are concerned. If you do interpret it into a Boolean algebra, you'll find that the interpretation of $\neg A\to\bot$ is $A$ regardless of whether $A$ is interpreted as the top element, bottom element, or some other element. You may find this blog post of mine helpful. $\endgroup$ Commented Jun 8, 2019 at 9:32
  • $\begingroup$ thanks for the hint $\endgroup$
    – user276611
    Commented Jun 8, 2019 at 9:40

You must log in to answer this question.