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 $$


$$\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.

  • 1
    $\begingroup$ In what way does it not display correctly? Simply deleting "format" from the LaTeX produces a reasonable display for me. In particular, it looks basically identical except that the bars above $[P]$ are not as wide (since they don't need to stretch to contain "format"). $\endgroup$ – Derek Elkins Jul 7 at 10:13
  • 2
    $\begingroup$ Your attempt are essentially correct. Just a clarification: which rules do you use for negation introduction and elimination? You seem to use them in a non-uniform way. $\endgroup$ – Taroccoesbrocco Jul 7 at 10:33
  • $\begingroup$ Thank you for the comments.On my display, if i do not add something to the 'fraction',in my case it is the word 'format', the sentence in the denominator is too high..so i am 'pushing it down :-). I do not understand what you mean @Taroccoesbrocco, just the oridinary ones...i think? $\endgroup$ – HalfAFoot Jul 7 at 11:21
  • $\begingroup$ Use \lower{1.5ex}{P\lor Q} to have the statement lowered to the same level as the denominator of the fractions. @HalfAFoot $\endgroup$ – Graham Kemp Jul 7 at 13:11

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}$$


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}$$

  • $\begingroup$ my goodness...... $\endgroup$ – HalfAFoot Jul 7 at 15:19

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.