2
$\begingroup$

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?

$\endgroup$
  • 2
    $\begingroup$ @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. $\endgroup$ – Taroccoesbrocco Apr 2 at 13:17
  • $\begingroup$ @MauroALLEGRANZA - Exactly! This is what I wrote in my answer. $\endgroup$ – Taroccoesbrocco Apr 2 at 13:38
  • $\begingroup$ I've edited the question to be more clear. $\endgroup$ – Aristu Apr 2 at 13:41
  • 1
    $\begingroup$ 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}$$ $\endgroup$ – DanielV Apr 4 at 3:49
2
$\begingroup$

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.

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

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.