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