I'm asked to prove $(p\rightarrow (q \vee r)) \leftrightarrow ((p \wedge \neg q)\rightarrow r)$ using inference rules and I'm not quite sure how to do it. This is what I have so far.

$1 [(p \wedge \neg q) \rightarrow r]\quad$ assume

$2 \space (p) \space\quad\wedge$-elimination (1)

$3 \space (\neg q) \space\quad \wedge$-elimination(1)

$4\space [r] \quad$ assume

$5 \space (q \vee r)$ $\quad\vee$-intro(3,4)

$6 \space(p \rightarrow(q\vee r)) \quad\rightarrow$-intro (2,6)

This only proves the biconditional one way (and I'm not even sure if its correct) and I don't know where to go from here.

  • 1
    $\begingroup$ You can only use ∧ elimination when ∧ is the main connective. (2) and (3) are horribly fallacious! $\endgroup$ Mar 19 '18 at 17:23
  • $\begingroup$ Sorry, can you explain a bit more? I'm terrible at inference proofs. $\endgroup$ Mar 19 '18 at 17:33

Proving $A \leftrightarrow B$ amounts to prove both $A \to B$ and $B \to A$. I will prove both of them using classical natural deduction, which seems to be the formal system you know. Given an inference rule $r$, I will use the notation \begin{align} \dfrac{A_1 \ \dots \ A_n}{B}r \end{align} which means that given the premises $A_1, \dots, A_n$, you can infer the conclusion $B$ by means of the inference rule $r$. So, a derivation in classical natural deduction will be a tree-like concatenation of inference rules in this notation.

Let us prove that $(p\rightarrow (q \vee r)) \to ((p \wedge \neg q)\rightarrow r)$: assume $(p\rightarrow (q \vee r))$, let us prove $((p \wedge \neg q)\rightarrow r)$

\begin{align} \dfrac{\dfrac{\dfrac{p \!\to\! (q \lor r) \quad \dfrac{[p \land \lnot q]^2}{p}\land_e}{q \lor r}\to_e \qquad \dfrac{\dfrac{\dfrac{[p \land \lnot q]^2}{\lnot q}\land_e \qquad [q]^1}{\bot}\lnot_e}{r}\bot_e \qquad [r]^1}{r}\lor_e^1}{(p \land \lnot q) \to r}\to_i^2 \end{align}

Now, let us prove that $((p \wedge \neg q)\rightarrow r) \to (p\rightarrow (q \vee r))$: assume $(p \land \lnot q) \to r$ and let us prove $p \to (q \lor r)$

\begin{align} \dfrac{\dfrac{q \lor \lnot q \qquad \dfrac{[q]^1}{q \lor r}\lor_{i_L} \qquad \dfrac{\dfrac{(p \land \lnot q) \to r \qquad \dfrac{[p]^2 \qquad [\lnot q]^1}{p \land \lnot q}\land_i}{r}\to_e}{q \lor r}\lor_{i_R}}{q \lor r}\lor_e^1}{p \to (q \lor r)}\to_i^2 \end{align}

where $q \lor \lnot q$ is provable in classical natural deduction as follows:

\begin{align} \dfrac{\dfrac{[\lnot (q \lor \lnot q)]^2 \qquad \dfrac{\dfrac{\dfrac{[\lnot (q \lor \lnot q)]^2 \qquad \dfrac{[q]^1}{q \lor \lnot q}\lor_{i_L}}{\bot}}{\lnot q}\lnot_i^1}{q \lor \lnot q}\lor_{i_R}}{\bot}\lnot_e}{q \lor \lnot q}\text{raa}^2 \end{align}

  • $\begingroup$ I understand the general concept of how to do it but not when it comes down to the actual steps $\endgroup$ Mar 19 '18 at 17:34
  • $\begingroup$ Sorry, I'm not really familiar with the format of your answer. $\endgroup$ Mar 19 '18 at 17:48
  • $\begingroup$ @drewdawg7 - See my edit, I tried to explain the formalism I use. Note that I'm using exactly the same inference rules you use, e.g. $\to_i$ stands for $\to$ intro, $\land_e$ stand for $\land$ elimination, etc. $\endgroup$ Mar 19 '18 at 18:18
  • $\begingroup$ Yeah, I get it now! That was really helpful, thank you. $\endgroup$ Mar 19 '18 at 18:22

1 $[(p∧¬q)→r]$ assume

$(p)$ ∧ elimination (1)

No, you cannot eliminate from the antecedant of an implication.   This is another assumptions.   Preferred format would be to indent or otherwise indicate the start of a sub proof (well, I guess you're trying that with the []-brackets.)   An assumption has been made and will later need to be discharged.

$(¬q)$ ∧ elimination(1)

Again, you cannot $\wedge$-eliminate from the antecedant of an implication.   You need $\land$ to be the highest priority in the order of operations. In statement $1$, it is $\to$ that has operational precedence.

This is actually an assumption.

$[r]$ assume

You are not actually assuming this; you appear to be using $\to$ elimination from the prior assumptions: $\{p\wedge \neg q, (p\wedge \neg q)\to r \}~\vdash~r$

Of course, you also missed the step where you used $\wedge$ introduction (not elimination) to obtain $p\wedge\neg q$ from the two preceeding assumptions.

$(q∨r)$ ∨ intro(3,4)

This you have correct, almost, you just need line 4 to obtain this, $r\vdash q\vee r$

$(p→(q∨r))$ → intro (2,6)

Unfortunately with the assumption in line 3 you have $p\to (\neg q\to (q\vee r))$

Before this you should perhaps have used LEM and a $\vee$-elimination to discharge assumptions $q$ and $\neg q$ (since $q\vdash q\vee r$ by $\vee$ introduction also).


You seek to demonstrate that when given the premise of $(p\wedge \neg q)\to r$, assuming $p$ will infer $q\vee r$, thus deducing $p\to(q\vee r)$.   So do just that.   I'd have suggested proof by contradiction, but LEM works too if allowed.

$\fitch{}{\fitch{1\quad (p\wedge\neg q)\to r\qquad\text{assumption}}{\fitch{2\quad p\qquad\text{assumption}}{\fitch{3\quad \neg q\qquad\text{assumption}}{4\quad p\wedge\neg q\qquad\text{conjunction introduction, 2,3}\\5\quad r\qquad\text{conditional elimination, 1,4}\\6\quad q\vee r\qquad\text{disjunction introduction, 5}}\\7\quad\neg q\to (q\vee r)\qquad\text{conditional introduction 3,6}\\\fitch{8\quad q\qquad\text{assumption}}{9\quad q\vee r\qquad\text{disjunction introduction, 8}}\\10\quad q\to(q\vee r)\qquad\text{conditional introduction, 8,9}\\11\quad q\vee\neg q\qquad\text{principle of excluded middle}\\12\quad q\vee r\qquad\text{disjunction elimination, 7, 10, 11}}\\13\quad p\to(q\vee r)\qquad\text{conditional introduction, 2,12}}\\14\quad ((p\wedge\neg q)\to r)~\to~(p\to(q\vee r))\qquad\text{conditional introduction, 1, 13}}$

For the other direction, demonstrate that under the premise of $p\to(q\vee r)$ that assuming $p\wedge\neg q$ will infer $r$, thus deducing $(p\wedge\neg q)\to r$ $$\fitch{}{\fitch{1\quad p\to( q\vee r)}{\fitch{2\quad p\wedge\neg q}{\vdots\\\cdot\quad r}\\\cdot\quad (p\wedge\neg q)\to r}\\\cdot\quad(p\to( q\vee r))~\to~((p\wedge\neg q)\to r)}$$


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.