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$?

  • 1
    $\begingroup$ I think it must be : $(A→C)→((B→C)→C)$; see page 84. $\endgroup$ – Mauro ALLEGRANZA Dec 3 '16 at 22:23
  • $\begingroup$ @MauroALLEGRANZA: I think you are right that the result is supposed to look like a form of disjunction elimination. $\endgroup$ – Rob Arthan Dec 3 '16 at 22:39

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.

  • $\begingroup$ Never mind: but my sketch does give the proof you asked for and the one you actually needed $\ddot{\smile}$. $\endgroup$ – Rob Arthan Dec 3 '16 at 22:42

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.


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.