# Thread: Derivation Error

1. ## Derivation Error

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

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

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

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

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

3. ...... $Fx$ ASS CD

4. ...... Show $Jx$

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

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

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

8. ......... $Gx$ 7 UI

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

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

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

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

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

14. ......... $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 $\forall x\, (Gx \vee Hx)$ before instantiating $\forall x\,Gx$ in step 8. To prove $\forall x\, (Gx \vee Hx)$, you fix some x, instantiate $\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.