Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Categorification of consequence relations

Ralph Sarkis (Jan 21 2023 at 14:28):

There is a well-known correspondence between consequence relations and closure operators (see the first few pages of Chapter 4 here and in particular Prop 4.2.3 --- closure operators are called consequence operators there). In short, given a relation ${\vdash} \subseteq \mathcal PX \times X$, we define $c_{\vdash}: \mathcal PX \rightarrow \mathcal P X$ by sending $S \subseteq X$ to $\{x \in X \mid S \vdash x\}$. When $\vdash$ is closed under some rules that are motivated by seeing it as an entailment relation (see Defn 4.1.1), then $c_{\vdash}$ is a closure operator, and we can go in the opposite direction.

Now, closure operators on $\mathcal PX$ are instance of monads on the posetal category $(\mathcal PX, \subseteq)$. Is there a categorification of consequence relations yielding a correspondence with some type of monads? It does not look like it because there are no "power categories" and the target of a consequence relation is merely a set (not that much structure), but I am still curious.

Nathanael Arkor (Jan 21 2023 at 17:07):

$\vdash$ can be written as a functor $\mathcal P X \times X \to 2$, which is equivalently $\mathcal P X \to 2^X = \mathcal P X$ by currying. The axioms for a consequence relation are necessarily those corresponding to the monad axioms until transposition. Categorifying, we may replace the power set construction with the presheaf construction. Hence monads on presheaf categories correspond to functors $\mathcal P X \times X \to \mathbf{Set}$, where $\mathcal P X = [X^\circ, \mathbf{Set}]$, satisfying axioms that correspond to the monad axioms under transposition.