Sequent-based logical argumentation

Arieli, Ofer; Straßer, Christian

doi:10.1080/19462166.2014.1002536

Sequent-based logical argumentation

Issue title: Applications of logical approaches to argumentation

Article type: Research Article

Authors: Arieli, Ofer^a; | Straßer, Christian^{b; c}

Affiliations: [a] School of Computer Science, The Academic College of Tel-Aviv, Tel-Aviv, Israel | [b] Department of Philosophy and Moral Sciences, Ghent University, Ghent, Belgium | [c] Institute for Philosophy II, Ruhr University Bochum, Germany

Correspondence: [*] Corresponding author. Email: [email protected]

Note: [] This article was originally published with errors. This version has been corrected. Please see Erratum (http://dx.doi.org/10.1080/19462166.2015.1015836).

Keywords: logical argumentation, structured argumentation, sequent calculi

DOI: 10.1080/19462166.2014.1002536

Journal: Argument & Computation, vol. 6, no. 1, pp. 73-99, 2015

Received 14 May 2014

Accepted 19 December 2014

Published: 2 January 2015

Get PDF

Abstract

We introduce a general approach for representing and reasoning with argumentation-based systems. In our framework arguments are represented by Gentzen-style sequents, attacks (conflicts) between arguments are represented by sequent elimination rules, and deductions are made according to Dung-style skeptical or credulous semantics. This framework accommodates different languages and logics in which arguments may be represented, allows for a flexible and simple way of expressing and identifying arguments, supports a variety of attack relations (including those that reflect relevance or quantitative considerations), and is faithful to standard methods of drawing conclusions by argumentation frameworks. Altogether, we show that argumentation theory may benefit from incorporating proof theoretical techniques and that different non-classical formalisms may be used for backing up intended argumentation semantics.

1.Introduction

Argumentation is the study of how jointly acceptable conclusions can be reached from a collection of arguments. In recent years, logic-based approaches for analysing and evaluating arguments, sometimes called logical (or deductive) argumentation, have been largely studied, yielding a variety of formal methods for argumentation-based reasoning (see, for instance, the reviews in Chesñevar, Maguitman, and Loui, 2000; Prakken and Vreeswijk, 2002). The goal of this paper is to provide an abstract, proof theoretical investigation of logical argumentation. Our starting point is that an argument is a pair of a finite set of formulas (Γ, the support set) and a formula (ψ, the conclusion), expressed in an arbitrary propositional language, such that the latter follows, according to some underlying logic, from the former. This abstract approach gives rise to Gerhard Gentzen's well-known notion of a sequent (Gentzen, 1934), extensively used in the context of proof theory. Accordingly, an argument is associated with a sequent of the form Γ⇒ψ and logical argumentation boils down to the exposition of formalised methods for reasoning with these syntactical objects.

This paper is a revised and extended version of Arieli (2013), where a sequent-based approach to logical argumentation is realised in the following two aspects:

Arguments as sequents.
We show that sequents are useful for representing logical arguments since they can be regarded as specific kinds of judgments. This has the obvious benefit that proof theoretical approaches may be used in the context of argumentation theory. For instance, well-studied sequent calculi may be incorporated for producing arguments in an automated way. Moreover, some restrictions in previous definitions of logical arguments, like minimality and consistency of support sets (see, e.g. Besnard & Hunter, 2001, 2009), may now be lifted, allowing for a more flexible way of expressing arguments, which also simplifies their identification.
Attacks as sequent elimination rules.
We show that interactions between arguments (expressed by attack relations) can by represented in terms of Gentzen-style rules of inference. This induces a general and uniform approach not only for introducing arguments, but also for eliminating them. Furthermore, in addition to known attack relations that are ‘imported’ to our framework (which are discussed in Arieli, 2013), we also introduce new types of attack relations, like attacks incorporating different kinds of modal operators, quantitative measurements, and attacks that are based on relevance considerations, implementing the well-known principle of variable sharing from relevance logics (Dunn and Restall, 2002) and applying it for argumentation reasoning.

Keeping our sequent-based setting generic and modular allows us to accommodate different types of languages and logics, including non-classical ones. This enables the use of different substructural logics, including paraconsistent logics (da Costa, 1974) that support robust methods of handling conflicts among arguments, and deontic logics (Aqvist, 2002) that incorporate modalities for modelling normative reasoning and handling problematic cases in which there are conflicts among norms.

The rest of this paper is organised as follows: in the next section we review some basic notions behind logical argumentation and introduce some related notations. Then, in Sections 3 and 4 we re-examine these notions and suggest some proof theoretical substitutes. This allows us to introduce, in Section 5, the notion of sequent-based logical argumentation frameworks, admitting different languages, logics, and inducing a family of entailment relations. The latter can be used for simulating existing entailments of logical argumentation and for introducing new ones. In Section 5 we illustrate reasoning with these entailments in different contexts and consider (also in the Appendix of the paper) some of their basic properties. Finally, in Section 6 we refer to some related work and in Section 7 we conclude.

2.Logical argumentation

Logical argumentation (sometimes called deductive argumentation) is a logic-based approach for formalising argumentation, disagreements, and entailment relations for drawing conclusions from argumentation-based settings (see, e.g. Besnard and Hunter, 2001; Pollock, 1992; Prakken, 1996; Simari & Loui, 1992). In logical argumentation arguments are expressed in terms of formal languages and acceptance of arguments is determined by logical entailments. A wealth of research has been conducted on formalising this kind of argumentation. Below we sketch some of the main notions behind logical argumentation, concentrating on one of the better-known approaches in this context, introduced by Besnard & Hunter (2001).

Definition 2.1

Definition 2.1Dung, 1995

An argumentation framework is a pair AF=⟨Args,A⟩, where Args is an enumerable set of elements, called arguments, and A is a relation on Args×Args whose instances are called attacks.

Definition 2.2

Definition 2.2Besnard & Hunter, 2001, 2009

Let L be a standard propositional language, S an enumerable set of formulas in L, and⊢cl the consequence relation of classical logic (for L). An argument in the sense of Besnard and Hunter (BH-argument, for short), formed by S, is a pair A=⟨Γ,ψ⟩, where ψ is a formula in L and Γ is a minimally consistent subset of S (where minimisation is with respect to set inclusion), such that Γ⊢clψ. Here, Γ is called the support set of the argument A and ψ is its consequent.

Different attack relations have been considered in the literature for logical argumentation frameworks (see, e.g. Amgoud and Besnard, 2009, 2010; Besnard & Hunter, 2001; Gorogiannis & Hunter, 2011; Pollock, 1987, 1992). Below we recall some of the better-known ones.

Definition 2.3

Let A1=⟨Γ1,ψ1⟩ and A2=⟨Γ2,ψ2⟩ be two BH-arguments.

A1 is a defeater of A2 if ψ1⊢cl¬⋀γ∈Γ2γ.
A1 is a direct defeater of A2 if there is γ∈Γ2 such that ψ1⊢cl¬γ.
A1 is an undercut of A2 if there is Γ2′⊆Γ2 such that ψ1⊢cl¬⋀γ∈Γ2′γ and ¬⋀γ∈Γ2′γ⊢clψ1.
A1 is a direct undercut of A2 if there is γ∈Γ2 s.t. ψ1⊢cl¬γ and ¬γ⊢clψ1.
A1 is a canonical undercut of A2 if ψ1⊢cl¬⋀γ∈Γ2γ and ¬⋀γ∈Γ2γ⊢clψ1.
A1 is a rebuttal of A2 if ψ1⊢cl¬ψ2 and ¬ψ2⊢clψ1.
A1 is a defeating rebuttal of A2 if ψ1⊢cl¬ψ2.

Example 2.4

Let S={p,¬p,q}. Then ⟨{¬p},¬p⟩ is an BH-argument (formed by S) which is a (direct) defeater and a (direct and canonical) undercut of the BH-argument ⟨{p},p∨q⟩. Note, further, that while q follows according to classical logic from {p,¬p}, the pair ⟨{p,¬p},q⟩ is not a BH-argument, since its support set is not classically consistent.

Definition 2.5

Let ArgsBH(S) be the (countably infinite) set of BH-arguments formed by S, and let A be a binary relation on ArgsBH(S), obtained by at least one of the conditions described in Definition 2.3. Then the pair AF(S)=⟨ArgsBH(S),A⟩ forms a (logical) argumentation framework.

3.Arguments as sequents

In the following sections we re-examine some of the basic concepts behind logical argumentation. First, in this section, we consider the notion of a logical argument. We argue that the minimality and consistency requirements in Definition 2.2 not only cause complications in the evaluation and the construction of arguments, but also may not be really necessary for capturing the intended meaning of this notion.

Minimality. Minimisation of supports is not an essential principle for defining arguments, thus there is no real reason to overload arguments with this condition. In mathematics, for instance, proofs are usually not required to be minimal in order to validate their claim, and in some other disciplines like law, medicine, and rhetoric, it is a common habit to have overlapping supports for backing up a particular conclusion. To see a more concrete example, consider a framework in which supports are expressed only by literals (atomic formulas or their negation). Then arguments like A=⟨{p,q},p∨q⟩ are excluded since their supports are not minimal, although one may consider {p,q} a stronger support for p∨q than, say, {p}, since the set {p,q} logically implies every minimal support of p∨q. Moreover, the size of {p,q} is bigger than that of {p}, and this may be relevant when quantitative considerations are involved (see Section 4.4).¹1^,²2
Consistency. The requirement that the support set Γ of an argument ⟨Γ,ψ⟩ should be consistent may be irrelevant for some logics, at least when consistency is defined by satisfiability. Indeed, in logics such as Priest's three-valued logic (Priest, 1989) or Belnap's four-valued logic (Belnap, 1977), every set of formulas in the language of {¬,∨,∧} is satisfiable.
Complexity. From a more pragmatic point of view, the involvement of minimally consistent subsets of the underlying knowledge-base poses serious questions on the computational viability of identifying arguments and generating them. Indeed, deciding the existence of a minimal subset of formulas that implies the consequent is already at the second level of the polynomial hierarchy (see Eiter & Gottlob, 1995). For first-order languages the problem is more severe, since arguments may not be generated in an effective way.

Our conclusion, then, is that what really matters for an argument, is that (i) its consequent would logically follow, according to the underlying logic, from the support set, and that (ii) there would be an effective way of constructing and identifying it. In what follows we therefore adhere to the following principles:

(1) Supports and consequents of arguments are solely determined by the logic.
(2) Arguments are syntactical objects that are effectively computable by a formal system that is related to the logic, and are refutable by the attack relation of the argumentation system.

For the first item we indicate what a logic is (Definition 3.1). The first part of the second item corresponds to the primary goal of proof theory, so notations and machinery are borrowed from that area (Definitions 3.2 and 3.3).

We denote by L an arbitrary propositional language having a countably infinite set Atoms(L) of atomic formulas. In what follows T,S (possibly primed or indexed) denote arbitrary theories (sets of formulas) in L, and Γ,Δ (possibly primed or indexed) denote finite theories in L. Given a language L, we fix a corresponding logic (sometimes called the base logic or the core logic), defined as follows.

Definition 3.1

A (propositional) logic for a language L is a pair L=⟨L,⊢⟩, where ⊢ is a (Tarskian) consequence relation for L, that is, a binary relation between sets of formulas and formulas in L, satisfying the following conditions:

Reflexivity: ifψ∈TthenT⊢ψ
Monotonicity: ifT⊢ψandT⊆T′thenT′⊢ψ
Transitivity: ifT⊢ψandT′,ψ⊢ϕthenT,T′⊢ϕ

In the sequel we shall exclude trivial consequence relations, that is, we shall assume that p⊬q for distinct atoms p and q.

In what follows we assume that L contains the following connectives:

A unary connective ¬ which is a ⊢-negation: for every atomic formula p of L it holds that p⊬¬p and ¬p⊬p,
A binary connective ∧ which is a ⊢-conjunction: for every set T of formulas and formulas ψ,ϕ it holds that T⊢ψ∧ϕ iff T⊢ψ and T⊢ϕ.

Also, when L has an implication connective ⊃, we shall assume that it is deductive with respect to the base consequence relation:³3

A binary connective ⊃ is called a ⊢-deductive implication if for every set T of formulas and formulas ψ,ϕ it holds that T,ψ⊢ϕ iff T⊢ψ⊃ϕ.

We shall denote by ⋀Γ the conjunction of all the formulas in (the finite theory) Γ, and abbreviate the formula (ψ⊃ϕ)∧(ϕ⊃ψ) by ψ↔ϕ.

Definition 3.2

Let L be a propositional language, and let ⇒ be a symbol that does not appear in L. An L-sequent (or just a sequent) is an expression of the form Γ⇒Δ, where Γ and Δ are finite sets of formulas in L.

Proof systems that operate on sequents are called sequent calculi (Gentzen, 1934). A crucial property shared by all the logics considered in this paper is that they have a sound and complete sequent calculus. For such a logic L=⟨L,⊢⟩, then, there is an effective way of drawing entailments: T⊢ψ iff for some finite subset Γ⊆T there is a proof of the sequent Γ⇒ψ in the corresponding sequent calculus.

Definition 3.3

Let L=⟨L,⊢⟩ be a logic with a corresponding sequent calculus C, and let S be a set of formulas in L. An L-argument based on S is an L-sequent of the form Γ⇒ψ, where Γ⊆S,⁴4 that is provable in C.⁵5 We denote by ArgL(S) the set of all the L-arguments that are based on S.

In the notation of Definition 3.3, we have that:

Proposition 3.4

Let L=⟨L,⊢⟩ be a propositional logic. Then Γ⇒ψ is in ArgL(S) iff Γ⊢ψ for a finite Γ⊆S.

Example 3.5

Consider Gentzen's sequent calculus LK (Figure 1), which is sound and complete for classical logic CL. In this case we have, for instance, that the sequent ψ⊃ϕ⇒¬ψ∨ϕ is derivable in LK and so it belongs to ArgCL(S) whenever S contains the formula ψ⊃ϕ. Note, however, that this sequent is not derivable by any sequent calculus that is sound and complete for intuitionistic logic IL (e.g. Gentzen's LJ), thus it is not in ArgIL(S) for any S.

Figure 1.

The proof system LK.

Proposition 3.6

For every logic L=⟨L,⊢⟩ and a set S of formulas in L, the set ArgL(S) is closed under the following rules:⁶6

S-Reflexivity: For every finite Γ⊆S and ψ∈Γ it holds that Γ⇒ψ∈ArgL(S)
S-Monotonicity: If Γ⇒ψ∈ArgL(S) and Γ⊆Γ′⊆S, then Γ′⇒ψ∈ArgL(S)
S-Transitivity: If Γ⇒ψ∈ArgL(S) and Γ′,ψ⇒ϕ∈ArgL(S), then also Γ,Γ′⇒ϕ∈ArgL(S)

Proof

By Proposition 3.4, S-Reflexivity (respectively, S-Monotonicity, S-Transitivity) follows from the reflexivity (respectively, the monotonicity, transitivity) of ⊢.

Remark 3.1

The set ArgsBH(S) of the BH-arguments is not closed under any rule in Proposition 3.6. To see this consider for instance the set S={p,q,¬p∨q,¬q∨p}. Then ⟨{p,¬p∨q},q⟩∈ArgsBH(S) and ⟨{q,¬q∨p},p⟩∈ArgsBH(S), however ⟨{p,¬p∨q,¬q∨p},p⟩∉ArgsBH(S), since its support set is not minimal. Thus ArgsBH(S) is not S-transitive. The fact that ⟨{p,¬p∨q,¬q∨p},p⟩∉ArgsBH(S) (while ⟨{p},p⟩∈ArgsBH(S)) also shows thatArgsBH(S) is not S-monotonic and that it is not S-reflexive.⁷7

Remark 3.2

Let L=⟨L,⊢⟩ be a logic and S a set of formulas in L. Then S-Transitivity can be strengthened as follows:

If Γ⇒ψ∈ArgL(S) and Γ′,ψ⊢ϕ for a finite Γ′⊆S, then Γ,Γ′⇒ϕ∈ArgL(S).

Note that unlike S-Transitivity, in the rule above ψ may not belong to S.

4.Attacks as sequent elimination rules

In order to represent attack relations we introduce rules for excluding arguments (i.e. sequents) in the presence of counter arguments. We call such rules sequent elimination rules, or attack rules. The obvious advantage of representing attacks by sequent elimination rules is that the form of such rules is similar to that of the construction rules, and both types of rules are expressed by the same syntactical objects. This allows us to uniformly identify and generate arguments and attacks by the same sequent-manipulation systems.

Typical conditions of attack rules consist of three ingredients: the attacking argument (the first sequent in the rule's prerequisites), the attacked argument (the last sequent in the rule's prerequisites), and the conditions for the attack (the other prerequisites). Conclusions of sequent elimination rules will be the elimination of the attacked argument. In the sequel, we denote by Γ⇏ψ the elimination (or, the discharging) of the argument Γ⇒ψ. Alternatively, if a sequent is denoted by s, its discharged counterpart will sometimes be denoted by s‾.

Definition 4.1

Let ArgL(S) be a set of L-arguments, C a sound and complete sequent calculus for L. A sequent elimination rule (or attack rule) is a Gentzen-type rule R of the following form:

Γ1⇒Δ1,…,Γn⇒ΔnΓn⇏Δn.

We say that R is ArgL(S)-applicable, alternatively: L-applicable or just applicable (with respect to θ), if there is an L-substitution θ such that θ(Γ1)⇒θ(Δ1) and θ(Γn)⇒θ(Δn) are in ArgL(S) and for each 1<i<n, θ(Γi)⇒θ(Δi) is C-provable. In this case we shall say that θ(Γ1)⇒θ(Δ1) R-attacks θ(Γn)⇒θ(Δn).

Note that applicability of a rule is defined with respect to a logic (and a substitution), and it is invariant with respect to a particular calculus C, as long as C is sound and complete for L.

4.1.Standard logical attacks, revisited

First, we show how the attack relations in Definition 2.3 can be described in terms of corresponding sequent elimination rules.

Attacks by defeaters. In terms of an arbitrary logic L=⟨L,⊢⟩ and L-arguments in ArgL(S), an argument Γ1⇒ψ1 is an L-defeater of an argument Γ2⇒ψ2 if ψ1⊢¬⋀Γ2. In the presence of a ⊢-deductive implication ⊃ in L, this means that ⊢ψ1⊃¬⋀Γ2, and so ⇒ψ1⊃¬⋀Γ2 is an L-argument in ArgL(S). It follows that attacks by defeaters may be represented by the following sequent elimination rule (relative to L):

Defeat:Γ1⇒ψ1⇒ψ1⊃¬⋀Γ2Γ2⇒ψ2Γ2⇏ψ2.

In the particular case where the underlying logic is classical logic CL, this rule is a sequent-based encoding of a defeater attack in the sense of Definition 2.3:

Proposition 4.2

Let A1=⟨Υ1,σ1⟩ and A2=⟨Υ2,σ2⟩ be two BH-arguments. Then A1 is a defeater of A2 in the sense of Definition 2.3 iff the rule Defeat defined above is CL-applicable with respect to a substitution θ, where θ(Γi)=Υi and θ(ψi)=σi, i=1,2.

Proof

Since Ai are BH-arguments it holds that Υi⊢clσi for i=1,2 and so the sequents Υi⇒σi are LK-provable (i=1,2). Moreover, since A1 is a defeater of A2, it holds that ⊢clσ1⊃¬⋀Υ2, thus ⇒σ1⊃¬⋀Υ2 is also LK-provable. It follows that the rule Defeat is CL-applicable with respect to a substitution θ such that θ(Γi)=Υi and θ(ψi)=σi (i=1,2). Conversely, let A1=⟨Υ1,σ1⟩ and A2=⟨Υ2,σ2⟩ be BH-arguments and suppose that the rule Defeat is CL-applicable with respect to a substitution θ such that θ(Γi)=Υi and θ(ψi)=σi (i=1,2). Then the attacking condition of this rule is LK-provable, which means that σ1⊢cl¬⋀Υ2, and so A1 is a defeater of A2 in the sense of Definition 2.3.

Remark 4.1

The following sequent elimination rule may be viewed as an equivalent form of Defeat, which moreover does not assume the availability of a deductive implication in the language.

Compact Defeat:Γ1⇒¬⋀Γ2Γ2⇒ψ2Γ2⇏ψ2

Definition 4.3

We say that an attack rule R1 L-implies an attack rule R2, if for every set of formulas S, whenever R2 is ArgL(S)-applicable its conclusion is produced by R1 (with respect to ArgL(S)). Formally: whenever Γ⇒ψ∈ArgL(S) R2-attacks Γ′⇒ψ′∈ArgL(S) there is Γ⇒ϕ∈ArgL(S) that R1-attacks Γ′⇒ψ′.⁸8 The Attack rules R1 and R2 are said to beL-equivalent, if each one of them L-implies the other.

From an argumentative point of view, the fact that a rule R1 implies a rule R2 intuitively means that any attack that is producible using R2 can be reproduced using R1 by means of an attacking argument with the same support set.

Proposition 4.4

For every logic L, Compact Defeat is L-equivalent to Defeat.

Proof

To show that Compact Defeat implies Defeat assume that the three conditions of Defeat hold with respect to ArgL(S). Since ⇒ψ1⊃¬⋀Γ2 is derivable, it holds that ⊢ψ1⊃¬⋀Γ2. Thus, since ⊃ is a ⊢-deductive implication, ψ1⊃¬⋀Γ2. This, together with the assumption that Γ1⇒ψ1 is derivable (and so it is an argument in ArgL(S)), imply by Remark 3.2 that Γ1⇒¬⋀Γ2 is an argument inArgL(S), and so by Definition 3.3 it is derivable in the underlying sequent calculus. It follows that Γ2⇏ψ2 is producible by Compact Defeat, and so Compact Defeat indeed implies Defeat.

To see that Defeat implies Compact Defeat suppose that the two conditions of Compact Defeat hold. Since ⊢ is reflexive, ¬⋀Γ2⊢¬⋀Γ2, and so, since ⊃ is a ⊢-deductive implication, ⊢¬⋀Γ2⊃¬⋀Γ2. We thus have that the sequent ⇒¬⋀Γ2⊃¬⋀Γ2 is derivable in the underlying sequent calculus. It follows that Γ2⇏ψ2 is producible by Defeat, and so Defeat indeed implies Compact Defeat.

Attacks by direct defeaters. Direct defeat with respect to an arbitrary logic L=⟨L,⊢⟩ and a set ArgL(S) ofL-arguments based on S, means that Γ1⇒ψ1 is an L-direct defeater of Γ2⇒ψ2 if ψ1⊢¬γ for some γ∈Γ2. Thus, a direct defeat attack may be expressed by the following sequent elimination rule:

Direct Defeat:Γ1⇒ψ1⇒ψ1⊃¬ϕΓ2,ϕ⇒ψ2Γ2,ϕ⇏ψ2.

It follows that an argument should be withdrawn in case that the negation of an element in its support set is implied by a consequent of another argument.

As in the case of attacks by defeaters, we have the following relation between attacks by direct defeaters in classical logic (Definition 2.3) and the above sequent-based formalisation:

Proposition 4.5

Let A1=⟨Υ1,σ1⟩ and A2=⟨Υ2,σ2⟩ be two BH-arguments. Then A1 is a direct defeater of A2 in the sense of Definition 2.3 iff the rule Direct Defeat defined above is CL-applicable with respect to a substitution θ where θ(Γi)=Υi and θ(ψi)=σi, i=1,2.

Proof

Similar to that of Proposition 4.2.

Remark 4.2

Again, it is possible to express an equivalent and more compact form of the rule above, which does not mention an implication connective:

Compact Direct Defeat:Γ1⇒¬ϕΓ2,ϕ⇒ψ2Γ2,ϕ⇏ψ2.

Proposition 4.6

For every logic L, Compact Direct Defeat is L-equivalent to Direct Defeat.

Proof

Similar to the proof of Proposition 4.4.

Similar links to BH-arguments as in Propositions 4.2 and 4.5 may be established for all the rules to be considered in what follows. Also, all these rules will have equivalent compact versions like those considered in Remarks 4.1 and 4.2. In the sequel, we shall avoid replicating the links to BH-arguments and formulating equivalent compact versions of the underlying rules.

Attacks by undercuts. For expressing undercuts with respect to a logic L=⟨L,⊢⟩ we first have to define logical equivalence in L. A natural way to do so is to require that ψ and φ are logically equivalent in L iff ψ⊢ϕ and ϕ⊢ψ. Using a ⊢-deductive implication ⊃ and a ⊢-conjunctive connective ∧, this means that ⊢(ψ⊃ϕ)∧(ϕ⊃ψ), that is, that ψ↔ϕ is a theorem of L. It follows that attacks by undercuts are represented by the following sequent elimination rule:

Undercut:Γ1⇒ψ1⇒ψ1↔¬⋀Γ2′Γ2,Γ2′⇒ψ2Γ2,Γ2′⇏ψ2.

Attacks by direct and canonical undercuts. Using the same notations as those for attacks by undercuts, and under the same assumptions on the language, attacks by direct undercuts may be represented by the following elimination rule:

Direct Undercut:Γ1⇒ψ1⇒ψ1↔¬γ2Γ2,γ2⇒ψ2Γ2,γ2⇏ψ2.

Similarly, attacks by canonical undercuts may be represented as follows:

Canonical Undercut:Γ1⇒ψ1⇒ψ1↔¬⋀Γ2Γ2⇒ψ2Γ2⇏ψ2.

Attacks by rebuttal and defeating rebuttal. By the discussion above it is easy to see that attacks by rebuttal and defeating rebuttal are also represented by sequent elimination rules. Indeed, these two attacks are represented as follows:

Rebuttal:Γ1⇒ψ1⇒ψ1↔¬ψ2Γ2⇒ψ2Γ2⇏ψ2,Defeating Rebuttal:Γ1⇒ψ1⇒ψ1⊃¬ψ2Γ2⇒ψ2Γ2⇏ψ2.

Remark 4.3

All of the attack rules discussed previously can be represented in a language with ⊢-negation and ⊢-conjunction only, that is, the availability of ⊢-deductive implication (and a corresponding connective for representing equivalence) may not be assumed. The attack rules in the reduced language are represented in Figure 2. In these rules the conditions are not necessarily S-arguments, as the premises of these conditions are not necessarily included in S.⁹9

Figure 2.

Sequent elimination rules.

Note that the compact version of Direct Undercut is the same as Compact Direct Defeat, the compact version of Canonical Undercut is the same as Compact Defeat, and the compact version of Defeating Rebuttal is the same as Compact Rebuttal.

As the next proposition shows, the relations between the attacks in Definition 2.3, indicated in Gorogiannis & Hunter (2011), carry on to our attack rules.

Proposition 4.7

Let L=⟨L,⊢⟩ be a propositional logic, where L has a ⊢-conjunction ∧. Then: (a) Defeating Rebuttal is L-equivalent to Rebuttal, (b) Undercut L-implies Canonical Undercut and Direct Undercut, (c) Canonical Undercut is L-equivalent to Defeat, (d) Direct Defeat isL-equivalent to Direct Undercut.

Proof

Part (a) follows from the fact that both rules are L-equivalent to Compact Rebuttal. Part (b) follows from the fact that Undercut holds in particular when Γ2 is a singleton (in which case Direct Undercut is obtained) and when Γ2 is the whole support set of the sequent (in which case Canonical Undercut is obtained). Part (c) follows from the fact that both Canonical Undercut and Defeat are equivalent to Compact Defeat. Part (d) follows from the fact that Direct Undercut and Direct Defeat are equivalent to Compact Direct Defeat.

Remark 4.4

Further relations between the elimination rules introduced above may be obtained under further assumptions on the underlying logics. For instance, when L is classical logic, Defeat implies Direct Defeat, since in LK the sequent ⇒ψ⊃¬⋀Γ is derivable from ⇒ψ⊃¬γ for any γ∈Γ. Similar considerations show that in this case Defeat also implies Undercut and Defeating Rebuttal.

4.2.Attacks incorporating modalities

The fact that our approach is language-independent enables us to apply it in different scenarios and for a variety of purposes. One of them, demonstrated in Straßer & Arieli (2014), applies sequent-based logical argumentation for modelling normative reasoning in the context of deontic logic (Aqvist, 2002). The idea is to reason with and about norms such as obligations, imperatives, permissions, etc. This is usually formalised by the primitive modal operator O that represents obligations and the defined modal operator P (where P=¬O¬) that represents permissions.

A paradigmatic instance for normative reasoning is so-called factual detachment, saying that if ϕ holds, and there is a commitment to ψ conditional on ϕ, then there is a commitment to ψ. Another instance is aggregation: if there is a norm to bring about ϕ and another norm to bring about ψ then there should be a norm to bring about φ∧ψ. Allowing for unrestricted factual detachment or unrestricted aggregation is problematic in cases in which norms conflict. As shown in Straßer & Arieli (2014) and demonstrated next, attack rules in the context of sequent-based argumentation are useful for representing and handling such conflicts.

Example 4.8

Consider the following example by Horty (1994):

When served a meal one ought to not eat with fingers.
However, if the meal is asparagus one ought to eat with fingers.

The statements above may be represented, respectively, by the formulas m⊃O¬f and (m∧a)⊃Of. Now, in case one is indeed served asparagus (m∧a) we expect to derive the (unconditional) obligation to eat with fingers (Of) rather than to not eat with fingers (O¬f). This is a paradigmatic case of specificity: a more specific obligation cancels (or overrides) a less specific one.

In our setting this may be handled by an attack rule advocating specificity, according to which the argument {m∧a,(m∧a)⊃Of}⇒Of attacks the argument {m,m⊃O¬f}⇒O¬f. Here, arguments are obtained by a sequent calculus for standard deontic logic SDL, which extends LK by the following inference rules for the modal operators: (Below, we denote OΓ for {Oϕ∣ϕ∈Γ})

KR:Γ⇒ϕOΓ⇒OϕDR:Γ⇒ϕOΓ⇒¬O¬ϕ.

The aforesaid attack rule may be formalised as follows:

Specifity:Γ,ϕ⊃ψ⇒ψΓ⇒ϕΓ′⇒ϕ′ϕ⇒ϕ′ψ⇒¬ψ′Γ′,ϕ′⊃ψ′⇒ψ′Γ′,ϕ′⊃ψ′⇏ψ′.

This rule aims at formalising the principle of specificity. It states that when two sequentsΓ′⇒ψ′ and Γ⇒ψ are conflicting, the one which is more specific gets higher precedence, and so the other one is discharged. Thus, in Example 4.1 for instance, Specificity allows to discharge the sequent m,m⊃O¬f⇒O¬f in light of the more specific sequentm∧a,(m∧a)⊃Of⇒Of.

Some variations of Specificity are given below (where NN′∈{OO,OP,PO}):¹⁰10

NN′−SpecΓ,ϕ⊃Nψ⇒NψΓ⇒ϕΓ′⇒ϕ′ϕ⇒ϕ′ψ⇒¬ψ′Γ′,ϕ′⊃N′ψ′⇒N′ψ′Γ′,ϕ′⊃N′ψ′⇏N′ψ′,NN′−SpecNegΓ,ϕ⊃Nψ⇒¬(ϕ′⊃N′ψ′)Γ⇒ϕΓ′⇒ϕ′ϕ⇒ϕ′ψ⇒¬ψ′Γ′,ϕ′⊃N′ψ′⇒ψ′Γ′,ϕ′⊃N′ψ′⇏ψ′.

For instance, PO-Spec models permission as derogation (Stolpe, 2010): a permission may suspend a more general obligation.

4.3.Relevant attacks

When L is a logic in which any formula follows from a contradiction (in particular, if L is classical logic, CL), any sequent is attacked according to each rule in Figure 2. Thus, for instance, when L=CL, S={p,¬p,q}, and the attack rule is Undercut, the sequent q⇒q is attacked by the (classically valid) sequent p,¬p⇒¬q, although – intuitively – q is not really related to the inconsistency in S.

In logics where negated contradictions are theorems, the above phenomenon may be avoided by having some premise attack rules together with restricted rebuttals in which the supports of the attacked arguments are not empty. By this, arguments with inconsistent supports are attacked by arguments with empty supports (whose conclusions are theorems) and arguments with empty supports are not attacked.

In what follows we describe an alternative way of handling attacks by inconsistent supports, in which the above assumptions on the underlying logic and the attack rules are not needed. For this, we follow the primary consideration behind relevance logics and consider variations of the attack rules, according to which the attacking sequent should contain information which is relevant to the attacked sequent (see, e.g. Dunn & Restall, 2002). This is enforced by the variable sharing property, a principle that in our case requires that the support sets of the attacking and the attacked sequents should share variables, and so the former is ‘relevant’ for the latter. Note that by monotonicity, support sets may be artificially extended to contain allegedly relevant information (e.g. p,¬p,q⇒¬q). To prevent this artificial enforcement of variable sharing, relevant attacks are performed only by sequents whose left hand sides contain the ‘most compact support’ for their consequents, as defined next.

Definition 4.9

Let Γ be a set of formulas and ψ a formula in a language L, and denote by Atoms(Γ) the set of atomic formulas that appear in (some formula of) Γ.

Γ is relevant to ψ, if Atoms(Γ)∩Atoms({ψ})=∅ implies that Γ=∅. A non-empty set Γ is irrelevant to a (non-empty) set Δ if Atoms(Γ)∩Atoms(Δ)=∅.
Γ is a most compact support for ψ (with respect to a logic L and a set of assertions S), if Γ⇒ψ∈ArgL(S) and there is no Γ′ with Atoms(Γ′)⊊Atoms(Γ) such that Γ′⇒ψ∈ArgL(S).¹¹11 We denote by mcs(ψ) the set of all formulas σ∈Υ such that ϒ is a most compact support for ψ (with respect to L and S).¹²12
Let R be an elimination rule in Figure 2, in which Γ1⇒ψ1 attacks Γ2⇒ψ2. The relevant variant of R is the application of R with the side conditions (i.e. a restriction on the application of R) that Γ1⊆mcs(ψ1) and Γ1 is relevant to Γ2.

Example 4.10

Relevant Undercut is defined as follows:

[R-Ucut]Γ1⇒ψ1ψ1⇒¬⋀Γ2¬⋀Γ2⇒ψ1Γ2,Γ2′⇒ψ2Γ2,Γ2′⇏ψ2

provided that Γ1 is included in mcs(ψ1) and it is relevant to Γ2. Thus, for instance, when L=CL and S={p,¬p,q}, each one of the the sequents p,q⇒(p∨¬q) and p,q⇒¬¬(p∨¬q) attacks according to this rule the sequent ¬p,q⇒¬(p∨¬q). Note, however, that unlike in the case of Undercut, according to Relevant Undercut p,¬p⇒¬q does not attack q⇒q, since {p,¬p} is not relevant to q.

Remark 4.5

While the variable sharing principle prohibits the possibility that arguments would attack other arguments which are irrelevant to them, a word of caution on using relevant attacks (at least according to our definitions) is in order here. Consider, for instance, the set S1={p,p→r,p∧q∧r,¬r}. In this case, the sequent ¬r⇒¬r is attacked according to [R-Ucut] only by p,p→r⇒r and not by p∧q∧r⇒r, since the latter is not in mcs(r) relative to S1. Moreover, the transition from S1 to its clausal form S2={p,p→r,q,r,¬r}, which keeps the two sets equivalent according to classical logic, has some implications on the attack relation, since ¬r⇒¬r is now attacked according to [R-Ucut] by r⇒r and not by p,p→r⇒r, which in turn does not belong to mcs(r) relative to S2. It follows that relevant attacks are sensitive to the syntactic structure of the underlying set of assertions.¹³13 We refer to Avron (2014) for an in-depth discussion on the relevance principle and corresponding logics.

4.4.Quantitative attacks

Attacks between arguments may be triggered also by considerations that are not necessarily purely logical, but can still be encoded in attack rules. One such consideration is concerned with the amount of formulas that support an argument. Thus, for instance, as we have already noted, when the left-hand-sides of the sequents consist only of literals, one may regard p,q⇒p∨q a stronger argument for p∨q than p⇒p∨q, since the former has a bigger support.

To represent the above considerations in our setting, one may add to the attack rules side conditions that take into account the cardinality of the support sets of the attacking and the attacked arguments. Note however, that one has to be careful with the formalisation of such conditions. For instance, a cardinality-based attack of Γ1⇒ψ on Γ2⇒¬ψ cannot stem only from the fact that |Γ1|>|Γ2| (where |Γ| denotes the size of Γ), since in this case the argument p,p→q⇒q could be attacked by an argument like p,p→r,r→q⇒q or even by r,p,p→q⇒q, whose support sets are bigger, but are certainly not stronger.

Example 4.11

A rebuttal attack rule for capturing 'stronger support due to more relevant evidence' may be formalized as follows:

Γ1⇒ψ1⇒ψ1↔¬ψ2Γ2⇒ψ2Γ2⇏ψ2if|Γ1∩mcs(ψ1)|⩾|Γ2∩mcs(ψ2)|,

where mcs(ψ) is the set of the most compact supports of ψ, defined in Definition 4.9.

To see an application of this rule, consider the set S={p,q,¬(p∨q)} and suppose that the underlying logic is classical logic. Then p,q⇒p∨q attacks according to the above rule the sequent ¬(p∨q)⇒¬(p∨q) (but not the other way around), since its relevant evidential support for p∨q is bigger than the relevant evidence the other sequent has for supporting ¬(p∨q).

We conclude Section 4 with a general observation about its realm.

Remark 4.6

Our purpose in this section was to exemplify the wide range of attack relations that can be expressed by sequent-based rules. How to choose the most appropriate attacks for specific needs is beyond the scope of this paper (mainly due to its generality and the fact that many context-dependent considerations are involved in the study of well-behaved attacks, among which are the language of the arguments and the type of the underlying logic). However, the suitability of attack relations for specific settings is an important issue that should be verified when it comes to applications. To see this we recall Remark 4.5 and the result by Gorogiannis & Hunter (2011) that in the scope of standard propositional languages and classical logic canonical undercuts and rebuttals yield complete extensions (see Definition 5.2) whose arguments have mutually inconsistent conclusions.

For assuring the well-behaviour of attack relations one may need to refer to rationality postulates tailored to the specific logic under consideration (like those specified by Caminada & Amgoud (2007)). This may trigger the introduction of additional machinery such as preference orderings over arguments, as described, for example, in Modgil & Prakken (2013)¹⁴14.

5.Sequent-based argumentation frameworks and their entailments

By Sections 3 and 4 we can now consider argumentation frameworks (Definition 2.1) whose arguments are sequents and whose attacks are obtained by sequent elimination rules. We call these structures sequent-based logical argumentation frameworks.

Definition 5.1

A (sequent-based) logical argumentation framework for a set of formulas S, based on a logic L and a set AttackRules of sequent elimination rules, is the pair AFL(S)=⟨ArgL(S),A⟩, where A⊆ArgL(S)×ArgL(S) and (s1,s2)∈A iff there is R∈AttackRules such that s1 R-attacks s2.

In what follows, somewhat abusing the notations, we shall sometimes identify A withAttackRules.

We are ready now to use sequent-based logical frameworks for commonsense reasoning. As usual in the context of abstract argumentation, we do so by incorporating Dung's notion of extension (Dung, 1995), defined next.

Definition 5.2

Let AFL(S)=⟨ArgL(S),A⟩ be a sequent-based logical argumentation framework (for the set S, based on the logic L), and let E⊆ArgL(S). We say that E attacks an argument (sequent) s if there is an argument s′∈E that attacks s (i.e. (s′,s)∈A). The set of arguments that are attacked by E is denoted E+. We say that E defends s if E attacks every argument s′ that attacks s. The set E is called conflict-free if it does not attack any of its elements (i.e. E+∩E=∅), E is called admissible if it is conflict-free and defends all of its elements, and E is complete if it is admissible and contains all the arguments that it defends. Now:

The minimal complete subset of ArgL(S) is the grounded extension of AFL(S),
A maximal complete subset of ArgL(S) is a preferred extension of AFL(S),
A complete subset E of ArgL(S) that attacks every argument in ArgL(S)∖E is a stable extension of AFL(S).

Below, we denote by Cmpl(AFL(S)) (respectively, by Grnd(AFL(S)), Prf(AFL(S)), Stbl(AFL(S))) the set of all the complete (respectively, all the grounded, preferred, stable) extensions of AFL(S).

The induced entailment relations are now defined as follows:

Definition 5.3

Let AFL(S)=⟨ArgL(S),A⟩ be a sequent-based logical argumentation framework (for the set S of formulas and a logic L), and suppose that Sem∈{Grnd,Prf,Stbl}.

S|∼L,A,Sem∀ψ if every extension E∈Sem(AFL(S)) contains an argument of the form Γ⇒ψ.¹⁵15 In this case we say that ψ skeptically follows from S according to Sem(AFL(S)).
S|∼L,A,Sem∃ψ if there is some extension E∈Sem(AFL(S)) that contains an argument of the form Γ⇒ψ. In this case we say that ψ credulously follows from S according to Sem(AFL(S)).¹⁶16

Notation 5.4

In what follows we shall omit from the entailment notations of Definition 5.3 subscripts or superscripts that do not matter for specific statements. For instance, we shall write |∼L,A,Sem to denote either |∼L,A,Sem∀ or |∼L,A,Sem∃. Similarly, we use the notation |∼ whenever a statement applies to each of the entailment relations in Definition 5.3.

Remark 5.1

A more cautious approach to skeptical reasoning would be to define AFL(S)-based entailments by S|∼L,A,Sem⊓ψ if there is an argument Γ⇒ψ in ArgL(S) that belongs to every extension E∈Sem(AFL(S)). Clearly, it holds that if S|∼L,A,Sem⊓ψ then S|∼L,A,Sem∀ψ. In what follows we shall concentrate on the entailments of Definition 5.3.

Example 5.5

Let us consider a sequent-based argumentation system for S1={p,¬p,q} that is based on classical logic CL, and whose only attack rule is Relevant Undercut (see Example 4.10). It is easy to see that no argument in ArgCL(S1) attacks the argument q⇒q, and so S1|∼CL,R-Ucutq. On the other hand, P⇒p and ¬p⇒¬p attack each other, therefore S1|≁CL,R-Ucutp and S1|≁CL,R-Ucut¬p.

Example 5.6

Consider the set S2={p,q,¬(p∧q)}. When classical logic is the base logic none of the formulas in S2 is derivable, since according to CL each pair of assertions in S2 attack the third one by (Relevant) Undercut.

Suppose now that the base logic is Priest's 3-valued paraconsistent logic LP (see Priest, 1989). A sound and complete sequent calculus for this logic is obtained by keeping the axiom, structural rules, and the inference rules for ∨ and ∧ of LK, and adding the axiom ⇒p,¬p and the negation rules in Figure 3.

Figure 3.

Negation rules for LP.

This time, whatever the attack rules in Figure 2 or their relevant versions are used, the consequences would be different than those that are obtained when CL is the base logic. Indeed, in LP sequents of the form p,¬(p∧q)⇒¬q are not derivable. It follows that while¬(p∧q)⇒¬(p∧q) is still attacked in LP (by p,q⇒p∧q), p⇒p and q⇒q are not attacked.

Example 5.7

Let us recall the set S3={m,a,m⊃O¬f,(m∧a)⊃Of} of Example 4.8. Suppose that SDL is the base logic and OO-SpecNeg is the single attack rule. We observe that, as expected, one concludes the following:

S3|≁SDL,OO-SpecNegO¬f. This is because one cannot derive O¬f, since the sequent m,m⊃O¬f⇒O¬f is attacked by m,a,(m∧a)⊃Of⇒¬(m⊃O¬f).
S3|≁SDL,OO-SpecNegOf. Indeed, the sequent m,a,(m∧a)⊃Of⇒Of is not attacked by an argument in ArgSDL(S3).¹⁷17

Remark 5.2

It is important to note at this point that the reasoning mechanism, depicted in the last examples, is reinforced by corresponding derivation procedures. Such derivations are dynamic in nature, as sequents may not only be introduced during a derivation, but may also be retracted. This brings about a deviation in the standard definition of derivability in Gentzen-type proof systems. We postpone the discussion about this to another paper. The interested reader is referred to Arieli & Straßer (2014) for some definitions and preliminary discussions on this matter.

Next, we consider some basic properties of |∼. In what follows, we fix a (sequent-based) logical argumentation framework AFL(S)=⟨ArgL(S),A⟩ for a set S of L-formulas, based on a logic L=⟨L,⊢⟩ with a sound and complete sequent calculus C, and where A is the set of attacks obtained by the sequent elimination rules in AttackRules (that is, (s1,s2)∈A iff there is R∈AttackRules and s1 R-attackss2).

Proposition 5.8

If ArgL(S) is conflict-free with respect to AFL(S) then S|∼ψ iff S⊢ψ.

Proof

If there are no attacks between arguments in ArgL(S), no attack rule in AttackRules is applicable, and so the single extension of AFL(S) is ArgL(S). It follows, then, that S|∼ψ iff there is a C-derivation of Γ⇒ψ for some Γ⊆S. Since C is sound and complete for L, the latter is a necessary and sufficient condition for Γ⊢ψ, and so (by the monotonicity of L) it is a necessary and sufficient condition for S⊢ψ.¹⁸18

The next result is an immediate corollary of Proposition 5.8:

Corollary 5.9

If AttackRules=∅ then |∼ and ⊢ coincide.

As the examples above show, |∼ and ⊢ are different. In the general case, we have:

Proposition 5.10

If S|∼ψ then S⊢ψ.

Proof

If S|∼ψ then in particular there is a sequent Γ⇒ψ∈ArgL(S) for some Γ⊆S. Thus, there is a proof in C for Γ⇒ψ, and so Γ⊢ψ. By the monotonicity of L we have that S⊢ψ.

Proposition 5.8 implies, in particular, the following results for all the attack relations considered previously in this paper:

Corollary 5.11

|∼is cautiously reflexive: for every formula ψ such that ψ⊬¬ψ it holds that ψ|∼ψ.¹⁹19

Corollary 5.12

For every atom p it holds that p|∼p.

Proof

By Corollary 5.11 and the fact that since ¬ is a negation, for every p it holds that p⊬¬p.

Despite of the last two corollaries, (all) the examples above show that |∼ may not be reflexive. These examples also show that in general |∼ is not monotonic either. For instance, when C=LK and A consists of any of the attack rules in Figure 2, we have that p|∼p while p,¬p|≁p.

Like reflexivity, weak forms of monotonicity can be guaranteed in particular cases. For instance, as Proposition 5.14 below shows, when adding unrelated information to an argumentation framework with relevant attack rules, this information should not disturb previous inferences. For this proposition we first recall the following known notion:

Definition 5.13

Let L=⟨L,⊢⟩ be a propositional logic.

A set T of formulas (in L) is called ⊢-consistent if there exists a formula ψ (in L) such that T⊬ψ.
We say that L is uniform, if for every two sets of formulas T1,T2 and formula ψ we have that T1⊢ψ when T1,T2⊢ψ and T2 is a ⊢-consistent theory that has no atomic formulas in common with Γ1∪{ψ}.

Remark 5.3

By Łos-Suzsko Theorem (Łos & Suzsko, 1958), a finitary propositional logic ⟨L,⊢⟩ is uniform iff it has a single characteristic matrix (see also Urquhart, 2001). Thus, for instance, the logics in this paper are uniform.

Proposition 5.14

Let L=⟨L,⊢⟩ be a uniform logic, and let R be a set of attack rules in Relevant Compact Defeat, Relevant Compact Direct Defeat, Relevant Undercut, Relevant Direct Undercut, and Relevant Canonical Undercut. If S1|∼L,Rψ and S2 is a ⊢-consistent set of formulas that is irrelevant (in the sense of Definition 4.9) to S1, then S1,S2|∼L,Rψ.²⁰20

Proof

First, we show the following lemma:

Lemma 5.15

No argument in ArgL(S1) is attacked, according to the rules in R, by an argument in ArgL(S1∪S2)−ArgL(S1).

Proof

In the notations of Definition 5.2, we have to show that ArgL(S1)∩(ArgL(S1∪S2)−ArgL(S1))+=∅. Indeed, assume for contradiction that some Υ⇒ψ∈ArgL(S1∪S2)−ArgL(S1) R-attacks some Γ⇒ϕ∈ArgL(S1), and let δ∈Υ∩S2 (such a δ exists, otherwise Υ⊆S1 and so Υ⇒ψ∈ArgL(S1)). In particular, δ∈mcs(ψ), and so there is a sequent Δ⇒ψ that R-attacks Γ⇒ϕ for some R∈R and where Δ is a most compact support for ψ that contains δ.

Suppose first that R is one of the defeat rules. In this case ψ=¬⋀Γ′, where Γ′⊆Γ. Since S2 is ⊢-consistent, by the uniformity of L we have that Δ∩S1⇒¬⋀Γ′∈ArgL(S1), but since Atoms(Δ∩S1)⊊Atoms(Δ) (as δ∈Δ), this contradicts the assumption that Δ is a most compact support for ψ.
Suppose now that R is one of the undercut rules. In this case both of ψ⇒¬⋀Γ′ and ¬⋀Γ′⇒ψ are C-derivable for some Γ′⊆Γ. Now, the application of Remark 3.2 on Δ⇒ψ and ψ⇒¬⋀Γ′ yields that Δ⇒¬⋀Γ′∈ArgL(S1∪S2). Hence, by the uniformity of L and since S2 is ⊢-consistent, Δ∩S1⇒¬⋀Γ′∈ArgL(S1). By Remark 3.2 again and the fact that ¬⋀Γ′⇒ψ is C-derivable, we get that Δ∩S1⇒ψ∈ArgL(S1). Once again, this is a contradiction to the choice of Δ as a most compact support for ψ, since Atoms(Δ∩S1)⊊Atoms(Δ).

The proof of Proposition 5.14 now proceeds as follows: By the lemma above, the addition of irrelevant information (S2) to existing information (S1) does not produce more attacks on existing arguments, and so every Sem-extension E1∈Sem(AFL(S1)) is included in some Sem-extension E2∈Sem(AFL(S1∪S2)). We also get the converse, since in our case the arguments in E∩(ArgL(S1∪S2)−ArgL(S1)) do not defend the arguments in E, and so if E∈Sem(AFL(S1∪S2)) then E2∩ArgL(S1)∈Sem(AFL(S1)). Suppose then that S1|∼L,Rψ. This means that every [some] extension E1∈Sem(AFL(S1)) contains an argument of the form Γ⇒ψ where Γ⊆S1, and so every [some] extension E2∈Sem(AFL(S1∪S2)) contains an argument of the form Γ⇒ψ where Γ⊆S1 (thus Γ⊆S1∪S2). This implies thatS1,S2|∼L,Rψ.

In the Appendix we show that, assuming that the base logic satisfies some simple properties, the cautious form of monotonicity in Proposition 5.14 holds also for frameworks with non-relevant attack rules (see Propositions A.2 and A.3).

We conclude this section by checking two properties of |∼ that assure proper handling of inconsistent information: paraconsistency (da Costa, 1974) and crash resistance (Caminada, Carnielli, & Dunne, 2012). We start with the former.

Proposition 5.16

If ⊢ is paraconsistent (p,¬p⊬q for p≠q) then so is |∼.

Proof

By Proposition 5.10, S|≁ψ when S⊬ψ. Thus, if p,¬p⊬q then p,¬p|≁q as well, and so |∼ is paraconsistent.

Next, we consider crash resistance.

Definition 5.17

Let S be a set of L-formulas such that Atoms(S)⊊Atoms(L).

S is called contaminating for |∼, if for every set T that is irrelevant for S and for every formula ϕ, it holds that S|∼φ iff S,T|∼φ.
|∼ is crash-resistant if there is no set of formulas that is contaminating for |∼.

Proposition 5.18

Let L=⟨L,⊢⟩ be a uniform logic that has the variable sharing property (so it resists irrelevant information: S⊬ψ when ψ is irrelevant to S). Then, in the notations of Proposition 5.14, |∼L,R is crash resistant.

Proof

Suppose for a contradiction that there is a set S that is contaminating for |∼L,R. Let p be an atom that does not appear in S. Then S⊬p and by Proposition 5.10, S|≁L,Rp. Since S is contaminating we have that S,p|≁L,Rp. On the other hand, by Corollary 5.12, p|∼L,Rp, and so by Proposition 5.14, S,p|∼L,Rp — a contradiction.

Proposition 5.19

Let L=⟨L,⊢⟩ be a logic with a ⊢-deductive ⊃. Suppose that

(1) L has the variable sharing property for consistent sets (if S is ⊢-consistent and ψ is irrelevant to S then S⊬ψ), and that
(2) L is consistency-enforcing (⊢¬⋀Γ whenever a finite Γ is ⊢-inconsistent).

Let ∅≠R⊆{Defeat, Compact Defeat, Undercut, Canonical Undercut, Compact Undercut}. Then, |∼L,R is crash resistant.

Proof.First we show:

Lemma 5.20

For any S and any s=Υ⇒ψ∈ArgL(S) such that ϒ is ⊢-inconsistent there is a s′∈ArgL(S)−ArgL(S)+ that R-attacks s.

Proof

Since ϒ is ⊢-inconsistent, by (2), s′=⇒¬⋀Υ∈ArgL(S). It is easy to see that s′ R-attacks s for all R∈R and that s′ is not attacked in ArgL(S).

Suppose for a contradiction that there is a set S that is contaminating for |∼L,R. Let p be an atom that does not appear in S. By (1), for every Υ⇒p∈ArgL(S), ϒ is ⊢-inconsistent. By Lemma 5.20 we have S|≁L,Rp and hence by the supposition also S,p|≁L,Rp. To see that S,p|∼L,Rp, suppose that Υ⇒ψ∈ArgL(S∪{p})R-attacks p⇒p. Then ψ⇒¬p∈ArgL(S∪{p}) and by transitivity, Υ⇒¬p∈ArgL(S∪{p}). If p∉Υ, ϒ is ⊢-inconsistent by (1). If p∈Υ then Υ−{p}⇒p⊃¬p∈ArgL(S) and again ϒ is ⊢-inconsistent by (1). By Lemma 5.20, then, Υ⇒ψ is attacked by some non-attacked sequent in ArgL(S∪{p}). It follows that p⇒p is defended by S∪{p} and hence S,p|∼L,Rp. Thus S is cannot be contaminating for |∼L,R.

6.Related work

Different approaches to logical argumentation have been introduced in the literature, including formalisms that are based on classical logic (Besnard & Hunter, 2001, 2009), defeasible reasoning (Governatori, Maher, Antoniou, & Billington, 2004; Pollock, 1991, 1995; Simari & Loui, 1992) abstract argumentation and the ASPIC+ framework (Modgil & Prakken, 2014; Prakken, 2010), assumption-based argumentation (Dung, Kowalski, & Toni, 2006), default logic (Prakken, 1993), situation calculus (Brewka, 2001), and so forth.

The starting point of this paper is Besnard and Hunter's approach to logical argumentation (Besnard & Hunter, 2001, 2009), which we believe is a successful way of representing deductive reasoning in argumentation-based environments (we refer to Besnard & Hunter, 2009 for some comparisons of this approach to other logic-based approaches, in particular the above-mentioned work on defeasible reasoning). Our work extends this approach in several ways: first, the usual conditions of minimality and consistency of supports are abandoned. This offers a simpler way of producing arguments and identifying them (also for systems that are not formulated in a Gentzen-type style).²¹21 Second, arguments are produced and are withdrawn by rules of the same style, allowing for a more uniform way of representing the frameworks and computing their extensions. Third, our approach is logic-independent. This allows in particular to rely on a classical as well as on a non-classical logic, and so, for instance, paraconsistent formalisms may be used for improving consistency-maintenance.

Another sequent-based approach to logical argumentation has been proposed by Pollock (1991, 1995), where arguments are sequences of sequents of the form ⟨Γ,p⟩, obtained by generic inference rules (Input, Reason, Supposition, Conditionalisation, and Dilemma), and organised in inference graphs. Unlike the present approach, Pollock distinguishes between defeasible and conclusive (strict) arguments, where only defeasible arguments can be attacked.

The ingredients of Pollock's setting may be simulated in our setting. First, in the presence of a calculus like LK, Pollock's rules are translatable into our representation. For instance, Input is the Axiom ψ⇒ψ with Left-Weakening, Supposition is Reflexivity, Conditionalisation is [⇒⊃], and Dilemma is reasoning by cases. Second, it is not difficult to adjust our setting for accommodating two (or more) kinds of arguments. In the presence of strict argument, denoted by Γ⇒ψ, and defeasible arguments, denoted by Γ↪ψ, one may define attack rules of the following form:

Γ1↪ψ1Γ2⇒ψ2…Γn−1⇒ψn−1Γn↪ψnΓn↪̸ψn.

The rule above expressed that (an argument obtained from the defeasible schema) Γ1↪ψ1 attacks (an argument obtained from the defeasible schema) Γn↪ψn, provided that the conditions in {Γ2⇒ψ2,…,Γn−1⇒ψn−1} are satisfied.

The ASPIC+ framework (Modgil & Prakken, 2014; Prakken, 2010) is a comprehensive instantiation of Dung's abstract argumentation framework (Dung, 1995). Just like Pollock's account, it distinguishes between defeasible and non-defeasible arguments based on the distinction between defeasible and strict rules. Arguments are inference trees. Attacks are generated in view of a contrariness function that also captures weaker negations than classical negation. Different consequence relations are devised in view of semantics for abstract argumentation. In this sense, ASPIC+, like our approach, provides a very flexible environment for logical argumentation, leaving open the choices of the underlying language, the core logic, and the adequate calculus.

Our approach overcomes some difficulties of using classical logic to obtain strict rules in ASPIC+ and in Pollock's OSCAR system (Pollock, 1992, 1995). In Wu (2012, Chapter 6) it is shown that consequences are not necessarily retained when unrelated information is added to those systems under the standard semantics such as preferred or grounded semantics. As shown in Propositions 5.3, this difficulty may be avoided in some of the sequent-based settings proposed here (see also Propositions A.2 and A.3 in the Appendix).

7.Conclusion and further work

The primary message of this paper is that sequent-based representation and reasoning is an appropriate setting for logic-based modelling of argumentation systems. Among others, this approach enables a general and natural way of expressing arguments and implies that well-studied techniques and methodologies may be borrowed from proof theory and applied in the context of argumentation theory.

Some important issues are left for future work. One of them is a development of practical means for computing the consequences of sequent-based argumentation frameworks. This requires an automated machinery that not only produces sequents, but is also capable of eliminating them, as well as their consequences. Here, techniques like those used in the context of dynamic proof theory for adaptive logics may be useful (see, e.g. Batens, 2007; Straßer, 2014). Some results in this direction are reported in Arieli & Straßer (2014).

Future work also involves the exploration of further utilisations of arguments as sequents. Below, we hint of two such opportunities:

We used Gentzen-type systems which employ finite sets of formulas. However, one could follow Gentzen's original formulation and use sequences instead. This would allow, for instance, to encode preferences in the arguments, where the order in a sequence represents priorities. In this way one would be able to argue, for example, that Γ⇒p for any finite sequence Γ of literals that contains p and in which the first appearance of p precedes any appearance of ¬p. Another possibility is to employ multisets in the sequents, for example, for representing majority considerations. Thus, one may state that Γ⇒p holds whenever the number of appearances of p in a multiset Γ of literals is strictly bigger than the number of appearances of ¬p in the same multiset. Of-course, the opposite may also be stated when incorporating mathematical objects other than (finite) sets. That is, it is possible to explicitly indicate that the order and/or the number of appearances of formulas do not matter, by introducing (either of) the following standard structural rules:
Permutation:Γ1,ψ,φ,Γ2⇒ΔΓ1,φ,ψ,Γ2⇒ΔΓ⇒Δ1,ψ,φ,Δ2Γ⇒Δ1,φ,ψ,Δ2,Contraction:Γ1,ψ,ψ,Γ2⇒ΔΓ1,ψ,Γ2⇒ΔΓ⇒Δ1,ψ,ψ,Δ2Γ⇒Δ1,ψ,Δ2.
The incorporation of more complex forms of sequents, such as hypersequents (Avron, 1987) or nested sequents (Brünnler, 2010), allows to express more sophisticated forms of argumentation, such as argumentation by counterfactuals or case-based argumentation. For instance, the nested sequent Γ1⇒(Γ2⇒ψ) may be intuitively understood by ‘if Γ1 were true, one would argue that Γ2⇒ψ’ and the hypersequent Γ1⇒ψ1∣Γ2⇒ψ2 may be understood (again, intuitively) as a disjunction, at the meta-level, of the arguments Γ1⇒ψ1 and Γ2⇒ψ2.

Notes

1 Clearly, the argument A may be split into two BH-arguments, A1=⟨{p},p∨q⟩ and A2=⟨{q},p∨q⟩, but in general such rewriting requires further processing and might cause a blowup in the number of arguments.

2 Another argument that is sometimes pleaded for set-inclusion minimisation is that it reduces the number of attacks. Again, it is disputable whether set-inclusion minimisation is the right principle for assuring this property, since, for instance, the singletons S1={p1} and S2={p2∧…∧pn}, supporting (e.g. in classical logic) the claim p1∨…∨pn, are incomparable w.r.t. set-inclusion (and moreover they even do not share any atomic formula), but it is obvious that as n becomes larger S2 becomes more exposed to attacks than S1.

3 The availability of an implication connective is not required – see Remark 4.3.

4 Following the usual convention, we shall omit set-brackets from the left-hand sides of sequents.

5 Obviously, for the definition of an L-argument it does not matter which of the calculi that are sound and complete for L is chosen.

6 Following the usual conventions, we use commas in a sequent for denoting the union operation, and omit curly brackets of singletons (i.e. we write ψ instead of {ψ}).

7 Note that ArgsBH(S) is cautiously S-reflexive: ⟨{ψ},ψ⟩∈ArgsBH(S) for a consistent formula ψ∈S.

8 Gorogiannis & Hunter (2011) consider a stricter implication between attacks, in which ϕ=ψ.

9 To reduce the amount of notations, we use the same names for the rules with and without the implication connective. This will not cause ambiguity in what follows.

10 Note that ‘PP-Spec’ or ‘PP-SpecNeg’ variants would not be sensible, since permissions with incompatible content do not conflict in any intuitive sense.

11 Note that this condition does not imply a subset-minimality of Γ, but rather assures that Γ does not contain information that is irrelevant (in the sense of Item (a)) for its conclusion.

12 For instance, when L=CL and S={p,q}, we have that p,q∈mcs(p∨q).

13 On the other hand, relevant attack rules have some desirable properties that are not necessarily shared by other rules, like being invariant with respect to irrelevant information – see Lemma 5.15.

14 See also the conclusion of this paper for a short discussion on implementing preferences in sequents.

15 Recall that by the definition of ArgL(S), this implies that Γ⊆S.

16 Similar entailment relations may of-course be defined for other semantics of abstract argumentation frameworks, such as semi-stable semantics (Caminada, 2006), ideal semantics (Dung, Mancarella, & Toni, 2007), eager semantics (Caminada, 2007), and so forth.

17 It is important to note that m,a,(m∧a)⊃Of⇒Of is attacked by SDL-derivable arguments (such as m,m⊃O¬f,m,a,(m∧a)⊃O¬f⇒¬((m∧a)⊃Of)), but none of them is in ArgSDL(S3).

18 In case that S is infinite, compactness of L should be assumed along the proof.

19 Note that the condition is indeed required here. For instance, in an argumentation framework based on CL and Undercut it holds that p∧¬p|≁CL,Ucutp∧¬p. (Indeed, according to any semantics considered here p∧¬p⇒p∧¬p is undefended, since it is attacked by ⇒¬(p∧¬p), and the latter is not attacked by any other sequent since its left-hand side is empty).

20 Recall that by Notation 5.4 this means that the proposition holds for every entailment of the form |∼L,R,Semπ considered in Definition 5.3, where L and R are as defined in the proposition, Sem is any of the standard argumentation semantics considered in this paper, and π∈{∀,∃}.

21 Other techniques for generating arguments are considered, for example, in Besnard, Grégoire, Piette, and Raddaoui (2010) and Efstathiou & Hunter (2011).

Conflict of interest disclosure statement

No potential conflict of interest was reported by the authors.

Funding

Christian Straßer's research was supported by the Alexander von Humboldt Foundation and the German Ministry for Education and Research.

References

1	Amgoud L., & Besnard P. ((2009) ). Bridging the gap between abstract argumentation systems and logic. Proc. SUM'09, LNCS, Vol. 5785. Heidelberg: Springer, pp. 12–27.
2	Amgoud L., & Besnard P. ((2010) ). A formal analysis of logic-based argumentation systems. Proc. SUM'10, LNCS, Vol. 6379. Heidelberg: Springer, pp. 42–55.
3	Aqvist L. ((2002) ). Deontic logic. In D. M. Gabbay and F. Guenthner (Eds.), Handbook of philosophical logic (Vol. 8, pp. 147–264). Dordrecht: Kluwer.
4	Arieli O. ((2013) ). A sequent-based representation of logical argumentation. Proc. CLIMA'13, LNCS, Vol. 8143. Heidelberg: Springer, pp. 69–85.
5	Arieli O., & Straßer C. ((2014) ). Dynamic derivations for sequent-based deductive argumentation. Proc. COMMA'14, Frontiers in artificial intelligence and applications, Vol. 266, IOS Press, pp. 89–100.
6	Avron A. ((1987) ). A constructive analysis of RM. Journal of Symbolic Logic, 52: , 939–951. doi: 10.2307/2273828
7	Avron A. ((2014) ). What is relevance logic? Annals of Pure and Appied Logic, 165: , 26–48. doi: 10.1016/j.apal.2013.07.004
8	Batens D. ((2007) ). A universal logic approach to adaptive logics. Logica Universalis, 1: , 221–242. doi: 10.1007/s11787-006-0012-5
9	Belnap N. D. ((1977) ). A useful four-valued logic. In M. Dunn and G. Epstein (Eds.), Modern uses of multiple-valued logics (pp. 7–37). Dordrecht: Reidel Publishing.
10	Besnard P., Grégoire É., Piette C., & Raddaoui B. ((2010) ). MUS-based generation of arguments and counter-arguments. Proc. IRI'10, IEEE, pp. 239–244.
11	Besnard P., & Hunter A. ((2001) ). A logic-based theory of deductive arguments. Artificial Intelligence, 128: , 203–235. doi: 10.1016/S0004-3702(01)00071-6
12	Besnard P., & Hunter A. ((2009) ). Argumentation based on classical logic. In I. Rahwan and G. R. Simari (Eds.), Argumentation in artificial intelligence (pp. 133–152). Dordrecht: Springer.
13	Brewka G. ((2001) ). Dynamic argument systems: A formal model of argumentation processes based on situation calculus. Journal of Logic and Computation, 11: , 257–282. doi: 10.1093/logcom/11.2.257
14	Brünnler K. ((2010) ). Nested sequents (PhD thesis). University of Bern.
15	Caminada M.W.A. ((2006) ). Semi-stable semantics. Proc. COMMA'06, IOS Press, pp. 121–130.
16	Caminada M.W.A. ((2007) ). Comparing two unique extension semantics for formal argumentation: ideal and eager. Proc. BNAIC'07, 81–87.
17	Caminada M.W.A., & Amgoud L. ((2007) ). On the evaluation of argumentation formalisms. Artificial Intelligence, 171: , 286–310. doi: 10.1016/j.artint.2007.02.003
18	Caminada M.W.A., Carnielli W.A., & Dunne P.E. ((2012) ). Semi-stable semantics. Journal of Logic and Computation, 22: , 1207–1254. doi: 10.1093/logcom/exr033
19	Chesñevar C.I., Maguitman A.G., & Loui R.P. ((2000) ). Logical models of argument. ACM Computing Surveys, 32: , 337–383. doi: 10.1145/371578.371581
20	da Costa N.C.A. ((1974) ). On the theory of inconsistent formal systems. Notre Dame Journal of Formal Logic, 15: , 497–510. doi: 10.1305/ndjfl/1093891487
21	Dung P.M. ((1995) ). On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence, 77: , 321–357. doi: 10.1016/0004-3702(94)00041-X
22	Dung P.M., Kowalski R., & Toni F. ((2006) ). Dialectic proof procedures for assumption-based, admissible argumentation. Artificial Intelligence, 170: , 114–159. doi: 10.1016/j.artint.2005.07.002
23	Dung P.M., Mancarella P., & Toni F. ((2007) ). Computing ideal sceptical argumentation. Artificial Intelligence, 171: , 642–674. doi: 10.1016/j.artint.2007.05.003
24	Dunn J.M., & Restall G. ((2002) ). Relevance logic. In D. Gabbay & F. Guenther (Eds.), Handbook of philosophical logic (Vol. 6, pp. 1–136). Dordrecht: Kluwer.
25	Efstathiou V., & Hunter A. ((2011) ). Algorithms for generating arguments and counterarguments in propositional logic. International Journal of Approximate Reasoning, 52: , 672–704. doi: 10.1016/j.ijar.2011.01.005
26	Eiter T., & Gottlob G. ((1995) ). The complexity of logic-based abduction. ACM Journal, 42: , 3–42. doi: 10.1145/200836.200838
27	Gentzen G., Investigations into logical deduction. In German. An English translation appears in ‘The collected works of Gerhard Gentzen’, edited by M.E. Szabo, North-Holland, 1969. (1934).
28	Gorogiannis N., & Hunter A. ((2011) ). Instantiating abstract argumentation with classical logic arguments: Postulates and properties. Artificial Intelligence, 175: , 1479–1497. doi: 10.1016/j.artint.2010.12.003
29	Governatori G., Maher M.J., Antoniou G., & Billington D. ((2004) ). Argumentation semantics for defeasible logic. Journal of Logic and Computation, 14: , 675–702. doi: 10.1093/logcom/14.5.675
30	Horty J.F. ((1994) ). Moral dilemmas and nonmonotonic logic. Journal of Philosiphical Logic, 23: , 35–65. doi: 10.1007/BF01417957
31	Łos J., & Suzsko R. ((1958) ). Remarks on sentential logics. Indagationes Mathematicae, 20: , 177–183.
32	Modgil S., & Prakken H. ((2013) ). A general account of argumentation with preferences. Artificial Intelligence, 195: , 361–397. doi: 10.1016/j.artint.2012.10.008
33	Modgil S., & Prakken H. ((2014) ). The ASPIC+ framework for structured argumentation: A tutorial. Argument and Computation, 5: , 31–62. doi: 10.1080/19462166.2013.869766
34	Pollock J.L. ((1987) ). Defeasible reasoning. Cognitive Science, 11: , 481–518. doi: 10.1207/s15516709cog1104_4
35	Pollock J.L. ((1991) ). A theory of defeasible reasoning. International Journal of Intelligent Systems, 6: , 33–54. doi: 10.1002/int.4550060103
36	Pollock J.L. ((1992) ). How to reason defeasibly. Artificial Intelligence, 57: , 1–42. doi: 10.1016/0004-3702(92)90103-5
37	Pollock J. ((1995) ). Cognitive carpentry. A blueprint for how to build a person. Cambridge, MA: MIT Press.
38	Prakken H. ((1993) ). An argumentation framework in default logic. Annals of Mathematics and Artificial Intelligence, 9: , 93–132. doi: 10.1007/BF01531263
39	Prakken H. ((1996) ). Two approaches to the formalisation of defeasible deontic reasoning. Studia Logica, 57: , 73–90. doi: 10.1007/BF00370670
40	Prakken H. ((2010) ). An abstract framework for argumentation with structured arguments. Argument and Computation, 1: , 93–124. doi: 10.1080/19462160903564592
41	Prakken H., & Vreeswijk G. ((2002) ). Logical systems for defeasible argumentation. In D. Gabbay and F. Guenthner (Eds.), Handbook of philosophical logic (Vol. 4, pp. 219–318). Dordrecht: Kluwer.
42	Priest G. ((1989) ). Reasoning about truth. Artificial Intelligence, 39: , 231–244. doi: 10.1016/0004-3702(89)90027-1
43	Simari G.R., & Loui R.P. ((1992) ). A mathematical treatment of defeasible reasoning and its implementation. Artificial Intelligence, 53: , 125–157. doi: 10.1016/0004-3702(92)90069-A
44	Stolpe A. ((2010) ). A theory of permission based on the notion of derogation. Journal of Applied Logic, 8: , 97–113. doi: 10.1016/j.jal.2010.01.001
45	Straßer C. ((2014) ). Adaptive logics for defeasible reasoning. Applications in argumentation, normative reasoning and default reasoning. Heidelberg: Springer.
46	Straßer C., & Arieli O. ((2014) ). Sequent-based argumentation for normative reasoning. Proc. DEON'14, LNAI, Vol. 8554. Heidelberg: Springer, pp. 224–240.
47	Urquhart A. ((2001) ). Many-valued logic. In D. Gabbay and F. Guenthner (Eds.), Handbook of philosophical logic (Vol. II, pp. 249–295). Dordrecht: Kluwer.
48	Wu Y. ((2012) ). Between argument and conclusion. Argument-based approaches to discussion, inference and uncertainty (PhD thesis). University of Luxembourg.

Appendices

Appendix. Some further results about the restricted monotonicity of |∼

Below we show that under some (rather intuitive) requirement on the base logic L, restricted monotonicity with respect to relevant attacks (Proposition 5.3) may be generalised to other attack rules. For this, we first need to introduce some new terminology.

Definition A.1

Let L=⟨L,⊢⟩ be a propositional logic.

We say that L is consistency-enforcing, if for every finite set of L-formulas Γ that is not ⊢-consistent it holds that ⊢¬⋀Γ.
We say that L is ¬∧-expanding, if Υ⊢¬⋀Γ implies that Υ⊢¬⋀Γ′ for every finite set Γ′ that contains Γ.

In what follows we consider sequent elimination rules representing premise attacks (prem-attacks, for short), that is: all the forms of defeat and undercut in Figure 2. In addition, we assume that a given set R of prem-attacks rules contains at least one of the rules Defeat, Compact Defeat, Undercut, Compact Undercut, or Canonical Undercut.

The main results of this Appendix are then the following:

Proposition A.2

Let L=⟨L,⊢⟩ be a uniform, ¬∧-expanding and consistency-enforcing logic, R a set of prem-attacking rules, and Sem a semantics which is either complete, grounded, preferred or stable. If S1|∼L,R,Sem∀ψ and S1 is irrelevant to S2, then S1,S2|∼L,R,Sem∀ψ.

Proposition A.3

Let L=⟨L,⊢⟩ be a uniform, ¬∧-expanding and consistency-enforcing logic, R a set of prem-attacking rules, and Sem a semantics which is either complete, grounded or preferred (The question whether this proposition holds also for stable semantics is left for future work.). If S1|∼L,R,Sem∃ψ and S1 is irrelevant to S2, then S1,S2|∼L,R,Sem∃ψ.

Note that, unlike Proposition 5.14, in the propositions above S2 need not be ⊢-consistent.

To show the Propositions A.2 and A.3, we need a few lemmas. The first lemma holds in every argumentation framework AF=⟨Args,A⟩ with a set Root(AF)=Args−Args+ of unattacked arguments.

Lemma A.4

Let AF′=AF↓Args−Root(AF)+ be the framework AF=⟨Args,A⟩, restricted to Args−Root(AF)+. Then Cmpl(AF)=Cmpl(AF′).

Proof

To see that Cmpl(AF)⊆Cmpl(AF′), suppose that E∈Cmpl(AF). Then Root(AF)⊆E. Since E is conflict-free, necessarily Root(AF)+∩E=∅, and so E⊆Args−Root(AF)+. Suppose now that E defends in AF′ an argument A∈Args−Root(AF)+. If E defends A also in AF then by the completeness of E, A∈E. If E does not defend A in AF, then there is a B∈Root(AF)+ that A-attacks A, butB∉E+. However, since B∈Root(AF)+, there is a C∈Root(AF) such that C A-attacks B. But Root(AF)⊆E, so C∈E, which contradicts the assumption that B∉E+. We have thus shown that every argument that is defended by E in AF′ is in E. Let now A∈E and suppose some B∈Args−Root(AF)+ attacks A in AF′. Clearly, B also attacks A in AF. By the completeness of E in AF, B is attacked by some C∈E in AF. Since B∈Args−Root(AF)+ and E⊆Args−Root(AF)+, C also attacks B in AF′. Hence, E defends itself in AF′. Altogether, we have shown that E∈Cmpl(AF′)

To see that Cmpl(AF′)⊆Cmpl(AF), suppose that E∈Cmpl(AF′). Note first that by the definition of AF′, Root(AF)⊆Root(AF′). Since E is complete in AF′, Root(AF′)⊆E, and hence Root(AF)⊆E. We now show that E∈Cmpl(AF). Clearly, E is conflict-free in AF since the only attacks that are added by moving from A′ (the attack relation of AF′) to A are attacks between Args and Root(AF)+ and between Root(AF)+ and Args. Suppose now that E defends in AF some A∈Args. IfE also defends A in AF′ then A∈E. Otherwise, E does not defend A in AF′. By the conflict-freeness of E and since Root(AF)⊆E, A cannot be in Root(AF)+. Hence, A∈Args−Root(AF)+, and so there is an A′-attacker B of A such that there is no C∈E such that C A′-attacks B. However, there must be a D∈E such that DA-attacks B. This means that B∈Root(AF)+. However, since B A′-attacks A, B∉Root(AF)+, a contradiction. We have thus shown that whenever E defends some A∈Args then A∈E. Conversely, suppose that A∈E and some B∈Args attacks A in AF. If B∈Root(AF)+ then B∈E+, since Root(AF)⊆E. In case B∈Args−Root(AF)+, also B∈E+, as E∈Cmpl(AF′). Thus, E defends all of its elements. Altogether, we have shown that E∈Cmpl(AF).

Remark A.1

Lemma A.4 may be adjusted to any completeness-based semantics, that is, to every semantics Sem such that Cmpl(AF)=Cmpl(AF′) implies Sem(AF)=Sem(AF′) and Sem(AF)⊆Cmpl(AF) (Note that all the semantics considered in this paper are completeness-based.). Thus, for every framework AF, its induced framework AF′ as defined in Lemma A.4, and a completeness-based semantics Sem, we have that Sem(AF)=Sem(AF′).

Next, we fix some logic L=⟨L,⊢⟩ and a sequent-based argumentation framework AFL(S)=⟨ArgL(S),A⟩, for which we use the following notations:

ArgL∅(S)={A∈ArgL(S)∣A is of the form ⇒Δ},
ArgL⊥(S)={A∈ArgL(S)∣A is of the form Υ⇒Δ where ϒ is ⊢-inconsistent}.

By Remark A.1 we conclude that every extension with respect to a completeness-based semantics of an argumentation framework AFL(S) whose base logic L is consistency-enforcing (and whose elimination rules are prem-attacking), consists only of sequents whose premises are ⊢-consistent. Formally:

Corollary A.5

Let AFL(S)=⟨ArgL(S),A⟩ be a sequent-based argumentation framework where L is consistency-enforcing and whose rules in R are prem-attacks. Then for every completeness-based semanticsSem and every E∈Sem(AFL(S)) it holds that E∩ArgL⊥(S)=∅.

Proof

Since AFL(S) has only prem-attack rules, ArgL∅(S)⊆Root(AFL(S)). Since L is consistency-enforcing, ArgL⊥(S)⊆ArgL∅(S)+ (This is due to the supposition that R contains at least one of the rules Defeat, Compact Defeat, Undercut, Compact Undercut, or Canonical Undercut, mentioned at the beginning of the Appendix. This allows to derive the sequent ⇒¬⋀Υ where ϒ is ⊢-inconsistent.). Thus:

(A1)

ArgL⊥(S)⊆ArgL∅(S)+⊆Root(AFL(S))+.

By Remark A.1, if E∈Sem(AFL(S)) then E∈Sem(AFL′(S)), and so:

(A2)

E∩Root(AFL(S))+=∅.

By Equations (A1) and (A2) the corollary follows.

The next two lemmas present other properties that will be needed in the sequel.

Lemma A.6

Let L=⟨L,⊢⟩ be a uniform and consistency-enforcing logic, and let R be a set of prem-attack rules. Suppose that S1 is a set of L-formulas that is irrelevant to a set of L-formulas S2. If an argument A=Υ⇒ψ∈ArgL(S1∪S2)−ArgL⊥(S1∪S2) R-attacks an argument B=Γ⇒ϕ∈ArgL(S1) according to a rule R∈R, then there is a formulaψ1 such that the argument A1=Υ∩S1⇒ψ1∈ArgL(S1) R-attacks B.

Proof

Suppose that A R-attacks B where R∈R.

Suppose first that R is a direct prem-attacking rule (i.e. either Direct Defeat, Compact Direct Defeat, or Direct Undercut). In this case ψ⊢ψ′ where ψ′∈Γ. Hence, by Remark 3.2, Υ⇒ψ′ is in ArgL(S1∪S2). Since Υ∩S2 is ⊢-consistent (because so is ϒ), by the uniformity of L, A1=Υ∩S1⇒ψ′∈ArgL(S1). Obviously, A1 R-attacks B.
Suppose now that R is a compact prem-attacking rule (Compact Defeat, Compact Direct Defeat, Compact Undercut). Then ψ=¬⋀Γ′ for some Γ′⊆Γ. Again, by the uniformity of L we have that A1=Υ∩S1⇒¬⋀Γ′∈ArgL(S1). Clearly, A1 R-attacks B.
Suppose that R is any other prem-attacking rule (that is, Undercut, Canonical Undercut, or Defeat). Then ψ⊢¬⋀Γ′ for some Γ′⊆Γ. By Remark 3.2, then, Υ⇒¬⋀Γ′∈ArgL(S1∪S2). Again, by the uniformity of L, we have that A1=Υ∩S1⇒¬⋀Γ′∈ArgL(S1). Clearly, A1 R-attacks B.

In each case, then, there is a formula ψ1 such that the argument Υ∩S1⇒ψ1 is in ArgL(S1) and R-attacks B.

Notation A.7

ES,R+={A∈ArgL(S)∣there is a B∈E such that B R-attacks A for some R∈R}.

Lemma A.8

Let AFL(S)=⟨ArgL(S),A⟩ be a sequent-based argumentation framework, where L is an ¬∧-expanding logic and R is a set of prem-attack rules. Suppose that E∈Cmpl(AFL(S)) and that A=Υ⇒Δ and A′=Υ′⇒Δ′ are derivable sequents where Υ′⊆Υ and Υ′⊆S. Then:

(1) If A∈E then A′∈E.
(2) If A′∈ES,R+ then A∈ES′,R+, where S′ is any set containing ϒ and S.

Proof

To see the first item, note that since E is a complete extension, we only have to show that E defends A′. Suppose then that B=Γ⇒ψ∈ArgL(S) R-attacks A′ where R∈R. We show thatB∈E+.

If R is a direct prem-attack or (Compact) Undercut, then B also attacks A, and so B∈E+.
In the other cases (Defeat, Compact Defeat, Canonical Undercut) ψ⇒¬⋀Υ′ is derivable. Since L is ¬∧-expanding, ψ⇒¬⋀Υ is derivable. By Remark 3.2, B′=Γ⇒¬⋀Υ∈ArgL(S). Clearly, B′ R-attacks A and so B′∈E+. However, since B′ has the same premise set as B, also B∈E+.

For the second item, let B=Γ⇒ψ be an argument in E that R-attacks A′ for some R∈R. Again, we consider two cases.

If R is a direct prem-attack or (Compact) Undercut, clearly B R-attacks A.
Let R be Defeat, Compact Defeat or Canonical Undercut. Then ψ⇒¬⋀Υ′ is derivable, and since L is ¬∧-expanding also ψ⇒¬⋀Υ is derivable. By Remark 3.2, B′=Γ⇒¬⋀Υ∈ArgL(S). Clearly, B′ R-attacks A. By Item 1, B′∈E.

In both cases there is an argument in E that R-attacks A, and so A∈ES′,R+.

The main lemma for Propositions A.2 and A.3 is the following:

Lemma A.9

Let L be a uniform, consistency-enforcing, and ¬∧-expanding logic, and let R be a set of prem-attack rules. If S1 is irrelevant to S2, then:

(1) If E∈Cmpl(AFL(S1∪S2)) then ES1,R+=(E∩ArgL(S))S1,R+.
(2) If E∈Cmpl(AFL(S1∪S2)) then E∩ArgL(S1)∈Cmpl(AFL(S1)).
(3) If E∈Cmpl(AFL(S1)) then E∈Adm(AFL(S1∪S2)).
(4) If E∈Prf(AFL(S1∪S2)) then E∩ArgL(S1)∈Prf(AFL(S1)).
(5) If E∈Stbl(AFL(S1∪S2)) then E∩ArgL(S1)∈Stbl(AFL(S1)).
(6) If E∈Cmpl(AFL(S1)) there is E′∈Cmpl(AFL(S1∪S2)) such that E⊆E′.
(7) If E∈Prf(AFL(S1)) there is E′∈Prf(AFL(S1∪S2)) such that E⊆E′.
(8) If Grnd(AFL(S1))={E} and Grnd(AFL(S1∪S2))={E′} then E⊆E′.

Proof

Let L, R, S1 and S2 be as in the lemma.

Item 1: Obviously, (E∩ArgL(S1))S1,R+⊆ES1,R+. For the converse, let B∈ArgL(S1) be an argument in ES1,R+. Then there is an argument A=Υ⇒ψ∈E that R-attacks B. By Lemma A.6 (which is applicable here, since by Corollary A.5, E∩ArgL⊥(S1∪S2))=∅), there is an argument A′=Υ∩S1⇒ψ′ such that A′ R-attacks B. By Lemma A.8(1), A′∈E, and so B∈(E∩ArgL(S1))S1,R+.

Item 2: Let E∈Cmpl(AFL(S1∪S2)). In particular, E and all its subsets are conflict-free, thus E∩ArgL(S1) is conflict-free. To see that E∩ArgL(S1) is admissible, suppose that A∈ArgL(S1) attacks some B∈E∩ArgL(S1). Then, since E is complete in AFL(S1∪S2), A∈ES1∪S2,R+ and hence A∈ES1,R+. By Item 1, A∈(E∩ArgL(S1))S1,R+. Thus E∩ArgL(S1) indeed defends itself. It remains to show that E∩ArgL(S1) defends exactly itself. For this, suppose that E∩ArgL(S1) defends some A∈ArgL(S1). Assume for a contradiction that A∉E∩ArgL(S1) and hence A∉E. Since E is complete, E does not defend A. Hence, there is an argument B=Υ⇒ψ∈ArgL(S1∪S2) such that B R-attacks A and B∉ES1∪S2,R+. Suppose first that B∈ArgL⊥(S1∪S2). Since L is consistency-enforcing, there is an argument C=⇒ϕ that attacks B. Since C∈ArgL∅(S1∪S2)⊆Root(AFL(S1∪S2))⊆E we have thatC∈E, which is a contradiction to our assumption that B∉ES1∪S2,R+. Hence, B∈ArgL(S1∪S2)−ArgL⊥(S1∪S2). By Lemma A.6 (which again is applicable here, since by Corollary A.5, E⊆ArgL(S1∪S2)−ArgL⊥(S1∪S2)), there is a B1=Υ∩S1⇒ψ′∈ArgL(S1) that R-attacks A. Hence, since E∩ArgL(S1) defends A, B1∈(E∩ArgL(S1))S1,R+⊆(E∩ArgL(S1))S1∪S2,R+. But then by Lemma A.8(2), also B∈(E∩ArgL(S1))S1∪S2,R+ and thus B∈ES1∪S2,R+ – a contradiction.

Item 3: Obviously E is conflict-free in ⟨ArgL(S1∪S2),R⟩, since it is conflict-free in ⟨ArgL(S1),R⟩. Suppose that A=Υ⇒ψ∈ArgL(S1∪S2)R-attacks some B∈E. If A∈ArgL⊥(S1∪S2) then by Equation (A1) in the proof of Corollary A.5, A∈Root(⟨ArgL(S1),R⟩)+ and soA∈ES1,R+ (since E is complete AFL(S1)). Suppose now A∉ArgL⊥(S1∪S2). Thus, by Lemma A.6, there is an argumentA1=Υ∩S1⇒ψ′∈ArgL(S1) such that A1 R-attacks B. Since E is admissible in AFL(S1), A1∈ES1,R+. Thus, by Lemma A.8(2), alsoA∈ES1∪S2,R+. Hence, E∈Adm(AFL(S1∪S2)).

Item 4: Suppose for a contradiction that E∩ArgL(S1)∉Prf(AFL(S1)). Then there is a set E′⊋E∩ArgL(S1) which is complete in AFL(S1). Let E″=E′∪E. Since E∈Prf(AFL(S1∪S2)) and E⊊E″, E″ is not admissible in AFL(S1∪S2). Thus, either E″ is not conflict-free or E″ is not defended. Assume first that E″ is not conflict-free. Hence, either there is some A∈E′ that attacks some B∈E, or there is some C∈E that attacks some D∈E′. Suppose the first case. Since E is defends itself, there is a B′∈E that attacks A and hence we're in the second case. Note that by Corollary A.5, C∉ArgL⊥(S1∪S2) since E is complete. Thus, by Item 1, there is an argumentC1∈E∩ArgL(S1) that attacks D. But this means that E′ is not conflict-free – a contradiction. We have thus established that E″ is conflict-free. Hence, E″ is not defended. However, since by Item 3, E′∈Adm(AF(S1∪S2)), and since E∈Adm(AF(S1∪S2)) and E″ is conflict-free, it is easy to see that E″ is defended – a contradiction. Thus, we have established that E∩ArgL(S1) is maximally admissible in ArgL(S1), which means that E∩ArgL(S1)∈Prt(AFL(S1)).

Item 5: Let A∈ArgL(S1). Since E is stable in AFL(S1∪S2), it is also complete and E∪ES1∪S2,R+=ArgL(S1∪S2). Hence, either A∈E, which implies that A∈E∩ArgL(S1) (since A∈ArgL(S1)), or A∈ES1∪S2,R+, which implies that A∈ES1+ (by the definition of ES1+ and again sinceA∈ArgL(S1)). In the latter case, by Item 1, A∈(E∩ArgL(S1))S1,R+. Since A is arbitrary in ArgL(S1) this shows that (E∩ArgL(S1))∪(E∩ArgL(S1))S1,R+=ArgL(S1). By Item 2, E∩ArgL(S1) is complete in AFL(S1). Thus, E∩ArgL(S1) is stable in AFL(S1).

Item 6: Let E∈Cmpl(AFL(S1)). By Item 3, E∈Adm(AFL(S1∪S2)). The rest follows by the fact that if E∈Adm(AFL(S1∪S2)) then there is a E′∈Cmpl(AFL(S1∪S2)) such that E⊆E′.

Item 7: Since E is in particular complete in ⟨ArgL(S1),R⟩, by Item 6 there is an extension E′∈Cmpl(AFL(S1∪S2)) for which E⊆E′. The rest follows immediately by the fact that each complete extension is included in some preferred extension of the same framework.

Item 8: By Item 2, E′∩ArgL(S1) is complete in AFL(S1), and thus E⊆E′∩ArgL(S1)⊆E′.

Now we can turn to the proofs of the main results of this Appendix:

Proof of Proposition A.2.

Suppose that S1|∼L,R,Sem∀ψ, and let E be an extension in Sem(AFL(S1∪S2)). First, we treat grounded semantics. By our assumption, there is an argument Γ⇒ψ in the grounded extension of AFL(S1). Thus, by Lemma A.9(8), Γ⇒ψ is in the grounded extension of AFL(S1∪S2), that is, in E. Thus S1,S2|∼L,R,Sem∀ψ. Suppose now that the semantics is either complete, preferred or stable. Again, by our assumption, there is an argument of the form Γ⇒ψ in every element of Sem(AFL(S1)). By Lemma A.9, E∩ArgL(S1)∈Sem(AFL(S1)), and so there is a sequent of the form Γ⇒ψ in E∩ArgL(S1). In particular, E contains a sequent of the form Γ⇒ψ, and so S1,S2|∼L,R,Sem∀ψ.

Proof of Proposition A.3.

Suppose that S1|∼L,R,Sem∃ψ. Hence, there is some extension E in Sem(AFL(S1)) that contains a sequent of the form Γ⇒ψ for some Γ⊆S1. By Lemma A.9, there is an extension E′ in Sem(AFL(S1∪S2)) that contains the extension E. Thus, Γ⇒ψ is in E′, and so S1,S2|∼L,R,Sem∃ψ.

Corollary A.10

Let L=⟨L,⊢⟩ be a uniform, ¬∧-expanding and consistency-enforcing logic, and let R be a set of prem-attacking rules.

|∼L,R,Sem∀ is crash resistant when Sem is a complete, grounded, preferred or stable semantics.
|∼L,R,Sem∃ψ is crash resistant when Sem a complete, grounded or preferred semantics.

The proof of Item 1 (respectively, of Item 2) is similar to that of Proposition 5.18, using Proposition A.2 (respectively, Proposition A.3) instead of Proposition 5.14.