{'fraction_non_alphanumeric': 0.03976514544969309, 'fraction_numerical': 0.008606885508406725, 'mean_word_length': 4.120942944994876, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Note on Nesting in Dyadic Deontic Logic

The paper reports on some results concerning Aqvist's dyadic logic known as system G, which is one of the most influential logics for reasoning with dyadic obligations ("it ought to be the case that ... if it is the case that ..."). Although this logic has been known in the literature for a while, many of its properties still await in-depth consideration. In this short paper we show: that any formula in system G including nested modal operators is equivalent to some formula with no nesting; that the universal modality introduced by Aqvist in the first presentation of the system is definable in terms of the deontic modality.


Introduction
Modern research into the use of deontic logic to represent and reason with normative statements began with the introduction in [10] of what has become known as standard deontic logic (SDL). SDL is based on a propositional language and uses modal operators for obligation and permission where, intuitively, Oϕ means that it ought to be the case (or, it is obligatory) that the formula ϕ be true, and as the dual, Pϕ means it is permitted that the formula ϕ be true.
Dyadic deontic logic (DDL) was introduced in [11] to cater for paradoxes in SDL resulting from so-called contrary-to-duty obligations as described in [3]. In DDL, dyadic modal operators (adapted from the conventions used to express conditional probabilities) enable modal formulae to express the conditions in which obligations and permissions apply so that, for example, O(ϕ|ψ) means that it is obligatory that the formula ϕ be true, provided or given that ψ is true.
The standard semantics used for DDL were introduced by Hansson in [5], who imposes restrictions on the language such that modal operators cannot be nested and mixed formulae (connecting modal and propositional formulae) are not permitted.
In [1],Åqvist proposes system G, a system of dyadic deontic logic which extends Hansson's logic with a universal necessity operator . Intuitively ϕ means that the formula ϕ is necessarily true (and the dual ♦ϕ means the formula ϕ is possibly true). 4 We present an interesting property of System G, namely that every formula with nested O and operators is equivalent to another formula without any nesting. It has already been established that this is the case for S5 logics in [7]. In System G, the operator is an S5 operator and it therefore follows from [7] that nestings of the are superfluous. The O operator however presents additional challenges as the nesting may occur within either argument of the operator. We can still prove that despite this, nestings of the O operator and of combinations of the O and operator are superfluous. These results provide an a posteriori justification to Hansson's original syntactic restrictions.
The rest of the paper is structured as follows. In Section 2 we introduce some preliminaries including the syntax, semantics and proof theory of System G. In Section 3 we show our main result that every System G formula with nested O and operators is equivalent to another formula without any nesting. We do this using both a semantic and a syntactic argument. As part of the proof, we also show that in System G, all -formulae can be expressed using the O modality only. We conclude in In Section 4. Longer proofs of the lemmas and theorems are provided in the appendix.

Some background on nesting deontic operators
The issue of whether deontic logic formalisms should allow operators to be nested within the scope of others has been considered as early as in [6]. Sentences in which deontic operators are nested are sentences like (taken from [6]): -It is obligatory that it is obligatory that everyone keeps his promises.
-It ought to be the case that what ought to be the case is the case.
The issue, from a deontic logic point of view, is whether statements such as the above ones should be objects in a logic or should rather be ignored (on different bases such as being non-meaningful, or trivial or uninteresting).
As pointed out in [4] (quoted in [12]), little attention was initially paid to nested modalities. In [11], von Wright defines the language of both his original and dyadic systems to exclude nesting with no explicit discussion of why this should be the case. Hansson in [5] follows this tradition and also explicitly forbids nesting in his language, commenting however that despite this restriction "almost all philosophical problems discussed in connection with deontic logic are expressible". In [1],Åqvist identifies nesting as one of the differences between Hansson's language and his proposed System G but does not discuss any implications of this difference. Some work has been done on the representation and meaning of nested modalities in some normative systems, such as in so-called stit logics in [2]. However, despite the fact that it is considered a powerful logic for handling contrary-toduty obligations, to the best of our knowledge, no research has been done on nested modalities in System G. In this paper we aim to address this and provide a technical answer to the issue of nesting (within System G).
Results of this type are well-known for normal monadic modal logics (e.g., for S5 [7]). In System G, the operator is an S5 operator and it therefore follows from [7] that nestings of the are superfluous. The O operator however presents additional challenges as the nesting may occur within either argument of the operator. We prove that despite this, nestings of the O operator and of combinations of the O and operator are superfluous.

Language, Syntax and Semantics of System G
Language Formally the language of system G is defined thus Definition 1 (Language of System G). Let P be a set of propositional atoms. The language of system G, L is defined by the following inductive syntax, where p ∈ P and ϕ ∈ L L : Conjunction, material implication and biconditional are defined from negation and disjunction in the expected way. We treat ⊤ as a propositional atom in P, and define ⊥ as ¬⊤. Parentheses may be used to clarify the order of operators.
O(ϕ 1 |ϕ 2 ) is read as 'ϕ 1 is obligatory, given ϕ 2 '. ϕ is read as 'Everywhere ϕ'. It follows that the duals of these operators P('Permitted') and ♦('Somewhere') are defined as follows: Semantics These formulae are evaluated using Kripke-style possible world semantics based on the so-called class of Strong H 3 models defined byÅqvist in [1] as follows: Given a set of propositional atoms P, a Strong H 3 model M is a structure S, , V , where -S is a non-empty set of possible worlds is a reflexive, transitive, fully connected and limited (see below) binary relation over S that satisfies the limit assumption condition described below.
-V is a valuation function V : P → ℘(S) that assigns a truth set to every proposition in P.
The weak preference relation captures the idea that for any two worlds t and s, if t s then s is at least as good as t. The relation is fully connected if and only if any two worlds in S are comparable, or formally that: The limitedness property can be characterised in terms of the opt function, defined as follows.

Definition 3 (opt function).
opt(X) = {x ∈ X | ∀y ∈ X : y x} (2) Intuitively, opt(X) are the elements of X that are at least as good as any other element in X. We say that opt(X) is the optimal set or the set of optimal elements of X.
The preference relation is then limited if and only if for every non-empty subset of S there is at least one optimal element, or formally: Definition 4 (Truth at a point). The notion of a formula ϕ ∈ L being true at a world s in a model M = S, , V , denoted M, s |= ϕ, is defined inductively as follows: ( ϕ denotes the truth set of ϕ, i.e. the set of worlds in which ϕ is true.) The truth definitions for P (the dual of O) and ♦(the dual of ), derived from (8) and (9) are as follows: We say that a formula ϕ is valid in Strong H 3 models if it is true in all worlds of all Strong H 3 models, and denote this |= H3 ϕ. (We sometimes drop the subscript if the class of models being referred to is clear.) If ϕ is valid with respect to a class of models, we say that ϕ is a validity of that class of models. We say that two formulae ϕ and ψ are semantically equivalent if ϕ ↔ ψ is a validity.

Observation 1
The modalities O and , as well as their duals, are global modalities in the following sense: AxiomaticsÅqvist proposes the following axioms and rules for system G (names are from [8]).

All propositional tautologies (PL)
S5 axioms for (S5) We refer to this axiom system as system G, and so we say that a formula ϕ is derivable in system G if it can be derived using this calculus. We denote this by ⊢ G ϕ. (For readability, we sometimes drop the subscript if the system referred to is clear). If ϕ is derivable in system G, we say that ϕ is a theorem of system G. We say that two formulae ϕ and ψ are provably equivalent if ϕ ↔ ψ is a theorem of System G.
Parent [8] shows that this axiom system is sound and strongly complete with respect to Strong H 3 models.

Nested formulae
In this section we present our main finding that any system G formula which contains nested modal operators is equivalent to some other formula without nesting. We present a semantic and a syntactic argument for this theorem.
Both arguments use the following definitions and lemma.
Definition 5 (Modal depth). The modal depth md(ϕ) of a formula ϕ ∈ L is defined inductively as where max represents the arithmetic maximum, i.e. for any x, y ∈ N, if x ≥ y then max(x, y) = x, otherwise max(x, y) = y.
Definition 6 (Unnested disjunctive normal form (UDNF)). Let L O be the sublanguage of L without formulae containing the -operator. We say that a formula ψ ∈ L O is in Unnested Disjunctive Normal Form (UDNF) if it is a disjunction of conjunctions of the form where n, k ∈ N and all of the formulae α, ϕ m , ψ m (m ≤ n + k) are propositional formulae (⊤ and ⊥ are considered propositional formulae). The formula δ is called a canonical conjunction and the formulae O(ϕ m | ψ m ) are called prenex formulae.
Observe that by the above definition, formulae in UDNF have a maximum modal depth of 1.

Semantic argument
First we state the following proposition which provides a means to obtain for every -formula, a semantically equivalent O-formula.
The following lemma guarantees that an O or ¬O formula within the scope of another can be brought out of that scope.

Lemma 2. LetÔ stand for an arbitrary but fixed
We can now state our main theorem as follows.

Syntactic argument
The syntactic argument has the same structure as the semantic argument with Proposition 1 and Lemma 2 replaced by syntactic counterparts.
The following is a syntactic counterpart to Proposition 1.
The following is a syntactic counterpart to Lemma 2.

Lemma 3. LetÔ stand for an arbitrary but fixed
Theorem 2. Every formula χ is provably equivalent to a formula in UDNF.
Proof. The proof is by induction on χ using the same argument as the proof for Theorem 1 except that Proposition 1 and Lemma 2 are replaced by their syntactic counterparts Proposition 2 and Lemma 3 respectively.

Conclusion
When he introduced restrictions on nesting and in [5],Hansson commented that in SDL, despite these restrictions, "almost all philosophical problems discussed in connection with deontic logic are expressible in his language." He, however, offers no justification for this conjecture and, in moving from SDL to the dyadic language, a formal definition of the dyadic language used in not given, and it is not explicit whether these restrictions are to be kept. It is generally considered that it was his intention that the dyadic language be so restricted, and this is stated explicitly, for example, in [9]. We note also that the list of example valid and invalid formulae given in [5] contain no nested formulae. From a technical point of view, it seems unnatural to forbid certain operators to appear in the scope of others. The main goal of our work has been to see whether such a restriction is necessary, and whether it actually limits the ability of the system to express deontic concepts. We have demonstrated that the answer to both questions is negative: forbidding nested modalities is not technically needed, and, on the other hand, not allowing them does not restrict the expressive power of the language either. This in some sense settles Hansson's conjecture, at least with respect to system G: if any interesting problems can be expressed in the full dyadic language, they also can in a restricted version where nesting is not permitted. Therefore, as ⊥ = ∅, opt( ¬ϕ ) = ∅. Therefore, given the limit assumption (3), ¬ϕ = ∅. Therefore ∀(t ∈ S)M, t |= ϕ. Therefore, by the truth definition of (9), M, s |= ϕ.

C Proof of Theorem 1
Proof. The theorem can be proved by induction on the syntax of χ (Definition 1). There are 5 cases to consider.
1. For the base case, if χ is a propositional atom, then by definition it is in UDNF. 2. If χ = ¬χ 1 then we show that if χ 1 has an equivalent formula in UDNF, so does χ. Suppose χ 1 = δ 1 ∨ · · · ∨ δ z for some z ≥ 1. By Definition 6 this is in UDNF. Then ¬χ 1 = ¬δ 1 ∧ · · · ∧ ¬δ z , where each ¬δ i is of the form The result then follows by applying the distributive law: 3. If χ = χ 1 ∨ χ 2 then we show that if χ 1 and χ 2 have an equivalent formula in UDNF, so does χ. Suppose χ 1 ↔ χ ′ 1 and χ 2 ↔ χ ′ 2 where χ ′ 1 and χ ′ 2 are in UDNF (i.e. disjunctions of canonical conjunctions). Then χ = χ ′ 1 ∨ χ ′ 2 which is also a disjunction of canonical conjunctions and thus in UDNF. 4. If χ = O(χ 1 |χ 2 ) then we show that if χ 1 and χ 2 have an equivalent formula in UDNF, so does χ. In the case where both χ 1 and χ 2 are propositional formulae, χ is already in UDNF. If χ 1 contains a prenex formula, we can, using Lemma 1, assume that χ 1 = π ∨ (λ ∧Ô) or χ 1 = π ∨ (λ ∧ ¬Ô) for some prenex formulaÔ. In the first case, item 15 of Lemma 2 tells us how to remove the prenex outside the scope of the outer O, in the second case we need item 16 to do this. Likewise, if χ 2 contains a prenex, we can write χ 2 either as π ∨ (λ ∧Ô), or else as π ∨ (λ ∧ ¬Ô). In the first case, we use item 14 of Lemma 2 to move the prenex outside the scope of O, and otherwise we use item 13. We can repeat this process of removing a prenex from within the scope of O until none are left, and finally, use the distributive law above to bring the result in normal form. 5. If χ = χ 1 then we show that if χ 1 has an equivalent formula in UDNF, so does χ. By Proposition 1 χ 1 is equivalent to O(⊥|¬χ 1 ). An equivalent formula can be obtained by applying cases 1 to 4 above to this formula.

D Proof of Proposition 2
Proof. First we note the following rules of inference that are known to be sound in propositional logic namely the rules of hypothetical syllogism (HS), biconditional introduction (BI), subconditional elimination (SCE), contraposition(Contra) and substitution of provable equivalences (Subst).