SourceForge.net LogoThe Eiffel Compiler / Interpreter (tecomp)

doc/papers/proof/quantified

Quantified expressions

Introduction

This article describes the use of quantified expressions and laws for quantified expressions. All the axioms and proved assertion belong to the class BOOLEAN, because only pure logic is involved.

Quantified expressions model some logic which is deeply rooted in our thinking. A universal quantification and its consequence can be expressed in the form of syllogisms.

  "All humans are mortal."         all(x:HUMAN) x.is_mortal
 
  "Sokrates is a human."           sokrates:HUMAN
 
  -- therefore
 
  "Sokrates is mortal."            sokrates.is_mortal  
 

A similar example can be stated to express existential quantification.

  "Sokrates is mortal."                      sokrates.is_mortal
 
  -- therefore
 
  "There exists a human which is mortal."    some(x:HUMAN) x.is_mortal
 

We are able to reason with existential and universal quantification like

  -- If
  "There is a human which is mortal"        some(x:HUMAN) x.is_mortal
  -- and
  "All mortal humans are not eternal"       all(x:HUMAN) x.is_mortal 
                                                         => not x.is_eternal
  -- then
  "There is a human which is not eternal"   some(x:HUMAN) not x.is_eternal
 

Another form of reasoning is quite common

  -- If
  "Not all cats are black"                not all(c:CAT) c.is_black
  -- Then
  "There is some cat which is not black"  some(c:CAT) not c.is_black
 
  -- If
  "All cats have four legs"               all(c:CAT) c.leg_count=4
  -- Then
  "There is no cat with not four legs"    not some(c:CAT) not (c.leg_count=4)
 

The formalization of the above examples leads to predicate logic with quantified expressions. The following chapters give the basic rules, the axioms and some usful laws to deal with quantified expressions within programs.

General rules

Quantified expressions have the general form

  all(x:T) e
 
  some(x:T) e
 

with the semantics that all objects of a certain type satisfy a certain property or there exists some object of a certain type which satisfies a certain property.

The variable "x" is called a bound variable, because it is valid only in the context of the quantified expression. The expression "e" usually contains the bound variable.

The name of the bound variable is not relevant. We can choose any name. However if we choose another name, we have to use the other name in the expression e as well.

  (all(x:T) e)  =  all(y:T) e[x:=y]
 
  (some(x:T) e) =  some(y:T) e[x:=y]
 

Note the need of parentheses in the above expressions because a quantified expression spans to the right as far as possible.

It is necessary that the renaming does not change the semantics of the expression. If the variable "y" already occurs within "e" then the above renaming is invalid. I.e. the renamed variable must be a fresh variable (a name which does not yet occur within the expression).

Valid assertions of the form

  all(x:T) e
 

can be used to generate valid expressions by substituting the bound variable "x" by any expression of type "T". Suppose we have the general law

  law: all(a,b:BOOLEAN) a => b => a and b
 

and we are in a context where "i" and "j" are variables of type NATURAL. Then we can use the above law to generate the valid assertion

  ass: i<=j => i/=j => i<=j and i/=j
 

We have generated this valid assertion by the substitution

  (a => b => a and b)[a,b:=i<=j,i/=j]
 

We say that the assertion "ass" matches the assertion "law". In general we say that an assertion "p" matches another assertion "q" if both assertions are identical or if "q" is a quantifed expression with the universal quantifier and there is a valid substitution for the bound variables of "q" which converts the expression within "q" into "p".

Substitutions

The expression

  e[x,y,...:=xexp,yexp,...]
 

Is the expression "e" where all free ocurrences of "x,y,..." have been substituted by "xexp,yexp,...". The substitution is defined recursively by

  -- x,y:   variables
  -- a,b:   arbitrary expressions
  -- unop:  a unary operator
  -- binop: a binary operator
  -- f:     n-ary function
 
  x[x:=xexp]           =    xexp
  y[x:=xexp]           =    y[x:=exp]
  (unop a)[x:=xexp]    =    unop a[x:=xexp]
  (a binop b)[x:=xexp] =    a[x:=xexp] binop b[x:=xexp]
  f(a,b,...)[x:=xexp]  =    f(a[x:=xexp],b[x:=xexp],...)
 

Rule: The substitution "e[x,y,...:=xexp,yexp,...] is valid if and only if all variable occurring within "xexp,yexp,..." are not bound within "e". I.e. free variables must remain free and not captured within some internal scope.

Generic assertions

Like generic classes, assertions can be generic as well. E.g. we can have

  all[G](x:G) e
 
  all[G] some(x:G) e
 

which means that the assertions must be valid for any type "G". It is possible to constrain the types with

  all[G:COMPARABLE](x:G) e
 
  all[G:COMPARABLE] some(x:G) e
 

with the meaning

  "type G is COMPARABLE" => "x is of type G" => e
 
  "type G is COMPARABLE" => "there is some x of type G which satisfies e"
 

We can also write

  some[G](x:G) e
 

with the obvious meaning

  "There exists some type G and some x of type G which satisfies e"
 

Laws for the universal quantifier

The expression

  all(x:X; y:Y) e
 

is a shorthand for

  all(x:X) all(y:Y) e
 

Our intiuition tells us that we can exchange the universal quanitifiers. We can prove this by

  (all(x:X) all(y:Y) e) => (all(y:Y) all(x:X) e)
    proof
      enter(3)
      -- all(x:X) all(y:Y) e
      -- y:Y
      -- x:X
      -- ===================
      -- e
      remove
    end
 

Since the proof contains just trivial steps the proof engine can proof this assertion automatically.

The universal quantifier distributes over "and".

  all[G](a,b:BOOLEAN) check
    (all(x:G) a and b) => all(x:G) a
      proof
        enter(2)
        premise(a and b)
        remove
      end
 
    (all(x:G) a and b) => all(x:G) b
      proof
        enter(2); premise(a and b); remove
      end
 
    (all(x:G) a) => (all(x:G) b) => all(x:G) a and b
      proof
        enter(3)
        premise(a,b)
        remove(2)
      end
 
    (all(x:G) a and b) = ((all(x:G) a) and (all(x:G) b))
      proof resolve end
  end
 

Existential quantification

Existential quantification is a general disjunction. Suppose there are objects "o1", "o2", "o3", of type T then we define "some(x) e" by

  (some(x:T) e) =  (e[x:=o1] or e[x:=o2] or e[x:o3] or ... )
 

How can we proof an existentially quantified assertion? Let us first ask: How do we proof a disjunction "a or b"? We prove "a or b" if we proof one of them. This is expressed in the two introduction rules of "or" (see article "Introduction into the proof engine"):

  all(a,b:BOOLEAN) check
    or_intro1: a => a or b
    or_intro2: b => a or b
  end
 

The existential quantifier has a similar introduction rule (which is an axiom).

  exist_intro:
  all[G](e:BOOLEAN)
     all(w:G) e[x:=w] => some(x:G) e
  proof axiom end
 

I.e. we can prove an existentially quantified expression if we find a witness for the bound variable. We can choose any witness we like, but we have to find one. The rule says: If we are in a context in which we have an expression "w" of type G which satisfies "e[x:=w"]" then we can conclude "some(x:G) e".

The introduction rule allows us to prove a goal which is an existentially quantified expression. But we need the other way round as well. We need to infer something from an assumption which is an existentially quantified expression. For "or" we have the elimination rule

  all(a,b,g: BOOLEAN)
    or_elim: a or b => (a=>g) => (b=>g) => g
 

This rule says that in order to prove a goal "g" in a context in which "a or b" is true, it is sufficient to prove that the goal is a consequence of "a" and a consequence of "b". This rule allows us to make case split. If we know that "a or b" is true we prove the goal under both cases. We assume "a" and prove the goal and we assume "b" and prove the goal.

For existential quantification we have a similar elimination rule.

  exist_elim: 
  all[G](e:BOOLEAN)
     some(x:G) e => (all(x:G) e => g) => g
  proof axiom end
 

I.e. if we know that there is some "x" satisfying "e" and if all "x" which satisify "e" imply that g is valid, then we can conclude the validity of "g".

Since an existentially quantified expression is a generalized disjunction we expect that "exists" distributes over "or", i.e. we expect

  all[G](a,b:BOOLEAN) check
    (some(x:G) a) => (some(x:G) a or b)
    (some(x:G) b) => (some(x:G) a or b)
    (some(x:G) a or b) => (some(x:G) a) or (some(x:G) b)
  end
 

to be valid.

We can prove these laws by

  all[G](a,b:BOOLEAN) check
    (some(x:G) a) => (some(x:G) a or b)
      proof
        enter
        premise(
          some(x:G) a,
          all(w:G)  a[x:=w] => some(x:G) a or b)
        remove
        enter(2)
        premise(a[x:=w] or b[x:=w])
        premise(a[x:=w])
        remove
      end
 
    (some(x:G) b) => (some(x:G) a or b)
      proof
        -- similar to the previous proof
      end
 
    (some(x:G) a or b) => (some(x:G) a) or (some(x:G) b)
      proof
        enter
        premise(
          some(x:G) a or b,
          all(w:G) a[x:=w] or b[x:=w] => (some(x:G) a) or (some(x:G) b)
        )
        remove
        enter(2)
        case_split(a[x:=w], b[x:=w])
        enter; premise(some(x:G) a); premise(a[x:=w]); remove
        enter; premise(some(x:G) b); premise(b[x:=w]); remove
      end
  end
 

For all three proves we can shift an existentially quantified expression onto the assumption stack and use the elimination rule "exist_elim". The first two proofs continue with the rule "or_intro" and the third with "or_elim" (i.e. a case split).

Laws for quantified expressions

De Morgan

The universal and the existential quantifier are interrelated. If we say that all objects do not satisfy a certain property we conclude that there is no object which satisfies this property. Furthermore if there is an object which does not satisfy a property we conclude that not all objects can satisfy this property.

The corresponding laws are similar to the de Morgan laws for "and" and "or". We expect the following assertions to be valid.

  all[G](e:BOOLEAN) check
    (all(x:G) not e)   =>  not some(x:G) e
    (not some(x:G) e)  =>  all(x:G) not e 
 
    (some(x:G) not e)  =>  not all(x:G) e
    (not all(x:G) e)   =>  some(x:G) not e
 
    (all(x:G) not e)   =   (not some(x:G) e)
    (some(x:G) not e)  =   (not all(x:G) e)
  end
 

The first one is proved by

  all[G](e:BOOLEAN) check
     (all(x:G) not e) => not some(x:G) e
     proof
       enter
       premise((some(x:G) e) => False)  -- proof by contradiction
       enter
       premise(some(x:G) e,             -- elimination rule for "exists"
               all(w:G) e[x:=w] => False )  -- rename bound variable
       remove
       enter(2)
       premise(e[x:=w], not e[x:=w])
       -- all(x:G) not e
       -- some(x:G) e
       -- w:G
       -- e[w:=a]
       -- =================
       -- e[x:=w]
       -- not e[x:=w]
       remove(2)
     end
  end
 

The line of reasoning is the following:

The second assertion is the first one flipped. It is proved by

  all[G](e:BOOLEAN) check
    (not some(x:G) e) => all(x:G) not e
    proof
      rewrite(all(x:G) e, all(w:G) e[x:=w]) -- rename
      enter(2)
      contradiction(some(x:G) e)
      -- not some(x:G) e
      -- w:G
      -- e[x:=w]
      -- ================
      -- some(x:G) e
      -- not some(x:G) e
      premise(e[x:=w]); remove
      remove
    end
  end
 

By entering two assumptions we put "not e" onto the goal stack. Using a proof by contradiction we assume the opposite. Having "e" among the assumptions we can prove "some(x:G) e". We can prove "not some(x:G) e" as well, because it is already on the assumption stack. Note how the introduction rule "exist_intro"

  exist_intro:
  all[G](e:BOOLEAN)
    all(a:G) e[x:=a] => some(x:G) e
 

has been used to prove "some(x:G) e".

The remaining third and forth implication are proved by

  all[G](e:BOOLEAN) check
    (some(x:G) not e) => not all(x:G) e
      proof
        premise((all(x:G) e) => not some(x:G) not e)
        rewrite(all(x:G) e, all(x:G) not not e)
        remove
      end
 
    (not all(x:G) e) => some(x:G) not e
      proof
        premise((not some(x:G) not e) => all(x:G) e)
        rewrite(all(x:G) e, all(x:G) not not e)
        remove
      end
  end
 

These two proofs use the laws of contraposition

  all(a,b:BOOLEAN) check
    (a => not b) => (b => not a)
    (not a => b) => (not b => a)
  end
 

and the law of double negation to transform the assertion into a form equivalent to one of the first two assertions.

With the first four implications the equivalences are trivially valid.

Reversal of the universal and existential quantifier

Can we flip the existential and the universal quanitifier? In one direction yes, in the other not. The valid direction is

  all[X,Y](e:BOOLEAN)
    (some(y:Y) all(x:X) e)  => all(x:X) some(y:Y) e
 

I.e. if there is a "y" such that for all "x" the assertion "e" is valid then for all "x" there is a "y" such that "e" is valid. The reverse is not true. Let's assume that "e" is "x has mother y". Certainly everybody has a mother. Therefore "all(x) some(y) e" is valid. But there is no single "y" which is mother for all "x", i.e. "some(y) all(x) e" is not valid.

The valid direction is proved by

  all[X,Y](e:BOOLEAN) check
    (some(y:Y) all(x:X) e)  => all(x:X) some(y:Y) e
    proof
      enter(2)
      premise(
        some(y:Y) all(x:X) e,
        (all(b:Y) all(a:X) e[x,y:=a,b] => all(x:X) some(y:Y) e
      )
      remove
      enter_all
      -- some(y:Y) all(x:X) e
      -- b:Y
      -- a:X
      -- e[a,b:=x,y]
      -- x:X
      -- ============
      -- some(y:Y) e
      premise(e[a,b:=x,y])
      remove
    end
  end
 

After the first enter command we reach the state

  some(y:Y) all(x:X) e
  x:X
  -----------------------
  some(y:Y) e
 

We have an existential quantified expression among the assumptions. Therefore the elimination rule "exist_elim" is applicable. In the above proof we have used some renaming of the bound variables to avoid confusion.

Summary

This article completes the rules of logic used by the programming language Modern Eiffel.

To have the complete set of the rules of logic please read the articles

The previous article has already introduced reasoning with inductive types with some very primitive examples.

The following articles will concentrate more on data types and computation.

Emacs suffix

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

- Introduction

- General rules

- Substitutions

- Generic assertions

- Laws for the universal quantifier

- Existential quantification

- Laws for quantified expressions

- De Morgan

- Reversal of the universal and existential quantifier

- Summary

- Emacs suffix


ip-location