Logic as a Tool: Quantification with David Gries
Logic as a tool: Quantification
David Gries
Professor Emeritus
Computer Science, Cornell
Based on an in-progress revision of
A Logical Approach to Discrete Math
by Gries and Schneider
1
Note: This is a workshop, and not a full-fledged class. We touch on
the highlights, but the slides contain a lot more information
When I teach a course on discrete structures, I spend:
1. 6-7 1-hour lectures on propositional logic
2. 6 1-hour lectures on quantification (predicate logic)
Between lectures, students have homework. They end up proving
50-60 theorems of logic and gain real understanding and a skill in
syntactic calculation. One could call it fluency in developing proofs.
2
Quantification
Provide a single uniform notation for all quantifications, unifying
what has been confusion. Scope, dummy, bound variable, free or
bound occurrence of a variable, etc. can be discussed in a single
setting
i=1
9
i*i
i . 0 ≠ i
i
2
> 0
(for all)
i . 0 ≠ i
i
2
> 0
(exists)
Provide axioms and theorems for manipulating quantifications.
This will give you basic information, which has been missing from
your mathematics education until now
3
Notation for Quantification
Mathematical convention
Our notation
i=1
9
i*i
(+ i | 1 ≤ i ≤ 9: i*i)
i=1
9
i*i
(* i | 1 ≤ i ≤ 9: i*i)
i . 0 ≠ i
i
2
> 0
(
i
| 0 ≠ i: i
2
> 0)
i . 0 ≠ i
i
2
> 0
(
i
| 0 ≠ i: i
2
> 0)
4
Dummy sometimes called the bound
variable
How to evaluate
(+ i | 1 ≤ i ≤ 4: i*i)
1. Write down values
i
in the range
1 ≤ i ≤ 4
:
1, 2, 3, 4
2. Write down the values of the body,
i*i
, one for each possible
value of i in the range:
1, 4, 9, 16
3. Put the operator
+
between each pair of values:
1 + 4 + 9 + 16
4. Evaluate the expression
: 30
5
How to evaluate (
i | –1 ≤ i ≤ 2: i
2
> 0)
1. Write down values
i
in the range
–1 ≤ i ≤ 2
:
-
1, 0, 1, 2
2. Write down the values of the body,
i
2
> 0
, one for each
possible value of i in the range:
1
> 0, 0 > 0, 1 > 0, 2 > 0
3. Put the operator
between each pair of values:
1
> 0
0 > 0
1 > 0
2 > 0
4. Evaluate the expression
: false
6
What operators are allowed in a quantification?
(
o
i | range : body)
Operator
o
can be any operator that is associative and
symmetric. If a range of false comes into play, it also needs an
Identity.
(gcd i | 1 ≤ i ≤ 9: i*i)
(greatest common divisor)
(
i | 1 ≤ i ≤ 9: i*i)
(minimum)
(
i | 1 ≤ i ≤ 9: I > 0)
(equivales)
7
General form of Quantification
(
o
i:t | range : E)
Value:
E[i:= v0]
o
E[i:= v1]
o
E[i:= v2]
o
…
where
{v0, v1, v2, …} is the set of values
for which R is true.
(
o
i |: E)
is abbreviation for
(
o
i | true: E)
Examples of quantifications with types
(
+
i:int | 1 ≤ i ≤ 2: i*i) = 1 + 4
(
+
i:real | 1 ≤ i ≤ 2: i*i) is undefined
8
o
:
operator
i
:
dummy
(bound variable)
t
:
type of dummy
(often omitted)
R
:
range
E
:
body
Scope, bound variables, free variables
(
o
i:t | R: P)
Scope of dummy
i
is
R
and
P
Scope rules for dummy similar to rules for local variable of a
procedure
public
void
p(
int
x) {int
k; k= x+x; k= 2; }
Scope of local variable
k
is procedure body. Any occurrence
of
k
outside procedure body refers to entirely different entity,
which just happens to have same name. In same way, scope of
i
in
(
o
i | R: P)
is
R
and
P
. An occurrence of
i
outside this expression refers to an
entirely different entity
9
Scope, bound variables, free variables
Occurrence of
v
is
bound
in an exp iff it is in the scope of dummy
v
. It is bound to nearest such dummy.
Occurrence of
v
is
free
if it is not bound.
occurs(“v”, “E”)
means that at least one variable in list
v
of
variables occurs free in at least one exp in exp list
E
.
Occurrences of a var in an exp without quantifications are free
i > 0
(
i | 0 ≤ i: x * i = 0)
10
Free. Gets value from state
Bound to dummy i
Translating English into Quantifications
Canonical English phrase for a quantification indicates operator,
names dummies, makes explicit range and body
Sum over k of k*k for k in range 1..10
(+k | 1 ≤ k ≤ 10: k * k)
Product over j of 2*j for even integers j between 0 and 10
(*j | even.j and 0 ≤ j ≤ 10: 2*j)
Minimum value over all j of j
3
– j
2
(
j | true: j
3
– j
2
)
Conjunction of even.j for positive
j
(
j | 0 < j: even.j)
For every odd integer k, 3*k is odd
(
k | odd.k: odd(3*k))
There exist two positive integers i and j whose sum is negative
(
i,
j | 0 < i
0 < j: i + j < 0)
11
It helps to put phrases in canonical form
Example
sum of the square of the odd positive integers
that are less than 50.
Dummy is not explicit so reword
sum of i*i for i an odd positive integer that
is less than 50
Now formalize
(+ i | odd.i
0 < i ≤ 50: i*i)
12
Universal Quantification
is associative and symmetric; can use in quantification
(
i | 1 ≤ i < 4: i < i
2
) (
i | 1 ≤ i < 4: i < i
2
)
is equivalent to
1 < 1
2
2
< 2
2
3
< 3
2
(false)
so it is true iff all conjuncts are true. Hence, read as
For all i such that i is in 1..3, i is less than i squared
Other words that signal universal quantification:
Every all for all for each any
13
Formalizing English statements
St
rategy
: If a phrase is to be formalized as universal
quantification, first put it in canonical form
For all i, [describe range of i], … holds
Sentence
: x is less than every positive integer
Canonical form
: For all i, i a positive integer, x < i
Formalization
:
(
i | i > 0: x < i)
Sentence
: Even integers are red
Canonical form
: For all integers k, where k is even, k is red
Formalization
:
(
k | even.k: k is red)
Sentence
: Paragraphs have at least two sentences
Canonical form
: For every paragraph p, p has at least two
sentences
Formalization
:
(
p:para : p has at least two sentences)
14
Convention
Convention
: Free variables in a theorem are considered to be
implicitly universally quantified
Example
:
red.x
If no particular state is implied by the discussion, the meaning is
that every value
x
satisfies
red.x
, i.e.
(
x |: red.x)
Example: Red numbers are pretty
15
Existential Quantification
is associative and symmetric; can use in quantification
(
i | 1 ≤ i < 4: i < i
2
) (
i | 1 ≤ i < 4: i
2
)
is equivalent to
1 < 1
2
2
< 2
2
3
< 3
2
(false)
so it is true (at least) if one disjunct is true —if
there exists
an
integer
i
in range 1..3 such that
i
2
Existential quantifications are signaled by
exists some there are there is at least one
16
Formalizing English statements
Strategy
: If a phrase is to be formalized as an existential
quantification, put it in canonical form:
There exist i, [describe range of i], such that … holds
Sentence
: Some even integer is green
Canonical form
: There is an i that is even such that i is green
Formalization:
(
i
| even.i: i is red)
Sentence
: At least one chapter has an even number of pages
Canonical
form
:There exists a chapter c such
that c has an even number of pages
Formalization
:
(
i:chap
|: even(c.size))
17
What is negation of
All integers are even
Not:
All integers are not even
but:
Not (all integers are even)
which is:
Some integer is not even
Not (all integers are even)
=
<Formalize using quantification>
!(
z |: even.z)
=
<Rewrite as a long conjunction>
!(…
even(–1)
even.0
even.1
even.2
…)
=
<De Morgan (9.23c)>
(…
!even(–1)
!even.0
!even.1
! even.2
…)
=
<Rewrite using using quantification>
(
z |: ! even.z)
=
<Return to English>
Some integer is not even
Negation and
Quantification
18
Take care with formalizations
Define
:
mother(m, c)
: “m is c’s mother”
English
: Every child has a mother
Canonical form
: For every child c, there is a mother for c
Formalization
:
(
c |: (
m |: mother(m, c)))
English
: There is a mother for every child
Canonical form
: There exists a mother m such that for every
child c, m is c’s mother
Formalization
:
(
m |: (
c |: mother(m, c)))
Means that there is one mother who is the mother of all!
Not what is meant! Probably meant: Every child has a mother
19
Divide and Conquer
Sentence too long/complicated to formalize in one step? Do it in
several steps
English
: An even integer is smaller than some odd integer
Canonical form
: For every even integer i, i is smaller
than some odd integer
Formalize
:
(
i| even.i:
i is smaller than some odd integer
)
Work on body
: i is smaller than some odd integer
Canonical fo
rm: There exists an odd integer j such that i < j
Formalize
:
(
j| odd.j: i < j)
Final form
:
(
i| even.i: (
j| odd.j: i < j))
20
Contextual Substitution Revisited
(
o
x | R: P) E[v:= P]
requires different definition because quantifications introduce
local variables.
Contextual substitution in a quantification:
If y does not occur free in v or F
(
o
y | R: P)[v:= F] = (
o
y | R[v:= F]: P[v:= F])
If y does occur free in v or F, let z be a fresh variable (it does not
occur free in v, R, P, or F). Then
(
o
y | R: P) [v:= F] = (
o
z | R[y:= z][v:= F] : P[y:= z][v:= F])
21
Examples of contextual substitution
(+ x | x
1..2:
y)[y:= y+z] = (+ x | x
1..2:
y+z)
(
i | i
0..n: b[i] = n)[n:= m] =
(
i | i
0..n: b[i] = m)
(
i | i
0..n: b[i] = n)[n:= i]
=
<
Change dummy
>
(
k | k
0..n: b[k] = n)[n:= i]
=
<
Contextual substitution
>
(
k | k
0..n: b[k] = i)
(
y | y
0..n: b[y] = n)[y:= m] =
(
j
| j
0..n: b[j] = n)
22
Reason for changing dummy
(
+
i | i
= n
: i) = n
Therefore
(
+
i | i
= n
: i)[n:= i] =
n
[n:= i] = i
But also, without required change in dummy, we have
(
+
i | i
= n
: i)[n:= i] =
(
+
i | i
= i
: i)
—bad substitution
Latter is undefined because all values of
i
satisfy
i = i
Correct way
(
+
i | i
= n
: i)[n:= i]
= <
Contextual substitution
>
(
+
j
| j
= n
: j)[n:= i]
= <
Definition of quantification
>
i
23
Pure Predicate Logic
Predicate logic formula
: boolean expression in which some
boolean variables may have been replaced by
•
Predicates
: calls on boolean functions whose arguments
may be of types other than boolean
Example
equal(x, x – z + z)
Example
less(x, y + z)
Function names are called
predicate symbols
Arguments are called
terms
•
Universal and existential quantification
Example
x < y
x = z
q(x, z + x)
Predicates
:
x < y, x = z, q(x, z + x)
Terms
: x, y, z, z + x
24
Pure Predicate Logic
Axioms
: Axioms of propositional logic
Axioms for
(
x | R:P)
—we will give more
Axioms for
(
x | R: P)
—we will give more
Inference rules
Leibniz (3.1)
Transitivity (3.2)
Equanimity (3.3
Leibniz for quantification (8.18)
25
Theories
In pure predicate logic, function symbols are
uninterpreted
(except for equality =). The logic provides no rules for
manipulating them. We will have general rules for manipulation
that are sound no matter what meanings are given to function
symbols
To get a
theory
: add axioms that give meaning to some
uninterpreted function symbols
Example
: Theory of integers: pure predicate logic plus axioms for
manipulating operators(i.e. functions +, –, <, <=, etc.)
Example
:
Theory of sets: add axioms for manipulating set
expressions containing operators like membership
,
union
Example
:
Joint theory of sets and integers allows reasoning
about expressions that contain both.
26
Theorems for Quantification
Theorems hold only if each quantification is well-defined and the
operator has identity
u
.
(+ i | 2 ≤ i ≤ 3: i*i) = 4 + 9
(+ i | 2 ≤ i ≤ 2: i*i) = 4
(+ i | 2 ≤ i ≤ 1: i*i) = ?
27
Answer is 0, because
the
Identity of +
is 0:
0 + x = x
(* i | 2 ≤ i ≤ 3: i*i) = 4 * 9
(* i | 2 ≤ i ≤ 2: i*i) = 4
(* i | 2 ≤ i ≤ 1: i*i) = ?
Answer is 1, because
the
Identity of *
is 1:
1 * x = x
Axioms for Quantification
(8.20) Axiom
Empty range
:
(
o
x | false: P) =
u
(+ i | false: P) = 0
(* i | false: P) = 1
(
i | false: P) = true
(
i | false: P) = false
(8.21) Axiom
Identity accumulation
:
(
o
x
| R:
u
) =
u
(
u
is the Identity of operator
o
)
28
Axioms for Quantification
(
8.22) Axiom
One-point rule
:
Provided
occurs(‘x’, ‘E’),
(
o
x | x = E: P) = P[x:= E]
Why the caveat? Consider this:
(+ i |i = i+ 1 : i) = 0
(since range is empty)
But if no caveat,
(+ i |i = i+ 1 : i) = i[i:= i+1]
, which is
i+1
Consider
(
o
x | x = E: P) = P[x:= E]
where
x
occurs free in
E
LHS has no free occurrence of
x
.
RHS has free occurrence of
x
.
How could they be equal in all states, in general?
29
Axioms for Quantification
(8.23) Axiom Distributivity:
Provided P,Q: bool or R is finite
(
o
x | R: P)
o
(
o
x | R: Q) = (
o
x | R: P
o
Q)
Example:
values of P for x
values of Q for x
satisfying R
satisfying R
2 + 5 + 8
3 + 1 + 9
2 + 3 + 5 + 1 + 8 + 9
30
Rest on fact that operator
o
is
associative and symmetric
Axioms for Quantification
(8.24) Axiom
Range Split
:
Provided P: bool or R, S finite
(
o
x | R
S
: P)
o
(o x | R
S: P) = (
o
x | R: P)
o
(o x | S: P)
Other
range split theorems
in slides giving all theorems
(8.26) Axiom Nesting: Provided not occurs(‘y’, ‘R’)
(
o
x, y | R
Q
: P) = (o x | R: (o y | S: P)
(8.29)
Dummy reorder
: (
o
x, y | R: P) = (
o
y, x | R: P)
31
Axioms for Quantification
(8.30)
Change of dummy
:
Provided
occurs(‘y’, ‘R, P’) and
f has inverse
(
o
x | R: P) = (
o
y | R[x:= f.y]: P[x:= f.y])
(8.31)
Dummy renaming
:
Provided
occurs(‘y’, ‘R, P’)
(
o
x | R: P) = (
o
y | R[x:= y]: P[x:= y])
(8.32) Split off term (example):
(
o
x | 0 ≤ i < n+1: P) = (
o
x | 0 ≤ i < n: P)
o
P[i:= n]
32
Use of Change of Dummy
(
o
x | R: P) = (
o
y | R[x:=f.y]: P[x:= f.y])
(+ x | 2 ≤ x ≤ 9: x
2
) = (+ y | 0 ≤ y ≤ 7: (y+2)
2
)
Convince yourself that this should hold
33
Use function
f.y = y + 2
f has an inverse
R is 2 ≤ x ≤ 9
R[x:= f.y]
is
2 ≤ y + 2 ≤ 9
which equals
0 ≤ y ≤ 7
P
is
x
2
P[x:= f.y]
is
(y+2)
2
Proof of Change of Dummy
The next slide contains a proof of
Change of Dummy
.
It is an
opportunity driven
proof: at each step, the shapes of the
current formula and the goal give inspiration for the step. This
makes the proof memorable.
Evidence that this proof is memorable comes from our courses.
The students were told they would have to present this proof on
a quiz. About 90 percent (out of 80–90 students) get it
completely right. We believe that this would be impossible with
an informal English proof.
34
(
o
y | R[x:= f.y]: P[x:= f.y])
start with side with structure
35
= <
One-point rule (8.22) —need quantification over x
>
(
o
y | R[x:= f.y]: (o x | x = f.y: P)
= <
Nesting (8.26) —move x to outside
>
(
o
x,y | R[x:= f.y]
x = f.y: P)
= <
Substitution (3.91) —to get ready to remove R[x ..]
>
(
o
x,y | R[x:= x]
x = f.y: P)
= <
R[x:= x] = R; Nesting (8.26) —move y inside
>
(
o
x | R: (
o
y | x = f.y: P)
= <
x = f.y
y = f
-1
.x –prepare to eliminate y
>
(
o
x | R: (
o
y | y = f
-1
.x: P)
= <
One-point rule (8.22)
>
(
o
x | R: P[y = f
-1
.x])
= <
Textual substitution –
occurs(‘y’, ‘P’)
>
(
o
x | R: P)
Head for
(
o
x | R: P)
Universal Quantification Theorems
is symmetric, is associative, and has an identity
true
Write
(
x | R: P)
or
(
x | R: P)
All axioms for quantification hold.
Additional axiom
(9.3) Axiom
over
:
Provided
occurs(‘x’, ‘P’),
P
(
x | R: Q)
(
x | R: P
Q)
Reason for caveat: ensure that LHS and RHS
have same set of free variables
Look at theorems at end for theorems for
36
Trading
Trading
: Moving a conjunct of the range to the body or vice
versa. Here are the basic Trading theorems
(9.4)
Trading
:
(
x | R: P)
(
x |: R
P)
(9.5a)
Trading
:
(
x | Q
R: P)
(
x | Q: R
P)
37
Modify Metatheorem Monotonicity
The range of a
quantification is an antimonotonic position. So
we have
(4.7)
Metatheorem Monotonicity
(see theorems)
Example of use
(
i | i = 3: i*I > 0)
<
Antimonotonicity: i = 3
i > 0
>
(
i | i > 0: i*I > 0)
38
i = 3 appears in 1 (an odd number)
antimonotonic position. So the direction
of the arrow changes.
Instantiation
(9.17)
Instantiation
:
(
x |: P)
P[x:= E]
One-point rule sharper than Instantiation. In some situations
Instantiation is useful. Like symmetry, often used implicitly.
Implicit use of Instantiation more concealed if universal
quantification itself is not written formally.
Example
Conventionally write
(9.20)
(
a,b |: a + b = b + a)
as
a + b = b + a
for all integers
a, b
Because universal quantification is a side comment and not part
of the formula, it is easy to forget that producing, say
x*y + z =
z + x* y
From (9.20) requires Instantiation
39
Metatheorem
(9.16)
Metatheorem
.
P
is a theorem iff (
x |: P) is a theorem.
Use this Metatheorem to discuss ways of stating axioms and
theorems in mathematics. Below are three different ways:
Axiom:
(
b, c: int |: b + c = c + b)
Axiom:
b + c = c + b
for integers
b, c
In this chapter,
b
and
c
have type integer
Axiom: b + c = c + b
40
Proof of Trading (9.5a)
(
x | Q
R: P)
(
x | Q: R
P)
(
x | Q
R: P)
=
<
Trading (9.4a)
>
(
x |: Q
R
P)
=
<
Shunting (3.69)
>
(
x |: Q
(
R
P))
=
<
Trading (9.4a)
>
(
x | Q:
R
P)
41
Heading for
(
x | Q: R
P)
Existential Quantification
is symmetric and associative and has a identity true
(
x | R: P)
or
(
x | R: P)
All axioms for quantification hold for
.
Additional axiom:
Axiom
Generalized De Morgan
:
(
x | R: P)
(
x | R:
P)
Idea behind generalization
P1
P2
(
P1
P2)
Generate theorems for
from theorems for
Use Unfold-fold to prove them.
42
Opportunity-driven proof
Prove (9.40), but with all ranges true:
(
x |: (
y
|: P))
(
y
|: (
x |: P))
There is a reason for each step, which is discussed in the hint.
(
x |: (
y
|: P))
43
=
<
Quantified freshy (9.9) —Universal quantification over
must appear at the outer level this gets it there.
>
(
y
|: (
x |: (
y
|: P)))
<
Monotonicity: Instantiation (9.17) —The inner
quantification over y has to be removed This does it
>
(
y
|: (
x |: P))
Using a Witness
New proof method to prove Interchange of quantifications (9.40)
with ranges true:
(
x |: (
y
|: P))
(
y
|: (
x |: P))
The antecedent indicates there exists a value for dummy
x
for
which
(
y
|: P)
holds. Give the value a name
xx
and use instead
the antecedent
(
y
|: P)[x:= xx].
Thus prove the theorem by
proving
(
y
|: P)[x:= xx]
(
y
|: (
x |: P))
(
y
|: P[x:= xx])
=
<One-point rule (8.22)>
(
y
|: (
x | x = xx: P))
<Monotonicity: x =xx
true>
(
y
|: (
x |: P))
44
Proving an Argument Sound
Socrates is human.
All humans are mortal.
Therefore some person is mortal.
45
soc
: Socrates
h.p
: person p is human
m.p
: person p is mortal
h.soc
(
p
|: h.p
m.p)
(heading for (
p |: m.p)
<
Monotonicity: Instantiation (9.13), with p:= soc
>
h.soc
(
h.soc
m.soc)
<
Modus ponens (3.77)
>
m.soc
<
-Introduction (9.28)
>
(
p |: m.p)
h.soc
(
p
|: h.p
m.p)
(
p |: m.p)
Proving an Argument Sound
All mosquitos are pests. No butterflies are pests. Therefore,
butterflies are not mosquitos.
(
c
|: m.c
p.c)
(
c
|: b.c
p.c)
(
c
| b.c:
p.c)
Motivate first step. Must weaken antecedent a
quantification
over c. First conjunct of antecedent already has this form.
Application of De Morgan to second puts second in that form.
(
c
|: m.c
p.c)
(
c
|: b.c
p.c)
=
<
DeMorgan (9.23b); DeMOrgan (3.52a)
>
(
c
|: m.c
p.c)
(
c
|:
b.c
p.c)
=
<
Distributivity (8.23)
>
(
c:
(m.c
p.c)
(
b.c
p.c))
=
<
Implication (3.65)
>
(
c:
(m.c
p.c)
(
p.c
b.c))
—you finish it
46
Mathematical Reasoning
Is there some real
x
for which
1/(x*x + 1) > 1
?
Formalized is following valid?
(
x
:real |: 1/(x*x + 1) > 1)
(
x
|: 1/(x*x + 1) > 1)
=
<
Arithmetic
>
(
x
|: 1 > x*x + 1)
=
<
Arithmetic
>
(
x
|: 0 > x*x)
=
<
x*x ≥ 0 —from theory of the reals
>
(
x
|: false)
=
<
(9.28)
>
false
47
Set Theory
View set theory as an extension of predicate logic. Add a new
type, notations for constants and operations, and axioms
Usual notations:
{x | P} set of values of
x
that satisfy predicate
P
{x*x| 0 ≤ x ≤ 100}{x*y | 0 ≤ x*y ≤ 100} what’s the dummy?
Our notation:
{x | P: x}{x | 0 ≤ x ≤ 100: x*x}{x |0 ≤ x*y ≤ 100: x*y} 48
Comprehension and enumeration
{x | P | E} the set of values of expression
E
where dummy
x
ranges over values that satisfy
P
{v0, v1, …, vn} shorthand for
{x | x = v0
x = v1
…
x = vn: x}
{1, 3, 1} = {x | x = 1
x = 3
x = 1: x} = {1, 3}49
Membership and Extensionality
(10.4) Axiom
Set membership
:
Provided not
occurs(‘x’, ‘F’),
F
{x | R: E}
(
x | R: F = E}
(10.5) Axiom
Extensionality
:
S = T
(
x |: x
S
x
T
}
Theorems
e
{x| false: E}
false
{x| false: E}
{}v
{x| x = e}
v = e
S = {x | x
S: x}
50
Proof of
S = {x | x
S: x}
According to axiom Extensionality (10.5), it suffices to prove
v
S
v
{x | x
S: x}
for arbitrary
v
. We have
v
{x | x
S: x}
=
<
Membership (10.4)
>
(
x | x
S: v = x}
=
<
Trrading (9.19), twice
>
(
x | x = v: x
S:}
=
<
One-point rule (8.22)
>
v
S
51
Definitions of some operations
(10.21) Axiom
Subset
:
S
T
(
x | x
S: x
T)
(10.26)
Axiom
Union
: w
S
T
w
S
w
T
(10.27) Axiom Intersection:
w
S
T
w
S
w
T
52
Russell’s Paradox
Suppose our theory of sets is untyped. Consider the set
S
of all
sets that do not contain themselves as elements
x
S
x
x
(
for all sets x
)
i.e.
(
x |: x
S
x
x)
53
The definition of S allows
us to prove false.
Therefore, S is not well
defined and cannot be
allowed.
We have:
(
x |: x
S
x
x)
<
Instantiation
>
S
S
S
S
=
<
(3.20)
>
false
Calculate a Generating Function
Generating function G(z) for sequence
c, c
2
, c
3
, c
4
, …
(**)
G(z) = (+ i | 1 ≤ i : c
i
* z
i
)
Is there a closed form for
G(z)
?
Cannot find by
“
intuition
”
. But can
calculate
it.
54
G(z) = (+i: 1 ≤ i: c
i
z
i
)
(**)
G(z) = (+ i | 1 ≤ i : c
i
z
i
)
55
To start, complicate
formula in some way.
= <
split off term
>
G(z) = cz + (+i: 2 ≤ i: c
i
z
i
)
Goal: make summa-
tion look like RHS of
definition of G(z)
= <
change of dummy
>
G(z) = cz + (+i: 1 ≤ i: c
i+1
z
i+1
)
= <
factor
>
G(z) = cz + cz(+i: 1 ≤ i: c
i
z
i
)
= <
Fold/unfold
>
G(z) = cz + czG(z)
= <
arithmetic
>
G(z) = cz / (1 – cz)
We used calculational logic
to
find
a theorem, not only
to proof it. The logic helps
in the creative process.
Delve into the complexities of quantification in logic with David Gries, a Professor Emeritus in Computer Science at Cornell University. Explore the nuances of quantification, discussing notation, evaluation, and permissible operators. Gain insights into foundational axioms and theorems as you develop a deep understanding of this essential logical concept.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Logic as a tool: Quantification David Gries Professor Emeritus Computer Science, Cornell Based on an in-progress revision of A Logical Approach to Discrete Math by Gries and Schneider 1
Note: This is a workshop, and not a full-fledged class. We touch on the highlights, but the slides contain a lot more information When I teach a course on discrete structures, I spend: 1. 6-7 1-hour lectures on propositional logic 2. 6 1-hour lectures on quantification (predicate logic) Between lectures, students have homework. They end up proving 50-60 theorems of logic and gain real understanding and a skill in syntactic calculation. One could call it fluency in developing proofs. 2
Quantification Provide a single uniform notation for all quantifications, unifying what has been confusion. Scope, dummy, bound variable, free or bound occurrence of a variable, etc. can be discussed in a single setting i=19 i*i i . 0 i i2 > 0 (for all) i . 0 i i2 > 0 (exists) Provide axioms and theorems for manipulating quantifications. This will give you basic information, which has been missing from your mathematics education until now 3
Notation for Quantification Mathematical convention i=19 i*i i=19 i*i i . 0 i i2 > 0 i . 0 i i2 > 0 Our notation (+ i | 1 i 9: i*i) (* i | 1 i 9: i*i) ( i | 0 i: i2 > 0) ( i | 0 i: i2 > 0) operator dummy range body Dummy sometimes called the bound variable 4
How to evaluate (+ i | 1 i 4: i*i) 1. Write down values i in the range 1 i 4: 1, 2, 3, 4 2. Write down the values of the body, i*i, one for each possible value of i in the range: 1, 4, 9, 16 3. Put the operator + between each pair of values: 1 + 4 + 9 + 16 4. Evaluate the expression: 30 5
How to evaluate ( i | 1 i 2: i2 > 0) 1. Write down values i in the range 1 i 2: 2. Write down the values of the body, i2 > 0, one for each possible value of i in the range: -1, 0, 1, 2 3. Put the operator between each pair of values: 1 > 0 0 > 0 1 > 0 2 > 0 1 > 0, 0 > 0, 1 > 0, 2 > 0 4. Evaluate the expression: false 6
What operators are allowed in a quantification? (o i | range : body) Operator o can be any operator that is associative and symmetric. If a range of false comes into play, it also needs an Identity. (gcd i | 1 i 9: i*i) ( i | 1 i 9: i*i) ( i | 1 i 9: I > 0) (greatest common divisor) (minimum) (equivales) 7
General form of Quantification o: operator i: dummy (bound variable) t: type of dummy (often omitted) R: range E: body (o i:t | range : E) Value: E[i:= v0] o E[i:= v1] o E[i:= v2] o where {v0, v1, v2, } is the set of values for which R is true. (o i |: E) is abbreviation for (o i | true: E) Examples of quantifications with types (+ i:int | 1 i 2: i*i) = 1 + 4 (+ i:real | 1 i 2: i*i) is undefined 8
Scope, bound variables, free variables (o i:t | R: P) Scope of dummy i is R and P Scope rules for dummy similar to rules for local variable of a procedure publicvoid p(int x) {int k; k= x+x; k= 2; } Scope of local variable k is procedure body. Any occurrence of k outside procedure body refers to entirely different entity, which just happens to have same name. In same way, scope of i in (o i | R: P) is R and P. An occurrence of i outside this expression refers to an entirely different entity 9
Scope, bound variables, free variables Occurrence of v is bound in an exp iff it is in the scope of dummy v. It is bound to nearest such dummy. Occurrence of v is free if it is not bound. occurs( v , E ) means that at least one variable in list v of variables occurs free in at least one exp in exp list E. Occurrences of a var in an exp without quantifications are free i > 0 ( i | 0 i: x * i = 0) Bound to dummy i Free. Gets value from state 10
Translating English into Quantifications Canonical English phrase for a quantification indicates operator, names dummies, makes explicit range and body Sum over k of k*k for k in range 1..10 (+k | 1 k 10: k * k) Product over j of 2*j for even integers j between 0 and 10 Minimum value over all j of j3 j2 (*j | even.j and 0 j 10: 2*j) ( j | true: j3 j2) ( j | 0 < j: even.j) ( k | odd.k: odd(3*k)) Conjunction of even.j for positive j For every odd integer k, 3*k is odd There exist two positive integers i and j whose sum is negative ( i,j | 0 < i 0 < j: i + j < 0) 11
It helps to put phrases in canonical form Example sum of the square of the odd positive integers that are less than 50. Dummy is not explicit so reword sum of i*i for i an odd positive integer that is less than 50 Now formalize (+ i | odd.i 0 < i 50: i*i) 12
Universal Quantification is associative and symmetric; can use in quantification ( i | 1 i < 4: i < i2) ( i | 1 i < 4: i < i2) is equivalent to 1 < 12 2 < 22 3 < 32 (false) so it is true iff all conjuncts are true. Hence, read as For all i such that i is in 1..3, i is less than i squared Other words that signal universal quantification: Every all for all for each any 13
Formalizing English statements Strategy: If a phrase is to be formalized as universal quantification, first put it in canonical form For all i, [describe range of i], holds Sentence: x is less than every positive integer Canonical form: For all i, i a positive integer, x < i Formalization: ( i | i > 0: x < i) Sentence: Even integers are red Canonical form: For all integers k, where k is even, k is red Formalization: ( k | even.k: k is red) Sentence: Paragraphs have at least two sentences Canonical form: For every paragraph p, p has at least two sentences Formalization: ( p:para : p has at least two sentences) 14
Convention Convention: Free variables in a theorem are considered to be implicitly universally quantified Example: red.x If no particular state is implied by the discussion, the meaning is that every value x satisfies red.x, i.e. ( x |: red.x) Example: Red numbers are pretty 15
Existential Quantification is associative and symmetric; can use in quantification ( i | 1 i < 4: i < i2) ( i | 1 i < 4: i2) is equivalent to 1 < 12 2 < 22 3 < 32 (false) so it is true (at least) if one disjunct is true if there exists an integer i in range 1..3 such that i2 Existential quantifications are signaled by exists some there are there is at least one 16
Formalizing English statements Strategy: If a phrase is to be formalized as an existential quantification, put it in canonical form: There exist i, [describe range of i], such that holds Sentence: Some even integer is green Canonical form: There is an i that is even such that i is green Formalization: ( i | even.i: i is red) Sentence: At least one chapter has an even number of pages Canonical form:There exists a chapter c such that c has an even number of pages Formalization: ( i:chap |: even(c.size)) 17
What is negation of All integers are even Not: All integers are not even but: Not (all integers are even) which is: Some integer is not even Negation and Quantification = = !( even( 1) even.0 even.1 even.2 ) = <De Morgan (9.23c)> ( !even( 1) !even.0 !even.1 ! even.2 ) = <Rewrite using using quantification> ( z |: ! even.z) = <Return to English> Some integer is not even Not (all integers are even) <Formalize using quantification> !( z |: even.z) <Rewrite as a long conjunction> 18
Take care with formalizations Define: mother(m, c): m is c s mother English: Every child has a mother Canonical form: For every child c, there is a mother for c Formalization: ( c |: ( m |: mother(m, c))) English: There is a mother for every child Canonical form: There exists a mother m such that for every child c, m is c s mother Formalization: ( m |: ( c |: mother(m, c))) Means that there is one mother who is the mother of all! Not what is meant! Probably meant: Every child has a mother 19
Divide and Conquer Sentence too long/complicated to formalize in one step? Do it in several steps English: An even integer is smaller than some odd integer Canonical form: For every even integer i, i is smaller than some odd integer Formalize: ( i| even.i: i is smaller than some odd integer) Work on body: i is smaller than some odd integer Canonical form: There exists an odd integer j such that i < j Formalize: ( j| odd.j: i < j) Final form: ( i| even.i: ( j| odd.j: i < j)) 20
Contextual Substitution Revisited (o x | R: P) E[v:= P] requires different definition because quantifications introduce local variables. Contextual substitution in a quantification: If y does not occur free in v or F (o y | R: P)[v:= F] = (o y | R[v:= F]: P[v:= F]) If y does occur free in v or F, let z be a fresh variable (it does not occur free in v, R, P, or F). Then (o y | R: P) [v:= F] = (o z | R[y:= z][v:= F] : P[y:= z][v:= F]) 21
Examples of contextual substitution (+ x | x 1..2: y)[y:= y+z] = (+ x | x 1..2: y+z) ( i | i 0..n: b[i] = n)[n:= m] = ( i | i 0..n: b[i] = m) ( i | i 0..n: b[i] = n)[n:= i] = <Change dummy> ( k | k 0..n: b[k] = n)[n:= i] = <Contextual substitution> ( k | k 0..n: b[k] = i) ( y | y 0..n: b[y] = n)[y:= m] = ( j | j 0..n: b[j] = n) 22
Reason for changing dummy (+i | i = n: i) = n Therefore (+i | i = n: i)[n:= i] = n[n:= i] = i But also, without required change in dummy, we have (+i | i = n: i)[n:= i] = (+i | i = i: i) bad substitution Latter is undefined because all values of i satisfy i = i Correct way (+i | i = n: i)[n:= i] = <Contextual substitution> (+j | j = n: j)[n:= i] = <Definition of quantification> i 23
Pure Predicate Logic Predicate logic formula: boolean expression in which some boolean variables may have been replaced by Predicates: calls on boolean functions whose arguments may be of types other than boolean Example equal(x, x z + z) Example less(x, y + z) Function names are called predicate symbols Arguments are called terms Universal and existential quantification Example x < y x = z q(x, z + x) Predicates: x < y, x = z, q(x, z + x) Terms: x, y, z, z + x 24
Pure Predicate Logic Axioms: Axioms of propositional logic Axioms for ( x | R:P) we will give more Axioms for ( x | R: P) we will give more Inference rules Leibniz (3.1) Transitivity (3.2) Equanimity (3.3 Leibniz for quantification (8.18) 25
Theories In pure predicate logic, function symbols are uninterpreted (except for equality =). The logic provides no rules for manipulating them. We will have general rules for manipulation that are sound no matter what meanings are given to function symbols To get a theory: add axioms that give meaning to some uninterpreted function symbols Example: Theory of integers: pure predicate logic plus axioms for manipulating operators(i.e. functions +, , <, <=, etc.) Example: Theory of sets: add axioms for manipulating set expressions containing operators like membership , union Example: Joint theory of sets and integers allows reasoning about expressions that contain both. 26
Theorems for Quantification Theorems hold only if each quantification is well-defined and the operator has identity u. (+ i | 2 i 3: i*i) = 4 + 9 (+ i | 2 i 2: i*i) = 4 (+ i | 2 i 1: i*i) = ? Answer is 0, because the Identity of + is 0: 0 + x = x (* i | 2 i 3: i*i) = 4 * 9 (* i | 2 i 2: i*i) = 4 (* i | 2 i 1: i*i) = ? Answer is 1, because the Identity of * is 1: 1 * x = x 27
Axioms for Quantification (8.20) Axiom Empty range: (o x | false: P) = u (+ i | false: P) = 0 (* i | false: P) = 1 ( i | false: P) = true ( i | false: P) = false (8.21) Axiom Identity accumulation: (o x | R: u) = u (u is the Identity of operator o) 28
Axioms for Quantification (8.22) Axiom One-point rule: Provided occurs( x , E ), (o x | x = E: P) = P[x:= E] Why the caveat? Consider this: (+ i |i = i+ 1 : i) = 0 (since range is empty) But if no caveat, (+ i |i = i+ 1 : i) = i[i:= i+1], which is i+1 Consider (o x | x = E: P) = P[x:= E] where x occurs free in E LHS has no free occurrence of x. RHS has free occurrence of x. How could they be equal in all states, in general? 29
Axioms for Quantification (8.23) Axiom Distributivity: Provided P,Q: bool or R is finite (o x | R: P) o (o x | R: Q) = (o x | R: P o Q) Example: values of P for x values of Q for x satisfying R 2 + 5 + 8 satisfying R 3 + 1 + 9 Rest on fact that operator o is associative and symmetric 2 + 3 + 5 + 1 + 8 + 9 30
Axioms for Quantification (8.24) Axiom Range Split: Provided P: bool or R, S finite (o x | R S: P) o (o x | R S: P) = (o x | R: P) o (o x | S: P) Other range split theorems in slides giving all theorems (8.26) Axiom Nesting: Provided not occurs( y , R ) (o x, y | R Q: P) = (o x | R: (o y | S: P) (8.29) Dummy reorder: (o x, y | R: P) = (o y, x | R: P) 31
Axioms for Quantification (8.30) Change of dummy: Provided occurs( y , R, P ) and (o x | R: P) = (o y | R[x:= f.y]: P[x:= f.y]) f has inverse (8.31) Dummy renaming: Provided occurs( y , R, P ) (o x | R: P) = (o y | R[x:= y]: P[x:= y]) (8.32) Split off term (example): (o x | 0 i < n+1: P) = (ox | 0 i < n: P) o P[i:= n] 32
Use of Change of Dummy (o x | R: P) = (o y | R[x:=f.y]: P[x:= f.y]) (+ x | 2 x 9: x2) = (+ y | 0 y 7: (y+2)2) Convince yourself that this should hold Use function f.y = y + 2 f has an inverse R is 2 x 9 R[x:= f.y] is 2 y + 2 9 which equals 0 y 7 P is x2 P[x:= f.y] is (y+2)2 33
Proof of Change of Dummy The next slide contains a proof of Change of Dummy. It is an opportunity driven proof: at each step, the shapes of the current formula and the goal give inspiration for the step. This makes the proof memorable. Evidence that this proof is memorable comes from our courses. The students were told they would have to present this proof on a quiz. About 90 percent (out of 80 90 students) get it completely right. We believe that this would be impossible with an informal English proof. 34
(o y | R[x:= f.y]: P[x:= f.y]) start with side with structure = <One-point rule (8.22) need quantification over x> (o y | R[x:= f.y]: (o x | x = f.y: P) = <Nesting (8.26) move x to outside> (o x,y | R[x:= f.y] x = f.y: P) = <Substitution (3.91) to get ready to remove R[x ..]> (o x,y | R[x:= x] x = f.y: P) = <R[x:= x] = R; Nesting (8.26) move y inside> (o x | R: (o y | x = f.y: P) = <x = f.y y = f-1.x prepare to eliminate y> (o x | R: (o y | y = f-1.x: P) = <One-point rule (8.22)> (o x | R: P[y = f-1.x]) = <Textual substitution occurs( y , P )> (o x | R: P) Head for (o x | R: P) 35
Universal Quantification Theorems is symmetric, is associative, and has an identity true Write ( x | R: P) or ( x | R: P) All axioms for quantification hold. Additional axiom (9.3) Axiom over : Provided occurs( x , P ), P ( x | R: Q) ( x | R: P Q) Reason for caveat: ensure that LHS and RHS have same set of free variables Look at theorems at end for theorems for 36
Trading Trading: Moving a conjunct of the range to the body or vice versa. Here are the basic Trading theorems (9.4) Trading: ( x | R: P) ( x |: R P) (9.5a) Trading: ( x | Q R: P) ( x | Q: R P) 37
Modify Metatheorem Monotonicity The range of a quantification is an antimonotonic position. So we have (4.7) Metatheorem Monotonicity (see theorems) Example of use ( i | i = 3: i*I > 0) <Antimonotonicity: i = 3 i > 0> ( i | i > 0: i*I > 0) i = 3 appears in 1 (an odd number) antimonotonic position. So the direction of the arrow changes. 38
Instantiation (9.17) Instantiation: ( x |: P) P[x:= E] One-point rule sharper than Instantiation. In some situations Instantiation is useful. Like symmetry, often used implicitly. Implicit use of Instantiation more concealed if universal quantification itself is not written formally. Example Conventionally write (9.20) ( a,b |: a + b = b + a) as a + b = b + a for all integers a, b Because universal quantification is a side comment and not part of the formula, it is easy to forget that producing, say x*y + z = z + x* y From (9.20) requires Instantiation 39
Metatheorem (9.16) Metatheorem. P is a theorem iff ( x |: P) is a theorem. Use this Metatheorem to discuss ways of stating axioms and theorems in mathematics. Below are three different ways: Axiom: ( b, c: int |: b + c = c + b) Axiom: b + c = c + b for integers b, c In this chapter, b and c have type integer Axiom: b + c = c + b 40
Proof of Trading (9.5a) ( x | Q R: P) ( x | Q: R P) ( x | Q R: P) = <Trading (9.4a)> ( x |: Q R P) = <Shunting (3.69)> ( x |: Q (R P)) = <Trading (9.4a)> ( x | Q: R P) Heading for ( x | Q: R P) 41
Existential Quantification is symmetric and associative and has a identity true ( x | R: P) or ( x | R: P) All axioms for quantification hold for . Additional axiom: Axiom Generalized De Morgan:( x | R: P) ( x | R: P) Idea behind generalization P1 P2 (P1 P2) Generate theorems for from theorems for Use Unfold-fold to prove them. 42
Opportunity-driven proof Prove (9.40), but with all ranges true: ( x |: ( y |: P)) ( y |: ( x |: P)) There is a reason for each step, which is discussed in the hint. ( x |: ( y |: P)) = <Quantified freshy (9.9) Universal quantification over must appear at the outer level this gets it there.> ( y |: ( x |: ( y |: P))) <Monotonicity: Instantiation (9.17) The inner quantification over y has to be removed This does it> ( y |: ( x |: P)) 43
Using a Witness New proof method to prove Interchange of quantifications (9.40) with ranges true: ( x |: ( y |: P)) ( y |: ( x |: P)) The antecedent indicates there exists a value for dummy x for which ( y |: P) holds. Give the value a name xx and use instead the antecedent ( y |: P)[x:= xx].Thus prove the theorem by proving ( y |: P)[x:= xx] ( y |: ( x |: P)) ( y |: P[x:= xx]) <One-point rule (8.22)> ( y |: ( x | x = xx: P)) <Monotonicity: x =xx true> ( y |: ( x |: P)) = 44
Proving an Argument Sound Socrates is human. All humans are mortal. Therefore some person is mortal. h.soc ( p |: h.p m.p) ( p |: m.p) soc: Socrates h.p: person p is human m.p: person p is mortal h.soc ( p |: h.p m.p) <Monotonicity: Instantiation (9.13), with p:= soc> h.soc (h.soc m.soc) <Modus ponens (3.77)> m.soc < -Introduction (9.28)> ( p |: m.p) (heading for ( p |: m.p) 45
Proving an Argument Sound All mosquitos are pests. No butterflies are pests. Therefore, butterflies are not mosquitos. ( c|: m.c p.c) ( c|: b.c p.c) ( c| b.c: p.c) Motivate first step. Must weaken antecedent a quantification over c. First conjunct of antecedent already has this form. Application of De Morgan to second puts second in that form. ( c|: m.c p.c) ( c|: b.c p.c) = <DeMorgan (9.23b); DeMOrgan (3.52a)> ( c|: m.c p.c) ( c|: b.c p.c) = <Distributivity (8.23)> ( c: (m.c p.c) ( b.c p.c)) = <Implication (3.65)> ( c: (m.c p.c) (p.c b.c)) you finish it 46
Mathematical Reasoning Is there some real x for which 1/(x*x + 1) > 1? Formalized is following valid? ( x:real |: 1/(x*x + 1) > 1) ( x |: 1/(x*x + 1) > 1) = <Arithmetic> ( x |: 1 > x*x + 1) = <Arithmetic> ( x |: 0 > x*x) = <x*x 0 from theory of the reals> ( x |: false) = <(9.28)> false 47
Set Theory View set theory as an extension of predicate logic. Add a new type, notations for constants and operations, and axioms Usual notations: {x | P} set of values of x that satisfy predicate P {x*x| 0 x 100} {x*y | 0 x*y 100} what s the dummy? Our notation: {x | P: x} {x | 0 x 100: x*x} {x |0 x*y 100: x*y} 48
Comprehension and enumeration {x | P | E} the set of values of expression E where dummy x ranges over values that satisfy P {v0, v1, , vn} shorthand for {x | x = v0 x = v1 x = vn: x} {1, 3, 1} = {x | x = 1 x = 3 x = 1: x} = {1, 3} 49
Membership and Extensionality (10.4) Axiom Set membership: Provided not occurs( x , F ), F {x | R: E} ( x | R: F = E} (10.5) Axiom Extensionality: S = T ( x |: x S x T} Theorems e {x| false: E} false {x| false: E} {} v {x| x = e} v = e S = {x | x S: x} 50
