Predicate calculus (formal deduction vs resolution) [closed]

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

closed as unclear what you're asking by Mauro ALLEGRANZA, kjetil b halvorsen, TZakrevskiy, N. F. Taussig, drhabApr 7 '15 at 11:02

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• What you mean by "use the 11 rules" is Hilbert calculus, right? If that's the case you should post exactly the axioms that you are using, as Hilbert can be expressed in different ways. – Sara Apr 6 '15 at 9:39
• I'm voting to close this question as off-topic because there are severe formatting problems, the post is unreadable. – kjetil b halvorsen Apr 7 '15 at 9:33

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.

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.