SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/negation

Negation and proofs by contradiction

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 "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 prove "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" the 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.

Emacs suffix

 Local Variables: 
 mode: outline
 coding: iso-latin-1
 outline-regexp: "=\\(=\\)*"
 End:
Table of contents

- Introduction

- Negation and its axioms

- Double negation

- The command "contradiction"

- Some more proofs

- Quodlibet

- Contrapositive

- De Morgan

- Excluded middle

- Summary

- Emacs suffix


ip-location