Relation between classical implication and intuitionistic implication

Question

Recently, I have read an article on combining classical and intuitionistic implications. On page 9, in their Proposition 6, the authors say that $$A\Rightarrow((A\Rightarrow B)\rightarrow (A\rightarrow B))$$ is an axiom in the combined logic. Note that the authors use $\Rightarrow$ for classical implication and use $\rightarrow$ for intuitionistic implication. The proof they give for this proposition is couched in terms of Kripke semantics. I am wondering if it is possible to provide a proof in terms of Natural Deduction or Sequent Calculus for this proposition? Thanks!

Answer 1

To prove this in terms of "Natural Deduction or Sequent Calculus", you would need a natural deduction or sequent calculus proof system provided for this logic. Just as this logic has a novel semantics, it would need a novel proof system. At the point Proposition 6 is proven, they have only presented a semantics. Definition 3 in the next section presents a Hilbert-style proof system. You can prove that formula using this proof system by starting from axiom X3 which states $A\to((A\Rightarrow B)\to(A\to B))$, then deriving $(A\Rightarrow B)\to(A\to B)$ using IMP with an assumed $A$. Finally, use (meta-)Theorem 4, the classical deduction theorem CDED, to turns this proof of $(A\Rightarrow B)\to(A\to B)$ conditional on $A$ into an unconditional proof of $A\Rightarrow((A\Rightarrow B)\to(A\to B))$. You can unfold the proof of Theorem 4 to get an explicit proof if you like, or you can try to derive it directly.