Intuition for the "internal logic" of a cotopos

Question

Let $\mathcal{E}$ be an elementary topos. By definition, $\mathcal{E}$ is a category that has finite limits, is Cartesian closed, and has a subobject classifier $\Omega$. This subobject classifier can be understood through a monomorphism $\mathrm{true} : * \rightarrow \Omega$ out of the terminal object, such that for every monomorphism $A \rightarrow X$ in our topos $\mathcal{E}$, there is a unique characteristic morphism $\chi_A : X \rightarrow \Omega$ such that the diagram $\require{AMScd}$ \begin{CD} A @>>> {*} \\ @VVV @VV{\mathrm{true}}V \\ X @>{\chi_A}>> \Omega \end{CD}

commutes and is a pullback. Of course, in the case of topoi, there is a very natural way to intuitively frame the subobject classifier's function with respect to the internal logic of the topos in question: each subobject $\phi:A \rightarrow X$ can be understood as subcollection of $X$ for which some (intuitionistic) proposition $\phi$ holds true. This is particularly intuitive in the case of the category of sets, where the subobject classifier binarily allocates values of $0$ or $1$ to subset membership relations, hence the law of the excluded middle holds in $\mathsf{Set}$.

While the subobject classifier $\Omega$ is a Heyting algebra in $\mathcal{E}$, in the dual structure $\mathcal{E}^{op}$ we have a quotient object coclassifier, which is an object (call it $\alpha$) with an epimorphism into the initial object $*$ of $\mathcal{E}^{op}$, such that for every epimorphism $X \rightarrow A$, there is a unique morphism $\mathcal{F}_A : \alpha \rightarrow X$ such that the diagram

\begin{CD} \alpha @>>> {*} \\ @V{\mathcal{F}_A}VV @VV{}V \\ X @>{}>> A \end{CD}

is a commutative pushout. By duality, it is the case that $\alpha$ is a co-Heyting algebra, which is dual to the notion of a Heyting algebra, and according to the nLab, they have interesting applications to the study of non-classical logic -- for example, if $\alpha$ were also a Heyting algebra (aka, a bi-Heyting algebra), it could potentially be associated with a quantum system by Döring's 2013 paper.

This would suggest that categories with co-Heyting algebras or bi-Heyting algebras as quotient object classifiers might have interesting properties as "models" of some non-classical logics, especially cotopoi (given the richness of topoi themselves), and yet I have not been able to produce an intuition that is as crisp as that I can associate with subobject classifiers in ordinary elementary topoi.

Is there any way, from a logical perspective, to think about the "classification" of isomorphism classes of epimorphisms by the quotient object coclassifier of a cotopos, or does dualization do away the meaningfulness of these notions? I have not found much literature on this subject (save for the references on the nLab), and would really appreciate some insights.

Answer 1

So, there are a bunch of really thorny issues hereabouts that no one (myself included) has really managed to get their heads around. I'm a philosopher by training, and more in tune with the logic, so forgive me if I butcher any of the deeper mathematics. Here are two intuitions that several people have had independently:

1. Co-intuitionistic logic (the syntactic dual of intuitionistic logic) may be intrinsically interesting either because it is in some sense naturally paraconsistent (as intuitionistic logic is naturally paracomplete: non-contradiction and excluded middle are dual) or because it provides a natural logic of refutation (as intuitionistic logic provides a natural logic of proof). There is a neat algebraic semantics of co-intuitionistic logic given by co-Heyting algebra (dual to Heyting algebra), but no one has been able to give a neat discursive interpretation of it, principally because it lacks an implication operator, and the dual co-implication operator is highly unintuitive.

2. Co-toposes might provide a way to extend the algebraic semantics of co-intuitionistic logic from the propositional to the predicate level, in precisely the way that toposes extend Heyting algebra. However, most people who have tried this do a simple syntactic dualisation (cf. Estrada-González's 2015 The Evil Twin: The Basics of Complement-Toposes), simply interpreting a topos in reverse (as a so-called complement topos), rather than dealing with an actual opposite category in which subobject classifiers are replaced with quotient classifiers. This produces nothing interesting. Those who try to pursue the semantic duality run up against various problems, the most obvious of which is the lack of good examples, i.e., cotoposes with non-trivial coexponents that might illuminate co-implication.

But it turns out there is a deeper problem here too. As far as I can tell, the person who pursued this line of thought the furthest is a guy called William James (who is impossible to google on that basis). He wrote a PhD dissertation titled Closed Set Logic in Categories at the Philosophy Department of the University of Adelaide in 1996. He ran into a really perplexing blockage, which is that while you might expect the quotient object lattice to be co-Heyting by simple duality with the subobject lattice, it isn't. The quotient lattice is a Heyting algebra.

However, James derives the internal logic of the lattice by means of a syntactic dualisation similar to that performed with 'complement toposes', interpreting the relevant morphisms in reverse. This is where @Andreas Blass's point is incredibly perceptive: it seems that, rather than having an internal algebra, the quotient classifier has an internal coalgebra. Alas, my understanding of coalgebra isn't really good enough to get a sense of what this internal coalgebra does, but I would be very interested to find out.

I have a sneaking suspicion that there may be some link with bisimulation here (if the characteristic morphism is read as a predicate, then we might read its dual as an invariant a la Jacobs). What I'm really curious about is whether there might be some connection between this and the logic of class hierarchies in OOP, which might usefully be approached from a paraconsistent perspective (e.g., multiple inheritance, conflicts, and class revision). That might perhaps head in the direction of elevating cointuitionistic logic to the predicate level. However, it remains to be seen whether there can be a genuine link created between cointuitionism and coalgebra in this context.

I'd love to discuss this more if you're interested.