1. ## Derivation Error

Pr1. $\displaystyle \exists x Fx \rightarrow \forall x Gx.$

Pr2. $\displaystyle \forall x (Gx \vee Hx) \rightarrow \forall x Jx.$

C. $\displaystyle \forall x (Fx \rightarrow Jx).$

1. Show $\displaystyle \forall x (Fx \rightarrow Jx)$

2. ... Show $\displaystyle Fx \rightarrow Jx$

3. ...... $\displaystyle Fx$ ASS CD

4. ...... Show $\displaystyle Jx$

5. ......... $\displaystyle \neg Jx$ ASS ID

6. ......... $\displaystyle \exists x Fx$ 3 EG

7. ......... $\displaystyle \forall x Gx$ Pr1 6 MP

8. ......... $\displaystyle Gx$ 7 UI

9. ......... $\displaystyle Gx \vee Hx$ 8 ADD

10. ......... Show $\displaystyle \forall x (Gx \vee Hx)$

11. ............ $\displaystyle Gx \vee Hx$ 9 R

12. ............ 11 UD (ERROR: x appears free in an antecedent line)

13. ......... $\displaystyle \forall x Jx$ Pr2 10 MP

14. ......... $\displaystyle Jx$ 13 UI

15. ......... 5 14 ID

16. ...... 4 CD

17. ... 2 UD

The above is my attempted solution. How do I fix the error at line 12?

2. ## Re: Derivation Error

First, you don't need reasoning by contradiction in step 5. The outline of the derivation is the following: you assume Fx is step 3, derive Jx in step 14, close Fx to get Fx -> Jx and introduce the universal quantifier. The assumption 5 has not been used until step 14, and it is not needed after that.

Concerning step 12, you need to start proving $\displaystyle \forall x\, (Gx \vee Hx)$ before instantiating $\displaystyle \forall x\,Gx$ in step 8. To prove $\displaystyle \forall x\, (Gx \vee Hx)$, you fix some x, instantiate $\displaystyle \forall x\,Gx$ with that x, add the second disjunct and then do universal introduction (UD).

3. ## Re: Derivation Error

emakarov, could you please show me how you would prove Ax (Gx v Hx)? I don't quite understand what you mean by "fix some x and instantiate AxGx with that x."

I have solved the problem using an entirely different method, i.e., quantifier negation, but it would be helpful if you could show me your way.

Thanks.

4. ## Re: Derivation Error

I have not worked with this notation, so the following is probably not completely correct, but it shows the idea.

Code:
7.  ......... ∀x Gx Pr1 6 MP

8.  ......... Show ∀x (Gx ∨ Hx)

9.  ............ Show Gx ∨ Hx

10. ............ Gx 7 UI

11. ............ Gx ∨ Hx 8 ADD

12. ......... 11 UD

13. ......... ∀x Jx Pr2 12 MP

etc.
You proved ∀x Gx in step 7, and now you need to prove ∀x (Gx ∨ Hx) to use Pr2. Currently, there are no suitable objects to instantiate x with in ∀x Gx. When you start proving ∀x (Gx ∨ Hx), you fix some x (the first step in the proof of a universal statement) and with that particular x you instantiate ∀x Gx.