# Understanding $\lor~E$ in Natural Deduction?

I'm reading Frank Pfenning's Lecture Notes on Natural Deduction. It's reasonable that the following $$\lor$$-elimination rule is incorrect since we can have any theorem $$\alpha$$ given a single theorem $$\beta$$.

$$\begin{array}{c} \alpha \lor \beta\\ \hline\hline \alpha \end{array}$$

The real $$\lor$$-elimination rule is given by:

$$\begin{array}{c} \alpha \lor \beta \quad [\alpha] \cdots \psi \quad [\beta] \cdots \psi \\ \hline\hline \psi \end{array}$$

where by $$[\alpha]$$, $$[\beta]$$ is denoted an assumption of both $$\alpha$$ and $$\beta$$. However what prevents someone from doing something like this?

$$\begin{array}{c} \alpha \lor \beta \quad [\alpha] \cdots \alpha \quad [\beta] \cdots \alpha \\ \hline\hline \alpha \end{array}$$

Which looks like the previous mistake (i.e. I want to derive any $$\alpha$$ from a $$\beta$$), but this is a valid inference. How does this differ from the wrong one?

• @MauroALLEGRANZA - I guess the question is about the third rule in the OP. He believes that it is not valid, but actually it is valid. – Taroccoesbrocco Apr 2 at 13:17
• @MauroALLEGRANZA - Exactly! This is what I wrote in my answer. – Taroccoesbrocco Apr 2 at 13:38
• I've edited the question to be more clear. – Aristu Apr 2 at 13:41
• The or elimination rule is just proof by cases. It might be more clear to you if you write it as $$\dfrac{\text{Case}_1 \lor \text{Case}_2 \quad \text{Case}_1 \to X \quad \text{Case}_2 \to X}{X}$$ – DanielV Apr 4 at 3:49

The elimination rule for $$\lor$$

\begin{align} \dfrac{\alpha \lor \beta \qquad [\alpha]\cdots\psi \qquad [\beta]\cdots\psi}{\psi}\lor_e \end{align}

is valid for any formula $$\psi$$, in particular for $$\psi = \alpha$$.

The case $$\psi = \alpha$$ for $$\lor_e$$ is not equivalent to the rule

\begin{align} \dfrac{\alpha \lor \beta}{\alpha} (*) \end{align}

which is unsound because in $$(*)$$ an important hypothesis (present in the rule $$\lor_e$$ with $$\psi = \alpha$$) is missing: that $$\alpha$$ is derivable from the further assumption $$\beta$$. In other words, the rule $$\lor_e$$ in the case $$\psi = \alpha$$ can be rewritten as (since $$\alpha$$ is trivially derivable from the further assumption $$\alpha$$) \begin{align} \dfrac{\alpha \lor \beta \qquad [\beta]\cdots\alpha}{\alpha} \end{align}

which is indeed perfectly derivable in natural deduction.

• Thanks, now I'm finally able to get it. – Aristu Apr 2 at 13:37
• @Aristu - Glad to hear that. – Taroccoesbrocco Apr 2 at 13:39