# Relation between classical implication and intuitionistic implication

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!

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.