# Inference Proof for Biconditional

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.

• You can only use ∧ elimination when ∧ is the main connective. (2) and (3) are horribly fallacious! – Peter Smith Mar 19 '18 at 17:23
• Sorry, can you explain a bit more? I'm terrible at inference proofs. – NotSoTuringComplete 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}

• I understand the general concept of how to do it but not when it comes down to the actual steps – NotSoTuringComplete Mar 19 '18 at 17:34
• Sorry, I'm not really familiar with the format of your answer. – NotSoTuringComplete Mar 19 '18 at 17:48
• @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. – Taroccoesbrocco Mar 19 '18 at 18:18
• Yeah, I get it now! That was really helpful, thank you. – NotSoTuringComplete 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).

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