Is there a category whose internal logic is paraconsistent?

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.


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.