# What is the dual of implication?

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?

• Apologies if this is a naïve question! I'm only passingly familiar with these things. – J. Abrahamson Jan 12 '14 at 17:37
• As another follow-up, my guess would be that we'd somehow represent the positive of a function as a continuation and thus exponentials somehow play double-duty as both positives and negatives. It reminds me a bit of Filinski's thesis which I skimmed the beginning of. Is there a connection? – J. Abrahamson Jan 12 '14 at 17:57
• where did you read/study these things? – magma Jan 12 '14 at 18:42
• Self-study, primarily. I'm watching Dr. Robert Harper's Homotopy Type Theory lectures currently, I've also read a few books on category theory including Lawvere's Conceptual Mathematics. – J. Abrahamson Jan 12 '14 at 18:47
• – J. Abrahamson Jan 12 '14 at 18:49

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$.