How can I solve the Disjunctive Syllogism P ∨ Q , -Q ⊢ P

Question

I am trying to figure this out but am stuck. I've gotten this far:

1(1) PvQ A

2(2) -Q A

3(3) Q A

2,3(4) -Q^Q 2,3 ^I

Am not sure how to derive P using propositional logic rules. (-E,-I,->I,->E,^I,^E,vI,vE)

Answer 1

You appear to be aiming for a vE proof. Good.

It is trivial that $P$ may be derived from an assumption of $P$.

What you need to show is that $P$ may be derived from the premised $\lnot Q$ and assumed $Q$.

The rules you list do not contain explosion (ex falso quodlibet) or double negation elimination. In order to proceed, I am presuming that your negation elimination rule is implemented as proof by contradiction (assuming a negated proposition derives a contradiction, therefore the proposition).

$$\dfrac{\lnot P\vdash \lnot Q\land Q}{\vdash P}{\small(\lnot\mathsf E)}$$

If this is your implementation, then since you have derived a contradiction, you just need to assume $\lnot P$ so as to discharge it.

$$\begin{array}{rcllrcl}1 & (1) & P\vee Q & \mathsf A &P\vee Q&\vdash& P\vee Q \\ 2 &(2)& \lnot Q& \mathsf A & \lnot Q&\vdash&\lnot Q \\ 3&(3)& Q& \mathsf A& Q&\vdash&Q \\ 2,3&(4)& \lnot Q\wedge Q &2,3~{\wedge}\mathsf I&\lnot Q,Q&\vdash&\lnot Q\wedge Q \\ 5&(5)& \lnot P& \mathsf A& \lnot P&\vdash&\lnot P \\ 2,3&(6)& P & 5,4~\lnot\mathsf E & \lnot Q, Q&\vdash& P \\&\vdots& \end{array}$$

Now you can complete the disjuction elimination.

Answer 2

I'm not sure, if these rules are the ones you are asking for, but let's try. I can see two approaches.

1. Using $\cfrac{\Gamma, A \vdash \Delta}{\Gamma \vdash \lnot A, \Delta} \quad ({\lnot}R)$ and ${\displaystyle {\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})} $ one obtains:

   1.1 ${P\lor Q,\neg Q \vdash P}$

   1.2 ${P\lor Q \vdash P,Q}$ from 1.1 by $({\lnot}R)$

   1.3 ${P\lor Q \vdash P\lor Q}$ from 1.1 by $({\lor }R_{2})$

   and 1.3 fits axiom schema.

2. Using ${\cfrac {\Gamma ,A\lor B\vdash \Delta }{\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }}$ $({\displaystyle L\lor})$ we get two axioms $Q, \lnot Q\vdash P$ and $P\vdash P$.

3. Not really a solution, but if you are not in the mood for formalisms, and the formula is concerning classical logic (Gentzen's LK), then "$A_1,..,A_n\vdash B_1,..,B_k$ is a theorem" translates to "$(A_1 \land .. \land A_n)\implies(B_1\lor .. \lor B_k) $ is a tautology".

Edit: here is a proof from https://proofs.openlogicproject.org/ :