<p>Non-monotonic logic is kind of a wide area -- do you have any particular logics in mind? Anyway, defeasibly assuming :) that </p>

<ol>
<li>you are interested in any logic in which the principle of monotony fails, and</li>
<li>you want a categorical semantics in the sense of categorical proof theory (rather than, say, a hyperdoctrine semantics), then</li>
</ol>

<p>one answer is that you can give a reasonable categorical semantics to any logic for which a sequent calculus with cut-elimination is known. Basically, the types are objects, normal forms of the sequent calculus are morphisms, and cut-elimination tells you how to implement composition. This gives you the initial category in whatever category of models you end up using to prove soundness and completeness. </p>

<p>This recipe is independent of monotonicity, and so it can work well even for non-monotonic logics. For example, one of the more important successes in categorical logic is its treatment of <a href="http://plato.stanford.edu/entries/logic-linear/" rel="nofollow"><em>linear logic</em></a>. This is a logic where, intuitively, propositions refer to <em>resources</em>, so that the linear implication $A \multimap B$ can be read as "$A$ can be consumed to produce $B$". The consequence relation of linear logic is non-monotonic (since the fact that $A$ can be consumed to produce $B$ does not mean that $A$ and $X$ can both be consumed to produce $B$). However, it has an excellent proof theory, and its categorical models are closely tied to the theory of monoidal categories. </p>

CC BY-SA 3.0
2014-10-28T12:47:28.050Z
Although, thinking about it, I have no idea where to start effectively. What is an initial category?
David Boshton
CC BY-SA 3.0
2014-10-28T12:55:19.650Z
When you prove soundness and completeness, you consider a collection of models, and then show that the calculus proves exactly the entailments provable in every model. Normally, you also want to organize your collection of models into a category, too, with a morphism between models being some suitable notion of homomorphism of models. Then showing soundness and completeness essentially means showing the term model of the calculus is the initial object in the category of models.
Neel Krishnaswami
CC BY-SA 3.0
2014-10-28T11:32:05.433Z
2014-10-28T11:32:05.433Z
Neel Krishnaswami
<p><em>[My apologies for writing this as an answer, despite the fact that it is basically just a comment to the previous answer. But I am not allowed to post a comment up there, since I do not have enough "reputation"]</em></p>

<p>The previous answer is not correct. Linear logic (as well as any of its substructural systems: MLL, MALL, MELL, ALL, whatever you want...) is perfectly <em>monotone</em>. </p>

<p>Neel's answer confuses "relevance" and "non-monotonicity".</p>

<p>Relevance can be seen as <em>non-monotonicity of the inference connector of the system</em>. Linear logic is relevant, in that the provability of $\;\vdash A \multimap B$ does not imply the provability of $\vdash X\otimes A \multimap B$. Relevance is a sort of <em>inner</em> non-monotonicity of the logic.</p>

<p>On the other side, what people call <em>non-monotonic logics</em> are systems where the <em>provability</em> itself of the system is not monotone: <strong>adding a new element to the set of formulas changes the set of provable formulas.</strong> It is a form of <em>meta</em> non-monotonicity, because it concerns provability and not the connector of inference. Linear logic is monotone: you can add whatever you want to the set of formulas, and any new axiom or inference rule to the system, but if you had a proof of the sequent  $\;\Gamma \vdash M: A$ before, you will still have it now, for you have not changed the other inference rules of the sequent calculus.</p>

<p>As far as I know, (real) non-monotonic logics are hard to put down in a sequent calculus form enjoying cut-elimination, or any other type of proof system with an equivalent notion of terminating proof-reduction. This is why the tradition categorical semantic approaches hardly would work for them.   </p>

CC BY-SA 3.0
2018-03-29T12:57:38.640Z
2018-03-31T15:20:32.103Z
2018-03-31T15:20:32.103Z
Domenico Ruoppolo
<p>Are there any categorical semantics for non-monotonic logics?</p>

<p>It appears that the simple answer to this is "No" since the obvious notion of composition fails for any model of a non-monotonic logic. But is there a model that actually works with an appropriately defined notion of composition?</p>

CC BY-SA 3.0
2014-10-27T13:42:05.003Z
Are you asking whether someone has done it, or whether it *can* be done? Surely it can be done, but I do not know whether it has been done. (You just shouldn't model the consequence relation as the subobject relation, but pass to a fancier fibration.)
Andrej Bauer
CC BY-SA 3.0
2014-10-27T17:04:44.653Z
I'm asking whether it can be done. Do you have a reference on an example fibration?
David Boshton
<ct.category-theory><semantics><denotational-semantics>
Categorical semantics for non-monotonic logics?
David Boshton
# Categorical semantics for non-monotonic logics?

(Asked by: username_0 on 2014-10-27)

Are there any categorical semantics for non-monotonic logics?

It appears that the simple answer to this is "No" since the obvious notion of composition fails for any model of a non-monotonic logic. But is there a model that actually works with an appropriately defined notion of composition?

**Tags:** ct.category-theory, semantics, denotational-semantics
> **Comments:**
> **username_1**: Are you asking whether someone has done it, or whether it *can* be done? Surely it can be done, but I do not know whether it has been done. (You just shouldn't model the consequence relation as the subobject relation, but pass to a fancier fibration.)  
> **username_0**: I'm asking whether it can be done. Do you have a reference on an example fibration?  

---

## 2 answers

### Answer by username_2 on 2014-10-28. Score: 4

Non-monotonic logic is kind of a wide area -- do you have any particular logics in mind? Anyway, defeasibly assuming :) that

1. you are interested in any logic in which the principle of monotony fails, and
2. you want a categorical semantics in the sense of categorical proof theory (rather than, say, a hyperdoctrine semantics), then

one answer is that you can give a reasonable categorical semantics to any logic for which a sequent calculus with cut-elimination is known. Basically, the types are objects, normal forms of the sequent calculus are morphisms, and cut-elimination tells you how to implement composition. This gives you the initial category in whatever category of models you end up using to prove soundness and completeness.

This recipe is independent of monotonicity, and so it can work well even for non-monotonic logics. For example, one of the more important successes in categorical logic is its treatment of [*linear logic*](http://plato.stanford.edu/entries/logic-linear/). This is a logic where, intuitively, propositions refer to *resources*, so that the linear implication $A \multimap B$ can be read as "$A$ can be consumed to produce $B$". The consequence relation of linear logic is non-monotonic (since the fact that $A$ can be consumed to produce $B$ does not mean that $A$ and $X$ can both be consumed to produce $B$). However, it has an excellent proof theory, and its categorical models are closely tied to the theory of monoidal categories.

> **Comments:**
> **username_0**: Although, thinking about it, I have no idea where to start effectively. What is an initial category?  
> **username_2**: When you prove soundness and completeness, you consider a collection of models, and then show that the calculus proves exactly the entailments provable in every model. Normally, you also want to organize your collection of models into a category, too, with a morphism between models being some suitable notion of homomorphism of models. Then showing soundness and completeness essentially means showing the term model of the calculus is the initial object in the category of models.  

---

### Answer by username_3 on 2018-03-29. Score: 4

*[My apologies for writing this as an answer, despite the fact that it is basically just a comment to the previous answer. But I am not allowed to post a comment up there, since I do not have enough "reputation"]*

The previous answer is not correct. Linear logic (as well as any of its substructural systems: MLL, MALL, MELL, ALL, whatever you want...) is perfectly *monotone*.

Neel's answer confuses "relevance" and "non-monotonicity".

Relevance can be seen as *non-monotonicity of the inference connector of the system*. Linear logic is relevant, in that the provability of $\;\vdash A \multimap B$ does not imply the provability of $\vdash X\otimes A \multimap B$. Relevance is a sort of *inner* non-monotonicity of the logic.

On the other side, what people call *non-monotonic logics* are systems where the *provability* itself of the system is not monotone: **adding a new element to the set of formulas changes the set of provable formulas.** It is a form of *meta* non-monotonicity, because it concerns provability and not the connector of inference. Linear logic is monotone: you can add whatever you want to the set of formulas, and any new axiom or inference rule to the system, but if you had a proof of the sequent $\;\Gamma \vdash M: A$ before, you will still have it now, for you have not changed the other inference rules of the sequent calculus.

As far as I know, (real) non-monotonic logics are hard to put down in a sequent calculus form enjoying cut-elimination, or any other type of proof system with an equivalent notion of terminating proof-reduction. This is why the tradition categorical semantic approaches hardly would work for them.


---

