K. van Berkel, A. Ciabattoni, E. Freschi, F. Gulisano, and M. Olszewski The Gentle Murder Paradox in Sanskrit Philosophy . To appear in: Fenrong Liu, Alessandra
Marra, Paul Portner, and Frederik Van De Putte (eds.). Deontic Logic and
Normative Systems: 15th International Conference (DEON2020/2021,
Munich). London: College Publications, 2021.
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.
In this work we discuss three logics of the prominent Mīmāṃsā philosophers
Prabhākara, Kumārila, and Maṇḍana. Their theories of normative reasoning are distinct and
were influential to the history of the Mīmāṃsā. We discuss these theories and their corresponding logic in the light of the
Śyena controversy, a controversy surrounding the killing one's enemy by performing the Śyena.
We use logical methods to show the three authors' different solutions to the Śyena. Furthmore, we
observe that the controversy is akin to a central challenge in deontic logic called the Gentle Murder Paradox. Correspondingly,
we obtain three Mīmāṃsā based solutions to this contemporary paradox in deontic logic.
K. van Berkel, D. Gabbay, and L. van der Torre If you want to smoke,don’t buy cigarettes: near-anankastics, contexts, and hyper modality . To appear in: Fenrong Liu, Alessandra
Marra, Paul Portner, and Frederik Van De Putte (eds.). Deontic Logic and
Normative Systems: 15th International Conference (DEON2020/2021,
Munich). London: College Publications, 2021.
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]).
X. Parent Preference Semantics for Hansson-type
Dyadic Deontic Logic: A Survey of Results . To appear in : D. Gabbay, J.
Horty, X. Parent, R. van der Meyden and L. van der Torre, Handbook of
Deontic Logic ans Normative Systems, Volume 2, College Publications, UK
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.
T. Dalmonte, C. Grellois, N. Olivetti Proof systems for the logics of bringing-it-about . To appear in: Fenrong Liu, Alessandra
Marra, Paul Portner, and Frederik Van De Putte (eds.). Deontic Logic and
Normative Systems: 15th International Conference (DEON2020/2021,
Munich). London: College Publications, 2021.
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.
T. Dalmonte, B. Lellmann, N. Olivetti, E. Pimentel. Hypersequent calculi for non-normal modal and deontic logics: countermodels and optimal complexity.
Journal of Logic and Computation, Volume 31, Issue 1, January 2021, Pages 67–111.
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.
E. Neufeld, E. Bartocci, A. Ciabattoni and G. Governatori. A Normative Supervisor for ReinforcementLearning Agents. Accepted for
publications to CADE 2021 (forthcoming).
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.
Lellmann, B., Gulisano, F., and Ciabattoni, A. Mīmāṃsā Deontic Reasoning using Specificity: A Proof Theoretic Approach.
In: Artificial Intelligence and Law (forthcoming) (2021)
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.
Freschi, E. and Pascucci, M. Deontic concepts and their clash in Mīmāṃsā: Towards an interpretation.
In: Theoria (2021)
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.
2020
Ciabattoni, A., and Lellmann, B. Sequent Rules for Reasoning and Conflict Resolution in Conditional Norms.
In: F. Liu, A. Marra, P. Portner, F. Van De Putte (Eds.): Deontic Logic and
Normative Systems: 15th International Conference (DEON2020/2021 Munich).
College Publications, London, (2020)
We introduce a sequent based method for reasoning with deontic assumptions using
specificity and superiority for conflict resolution. In short, the principle of
specificity states that, in case of conflicting norms, the more specific norm overrides
the more general one. We illustrate the method using various examples. An
implementation of the prover is also available at .
Olszewski, M., Parent, X., and van der Torre, L. Input/output logic with a consistency check – the case of permission.
In: F. Liu, A. Marra, P. Portner, F. Van De Putte (Eds.): Deontic Logic and
Normative Systems: 15th International Conference (DEON2020/2021 Munich).
College Publications, London, (2020)
In this paper, we focus on one of the less explored sides of
input-output logic, namely permission. Permission in input/output logic
has only been studied in the original framework. In this article, we
look at different kinds of permission operations with new input/output
logics as the underlying obligation operations. As opposed to the logics
from the original framework , those new logics allow for
contrary-to-duty reasoning by having a built-in consistency check which
filters out excess output and they are not closed under logical
consequence. We propose rule-sets to describe each of the three kinds of
permission studied, and get a characterization result for positive
static permission with its rule-set. This is the definition of a first
positive permission proof system for constrained output.
van Berkel, K., and Lyon, T. The Varieties of Ought-implies-Can and Deontic STIT Logic.
In: F. Liu, A. Marra, P. Portner, F. Van De Putte (Eds.): Deontic Logic and
Normative Systems: 15th International Conference (DEON2020/2021 Munich).
College Publications, London, (2020)
The principle of Ought-implies-Can fulfills a central role in formal systems
normative reasoning. However, in the philosophical literature we find a large
variety of OiC interpretations. Which principle should be formally adopted?
This paper provides a modular framework for deontic agency logic accounting for
a multitude of OiC readings. In particular, we discuss, compare, and formalize
ten such readings. We formally analyze the resulting systems and discuss how
the different OiC principles are logically related. In particular, we propose
an endorsement principle describing which OiC readings logically commit one to
accepting others.
E. Freschi. Reconstructing an episode in the history of philosophy: arthāpatti in
Kumārila’s commentators.
In: F. Sferra, V. Vergiani (eds.), Festschrift for Raffaele Torella. (forthcoming)
This article explains the interpretation of the chapter dedicated to the
epistemological instrument called arthāpatti in one of the masterpieces of
the Sanskrit philosopher Kumārila Bhaṭṭa. Kumārila was one of the main
authors of the Mīmāṃsā school and a profound innovator when it comes to
Mīmāṃsā logic and epistemology. His commentators prosecute some of these
developments and fine-tune others.
E. Freschi. Mīmāṃsā between epistemology and hermeneutics: The history of arthāpatti.
In: V. Eltschinger et al (eds.), Festschrift for John Taber. (forthcoming)
This article discusses the historical evolution of the epistemological teachings
of the Mīmāṃsā school using the case-study of arthāpatti. This is an instrument
of knowledge considered to be different from syllogistic inference by Mīmāṃsā
authors. Different authors individuate its peculiarity in the fact that it involves
quantification (Kumārila) or that it involves belief revision (Śālikanātha).
E. Freschi and A. Ollett. Kumārila Bhatta's Explanation in Verse. In: M. Keating (Ed.): Controversial
Reasoning in Indian Philosophy: Major Texts and Arguments on Arthâpatti.
Bloomsbury (2020), chapter 1
Arthāpatti is an instrument of knowledge considered by Mīmāṃsā authors to be distinct from inference. This article analyses the stance on arthāpatti of the Mīmāṃsā author Kumārila (6th c. CE?), who analyses the formal structure of inference and arthāpatti and shows their differences. In particular, the syllogistic form of inference cannot be reconstructed in the case of arthāpatti, which implies a quantification. Kumārila also discusses at length the case of arthāpatti applied to linguistic expressions.
This article focuses on the epistemology of the Mīmāṃsā school and discusses
the formal structure of an instrument of knowledge allegedly distinct from
that of syllogism.
E. Freschi and A. Ollett. Prabhākara's Long Explanation. In: M. Keating (Ed.): Controversial Reasoning in
Indian Philosophy: Major Texts and Arguments on Arthâpatti. Bloomsbury (2020), chapter 2.
Arthāpatti is an instrument of knowledge considered by Mīmāṃsā authors to be distinct from inference. This article analyses the stance on arthāpatti of the Mīmāṃsā author Prabhākara (6th c. CE?), who analyses inference and arthāpatti and shows their differences insofar as in the case of inference one moves from the effect (e.g., smoke) to the cause (e.g., fire), insofar as without it the effect would not be possible. By contrast, the direction of reasoning is reversed in the case of arthāpatti.
This article focuses on the epistemology of the Mīmāṃsā school and discusses
the formal structure of an instrument of knowledge allegedly distinct from
that of syllogism.
E. Freschi and A. Ollett. Śālikanātha's Straightforward and Lucid Gloss; Comprehensive Survey of the Epistemic
Instruments. In: M. Keating (Ed.): Controversial Reasoning in
Indian Philosophy: Major Texts and Arguments on Arthâpatti. Bloomsbury (2020), chapter 3.
Arthāpatti is an instrument of knowledge considered by Mīmāṃsā authors to be
distinct from inference. This article analyses the stance on arthāpatti of the
Mīmāṃsā author Śalikanātha (9th c. CE?), who identifies the distinctive element
of arthāpatti in the epistemological crisis it creates in the knower who, for a
moment, sees her beliefs challenged. The knower's reaction is the needed belief
update which is the real form of arthāpatti. Śālikanātha also refutes the case
of arthāpatti based on linguistic expressions and concludes that there is not
such a distinct arthāpatti, since one's belief update needs to reach the level
of meaning, and cannot remain at the level of language only.
This article focuses on the epistemology of the Mīmāṃsā school and discusses
the formal structure of an instrument of knowledge allegedly distinct from
that of syllogism.
K. van Berkel, T. Lyon, F. Olivieri.
A Decidable Multi-agent Logic for Reasoning About Actions, Instruments, and Norms.
In: M. Dastani, H. Dong, L. van der Torre (Eds.): Proceedings of CLAR 2020. LNCS, vol.12061, pp.219-241, Springer
We formally introduce a novel, yet ubiquitous, category of norms: norms of
instrumentality. Norms of this category describe which actions are obligatory,
or prohibited, as instruments for certain purposes. We propose the Logic of
Agency and Norms (L𝖠𝖭) that enables reasoning about actions, instrumentality,
and normative principles in a multi-agent setting. Leveraging 𝖫𝖠𝖭, we
formalize norms of instrumentality and compare them to two prevalent norm
categories: norms to be and norms to do. Last, we pose principles relating
the three categories and evaluate their validity vis-à-vis notions of
deliberative acting. On a technical note, the logic will be shown decidable
via the finite model property.
In this work we present a logic that enables reasoning about obligations and
prohibitions in a multi-agent setting. In particular, we introduce a novel,
previously understudied, category of norms: norms of instrumentality. Norms
of this category describe which actions are obligatory (prohibited) as
instruments for certain purposes. Such norms are, for instance, ubiquitous
in protocols: e.g. ``a surgeon is obliged to use a scalpel (action) to bring
about (instrument) a necessary incision during surgery (result)’’. We discuss
this category in relation to available norm classes from the literature and
study a protocol example.
D. Glavaničová and M. Pascucci A realistic view on normative conflicts. Logic and Logical Philosophy. Published online: February 4, 2020.
Kulicki and Trypuz (2016) introduced three systems of multivalued deontic action logic
to handle normative conflicts. The first system suggests a pessimistic view on normative
conflicts, according to which any conflicting option represents something forbidden; the
second system suggests an optimistic view, according to which any conflicting option
represents something obligatory; finally, the third system suggests a neutral view, according
to which any conflicting option represents something that is neither obligatory nor forbidden.
The aim of the present paper is to propose a fourth system in this family, which comes with
a realistic view on normative conflicts: a normative conflict remains unsolved unless it is
generated by two or more normative sources that can be compared. In accordance with this, we
will provide a more refined formal framework for the family of systems at issue, which allows
for explicit reference to sources of norms. Conflict resolution is thus a consequence of a
codified hierarchy of normative sources.
The present article is addressed to logicians. It introduces a logical system in which
normative sources assign a deontic value to actions and can be used to solve cases of
conflict among norms.
S. Saxena.
When Texts Clash: Mīmāṃsā Thinkers on Conflicting Prescriptions and Prohibitions.
Journal of Indian Philosophy. Published online 02 April 2020.
The Mīmāṃsā mission of disambiguating Vedic texts led the thinkers of the tradition
to confront several instances of apparently conflicting Vedic commands. Consider the
two cases: ‘give alms daily’ vs ‘do not give alms during ritual X’, and ‘never harm
another’ vs ‘sacrifice an animal during ritual Y’. Each command in these two cases is
derived from the Vedas and Mīmāṃsā authors thus attempted to resolve such cases of
deontic conflict by putting forth hermeneutic solutions, without taking recourse to
any other epistemic source. In this paper, I present several instances of conflicting
Vedic commands and indicate three distinct types of deontic conflicts as well as their
corresponding solutions as identified by Mīmāṃsā thinkers. This study is based on
discussions put forth in four important Mīmāṃsā texts: the Pūrvamīmāṃsāsūtra, the
Śābarabhāṣya, Kumārila’s Ṭupṭīkā and Āpadeva’s Mīmāṃsānyāyaprakāśa. I explain the
foundational difference between prescriptions (vidhi) and prohibitions (pratiṣedha
/ niṣedha) for Mīmāṃsā thinkers, and thereby also discuss several technical conceptions
such as paryudāsa, vikalpa, prāpti and bādha among others. In doing so, I attempt
to highlight certain fundamental tenets of the vast and intricate hermeneutic
framework developed within the Mīmāṃsā tradition.
The Mīmāṃsā mission of disambiguating Vedic texts led the thinkers of the tradition
to confront several instances of apparently conflicting Vedic commands. In this paper,
Saxena presents several instances of conflicting Vedic commands and indicates three
distinct types of deontic conflicts as well as their corresponding solutions as
identified by Mīmāṃsā thinkers. In doing so, he highlights certain fundamental tenets
of the vast and intricate hermeneutic framework developed within the Mīmāṃsā tradition.
T. Dalmonte, B. Lellmann, N. Olivetti, E. Pimentel.
Countermodel construction via optimal hypersequent calculi for
non-normal modal logics.
In: S. Artemov, A. Nerode (Eds.): Proceedings of LFCS 2020. LNCS, vol.11972, pp.27-46, Springer
We develop semantically-oriented calculi for the cube of non-normal modal
logics and some deontic extensions. The calculi manipulate hypersequents
and have a simple semantic interpretation. Their main feature is that they
allow for direct countermodel extraction. Moreover they provide an optimal
decision procedure for the respective logics. They also enjoy standard
proof-theoretical properties, such as a syntactical proof of cut-admissibility.
This article continues the investigation into proof-theoretic formalisms suitable
for generating countermodels for non-normal modal and deontic logics. In contrast
to the previous article Combining monotone and normal modal logics in nested
sequents -- with countermodels, the operators here do not need to be monotone.
This is relevant, since operators for conditional obligations are typically not
monotone in the argument representing the condition.
E. Freschi The Deontic Nature of Language in the Mīmāṃsā school and thereafter.
In: Alessandro Graheli (ed.) The Bloomsbury handbook of Indian philosophy of language. Bloomsbury, London, chapter 15.
The authors of the Nyāya school are generally upholders of a Tractatus-like view of language
as reproducing ontologically given states of affairs in a way which preserves their epistemic validity.
In other words, a sentence like ``The cat is on the mat'' simply describes the state of affairs of a
feline lying on a piece of soft textile. This view might appear to be the obvious option to Euro-American
readers, who are surely familiar with it, but it was by no means the only one in the history of early
Indian reflections on language. This contribution discuss the idea that language communicates a
deontic meaning, i.e. something to be done. First the view of the Mīmāṃsā school
about language communicating a deontic meaning is discussed. Then, its epistemological and logical
consequences are assessed. Last, the Vedānta approach to the Veda is analysed. Śaṅkara
distinguishes sharply between parts of the Veda such as the Brāhmaṇas, which convey a deontic
meaning, and others, such as the Upaniṣads, which convey a truthful description of the brahman. Rāmānuja
harmonises the two by stating that all Vedic statements convey descriptions. Veṅkaṭanātha
reinserts Mīmāṃsā assumptions into the picture by noting that it is only on the
basis of truthful descriptions that purposes can be conveyed and that therefore deontic meanings depend
on descriptive ones.
This paper is addressed to philosophers of language and historians of (Indian)
philosophy and explains the Mīmāṃsā theories of language as conveying a purpose
or a duty. According to this approach, the sacred texts (or language in general)
communicate a meaning which is necessarily deontic, i.e., it is something to be
done. Authors of the Bhāṭṭa sub-school of Mīmāṃsā stress more the fact that this
is a purpose, whereas authors of the Prābhākara sub-school stress more its being a duty.
E. Freschi Meanings of Words and Sentences in Mīmāṃsā
In: Alessandro Graheli (ed.) The Bloomsbury Handbook of Indian Philosophy of Language. Bloomsbury, London, chapter 9.
What is the meaning (in Sanskrit vācya)? What is the carrier of the meaning
(in Sanskrit vaācaka)? In other words, how can one identify the linguistically
relevant elements on the side of the meaning and on the side of the expressive factors?
The typical candidates for the latter role are phonemes, individual morphemes or words,
whole sentences or the sphoṭa. As for the meaning, different schools identify
it as corresponding to the exclusion of everything else (\emph{apoha}), to an entity in
the external world (so Nyāya), to a complex state of affairs (so the Bhāṭṭa
interpretation of worldly language and the Vedaānta one), to a duty (so the Praābhaākaras).
One view influences the other, since if one identifies the meaning conveyed in linguistic
communication (śābda) as a duty, one needs to take into account the
perspective of a whole sentence, whereas other theories may favour a more atomistic approach.
In this contribution, I analyse the Mīmāṃsā answer to these questions
through the two theories of abhihitānvaya- and anvitābhidhānavāda.
This paper is addressed to philosophers of language and historians of
(Indian) philosophy and explains the Mīmāṃsā theories of language. What
is the meaning? What is the carrier of the meaning? In other words,
how can one identify the linguistically relevant elements on the side of
the meaning and on the side of the expressive factors? As for the meaning,
different schools identify it as corresponding to an entity in the external
world, to a complex state of affairs, to a duty (so the Prābhākara
sub-school of Mīmāṃsā), etc. One view influences the other, since if one
identifies the meaning conveyed in linguistic communication as a duty, one
needs to take into account the perspective of a whole sentence, whereas
other theories may favour a more atomistic approach.
2019
D. Glavaničová and M. Pascucci Formal analysis of responsibility attribution in a multimodal framework. In: M. Baldoni et al (Eds.): Proceedings of PRIMA 2019. LNCS, vol. 11873, pp.36-51. Springer.
The present article is devoted to a logical treatment of some fundamental concepts involved in responsibility attribution. We specify a theoretical framework based on a language of temporal deontic logic with agent-relative operators for deliberate causal contribution. The framework
is endowed with a procedure to solve normative conflicts which arise from the assessment of different normative sources. We provide a characterization result for a basic system within this framework and illustrate how the concepts formalized can be put at work in the analysis of examples of legal reasoning.
This work is addressed to logicians. It provides essential formal tools to represent judgements of responsibility with respect to certain courses of events.
K. van Berkel and T. Lyon. A Neutral Temporal Deontic STIT Logic. In: P. Blackburn et al (Eds.): Proceedings of LORI 2019. LNCS, vol.11813, pp.340-354. Springer.
In this work we answer a long standing request for temporal embeddings of deontic STIT
logics by introducing the multi-agent STIT logic TDS. The logic is based upon atemporal
utilitarian STIT logic. Yet, the logic presented here will be neutral: instead of
committing ourselves to utilitarian theories, we prove the logic TDS sound and complete
with respect to relational frames not employing any utilitarian function. We demonstrate
how these neutral frames can be transformed into utilitarian temporal frames, while
preserving validity. Last, we discuss problems that arise from employing binary utility
functions in a temporal setting.
We present a formalism that allows us to reason about obligations of agents in a temporal
context. With this formalism we analyze some of the consequences of considering available
formal utilitarian theories in a temporal setting.
K. van Berkel, A. Ciabattoni, E. Freschi, and S. Modgil.
Evaluating Networks of Arguments: A Case Study in Mīmāṃsā Dialectics.
In: P. Blackburn et al (Eds.): Proceedings of LORI 2019. LNCS, vol.11813, pp.355-369. Springer.
We formalize networks of authored arguments. These networks are then mapped to
ASPIC+ theories that subsequently instantiate Extended Argumentation Frameworks.
Evaluation of arguments in the latter determines the status of the arguments in
the source networks. The methodology is illustrated through a collaboration
between scholars of South Asian philosophy, logicians and formal argumentation
theorists, analyzing excerpts of Sanskrit texts concerning a controversial
normative debate within the philosophical school of Mīmāṃsā.
In this paper we consider a formal tool ASPIC+ for representing and analyzing
argument structures and the relations between arguments. We apply these tools
and analyse a part of the Mīmāṃsā debate around a controversial Vedic ritual
known as sati; the immolation of widows on their husbands' funeral pyre. This
debate has had deep socio-political implications in India since the 9th c.
until today.
T. Libal and M. Pascucci Automated reasoning in normative detachment structures with ideal conditions. In: Proceedings of ICAIL 2019. Pp.63-72. ACM.
In this article we introduce a logical structure for normative reasoning, called Normative
Detachment Structure with Ideal Conditions, that can be used to represent the content of
certain legal texts in a normalized way. The structure exploits the deductive properties of
a system of bimodal logic able to distinguish between ideal and actual normative statements,
as well as a novel formalization of conditional normative statements able to capture
interesting cases of contrary-to-duty reasoning and to avoid deontic paradoxes. Furthermore,
we illustrate how the theoretical framework proposed can be mechanized to get an automated
procedure of query-answering on an example of legal text.
The present article is addressed to logicians and legal experts. It introduces a general
framework for the automated analysis of tasks of normative reasoning related to legal
texts. As a case study, we analyse some articles from the United Nations Convention on
Contracts for the International Sale of Goods.
B. Lellmann. Combining monotone and normal modal logic in nested sequents -- with countermodels.
In: S. Cerrito and A. Popescu (Eds.): TABLEAUX 2019. LNCS, vol.11714, pp.203-220. Springer.
We introduce nested sequent calculi for bimodal monotone modal logic, aka. Brown’s
ability logic, a natural combination of non-normal monotone modal logic M and normal
modal logic K. The calculus generalises in a natural way previously existing calculi
for both mentioned logics, has syntactical cut elimination, and can be used to
construct countermodels in the neighbourhood semantics. We then consider some
extensions of interest for deontic logic. An implementation is also available.
This article is addressed to logicians and proof-theorists. Apart from contributing
to the general theory of proof systems for modal and deontic logics, it develops
the technical foundations for providing actual certificates for the underivability
statements used in the treatment of the specificity principle in our previous article
Resolving Conflicting Obligations in Mīmāṃsā: A Sequent-based Approach.
R. Goré and B. Lellmann. Syntactic cut-elimination and backward proof-search for tense logic via linear nested sequents.
In: S. Cerrito and A. Popescu (Eds.): TABLEAUX 2019. LNCS, vol.11714, pp.185-202. Springer.
We give a linear nested sequent calculus for the basic normal tense logic Kt. We
show that the calculus enables backwards proof-search, counter-model construction
and syntactic cut-elimination. Linear nested sequents thus provide the minimal
amount of nesting necessary to provide an adequate proof-theory for modal logics
containing converse. As a bonus, this yields a cut-free calculus for symmetric
modal logic KB.
This article is mainly addressed to logicians and proof-theorists, and explores the
theoretical foundations of the project. In particular, it provides important insight
into the expressive strength of the linear nested sequent framework. This is
particularly relevant for deciding which proof-theoretic framework to use for the
deontic logics developed in the project.
E. Pimentel, R. Ramanayake and B. Lellmann.
Sequentialising nested sequents. In: S. Cerrito and A. Popescu (Eds.): TABLEAUX 2019. LNCS, vol.11714, pp.147-165. Springer.
In this work, we investigate the proof theoretic connections between sequent and
nested proof calculi. Specifically, we identify general conditions under which a
nested calculus can be transformed into a sequent calculus by restructuring the
nested sequent derivation (proof) and shedding extraneous information to obtain a
derivation of the same formula in the sequent calculus. These results are
formulated generally so that they apply to calculi for intuitionistic, normal
modal logics and negative modalities.
This article is addressed to logicians and proof-theorists. It provides very general
insights into the expressive strength of the nested sequent framework compared to the
sequent framework. Its relevance for the project lies in the fact that a good understanding
of these issues is fundamental for choosing the appropriate proof-theoretical framework for
the logics developed in the project.
E. Freschi, A. Ollett and M. Pascucci
Duty and sacrifice. A logical analysis of the Mīmāṃsā theory of Vedic injunctions.
History and Philosophy of Logic 40(4), pp.323-354 (2019).
The Mīmāṃsā school of Indian philosophy has for its main purpose the interpretation of
injunctions that are found in a set of sacred texts, the Vedas. In their works, Mīmāṃsā authors provide
some of the most detailed and systematic examinations available anywhere of statements with a deontic
force; however, their considerations have generally not been registered outside of Indological scholarship.
In the present article we analyze the Mīmāṃsā theory of Vedic injunctions from a logical and philosophical
point of view. The theory at issue can be regarded as a system of reasoning based on certain fundamental
principles, such as the distinction between strong and weak duties, and on a taxonomy of ritual actions.
We start by reconstructing the conceptual framework of the theory and then move to a formalization
of its core aspects. Our contribution represents a new perspective to study Mīmāṃsā and outlines its
relevance, in general, for deontic reasoning.
This article is addressed to the communities of Sanskritists and philosophical logicians. We introduce a logical framework in which it is possible to represent some key-features of the taxonomy of Vedic injunctions developed by Mīmāṃsā authors. In particular, we show that Vedic injunctions basically concern the performance of fixed, occasional and elective sacrifices. Furthermore, we point out the fact that injunctions can make reference either to the principal ritual action or to a subsidiary action within a certain sacrifice, as well as the fact that an injunction is always triggered by some eligibility conditions.
K. van Berkel and T. Lyon. Cut-free Calculi and Relational Semantics for Temporal STIT logics.
In: F. Calimeri et al (Eds.): JELIA 2019. LNAI, vol.11468, pp.803-819. Springer.
We present cut-free labelled sequent calculi for a central
formalism in logics of agency: STIT logics with temporal operators.
These include sequent systems for Ldm, Tstit and Xstit. All calculi pre-
sented possess essential structural properties such as contraction- and
cut-admissibility. The labelled calculi G3Ldm and G3Tstit are shown
sound and complete relative to irreflexive temporal frames. Additionally,
we extend current results by showing that also Xstit can be characterized
through relational frames, omitting the use of BT+AC frames.
This paper is mainly directed to philosophers and logicians interested in the
proof-theoretic behavior of interaction between agents. That is, we provide a
proof theory for several versions of one of the fundamental logics of agency:
STIT logic. STIT is an acronym for `Seeing To It That' and has been developed
for the formal investigation of multi-agent interaction and group-choice making.
This paper is a preparatory work and we aim to extend this work to incorporate
Deontic STIT logic in order to investigate the formal aspects of normative choice-making.
M. Girlando, B. Lellmann and N. Olivetti.
Nested sequents for the logic of conditional belief.
In: F. Calimeri et al (Eds.): JELIA 2019. LNAI, vol.11468, pp.709-725. Springer.
The logic of conditional belief, called Conditional Doxastic Logic (CDL), was
proposed by Board, Baltag and Smets to model revisable belief and
knowledge in a multi-agent setting. We present a proof system for CDL
in the form of a nested sequent calculus. To the best of our
knowledge, ours is the first internal and standard calculus for this
logic. We take as as primitive a multi-agent version of the
“comparative plausibility operator”, as in Lewis’ counterfactual
logic. The calculus is analytic and provides a decision procedure for
CDL. As a by-product we also obtain a nested sequent calculus for
multi-agent modal logic S5i .
This article is addressed mainly to logicians and proof-theorists. It
introduces a novel proof-theoretic calculus for the logic of
conditional beliefs, which is used to model how agents can revise
their beliefs in the face of new information. This logic is related to
a class of deontic logics of potential relevance to deontic reasoning
in Mīmāṃsā. The main point of interest for the project however lies in
the methods employed in the construction of the nested sequent
calculus. These yield insights highly relevant to the development of
general methods for the construction of nested sequent calculi for
non-normal modal and deontic logics.
B. Lellmann and E. Pimentel Modularisation of sequent calculi for normal and non-normal modalities. ACM Transactions on Computational Logic 20(2), Article 7 (2019)
In this work we explore the connections between (linear) nested sequent calculi
and ordinary sequent calculi for normal and non-normal modal logics. By proposing
local versions to ordinary sequent rules we obtain linear nested sequent calculi for a
number of logics, including to our knowledge the first nested sequent calculi for
a large class of simply dependent multimodal logics, and for many standard non-normal
modal logics. The resulting systems are modular and have separate left and right
introduction rules for the modalities, which makes them amenable to specification as
bipole clauses. While this granulation of the sequent rules introduces more choices
for proof search, we show how linear nested sequent calculi can be restricted to
blocked derivations, which directly correspond to ordinary sequent derivations.
This paper is addressed mainly to proof-theorists and logicians. It addresses the
technical issue of how to obtain modular derivation systems for normal and non-normal
modal logics. In particular, we investigate how to convert sequent calculi into (linear)
nested sequent calculi, a proof-theoretic framework which is much more suitable for
modularly capturing large classes of logics. Together with earlier work on the conversion
of axioms into sequent rules this provides some fundamental methods for the construction
of derivation systems for logics extracted from the Mīmāṃsā texts in
the form of axiomatic systems.
2018
A. Ciabattoni, B. Lellmann and K. van Berkel Deontic Reasoning: From Ancient Texts To Artificial Intelligence: Workshop Report. SIGLOG News 5(4): 48-51 (2018)
The interdisciplinary workshop 'Deontic Reasoning: from Ancient Texts to Artificial Intelligence' (ATAI), bringing together experts from the fields of Logic, Sanskrit, Philosophy, Artificial Intelligence and Law, was held at the Vienna University of Technology (TU Wien) on June 11-13, 2018. In nuce, the aim of the workshop was to foster new connections between the aforementioned research areas and facilitate the interchange of ideas with respect to shared grounds of interest, in particular normative reasoning.
K. van Berkel and M. Pascucci Notions of Instrumentality in Agency Logic. In: Miller T., Oren N., Sakurai Y., Noda I., Savarimuthu B., Cao Son T. (eds)
PRIMA 2018: Principles and Practice of Multi-Agent Systems. PRIMA 2018. Lecture Notes in Computer Science, vol 11224. Springer, Cham
We present a logic of agency called LAE whose language includes propositional constants
for actions and expectations. The logic is based on Von Wright’s theory of agency in
general and his analysis of instrumentality in particular. An axiomatization of the logic,
including an independence of agents axiom, is provided and soundness and completeness
are shown with respect to its intended class of frames. The framework of LAE will allow
us to formally define a manifold of concepts involved in agency theories, including
Von Wright’s four elementary forms of action, the notion of forbearance and notions of
instrumentality that make reference to an agent’s expectations.
This paper is addressed to logicians and philosophers interested in the formal investigation
of agency. We start with an analysis of Von Wright’s theory of agency, describing what
we mean when we ascribe agency to a human being. We focus on three core concepts:
`action’, `ability’ and `instrument’ (i.e. means to an end). In particular, we investigate
different notions of instrumentality related to an agent’s expectations about the future
performance of an instrument with respect to its purpose. We introduce a new logic of actions
and expectations, called LAE, with which we formally capture and analyze these philosophical
definitions. For example, the logic enables us to capture and explain scenarios in which
some agent expects that some instrument will generate a particular outcome but becomes
disappointed instead. On the long run, this formalization will be applied for a rigorous
analysis of the role played by notions of instrumentality in deontic scenarios.
E. Freschi The role of paribhāṣās in Mīmāṃsā: rational rules of textual exegesis.
In: G. Pellegrini (eds.): Meanings out of Rules! Definitions, functions and uses of paribhāṣās in Śrautasūtras, Vyākaraṇa, Mīmāṃsā and Vedānta. Asiatische Studien/Études Asiatiques, vol.72, 2. pp.567-595. (2018)
This article provides a first investigation on the metarules adopted in the Mīmāṃsā
school of textual exegesis. These are not systematically listed and discussed,
but they can be seen at work throughout the history of Mīmāṃsā.̄ The Mīmāṃsā school
has the exegesis of the sacred texts called Veda as its main focus. The metarules
used to understand the Vedic texts are, however, not derived from the Veda itself
and are rather rational rules which can be derived from the use of language in
general and which Mīmāṃsā authors recognized and analyzed. Since the metarules are
considered to be not derived from the Veda, it is all but natural that later authors
inspired by Mīmāṃsā apply them outside the precinct of the Veda, for instance in the
fields of textual linguistics, poetics, theology and jurisprudence.
A. Ciabattoni, F. Gulisano and B. Lellmann Resolving Conflicting Obligations in Mīmāṃsā: A Sequent-based Approach.
In: J. Broersen, C. Condoravdi, S. Nair, G. Pigozzi (eds.): Proceedings of DEON 2018, pp.91-109. College Publications (2018).
The Philosophical School of Mīmāṃsā provides a treasure trove of more
than 2000 years worth of deontic investigations. In this paper we
formalize the Mīmāṃsā approach of resolving conflicting obligations
by giving preference to the more specific ones. From a technical point
of view we provide a method to close a set of prima-facie obligations
under a restricted form of monotonicity, using specificity to avoid
conflicting obligations in a dyadic non-normal deontic logic. A
sequent-based decision procedure for the resulting logic is also
provided.
The paper is addressed mainly to proof theorists and (deontic) logicians.
It investigates Mīmāṃsā reasoning using the principles to resolve apparent
contradictions in the Vedas, called Guṇapradhāna and Vikalpa.
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.
In this paper we extend the logic bMDL introduced
in (Ciabattoni et al. 2015) with a proof-theoretic mechanism
to deal with Guṇapradhāna and Vikalpa. More specifically, the sequent calculus
for bMDL is extended by rules that handle the non-monotonic way of Mīmāṃsā
reasoning from explicit (prima-facie) obligations found in the Vedas (called
Śrauta) to all-things-considered obligations. As such it constitutes an
important step in the project of formalising Mīmāṃsā deontic reasoning.
A prototype implementation of the methods from this paper is available
as deonticProver.
A. Ciabattoni and F. Genco Hypersequents and Systems of Rules: Embeddings and Applications.
ACM Transaction on Computational Logic 19(2), Article 11 (2018).
We define a bi-directional embedding between hypersequent calculi and
a subclass of systems of rules (2-systems). In addition to showing
that the two proof frameworks have the same expressive power, the
embedding allows for the recovery of the benefits of locality for
2-systems, analyticity results for a large class of such systems, and a
rewriting of hypersequent rules as natural deduction rules.
There are many proof theoretic formalisms to define reasoning tools for logics.
This paper, addressed to proof theorists, investigates two such
formalisms: hypersequents and a subclass of systems of rules called 2-systems. We show that the
two formalisms have the same expressive power (= they can capture the same logics), and derivations
in one formalism can be effectively trasformed into derivations in the other formalism.
In the context of the project the result is useful to understand which Hilbert axioms
(that are typically used to introduce/describe logics) can be captured using
hypersequents; moreover it sheds light on how to generalize the hypersequent framework.
2017
E. Freschi The ``frame'' status of Veda-originated knowledge in Mīmāṃsā
In: Alice Crisanti, Cinzia Pieruccini, Chiara Policardi, and Paola M. Rossi (eds.) Anantaratnaprabhava. Studi in onore di Giuliano Boccali. Università degli
Studi di Milano-Dipartimento di Studi letterari, filologici e linguistici, Ledizioni, Milano (2017), volume 2, pp.9--20.
An issue that is silently present in all of our theoretical enquires, namely the boundaries of
knowledge, was also bravely faced by Mīmāṃsā authors. According to them,
the boundaries of human possibilities of knowledge are the limits of what can be experienced –
the "is". But there is no human faculty that can know what must be done – the "ought". At this
point only the Veda can step in. From this standpoint, we can compare the role of the Veda to
that of any other a priori premise in European philosophy, such as Kant’s categories, Hegel’s
threefold movement of the spirit, Malebranche’s God, etc.
This paper is adddressed to historians of (Indian) philosophy and explains the role of cognitions originated through the sacred texts (Vedas) for the Mīmāṃsā school. The Vedas, according to Mīmāṃsā, contain prescriptions and prohibitions and are the only source about what human beings need to do (as opposed to what there is). They are, therefore, the only valid source of knowledge regarding deontic notions, whereas notions relating to states of affairs can be gained through sense perception, inference and the other instruments of knowledge. The article also discusses the scope of "true" in the case of deontic notions and compares the role of sacred texts for Mīmāṃsā authors to the role of sacred texts for Augustinus, since the latter also stated that sacred texts are a valid source only as for specific topics, not accessible to sense-perception etc.
A. Ciabattoni, E. Freschi, F. Genco and B. Lellmann Understanding Prescriptive Texts: Rules and Logic as elaborated by the Mīmāṃsā school.
Journal of World Philosophies 2(1), pp.47-66 (2017).
The Mīmāṃsā school of Indian philosophy elaborated complex ways of interpreting the prescriptive portions of the Vedic sacred texts.
The present article is the result of the collaboration of a group of scholars of logic, computer science, European philosophy and Indian
philosophy and aims at the individuation and analysis of the deontic system which is applied but never explicitly discussed in Mīmāṃsā texts.
The article outlines the basic distinction between three sorts of principles – hermeneutic, linguistic and deontic. It proposes a mathematical
formalisation of the deontic principles and uses it to discuss a well-known example of seemingly conflicting statements, namely the
prescription to undertake the malefic Śyena sacrifice and the prohibition to perform any harm.
The paper is addressed to historians of (Indian) philosophy. It proposes a first classification of the principles contained in the Mīmāṃsā texts
as hermeneutic, linguistic and deontic. Section 5 describes in a non-technical way the results obtained in the paper (Ciabattoni et al. 2015)
where a logic formalization of some of the deontic principles is used to analyze the
seemingly conflicting statements around the Śyena sacrifice.
M. Pascucci Anderson's restriction of deontic modalities to contingent propositions.
Theoria 83(4), pp.440-470 (2017).
The deontic status of tautologies and contradictions is one of the major puzzles for
authors of early works on deontic logic. It is well-known that von Wright (1951) addresses this
problem by adopting a Principle of Deontic Contingency, which says that tautologies are not
necessarily obligatory and contradictions are not necessarily forbidden. A more radical solution is
proposed by Anderson (1956) within a reductionist approach to deontic logic and consists in
restricting the range of application of deontic modalities to contingent propositions. Anderson’s
solution has not received much attention in the literature, despite reflecting a typical feature of
ordinary deontic reasoning, where non-contingent propositions are rarely, if ever, taken into
account. In the present article we explore some of its formal consequences, providing a taxonomy
of the properties of the Andersonian operators of obligation and permission for contingent propositions,
O' and P', in the class of normal alethic systems.
This article is addressed to logicians. It analyses the relation between alethic and deontic
modal notions (e.g., between necessity and obligation); in particular it investigates the
formal consequences of the idea that all propositions having a relevant deontic status are
contingent. The facts observed can be used, in general, as a philosophical basis for logical
systems in which only formulas having some specified properties are allowed to be in the
scope of a deontic (or modal) operator.
Preliminary results
A. Ciabattoni, E. Freschi, F. Genco and B. Lellmann Mīmāṃsā Deontic Logic: Proof Theory and Applications. Proceedings of TABLEAUX 2015.
Lecture Notes in Computer Science 9323. pp. 323-338. 2015.
Starting with the deontic principles in the Mīmāṃsā texts we introduce a new deontic logic. We use general proof-theoretic methods to
obtain a cut-free sequent calculus for this logic, resulting in decidability, complexity results and neighbourhood semantics. The latter
is used to analyse a well known example of conflicting obligations from the Vedas.
The paper is addressed to logicians. Using some deontic principles (metarules) contained in the Mīmāṃsā texts, it introduces a new deontic
logic which is used to analyze the seemingly conflicting statements around the Śyena sacrifice. In particular, the interpretation of the
mathematical structure validating these statements turns out to coincide with the controversial interpretation of Prābhākara, which can be
reformulated as the lesser of two evils principle.