HOW
TO START A DIRECT DERIVATION
Remember
that in a valid argument in which there is no contradiction in the
premises we are saying that the conclusion is somehow already present
in the premises. What we have then is a type of detective story
in which we need to release it, typically by using one or another of
our three key inference rules. Imagine you are a detective hired
to find where a missing person is being held, and you have been given a
set of clues. The conclusion is the missing person and the
premises are the clues. Let's look at an example.
P -> (Q v R), ~(~P
v S), ~R |- Q
Begin by looking to see where you find Q in the premises. It's
there with the expression Q v R,
and if I knew first that the entire expression is true I know that with
that ~R I could eliminate
the wedge and have Q by
itself. But how will I find it true? Here I see that If I
knew P is true I'd be in
business. I do find ~P
in the second premise, and now I know that with that curl in front I
could get finally get P by
itself.
The derivation will start by listing the premises in order and after
the last reminding us of what we are trying to show true.
1. P -> (Q v R)
2. ~(~P v S)
3.
~R
/ show Q
Now with the next line we go at getting P true all by itself.
4. P &
~S 2,
DM remember you must
indicate the numbers of the lines used as well as the rule
5.
P
4, Simp
now we can go back to the first premise to get Q v R
6. Q v
R 1,5 ,
MP you
have two call lines to indicate for this rule
and finally I can free Q
from its link to R
7.
Q
3,6, DS
When we have arguments with quantifiers often enough we may have the
same patterns, but to work with the inference rules we need to
eliminate the quantifiers.
(x)[Fx -> (Gx v Hx)], ~[~(x)Fx
v (Ex)Jx], (Ex)~Hx |- (Ex)Gx
I f you work your way backwards in the same way as above you'll see
that you want to go quickly to get rid of that Fx in order to get (Gx v Hx). But you also
would know that we will not have something like x here without a quantifier, so
we would want to instantiate that first expression. However,
looking at what else is given, you should spot that existential
quantifier in the third premise. This waves a red flag at us to
make sure we do not violate the new name rule.
Let's begin with the premises, just as before.
1. (x)[Fx -> (Gx v Hx)]
2. ~[~(x)Fx v (Ex)Jx]
3.
(Ex)~Hx
/ show (Ex)Gx
Now we look to that premise with an existential quantifier.
4.
~Ha
3, EI we are respecting
the new name rule since "a" is not in use so far
Now we see what we need to move forward.
5. (x)Fx &
~(Ex)Jx 2, DM
6. (x)Fx
5, Simp
7. Fa
6, UI
We then go ahead to make this a story about someone named "a" by
instantiating that first premise.
8. Fa -> (Ga v Ha)
1, UI
From here on in we are going through the same steps as we had in the
first example.
9. Ga v
Ha
7,8, MP
10.
Ga
4,9, DS
And since we need to end up with a quantified expression we finish by
introducing the existential quantifier.
11.
(Ex)Gx
10, EG
Now not all arguments can be worked through with a direct derivation,
but it is the technique you should think of first before going to
anything else.