8
$\begingroup$

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?

$\endgroup$
  • 3
    $\begingroup$ 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.) $\endgroup$ – Andrej Bauer Oct 27 '14 at 13:42
  • 1
    $\begingroup$ I'm asking whether it can be done. Do you have a reference on an example fibration? $\endgroup$ – David Boshton Oct 27 '14 at 17:04
4
$\begingroup$

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. 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.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ Although, thinking about it, I have no idea where to start effectively. What is an initial category? $\endgroup$ – David Boshton Oct 28 '14 at 12:47
  • 1
    $\begingroup$ 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. $\endgroup$ – Neel Krishnaswami Oct 28 '14 at 12:55
4
$\begingroup$

[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.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.