proof for relational predicate logic

Question

I have been working on this problem for over an hour and I think I have simply missed something. I need some help. The rules I am allowed to use are the Basic Inference rules (MP, MT, HS, Simp, Conj, DS, Add, CD), the Replacement Rules (DN, Comm, Assoc, Dup, DeM, BE, Contrap, CE, Exp, Dist.), CP, IP, and EI, UI, EG, UG.

The problem is:

1. ¬(∃x)(Axa ∧ ~Bxb)
2. ¬(∃x)(Cxc ∧ Cbx)
3. (∀x)(Bex → Cxf)

/∴ ¬(Aea ∧ Cfc)

Any help would be appreciated. Thanks.

Edit: Fixed the format of the question. The system is quantificational predicate logic. I've never called it anything else.

Answer 1

It is useful to have a proof checker to aid learning how to use natural deduction. I have linked to one below in the references.

Using that proof checker and the rules described in forallx I was able to prove the result in 22 lines which included 3 lines for the premises and 1 line for the goal.

Although I don't see it listed I assume you have the change of quantifier replacement rule. If not a derivation is in forallx on pages 260-1. Use that to change the first two premises from "~(∃x)" to "(∀x)~".

Next eliminate the universal quantifier by assigning a different name to the variable "x" in each premise. You should chose these names wisely. Look at the goal to try to pick names that will help you reach the goal.

Then use De Morgan rules to transform the lines with a negation in front of the conjunction to a disjunction of negations.

After that preparatory work, I derived something like the following line: "¬Aea ∨ ¬¬Beb". I used disjunction elimination by considering both cases. I wanted to reach the following: "¬Aea ∨ ¬Cfc". Now that is not quite the desired result but with a use of the De Morgan rules I could convert that into the final goal: "¬(Aea ∧ Cfc)".

---

References

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/

Answer 2

Use an Indirect Proof.

Begin by assuming (Aea ∧ Cfc), use the first premise to derive Beb, the third to derive Cbf, and the second to derive a contradiction.

Some of your subproofs will likewise be Indirect Proofs; using existential generalisation to derive their contradictions.

Assuming, that the thing you call IP operates as expected (derive a contradiction from an assumption, thereby deducing that the negation of the assumption holds).