1. ## Herbrand Logic

Given $\forall x.(p(x) \implies q(x))\quad and \quad p(a)$ use the Fitch system to prove q(a)

I have started:

$1) \forall X.(p(X) \implies q(X)) \qquad (Premise)\\2) p(a) \qquad (Premise)\\3) \exists X.p(X) \qquad (Existential \quad Introduction:2)$

but I do not know how to continue. I believe I must prove also $\forall x.(p(x) \implies q(a))$ and by existential elimination I will get q(a). Can you help me solve it?

2. ## Re: Herbrand Logic

This is much simpler. Instantiate x with a in ∀x (p(x) => q(x)) and then use Modus Ponens (implication elimination) with p(a).

Thanks!