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

Question

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.

Thank you all in advance!

Answer 1

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.