# Introduction

This article is dedicated to boolean lattices. A boolean lattice is another

name for a boolean algebra.

A boolean lattice is an algebraic structure with two binary operators “*” and

“+” which represent “and” and “or”, a unary operator “-” which represents

negation. The binary operators are commutative, associative and

distributive. Furthermore there are the constants “0” and “1” which represent

“False” and “True”. “0” is neutral for “+” and “1” is neutral for “*”. In

addition to that we have the axioms “a*(-a)=0” and “a+(-a)=1” for all “a”.

I.e. a boolean lattice is a distributive lattice with some additional

operations, some additional axioms and some lost axioms (e.g. the absorption

laws are not axioms in a boolean lattice).

The fact that in a boolean lattice some of the inherited axioms loose their

axiom status requires some attention.

# Inheriting axioms

Abstract modules can have axioms and abstract operations. Axioms are

assertions which do not have a proof. They are assumptions. From the axioms

some other assertions can be derived. I.e. we have the following logic within

an abstract module “m1”.

m1_axioms => m1_assertions

If we design a module “m2” which inherits “m1” we can decide which of the

axioms we keep and which of them we abandon. I.e. we split the axioms

m1_axioms = kept_axioms + lost_axioms

Furthermore we can give “m2” some new axioms, i.e. we get

m2_axioms = kept_axioms + new_axioms

The axioms of “m2” are not sufficient to prove the derived assertions of

“m1” because some axioms of “m1” lost their axiom status. In order to use the

asssertions of “m1” the module “m2” has to provide a proof for all abandoned

axioms based on its own axioms.

m2_axioms => lost_axioms

These proofs must be done without the use of the derived assertions of

“m1”. Otherwise we introduce circular reasoning. As soon as the abandoned

axioms are proved within “m2” the full power of the derived assertions of the

module “m1” is available within the module “m2”.

# The base class DISTRIBUTIVE_LATTICE

A boolean lattice inherits from a distributive lattice. A distributive lattice

is based in the following operations and axioms

deferred class DISTRIBUTIVE_LATTICE end feature -- Operations * (a,b: CURRENT): CURRENT deferred end + (a,b: CURRENT): CURRENT deferred end = (a,b: CURRENT): BOOLEAN deferred end <= (a,b: CURRENT): BOOLEAN ensure Result = (a=a*b) end >= (a,b: CURRENT): BOOLEAN ensure Result = (a+b=b) end -- ... "<", ">" defined in the usual manner (not important for the -- following) end feature -- Axioms all(a,b,c:CURRENT) deferred ensure -- strong equality a=b => a~b -- commutative a*b = b*a a+b = b+a -- associative a*b*c = a*(b*c) a+b+c = a+(b+c) -- absorption a = a*(a+b) a = a+(a*b) -- distributive a*(b+c) = a*b+a*c a+(b*c) = (a+b)*(a+c) end end

With this operations and axioms a couple of assertions have already been

proved.

feature -- Proved assertions all(a,b,c:CURRENT) ensure a=a (a=b) = (b=a) a=b => b=c => a=c a*a = a a+a = a a*b <= a a*b <= b c<=a => c<=b => c<=a*b a <= a+b b <= a+b a<=c => b<=c => a+b<=c a<=a a<=b => b<=a => a=b a<=b => b<=c => a<=c a<=b = b>=a end end

For a descendant of “distributive_lattice” it is not important how the proofs

have been done.

# The derived class BOOLEAN_LATTICE

The module “boolean_lattice” has the following basic definitions in addition to

the already inherited ones.

deferred class BOOLEAN_LATTICE inherit DISTRIBUTIVE_LATTICE end feature -- Additional operations and axioms 0: CURRENT -- The bottom element. deferred end 1: CURRENT -- The top element. deferred end - (a:CURRENT): CURRENT -- The complement (negation) of `a'. deferred end all(a,b:CURRENT) deferred ensure neutral_0: a+0 = a neutral_1: a*1 = a compl_0: a*(-a) = 0 compl_1: a+(-a) = 1 end end

A compiler analyzing the module “boolean_lattice” discovers that the module

does not have any effective assertion which states strong equality,

commutativity, associativity and distributivity. Therefore it concludes that

these laws are kept as axioms. Because the class BOOLEAN_LATTICE is an

abstract class it is allowed to have axioms

Furthermore the compiler discovers that the absorption laws are stated as

effective assertions within the module (see next chapter). From this fact it

concludes that it has to prove the absorption laws without using any inherited

derived assertions.

# Idempotence and absorption

In a boolean lattice it is possible to prove the idempotence laws of the join

and meet operation based on the distributivity and the neutrality axioms.

feature -- Idempotence all(a:CURRENT) check c1: a*a + a*(-a) = a*a -- compl_0, neutral_0 c2: (a+a)*(a+(-a)) = a+a -- compl_1, neutral_1 ensure idem_1: a = a*a -- c1, distr, compl_1 idem_2: a = a+a -- c2, distr, compl_0 end end

Having the idempotence laws available it is possible to prove some facts about

“0” and “1”.

feature -- Properties of "0" and "1" all(a:CURRENT) check c1: a*0 = a*(a*(-a)) -- compl_0 c2: a+1 = a+(a+(-a)) -- compl_1 ensure bottom: a*0 = 0 -- c1, assoc, idem, compl_0 top: a+1 = 1 -- c2, assoc, idem, compl_1 max_1: a<=1 -- def "<=", neutral_1 min_0: 0<=a -- def "<=", bottom end end

feature -- Top and bottom are complements all check c1: -0 = (-0) * (0 + (-0)) -- neutral_1, compl_1 c2: -1 = (-1) + 1*(-1) -- neutral_0, compl_0 ensure bot_compl: -0 = 1 -- c1, distr, idem, compl_0, compl_1 top_compl: -1 = 0 -- c2, distr, idem, compl_1, compl_0 end end

With the help of the idempotence laws and the assertions “a*0=0” and “a+1=1”

it is possible to prove the absorption laws.

feature -- Absorption all(a,b:CURRENT) check c1: a*(a+b) = a*1+a*b -- distr, idem, neutral_1 c2: a+a*b =(a+0)*(a+b) -- distr, idem, neutral_0 ensure absorb_1: a*(a+b) = a -- c1, distr, top, neutral_1 absorb_2: a+a*b = a -- c2, distr, bottom, neutral_0 end end

Since the absorptions laws are proved based on the inherited axioms and the

new axioms, all proved assertions inherited from the module

“distributed_lattice” can be used from now on without the danger of creating

circular proofs.

# Involution

In a boolean algebra the inversion law “-(-a)=a” is valid. Since the inversion

law is an equality, it can be proved by using the law of antisymmetry of the

order relation.

feature -- Involution all(a:CURRENT) check c1: a = a*((-a)+(-(-a))) -- neutral_1, compl_1 c2: a <= -(-a) -- c1, dist, compl_0, neutral_1, def "<=" c3: a = a + (-a)*(-(-a)) -- neutral_0, compl_0 c4: a >= -(-a) -- c3, dist, compl_1, neutral_0, def ">=" ensure -(-a) = a -- antisymm, c2,c4 end end

# Order reversal

Negation inverts the order, i.e. “a<=b” is equivalent to “-b <= -a”. The order

reversal law is similar to the contrapositive law of boolean values. Since the

order reversal law is a boolean equivalence, it can be proved by proving the

forward and backward direction.

We use an additional lemma to prove the forward an backward direction. Since

the auxiliary lemma is not interesting to the user we put it into a private

feature block.

feature{NONE} -- Lemma for order reversal reversal_lemma: all(a,b:CURRENT) require a<=b check c1: a = a*b c2: -b = (-b)*(-a) + (-b)*a -- neutral_1, compl_1, dist c3: (-b)*a = (-b)*(a*b) -- c1 c4: (-b)*a = 0 -- c3, com, assoc, compl_0, bottom c5: -b = (-b)*(-a) -- c2, c4, neutral_0 ensure -b <= -a -- c5 end end

With this lemma it is easy to prove the order reversal law.

feature -- Order reversal all(a,b:CURRENT) check c1: (-b <= -a) => (-(-a) <= -(-b)) -- reversal_lemma ensure (a<=b) = (-b <= -a) -- fwd: reversal_lemma, bwd: c1,inversion end end

# De Morgan’s laws

The laws of de Morgan

-(a*b) = (-a)+(-b) -(a+b) = (-a)*(-b)

are equality laws. They can be proved with the help of the antisymmetry law of

the corresponding order relation. We factor out the needed inequality laws and

put them into a private feature block.

feature{NONE} -- Lemmas for de Morgan lemma_1: all(a,b:CURRENT) check c1: a <= a+b -- inherited c2: b <= a+b -- inherited c3: -(a+b) <= -a -- c1, order reversal c4: -(a+b) <= -b -- c2, order reversal ensure -(a+b) <= (-a)*(-b) -- c3, c4, meet is infimum end lemma_2: all(a,b:CURRENT) check c1: a*b <= a -- inherited c2: a*b <= b -- inherited c3: -a <= -(a*b) -- c1, order reversal c4: -b <= -(a*b) -- c2, order reversal ensure (-a)+(-b) <= -(a*b) -- c3, c4, join is supremum end end

With the help of the lemmas the proof of De Morgan’s laws is straighforward.

feature -- De Morgan all(a,b:CURRENT) check c1: -((-a)+(-b)) <= a*b -- lemma_1, involution c2: -(a*b) <= (-a)+(-b) -- c1, order reversal c3: a+b <= -((-a)*(-b)) -- lemma_2, involution c4: (-a)*(-b) <= -(a+b) -- c3, order reversal ensure -(a*b) = (-a)+(-b) -- c2, lemma_2, antisymm -(a+b) = (-a)*(-b) -- c4, lemma_1, antisymm end end