# Is there a category whose internal logic is paraconsistent?

The internal language of topoi is higher-order typed intuitionistic logic. Now according to wikipedia, the dual of intuitionistic logic, in some sense is paraconsistent. They say

Intuitionistic logic allows $$A ∨ ¬A$$ not to be equivalent to true, while paraconsistent logic allows $$A ∧ ¬A$$ not to be equivalent to false. Thus it seems natural to regard paraconsistent logic as the "dual" of intuitionistic logic.

they go on to say:

A specific paraconsistent logic is dual-intuitionistic logic or paracomplete logic, this duality can be best seen in sequent calculus framework, where

Both $$\vdash A \vee \neg A$$ and $$\neg \neg A \vdash A$$ are not derivable in intuitionistic logic, whereas

Both $$A ∧ \neg A \vdash$$ and $$A \vdash \neg \neg A$$ are not derivable in paraconsistent logic.

Given duality has a strong presence in Category theory, given that the internal language of toposes are intuitionistic, are there categories whose natural interpetation as a logic is dual-intuitionistic, or paraconsistent in some other way?

• How is it possible that $A\lor\lnot A\vdash$ is not derivable in paraconsistent logic? What could that even mean? Wouldn't the paraconsistent logic version of the nonderivability of $\vdash A\lor \lnot A$ be something involving $A\land\lnot A$?
– MJD
Aug 26, 2013 at 2:15
• @MJD - Indeed, the dualization would require disjunction to be substituted by conjunction. The original question needs some editing. Aug 31, 2013 at 14:48
• Why is the text at the bottom of the question in such a alrge font? I tried to fix it - but can't see how its occurring. Can someone with a tad more knowledge of how it formatting works fix it please. It doesn't look good. Nov 13, 2013 at 6:08
• I fixed the formatting of the bolded text. Jun 12, 2014 at 18:58
• @parsnip: thanks Jun 12, 2014 at 20:08

In the context of topos theory the answer would be no. The reason is (which I think is what you are saying) that in a topos the lattice of subobjects of the subobject classifier is a Heyting algebra, not (generally) a co-Heyting algebra. The duality you are talking about above is really saying that paraconsistent logic is algebraically like a co-Heyting algebra, while intuitionistic logic is algebraically like a Heyting algebra.

Of course, it should not be surprising that topos theory is not ideal for modeling paraconsistent logic seeing that it was designed to be ideal for intuitionistic logic (and paraconsistent logic is quite disjoint from it).

Now, to partly answer you question, it is unlikely that a notion dual to a topos will model paraconsistent logic. The reason is that the dual of a topos is (of course) generally not a topos and subobjects in the dual (which are the same as quotient objects in the original topos) don't have any Heyting or co-Heyting structure. What happens is that the lattice of quotient objects in the dual of a topos is the Hetying algebra of the subobjects in the original topos. In any case, no co-Heyting algebra there.

Whether there are categories that model paraconsistent logic, I think is currently not known.

• What do you think about minimal logic in nlab? They say that it is paraconsistent, because it is intuitionistic logic without explosion, (so unlike the example in my question), and by the curry-howard isomorphism is equivalent to simply typed lambda calculus (natural deduction proofs in minimal logic are equivalent to typing derivations in typed lambda calculus), and this is modelled by closed cartesian categories? Aug 27, 2013 at 1:45
• @MoziburUllah For a few references: Vladimir Vasyukov has produced a few papers on categorical semantics for paraconsistent logics; Sergei Odintsov has a whole book on paraconsistent constructive negations. Aug 31, 2013 at 14:41
• Seems to me the quotient lattices do form co-heyting algebras. May 25, 2017 at 6:59

Linear logic is a weakened relevance logic, which are paraconsistent logics. *-Autonomous categories with some extra structure have linear logic as their internal language. In fact they're also more naturally interpreted by polycategories.

If $a:A\rightarrow X$ and $b:B\rightarrow X$ are two monomorphisms in a category $\mathcal C$ such that $a\leq b$ in $\text{Sub}(X)$, shouldn't we have that $b^\text{op} \leq a^\text{op}$ in $\mathcal C^\text{op}$ ? Then if $\mathcal C$ is a topos, $\mathcal C^\text{op}$ should have quotient objects forming co-Heyting algebras.