Understanding $\lor~E$ in Natural Deduction?

Question

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?

Answer 1

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.