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