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

About these ads
  1. Leave a comment

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

Join 34 other followers

%d bloggers like this: