## deonticProver2.0

#### Examples

Syntax for formulae
``````Phi ::= a,b,c,... | false | true | neg Phi | Phi and Phi| Phi or Phi | Phi -> Phi | Op(Phi, Phi)
``` with `a,b,c`,... atoms and `op` an operator```
Syntax for factual assumptions
``````a1 and a2 and ... and aN -> b1 or ... or bM
``` with `a1`, ..., `aN`, `b1`, ..., `bM` atoms```
Syntax for deontic assumptions
``````op(phi,psi) | norm:op(phi,psi) | per(op,phi,psi) | norm:per(op,phi,psi)
``` with `op` an operator, `norm` an atom, and `phi,psi` propositional```
Syntax for superiority relation
``norm1 beats norm2` with `norm1`, `norm2` atoms`
Syntax for operator definitions
````(op,type)` with `op` the operator you want to define and
`type` one of `obl` or `for````
Syntax for operator inclusions
``op1 -> op2` with `op1` and `op2` operators`
Syntax for operator conflicts
``confl(op1,op2)` with `op1,op2` operators`
Syntax for nontrivial operators
``op` with `op` operator`

Main examples from the article.

The asparagus example
Deontic assumptions:
`obl(neg eat_with_fingers, true), obl(eat_with_fingers, asparagus), obl(neg asparagus, true)`.
Operators: `(obl,obl)`.
Operator conflicts: `confl(obl,obl)`.
Possible questions: `obl(neg asparagus, true)` or `obl(eat_with_fingers, asparagus)` or `neg obl(neg eat_with_fingers, asparagus)`.
This example illustrates that more specific deontic assumptions like the obligation to eat with your fingers if asparagus is served override more general conflicting ones like the obligation not to eat with your fingers in general, but not more general nonconflicting ones like the general obligation not to serve asparagus.

The extended asparagus example
Deontic assumptions:
`obl(neg eat_with_fingers, true), obl(eat_with_fingers, asparagus), obl(neg asparagus, true), obl(neg eat_with_fingers, grandparents), per(eat_with_fingers, grandparents and asparagus)`.
Operators: `(obl,obl), (per,obl)`.
Operator conflicts: `confl(obl,obl), confl(obl,per)`.
Possible question: `obl(eat_with_fingers, asparagus and grandparents)`.
This is an extension of the asparagus example above, illustrating that more specific permissions, like the permission to eat asparagus with your fingers at your grandparents', can have the effect of reinstating more general obligations, like the obligation to eat asparagus with your fingers. Removing the permission from the deontic assumptions results in an unresolvable conflict between the obligation to eat asparagus with your fingers and the obligation to not eat with your fingers at your grandparents', hence in the situation where you are served asparagus at your grandparents' neither the obligation to eat with your fingers, nor the one not to do so can be derived.

The Drowning Twins
Factual assumptions:
`save_twin_1 and save_twin_2 -> false`.
Deontic assumptions:
`obl(save_twin_1, reachable_twin_1), obl(save_twin_2, reachable_twin_2)`.
Operators: `(obl,obl)`.
Operator conflicts: `confl(obl,obl)`.
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.

Must-ought-should
Factual assumptions:
`help_friend -> murder`.
Deontic assumptions:
`must(neg murder, true), ought(help_friend, true)`
Operators: `(must,obl), (ought,obl), (should,obl)`
Operator inclusions: `must -> ought, must -> should, ought -> should`
Operator conflicts: `confl(must,must)`
Nontrivial operators: `ought`
Possible questions are `must(neg murder, true)`, or `ought(neg murder, true)`, or `ought(murder,true)`.
This example illustrates inclusions between operators with different properties. While the D axiom `neg (must(p,q) and must(neg p,q))` and the P axiom `neg must(false,q)` are both derivable for the operator `must`, only the P axiom is derivable for the operator `ought`, and neither is derivable for `should`.

The Order Puzzle
Deontic assumptions:
`1:obl(neg open_window, heating), 2:obl(open_window,true), 3:obl(heating,true)`
Superiority relation:
`1 beats 2, 2 beats 3`
Operators: `(obl,obl)`
Operator conflicts: `confl(obl,obl)`
Possible questions are `obl(heating, open_window and neg heating)`, or `obl(neg open_window, open_window and neg heating)`.
This example illustrates that deontic detachment does not hold for the base logic MD. In particular, there is no aggregation of priorities along chains of conditional obligations, which could make the obligation to open the window overrule the one to turn on the heating, hence the latter is derivable. Adding the deontic assumption `obl(neg heating, open_window)` would prevent the derivation of the obligation to turn on the heating given the window is open, but using the specificity mechanism instead of the priorities.

Permissions as exceptions 1
Deontic assumptions:
`for(parking, true), per(parking,permit)`.
Operators: `(for,for), (per,obl)`.
Operator conlicts: `confl(for,for), confl(for,per)`.
Possible questions are `for(parking, true) and for(parking, lazy)` or `for(parking, permit)` or `for(parking, permit and lazy)`.
This example illustrates how permissions can be modelled as exceptions to other operators, in this case to the prohibition operator `for`. We could also add other operators, e.g., an obligation type operator `(obl,obl)` with the additional deontic assumption `obl(neg parking, true)` and have the permission act as exception to this operator as well by adding the operator conflict `confl(obl,per)`.

Permissions as exceptions 2
Factual assumptions:
`steal_food -> steal, steal and respect_others_property -> false`.
Deontic assumptions:
`for(steal, true), obl(respect_others_property, true), per(steal_food, starving)`.
Operators: `(for,for), (obl,obl), (per,obl)`.
Operator conlicts: `confl(for,for), confl(obl,obl), confl(for,per), confl(obl,per)`.
Possible questions are `for(steal_food, true) and obl(neg steal_food, lazy)` or `for(steal_food, starving)` or `obl(neg steal_food, starving)` or `for(steal and neg steal_food, starving)`.
This example extends the previous one and illustrates how permissions can be modelled as exceptions to several other operators, in this case to the prohibition operator `for` and the obligation operator `obl`. While the permission to steal food when you are starving overrules the general prohibition to steal and the general obligation to respect others' property in case one is starving, we can still derive that it is forbidden to steal anything which is not food in case you are starving.

Sanctions and violations
Deontic assumptions:
`sanc(parking, true), viol(parking, true), per_viol(parking, permit), per_sanc(parking, fine_paid)`.
Operators: `(viol,for), (sanc,for), (per_viol,obl), (per_sanc,obl)`.
Operator inclusions: `sanc -> viol`.
Operator conlicts: `confl(viol,viol), confl(viol,per_viol), confl(sanc,per_sanc)`.
Possible questions are `sanc(parking, true) and viol(parking, true) and viol(parking, fine_paid)` or `sanc(parking, fine_paid)` or `sanc(parking, permit)` or `viol(parking, permit)`.
This example illustrates how to model sanctions and violations using two operators `sanc` and `viol`. In particular, permissions-as-exceptions to the violation operator also overrule the sanction operator, but not vice versa. In particular, it is possible to violate the prohibition to park without further sanction in case the fine was paid.

The fence example
Factual assumptions:
`white_fence -> fence`.
Deontic assumptions:
`viol(fence, true), sanc(fence, true), per_viol(fence, at_the_sea), per_sanc(white_fence, fence)`.
Operators: `(viol,for), (sanc,for), (per_viol,obl), (per_sanc,obl)`.
Operator inclusions: `sanc -> viol`.
Operator conlicts: `confl(viol,viol), confl(viol,per_viol), confl(sanc,per_sanc)`.
Possible questions are `viol(white_fence, fence)` or `sanc(white_fence, fence)` or `viol(fence, at_the_sea)` or `sanc(fence,fence)` or `sanc(fence and neg white_fence,fence)`.
This example illustrates how to model certain aspects of contrary-to-duty reasoning using the two operators `viol` for the primary prohibition and `sanc` for the secondary one. The mechanism is as in the previous example in that exceptions to the primary prohibition, like the permission to have a fence at the sea, overrule both the primary and secondary norm, while the contrary-to-duty statement "If there is a fence, it must be a white fence" is modelled as an exception to the secondary norm and hence does not overrule the primary norm. Note that since here we take permissions to be upwards monotone, i.e., of obligation type, we do not have free-choice-permission. In particular, this means that we cannot derive the secondary prohibition `sanc(fence,fence)`, because having a fence does not in all cases violate the secondary norm. However, we can derive `sanc(fence and neg white_fence)`, since having a non-white fence is not covered by the exception.

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 superiority relation, possible relations are given by
` kant beats law` or `law beats kant`.
Operators: `(for,for), (obl,obl)`
Operator conflicts: `confl(obl,obl), confl(for,for), confl(obl,for)`.
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 general Kantian prohibition to lie and the more specific obligation by law to protect the witness in case the killer comes asking.

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 superiority 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`.
Operators: `(for,for), (obl,obl)`
Operator conflicts: `confl(obl,obl), confl(for,for), confl(obl,for)`.
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.

Examples from Mimamsa reasoning.

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) ```.
Operators: `(obl,obl)`.
Operator conflicts: `confl(obl,obl)`.
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.

Hierarchie between sruti and smrti texts 1
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 superiority relation is given by
``` sruti beats smrti ```.
Operators: `(obl,obl), (for,for)`.
Operator conflicts: `confl(obl,obl), confl(obl,for), confl(for,for)`.
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 ```.
Operators: `(obl,obl)`.
Operator conflicts: `confl(obl,obl)`.
Possible questions are `obl(neg cover_post, ritual_X)` or `obl(cover_post or touch_post, 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.

Some standard paradoxa of deontic logic.

The deontic assumptions are given by
``` obl(help_Smith, mugged_Smith), for(mugged_Smith, true) ```.
Operators: `(obl,obl), (for,for)`.
Operator conflicts: `confl(obl,obl), confl(obl,for), confl(for,for)`.
Possible questions: `obl(mugged_Smith, mugged_Smith)` or `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 mugged, and that he should not be mugged in the first place. In Standard Deontic Logic it is possible from the first assumptions to derive that Smith should be mugged. In our setting this would correspond to `obl(mugged_Smith, mugged_Smith)`, which is not derivable. 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 factual assumptions are given by
`care_for_mother and join_resistance -> false`.
The deontic assumptions are given by
`family:obl(care_for_mother, mother_depends_on_you), vengeance:obl(join_resistance, brother_was_killed)`.
Apart from the empty superiority relation, possible relations could be given by `family beats vengeance` or `vengeance beats family`.
Operators: `(obl,obl)`.
Operator conflicts: `confl(obl,obl)`.
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)`.
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.

Sophie's Choice
The factual assumptions are
`true -> sacrifice_child_1 or sacrifice_child_2`.
The deontic assumptions are
`for(sacrifice_child_1, true), for(sacrifice_child_2, true)`.
Operators: `(for,for)`.
Operator conflicts: `confl(for,for)`.
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.

`obl(assist_neighbours, true), obl(tell_neighbours, assist_neighbours), obl(neg tell_neighbours, neg assist_neighbours)`.
Operators: `(obl,obl)`.
Operator conflicts: `confl(obl,obl)`.
Possible questions are `obl(assist_neighbours, neg assist_neighbours) and obl(neg tell_neighbours, neg assist_neighbours)` or `obl(tell_neighbours, true)`.