4

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.

Improve this question

2 Answers 2

Reset to default
4

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
Improve this answer
2
  • 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
    Commented 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.
    – Hunan Rostomyan
    Commented Apr 28, 2015 at 5:19
0

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.

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/

Improve this answer

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .