# Fitch style disjunction elimination

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

``````P(x) v Q(x)
not P(x)
----------
Q(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)
| ----
|| ??
|??
---------
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.

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 '15 at 5:09
• 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. – Hunan Rostomyan Apr 28 '15 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". Using truth-function logic this would be simpler: 