Inference Proof for Biconditional

Question

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.

Answer 1

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}

Answer 2

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

2 $(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.

3 $(¬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.

4 $[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.

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

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

6 $(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).

---

$\def\fitch#1#2{{\quad\begin{array}{|l}#1\\\hline#2\end{array}}}$

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