COMP2022|2922
Models of Computation
Lesson 4a: Equivalences of Predicate Logic
Presented by
Sasha Rubin
School of Computer Science
Formulas that “mean the same thing” are called equivalent. We now study common equivalences, also called laws.
1/32
Equivalences
Definition
Two formulas F and G are (logically) equivalent if they are assigned the same truth value in every structure under every assignment. This is written F ≡ G.
Fact. All equivalences which have been proved for formulas in propositional logic also hold for formulas of predicate logic.
Example
– De Morgan’s Law: ¬(F ∧ G) ≡ (¬F ∨ ¬G) holds for all formulas F, G of predicate logic.
– E.g., ¬(∃xP (x) ∧ Q(y)) ≡ (¬∃xP (x) ∨ ¬Q(y)).
2/32
Equivalences involving quantifiers
For all formulas F, G: (Q. Negation)
(Q. Unification) (Q. Transposition) (Q. Extraction)
¬∀xF
¬∃xF (∀xF ∧ ∀xG) (∃xF ∨ ∃xG)
∀x∀yF
∃x∃yF if x ̸∈ Free(G) : (∀xF ∧G) (∀xF ∨G) (∃xF ∧G) (∃xF ∨G)
≡ ∃x¬F
≡ ∀x¬F
≡ ∀x(F ∧ G) ≡ ∃x(F ∨ G) ≡ ∀y∀xF
≡ ∃y∃xF
≡ ∀x(F ∧G) ≡ ∀x(F ∨G) ≡ ∃x(F ∧G) ≡ ∃x(F ∨G)
3/32
Equivalences
Here are informal reasons behind some of these equivalences:1 1. ¬∀xF ≡ ∃x¬F
– the LHS says that not all x satisfy F ,
– which means the same thing as some x doesn’t satisfy F, – which means that some x does satisfy ¬F,
– which is what the RHS says.
2. (∀xF ∧∀xG) ≡ ∀x(F ∧G)
– the LHS says that F holds for every x and G holds for every x,
– which is the same as saying both F and G hold for every x, – which is what the RHS says.
3. ∀x∀yF ≡ ∀y∀xF
– Both sides say that F holds for all values of the listed variables.
4. (∀xF∧G)≡∀x(F∧G)ifx̸∈Free(G)
– LHS says F holds for every x, and G holds.
– RHS says F and G hold for every x; but G doesn’t depend on
the value of x.
1To do prove them formally, use the inductive definition of truth-value.
4/32
Equivalences
Example
Show that ¬(∃xP (x, y) ∨ ∀z¬R(z)) ≡ ∀x∃z(¬P (x, y) ∧ R(z))
¬(∃x P (x, y) ∨ ∀z¬R(z))
≡ (¬∃xP (x, y) ∧ ¬∀z¬R(z))
≡ (∀x¬P (x, y) ∧ ∃z¬¬R(z)) ≡ (∀x¬P (x, y) ∧ ∃zR(z))
≡ ∀x(¬P (x, y) ∧ ∃zR(z))
≡ ∀x(∃zR(z) ∧ ¬P (x, y))
≡ ∀x∃z(R(z) ∧ ¬P (x, y)) ≡ ∀x∃z(¬P (x, y) ∧ R(z))
DeMorgan’s Laws Quantifier Negation Double Negation Quantifier Extraction Comm ∧ Quantifier Extraction Comm. ∧
5/32
Equivalences
To show that F1 ̸≡ F2 we should find a counterexample, i.e., a structure A and assignment such that
TV(F1, α, A) ̸= TV(F2, α, A).
Show that (∀xP (x) ∧ Q(x)) ̸≡ ∀x(P (x) ∧ Q(x)) Here is a counter-example:
– The structure A = (A,PA,QA) has domain A = {1,2}, predicates P A = {1, 2}, QA = {2},
– the assignment α maps variable x to domain element 2.
1. Then TV((∀xP (x) ∧ Q(x)), α, A) = 1 (since every element of
AisinP andα(x)isinQ).
2. And TV(∀x(P (x) ∧ Q(x)), α, A) = 0 (since not every
elementofAisinP andinQ).
This also shows why we can’t drop x ̸∈ Free(G) for Quantifier Extraction.
6/32
Equivalences
Example
Show that (∀xP (x) ∧ Q(x)) ≡ ∀y(P (y) ∧ Q(x)).
(∀xP (x) ∧ Q(x)) ≡ (∀yP (y) ∧ Q(x)) rename bound variable
≡ ∀y(P (y) ∧ Q(x)) Quantifier Extraction
– Bound variables are like dummy variables, and so one can rename them as follows.
– Let F be a formula in which the variable z does not occur in F. The renaming of variable x by z in F is the formula F′ that results from F by simultaneously replacing all occurrences of x, that are bound by the same occurrence of a quantifier, by the variable z. We say that F′ is a renaming of F.
– Fact. Renamings preserve the formula up to logical equivalence.
– In other words, renamings only change the syntax, not the semantics (truth-value) of a formula.
7/32
Equivalences: renaming
Examples
1. ∃zQ(z, y) is a renaming of ∃xQ(x, y).
2. (∃xP (x) ∨ ∃zQ(z, x)) is not a renaming of
(∃wP (w) ∨ ∃zQ(z, x)) since x already occured in the formula.
3. (∃zP (z) ∧ ∀zQ(z)) is not a renaming of (∃xP (x) ∧ ∀xQ(x)) since a renaming only applies to variables bound by a single quantifier.
8/32
Application of equivalences
Every formula can be transformed into an equivalent one that has a rigid structure, called a normal form.
9/32
Normal forms
We will look at two normal forms. 1. Negation normal form (NNF) 2. Prenex normal form (PNF)
10/32
Normal forms: NNF
Definition
A formula F is in negation normal form (NNF) if negations only occur immediately infront of atomic formulas.
Theorem
For every formula F there is an equivalent formula in NNF. Algorithm (“push negations inwards”)
Substitute in F every occurence of a subformula of the form ¬¬G by G, and
¬∀xF by ∃x¬F ¬∃xF by ∀x¬F ¬(G∧H) by (¬G∨¬H) ¬(G∨H) by (¬G∧¬H)
until no such subformulas occur, and return the result.
Why is this algorithm correct?
11/32
Normal forms: NNF
Example
Put ¬∃x(P (x) ∧ ¬∃yQ(y, x)) into NNF.
12/32
Normal forms: PNF
Definition
A formula F is in prenex normal form (PNF) if it has the form Q1x1Q2x2 · · · QnxnF
where each Qi ∈ {∃, ∀} is a quantifier symbol, the xis are variables, n ≥ 0 (so, there may be no quantifiers in the prefix), and F does not contain a quantifier.
Example
– ∀x(¬P (x) ∨ ∃y(N (y) ∧ L(x, y))) is not in PNF. – ∀x∃y(¬P(x)∨(N(y)∧L(x,y))isinPNF.
13/32
Normal forms: PNF
Theorem
For every formula F there is an equivalent formula in PNF. Algorithm (“pull quantifiers out the front”)
1. Put F in NNF, call the result F′.
2. Substitute in F′ every occurence of a subformula of the form
(∀xF ∧G) by ∀x(F ∧G) (∀xF ∨G) by ∀x(F ∨G) (∃xF ∧G) by ∃x(F ∧G) (∃xF ∨G) by ∃x(F ∨G)
until no such subformulas occur (use commutativity to handle (G ∧ ∀xF ), etc.), and return the result.
3. NB. To apply these equivalences we need that x ̸∈ Free(G). This can always be achieved by renaming the bound variable x.
14/32
Normal forms: PNF
Put the following into PNF
– (Q(x)∨∀xR(x,x))
15/32
Normal forms: PNF
Put the following into PNF
– (∀yP(z,y)∨∃wQ(w))
– (∀yP(z,y)∨∃yQ(y))
16/32
Logical consequence
Definition
A sentence F is a logical consequence2 of the set {E1, · · · , Ek} of sentences if every structure A in which all of the E1, · · · , Ek are true, also F is true. In this case we write
{ E 1 , · · · , E k } |= F E 1 , · · · , E k |= F
or simply
Example
– ∀x R(x, x) is a logical consequence of {∀x∀y R(x, y)}.
– P (c) is a logical consequence of {Q(c), ∀x (Q(x) → P (x))}.
2This definition mimics the one for Propositional Logic.
17/32
COMP2022|2922
Models of Computation
Lesson 4b: Deductive system for Predicate Logic
Presented by
Sasha Rubin
School of Computer Science
Deductive systems are a syntactic mechanism for deriving validities as well as logical consequences from assumptions
18/32
Natural deduction
– We extend ND for propositional logic with rules to handle quantifiers.
– Each quantifier symbol ∃, ∀ has two types of rules:
1. Introduction rules introduce the quantifier 2. Elimination rules remove the quantifier
19/32
Natural Deduction: replacing free variables by terms
Definition
For a formula F , variable x, term t, we can obtain a formula F [t/x] by simultaneously replacing all free occurrences of x in F by t.
– The idea is that whatever F said about x, now F[t/x] says about t.
– In a few slides, we will restrict when we are allowed to make such replacements.
20/32
Natural Deduction: inference rules involving ∀
(∀E )
S⊢∀xF S⊢F[t/x]
where t is a term that is free to replace x in F.
(∀I )
S⊢F[c/x] S⊢∀xF
where c is a constant symbol, not occuring in F, nor in any formula in S.
(∀E) formalises the reasoning
If we know that F holds for every x, then it must hold, in particular, taking x = t.
21/32
Natural Deduction: inference rules involving ∀
(∀E )
S⊢∀xF S⊢F[t/x]
where t is a term that is free to replace x in F.
(∀I )
S⊢F[c/x] S⊢∀xF
where c is a constant symbol, not occuring in F, nor in any formula in S.
(∀I) formalises the reasoning
Let c be any element . . . [prove F [c/x]]. Since c was arbi- trary, deduce F holds for all x.
That c is arbitrary is captured by requiring that c is not in the assumptions used to prove F [c/x], and so c is not constrained in any way.
21/32
Natural Deduction: example using ∀ ∀x∀yP (x, y) ⊢ ∀y∀xP (x, y)
Line
Assumptions
Formula
Justification
References
1
1
∀x∀yP (x, y)
Asmp. I
2
1
∀yP(c,y)
∀E
1
3
1
P(c,d)
∀E
2
4
1
∀xP (x, d)
∀I*
3
5
1
∀y∀xP (x, y)
∀ I **
4
* the constant c does not occur in F (i.e., P(x,d)), nor in the formula of its assumption (in line 1).
** the constant d does not occur in F (i.e., ∀xP(x,y)), nor in the formula of its assumption (in line 1).
The conditions on (∀ E) that talk about “free to replace” will be explained next.
22/32
Natural Deduction: free to replace
Example
Say F is the formula ∃y(x < y) expressing, about numbers, that there is some number bigger than x. Then the formula F[t/x] taking t = z + 1 is ∃y(z + 1 < y) which says that there is some number bigger than z + 1.
Note
The formula F [t/x] taking t = y + 1 is the formula ∃y(y + 1 < y) which says that there is some number bigger than its successor.
– What went wrong? We changed x from being free to y + 1 where y is bound.
– We disallow such substitutions.
If no variable y of t is in the scope of a quantifier Qy in F[t/x] then we say that t is free to replace x in F.
23/32
Natural Deduction: example using ∀ ∀x∀yP (x, y) ⊢ ∀y∀xP (x, y)
Line
Assumptions
Formula
Justification
References
1
1
∀x∀yP (x, y)
Asmp. I
2
1
∀yP(c,y)
∀E*
1
3
1
P(c,d)
∀ E **
2
4
1
∀xP (x, d)
∀I
3
5
1
∀y∀xP (x, y)
∀I
4
* The term c is free to replace x in F = ∀yP(y,x). ** The term d is free to replace y in F = P(c,y).
24/32
Natural Deduction: example using ∀ ∀x(P (x) ∧ Q(x)) ⊢(∀xP (x) ∧ ∀xQ(x))
Line
Assumptions
Formula
Justification
References
1
1
∀x(P (x) ∧ Q(x))
Asmp. I
2
1
(P (c) ∧ Q(c))
∀E*
1
3
1
P (c)
∧E
2
4
1
∀xP (x)
∀I*
3
5
1
Q(c)
∧E
2
6
1
∀xQ(x)
∀I*
5
7
1
(∀xP (x) ∧ ∀xQ(x))
∧I
4,6
* Check that the conditions in lines 2,4,6 are satisfied.
25/32
Natural Deduction: inference rule ∃I
(∃I )
S⊢F[t/x] S⊢∃xF
where t is a term that is free to replace x in F.
(∃I) formalises the reasoning
If we know that F holds for a specific term t, then we know it holds for some x.
26/32
Natural Deduction: example using ∃I ∀xP (x) ⊢ ∃xP (x)
Line
Assumptions
Formulas
Just.
Ref.
1
1
∀xP (x)
Asmp. I
2
1
P (c)
∀E
1
3
1
∃xP (x)
∃I*
2
* the constant c is free to replace x in P (x)
27/32
Natural Deduction: inference rule ∃E
(∃E )
S1 ⊢∃xF S2 ∪{F[c/x]}⊢G S1 ∪ S2 ⊢ G
where c is a constant symbol, not occuring in F, nor in G, nor in any formula in S2.
(∃E) formalises the reasoning
If we prove G from F[c/x], but we did not use any other
properties of c, then we can prove G from the weaker as- sumption that some x satisfies F.
28/32
Natural Deduction: inference rule ∃E
(∃E )
S1 ⊢∃xF S2 ∪{F[c/x]}⊢G S1 ∪ S2 ⊢ G
where c is a constant symbol, not occuring in F, nor in G, nor in any formula in S2.
How to use (∃E)?
1. Assume F[c/x] ensuring that c does not occur in F.
2. Derive G making sure that c is not in the assumption set of G except for F[c/x].
3. Cancel the assumption F [c/x], and conclude G.
28/32
Natural Deduction: example using ∃E ∀x(Q(x) → P (y)), ∃xQ(x) ⊢ P (y)
Line
Assumptions
Formulas
Just.
Ref.
1
1
∀x(Q(x) → P (y))
Asmp. I
2
2
∃xQ(x)
Asmp. I
3
1
(Q(c) → P (y))
∀E
1
4
4
Q(c)
Asmp. I
5
1,4
P(y)
→E
3,4
6
1,2
P(y)
∃E
2,4,5
29/32
Natural Deduction: incorrect usage of (∃E)
∃xP(x)⊢∀xP(x) ...?
Line
Asmp.
Form.
Just.
Ref.
1
1
∃xP (x)
Asmp. I
2
1
P (c)
∃E
?,?,?
3
1
∀xP (x)
∀I
2
Here is the faulty argument in natural language:
We are given that some x has F. Let c be such an x. Since c was chosen arbitrarily (?!), conclude that every x has F .
30/32
Natural Deduction: e.g. using ∃ and ∀ ¬∃x¬P (x) ⊢ ∀xP (x)
Line
Asmp.
Form.
Just.
Ref.
1
1
¬∃x¬P (x)
Asmp. I
2
2
¬P [c/x]
Asmp. I
3
2
∃x¬P (x)
∃I *
2
4
1,2
⊥
¬E
1,3
5
1
P [c/x]
RA
2,4
6
1
∀xP (x)
∀I **
5
* c is free to replace x in ¬P(x)
** c does not appear in P(x) nor in the assumption 1
31/32
Deductive system: wrapping up
– We introduced Natural Deduction (ND) for Predicate Logic as a way to derive logical consequences in a way that can be checked by machine.
– Just like for Propositional Logic, ND for Predicate Logic is sound (meaning it can only derive logical consequences) and complete (meaning that it can derive all logical consequences).
– However, unlike Propositional Logic, there is no algorithm that can decide, given E1,··· ,Ek,F whether or not F is a consequence of E1, · · · , Ek.
– We will discuss this when we cover undecidability (Lec 10).
– This means that finding proofs of Predicate Logic inherently require human ingenuity.
32/32