Topic DPL: Derivations in predicate logic

2 More derivations

So far you have learned two of the four

quantifier rules. In this section you will

learn the other two rules for the quantifiers.

2.1 Universal Quantifier Introduction

Universal Quantifier Introduction permits you, in

certain circumstances, to add a universal quantifier

to a derivation. For example,

This shows
∀x(Sx&Fx)
∀xSx
.

Here is a statement of
∀I:

∀I (Universal Quantifier Introduction)

For any variable v and constant c,

if you have derived φv/c, and c does not occur in φ,

and c does not occur in anything φv/c depends on,

and
∀vφ is a well-formed formula of MPL,

then you can write down
∀vφ,

depending on everything φv/c depends on.

This may look a little complicated at first, but once

you see the reason it is written that way, you will

find it no more complicated than the quantifier rules

you have learned already. Suppose you have written

down φv/c in your derivation. If you want to write

down
∀vφ
using this rule you need to satisfy three

restrictions. The first restriction is that c does not
occur

in φ. The second restriction is that c does not occur in

anything φv/c depends on. The third and last restriction

is that
∀vφ
be a well-formed formula of MPL.

Let's think about why these restrictions are built

into the rule.

If the third restriction was not present, then the

following would be a correct derivation:

The expression on line 2 is not a

well-formed formula of MPL. One of the goals

of our system is to make sure that each of the

rules of our system is sound, that is, at each line

in our derivation you write down a formula which

is entailed by its dependencies. If you could

write down line 2 we would have failed to achieve

one of the goals of our system.

Exercise 2.1a

Some natural deduction systems permit you to write

down expressions which are not well-formed formulas.

Can you think of any reason why this might be a

good idea?

The second restriction on Rule
∀I
is that the c

does not occur in anything φv/c depends on.

If that restriction was not present, Rule
∀I
would

not be a sound rule. It is easy to see why:

"Fa" does not entail "∀xFx".
So the formula on

line 2 is not entailed by its dependencies.

If you could use Rule
∀I
to write down line 2,

then Rule
∀I
would not be sound. Rule
∀I
does

not permit you use line 1 to write down line 2

because "a" occurs in "Fa" and the "Fa" on line 1

depends on "Fa".

Exercise 2.1b

Explain why "Fa" does not entail "∀xFx".

The final restriction on Rule
∀I
is that c does not

occur in φ. If this restriction was not present then,

again, Rule
∀I
would not be a sound rule:

In this example, φ is "(Fa→Fx)",
v is "x", c is "a",

and φv/c is "(Fa→Fa)". If Rule
∀I
worked this way,

we would be able to show
∀x(Fa→Fx)
even though

it is not the case that
∀x(Fa→Fx).
Thus, if

Rule
∀I
worked this way, it would be unsound.

Exercise
2.1c

Explain why line 3 in the last example violates Rule
∀I.

Exercise 2.1d

Show that it is not the case that
∀x(Fa→Fx).

2.2 Existential Quantifier Elimination

Now for the last quantifier rule, existential

quantifier elimination. Here is an example:

Rule
∃E
permits you to derive things when you

have an existentially quantified formula as in

"∃x(Sx&Rx)"
on line 1. To use the rule,

you assume an instance of the existentially quantified

formula and then derive something from it. In this case

"(Sa & Ra)" is assumed and "∃xSx"
is derived from it.

At this point Rule
∃E
lets you write down what you

have just derived a second time, changing its dependencies.

While line 4 depended on the assumption

in line 2, the rule lets you write down the same formula

depending on the existentially quantified formula in line
1.

In essence, the idea behind of the rule is this:

when an existentially quantified formula like
"∃xFx"
is

true under some interpretation, then you know

that at least one formula like "Fa" or "Fb" or

"Fc" or (and so on) is also true. But you don't know

which one. Still, what you can do is assume one of

these formulas (such as "Fb") and try to show

something that you could show whether you

assume "Fa" or "Fb" or "Fc" or whatever.

For example, in the derivation above, we assumed

"(Sa & Ra)" to derive "∃xSx".
But we could have

just as well assumed "(Sb & Rb)" or "(Sc & Rc)"
etc.

The choice of the constant didn't matter in

deriving "∃xSx".
That shows that "∃xSx"
follows

not only from "(Sa & Ra)", but from

"∃x(Sx&Rx)"
as well.

Here is the rule, with all its restrictions:

∃E (Existential Quantifier Elimination)

For any variable v and constant c,

if you have derived
∃vφ, assumed φv/c, and derived ψ,

and c does not occur in ψ, φ, or anything ψ depends on
(except φv/c),

then you can write down ψ a second time, depending on
everything

the first ψ depends on (except the assumption φv/c)
together with

everything
∃vφ depends on.

Here are two examples of misuse of the rule,

to help see how to use it correctly.

In this last example, φ is "Fx", v is "x",

c is "a",
∃vφ
is "∃xFx",
φv/c is "Fa",

and ψ is "(Fa & Ga)". The problem here

is that c occurs in ψ on line 4

("a" occurs in the formula on line 4).

So Rule
∃E
cannot be used this way at

line 5.

Here is another example of an incorrect

use of the rule:

To be sure, this example is not correct,

otherwise you would be able to show

that if something is fat, then everything is fat!

Exercise
2.2a

What restriction of the rule is violated

on line 3 of the last example?

2.3 Soundness and completeness

Our MPL natural deduction system is sound.

You can verify this for yourself, by examining

each of the rules to ensure that the rules only

permit you to write down well-formed formulas

which are entailed by their dependencies.

That the system as a whole is sound means:

For any MPL formula φ,
if φ,
then φ,

and

For any MPL formula φ,
and list of MPL formulas
X,

if
X φ
then
X φ.

The system is also good for a further reason;

it is complete. That the system is complete means:

For any MPL formula φ,
if φ
then φ.

and

For any MPL formula φ,
and list of MPL formulas
X,

if
X φ
then
X φ.

We won't prove completeness of our MPL system

in this introductory course. But it is useful to

know that the system is complete.

In SL you can use the truth table method

to determine whether or not a particular SL formula

is valid. But in MPL you cannot rely on the truth

table method to determine whether or not an MPL

formula is valid. You need some other method.

Since the natural deduction is system for MPL

is complete, if an MPL formula is valid, there is

a derivation of the formula using the system.

Exercise 2.3a

Show that "∀x(Fx→Fx)"
is valid in two different ways.

Exercise
2.3b

Suppose you try to find a derivation of a certain MPL

formula, but you do not succeed in finding a derivation.

Does it follow that that formula is not valid?

2.4 Practice

Exercise
2.4a

Show
the following:

∀xHx
⊢
Ha

∀xHx, (Hc
→
∃xGx)
⊢
∃xGx

∀x(Hx→Mx),
∀xHx
⊢
∀xMx

Ha
⊢
∃yHy

(Ab
→
Dc)
⊢ (Ab
→
∃xDx)

∃x(Fx
&
Gx)
⊢
∃xFx

∀x(Fx→∀yGy)
⊢
∀x∀y(Fx→Gy)

∀x(Px→Qx),
∀x(Qx→Px)
⊢
∀x(Px↔Qx)

∃x~Px
⊢
~∀xPx

(∃xPx→∀x(Qx→Rx)),
(Pa&Qa)
⊢
Ra

(∀x(Px→Qx)→∃x(Rx&Sx)),
(∀x(Px→Sx)&∀x(Sx→Qx))
⊢
∃xSx

(∀x(Px&~Qx)→∃xRx),
~∃x(Qx∨Rx)
⊢
~∀xPx

(∃x~Px→∀x~Qx),
(∃x~Px→∃xQx),
∀x(Px→Rx)
⊢
∀xRx

~∃x(Px∨Qx),
(∃xRx→∃xPx),
(∃xSx→∃xQx)
⊢
~∃x(Rx∨Sx)