Predicate calculus (formal deduction vs resolution) I am part of the logic club at my school and the question of the week was;
Use formal deduction for predicate calculus to show that the following argument is valid. State each rule you use.
Premise 1: ∀x(F(x) → G(x)) → ∃x(H(x) ∧ ¬I(x)) 
Premise 2: ∀x(H(x) → I(x))
Conclusion: ∃x(F(x)∧¬G(x))
Can anybody help me out? I know I have to use the 11 rules. For the first one I've never seen something with two -->'s before in a row
Thank you
 A: To prove it, it is enough to contrapose the first premise, getting :

$¬∃x(H(x) ∧ ¬I(x)) \to ¬∀x(F(x) → G(x))$ 

i.e.

$∀x¬(H(x) ∧ ¬I(x)) \to ∃x¬(F(x) → G(x))$.

By the tautological equivalence :  $\lnot (p \land \lnot q) \equiv (p \to q)$, we can see that the antecedent of the conditional is equal to the second premise.
We have to use it to "detach" the consequent by modus ponens, deriving : 

$∃x¬(F(x) → G(x))$.

Using again the abobe tautological equivalence, we can rewrite the last formula as :


$∃x(F(x) \land \lnot G(x))$


which is the conclsion.
A: I believe you would benefit from using the law of contraposition on your first premise.
The law says that the conditional statement $P\rightarrow Q$ is equivalent to $\neg Q\rightarrow \neg P$, and in your case, I would take $P$ to be $\forall x (F(x)\rightarrow G(x))$ and $Q$ to be $\exists x (H(x)\wedge \neg I(x))$.
When you negate $Q$, you get exactly your second premise. Can you see this?
In total, premise 1 is equivalent to $\neg Q\rightarrow\neg P$, and premise 2 is equivalent to $\neg Q$. Thus $\neg P$ is true (by modus ponens), but $\neg P$ is in fact equivalent to your conclusion.
