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.
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.
D. Glavaničová and M. Pascucci A realistic view on normative conflicts. Logic and Logical Philosophy. Forthcoming.
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.
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 Mimamsa. 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.
E. Freschi and A. Ollett. Arthāpatti in Kumārila. In: M. Keating (Ed.): Controversial Reasoning in
Indian Philosophy: Major Texts and Arguments on Arthâpatti. Bloomsbury (forthcoming)
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. Arthāpatti in Prabhākara. In: M. Keating (Ed.): Controversial Reasoning in
Indian Philosophy: Major Texts and Arguments on Arthâpatti. Bloomsbury (forthcoming)
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. Arthāpatti in Śālikanātha. In: M. Keating (Ed.): Controversial Reasoning in
Indian Philosophy: Major Texts and Arguments on Arthâpatti. Bloomsbury (forthcoming)
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.
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.
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
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
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.
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.