# Introduction

The last blog entry gave an introduction to Modern Eiffel’s proof engine. The

basic rules have been explained, the boolean operations “=>”, “and” and “or”

have been introduced with their corresponding axioms and some proofs have been

given for expressions using these operations. The class BOOLEAN up to now

looks like

immutable class BOOLEAN inherit COMPARABLE redefine is_equal end feature implication alias "=>" (o:BOOLEAN): BOOLEAN ... is_equal (o:BOOLENA): BOOLEAN ... conjuncted alias "and" (o:BOOLEAN): BOOLEAN ... disjuncted alias "or" (o:BOOLEAN): BOOLEAN ... all(a,b,c: BOOLEAN) check reflexivity: a => a modus_ponens: a => (a=>b) => b transitivity: (a=>b) => (b=>c) => (a=>c) reorder: (a=>b=>c) => (b=>a=>c) end ... -- some more proved assertions end

In this blog entry the boolean operation “not” and its axioms will be

introduced into the class BOOLEAN which open up the world of proofs by

contradiction.

# Negation and its axioms

The concept of negation is strongly related to the concept of

contradiction. If we say that some statement “a” is wrong (expressed as “not

a”) we can prove it in the following manner. We assume that “a” is valid and

derive from this assumption something which is inacceptable, i.e. something

which is definitely false e.g. a contradiction. Since the assumption of “a”

leads us to something unacceptable we can safely conclude that “a” must be

false. I.e. our proof is a refutation of “a”.

This basic idea is expressed in the axioms of negation.

negated alias "not": BOOLEAN external "built_in" ensure all(a:BOOLEAN) check intro: (a => False) => not a elim: a => not a => False indirect: (not a => False) => a end end

Recall that postconditions of built-in functions are accepted by the proof

engine without proof, i.e. they are treated as axioms.

The boolean constant “False” represents something which cannot be true.

The first axiom “intro” states the following: In order to prove that something

(i.e. “a”) is false it is sufficient to show that the assumption of “a” leads

to “False”.

The corresponding “elim” axiom states the opposite direction. If something

(i.e. “a”) is valid then the assumption that “a” is wrong leads to “False”.

The axiom “elim” is written in this form because it is convenient in the

following chapters. But in order to see the symmetry between “intro” and “elim”

we can write “elim” in the form “not a => (a => False)”. It is easy to prove

that the second form is valid as well (just use some trivial “enter” and

“premise” commands).

Note that the axioms “intro” and “elim” together postulate the fact that “not

a” and “a=>False” are equivalent. Many textbooks about logic do not introduce

“not” as an independent operation. They define “not a” by being equivalent to

“a=>False”.

In the “elim” axiom is “False” occurs on the right hand side of an

implication. This means that we can derive “False” if we have some

contradictory assumptions (the premises of “False” are “a” and “not a”).

The axiom “indirect” opens up the possibility to proof an assertion “a”

indirectly. Instead to prove “a” directly we can assume “not a” and derive

“False” from it.

# Double negation

The law of double negation states that “a” and “not not a” are equivalent. We

can proof this law using the axioms of negation.

all(a:BOOLEAN) check fwd: a => not not a proof enter premise(not a => False) -- using "intro" enter -- a, not a : False premise(a, not a) end bwd: not not a => a proof enter premise(not a => False) -- using "indirect" enter -- not not a, not a: False premise(not a, not not a) end equiv: a = not not a end

The proofs are not difficult. But it is worthwhile to go through some of them

step by step. In order to prove “a => not not a” we issue “enter” which leads

to the state

a : not not a

with the current goal “not not a”. I.e. we want to prove that “not a” is

wrong. In order to do this we use the axiom “intro” and assume that “not a”

leads to “False”. After the next “enter” we reach

a, not a: False

i.e. we have to prove “False” using the assumptions. From the axiom “elim” we

know that we can prove “False” if we have some contradiction. In the

assumptions we have already the contradiction “a” and “not a”. Therefore the

command “premise(a, not a)” leads to the state

a, not a: a, not a

Both goals are discharged automatically by the proof engine using implicitely

two removes.

The proof of “not not a => a” has the same structure. It uses the axiom

“indirect” instead of the axiom “intro”.

After having a proof for “a => not not a” and “not not a => a” the proof

engine can derive a proof of “a = not not a” automatically.

# The command “contradiction”

Proofs by contradiction usually have a certain pattern. The current goal is

transformed into an implication with “False” on the right hand side by using

either the “intro” or the “indirect” axiom. Then the assumption on the left

hand side of the implication is shifted onto the assumption stack. Then the

current goal “False” is proved by some contradiction using the axiom “elim”.

The command “contradiction” is introduced to give a shorthand for this pattern

and enhance the readability of proofs by contradiction.

-- shorthand for -- state before: ... : not x ... contradiction(y) premise(x=>False) enter premise(y,not y) -- state after: ... x: y, not y ... -- state before: ... : x ... contradiction(y) premise(not x=>False) enter premise(y,not y) -- state after: ... not x: y, not y ...

We can redo the proofs of double negation using the command “contradiction”.

all(a:BOOLEAN) check a => not not a proof enter; contradiction(a) end not not a => a proof enter; contradiction(not a) end a = not not a end

The proofs are more concise and communicate better the proof idea.

Since “contradiction” uses only the basic commands “premise” and “enter” it is

like “case_split” (see previous blog entry) a convenience command.

We can use the command “contradicton” to prove that (a and not a) is not

valid.

all(a:BOOLEAN) check contradiction: not (a and not a) proof contradiction(a) premise(a and not a); remove premise(a and not a); remove end end

# Some more proofs

## Quodlibet

If we start reasoning we should not make false assumptions, because with false

assumptions everything breaks down. The corresponding laws of logic tells us

that “from a false assumptions follows everything” (or in latin “ex falso

quodlibet”) and that “from a contradiction follows everything” (in latin “ex

contradictio quodlibet”).

We can prove these two laws with the proof engine by issuing some simple

commands.

all(a,b:BOOLEAN) check ex_falso: False => a proof enter; premise(not a => False); enter; remove end ex_contradictio: a => not a => b proof enter(2); premise(False); premise(a,not a); remove(2) end end

Note how the second proof uses the already proved assertion “ex_falso” with

the command “premise(False)”. We could have proved the assertion

“ex_contradictio” directly like

a => not a => b proof enter(2) premise(not b => False) enter premise(a, not a) remove(2) end

This proof is just one command longer than the above given proof. Therefore we

have not gained a lot in the first proof by using “ex_falso”. But you should

keep in mind that the proof engine allows us to modularize our proofs. We can

first proof simpler assertions and combine them to proof more complex

assertions.

## Contrapositive

Let’s assume that “a=>b” is a valid assumption, i.e. “a” is stronger than

“b”. If we know additionally that “b” is not true, we conclude that “a” cannot

be true either. Why? If “a” were true, then “b” must be true as well which

contradicts the fact that “b” is false.

This line or reasoning is used to prove the four possible contrapositive laws

of implication.

all(a,b:BOOLEAN) check contra1: (a=>b) => not b => not a proof enter(2); contradiction(b) -- a=>b, not b, a : b, not b end contra2: (not a => not b) => b => a proof enter(2); contradiction(b) -- not a => not b, b, not a : b, not b end contra3: (a => not b) => b => not a proof enter(2); contradiction(b) -- a => not b, b, a : b, not b end contra4: (not a => b) => not b => a proof enter(2); contradiction(b) -- not a => b, not b, not a : b, not b premise(not a) end end

## De Morgan

There are two “De Morgan” laws in logic. One for the operator “or” and one

for the operator “and”.

all(a,b:BOOLEAN) check de_morgan_or: not (a or b) = not a and not b de_morgan_and: not (a and b) = not a or not b end

Our intuition tells us, that these laws are valid.

The expression “a or b” can only be false if both “a” and “b” are

false. Otherwise “a or b” would be true.

The expression “a and b” is false, if “a” or “b” is false. If both are true,

“a and b” is true and therefore cannot be false. In the following we use the

proof engine to verify the assertions.

The reader is encouraged to try to proof De Morgan’s laws before reading

further.

The first trials to proof De Morgan’s laws usually end up with some

complicated looking proofs. In the following some basic techniques are

explained to keep the proofs simple and readable.

Before trying to proof De Morgan’s laws let us analyze the structure of the

laws. The laws are boolean equivalences. Therefore it is necessary to prove

the forward and the backward direction. It is convenient to state the forward

and backward direction as separate assertions, because the proof engine can

proof an equivalence automatically using an implicit “resolve” if the forward

and backward direction is given. Therefore we state

fwd: not (a or b) => not a and not b bwd: not a and not b => not (a or b)

The forward direction has an expression of the form “x and y” on the right

hand side of an implication. The usual command sequence “enter; premise(x,y)”

enter a state where we have the goals “not a” and “not b” as two separate

goals still to be proved. Both must follow from the assumption “not (a or

b)”. Why not state them as separate assertions?

lemma1: not (a or b) => not a lemma2: not (a or b) => not b

If we analyze the structure we see that both lemmas fit the pattern “not x =>

not y”. In the previous chapter “contrapositive” we have already proved

“(y=>x) => (not x => not y)” (parentheses around the last implication are not

necessary, but have been inserted to see the structure better). I.e. we can

apply the command “premise(a => a or b)” to the first lemma which leaves us

with a trivial goal on the goal stack.

Since the command “premise(a => a or b)” transforms the current goal “not (a

or b) => not a” into a simpler one, the proof engine will issue this command

automatically. I.e. no explicit proof is necessary for “lemma1”. The same

reasoning applies to “lemma2”.

Having “lemma1” and “lemma2” let the proof engine proof “fwd” automatically as

well. The commands “enter; premise(not a, not b); remove(2)” will be issued

by the implicit resolve command.

Now let us look at the backward direction

bwd: not a and not b => not (a or b)

This assertion has the structure “x and y => z”. From the previous blog entry

we have already proved that this follows from “x=>y=>z”. We can state the

backward direction in the curried form as another lemma and prove it.

lemma3: not a => not b => not (a or b) proof enter(2); premise(a or b => False); enter -- not a, not b, a or b : False case_split(a,b) enter; premise(a, not a); remove(2) enter; premise(b, not b); remove(2) end

This is the only necessary explicit proof. The following code is sufficient to

proof De Morgan’s law for “or”.

de_morgan_or: all(a,b:BOOLEAN) check lemma1: not (a or b) => not a lemma2: not (a or b) => not b fwd: not (a or b) => not a and not b lemma3: not a => not b => not (a or b) proof enter(2); premise(a or b => False); enter -- not a, not b, a or b : False case_split(a,b) enter; premise(a, not a); remove(2) enter; premise(b, not b); remove(2) end bwd: not a and not b => not (a or b) law: not (a or b) = (not a and not b) end

I have to admit that all my first proofs of this law have been much more

complicated. This happened because I did not analyze the structure of the

assertions and I did not use the previously proved assertions. It takes some

time improve this skill, but it pays off as you see above.

The possibilities of the (implicit) command “resolve” are not very

powerful. There are other theorem provers with much more sophisticated search

strategies to find a proof for a theorem. However even the limited automation

features of “resolve” might sometimes surprise.

If you write the proofs in a way which uses fully the capabilities of

“resolve” your reader of your proofs might not be able to follow your line of

reasoning. Therefore it might be useful to write more explicit proof commands

instead of letting the proof engine derive them. It is a matter of taste how

much proof commands you write. But it is a good guideline to code the proof

explicitely until the remaining steps are really trivial.

Therefore I would prefer to make the first step to proof “lemma1” and “lemma2”

explicit.

de_morgan_or: all(a,b:BOOLEAN) check lemma1: not (a or b) => not a proof premise(a => a or b) end lemma2: not (a or b) => not b proof premise(b => a or b) end ... -- other assertions as before end

The following code snippet gives a proof for the second of De Morgan’s

laws. It uses just one lemma to keep the proofs compact. The proofs make some

steps explicit which could be done by the proof engine automatically. The

reader is encouraged to find out the commands which could have been derived

automatically.

de_morgan_and: all(a,b:BOOLEAN) check lemma: not not a and not not b => a and b proof premise(not not a => not not b => a and b) enter(2) premise(a,b) -- not not a, not not b: a, b premise(not not a); remove premise(not not b); remove end fwd: not (a and b) => not a or not b proof premise(not (not a or not b) => a and b) enter premise(not not a and not not b) premise(not (not a or not b)) remove end bwd: not a or not b => not (a and b) proof premise(a and b => not (not a or not b)) premise(a => b => not (not a or not b)) enter(2) -- a, b : not (not a or not b) premise(not not a and not not b) end law: not (a and b) = (not a or not b) end

## Excluded middle

For completeness we add a proof of the “excluded middle”.

all(a:BOOLEAN) check a or not a proof contradiction(not a) -- not (a or not a) : not a, not not a premise(not (a or not a)); remove premise(not (a or not a)); remove end end

# Summary

This and the previous blog entry have been dedicated to the propositional

calculus. It has been shown how the proof engine can be used to proof all

basic laws of logic.

This is possible with a few axioms introduced in the basic operations for

conjunction, disjunction, equality and negation and just a handful of proof

commands with their corresponding rules.

-- basic commands remove -- remove the current goal premise(p1,p2,...) -- substitute the current goal by the set p1, p2, ... enter -- shift an assumption onto the assumption stack -- convenience commands case_split(a,b) -- use a case split where "a or b" must be valid contradiction(a) -- show that the negation of the current goal leads -- to the contradiction "a and not a" -- automation resolve -- issue the commands "remove", "enter", "premise" -- repeatedly as long the goal does not get more -- complicated (depth of the expression tree)

But propositional calculus is not sufficient for computer programs. Computer

programs shall do some useful calculations and execute some useful actions. In

the following blog entries more calculations will be introduced hand in hand

with the appropriate verification techniques.