# 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

## 1 Answer

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!)

• That's basically exactly what I was looking for, thank you! It's obvious now how the adjoints provide a dualization, though clearly I need to become more comfortable thinking with them. Do you have any intuition or sources on what it means that Heyting algebras lack co-exponentials? Are there dual Heyting algebras which take the co-exponential as primitive? I'd like to find some way to track the symmetry breaking. – J. Abrahamson Jan 12 '14 at 18:36
• Heyting algebras, unlike Boolean algebras, aren't symmetric in the sense that the dual of a Heyting algebra isn't necessarily a Heyting algebra. (But the dual of a Boolean algebra is a Boolean algebra.) This is precisely because a Heyting algebra is defined to have exponentials, but isn't defined to have coexponentials -- and the existence of coexponentials isn't implied by the other properties of a Heyting algebra. – Clive Newstead Jan 12 '14 at 18:40
• By the way, whenever I say 'dual' I mean something very precise, i.e. the notion of a categorical dual. – Clive Newstead Jan 12 '14 at 18:42
• I suppose I might be looking for Esakia spaces. – J. Abrahamson Jan 12 '14 at 18:45
• ncatlab.org/nlab/show/co-Heyting+algebra – Anthony Dec 20 '18 at 7:57