Usage of classical logical symbols in intuitionistic logic

Question

Using the Johansson's minimal logic which is a weaker form of intuitionistic logic, the author in here proves on page 83 that $A \implies B \land B \implies C$ implies $C$ holds whenever $C$ is a stable formula in the sense that $\neg \neg C \implies C$.

He defines the symbol

$ A \tilde{\lor} B \triangleq \neg A \implies \neg B \implies \bot$

and proves $A \tilde{\lor} B \implies (A \implies B) \implies (B \implies C) \implies C$.

How is it done?

Is it derived from $A \implies C \land B \implies C \land A \lor B \vdash C$?

Answer 1

Here's a sketch of a natural deduction proof (both for the result as you have stated it and as it is given in the source that you cite): we are given assumptions:

$$ \begin{array}{lll} (1) & \lnot A \implies \lnot B \implies \bot &\mbox{(i.e., $A\mathrel{\overline{\lor}} B$)}\\ (2) & A \implies B & \mbox{(or $A \implies C$. See comment above.)}\\ (3) & B \implies C\\ (4) & \lnot\lnot C \implies C & \mbox{(i.e., stability of $C$)} \end{array} $$

and we want to derive $C$. Assume $\lnot C$, i.e., assume $C \implies \bot $, then from $(3)$ we get $\lnot B$ and from $(2)$ we get $\lnot A$, so that $(1)$ gives us $\bot$. Discharging our assumption $\lnot C$, gives us that $(1)$, $(2)$ and $(3)$ imply $\lnot C \implies \bot$, i.e., $\lnot\lnot C$. But then using $(4)$, we get $C$, which is what we wanted.

Answer 2

1) $A \overline \lor B$ --- premise [1]

2) $A \to C$ --- premise [2]

3) $\lnot C$ --- assumed [a]

4) $A$ --- assumed [b]

5) $C$ --- $\to$-elim

6) $\bot$ --- from 3) and 5)

7) $\lnot A$ --- from 4) and 6), discharging [b]

8) $\lnot A \to (\lnot B \to \bot)$ --- from [1] by def

9) $\lnot B \to \bot$ --- from 7) and 8) by $\to$-elim

10) $B \to C$ --- premise [3]

11) $B$ --- assumed [c]

12) $C$ --- from 10) and 11) by $\to$-elim

13) $\bot$ --- from 3) and 12)

14) $\lnot B$ --- from 11) and 13) discharging [c]

15) $\bot$ --- from 9) and 14) by $\to$-elim

16) $\lnot \lnot C$ --- from 3) and 15), discharging [a]

17) $C$ --- from 16) and $\lnot \lnot C \to C$ : $C$ is stable

$(A \overline \lor B) \to ((A \to C) \to ((B \to C) \to C))$ --- from 1), 2), 10) and 17) bt $\to$-intros.