Monoidal logics are logics that can be seen as specific instances of monoidal categories. They are constructed using specific rules and axiom schemata that allow to make explicit the monoidal structure of the logics. Among monoidal logics, we find Cartesian logics, which are instances of Cartesian categories. As it happens, many paradoxes in epistemic, deontic and action logics can be related to the Cartesian structure of the logics that are used. While in epistemic and deontic logics the source of the paradoxes is often found within the principles that govern the modal operators, our framework enables us to show that many problems can be avoided by adopting a proper monoidal structure. Thus, the usual modal rules and axiom schemata do not necessarily need to be discarded to avoid the paradoxes. In this respect, monoidal logics oe↵r an alternative way to model knowledge, actions and normative reasoning. Furthermore, it provides us with new avenues to analyze modalities.
Monoidal logics were recently introduced by Peterson [
In the present paper, we show how monoidal logics are relevant to artificial intelligence given that they enable us to expose and solve some problems that are related to epistemic, deontic and action logics. While these kinds of logic are often formalized as di↵erent variations of modal logics, we begin in section 2 by summarizing the framework we adopt for modal logics (section 2.1) and monoidal logics (section 2.2). That being done, we present and discuss some paradoxes in section 3 and analyze them in light of our framework. We conclude in section 4 with avenues for future research. 2.1
Following Chellas [
The interest of Chellas’s approach is that it clearly relates the rules governing the modalities to the consequence relation of classical logic. Using the following inference rules, we can adopt the following definitions3: – – – is classical if it is closed under (RE); is monotonic if it is closed under (RM); is normal if it is closed under (RK).
' ⌘ 2' ⌘ 2 (RE) ' 2' 2 (RM) ' 2' (RN) (' 1 ^ · · · ^ ' n) (2' 1 ^ · · · ^ 2' n) 2 (RK) with n 0
While a classical system preserves logical equivalences under 2, a monotonic system insures that 2 preserves consequences. The relations between these systems is as follows: if is normal, then it is monotonic, and furthermore if it is monotonic, then it is classical. A classical system E is usually defined by LP C + (RE), a monotonic system M by LP C + (RM) and a normal system K by LP C + (RK). In addition to the usual definition of these systems, one can also have alternative formulations using the following axiom schemata: 2(' ^ ) (2' ^ 2 ) (M) 2(' ) (2' 2 ) (K) 2> (N)
Using these axioms, monotonic and normal systems can alternatively be defined:
K = LP C + (K) + (RN) = M + (K) + (N)
M = E + (M) 2 That is, atoms, > and ? are formulas, and if ' and are formulas, then so are ' ^ , ' , ' _ and 2' . 3 Note that there are other types of modal systems, such as regular systems, but we leave them aside for the purpose of the present paper.
Many extensions can be constructed from these systems. The usual modal axioms are D, T, 4 and 5.4
D is usually considered as a deontic axiom, which means that if ' is obligatory, then it is also permitted. T is usually used as an axiom for necessity, meaning that if ‘it is necessary that ' is true’ is true, then ' is true. 4 and 5 are usually used for epistemic modalities, the former meaning that if an agent knows ' , then he knows that he knows ' and the latter meaning that if ' is true, then an agent knows that it is possible for ' to be true. 2.2
The rationale behind monoidal logics is to use category theory to analyze the proof theory of logical systems. By doing so, one can expose the categorical structure of di↵erent logics and classify these systems accordingly. Consider the language L = {P rop, (, ), ⌦ , 1, (, , 0}, where P rop is a collection of atomic propositions. The connective ⌦ is understood as some form of conjunction (although not necessarily ^ ), ( is an implication and a disjunction (but not necessarily _ ). Negation and well-formed formulas are defined as usual (¬' =df ' ( 0). ' := pi | 0 | 1 | ' ⌦ | ' ( | '
To define monoidal logics, we need to first define the consequence relation (see the rules and axiom schemata in figure 1).5 To do so, we define a deductive system and we require that proofs are reflexive and transitive.
Definition 1. A deductive system D is a collection of formulas and (equivalence classes of ) proofs (deductions). It has to satisfy (1) and (cut).
Then, one can introduce a conjunction ⌦ with a unit 1 using a monoidal deductive system. This conjunction is minimally associative but is not necessarily commutative. The unit 1 can be absorbed by ⌦ from (r) and (l). Definition 2. A monoidal deductive system M is a deductive system satisfying (r), (l), (t) and (a).
When this is done, one can do either one of two things. Either one keeps the
monoidal structure and adds an implication, and then perhaps classical
negations, or one adds some structure to the conjunction by requiring that it be
commutative.6 In the latter case, one can define a symmetric deductive system,
4 Note that there are other axioms, see [
Definition 3. A symmetric monoidal deductive system S is a monoidal deductive system satisfying (b). 3.1 A symmetric closed deductive system SC satisfies (cl). 3.2 A symmetric closed deductive system with classical negation SCC satisfies (¬¬).
From a symmetric deductive system, one can add some more structure to the conjunction and define a Cartesian deductive system. In such a case, ⌦ is the usual conjunction ^ of classical or intuitionistic logics. The rule (Cart) allows us to introduce and eliminate the conjunction, while (!) means that anything implies the truth. As it was the case for symmetric deductive system, one can also add an implication and classical negation.
Definition 4. A Cartesian deductive system C is a deductive system satisfying (Cart) and (!). 4.1 A Cartesian closed deductive system CC satisfies (cl). 4.2 A Cartesian closed deductive system with classical negation CCC satisfies (¬¬).
The relationship between these deductive systems is as follows: if D is Cartesian, then it is symmetric, and furthermore if it is symmetric, then it is monoidal. As a notational convention, we use the symbols {⌦ , 1, (, , 0} for non-Cartesian deductive systems and {^ , >, , _ , ?} for Cartesian ones.
(1) (¬¬) ' ! ' ' ⌦ ' ' ! ⇢
! ⇢ / ' ⌦ ⇢
/ ⇢ / ( ⇢ ⇢ / ⌦ ⌧ (cl) / ⌧ '
/ ' (cut) (t) ⌧ ⌧ ' ' ' / (' ⌦ / ⌦ 1 / ) ⌦ ⇢ / ' ⌦ ( ⌦ ⇢ ) / 1 (!) ¬¬' (r)
/ ' (a) ' ' / ' ' ' ' ' / ⌦ ⇢ / 1 ⌦
/ / ⌦ ⌧ / ⌧ ⌦ / ⇢ (l) (b) (Cart)
The co-tensor can be axiomatized through a deductive system defined as an opposite deductive system Dop where the formulas remain the same but the deduction arrows are reversed and ⌦ /1 are respectively replaced by /0. Hence, we obtain the co-versions of the aforementioned rules and we can define comonoidal (coM), co-symmetric (coS) and co-Cartesian (coC) deductive systems.
The interest of this approach is that deductive systems can be classified
according to their categorical structure (cf. [
On the semantical level, monoidal logics can be interpreted within the
framework of partially-ordered residuated monoids (see [
Epistemic logics are usually defined as normal K45-, KD45-, KT4- or
KT5systems. Notwithstanding these di↵erent axiomatizations, the problem of logical
omniscience is linked to the basic structure of a normal system and can be
related to many rules and axioms. While it is usually attributed to the K-axiom
for distribution (e.g., [
The rule RN expresses a weak form of logical omniscience. It means that an agent knows each and every theorem of the system. Combined with the K-axiom for distribution, this implies a stronger form of omniscience. Indeed, K is logically equivalent to the following formula, which states that knowledge (or belief) is closed under implications that are known (or believed).
(2' ^ 2(' )) 2
Considered together with RN, the K-axiom implies that an agent knows every logical consequence of his prior knowledge. This is the usual presentation of the problem of logical omniscience, which amounts to attribute the problem to RK (which, as we know, is logically equivalent to K+RN). Hence, even though ‘full’ logical omniscience happens when RK is satisfied, it should be emphasized that some weaker form of logical omniscience can also happen in non-normal modal logics that satisfy either K or RN (but not both).
In addition to these three forms of logical omniscience, others are also present
in some non-normal modal logics. For instance, the rule RM entails that if an
agent knows something, then he knows all tautologies. That does not imply that
the agent knows per se every tautology, but only that as soon as he knows, say,
' , then he knows every tautology. This is a consequence of the following instance
of RM (with > some tautology).
7 This semantical framework is inspired by the work of [
Furthermore, another weaker form of omniscience can be related to RE.
Although he specifies that this does not reduce to logical omniscience per se,
Stalnaker [
Consequently, it appears that even classical systems are not completely immune to the objection of logical omniscience. But still, modal logics are widely relevant to the analysis of epistemic modalities, and thus an important question is whether or not it is possible to utterly avoid logical omniscience while keeping other relevant principles of modal logics. Fortunately, the answer to that question is yes, and the solution is to look at this problem from the perspective of monoidal logics.
Despite all the modal rules and axioms that were used in the presentation of the problem of logical omniscience, it should be noted that there were also two propositional principles at play. On the one hand, in the case of RM, it is the fact that ' > is a theorem that allows us to conclude that if an agent knows that ' , then he knows every tautology. From a categorical perspective, this amounts to the fact that > is a terminal object. On the other hand, in the case of RE, it is the fact that tautologies are logically equivalent that leads to a weaker form of logical omniscience. Although this might not be explicit at first glance, it happens that this is also related to the fact that > is terminal. ' ! / > * ' ✏
As it is shown in the diagram above, if a formula ' is a theorem, then we know that there is a proof > / ' . This is standard for any monoidal logic. That being said, it is the arrow ! that entails the logical equivalence between any tautology and > (hence between each and every tautologies).
From a categorical perspective, this arrow is related to the Cartesian structure of classical modal logics, which follows from the fact that they are extensions of (classical) propositional logic. It is however possible to define propositional logics that still have a classical negation but that do not have this Cartesian structure. Indeed, the closest alternative system would be a symmetric monoidal closed deductive system with classical negation SCC. In such a system, > is not terminal and tautologies (resp. contradictions) are not logically equivalent. Therefore, one could easily add the rules RE or RM to a SCC without facing the weaker forms of logical omniscience related to these rules. Note, however, that RN would still imply that the agent knows every tautology and, moreover, that K would still mean that knowledge is closed under known implications. 3.2
Ross’s paradox [
Despite the fact that Ross’s paradox is ususally objected to the standard system (i.e., a normal system), it should be noted that it is actually derivable in monotonic systems. Indeed, it is a special case of RM: ' 2' (' _ ) 2(' _ ) (RM)
But even though Ross’s paradox appears as a consequence of monotonic systems, it happens that RM does not necessarily leads to it. As we can see in the instance of RM above, the formula that allows us to derive the undesired consequence is ' (' _ ). This formula is a specific instance (on the right below) of the co-version of the rule for Cartesian systems (on the left).9 ' / ⇢ ' _ / ⇢ / ⇢ (co-Cart) ' _ '
/ ' _ / ' _ (1) (co-Cart)
It is noteworthy that the arrow ' / ' _ expresses a fundamental property of the disjunction _ . Indeed, this arrow is an injection map that allows us to define _ as a categorical co-product. Put die↵rently, it is a fundamental property of co-Cartesian deductive systems, which is not derivable in non-Cartesian ones. Hence, in the presence of RM, Ross’s paradox is derivable as soon as the co-tensor is axiomatized within a coC.
As a result, it is possible to keep some desired principles governing the 2 operator and add RM or RK to a SCCcoS while avoiding Ross’s paradox. 3.3
Prior’s paradox [
In words, this means that if ' is forbidden, then carrying out ' commits us to any . This is obviously an undesirable principle. As in the case of Ross’s paradox, this is actually a consequence of RM. 9 Note that ' / if and only if > 2¬' ¬' 2¬' 2('
) (' 2(' / ' ) ) .
(RM)
Yet, although Prior’s paradox might be seen as an instance of RM, it is still possible to have a modal system satisfying that rule without enabling the derivation of the paradox. If we consider the logical equivalence between ' and ¬' _ , then ¬' (' ) can also be seen as a special instance of (coCart). That being said, it is noteworthy that Prior’s paradox is deeply related to the (co)-Cartesian structure of the logic. Indeed, the formula ¬' (' ) actually hides the fact that ? is initial, which is also a fundamental characteristic of (co)-Cartesian deductive systems.
¬' ' ^ ¬ ' / ¬'
/ ? ' ^ ¬ ' ¬' (1) (cl) / ' / ? (cl) / (? ) (cut)
As it is shown in the proof above, the derivation of Prior’s paradox requires the axiom schema stating that ? is initial.10 In this respect, the paradox can be correlated to the (co-)Cartesian structure of the logic. Therefore, it is possible to avoid Prior’s paradox while keeping RM or RK, for instance if we add RM or RK to a SCCcoS. 3.4
In the philosophy literature, the two main action logics that are used are stit
and dynamic logics (cf. [
Apart from dynamic logics based on Kleene algebras, all the aforementioned
approaches share a common structure, namely that of a Cartesian deductive
10 Note that the axiom ? is actually co-!.
11 The acronym stit stands for ‘seeing to it that’.
12 More precisely, consequences of actions (intended or not).
13 See for example [
Now, an interesting property of Cartesian deductive systems is that they satisfy idempotence of conjunction (i.e., ' is logically equivalent to ' ^ ' ). This follows from the derivations below.
Although it was not formulated in these terms when he introduced linear
logic, Girard [
From the perspective of monoidal logics, we can see that this paradox affects CCCs, and thus the closest alternative to model action while avoiding the paradox is to use an instance of a SCC. 3.5
Contrary-to-duty reasoning is deeply relevant to artificial intelligence. As it stands, the three main problems one faces when trying to model contrary-toduty reasoning are augmentation, factual detachment and deontic explosion.
Augmentation (cf. [
' 2 (' ^ ⇢ ) 2 (aug)
Modeling a deontic conditional using ' 2 , this implies that whenever there is an obligation 2 conditional to a context ' , then this obligation is also conditional to the augmented context ' ^ ⇢ for any ⇢ . This is undesirable given that the extra conditions ⇢ might be such that the obligation does not hold anymore.14
The problem of factual detachment (cf. [
In a nutshell, the problem of factual detachment can be formulated as follows: even though one might want to detach the obligation 2 from the context ' and the deontic conditional ' 2 , there might be other conditions ⇢ that will thwart the detachment of 2 . Thus the problem: detachment is desired but only when we can insure that nothing else will thwart the detached obligation. However, if a logic satisfies the aforementioned inference pattern, then it allows for unrestricted detachment.
Finally, the problem of deontic explosion (see for instance [
These issues have been thoroughly analyzed in [
2 )) 2 ) 2 )
In this respect, it can be argued that the three major problems one faces
when trying to model contrary-to-duty reasoning are related to the Cartesian
structure of the logic that is used. To avoid these problems, one must therefore
use a logic that has a weaker structure to model contrary-to-duty reasoning. As
such, we developed a logic for conditional normative reasoning on the grounds
of a monoidal logic (precisely, an instance of a SCCcoS) in [
Summing up, we showed using the framework of monoidal logics that many paradoxes in epistemic, deontic and actions logics are related to the Cartesian structure of the logic that are used. While the source of some paradoxes in epistemic and deontic logic is usually attributed to the rules and axiom schemata 15 Or within a regular system. that govern the modalities, we showed that the source of these problem is actually the Cartesian structure of the logic. As a result, it is possible to keep some desired modal rules and axiom schemata while avoiding the paradoxes by using a logic that has a monoidal structure rather than a Cartesian one.
For future research, it remains to explore the logical properties of the monoidal
modal logics that can be constructed from the rules and axiom schemata of
classical modal logics. We will need to properly study the relations between the
different rules and axioms and determine how accessibility relations can be defined
within the framework of partially-ordered residuated monoids. We also intend to
explore how monoidal modal logics can be used to model artificial agents with
the help of monoidal computers (cf. [