You may divide Intuitionistic Propositional Logic into the negative and positive fragments. The negative fragment includes truth, conjunction, and implication while the positive fragment includes falsity and disjunction. There is an obvious duality between (truth, conjunction) and (falsity, disjunction) but implication lacks a dual. Is there a dual to implication?

Taken as a category we can make the (truth, conjunction)/(falsity, disjunction) duality explicit as (final, product)/(initial, coproduct) but I've never seen a dual to the exponential object. Is there a meaningful way to dualize the exponential object?

As a follow up there may be no way to dualize implication/exponential. If that is the case, why is implication thought to be contained in the negative fragment of IPL?


First look at how you get the exponential. In a category with products, the exponential functor $B \Rightarrow (-)$ can be defined as being right-adjoint to the functor $(-) \times B$. So in this case, $b \Rightarrow (-)$ is right-adjoint to $(-) \wedge b$, i.e. satisfies the rule $$a \wedge b \vdash c \quad \text{if and only if} \quad a \vdash b \Rightarrow c$$ In the case of classical logic, we can thus define $b \Rightarrow c = (\neg b) \vee c$, though in constructive logic $\Rightarrow$ needs to be taken as primitive. But this is fine: truth values in IPL live in a Heyting algebra, and all Heyting algebras have exponentials!

Dually, you get a coexponential object, for which I don't know the notation so I'll write $A \Rightarrow^{\text{op}} (-)$, which can be defined in a category with coproducts as being left-adjoint to the functor $(-)+A$. So in this case, $a \Rightarrow^{\text{op}} (-)$ is left-adjoint to $(-) \vee a$, i.e. satisfies the rule $$a \Rightarrow^{\text{op}} b \vdash c \quad \text{if and only if} \quad b \vdash c \vee a$$ In the case of classical logic, we can thus define $a \Rightarrow^{\text{op}} b = (\neg a) \wedge b$.

However a Heyting algebra can't in general be expected to have coexponentials, which is why implication appears to have no dual in constructive logic (because it doesn't!)