We report our first results regarding the automated verification of deontic correspondences (broadly conceived) and related matters in Isabelle/HOL, analogous to what has been achieved for the modal logic cube. We report our first results regarding the automated verification of deontic correspondences (broadly conceived) and related matters in Isabelle/HOL, analogous to what has been achieved for the modal logic cube in [1]. To look at Standard Deontic Logic (SDL) and extensions [2, 3] would not be very interesting. First, no new insights would be gained, since SDL is a normal modal logic of type KD. Second SDL is vulnerable to the well-known deontic paradoxes, like in particular Chisholm's paradox of contrary-to-duty obligation (see [3] for details). We focus on the dyadic deontic logics with a preference-based semantics, which originate from the work of Danielsson, Hansson, van Fraassen, Lewis and others. One uses an "intensional" conditional to represent conditional obligation sentences that is weaker than the one obtained using material implication. The semantics generalizes that of SDL, by allowing for grades of ideality. That framework is particularly popular in deontic logic, see the overview chapter in the second volume of the Handbook of Deontic Logic [4]. In that framework, a preference relation ⪰ ranks the possible worlds in terms of comparative goodness or betterness.1 The conditional obligation of ψ, given ϕ (notation: ○(ψ/ϕ)) is evaluated as true if the best ϕ-worlds are all ψ-worlds. Like in modal logic, different properties of the betterness relation yield different systems. So far the correspondence between properties and modal axioms have been established "with pen and paper". This raises the question of how much of this correspondence can be automated. As explained in [1] we believe that "automation facilities could be very useful for the exploration of
the meta-theory of other logics, for example, conditional logics, since the overall methodology is obviously transferable to other logics of interest". Here we follow up on that suggestion, building on results from [5], where the weakest available system (called E) has faithfully been embedded in Higher-Order Logic (HOL). In the present paper we consider extensions of E, already identified with pen and paper. We look at connections or correspondences between axioms and semantic conditions as "extracted" by relevant soundness and completeness theorems. Thus, we take "correspondence" in the same (broad) sense as Hughes and Cresswell, who write: "D, T, K4, KB [are] produced by adding a single axiom to K and [...] in each case the system turns out to be characterized by [sound and complete wrt] the class of models in which [the accessibility relation] R satisfies a certain condition. When such a situation obtains–i.e. when a system K+α is characterized by the class of all models in which R satisfies a certain condition−we shall [...] say [...] that the wff α itself is characterized by that condition, or that the condition corresponds [their italics] to α." [6, p. 41]
The theory file we discuss is available for downloading at http://logikey.org under subrepository "/Deontic-Logics/cube-dll/" (file "cube.thy").
The paper is organized as follows. Section 2 recalls system E and its extensions. Section 3 shows the embedding of E in Isabelle/HOL. Section 4 describes the encoding of the properties of the betterness relation. Section 5 studies the correspondence between the latter properties and the axioms. Section 6 looks at a well-known alternative evaluation rule for the conditional put forth by Lewis [7]. Section 7 concludes.
We describe the semantics and proof theory of system E and its extensions. This one introduces the primitive symbol ○(_/_) for "it is obligatory that ... given that ...", from which symbol P (_/_) for "it is permitted that ... given that ..." is defined. The language also has □ and ♢ .
We start with the main ingredients of the semantics. A preference model is a structure M = (W, ⪰, V ), where W is a non-empty set of possible worlds, ⪰ is a preference relation ranking elements of W in terms of betterness or comparative goodness, and V is a function assigning to each propositional letter a subset of W (intuitively, the subset of those worlds where the propositional letter is true). a ⪰ b may be read "a is at least as good as b". ≻ is the strict counterpart of ⪰, defined by a ≻ b (a is strictly better than b) iff a ⪰ b and b ̸⪰ a. ≈ is the equal goodness relation, defined by a ≈ b (a and b are equally good) iff a ⪰ b and b ⪰ a.
The truth conditions for modal and deontic formulas read: • M, a ⊨ □ϕ iff ∀b ∈ W we have M, b ⊨ ϕ • M, a ⊨ ○(ψ/ϕ) iff ∀b ∈ best(ϕ) we have M, b ⊨ ψ When no confusion can arise, we omit the reference to M and simply write a |= ϕ. Intuitively, ○(ψ/ϕ) is true if the best ϕ-worlds are all ψ-worlds. There is variation among authors regarding the formal definition of “best”. It is sometimes cast in terms of maximality (we call this the max rule) and some other times cast in terms of optimality (we call this the opt rule). An ϕ-world a is maximal if it is not (strictly) worse than any other ϕ-world. It is optimal if it is at least as good as any ϕ-world. The two notions coincide only when "gaps" (incomparabilities) in the ranking are ruled out. Formally: where
Max rule Opt rule best(ϕ) = max(ϕ) best(ϕ) = opt(ϕ) a ∈ max(ϕ) ⇔ a |= ϕ & ¬∃b (b ⊨ ϕ & b ≻ a) a ∈ opt(ϕ) ⇔ a |= ϕ & ∀b (b ⊨ ϕ → a ⪰ b) The relevant properties of ⪰ are (universal quantification over worlds is left implicit): • Reflexivity: a ⪰ a; • Transitivity: if a ⪰ b and b ⪰ c, then a ⪰ c; • Totalness or (strong) connectedness: a ⪰ b or b ⪰ a (or both); • Interval order: ⪰ is reflexive and Ferrers (if a ⪰ b and c ⪰ d, then a ⪰ d or c ⪰ b). The interval order condition makes room for the idea of non-transitive equal goodness relation due to discrimination thresholds. These are cases where a ≈ b and b ≈ c but a ̸≈ c (see [8]).
Lewis’ limit assumption is meant to rule out sets of worlds without a "limit" (viz. a best element). Its exact formulation varies among authors. It exists in (at least) the following four versions, where best ∈ {max, opt}
If ∃x s.t. x |= ϕ then best(ϕ) ̸= ∅ Smoothness (or stopperedness) If x |= ϕ, then: either x ∈ best(ϕ) or ∃y s.t. y ≻ x & y ∈ best(ϕ) (LIM) (SM) A betterness relation ⪰ will be called "opt-limited" or "max-limited" depending on whether (LIM) holds with respect to opt or max. Similarly, it will be called "opt-smooth" or "max-smooth" depending on whether (SM) holds with respect to opt or max. For pointers to literature, and the relationships between these versions of the limit assumption, see [9, 4].
The above semantics may be viewed as a special case of the selection function semantics flavored by Stalnaker and generalized by Chellas [10]. The preference relation is replaced with a selection function f from formulas to subsets of W , such that, for all ϕ, f (ϕ) ⊆ W . Intuitively, f (ϕ) outputs all the best ϕ-worlds. The evaluation rule for the dyadic obligation operator is phrased thus: ○(ψ/ϕ) holds when f (ϕ) ⊆ ‖ψ‖, where ‖ψ‖ is the set of ψ-worlds. It is known that when suitable constraints are put on the selection function, the two semantics (Ext) permits the replacement of necessarily equivalent formulas in the antecedent of deontic conditionals. (Id) is the deontic analogue of the identity principle. (D⋆) rules out the possibility of conflicts between obligations, for a "consistent” context A. (CM) and (DR) correspond to the principle of cautious monotony and disjunctive rationality from the non-monotonic logic literature. (CM) tells us that complying with an obligation does not modify the other obligations arising in the same context. (DR) tells us that if a disjunction of states of affairs triggers an obligation, then at least one disjunct triggers this obligation. Due to Spohn, (Sp) is equivalent with the principle of rational monotony; ○(ψ → ξ/ϕ) is changed into ○(ξ/ϕ). The principle says that realizing a permission does not modify the other obligations arising in the same context.
For more background on these systems, see [4] and the references therein.
Our modelling of System E in Isabelle/HOL reuses and adapts prior work [5] and it instantiates and applies the LogiKEy methodology [14], which supports plurality at different modelling layers.
3Even though smoothness does not play any apparent role in the validation of the axiom, the completeness result is for a class of models satisfying this property.
Classical higher-order logic (HOL) is fixed in the LogiKEy methodology and infrastructure [14] as a universal meta-logic [15] at the base layer (L0), on top of which a plurality of (combinations of) object logics can become encoded (layer L1). In the case of this paper, we encode extensions of System E at layer L1 in order to assess them. Employing these object logics notions of layer L1 we can then articulate a variety of logic-based domain-specific languages, theories and ontologies at the next layer (L2), thus enabling the modelling and automated assessment of different application scenarios (layer L3). Note that the assessment studies conducted in this paper at layer L3 do not require any further knowledge to be provided at layer L2; hence layer L2 modellings do not play a role in this paper.
LogiKEy significantly benefits from the availability of theorem provers for HOL, such as Isabelle/HOL which internally provides powerful automated reasoning tools such Sledgehammer [16, 17] and Nitpick [18]. The automated theorem proving systems integrated via Sledgehammer include higher-order ATP systems, first-order ATP systems, and SMT (satisfiability modulo theories) solvers, and many of these systems in turn use efficient SAT solver technology internally. Indeed, proof automation with Sledgehammer and (counter)model finding with Nitpick were invaluable in supporting our exploratory modeling approach at various levels. These tools were very responsive in automatically proving (Sledgehammer), disproving (Nitpick), or showing consistency by providing a model (Nitpick). In the first case, references to the required axioms and lemmas were returned (which can be seen as a kind of abduction), and in the case of models and counter-models they often proved to be very readable and intuitive. In this section and subsequent ones, we highlight some explicit use cases of Sledgehammer and Nitpick. They have been similarly applied at all levels as mentioned before.
It can be shown that the embedding of E in Isabelle/HOL is faithful [5], in the sense that a formula ϕ in the language of E is valid in the class PREF of all preference models if and only if the HOL translation of ϕ (notation: ⌊ϕ⌋) is valid in the class of Henkin models of HOL.
|=PREF ϕ if and only if |=HOL ⌊ϕ⌋
Remember that the establishment of such a result is our main success criterium at layer L1 in the LogiKEy methodology.
This first two screenshots show the encoding of E in Isabelle/HOL. Fig. 2 shows the basic ingredients in the preferential model, and describes how the propositional and alethic modal connectives are handled. The betterness relation ⪰ is encoded as a binary relational constant r (l. 61). In Fig. 3, the notions of optimality and maximality are encoded. Different pairs of modal operators (obligation, permission) are introduced to distinguish between the two types of truth-conditions.
The model finder nitpick is able to verify the consistency of the formalization (l. 83) and to verify the non-equivalence between the two types of truth-conditions (l. 85). It is also able to show the validity of the axioms of E and the invalidity of the axioms pertaining to the stronger systems under both evaluation rules.
The encoding of the properties of the betterness relation are shown in Fig. 4 and 5. On l. 106-116 of Fig. 4, one sees the different versions of Lewis’ limit assumption. The property in Fig. 5 is the interval order condition. This one is usually described as the combination of totalness with the Ferrers condition as shown on l. 136. Sledgehammer is able to confirm a fact in general overlooked in the literature, that totalness can be replaced by the simpler condition of reflexivity (l. 139-141). More weakenings of transitivity are considered in the theory file. For simplicity’s sake we put them aside.
Here we check known correspondences between modal axioms under the max rule.
First, nitpick is able to confirm that the formula is not valid unless the matching property is assumed. Fig. 6 and 9 show that, when the relevant property is not assumed, a counter-model for D⋆, CM, DR and Sp is found by Nitpick.
In Fig. 7, 8 and 9, it is confirmed that if the property is assumed, then the axiom is validated. Thus, the implications having the form "property ⇒ axiom” are all verified; Fig. 7 shows it for limitedness and smoothness, Fig. 8 for the interval order condition, and Fig. 9 for the combination of transitivity and totalness. But the converse implications are all falsified by Nitpick. We will come back to this point later on.
The outcomes of our experimentation are the same as for the max rule except for one small change. Transitivity no longer needs totalness to validate Sp. This one only needs transitivity. Besides the assumption of transitivity of the betterness relation gives us a principle of transitivity for a weak preference operator over formula, defined by φ ≥ ψ iff P (φ/φ ∨ ψ). This is shown in Fig. 10.
In [1], proper inclusion between systems in the modal cube are verified by looking at the model constraints of their respective axiomatizations. Because of the lack of full equivalence between modal axiom and property of the relation, we cannot do the same, at least not yet. Nor can we show equivalence between systems when restraining the number of worlds.
Variant evaluation rules have been proposed for the conditional in order to handle some of the problems encountered with the usual pattern of evaluation in terms of best. This section takes the example of Lewis [7]’s evaluation rule. In order to avoid commitment to the limit assumption, Lewis suggested that ○(ψ/ϕ) should be true whenever there is no ϕ-world or there is a ϕ ∧ ψ-world which starts a (possibly infinite) sequence of increasingly better ϕ ∧ ψ-worlds. Formally: a ⊨ ○(ψ/ϕ) iff ¬∃b (b |= ϕ) or ∃b (b |= ϕ ∧ ψ & ∀c (c ⪰ b ⇒ c |= ϕ → ψ)) (∃∀) We shall refer to the statement appearing at the right-hand-side of "iff" as the ∃∀ rule. The encoding is shown in Fig.11.
Isabelle/HOL is able to verify in what sense the standard account in terms of best requires the limit assumption. The law “from ♢ ϕ, ○(ψ/ϕ) and ○(¬ψ/ϕ) infer ○(χ/ϕ)" is valid. This is known as the principle of "deontic explosion”. It says that, in the presence of a conflict of duties (unless it is triggered by an "inconsistent" state of affairs) everything becomes obligatory. This has led most authors to make the limitedness assumption in order to validate D*, and hence make the principle of deontic explosion harmless: the set {♢ ϕ, ○(ψ/ϕ), ○(¬ψ/ϕ)} is not satisfiable. This is shown in Fig. 12. On l. 321, the validity of the DEX formula (=principle of deontic explosion) is shown under the max rule. On l. 326, the DEX formula is falsified under the ∃∀ rule.
Isabelle/HOL is also able to verify that when all the standard properties of the betterness relation are assumed, then the three evaluation rules collapse. This is shown in Fig. 13. L.335 shows the equivalence between the ∃∀ rule and the opt rule, and l. 342 shows the equivalence between the ∃∀ rule and the max rule.
In Fig. 14 Sledgehammer shows the validity of the axioms of E holding independently of the properties assumed of the betterness relation.
In Fig. 15 Sledgehammer confirms that the D⋆ axiom and the Sp axiom call for totalness and transitivity, respectively.
Similarly, Fig. 16 shows that COK and CM call for both transitivity and totalness.
To conclude, with regards to correspondence, the situation for conditional (deontic) logic is still slightly different from the one for traditional modal logic. In the latter setting, the full equivalence between the property of the relation and the modal formula is verified by automated means. In the former setting only the direction "property ⇒ axiom" is verified by automated means. To be more precise, what is verified is the fact that, if the property holds, then the axiom holds. What is not confirmed is the converse statement, that if the axiom holds then the property holds. This asymmetry deserves to be discussed.
First, it is usual to distinguish between validity on a frame and validity in a model based on a frame. A frame is a pair ℱ = (W, R), with W a set of worlds and R the accessibility relation. A model based on ℱ = (W, R) is the triplet ℳ = (W, R, V ) obtained by adding a specific valuation V , or a specific assignment of truth-values to propositional letters at worlds. For a formula to be valid on a frame ℱ , it must be valid in all models based on ℱ . In other words, it must be true for every assignment to the propositional letters. We have worked at the level of models. But in so-called correspondence theory (see e.g. [19]) the link between formulas and properties is in general studied at the level of frames themselves. One shows that ℱ meets a given condition iff formula A is valid on ℱ . In a recent extension of the semantical embedding approach for public announcement logic PAL, see [20], an explicit dependency on the concrete evaluation domain has been modeled. It remains future work to study whether this idea can be further extended and adapted to also support a notion of validity for frames as needed here.
Second, the most we got is that a given property is a sufficient condition for the validity of the axiom, but not a necessary one. For instance, to disprove the implication "CM ⇒ m-smoothness" under the max rule (Fig. 7), Nitpick exhibits a model in which CM holds and m-smoothness falsified. The Henkin model is shown in Fig. 17. The corresponding preferential modal is also both the max rule and the opt rule neither reflexivity nor totalness correspond to an axiom. Finally, under the ∃∀ rule the limit assumption has no import.All this has been established with pen and paper. It would be worth exploring the question as to whether and how this problem could be tackled in Isabelle/HOL.
Xavier Parent was funded in whole, or in part, by the Austrian Science Fund (FWF) [M 3240N, ANCoR project]. For the purpose of open access, the author has applied a CC BY public copyright licence to any Author Accepted Manuscript version arising from this submission. We thank the anonymous reviewers for their valuable comments which helped to improve this paper. iovwpWGQPZmYr/uTX+9y87dOgHRz5j2 : ¬' , ¬ψ, χ l<atexish1_b64="0EqUKfnkLNI3BM>ACcVDSFJ2 iG/vLKVXBTugWYzQRf58j3H+qrmPyw3 : ' , ¬ψ, ¬χ l<atexish1_b64="cESD2ZkpM0JdFO7No>ACnIU9
Germany, 2015, pp. 27–41.
[1] C. Benzmüller, M. Claus, N. Sultana, Systematic verification of the modal logic cube in
Isabelle/HOL, in: C. Kaliszyk, A. Paskevich (Eds.), PxTP 2015, volume 186, EPTCS, Berlin, [2] B. Chellas, Modal Logic, Cambridge University Press, Cambridge, 1980. [3] X. Parent, L. van der Torre, Introduction to Deontic Logic and Normative Systems, College [4] X. Parent, Preference semantics for dyadic deontic logic: a survey of results, in: D. Gabbay, J. Horty, X. Parent, R. van der Meyden, L. van der Torre (Eds.), Handbook of Deontic Logic and Normative Systems, volume 2, College Publications, London. UK, 2021, pp. 7–70. [5] C. Benzmüller, A. Farjami, X. Parent, Åqvist’s dyadic deontic logic E in HOL, Journal of Applied Logics – IfCoLoG Journal of Logics and their Applications (Special Issue: Reasoning for Legal AI) 6 (2019) 733–755. [6] G. E. Hughes, M. J. Cresswell, A companion to modal logic, Methuen, London, 1984. [7] D. Lewis, Counterfactuals, Blackwell, Oxford, 1973. [8] R. Luce, Semiorders and a theory of utility discrimination, Econometrica 24 (1956) 178–191. [9] X. Parent, Maximality vs. optimality in dyadic deontic logic, Journal of Philosophical Logic 43 (2014) 1101–1128. 164–177.
(2012) 257–271. [10] B. Chellas, Basic conditional logic, Journal of Philosophical Logic 4 (1975) pp. 133–153. [11] X. Parent, Completeness of Åqvist’s systems E and F, Review of Symbolic Logic 8 (2015) [12] C. Benzmüller, D. Gabbay, V. Genovese, D. Rispoli, Embedding and automating conditional logics in classical higher-order logic, Annals of Mathematics and Artificial Intelligence 66 [13] X. Parent, On some weakened forms of transitivity in the logic of norms, in: L. Giordanni, G. Casini (Eds.), NMR 2022: 20th International Workshop on Non-Monotonic Reasoning, CEUR-WS, 2022, pp. 147–150. Extended abstract. [14] C. Benzmüller, X. Parent, L. van der Torre, Designing normative theories for ethical and legal reasoning: Logikey framework, methodology, and tool support, Artificial Intelligence 287 (2020) 103348. [15] C. Benzmüller, Universal (meta-)logical reasoning: Recent successes, Science of Computer
Programming 172 (2019) 48–62. [16] J. C. Blanchette, S. Böhme, L. C. Paulson, Extending Sledgehammer with SMT solvers,
Journal of Automated Reasoning 51 (2013) 109–128. [17] J. C. Blanchette, C. Kaliszyk, L. C. Paulson, J. Urban, Hammering towards QED, Journal of
Formalized Reasoning 9 (2016) 101–148. [18] J. C. Blanchette, T. Nipkow, Nitpick: A counterexample generator for higher-order logic based on a relational model finder, in: M. Kaufmann, L. C. Paulson (Eds.), ITP 2010, volume 6172 of LNCS, Springer, 2010, pp. 131–146. [19] J. Van Benthem, Correspondence theory, in: D. M. Gabbay, F. Guenthner (Eds.), Handbook of Philosophical Logic, Springer Netherlands, Dordrecht, 2001, pp. 325–408. [20] C. Benzmüller, S. Reiche, Automating public announcement logic with relativized common knowledge as a fragment of HOL in LogiKEy, Journal of Logic and Computation (2022). [21] P. Andrew, An introduction to mathematical logic and type theory, Springer, 2002.