Direct derivations

involve a step-by-step movement from a set of assumptions to an intended conclusion.  They are not the only way in which we show that a given wff would be "true" if other wff's are "true," and there will be many argument forms for which we must use other techniques.  But these let us get started.

Let's review the set of rules we have proposed so far.

p, q |- p&q     & int
p & q |- p       & elim
p |- p v q         v int
p v q, ~p |-q     v elim
p = ~~p           DN
p -> q, p |- q   -> elim
Ax(Fx) |- Fa    UQ elim
Fa |- Ex(Fx)    EQ int

A derivation or proof will have numbered lines with a justification for the wff in each line (just as in our original game, in the very first exercise you did).

Here is your first sample derivation.    The argument form we want to prove valid
is A -> B, ~B v C, A & D |- C

1.  A->B      Ass
2.  ~B v C    Ass
3.  A & D    Ass
4.  A             3  & elim
5.  B             1,4  -> elim
6.  ~~B         5  DN
7.  C             2,6  v elim

Here is a second.   Ax((Fx & Gx) -> Hx), Fa, Ax(Gx) |- Ex(Hx)

1.  Ax((Fx & Gx) -> Hx)    Ass
2.  Fa                                   Ass
3.  Ax(Gx)                           Ass
4.  (Fa & Ga) -> Ha            1  UQ elim
5.  Ga                                   3  UQ elim
6.   Fa & Ga                        2,5   & int
7.   Ha                                  4,6   -> elim
8.   Ex(Hx)                           7   EQ int
 

Practice exercises

Attempt derivations for the following argument forms.  Submit your answers to your instructor through this email address: dmcf@schoolmail.com

(A v B) -> C, D -> A, D |- C v E
Ax(Fx & Gx),  Fa -> Hb,  Gb -> Jc  |-  Ex(Hx) & Ex(Jx)

Follow the examples above for the way in which to show your steps.