Logic Proof using Inference rules and replacement rules

Question

I am trying to prove the following using the inference and replacement rules in logic:

(A . F) ⊃ (C ∨ G), ~ (C ∨ (F . G)), F ≡ ~ (X . Y), ~ (X ∨ ~ W) /∴ ~ (A ∨ X)

I have this so far:

Work

But I do not know where to go. Any help would be greatly appreciated.

Answer 1

I won't write out an exact natural deduction proof since that seems to be the purpose of the exercise. Also, you haven't actually listed your axioms. You could translate the following outline of a proof into the a natural deduction proof though (assuming you have some version of the excluded middle as an axiom):

From $\lnot (C \lor (F \land G))$ derive 2 propositions, $\lnot C$ and $\lnot F \lor \lnot G$.

From $\lnot C$ and $(A \land F) \implies (C \lor G)$ derive $(A \land F) \implies G$.

From $\lnot (X \lor W)$ derive 2 propositions, $\lnot X$ and $\lnot \lnot W$.

From $F = \lnot (X \land Y)$ derive $(\lnot X \lor \lnot Y) \implies F$. From $\lnot X$ and previous derive $F$.

From $F$ and $\lnot F \lor \lnot G$ derive $\lnot G$. From $\lnot G$, $F$ and $(A \land F) \implies G$ derive $\lnot A$.

From $\lnot A$ and $\lnot X$ derive $\lnot (A \lor X)$.

For some of these, you may need to derive intermediary results, like Demorgans.