a1 and a2 and ... and aN -> b1 or ... or bM
with a1, ..., aN, b1, ..., bM atoms
Syntax for deontic assumptions
obl(phi,psi) | pero(phi,psi) | for(phi,psi) | perf(phi,psi) | rec(phi,psi) | norm:obl(phi,psi) | norm:pero(phi,psi) | norm:for(phi,psi) | norm:perf(phi,psi) | norm:rec(phi,psi)
with phi,psi propositional and norm an atom
Syntax for superiority relation
norm1 beats norm2 with norm1, norm2 atoms
Chariot makers and Agnihotra
The factual assumptions are given by
chariotmaker -> sudra, sudra and member_higher_caste -> false
.
The deontic assumptions are given by
obl(agnihotra,true), obl(neg agnihotra, neg member_higher_caste), obl(agnihotra, chariotmaker)
.
Possible questions are obl(agnihotra,sudra) or obl(neg agnihotra, teacher and sudra).
This example illustrates the use of the specificity principle in Mimamsa reasoning: In general one should perform the agnihotra ritual; but in the more specific case where one is not a member of the higher castes one should refrain from doing so; yet in the even more specific case where one is a chariotmaker, one again should perform the ritual.
Ye Yajamahe mantra
There are no factual assumptions.
The deontic assumptions are given by
obl(ye_yamahe,true), for(ye_yamahe,fore_sacrifice)
.
Possible questions are for(ye_yamahe,fore_sacrifice) or obl(ye_yamahe,fore_sacrifice).
The alternative interpretations reinterpret the more specific prohibition, e.g., as an exception to the more general obligation. This changes, e.g., whether for(ye_yamahe,fore_sacrifice) is derivable.
This example illustrates the generation of alternative interpretations. The Mimamsa authors encountered the case of the two seemingly conflicting statements that performing the Ye Yamahe mantra during a particular ritual seemed to be at the same time obligatory and prohibited. Reinterpreting these statements yields a way to resolve the conflict. Ticking the boxes for the reinterpretations in the system yields a comparison in terms of the number of underivable deontic assumptions and the naturalness of the intepretations.
Permission to eat after a certain time
There are not factual assumptions.
The deontic assumptions are given by
for(eat,sacrificeX), obl(eat, sacrificeX and afterTimeT)
.
Possible questions are for(eat, sacrificeX and afterTimeT) and obl(eat, sacrificeX and afterTimeT).
The alternative interpretations reinterpret the more general prohibition, e.g., as a negative obligation.
This example again illustrates the generation of alternative interpretations. The example considered by the Mimamsa authors at first seems to consist of the statements that it is forbidden to eat during a particular sacrifice, and that it is obligatory to eat after a certain moment during the same sacrifice. Ticking the boxes for the reinterpretations yields alternative interpretations of these statements, a number of which have been considered by the Mimamsa authors.
Sodasin in Atiratra sacrifice
There are not factual assumptions.
The deontic assumptions are given by
obl(sodasin, atiratra), for(sodasin, atiratra)
.
Possible questions are obl(sodasin, atiratra) and for(sodasin, atiratra).
In its original form, this is an instance of vikalpa, i.e., neither of the deontic assumptions is derivable. The alternative interpretations change this in different ways.
This example again illustrates the generation of alternative interpretations. The Mimamsa authors encountered the two seemingly conflicting statements that performing the Sodasin during the Atiratra ritual is at the same time obligatory and prohibited. The alternative interpretations provide possible reinterpretations avoiding this conflict.
Hierarchie between sruti and smrti texts 1
There are no factual assumptions.
The deontic assumptions are given by
sruti:obl(agnihotra, caste_1 or caste_2 or caste_3), smrti:for(agnihotra, caste_3 or caste_4)
.
The relation is given by
sruti beats smrti
.
Possible questions are obl(agnihotra, caste_3), for(agnihotra, caste_3), or for(agnihotra, caste_4).
This example illustrates the use of a superiority relation between norms. Without such a relation the reasoning would be skeptical, and the system would be able to derive neither that it is obligatory to perform the Agnihotra ritual given one is a member of the third caste, nor that it is prohibited. With the additional information that Sruti texts (coming directly from the Vedas) have a higher authority than Smrti texts (i.e., commentaries on the Vedas), this tie can be broken.
Hierarchie between sruti and smrti texts 2
The factual assumptions are
cover_post and touch_post -> false
.
The deontic assumptions are:
smrti:obl(cover_post, ritual_X), sruti:obl(touch_post, ritual_X)
.
The superiority relation is given by
sruti beats smrti
.
Possible questions are obl(neg cover_pole, ritual_X) or obl(cover_pole or touch_pole, ritual_X) while varying the superiority relation.
This example again illustrates the use of a superiority relation between norms. Again, without information on whether the obligation to touch a certain post during a particular ritual or the one to cover the post completely with cloth (therefore making it impossible to touch it) takes precedence, the system cannot conclude either. The additional information that one of the obligations comes from the Sruti text, the other one from the Smrti ones, and that Sruti texts overrule Smrti texts breaks the tie.
Studienförderungsgesetz
The factual assumptions are given by
has_child and between_30_and_35 -> exception, exception and less_than_30 -> false, between_30_and_35 and less_than_30 -> false, over_35 and between_30_and_35 -> false, over_35 and less_than_30 -> false
.
The deontic assumptions are given by
obl(eligible_for_support, conditions and less_than_30), obl(neg eligible_for_support, neg less_than_30), obl(neg eligible_for_support, neg conditions), obl(eligible_for_support, conditions and exception)
.
Possible questions are obl(eligible_for_support, conditions and less_than_30 and has_child) or obl(neg eligible_for_support, conditions and over_35 and has_child) or obl(eligible_for_support, conditions and between_30_and_35 and has_child and has_own_business).
This example gives a formalisation of some clauses of Paragraph 6 of the Studienbeihilfegesetz, the Austrian law for granting financial support to university students. This illustrates how the prover can be used for legal reasoning.
The Kantian Witness Protection Agent
The factual assumptions are given by
protect_witness -> lie
.
The deontic assumptions are given by
kant:for(lie, true), law:obl(protect_witness, killer_asks)
.
Apart from the empty relation, possible relations are given by
kant beats law
or
law beats kant
.
Possible questions are obl(lie, killer_asks) or for(lie, killer_asks).
This example illustrates how the superiority relation can decide conflicts between norms from different sources. The setting is that a witness protection agent adhering to Kantian philosophy is asked by a killer about the location of the witness, and is torn between the Kantian prohibition to lie and the obligation by law to protect the witness.
The Self-preserving Kantian Witness Protection Agent
The factual assumptions are given by
protect_witness -> lie, lie and save_yourself -> false
.
The deontic assumptions are given by
kant:for(lie, true), law:obl(protect_witness, killer_asks), common_sense:obl(save_yourself, true)
.
Apart from the empty relation, possible relations are given by
kant beats law, law beats common_sense, common_sense beats kant
or
law beats kant, kant beats common_sense, common_sense beats law
.
Possible questions again are obl(lie, killer_asks) or for(lie, killer_asks).
This example extends the previous one with a third obligation rooted in common sense. The additional assumption is that the killer would notice that the agent is lying and kill both the witness and the agent. The superiority relation could have many different forms, the two suggested ones are interesting in that they show that the relation may contain cycles of length three.
Good Samaritan Paradox
The deontic assumptions are given by
obl(help_Smith, mugged_Smith), for(mugged_Smith, true)
.
There are no factural assumptions.
In SDL we have the paradox that we can derive that it is obligatory that Smith be mugged. In our setting this would correspond to obl(mugged_Smith, mugged_Smith), which is not derivable.
However, we can derive for(mugged_Smith, mugged_Smith) and obl(help_Smith, mugged_Smith).
This is the standard Good Samaritan Paradox, where the assumptions are that one should help Smith in case he is robbed, and that he should not be robbed in the first place. In Standard Deontic Logic it is possible from the first assumptions to derive that Smith should be mugged. The fact that this is not derivable here stems from the logic using a dyadic operator to implement obligations, which avoid the inference from "help Smith who is mugged" to "Smith is mugged".
Sartre's dilemma
The deontic assumptions are given by family:obl(care_for_mother, mother_depends_on_you), vengeance:obl(join_resistance, brother_was_killed).
The factual assumptions are given by care_for_mother and join_resistance -> false.
Possible questions are obl(join_resistance, mother_depends_on_you and brother_was_killed) or obl(neg join_resistance, mother_depends_on_you and brother_was_killed). Possible superiority relations could be given by family beats vengeance or vengeance beats family.
This is the standard Sartre's dilemma, where a young French person is torn between the obligations to care for his mother who depends on him and to join the resistance agains the occupying Nazi force in order to avenge the death of his brother. The tie between the two obligations can be broken by labelling one of the sources of the two obligations superior to the other one.
The Drowning Twins
The deontic assumptions are obl(save_twin_1, reachable_twin_1), obl(save_twin_2, reachable_twin_2).
The factual assumptions are save_twin_1 and save_twin_2 -> false.
Possible questions are obl(save_twin_1, reachable_twin_1 and reachable_twin_2) or obl(save_twin_1 or save_twin_2, reachable_twin_1 and reachable_twin_2).
This is the standard Drowning Twins example, where two identical twins are both drowning in a pool, and it is not possible to reach both of them in time to save them. The example illustrate that that the system satisfies the disjunctive solution: While it is not possible to decide which of the twins to save, it is at least derivable that one should save the first or the second.
Sophie's Choice
The deontic assumptions are for(sacrifice_child_1, true), for(sacrifice_child_2, true)
The factual assumptions are true -> sacrifice_child_1 or sacrifice_child_2
Possible questions are for(sacrifice_child_1, true) or for(sacrifice_child_1 and sacrifice_child_2, true).
This is the standard analog of the Drowning Twins example in terms of prohibitions: Sophie and her two children are at a concentration camp, and Sophie has to decide which of the two children to sacrifice in order to save the other one. Similarly to the previous example, while the system does not decide which child to sacrifice, it derives that Sophie should not sacrifice both of them.
Chisholm's paradox
The deontic assumptions are obl(assist_neighbours, true), obl(tell_neighbours, assist_neighbours), obl(neg tell_neighbours, neg assist_neighbours)
There are no factual assumptions.
Possible questions are obl(assist_neighbours, neg assist_neighbours) and obl(neg tell_neighbours, neg assist_neighbours) or obl(tell_neighbours, true).
This is the standard Chisholm example, where one should go to the assistance of one's neighbours and one should tell them whether one is coming ore not. The counterintuitive inference that one should not help the neighbours if one does not do so, which is possible in Standard Deontic Logic SDL, is avoided mainly due to the use of a dyadic operator for obligations.
where atom is any Prolog atom, e.g., p,q,r,...,kill,syena,harm,...
The usual conventions about binding strength of the connectives apply, i.e.,
and binds stronger than or binds stronger than ->.
Facts are lists of clauses, i.e., lists of formulae of the form atom1 and atom2 and ... -> atomn or atomn+1 or ...
Deontic assumptions are lists of non-nested deontic formulae, i.e., lists of formulae of the form obl(A,B), pero(A,B), for(A,B), perf(A,B) or rec(A,B), where the formulae A and B do not contain the obl, pero, for, perf and rec operators.
To run the prover, input your formula, your factual assumptions, and your deontic assumptions, then and hit 'Prove'. If the formula is derivable, the derivation is displayed automatically. You might need to zoom in a bit for large derivations.
NOTE: In some cases the derivations might become too large for TeX
to handle (if they are more than about 19 feet). In these cases no
pdf output is produced. However, you may still download the latex
source code and manually split the derivation.
The prover implements backwards proof search in a deontic logic with the dyadic non-normal modalities obl(.,.) for obligations, for(.,.) for prohibitions and rec(.,.) for recommendations or weak obligations. The axioms are given by the dyadic version
of non-normal modal logic MD for the obligation operator
obl(.,.), the downwards monotone version of the same logic for the prohibition operator for, an interaction axiom between these two, and the dyadic version of non-normal modal logic MP for the recommendation operator rec. More specifically, the axioms and rules for these operators are the following:
(A -> B) / obl(A,C) -> obl(B,C)
(B -> C) and (C -> B) / obl(A,B) -> obl(A,C)
neg (obl(A,B) and obl(neg A, B))
(B -> A) / for(A,C) -> for(B,C)
(B -> C) and (C -> B) / for(A,B) -> for(A,C)
neg (for(A,B) and for(neg A,B)),
neg(obl(A,B) and for(A,B))
(A -> B) / rec(A,C) -> rec(B,C)
(B -> C) and (C -> B) / rec(A,B) -> rec(A,C)
neg rec(false,A)
The system further implements an extension of
the reading of the specificity principle in the step from
deontic assumptions to provable formulae from the article Resolving
conflicting obligations in Mimamsa: A sequent-based
approach. In particular, the deontic assumptions can include explicit exceptions to obligations and prohibitions in the form of obligation-permissions using the operator pero(.,.) and prohibition-permissions using the operator perf(.,.), respectively.
The calculi are implemented in their rendering in
the framework of linear nested sequents, following the
methods of decomposing sequent rules into linear nested sequent
rules from this paper.
The prover also automatically calculates the set of underivable deontic assumptions, i.e., assumptions which are cancelled out by other assumptions and hence involved in a case of vikalpa. It further suggests a number of other possible reinterpretations of the prohibitions and obligations contained in the deontic assumptions, and calculates their scores in terms of number of instances of underivable deontic assumptions, and naturalness of the interpretation.
The possible reinterpretations of prohibitions and obligations are given by:
Reinterpret for(a,b) as obl(neg a,b)
Reinterpret for(a,b) as obl(a,neg b)
Reinterpret for(a,b) as pero(neg a,b)
Reinterpret obl(a,b) as rec(a,b).
Reinterpret obl(a,b) as perf(a,b).
The possible reinterpretations which should be taken into account are given by ticking the corresponding boxes under "Alternative interpretations".
For further information, contact Björn Lellmann. We thank Carlos Olarte for his help in implementing this site.