Streamlining Input/Output Logics with Sequent Calculi (Extended Abstract)

1 Introduction

Input/Output (I/O) logic is a general framework proposed by [Makinson and van der Torre, 2000] to reason about conditional norms. I/O logic is not a single logic but rather a family of logics, each viewed as a "transformation engine", which converts an input (condition under which the obligation holds) into an output (what is obligatory under these conditions). Many different I/O logics have been defined, e.g., [Makinson and van der Torre, 2001; van der Torre and Parent, 2013; Parent and van der Torre, 2014; Stolpe, 2015], and also used as building blocks for causal reasoning [Bochman, 2003; Bochman, 2004; Bochman and Lifschitz, 2015; Bochman, 2021], laying down the logical foun[McCain and Turner, 1997],

and for legal reasoning [Ciabattoni et al., 2021]. I/O logics manipulate Input-Output pairs (A,B), which consist of boolean formulae representing either conditional obligations (for the original I/O logics) or causal relations (A causes B, for their causal counterparts). Different I/O logics are defined by varying the mechanisms of obtaining new pairs from a set of pairs (entailment problem). The semantics of the original I/O logics is procedural, while their causal counterparts adopt bimodels, which are pairs of arbitrary deductively closed sets of formulae. Each I/O logic possesses a proof calculus, consisting of axioms and rules but not suitable for proof search.

This paper deals with the four original I/O logics OUT1OUT4 in [Makinson and van der Torre, 2000] and their causal counterpart OUT⊥1 -OUT⊥4 in [Bochman, 2004]. We introduce proof-search-oriented sequent calculi and use them to bring together scattered results and to provide uniform solutions to various unresolved problems. Indeed [van Berkel and Straßer, 2022] characterized many I/O logics through an argumentative approach using sequent-style calculi. Their calculi are not proof search-oriented. First sequent calculi of this kind for some I/O logics, including OUT1 and OUT3, have been proposed in [Lellmann, 2021]. Their implementation offers an alternative decidability proof, though suboptimal (entailment is shown to be in ΠP3 ), and the problem of finding proof-search-oriented calculi for OUT2 and OUT4 was left open there. A prover for these two logics was introduced in [Benzm¨uller et al., 2019]. The prover encodes in classical Higher Order Logic their embeddings from [Makinson and van der Torre, 2000] into the normal modal logics K and KT. Finding an embedding of OUT1 and OUT3 into normal modal logics was left as an open problem, that [van der Torre and Parent, 2013] indicates as difficult, if possible at all. An encoding of various I/O logics into more complicated logics (adaptive modal logics) is in [Straßer et al., 2016]. Using their procedural semantics, [Steen, 2021] defined goaldirected decision procedures for the original I/O logics, without mentioning the complexity of the task. [Sun and Robaldo, 2017] showed that the entailment problem for OUT1, OUT2, and OUT4 is co-NP-complete, while for OUT3 complexity was found to be between classes co-NP and P NP , though not precisely resolved.

* This is the extended abstract of the paper with the same title [Ciabattoni and Rozplokhas, 2023] presented at KR 2023, where it received the Ray Reiter Best Paper Prize.

In this paper, we follow a new path that streamlines the considered logics (see [Ciabattoni and Rozplokhas, 2023] for all proofs). Inspired by the modal embedding of OUT⊥2 and OUT⊥4 in [Bochman, 2003], we design well-behaving sequent calculi for Bochman's causal I/O logics. The normal form of derivations in these calculi establishes a simple syntactic link between derivability in the original I/O logics and in their causal versions, enabling the use of our calculi for the original I/O logics as well. As a by-product, the following results are achieved uniformly across all four original I/O logics and their causal versions:

• a simple possible worlds semantics
• co-NP-completeness and efficient automated procedures for the entailment problem
• embeddings into the shallow fragment of the modal logics K, KD, and their extension with axiom F.

2 Preliminaries

In the I/O logic framework, conditional norms (or causal relations) are expressed as pairs (B, Y ) of propositional boolean formulae. Different I/O logics are obtained by varying the mechanisms of obtaining new input-output pairs from a given set of these pairs. The mechanisms introduced in the original paper [Makinson and van der Torre, 2000] are based on the following (axioms and) rules (|= denotes semantic entailment in classical propositional logic):

(TOP) (⊤,⊤) is derivable from no premises

(BOT) (⊥,⊥) is derivable from no premises

Different I/O logics are given by different subsets R of these rules, see Fig. 1. The basic system, called simpleminded output OUT1, consists of the rules {(TOP), (WO), (SI), (AND)}. Its extension with (OR) (for reasoning by cases) leads to basic output logic OUT2, with (CT) (for reusability of outputs as inputs in derivations) to simpleminded reusable output logic OUT3, and with both (OR) and (CT) to basic reusable output logic OUT4. Their causal counterpart [Bochman, 2004], that we denote by OUT⊥i for i = 1, . . . , 4, extends the corresponding logics with (BOT).

Definition 1. Given a set of pairs G and a set R of rules, a derivation in an I/O logic of a pair (B, Y ) from G is a tree with (B, Y ) at the root, each non-leaf node derivable from its immediate parents by one of the rules in R, and each leaf node is an element of G or an axiom from R.

G ⊢OUT∗ (B, Y ) indicates that (B, Y ) is derivable in the I/O logic OUT∗ from the set of pairs in G (entailment problem). (B, Y ) is the goal pair, the formulae B and Y are the goal input and goal output respectively, and the pairs in G are called deriving pairs.

3 Sequent Calculi for I/OLogics

We define sequent calculi for all four causal I/O logic in a modular fashion. The characterization of their derivations allows us to establish a syntactic link between causal and original I/O logics, thereby enabling the utilization of these calculi for the original I/O logics as well.

Figure 1: Concluding rules (same for all causal I/O logic)

The basic objects of the calculi for the causal I/O logic are

dealing with pairs, as well as

dealing with boolean formulae (meaning that {A1, . . . ,An} |= (B1 ∨ · · · ∨ Bm)). The calculi are defined by extending Gentzen's sequent calculus LK for classical logic [Gentzen, 1935] with three rules manipulating I/O sequents: two concluding rules (see Fig. 1) that transform the derivation of the goal pair into an LK derivation of either the goal input or the goal output, and one elimination rule - different for each logic - that removes one of the deriving pair while modifying the goal pair (Fig. 2).

Definition 2. A derivation in our calculi is a finite labeled tree whose internal nodes are I/O or LK sequents s.t. the label of each node follows from the labels of its children using the calculus rules. We say that an I/O sequent (A1,X1), . . . , (An,Xn) ⊢ (B, Y ) is derivable if all the leaves of its derivation are LK axioms.

Derivations of I/O sequents consists of two parts. Starting from the bottom, we first encounter rules dealing with pairs (pair elimination and concluding rules) followed by LK rules.

It is easy to see that using (IN) and (OUT) we can derive (TOP) and (BOT); their soundness in the weakest causal I/O logic OUT⊥1 is expressed by the following result

We present below the calculi for each causal I/O logic.

Production Inference OUT⊥1 . The calculus SC ⊥1 for OUT⊥1 is obtained by adding to the core calculus (consisting of LK with the rules (IN) and (OUT)) the pair elimination rule (E1) in Fig. 2.

Notation 1. P(X) will denote the set of all partitions of the set X, i.e., P(X) = {(I, J) | I ∪ J = X, I ∩ J = ∅}

The following lemma provides a useful characterization of derivability in SC ⊥1 of an I/O sequent (A1,X1), . . . , (An,Xn) ⊢ (B, Y ) via the derivability of certain sequents in LK. The intuition behind it is that the characterization considers all possible ways to apply the rule (E1), by partitioning the premises of (A1,X1), . . . , (An,Xn) ⊢ (B, Y ) into two disjoint sets (I of remaining deriving pairs and J of eliminated pairs).

Lemma 2 (Characterization lemma for SC ⊥1 ). (A1,X1), . . . , (An,Xn) ⊢ (B, Y ) is derivable in SC ⊥1 iff for all partitions (I, J) ∈ P({1, . . . , n}), at least one of the following holds:

• B ⇒Ai is derivable in LK for some i ∈ I,
• B ⇒ is derivable in LK,
• {Xj}j∈J ⇒ Y is derivable in LK.

Basic Production Inference OUT⊥2 . The calculus SC ⊥2 for OUT⊥2 is obtained by adding to the core calculus (consisting of LK with the rules (IN) and (OUT )) the pair elimination rule (E2) in Fig. 2.

Notice that if a concluding rule (IN) or (OUT) can be applied to the conclusion of (E2), it can also be applied to its premises. This observation implies that if (A1,X1), . . . , (An,Xn) ⊢ (B, Y ) is derivable in SC ⊥2 there is a derivation in which the concluding rules are applied only when all deriving pairs are eliminated. We use this I/O normal form of derivations in the proof of the following lemma.

Lemma 3 (Characterization lemma for SC ⊥2 ). (A1,X1), . . . , (An,Xn) ⊢ (B, Y ) is derivable in SC ⊥2 iff for all partitions (I, J) ∈ P({1, . . . , n}), either B ⇒ {Ai}i∈I or {Xj}j∈J ⇒ Y is derivable in LK.

Regular Production Inference OUT⊥3 . The calculus SC ⊥3 for OUT⊥3 consists of LK with (IN) and (OUT) extended with the pair elimination rule and (E3) in Fig. 2.

Lemma 4 (Characterization lemma for SC ⊥3 ). (A1,X1), . . . , (An,Xn) ⊢ (B, Y ) is derivable in SC ⊥3 iff for all (I, J) ∈ P({1, . . . , n}), one of the following holds:

• B, {Xj}j∈J ⇒Ai is derivable in LK for some i ∈ I,
• B, {Xj}j∈J ⇒ is derivable in LK,
• {Xj}j∈J ⇒ Y is derivable in LK.

Causal Production Inference OUT⊥4 . The calculus SC ⊥4 consists of LK with the the rules (IN) and (OUT ), extended with the pair elimination rule (E4) in Fig. 2.

Inspired by the normal modal logic embedding of OUT⊥4 in [Bochman, 2003], the shape of the rule (E4) requires to amend the statement of the characterization lemma (w.r.t. Lemma 3).

Lemma 5 (Characterization lemma for SC ⊥4 ). (A1,X1), . . . , (An,Xn) ⊢ (B, Y ) is derivable in SC ⊥4 iff for all (I, J) ∈ P({1, . . . , n}), either B, {Xj}j∈J ⇒ {Ai}i∈I or {Xj}j∈J ⇒ Y is derivable in LK.

Causal I/O Logics vs. Original I/O Logics. We establish the following syntactic correspondence between derivability in original and causal I/O logics.

The above theorem enables us to use the calculi developed for the causal I/O logics also for OUT1 -OUT4.

4 Applications

Our calculi are used to uniformly establish the following results for the eight considered logics: possible worlds semantics, co-NP-completeness and automated deduction methods, and new embeddings into normal modal logics.

4.1 PossibleWorlds Semantics

We design the semantics by looking at the countermodels provided by the characterization lemmas. A contrapositive reading of these lemmas leads indeed to countermodels for non-derivable statements in all considered causal I/O logics. These countermodels consist of (a partition and) several boolean interpretations (two for OUT⊥2 , OUT⊥4 and their causal versions, and (n + 2) for OUT⊥1 , OUT⊥3 and their causal versions) that falsify the LK sequents from the respective lemma statement. A suitable generalization of these countermodels provides alternative semantic characterizations for both the original and the causal I/O logics.

Definition 3. An I/O model is a pair (In, out) where out is the output world, and In is a set of input worlds.

Definition 4. An I/O pair (A, X) is 1-2-valid in an I/O model (In, out) if (∀in ∈ In. in ⊨ A) implies out ⊨ X. An I/O pair (A, X) is 3-4-valid in an I/O model (In, out) if (∀in ∈ In. in ⊨ A) implies (∀w ∈ {out} ∪ In. w ⊨ X).

Proposition 1 (Semantics of I/O models). G ⊢OUTk (B, Y ) (resp. G ⊢OUT⊥k (B, Y )) iff for all I/O models (satisfying the corresponding conditions in Tab. 2) the validity of all pairs in G implies the validity of (B, Y ).

Let us see our semantics at work in the normative context.

Example 1. Consider the normative code, inspired by the EU General Data Protection Regulation, comprising the conditional obligations (⊤, Lawful), (¬Lawful, Erase), and (Lawful, ¬Erase), where Lawful represents lawful data processing and Erase data erasure. Assume that ¬Lawful holds. The question asked in [Benzm¨uller et al., 2019] is whether some unethical obligation (like KillBoss) can be derived in OUT1 and OUT2 due to the potentially contradictory obligations. A countermodel (In, out) to this entailment problem should be s.t. (a) all input worlds satisfy ¬Lawful, (b) out does not satisfy KillBoss and (c) for every conditional obligation (A,X) in the norm base either out satisfies X or there is an input world that does not satisfy A. We take out and In satisfying {¬KillBoss, Lawful, Erase} and ¬Lawful, respectively. Intuitively out is an 'ideal' world as it satisfies all conditional obligations triggered in the given situation (and in which KillBoss does not happen), while In describes a case consistent with the given situation which explains why (Lawful, ¬Erase) is not triggered.

Figure 2: Sequent rules for pair elimination (one for each considered causal I/O logic)

4.2 Complexity and Automated Deduction

An immediate corollary of our results is co-NP-completeness for all of the considered logics. Moreover, we can explicitly reduce the entailment problem in all of them to the (un-)satisfiability of one classical propositional formula of polynomial size, a thoroughly studied problem with a rich variety of efficient tools available. The result is as follows

The result is extended to the original I/O logics via Th. 1.

4.3 Embeddings into Normal Modal Logics

As a corollary of the soundness and completeness of I/O logics w.r.t. I/O models we provide uniform embeddings into normal modal logics.

More precisely we show that G ⊢ (B, Y ) in I/O logics iff a certain sequent consisting of shallow formulae only (meaning that the formulae do not contain nested modalities) is valid in suitable normal modal logics. To do that we establish a correspondence between pairs and shallow formulae.

The I/O models already use the terminology of Kripke semantics that define normal modal logic. To establish a precise link between the two semantics we need only to define the accessibility relation on worlds. We will treat the set of input worlds In as the set of worlds accessible from the output world out. Under this view on input worlds, 1-2-validity (resp. 3-4-validity) of the pair (A,X) is equivalent to the truth of the modal formula □A→X (resp. □A → X ∧ □X) in the world out.

Also, the conditions on the number of input worlds that are used in Prop. 1 to distinguish different I/O logics can be expressed in normal modal logics by standard Hilbert axioms. Specifically, axiom D: □A → ♢A forces Kripke models to have at least one accessible world, while F: ♢A → □A forces them to have at most one accessible world. As shown below, the embedding works for the basic modal logic K extended with D (which results in the well-known standard deontic logic [von Wright, 1951] KD), with F, or both axioms.

Below we abbreviate validity e.g. in the logics K (respectively K + F) with |=K/K+F.

Theorem 2. (B, Y ) is derivable from pairs G in

• OUT1 and OUT2 iff G□1/2 |=K/K+F □B → Y
• OUT3 and OUT4 iff G□3/4 |=K/K+F □B → Y ∧□Y
• OUT⊥1 and OUT⊥2 iff G□1/2 |=KD/KD+F □B → Y
• OUT⊥3 and OUT⊥4 iff G□3/4 |=KD/KD+F □B→Y ∧□Y where G□1/2 = {□Ai →Xi | (Ai,Xi) ∈ G}, and G□3/4 = {□Ai →Xi ∧□Xi | (Ai,Xi) ∈ G}.

5 Conclusions

We have introduced sequent calculi for I/O logics. Our calculi provide a natural syntactic connection between derivability in the four original I/O logic [Makinson and van der Torre, 2000] and in their causal version [Bochman, 2004]. Moreover, the calculi yield natural possible worlds semantics, complexity bounds, embeddings into normal modal logics, as well as efficient deduction methods. It is worth noticing that our methods for the entailment problem offer derivability certificates (i.e., derivations) or counter-models as solutions. The efficient discovery of the latter can be accomplished using SAT solvers, along the line of [Lahav and Zohar, 2014].

Our work encompasses many scattered results and presents uniform solutions to various unresolved problems; among them, it contains first proof-search oriented calculi for OUT⊥2 and OUT⊥4 ; it provides a missing direct formal connection between the semantics of the original and the causal I/O logics; it introduces a uniform embedding into normal modal logics, that also applies to OUT1 and OUT3, despite the absence in these logics of the (OR) rule; moreover, it settles the complexity of the logics OUT3 and OUT⊥3 . The latter logic has been used in [Bochman, 2018] as the base for actual causality and in [Bochman, 2004], together with OUT⊥4 , to characterize strong equivalence of causal theories w.r.t. two different non-monotonic semantics. Furthermore OUT4 has been used in [Ciabattoni et al., 2021] as a base for formalizing Kelsen's theory of norms [Kelsen, 1991]. The automated deduction tools we have provided might be used also in these contexts.

In this paper, we have focused on monotonic I/O logics. However, due to their limitations in addressing different aspects of causal reasoning [Bochman, 2021] and of normative reasoning, several non-monotonic extensions have been introduced. For example [Makinson and van der Torre, 2001; Parent and van der Torre, 2014] have proposed non-monotonic extensions that have also been applied to represent and reason about legal knowledge bases, as demonstrated in the work by Robaldo et al. [Robaldo et al., 2020]. Our new perspective on the monotonic I/O logics contributes to increase their understanding and can provide a solid foundation for exploring non-monotonic extensions.

Acknowledgements

Work partially supported by EU research and innovation programme under grant agreement No 101034440, the WWTF project ICT22-023, and the FWF (Weave) Project I 6372-N.