proving $ (A \rightarrow B \vee C )\rightarrow((A\rightarrow B) \vee (A\rightarrow C))$

Question

I'm looking for a way to prow $ (A \rightarrow B \vee C )\rightarrow((A\rightarrow B) \vee (A\rightarrow C))$ from the following axioms and rules $$\vdash A \rightarrow A$$ $$\vdash A \wedge B \rightarrow A$$ $$\vdash A \wedge B \rightarrow B$$ $$\vdash A \rightarrow A \vee B $$
$$\vdash B \rightarrow A \vee B $$ $$A, B \vdash A\wedge B$$
$$A, A \rightarrow B \vdash B$$ $$\vdash A\wedge (B \vee C) \rightarrow (A\wedge B)\vee (A\wedge C)$$ $$\vdash A \rightarrow (B \rightarrow B)$$ $$\vdash (A\rightarrow B)\wedge (A\rightarrow C) \rightarrow(A\rightarrow B\wedge C)$$ $$\vdash (A\rightarrow C)\wedge (B\rightarrow C) \rightarrow(A\vee B \rightarrow C)$$ $$\vdash (A\rightarrow B)\wedge (B\rightarrow C) \rightarrow(A\rightarrow C)$$ $$(A\rightarrow B) \vee E,(C\rightarrow D) \vee E \vdash((B\rightarrow C)\rightarrow(A\rightarrow D)) \vee E$$ $$A \vee C, (A\rightarrow B)\vee C\vdash B\vee C$$ $$A\rightarrow B, C\rightarrow D\vdash(B\rightarrow C)\rightarrow (A\rightarrow D)$$

Answer 1

See :

• Greg Restall, Subintuitionistic logic, NDJFL, 35-1 (1994).

The system is a subsystem of Intuitionistic Logic.

If so, the formula :

$(A→B∨C)→((A→B)∨(A→C))$

is not provable, because it is not intuitionistically valid.

---

For a counterexample to the formula, consider the Kripke model with three nodes : $w_0, v_1, v_2$, where $w_0$ is the root (the base world) and $w_0Rv_1, w_0Rv_2$, such that :

$w_0$ forces no propositional variable, while : $v_1 \vDash A,B$ and $v_2 \vDash A,C$.

The semantical rules for $\lor$ and $\rightarrow$ are the same used for intuitionistic logic : see Definition 2.1, page 118.