Why do we use 2-valued logic (True / False) instead of for example 4-valued logic (Boolean Algebra on two elements powerset)? 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

 A: 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.
