Syntax for factual assumptionsPhi ::= a,b,c,... | false | true | neg Phi | Phi and Phi| Phi or Phi | Phi -> Phi | Op(Phi, Phi)
witha,b,c
,... atoms andop
an operator
Syntax for deontic assumptionsa1 and a2 and ... and aN -> b1 or ... or bM
witha1
, ...,aN
,b1
, ...,bM
atoms
Syntax for superiority relationop(phi,psi) | norm:op(phi,psi) | per(op,phi,psi) | norm:per(op,phi,psi)
withop
an operator,norm
an atom, andphi,psi
propositional
Syntax for operator definitionsnorm1 beats norm2
withnorm1
,norm2
atoms
Syntax for operator inclusions(op,type)
withop
the operator you want to define andtype
one ofobl
orfor
Syntax for operator conflictsop1 -> op2
withop1
andop2
operators
Syntax for nontrivial operatorsconfl(op1,op2)
withop1,op2
operators
op
withop
operator
obl(neg eat_with_fingers, true), obl(eat_with_fingers, asparagus), obl(neg asparagus, true)
.(obl,obl)
.confl(obl,obl)
.obl(neg asparagus, true)
or obl(eat_with_fingers, asparagus)
or neg obl(neg eat_with_fingers, asparagus)
.
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)
.(obl,obl), (per,obl)
.confl(obl,obl), confl(obl,per)
.obl(eat_with_fingers, asparagus and grandparents)
.
save_twin_1 and save_twin_2 -> false
.obl(save_twin_1, reachable_twin_1), obl(save_twin_2, reachable_twin_2)
.(obl,obl)
.confl(obl,obl)
.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)
.
help_friend -> murder
.must(neg murder, true), ought(help_friend, true)
(must,obl), (ought,obl), (should,obl)
must -> ought, must -> should, ought -> should
confl(must,must)
ought
must(neg murder, true)
, or ought(neg murder, true)
, or ought(murder,true)
.
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
.
1:obl(neg open_window, heating), 2:obl(open_window,true), 3:obl(heating,true)
1 beats 2, 2 beats 3
(obl,obl)
confl(obl,obl)
obl(heating, open_window and neg heating)
, or obl(neg open_window, open_window and neg heating)
.
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.
for(parking, true), per(parking,permit)
.(for,for), (per,obl)
.confl(for,for), confl(for,per)
.for(parking, true) and for(parking, lazy)
or for(parking, permit)
or for(parking, permit and lazy)
.
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)
.
steal_food -> steal, steal and respect_others_property -> false
.for(steal, true), obl(respect_others_property, true), per(steal_food, starving)
.(for,for), (obl,obl), (per,obl)
.confl(for,for), confl(obl,obl), confl(for,per), confl(obl,per)
.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)
.
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.
sanc(parking, true), viol(parking, true), per_viol(parking, permit), per_sanc(parking, fine_paid)
.(viol,for), (sanc,for), (per_viol,obl), (per_sanc,obl)
.sanc -> viol
.confl(viol,viol), confl(viol,per_viol), confl(sanc,per_sanc)
.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)
.
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.
white_fence -> fence
.viol(fence, true), sanc(fence, true), per_viol(fence, at_the_sea), per_sanc(white_fence, fence)
.(viol,for), (sanc,for), (per_viol,obl), (per_sanc,obl)
.sanc -> viol
.confl(viol,viol), confl(viol,per_viol), confl(sanc,per_sanc)
.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)
.
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.
protect_witness -> lie
.kant:for(lie, true), law:obl(protect_witness, killer_asks)
. kant beats law
or law beats kant
.(for,for), (obl,obl)
confl(obl,obl), confl(for,for), confl(obl,for)
.obl(lie, killer_asks)
or for(lie, killer_asks)
.
protect_witness -> lie, lie and save_yourself -> false
.kant:for(lie, true), law:obl(protect_witness, killer_asks), common_sense:obl(save_yourself, true)
.kant beats law, law beats common_sense, common_sense beats kant
or law beats kant, kant beats common_sense, common_sense beats law
.(for,for), (obl,obl)
confl(obl,obl), confl(for,for), confl(obl,for)
.obl(lie, killer_asks)
or for(lie, killer_asks)
.
chariotmaker -> sudra, sudra and member_higher_caste -> false
.
obl(agnihotra,true), obl(neg agnihotra, neg member_higher_caste), obl(agnihotra, chariotmaker)
.(obl,obl)
.confl(obl,obl)
.obl(agnihotra,sudra)
or obl(neg agnihotra, teacher and sudra)
.
sruti:obl(agnihotra, caste_1 or caste_2 or caste_3), smrti:for(agnihotra, caste_3 or caste_4)
.
sruti beats smrti
.(obl,obl), (for,for)
.confl(obl,obl), confl(obl,for), confl(for,for)
.obl(agnihotra, caste_3)
, for(agnihotra, caste_3)
, or for(agnihotra, caste_4)
.
cover_post and touch_post -> false
.
smrti:obl(cover_post, ritual_X), sruti:obl(touch_post, ritual_X)
.
sruti beats smrti
.(obl,obl)
.confl(obl,obl)
.obl(neg cover_post, ritual_X)
or obl(cover_post or touch_post, ritual_X)
while varying the superiority relation.
obl(help_Smith, mugged_Smith), for(mugged_Smith, true)
.(obl,obl), (for,for)
.confl(obl,obl), confl(obl,for), confl(for,for)
.obl(mugged_Smith, mugged_Smith)
or for(mugged_Smith, mugged_Smith) and obl(help_Smith, mugged_Smith)
.
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".
care_for_mother and join_resistance -> false
.family:obl(care_for_mother, mother_depends_on_you), vengeance:obl(join_resistance, brother_was_killed)
.family beats vengeance
or vengeance beats family
.(obl,obl)
.confl(obl,obl)
.obl(join_resistance, mother_depends_on_you and brother_was_killed)
or obl(neg join_resistance, mother_depends_on_you and brother_was_killed)
.
true -> sacrifice_child_1 or sacrifice_child_2
.for(sacrifice_child_1, true), for(sacrifice_child_2, true)
.(for,for)
.confl(for,for)
.for(sacrifice_child_1, true)
or for(sacrifice_child_1 and sacrifice_child_2, true)
.
obl(assist_neighbours, true), obl(tell_neighbours, assist_neighbours), obl(neg tell_neighbours, neg assist_neighbours)
.(obl,obl)
.confl(obl,obl)
.obl(assist_neighbours, neg assist_neighbours) and obl(neg tell_neighbours, neg assist_neighbours)
or obl(tell_neighbours, true)
.
© 2020 TU Wien, Theory and Logic Group - Björn Lellmann