I am having difficulty in formally proving a simple argument. Consider

P(x) v Q(x)
not P(x)

It is easy to see that the argument is indeed valid, but I cannot seem to prove it formally. Here is one attempt:

P(x) v Q(x)
not P(x)
|| P(x)
| ----
|| _|_     _|_ intro 2,3
|| Q(x)
| ----
|| ??

I am obviously stuck on a basic proof, and I would appreciate any pointers. I am used to the Fitch style notation and make use of an application called 'Fitch' to do formal proofs, so I would appreciate guidance in the parlance of Fitch.

2 Answers 2


A summary of the rules can be found here.

1. P(x) v Q(x)    hyp
2. ~P(x)          hyp

3. | P(x)         hyp
4. | ⊥            ⊥ Intro 2, 3
5. | Q(x)         ⊥ Elim, 4

6. | Q(x)         hyp
7. | Q(x)         Reit 6

8. Q(x)           v Elim, 1, 3-5, 6-7
  • as I said, I don't know Fitch per se. But this is the idea. vE seems painful this way. Fitch has never heard of disjunctive syllogism?
    – virmaior
    Apr 28, 2015 at 5:09
  • 1
    As you know, different systems take different rules/axioms as primitive. So long as the system is complete with respect to the standard semantics, I don't think it's a flaw of the system that it doesn't take disjunctive syllogism (= the thing we're proving here) as a primitive rule. Apr 28, 2015 at 5:19

I agree with Hunan Rostomyan's answer using disjunction elimination (vE) as well as virmaior's comment, "vE seems painful this way. Fitch has never heard of disjunctive syllogism?"

Here is a proof that uses disjunctive syllogism. As a proof this also illustrates that one has to follow the rules for well-formed statements built into whatever proof checker one is using so it can generate an answer.

In my case, the Fitch-style proof checker refused to accept the premises or conclusion as well-formed in first-order logic without the "x" being quantified. So, I added universal quantification of "x" on the premises and conclusion. This required that I first eliminate the universal quantifier, then use disjunctive syllogism (DS) and then introduce the universal quantifier.

The proof checker I am using is not the same one the OP is using. This may introduce other differences. For example, I could not use notation such as "P(x)", but I had to use "Px".

enter image description here

Using truth-function logic this would be simpler:

enter image description here

For more information on the rules see forall x: Calgary Remix.


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/

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.