Derived Rules and
Applications
Introduction
In predicate logic, as in sentential logic,
there are more valid patterns of inference than just those represented
by the basic inference rules alone. Once again, we can break
down these more sophisticated inferences into a series of applications
of just the basic rules, thereby demonstrating their validity.
In this chapter, we look at a number of derived rules of inference
for predicate logic that are not only useful when it comes to
performing derivations, but that also highlight some of the properties
of the quantifiers. We also introduce the notion of prenex normal
form, the predicate logic counterpart of disjunctive and conjunctive
normal forms.
Goals for this
chapter

Learn a number of derived rules of inference
for predicate logic.

Learn about properties of quantifiers and
the connection between these properties and the derived rules
of inference.

Demonstrate, via derivations, that the
derived rules are valid.

Learn about prenex normal form.
Quantifiers and
Bound Variables
As you may have noticed, when it comes to bound
occurrences of variables, it really doesn't make a difference
which variable we actually use. Just consider the following sentence,
and the various ways that we could symbolise it:

All pairs formulae that differ only in
the choice of bound variables are equivalent.
Here's our translation key:
UD: The world and everything in it.
Expression  Translation 
F(x)
:  x is a formula 
D(x,y)
:  x and y differ only in the choice of bound variables 
Q(x,y)
:  x and y are equivalent 
Here are some possible translations:

(∀x)(∀y)(((F(x) & F(y)) & D(x,y)) → Q(x,y))

(∀y)(∀x)(((F(y) & F(x)) & D(y,x)) → Q(y,x))

(∀y)(∀z)(((F(y) & F(z)) & D(y,z)) → Q(y,z))

(∀w)(∀v)(((F(w) & F(v)) & D(w,v)) → Q(w,v))
We could go on, but we think you'll have gotten
the idea by now.
Here are a pair of derived rules that will
allow us to change bound variables, one for each type of quantifier:
a.   
(∀x)P
   
..   
...
   
c.   
(∀y)P(y/x)
  CBV:  a 
Where:

y does not occur in
P.
a.   
(∃x)P
   
..   
...
   
c.   
(∃y)P(y/x)
  CBV:  a 
Where:

y does not occur in
P.
The only restriction on the rule is, of course,
that the new bound variable cannot already occur in the formula
P. This restriction prevents the ''accidental'' binding of any
free occurrences of variables in
P, as well as the duplication
of variables of quantification.
You'll note that we cite the rule in precisely
the same way for each type of quantifier—that's because it
isn't important which kind of quantifier appears in the formula,
the only important thing is that the variable is bound.
Quantifiers and
Connectives
Introduction
Most of the derived rules that we'll be looking
at involve the relationships between the quantifiers and the
various connectives. You've done enough predicate logic derivations
at this point that we're certain you'll have already noticed
some of the relationships we're about to explore, so without
further ado, let's get started.
Negation
Our first batch of derived rules for predicate
logic have to do with the relationship between negation and
the universal and existential quantifiers. This relationship
is often described by saying that universal and existential
quantifiers can each be defined in terms of the other with
the help of negation, much as can disjunction and conjunction,
with the help of double negation and DeMorgan's laws. As a
result, we could make do with only one of the quantifier symbols
in our store of basic expressions for the language of predicate
logic, though it is handy to have both around.
So how do we define the quantifiers? Let's
start with universal quantifiers: If something is true of every
individual, then there is no individual for which that something
is false. Similarly, in the case of the existential quantifier,
if something is true of some individual, then it can't be false
for all of them. Here are the rules:
a.   
(∀x)P
   
..   
...
   
c.   
¬(∃x)¬P
  Def∀E:  a 
a.   
¬(∃x)¬P
   
..   
...
   
c.   
(∀x)P
  Def∀I:  a 
a.   
(∃x)P
   
..   
...
   
c.   
¬(∀x)¬P
  Def∃E:  a 
a.   
¬(∀x)¬P
   
..   
...
   
c.   
(∃x)P
  Def∃I:  a 
You'll note that we use the same citation
style here as we did for the rules for the definition of the
conditional back in the chapter on derived rules for sentential
logic—we cite both the definition we employ, as well as
distinguishing the two ''directions'' by noting whether we
introduce or eliminate the defined quantifier.
One immediate consequence of the above interdefinability
of the quantifiers is, of course, the relationship between
the quantifiers and a
single occurrence of a negation.
Of course, this relationship is just what you'd expect: Not
everything satisfies a predicate if and only if there is something
that does not satisfy it. Similarly, if it is not the case
that something satisfies a predicate, then everything does
not satisfy it, and vice versa. Here are the rules:
a.   
¬(∀x)P
   
..   
...
   
c.   
(∃x)¬P
  ¬∀:  a 
a.   
(∃x)¬P
   
..   
...
   
c.   
¬(∀x)P
  ∃¬:  a 
a.   
¬(∃x)P
   
..   
...
   
c.   
(∀x)¬P
  ¬∃:  a 
a.   
(∀x)¬P
   
..   
...
   
c.   
¬(∃x)P
  ∀¬:  a 
You'll note that we cite these rules by simply
listing the type of quantifier and the position of the negation
in the justifying formula.
Conjunction
As you may recall from the chapter on derived
rules for sentential logic, one operator is
DISTRIBUTIVE with respect
to a second operator just in case you can apply the two operations
in either order and still end up with the same result. Hence,
we found that conjunction and disjunction are each distributive
with respect to the other, but that the conditional and biconditional
are not distributive with respect to any of our connectives.
Of course, distributivity is not a property
of only binary connectives—the distributivity of quantifiers
with respect to the connectives (and of the connectives with
respect to the quantifiers) is a fascinating topic, and the
inspiration for our next batch of derived rules.
It's pretty obvious that universal quantifiers
are distributive with respect to conjunction, and vice versa.
One simple example is enough to convince anyone: If everything
is a black cat, then everything is black, and everything is
a cat. Similarly, if everything is black, and everything is
a cat, then it's a sure bet that everything is a black cat.
Accordingly, here are the rules for the distributivity of universal
quantifiers and conjunction:
a.   
(∀x)(P & Q)
   
..   
...
   
c.   
(∀x)P & (∀x)Q
  ∀&:  a 
a.   
(∀x)P & (∀x)Q
   
..   
...
   
c.   
(∀x)(P & Q)
  &∀:  a 
As for the rule citations, we simply list
the two operators, the universal quantifier and conjunction,
with the one that gets distributed listed first.
Now, while it works both ways when it comes
to universal quantifiers and conjunction, existential quantifiers
are a different matter. Again, one simple example is enough
to be convincing: If something is pink, and something is an
elephant, this alone is not enough to guarantee that something
is a pink elephant. If, on the other hand, something
is a pink elephant, then there
is something that is pink, and also something that is an elephant.
Here is the appropriate rule:
a.   
(∃x)(P & Q)
   
..   
...
   
c.   
(∃x)P & (∃x)Q
  ∃&:  a 
Disjunction
Given the symmetry between conjunction and
disjunction that we saw manifest in so many ways in the context
of sentential logic, you've probably already determined that
the situation with disjunction will once again be the mirror
image of that for conjunction: That existential quantifiers
will be distributive with respect to disjunction, and vice
versa, while the relationship only holds in one direction with
respect to universal quantifiers, and that this, furthermore,
will be in the opposite direction than that of existential
quantifiers and conjunction.
Indeed, you are correct.
As for universal quantifiers, here's an example:
Everything is either a cat or it isn't, but this doesn't mean
that either everything is a cat or that nothing is. On the
other hand, if either everything is a cat, or everything is
not a cat, then everything either is a cat or not. Here's the
rule:
a.   
(∀x)P v (∀x)Q
   
..   
...
   
c.   
(∀x)(P v Q)
  v∀:  a 
Here are the rules for the existential quantifier:
a.   
(∃x)(P v Q)
   
..   
...
   
c.   
(∃x)P v (∃x)Q
  ∃v:  a 
a.   
(∃x)P v (∃x)Q
   
..   
...
   
c.   
(∃x)(P v Q)
  v∃:  a 
Aside from the basic interaction of disjunction
and the quantifiers, it turns out that certain sentential patterns
of inference involving disjunction have predicate counterparts,
where the truthfunctional structure of the argument is simply
moved to the inside of universally quantified formulae. What
exactly do we mean, here? Consider the following predicate
versions of the disjunctive syllogism:
a.   
(∀x)(P v Q)
   
b.   
(∀x)¬Q
   
..   
...
   
d.   
(∀x)P
  PDS:  a, b 
a.   
(∀x)(P v Q)
   
b.   
(∀x)¬P
   
..   
...
   
d.   
(∀x)Q
  PDS:  a, b 
Actually, we don't even need both of the
premises to be universally quantified, as the following demonstrate:
a.   
(∀x)(P v Q)
   
b.   
(∃x)¬Q
   
..   
...
   
d.   
(∃x)P
  PDS∃:  a, b 
a.   
(∀x)(P v Q)
   
b.   
(∃x)¬P
   
..   
...
   
d.   
(∃x)Q
  PDS∃:  a, b 
Of course, other sentential rules involving
disjunction have similar predicate counterparts. We'll leave
it to you to discover more on your own (and, of course, in
the exercises).
The Conditional
So, is the conditional distributive with
respect to either quantifier? Given the definition of the conditional
and the definitions of the quantifiers, you have everything
you need to sit down and figure it out for yourself. Why not
give it a shot, then continue on to see if you are right.
If you came to the conclusion that the conditional
is distributive with respect to the universal quantifier, but
that the relationship only holds in one direction, then you'd
be absolutely correct. Here's the rule:
a.   
(∀x)(P → Q)
   
..   
...
   
c.   
(∀x)P → (∀x)Q
  ∀→:  a 
Of course, just because that is the only
true distributivity relation between the conditional and the
quantifiers, that doesn't mean that there aren't other, just
as interesting inferences that can be drawn from a quantifiedover
conditional. Consider the following:
a.   
(∀x)(P → Q)
   
..   
...
   
c.   
(∃x)P → (∃x)Q
  ∀→∃:  a 
a.   
(∃x)(P → Q)
   
..   
...
   
c.   
(∀x)P → (∃x)Q
  ∃→:  a 
Just as we found with disjunction, many of
the sentential patterns of inference involving the conditional
have predicate counterparts. The hypothetical syllogism and
Modus Tollens are two perfect examples:
a.   
(∀x)(P → Q)
   
b.   
(∀x)(Q → R)
   
..   
...
   
d.   
(∀x)(P → R)
  PHS:  a, b 
a.   
(∀x)(P → Q)
   
b.   
(∀x)¬Q
   
..   
...
   
d.   
(∀x)¬P
  PMT:  a, b 
To finish off our discussion of the conditional
and quantifiers, think back to the discussion of properties
of the conditional in the chapter on sentential derived rules.
Do you recall the derived rule transposition? We mentioned
at the time that transposition was the sentential analogue
of a classical form of inference known as
CONTRAPOSITION, which
we saw in its full form in our discussion of Aristotelian logic.
Well, we can now present the full form of contraposition for
universal statements, which is as follows:
a.   
(∀x)(P → Q)
   
..   
...
   
c.   
(∀x)(¬Q → ¬P)
  Contra:  a 
The Biconditional
If you think for a moment about the distributivity
relations we've seen for conjunction and for the conditional
with respect to the quantifiers, we're sure that the next rule
will come as no surprise:
a.   
(∀x)(P ↔ Q)
   
..   
...
   
c.   
(∀x)P ↔ (∀x)Q
  ∀↔:  a 
Of course, there are other inferences one
can make from a quantifiedover biconditional, but we'll leave
it up to you to discover what they are.
As for predicate counterparts of rules for
the biconditional, we'll point out one of them: The predicate
counterpart of the Replace Equivalents rule, the one rule of
replacement that we have. Again, our quantified version will
allow the replacement of a subformula by an equivalent, only
this time we also allow the replacement of substitution instances
of one equivalent by substitution instances of the other equivalent.
Here's the rule:
a.   
(∀x)(P ↔ Q)
   
b.   
P(t/x)
   
..   
...
   
d.   
Q(t/x)
  QRE:  a, b 
Well, that just about does it for the relationship
between the quantifiers and the connectives. Certainly we haven't
presented every possible derived rule for predicate logic,
but we have captured all of the fundamental relationships
between a given quantifier and one of the connectives. Now
all that's left to do is to look at the interaction of multiple
quantifiers, and we'll have a complete supply of derived rules
at our disposal.
Rules for Multiple
Quantifiers
Just as with negation, when it comes to multiple
quantifiers, you really don't need to consider more than two
at a time, even though there is no quantificational equivalent
to the rules for double negation—if you have a group of more
than two quantifiers to worry about, you can always work your
way through them two at a time.
Since we only need to consider pairs of quantifiers,
there are only four configurations that need to be considered:
∀∀
∃∃
∀∃
and
∃∀
As for the first two, you've already encountered a few of examples
of these configurations in the derivations you performed from
the previous chapter's exercises, so you'll certainly have noticed
that the order of multiple quantifiers of the same type doesn't
matter. Accordingly, here are the rules:
a.   
(∀x)(∀y)P
   
..   
...
   
c.   
(∀y)(∀x)P
  ∀∀:  a 
a.   
(∃x)(∃y)P
   
..   
...
   
c.   
(∃y)(∃x)P
  ∃∃:  a 
The order of mixed pairs of quantifiers, on
the other hand, is important. If you'll think about the rule
∃E
for a
few minutes, it should be clear that an existential quantifier
can move
inwards past a universal quantifier
without difficulty, but that there's no way to legitimately bring
an existential quantifier
outwards past a universal one. This
is exactly what you'd expect, though, since, for example, if
there is a single person that everyone loves, then everybody
loves somebody. On the other hand, just because everyone has
a kidney, for example, this doesn't mean that it is the same
kidney in each case. Accordingly, here is the one rule we have
for mixed pairs of quantifiers:
a.   
(∃x)(∀y)P
   
..   
...
   
c.   
(∀y)(∃x)P
  ∃∀:  a 
Well, we now have a comprehensive slate of
derived rules for predicate logic. We'll be putting some of them
to good use in just a moment in order to demonstrate that every
formula of predicate logic is equivalent to a formula in prenex
normal form, so we should move on to the next section to explain
what prenex normal form happens to be.
Prenex Normal Form
A formula of predicate logic is said to be
in
PRENEX NORMAL FORM just
in case no quantifier in the formula occurs inside the scope
of any operator other than another quantifier, i.e., just in
case all the quantifiers occurring in the formula occur at the
''beginning'' of the formula.
Here are a few examples of formulae in prenex
normal form:

G(s)

(∀x)R(x,d)

(∀x)(∃y)(F(x) → ¬L(x,y))

(∀z)(∃x)(∀y)(M(x,y) & N(z,y))
Here are a few examples of formulae that are
not in prenex normal form:

G(a) & (∀x)(G(x) → H(x))

(∃z)(H(z,a) → (∀y)(P(y,z) v Q(z,y)))

¬(∀x)P(x)
A little more formally, we can state the definition
of prenex normal form as follows:
Definition:
A formula
P is in prenex normal form just in case
P is of the form
Q_{1},...
Q_{n}
F, where each of the
Qs is a quantifier, and
F contains no quantifiers.
So much for the definition—we've already
mentioned that every formula of predicate logic is equivalent
to a formula in prenex normal form. How are we going to go
about proving this? We obviously aren't going to be able to
adapt the truthtable method that we used to prove that every
formula of sentential logic is equivalent to a formula in disjunctive
normal form. What we're going to do instead is to make use
of some of the principles captured by our new derived rules
to demonstrate that any formula has a prenex equivalent.
Let's start out by considering atomic formulae.
Since they contain no quantifiers, atomic formulae are actually
already in prenex normal form, so we don't need to do anything,
here.
So far, so good. We already have the situation
with atomic formulae in hand. The only thing we have left to
worry about, then, are nonatomic formulae. This may seem like
it will be impossible to deal with, but there's a trick to
it. You see, there are only seven different ways to construct
nonatomic formulae—with a single formula, we can negate
it, universally quantify over it, or existentially quantify
over it, and with two formulae, we can form a conjunction,
disjunction, conditional, or biconditional from them. Now,
here's the trick: We only have to consider cases where the
immediate subformulae are themselves in prenex normal form—that
is, we only have to demonstrate that we can convert any formula
whose immediate subformulae are all in prenex normal form into
a formula in prenex normal form. After all, if the immediate
subformulae are not in prenex normal form, we can just use
the same conversion techniques to the immediate subformulae
themselves. Neat, isn't it?
Okay, so let's start with negation. We need
to be able to convert a formula of the following form into
prenex normal form:
This, however, is a trivial matter, as the
derived rules for quantifiers and negations make evident. We
just need to move the negation in past all the quantifiers,
changing the type of each quantifier (from universal to existential
or vice versa) along the way. So much for negations.
Next, we have universally and existentially
quantified formulae to consider, but if our immediate subformula
is already in prenex normal form, then adding another quantifier
won't change anything there, so we're already done.
The only cases we have left to worry about,
then, are those where the main connective of our formula is
one of the binary connectives. What we need to do is to find
a way of converting any formula
P * Q
into prenex normal form (where
* is one of the binary
connectives) given the assumption that
P and
Q are themselves in prenex normal form. Here's how we'll
do it: First, we'll change any bound variables that the two
immediate subformulae have in common, so that no two quantifiers
in the formula as a whole have the same variable of quantification.
Once we've taken care of that, it's actually an easy matter
to bring all the quantifiers out to the ''front'' of the formula,
one at a time. We won't get into a detailed demonstration of
this point, here—we'll let you take care of it in the exercises
by completing a number of derivations.
Now that we have dealt with the binary connectives,
we've done what we set out to do—demonstrate that for any
formula whose immediate subformulae are all in prenex normal
form, we can find a formula in prenex normal form that is
equivalent to the original formula. As we mentioned, this also
suffices to demonstrate that we can find a prenex equivalent
for
any formula—if its immediate
subformulae are
not in prenex normal form, we just
have to find prenex equivalents to the subformulae first.
At this point, you might be a little suspicious—after
all, what if the subformulae of the subformulae are not in
prenex normal form? Well, then we would just have to find prenex
equivalents for them, too. What about subformulae of subformulae
of subformulae, and so on? Recall that the first thing we did
was to point out that since atomic formulae contain no quantifiers,
they are by default in prenex normal form? Well, as you know,
eventually you'll get to nothing but atomic formulae as subformulae,
and these
are in prenex normal form, so you'll
be able to apply the above transformation techniques starting
with these, on up the parse tree until you have transformed
the entire formula into a prenex equivalent. Works out quite
nicely, doesn't it?
Exercises
Exercise: 13.1
Complete the following derivations in order to demonstrate that
our rules for changing bound variables are valid, and to practice
using those rules.
i  
Derive:
(∀y)P(y) 

Try it in the CPL: 

ii  
Derive:
(∃y)P(y) 

Try it in the CPL: 

iii  
Derive:
(∀u)(∀v)(∀w)(R(u,v,w) & Q(v,w)) 
1.   
(∀x)(∀y)(∀z)(R(x,y,z) & Q(y,z))
  Prem  

Try it in the CPL: 

iv  
Derive:
(∃v)(∃w)(H(v,w) v G(w,v)) 
1.   
(∃x)(∃y)(H(x,y) v G(y,x))
  Prem  

Try it in the CPL: 

v  
Derive:
(∀w)(∃v)(∀z)P(w,v,z) 
1.   
(∀x)(∃y)(∀u)P(x,y,u)
  Prem  

Try it in the CPL: 

Exercise: 13.2
Complete the following derivations in order to demonstrate that
our rules regarding quantifiers and negation are valid.
i  
Derive:
¬(∃x)¬P(x) 

Try it in the CPL: 

ii  
Derive:
(∀x)P(x) 

Try it in the CPL: 

iii  
Derive:
¬(∀x)¬P(x) 

Try it in the CPL: 

iv  
Derive:
(∃x)P(x) 

Try it in the CPL: 

v  
Derive:
(∃x)¬P(x) 

Try it in the CPL: 

vi  
Derive:
¬(∀x)P(x) 

Try it in the CPL: 

vii  
Derive:
(∀x)¬P(x) 

Try it in the CPL: 

viii  
Derive:
¬(∃x)P(x) 

Try it in the CPL: 

Exercise: 13.3
Complete the following derivations in order to demonstrate that
our rules regarding quantifiers, conjunction, and disjunction are
valid.
i  
Derive:
(∀x)P(x) & (∀x)Q(x) 
1.   
(∀x)(P(x) & Q(x))
  Prem  

Try it in the CPL: 

ii  
Derive:
(∀x)(P(x) & Q(x)) 
1.   
(∀x)P(x) & (∀x)Q(x)
  Prem  

Try it in the CPL: 

iii  
Derive:
(∃x)P(x) & (∃x)Q(x) 
1.   
(∃x)(P(x) & Q(x))
  Prem  

Try it in the CPL: 

iv  
Derive:
(∀x)(P(x) v Q(x)) 
1.   
(∀x)P(x) v (∀x)Q(x)
  Prem  

Try it in the CPL: 

v  
Derive:
(∃x)P(x) v (∃x)Q(x) 
1.   
(∃x)(P(x) v Q(x))
  Prem  

Try it in the CPL: 

vi  
Derive:
(∃x)(P(x) v Q(x)) 
1.   
(∃x)P(x) v (∃x)Q(x)
  Prem  

Try it in the CPL: 

vii  
Derive:
(∀x)P(x) 
1.   
(∀x)(P(x) v Q(x))
  Prem  
2.   
(∀x)¬Q(x)
  Prem  

Try it in the CPL: 

viii  
Derive:
(∀x)Q(x) 
1.   
(∀x)(P(x) v Q(x))
  Prem  
2.   
(∀x)¬P(x)
  Prem  

Try it in the CPL: 

ix  
Derive:
(∃x)P(x) 
1.   
(∀x)(P(x) v Q(x))
  Prem  
2.   
(∃x)¬Q(x)
  Prem  

Try it in the CPL: 

x  
Derive:
(∃x)Q(x) 
1.   
(∀x)(P(x) v Q(x))
  Prem  
2.   
(∃x)¬P(x)
  Prem  

Try it in the CPL: 

Exercise: 13.4
Complete the following derivations in order to demonstrate that
our rules regarding quantifiers, the conditional, and the biconditional
are valid.
i  
Derive:
(∀x)P(x) → (∀x)Q(x) 
1.   
(∀x)(P(x) → Q(x))
  Prem  

Try it in the CPL: 

ii  
Derive:
(∃x)P(x) → (∃x)Q(x) 
1.   
(∀x)(P(x) → Q(x))
  Prem  

Try it in the CPL: 

iii  
Derive:
(∀x)P(x) → (∃x)Q(x) 
1.   
(∃x)(P(x) → Q(x))
  Prem  

Try it in the CPL: 
iv  
Derive:
(∀x)(P(x) → R(x)) 
1.   
(∀x)(P(x) → Q(x))
  Prem  
2.   
(∀x)(Q(x) → R(x))
  Prem  

Try it in the CPL: 
v  
Derive:
(∀x)¬P(x) 
1.   
(∀x)(P(x) → Q(x))
  Prem  
2.   
(∀x)¬Q(x)
  Prem  

Try it in the CPL: 
vi  
Derive:
(∀x)(¬Q(x) → ¬P(x)) 
1.   
(∀x)(P(x) → Q(x))
  Prem  

Try it in the CPL: 
vii  
Derive:
(∀x)P(x) ↔ (∀x)Q(x) 
1.   
(∀x)(P(x) ↔ Q(x))
  Prem  

Try it in the CPL: 
viii  
Derive:
Q(a) 
1.   
(∀x)(P(x) ↔ Q(x))
  Prem  
2.   
P(a)
  Prem  

Try it in the CPL: 
Exercise: 13.5
Complete the following derivations in order to demonstrate that
our rules for multiple quantifiers are valid, and to practice using
those rules.
i  
Derive:
(∀y)(∀x)R(x,y) 

Try it in the CPL: 
ii  
Derive:
(∃y)(∃x)R(x,y) 

Try it in the CPL: 
iii  
Derive:
(∀y)(∃x)R(x,y) 

Try it in the CPL: 
iv  
Derive:
(∀y)(∀x)¬R(x,y) 
1.   
(∀x)(∀y)(R(x,y) → Q(x,y))
  Prem  
2.   
(∀y)(∀x)¬Q(x,y)
  Prem  

Try it in the CPL: 
v  
Derive:
(∀w)((∃u)L(u,w) → (∃u)M(w,u)) 
1.   
(∀u)(∀w)(L(u,w) → M(w,u))
  Prem  

Try it in the CPL: 
vi  
Derive:
(∀y)((∃x)R(x,y) & (∃z)S(y,z)) 
1.   
(∃x)(∀y)(R(x,y) & S(y,x))
  Prem  

Try it in the CPL: 
Exam