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.