Quick question regarding alternative solutions to Natural deduction problem

Question

Could someone verify that the following alternative attempts are both correct in the proof of the problem?

$$\{P \lor \neg Q , R \rightarrow \neg P \} \vdash Q \rightarrow \neg R $$

Attempt:

$$\cfrac{\cfrac{format}{P \lor \neg Q} \qquad \cfrac{\cfrac{\cfrac{[R] \quad R \rightarrow \neg P}{\neg P} \qquad \cfrac{format}{[P]}}{\neg R}}{Q \rightarrow \neg R} \qquad \cfrac{\cfrac{[Q] \quad [\neg Q]}{\neg R}}{Q \rightarrow \neg R}}{Q \rightarrow \neg R}$$

Alternative attempt: $$\cfrac{\cfrac{\cfrac{format}{P \lor \neg Q} \qquad {\cfrac{\cfrac{format}{[P]} \quad \cfrac{[R] \quad R \rightarrow \neg P}{\neg P}}{\neg R}} \qquad \cfrac{[Q] \quad [ \neg Q]}{\neg R}}{\neg R}}{Q \rightarrow \neg R}$$

I had to add the word 'format' in the 'fractions' because i could not get the formatting to display correctly,sorry.I know the first attempt is correct and i was wondering if the alternative is correct too.

Thank you for your help.

Answer 1

You shouldn't have any statements with a blank line over them, like $$\dfrac{}{P \lor \lnot Q}$$ Every line represents an invocation of a rule of inference, and there is no general rule of inference to infer $P \lor \lnot Q$. It is just an assumption. Instead it should just be

$$\dfrac{[P \lor \lnot Q] \qquad \dots}{\dots}$$

Same for the other blank lines. Otherwise both proofs are correct.

---

Just to be clear, it is sometimes appropriate to have blank lines. For example, if you have "the law of the excluded middle", then it would be appropriate to have

$$\dfrac{\dfrac{}{Z \lor \lnot Z} \qquad \dots}{\dots}$$

Because $Z \lor \lnot Z$ is axiomatic, it isn't some arbitrary assumption.

Answer 2

You should include the rules of inference used to justify the derivations, and also make sure you have matched the schema for your particular proof system (there are many variations).

If your version of "disjunction elimination" requires conditionals, then your first attempt needs to deduce $P\to\lnot R$ and $\lnot Q\to\lnot R$; since you are eliminating $P\lor\lnot Q$, after all.   Then you eliminate the assumption of $Q$ with conditional introduction.

$$\dfrac{\dfrac{\lower{1.5ex}{P\vee\lnot Q}\quad\dfrac{\dfrac{\lower{1.5ex}{[P]^3}\quad\dfrac{[R]^4\quad R\to\lnot P}{\lnot P}{\small\to\!\mathsf E}}{\lnot R}{\small\lnot\mathsf I^4}}{P\to\lnot R}{\small\to\!\!\mathsf I^3}\quad\dfrac{\dfrac{[\lnot Q]^2\quad [Q]^1}{\lnot R}{\small\lnot\mathsf E}}{\lnot Q\to\lnot R}{\small\to\!\mathsf I^2}}{\lnot R}{\small\vee\mathsf E}}{Q\to\lnot R}{\small\to\!\mathsf I^1}$$

---

However

I notice that you appear to be using a variant of the negation introduction and elimination rules which do not use the $\bot$ symbol; skipping out the explicit "these statements are a contradiction" step (more usually called negation elimination).   That version of negation elimination rule is basically ex falso quodlibet. $$\dfrac{\phi\quad\lnot\phi\quad [\rho]^\bullet}{\lnot\rho}{\small\lnot\mathsf I^\bullet}\qquad\dfrac{\phi\quad\lnot\phi}{\psi}{\small\lnot\mathsf E}$$

If this is intentional, it is quite okay, and does admittedly save space, rather than:$$\dfrac{\dfrac{\phi\quad\lnot\phi}{\bot}{\small\lnot\mathsf E}\quad\lower{1.25ex}{[\rho]^\bullet}}{\lnot\rho}{\small\lnot\mathsf I^\bullet}\qquad\dfrac{\dfrac{\phi\quad\lnot\phi}{\bot}{\small\lnot\mathsf E}}{\psi}{\small\mathsf{EFQ}}$$

If so, this does suggest to me that your version of "disjunction elimination" would likewise also skip the conditional introduction step, and just require the subproofs to derive the same conclusion: $\lnot R$. That is, your second attempt.

$$\dfrac{\dfrac{\lower{1.5ex}{P\vee\lnot Q}\quad\dfrac{\lower{1.5ex}{[P]^3}\quad\dfrac{[R]^4\quad R\to\lnot P}{\lnot P}{\small\to\!\mathsf E}}{\lnot R}{\small\lnot\mathsf I^4}\quad\dfrac{[\lnot Q]^2\quad [Q]^1}{\lnot R}{\small\lnot\mathsf E}}{\lnot R}{\small\vee\mathsf E^{2,3}}}{Q\to\lnot R}{\small\to\!\mathsf I^1}$$