Topic DPL: Derivations in predicate logic

1 Derivations in monadic predicate logic

Now you will learn a natural deduction system
for Monadic predicate logic.

1.1 The rules are very similar

We adopt versions of the 12 rules from the natural
deduction system for SL discussed in Topics 1 and 2.
While the old rules applied to SL formulas, these adopted
rules apply to MPL formulas. Otherwise, the rules are
unchanged. This provides rules for all the connectives
of MPL.

Additionally, rules for the quantifiers '∃' and '∀' are
needed. For each quantifier, there is an elimination rule
and an introduction rule. With the four quantifier rules,
that makes 16 rules in all.
Here are all of the rules, if you are in a hurry.

Exercise 1.1a

Explain why rule &E for MPL is a sound rule.

1.2 Rule of Existential Quantifier Introduction

The first quantifier rule is the rule of Existential Quantifier
Introduction. Here is this rule in action to show Sa ∃xSx:

Rule ∃I says that you can take a formula you have
written already, replace one or more occurrences of some
constant in the formula with a new variable, and then attach
the existential quantifier to the front. The dependencies of the
new formula are the same as the old formula.

Notice that ∃I is a sound rule. That means that when
you use the rule, the formula you write down is entailed
by its dependencies. Consider the previous example, where
the rule is used at line 2. Note that for any interpretation under
which "Sa" is true, "∃xSx" is true under that interpretation too.

Exercise 1.2a

Explain why for any interpretation under which
"Sa" is true, "∃xSx" is true too.

Here is another example of ∃I in action:

Two details should be noted in using ∃I.
The first detail is that ∃I applies to the whole
formula, not to part of the formula. That means
that the quantifier is added at the beginning of the
formula, not in the middle. Thus, for example,
the following derivation is incorrect:

If you could do this, then rule ∃I would not be sound
because you could write down a formula which is not
entailed by its dependencies. Line 2 is not entailed by
its dependency, line 1. Take an interpretation under
which "Sa" and "Ab" are false, but "Sb" is true. This is
an interpretation under which "(Sa → Ab)" is true and
"(∃xSx → Ab)" is false. So "(Sa → Ab)" does not entail
"(∃xSx → Ab)".

So, remember: when using ∃I, the existential quantifier
must be added to the front of the formula. The following
is an example of a similar, but correct derivation:

Exercise 1.2b

Show (Fa & Ga) ⊢ (∃xFx & Ga)

The second detail to be noted about ∃I
is that that the formula you write down must
be a well-formed formula of MPL. Thus, for
example, the following derivation
is not correct:

The derivation is not correct because the formula
on line 2 is not a well-formed formula of MPL.
The variable 'x' already occurs in line 1, so you
cannot use the variable 'x' in applying ∃I. You need
to choose a different variable. You could, for instance,
use 'y' instead:

In using ∃I you always need to choose a new
variable or the expression you write down
will not be a well-formed formula.

Exercise 1.2c

Explain why "∃x(∃xSx & Rx)" is not a well-formed
formula of MPL.

On the list of rules, Rule ∃I is stated precisely
using some shorthand symbolism:

∃I (Existential Quantifier Introduction)
For any variable v and constant c,
if you have derived φv/c,
and ∃vφ is a well-formed formula of MPL,
then you can write down ∃vφ,
depending on everything φv/c depends on.

This statement of the rule uses the symbolism
"φv/c". This symbolism is a shorthand
which makes it simpler to state the quantifier
rules. As we will be using it, "φv/c" means that
you take an expression φ and replace all
occurrences of v with c. For example,
if φ is "(Fx&Fb)", v is "x" and c is "a", then
φx/a is "(Fa&Fb)". If v is "x" and c is "b"
then φx/b is "(Fb&Fb)".

Exercise 1.2d

State Rule ∃I without the shorthand symbolism.

1.3 Rule of Universal Quantifier Elimination

A second straightforward rule for the quantifiers is
the rule of universal quantifier elimination, ∀E:

∀E (Universal Quantifier Elimination)
For any variable v and constant c,
if you have derived ∀vφ,
then you can write down φv/c,
depending on everything ∀vφ depends on.

This rule is easy to use. For instance:

Or, another example:

However, the following is incorrect:

This is incorrect because line 1 is a conjunction,
not a formula beginning with a universal quantifier.
Since the formula on line 1 does not begin with
a universal quantifier, ∀E does not apply. ∀E only
applies to formulas beginning with a universal
quantifier.

Exercise 1.3a

Explain why Rule ∀E is a sound rule.

1.4 An example

Here is an example of a derivation in MPL using
rules you have learned so far:

This shows (Sb→∀xEx), ~Ea ~∀xSx .

Exercise 1.4 a

Find a shorter derivation showing that (Sb→∀xEx), ~Ea ~∀xSx .