Prove material implication without law of excluded middle Can we prove the material implication
$$ A \to B \vdash \neg A \vee B $$
without using the law of excluded middle?
It's trivial with the law of excluded middle, but I'm wondering if it can proven simply by syntactically using the introduction and elimination rules of disjunction and implication.
I'm going to assume classical logic ($\dfrac{\neg\neg e}{e}$) because I'm not so sure it can be done in intuitionistic logic; can it?
 A: We can prove $A \rightarrow B \vdash \neg A \vee B$ using double negation elimination without invoking the law of excluded middle in its usual form.
Assume $A \rightarrow B$. If we have double negation elimination, it's sufficient to prove $\neg\neg (\neg A \vee B)$ instead of $\neg A \vee B$. So assume¹ $\neg (\neg A \vee B)$ for a contradiction. Assume² $A$ for a contradiction. Since $A$ and $A \rightarrow B$ hold by assumption, we have $B$ by implication elimination (modus ponens). Then, we get $\neg A \vee B$ from $B$ by disjunction introduction. This contradicts our assumption that $\neg (\neg A \vee B)$, hence we can discharge assumption 2 and conclude $\neg A$. But $\neg A \vee B$ follows again from $\neg A$ by disjunction introduction. Thus we can discharge assumption 1 and conclude $\neg \neg (\neg A \vee B)$. By double negation elimination $\neg A \vee B$ holds.
Regarding your second question: you cannot prove $A \rightarrow B \vdash \neg A \vee B$ in intuitionistic logic. If you could prove $A \rightarrow B \vdash \neg A \vee B$ in intuitionisitic logic, you could set $B = A$ and get a proof of $A \rightarrow A \vdash \neg A \vee A$ in intuitionistic logic. But $A \rightarrow A$ is a theorem of intuitionistic logic, and $\neg A \vee A$ is not, so no such proof exists.
A: There are two things to note here.
The first is that the double negation elimination rule ($\neg \neg P \vdash P$) is equivalent to the law of excluded middle. This is because it's possible to prove $\neg \neg (P \lor \neg P)$ without using any form of classical logic. Applying double negation elimination then gives us $P \lor \neg P$.
Therefore, anything that can be proved with the law of excluded middle can also be proved using double negation elimination.
The second thing to note is that the principle you have outlined is actually equivalent to the law of excluded middle. Simply substitute $A$ for $B$; then the principle becomes $A \to A \vdash \neg A \lor A$. And clearly $A \to A$ is always a tautology. So we have proved the law of excluded middle from your rule.
This means that it is not possible to prove the rule $A \to B \vdash \neg A \lor B$ solely using constructive logic (aka solely using the introduction and elimination rules of logic, without using "classical logic" principles like double negation elimination or excluded middle).
