4
$\begingroup$

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!

$\endgroup$

1 Answer 1

2
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Hi Derek, thanks for the answer. The problem for me is that the axiom that you refer to in their Definition 3 is based on their Proposition 6. So, I don't really want to use this to prove Proposition 6. I am wondering if we could use, for example, propositional truncation, or Godel's negative translation to do that. But I have not found a way to do that. Any idea? $\endgroup$
    – ferdinand
    Sep 26, 2019 at 7:26
  • 1
    $\begingroup$ There's no avoiding this. They're defining their logic via the given semantics. Even if this logic could be understood via a translation into intuitionistic logic (which seems very plausible), you would need to use the semantics to prove this (likely indirectly by using the proof system in Definition 3, though you could do it directly if you wanted). $\endgroup$ Sep 26, 2019 at 7:50

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .