Inspired by Kelsen’s view that norms establish causal-like connections between facts and sanctions, we develop a deontic logic in which a proposition is obligatory iff its complement causes a violation. We provide a logic for normative causality, define non-contextual and contextual notions of illicit and duty, and show that the logic of such duties is well-behaved and solves the main deontic paradoxes.

We introduce a deontic logic based on causality and violation constants, and check its behaviour with respect to some standard paradoxes from the Deontic Logic literature. Although inspired by Kelsen's legal theory, the corresponding "logic of prohibitions" could be used as the base logic to formalize Mimamsa prohibitions.

In his Vidhiviveka, Maṇḍanamiśra delineates his own view of pravṛttihetu or the causal factor of motivation. On his view, it is iṣṭasādhanatā or the property of being the means for some desired end of a human being. The present article shows how Maṇḍana builds up his own theory of iṣṭasādhanatā on the rival theories of niyoga and pratibhā, by showing how iṣṭasādhanatā alone supplies the missing content of the cognitions of kartavyatā or ‘something to be done’, without which no activity is possible. Maṇḍana also shows how iṣṭasādhanatā which is at work behind such basic activities of human being like a new-born baby’s suckling of the mother’s breast, or that of other living beings like the singing of the male cuckoo at the advent of spring, and cannot be, contrary to the Pratibhāvādin opponent’s claim, caused by pratibhā or mere cognition devoid of a content. For doing so, Maṇḍana takes the help of a decontextualised Nyāyasūtra. He also shows how a mere cognition of duty without any definite end towards which it is directed, is insufficient to lead one to undertake any action. Thus, Maṇḍana establishes both the necessity and sufficiency of iṣṭasādhanatā as an instigator by proving how an understanding of the action to be the means for accomplishing some desired end precedes the actual undertaking of any action, and how it works as a viable theory accounting for not only the actions of human beings but also all living beings.

For decades, the gentle murder paradox has been a central challenge for deontic logic. This article investigates its millennia-old counterpart in Sanskrit philosophy: the Śyena controversy. We analyze three solutions provided by Mīmāṃsā, the Sanskrit philosophical school devoted to the analysis of normative reasoning in the Vedas, in which the controversy originated. We introduce axiomatizations and semantics for the modal logics formalizing the deontic theories of the main Mīmāṃsā philosophers Prabhākara, Kumārila, and Maṇḍana. The resulting logics are used to analyze their distinct solutions to the Śyena controversy, which we compare with formal approaches developed within the contemporary field of deontic logic.

This work is adressed to deontic logicians and scholars of Indian Philosophy. We present three logics of the leading Mīmāṃsā philosophers Prabhākara, Kumārila, and Maṇḍana. We discuss their distinct theories of normative reasoning and their corresponding logic in the light of the Śyena controversy, a controversy surrounding the killing one's enemy by performing the Śyena. The controversy is due to the fact that the Śyena appears to be prescribed in the Vedas, that also prohibits the performance of violence. We use logical methods to analyze and shed light on the three authors' different solutions to the Śyena. Furthmore, we observe that the controversy is akin to a central challenge in deontic logic known as Gentle Murder Paradox. Correspondingly, we obtain three Mīmāṃsā based solutions to this contemporary paradox in deontic logic.

In this discussion paper we are interested in anankastic conditionals such as ``if you want to smoke you must buy cigarettes" and near-anankastic conditionals such as ``if you want to smoke, you must not buy cigarettes." First, we discuss challenges to representing such conditionals in deontic logic, in particular in relation to the use of context. We do this through a discussion of the Tobacco shop scenario, an example dealing with ambiguity of certain deontic conditionals. Second, we illustrate how ambiguity of natural language can be formally represented through the use of hyper-modalities, using a minimal modal logic for (near-)anankastic conditionals. We illustrate how the hyper-modal setting can disambiguate such conditionals. As the Tobacco shop scenario suggests, in our formalism interaction between antecedent, consequent, and context can reduce ambiguity in the involved conditionals.

This works investigates the use of conditional deontic expressions which are called `anankastic conditionals’. These are expressions such as ``if you want to go to Harlem, you must take the A-train’', which relate strongly to means-end reasoning (e.g., taking the A-train is the best means for going to Harlem). We developed a deontic logic that allows us to logically reason with such conditionals, including deontic near-anankastic conditionals. Further investigation may be directed to a comparison of the logic of instrumentality developed for the Mīmāṃsā author Maṇḍana and the logic of anankastics (cf. `if you desire to kill your enemy, you must perform the Śyena’ in [Berkel,Ciabattoni,Freschi,Gulisano,Olszewski 2021]).

The paper gives an overview of logics of conditional obligation developed in modern times, using a semantical approach based on a betterness relation. This study should enable a fruitful comparison with the deontic logics presupposed by the Mīmāṃsā authors, and so will help to provide a better understanding of the specificities of these ones.

The logic of Bringing-it-About was introduced by Elgesem to formalise the notions of agency and capability. It contains two families of modalities indexed by agents, the first one expressing what an agent brings about (does), and the second expressing what she can bring about (can do). We first introduce a new neighbourhood semantics, defined in terms of bi-neighbourhood models for this logic, which is more suited for countermodel construction than the semantics defined in the literature. We then introduce a hypersequent calculus for this logic, which leads to a decision procedure allowing for a practical countermodel extraction. We finally extend both the semantics and the calculus to a coalitional version of Elgesem logic proposed by Troquard.

The logic of bringing-it-about represents a standard reference in the literature on agency logic. It provides a formalisation of agents’ actions in terms of their results: that an agent “does something” is interpreted as the fact that the agent brings about something. For instance, “John does a bank transfer” is interpreted as “John brings it about that the bank transfer is done”. Elgesem’s logic of bringing-it-about contains two modalities indexed by agents E_i and C_i. The former one expresses the agentive modality of bringing-it-about, whereas the latter one expresses capability: roughly speaking, E_lucy(BankTransfer) means that Lucy makes a bank transfer, whereas C_lucy(BankTransfer) means that Lucy can make a bank transfer. Elgesem’s logic is also well-suited for formalising notions of control, power, and delegation. Elgesem’s logic deals with actions of a single agent, who might be a human individual, or an institution or a group conceived as an indivisible entity. A natural extension of this logic is to handle groups or coalitions that act jointly to bring about an action. This has been proposed by Troquard who has developed an extension of Elgesem’s logic to handle “coalitions”: individuals may gather in coalitions to bring about a joint action. In such a joint action, each participant must be involved, so that the logic rejects coalition monotonicity: E_g(A) -> E_h(A) whenever g is included in h is not assumed to be valid. In this work we define the first proof systems for the logics of bringing-it-about that provide derivations or countermodels for all formulas. We also present a proof search algorithm based on the calculi that provides a decision procedure for the logics: given any formula, it establishes whether the formula is valid or not. This algorithm is also suitable to be implemented as a theorem prover for the logics.

We present some hypersequent calculi for all systems of the classical cube and their extensions with axioms T, P, and D, and for every n>=1, rule RD+n. The calculi are internal as they only employ the language of the logic, plus additional structural connectives. We show that the calculi are complete with respect to the corresponding axiomatization by a syntactic proof of cut elimination. Then, we define a terminating proof search strategy in the hypersequent calculi and show that it is optimal for coNP-complete logics. Moreover, we show that from every failed proof of a formula or hypersequent it is possible to directly extract a countermodel of it in the bi-neighbourhood semantics of polynomial size for coNP logics, and for regular logics also in the relational semantics. We finish the paper by giving a translation between hypersequent rule applications and derivations in a labelled system for the classical cube.

This paper extends the results of our previous article Countermodel construction via optimal hypersequent calculi for non-normal modal logics with the analysis of some standard deontic principles for obligations. The considered principles characterize normative codes in such a way that they cannot contain single impossible obligations, or two contradictory obligations, or arbitrary numbers of inconsistent obligations, namely obligations that cannot be fulfilled all together. We define some proof-systems for the non-normal logics characterized by these principles that allow one to derive all valid formulas in the logics. Our calculi are also suitable to define countermodels of non-valid formulas in an optimal way, and to be implemented in the form of automated theorem provers.

We introduce a modular and transparent approach for aug-menting the ability of reinforcement learning agents to comply with agiven norm base. The normative supervisor module functions as bothan event recorder and real-time compliance checker w.r.t. an externalnorm base. We have implemented this module with a theorem prover fordefeasible deontic logic, in a reinforcement learning agent that we taskwith playing a “vegan” version of the arcade game Pac-Man.

The paper adresses to computer scientists and AI practictioners. It implements one of the Mīmāṃsā principles to tackle a key problem in autonomous agents: how to choose between actions that should be avoided. We tested our method on variations of the Pac-Man game, subject to a variety of “ethical” constraints. Reinforcement learning (RL) is the state of the art methodology to teach to autonomous agents how to adapt to (potentially unpredictable) changes in their environment. Performing human roles, however, elicits the further requirement that agents should align themselves with the ethical standards their human counterparts are subject to, introducing an additional requirement for ethical reasoning. We propose a modular and transparent approach for augmenting the ability of RL agents to comply with a given -- external -- norm base. We introduce a normative supervisor implemented with a theorem prover for defeasible deontic logic. We place the normative supervisor in the already-trained agent’s control loop between the localization and policy module. When at a given state the RL policy cannot propose any solution compliant with the norm base, we use one of the "suspension commands" from Mīmāṃsā (so called economicity principle) to select the ‘Lesser of two Evils’ solutions.

Over the course of more than two millennia the philosophical school of Mīmāṃsā has thoroughly analyzed normative statements. In this paper we approach a formalization of the deontic system which is applied but never explicitly discussed in Mīmāṃsā to resolve conflicts between deontic statements by giving preference to the more specific ones. We first extend with prohibitions and recommendations the non-normal deontic logic extracted in Ciabattoni et al. (2015) from Mīmāṃsā texts, obtaining a multi modal dyadic version of the deontic logic MD. Sequent calculus is then used to close a set of prima-facie injunctions under a restricted form of monotonicity, using specificity to avoid conflicts. We establish decidability and complexity results, and investigate the potential use of the resulting system for Mīmāṃsā philosophy and, more generally, for the formal interpretation of normative statements.

The paper is an extended version of the DEON 2018 paper. It is addressed mainly to proof theorists and (deontic) logicians. It formalizes Mīmāṃsā reasoning that uses the principles called Guṇapradhāna and Vikalpa, to resolve apparent contradictions in the Vedas. The former, known in AI as specificity principle, states that more specific rules override more generic ones. The latter, known in deontic logic as disjunctive response, states that when there is a real conflict between obligations, any of the conflicting injunctions may be adopted as option. Vikalpa is considered by Mīmāṃsā as a last resort, and hence it has to be used with care. In this paper we extend the Basic Mīmāṃsā Deontic Logic bMDL with the (non derivable) operators of Recommendation and Prohibition AND with a proof-theoretic mechanism to deal with Guṇapradhāna and Vikalpa. We establish decidability and complexity results for the resulting logic, and investigate the potential use of the resulting system for Mīmāṃsā philosophy and, more generally, for the formal interpretation of normative statements.

The article offers an overview of the deontic theory developed by the philosophical school of Mīmāṃsā, which is, and has been since the last centuries BCE, the main source of normative concepts in Sanskrit thought. Thus, the Mīmāṃsā deontics is interesting for any historian of philosophy and constitutes a thought-provoking occasion to rethink deontic concepts taking advantage of centuries of systematic reflections on these topics. Some comparison with notions currently used in Euro-American normative theories and metaethical principles is offered in order to show possible points of contact and deep divergences.
More in detail, after an introduction explaining the methodology and aims of our work, we discuss how Mīmāṃsā authors distinguished and defined some fundamental deontic concepts, such as different types of prescriptions and prohibitions. We then discuss how Mīmāṃsā authors approached the problem of conflicts among commands without jeopardising the validity of the normative text issuing them. In the second part of the article we introduce our formal apparatus, which is construed around the main taxonomic and conceptual distinctions used in the first part. Our formal rendering captures the most important features of the Mīmāṃsā theory, and can thus serve as a concise and rigorous presentation of it for scholars working in deontic logic.

The article offers an overview of the deontic theory developed by the philosophical school of Mīmāṃsā. We discuss how Mīmāṃsā authors distinguished and defined some fundamental deontic concepts, such as different types of prescriptions and prohibitions. We then discuss how Mīmāṃsā authors approached the problem of conflicts among commands without jeopardising the validity of the normative text issuing them. Some comparison with notions currently used in Euro-American normative theories and metaethical principles is offered in order to show possible points of contact and deep divergences.