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 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
variable 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:

– After entering the implication we have to prove “not some(x:G) e”. We prove
this by contradition, i.e. we use the general law “(a=>False) => not a”. With
one enter step we have “some(x:G) e” amongst the assumptions and have to prove
the goal “False”. We can prove this by deriving a contradiction from the
assumptions.

– Having “some(x:G) e” amongst the assumptions gives the opportunitiy to
exploit the elimination rule “exist_elim”. We use this rule by a premise
command.

– The first premise is “some(x:G) e” which can be removed immediately (it is
identical to an assumption).

– The left hand side of the second premise “all(w:G) e[x:=w] => False” can be
entered onto the assumption stack. This puts “e” onto the assumptions. Since
we have already “all(x:G) not e” on the assumption stack the contradiction is
obvious.

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” amongst 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 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 amongst 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

– Introduction to the proof engine

– Proofs by contradiction

– This article

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.

Advertisements
  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

%d bloggers like this: