I'm having trouble understanding writing out a proof. The proof I'm trying to work with is :

enter image description here

How do I reach this goal? Which rules do I use and with which support steps to each rule (proofs to prove each step?) Using only inference rules, reit, quantifier rules.

  • 1
    Do not edit out the question once you have an answer. (Though you should replace the image with text, you should not just delete it to leave no context for future readers..) Jun 7, 2019 at 2:14

2 Answers 2


This is only a description of the justifications for the steps. How you describe the justifications in the proof checker will depend on that tool.

Lines 5 and 6 used universal elimination to replace the variable x with the name a. You will likely need to reference which lines were used.

Line 8 used conditional elimination which should reference the conditional on line 6 and its antecedent on line 7. This gives you the consequent.

Similarly line 9 used conditional elimination which should reference the conditional on line 5 and its antecedent on line 8. This allows you to derive the consequent.

Line 10 derives the contradiction between lines 9 and 4. This is contradiction introduction.

Line 11 derives the negation of the assumption on line 7 discharging the subproof on lines 7 to 10. This is negation introduction.

Line 12 uses existential introduction. This is copied to the last line where existential elimination was used. This existential elimination began with the assumption on line 4 replacing the variable x in line 3 with the name a. This subproof was able to be closed when a line was derived that did not use the name a. That happened on line 12.


Here is a complete proof with all steps justified in the Fitch program. enter image description here

You must log in to answer this question.