Are these two forms of disjunction elimination equivalent?

Question

I know of at least two inference rules for disjunction elimination:

1. $a \vee b, \neg a \vdash b$

2. $a \vee b, a \to c, b \to c \vdash c$ (also known as proof by cases)

I know the second follows from the first, because I have proved it. But does the first follow from the second? I have not been able to prove this.

Answer 1

Indeed, assuming $\neg a$ is equivalent to $a \to \bot$ and assuming you're allowed access to $\neg \neg b \to b$. (Just let $c = \bot$.)

Note that you do need some form of the law of excluded middle for this implication, because the second is constructively valid but the first is not.

Answer 2

Technically, neither one follows from the other unless you add some further inference rules.

But supposing you have some formalized forms of conditional proof as well as proof by contradiction, you can, given $\neg a$, show that $a \rightarrow b$, and it should also be easy to show $b \rightarrow b$ is always valid. If you can show those two things, then you can get the first from the second.