Proving a reasoning sentence by the help of natural deduction rules for propositional logic

I have a reasoning sentence that I am supposed to prove that is valid by the help of natural deduction rules for prepositional logic. Here is the reasoning sentence to be proved:

“If Jennifer does not come to the party, then John will come to that party. If John comes to the party, then also James will come to that party. If both John and James are on the party, then Jennifer will not come to the party. Then it is concluded that either John is at the party but not Jennifer, or Jennifer is at the party but not John.”

Let the variables p, q and r represent the following declarative sentences:

p: Jennifer is at the party

q: John is at the party

r: James is at the party

(Could someone help me with the formatting the logical symbols so it will be more clear to read? Thanks in advance!)

Firstly, I need to rewrite the whole reasoning sentence as a logical sequent. This is the following sequent I have written:

¬p->q, q->r, (q^r)-> ¬p |- (q^¬p)v(¬q^p)

Then I have to prove this that this is valid. Here is my attempt to prove the whole logical sequent:

1. ¬p->q premise
2. q->r premise
3. (q^r)-> ¬p premise
4. q assumption
5. r ->e 4, 2
6. (q^r) ^i 4, 5
7. ¬p ->e 6, 3
8. p assumption
9. falsum ¬e 8, 7
10. ¬q ¬i 4-9
11. ¬¬p MT 1, 10
12. p ¬¬e 11
13. ¬q^p ^i 10, 12
14. (¬p^q)v(¬q^p) Vi(2) 13

But I am not sure if the proof is correct or even if the logical sequent that was formulated by me is correct. I feel it’s like a little too long proof for this size of assignment and I don’t know if there aren’t more efficient ways of proving the reasoning sentence that was mentioned in the beginning question. Could you please check if I have done right or if not, the please tell where I have made mistakes in my attempt to prove that the reasoning sentence is valid.

• It seems to me that there is a problem : assumption $p$ in 8 has not been discharged. – Mauro ALLEGRANZA Sep 20 '15 at 13:39
• That is what I have expected a little. I didnt feel that I have not done right with the "mini" box that represent the rows 8-9. But I am also not sure how I can handle with that. Or if my proof technique is correct at all... :/ – user2566415 Sep 20 '15 at 13:44

A general point. We need to prove a disjunction $C \lor D$. How can we prove a disjunction if it isn't already a component of one of the premisses we could e.g. extract by a modus ponens or something like that? There are two promising strategies (options that should work, if not ideally elegantly):

1. Find a disjunction $A \lor B$, show that $A$ proves $C$ and hence $C \lor D$, show that $B$ proves $D$ and hence $C \lor D$, and use $\lor$-elimination.
2. Brute force: assume $\neg (C \lor D)$, and aim for a reductio.

So that's the general advice. How does it work out in this particular case?

Let's try (1): ok we haven't a dijunctive premiss to play the role of $A \lor B$, but we can always supply one, i.e. a suitable instance of excluded middle. So here goes. You need to fill in the dots with a proof from no premisses of $p \lor \neg p$, assuming that the law of excluded middle isn't given as a basic rule in your natural deduction system: but that's a routine derivation.

$¬p \to q\\ q \to r\\ (q \land r) \to ¬p\\ \vdots\\ p \lor \neg p\\ \quad\mid\quad p\\ \quad\mid\quad\quad\mid\quad q\\ \quad\mid\quad\quad\mid\quad r\\ \quad\mid\quad\quad\mid\quad (q \land r)\\ \quad\mid\quad\quad\mid\quad \neg p\\ \quad\mid\quad\quad\mid\quad \bot\\ \quad\mid\quad \neg q\\ \quad\mid\quad (\neg q \land p)\\ \quad\mid\quad (q \land \neg p) \lor (\neg q \land p)\\ \quad --\\ \quad\mid\quad \neg p\\ \quad\mid\quad q\\ \quad\mid\quad (q \land \neg p)\\ \quad\mid\quad (q \land \neg p) \lor (\neg q \land p)\\ (q \land \neg p) \lor (\neg q \land p)\\$

Here's how to do the proof by method (2) reductio: it looks (unsurprisingly) rather similar, using many of the same ideas!

$¬p \to q\\ q \to r\\ (q \land r) \to ¬p\\ \quad\mid\quad\neg(q \land \neg p) \lor (\neg q \land p)\\ \quad\mid\quad\quad\mid\quad p\\ \quad\mid\quad\quad\mid\quad\quad\mid\quad q\\ \quad\mid\quad\quad\mid\quad\quad\mid\quad r\\ \quad\mid\quad\quad\mid\quad\quad\mid\quad (q \land r)\\ \quad\mid\quad\quad\mid\quad\quad\mid\quad \neg p\\ \quad\mid\quad\quad\mid\quad\quad\mid\quad \bot\\ \quad\mid\quad\quad\mid\quad \neg q\\ \quad\mid\quad\quad\mid\quad (\neg q \land p)\\ \quad\mid\quad\quad\mid\quad (q \land \neg p) \lor (\neg q \land p)\\ \quad\mid\quad\quad\mid\quad \bot\\ \quad\mid\quad \neg p\\ \quad\mid\quad q\\ \quad\mid\quad (q \land \neg p)\\ \quad\mid\quad (q \land \neg p) \lor (\neg q \land p)\\ \quad\mid\quad \neg(q \land \neg p) \lor (\neg q \land p)\\ \neg\neg(q \land \neg p) \lor (\neg q \land p)\\ (q \land \neg p) \lor (\neg q \land p)\\$

It will be a useful reality check to think through why, at each step, once you've chosen between using the two overall strategies, you really do the only sensible thing at each stage of the proof.

• Okay, everything with your solutions make sense, I should have thought about the LEM rule you have applied on row 3 (after the dots) in your first solution. But I was uncomfortable with using it and instead tried to keep with using rules I felt more confident with. I hoped that I was close to the real solution of proving the logical sequent, but now it has turned out that I was not :/ Anyway, thank you for helping me with proving this logical sequent! I hope that you haven't put too much effort on this :) – user2566415 Sep 20 '15 at 18:41
• Careful. I didn't use the LEM rule in the first proof (not a basic rule in many natural deduction systems). Rather the idea is that you prove $p \lor \neg p$ using the other rules that are basic in your system. – Peter Smith Sep 20 '15 at 18:48
• Okay, what does the logical expression on row 3 in your first proof present? Isn't the LEM rule valid specifically for the natural deduction in propositional logic? I hope it doesn't mind if I ask questions, even the silly ones :) – user2566415 Sep 20 '15 at 18:54
• Sorry if I was a little unclear. What I meant was that I wasn't invoking LEM as a basic rule (I'm assuming it isn't a basic rule of your natural deduction system). So you can't just appeal to it in a proof in your system. It will, however, be a valid derived rule of course, in the sense that any instance of LEM can be derived from the other rules. The vertical dots, as I said, were there to hold the place of such a derivation. – Peter Smith Sep 20 '15 at 19:12
• Okay, now I understand. Thank you for taking your time to explain this detail for me :D – user2566415 Sep 20 '15 at 19:56