Sequent-based logical argumentation

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 $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ 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 Dung, 1995

An argumentation framework is a pair $\mathcal{AF}=⟨\mathit{Args}\mathrm{,}\mathcal{A}⟩$ , where Args is an enumerable set of elements, called arguments, and $\mathcal{A}$ is a relation on $\mathit{Args}\times \mathit{Args}$ whose instances are called attacks.

Definition 2.2 Besnard & Hunter, 2001, 2009

Let $\mathcal{L}$ be a standard propositional language, $\mathcal{S}$ an enumerable set of formulas in $\mathcal{L}$ , and ${⊢}_{\mathit{cl}}$ the consequence relation of classical logic (for $\mathcal{L}$ ). An argument in the sense of Besnard and Hunter (BH-argument, for short), formed by $\mathcal{S}$ , is a pair $\mathit{A}=⟨\mathrm{\Gamma }\mathrm{,}\mathit{\psi }⟩$ , where ψ is a formula in $\mathcal{L}$ and Γ is a minimally consistent subset of $\mathcal{S}$ (where minimisation is with respect to set inclusion), such that $\mathrm{\Gamma }{⊢}_{\mathit{cl}}\mathit{\psi }$ . 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 ${\mathit{A}}_1=⟨{\mathrm{\Gamma }}_1\mathrm{,}{\mathit{\psi }}_1⟩$ and ${\mathit{A}}_2=⟨{\mathrm{\Gamma }}_2\mathrm{,}{\mathit{\psi }}_2⟩$ be two BH-arguments.

${\mathit{A}}_1$ is a defeater of ${\mathit{A}}_2$ if ${\mathit{\psi }}_1{⊢}_{\mathit{cl}}\neg {\bigwedge }_{\mathit{\gamma }\in {\mathrm{\Gamma }}_2}\mathit{\gamma }$ .

${\mathit{A}}_1$ is a direct defeater of ${\mathit{A}}_2$ if there is $\mathit{\gamma }\in {\mathrm{\Gamma }}_2$ such that ${\mathit{\psi }}_1{⊢}_{\mathit{cl}}\neg \mathit{\gamma }$ .

${\mathit{A}}_1$ is an undercut of ${\mathit{A}}_2$ if there is ${\mathrm{\Gamma }}_2^{\prime }\subseteq {\mathrm{\Gamma }}_2$ such that ${\mathit{\psi }}_1{⊢}_{\mathit{cl}}\neg {\bigwedge }_{\mathit{\gamma }\in {\mathrm{\Gamma }}_2^{\prime }}\mathit{\gamma }$ and $\neg {\bigwedge }_{\mathit{\gamma }\in {\mathrm{\Gamma }}_2^{\prime }}\mathit{\gamma }{⊢}_{\mathit{cl}}{\mathit{\psi }}_1$ .

${\mathit{A}}_1$ is a direct undercut of ${\mathit{A}}_2$ if there is $\mathit{\gamma }\in {\mathrm{\Gamma }}_2$ s.t. ${\mathit{\psi }}_1{⊢}_{\mathit{cl}}\neg \mathit{\gamma }$ and $\neg \mathit{\gamma }{⊢}_{\mathit{cl}}{\mathit{\psi }}_1$ .

${\mathit{A}}_1$ is a canonical undercut of ${\mathit{A}}_2$ if ${\mathit{\psi }}_1{⊢}_{\mathit{cl}}\neg {\bigwedge }_{\mathit{\gamma }\in {\mathrm{\Gamma }}_2}\mathit{\gamma }$ and $\neg {\bigwedge }_{\mathit{\gamma }\in {\mathrm{\Gamma }}_2}\mathit{\gamma }{⊢}_{\mathit{cl}}{\mathit{\psi }}_1$ .

${\mathit{A}}_1$ is a rebuttal of ${\mathit{A}}_2$ if ${\mathit{\psi }}_1{⊢}_{\mathit{cl}}\neg {\mathit{\psi }}_2$ and $\neg {\mathit{\psi }}_2{⊢}_{\mathit{cl}}{\mathit{\psi }}_1$ .

${\mathit{A}}_1$ is a defeating rebuttal of ${\mathit{A}}_2$ if ${\mathit{\psi }}_1{⊢}_{\mathit{cl}}\neg {\mathit{\psi }}_2$ .

Example 2.4

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

Definition 2.5

Let ${\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ be the (countably infinite) set of BH-arguments formed by $\mathcal{S}$ , and let $\mathcal{A}$ be a binary relation on ${\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ , obtained by at least one of the conditions described in Definition 2.3. Then the pair $\mathcal{AF}\mathrm{(}\mathcal{S}\mathrm{)}=⟨{\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{,}\mathcal{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 $\mathit{A}=⟨\{\mathit{p}\mathrm{,}\mathit{q}\}\mathrm{,}\mathit{p}\vee \mathit{q}⟩$ are excluded since their supports are not minimal, although one may consider $\{\mathit{p}\mathrm{,}\mathit{q}\}$ a stronger support for $\mathit{p}\vee \mathit{q}$ than, say, $\{\mathit{p}\}$ , since the set $\{\mathit{p}\mathrm{,}\mathit{q}\}$ logically implies every minimal support of $\mathit{p}\vee \mathit{q}$ . Moreover, the size of $\{\mathit{p}\mathrm{,}\mathit{q}\}$ is bigger than that of $\{\mathit{p}\}$ , and this may be relevant when quantitative considerations are involved (see Section 4.4). ¹

1

Clearly, the argument A may be split into two BH-arguments, ${\mathit{A}}_1=⟨\{\mathit{p}\}\mathrm{,}\mathit{p}\vee \mathit{q}⟩$ and ${\mathit{A}}_2=⟨\{\mathit{q}\}\mathrm{,}\mathit{p}\vee \mathit{q}⟩$ , but in general such rewriting requires further processing and might cause a blowup in the number of arguments.

^{, 2}

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 ${\mathit{S}}_1=\{{\mathit{p}}_1\}$ and ${\mathit{S}}_2=\{{\mathit{p}}_2\wedge \dots \wedge {\mathit{p}}_{\mathit{n}}\}$ , supporting (e.g. in classical logic) the claim ${\mathit{p}}_1\vee \dots \vee {\mathit{p}}_{\mathit{n}}$ , 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 ${\mathit{S}}_2$ becomes more exposed to attacks than ${\mathit{S}}_1$ .

Consistency. The requirement that the support set Γ of an argument $⟨\mathrm{\Gamma }\mathrm{,}\mathit{\psi }⟩$ 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 $\{\neg \mathrm{,}\vee \mathrm{,}\wedge \}$ 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:

Supports and consequents of arguments are solely determined by the logic.

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 $\mathcal{L}$ an arbitrary propositional language having a countably infinite set $\mathsf{Atoms}\mathrm{(}\mathcal{L}\mathrm{)}$ of atomic formulas. In what follows $\mathcal{T}\mathrm{,}\mathcal{S}$ (possibly primed or indexed) denote arbitrary theories (sets of formulas) in $\mathcal{L}$ , and $\mathrm{\Gamma }\mathrm{,}\mathrm{\Delta }$ (possibly primed or indexed) denote finite theories in $\mathcal{L}$ . Given a language $\mathcal{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 $\mathcal{L}$ is a pair $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ , where ⊢ is a (Tarskian) consequence relation for $\mathcal{L}$ , that is, a binary relation between sets of formulas and formulas in $\mathcal{L}$ , satisfying the following conditions:

Reflexivity: $\text{if}\mathit{\psi }\in \mathcal{T}\text{then}\mathcal{T}⊢\mathit{\psi }$

Monotonicity: $\text{if}\mathcal{T}⊢\mathit{\psi }\text{and}\mathcal{T}\subseteq {\mathcal{T}}^{\prime }\text{then}{\mathcal{T}}^{\prime }⊢\mathit{\psi }$

Transitivity: $\text{if}\mathcal{T}⊢\mathit{\psi }\text{and}{\mathcal{T}}^{\prime }\mathrm{,}\mathit{\psi }⊢\mathit{\varphi }\text{then}\mathcal{T}\mathrm{,}{\mathcal{T}}^{\prime }⊢\mathit{\varphi }$

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

In what follows we assume that $\mathcal{L}$ contains the following connectives:

A unary connective ¬ which is a ⊢-negation: for every atomic formula p of $\mathcal{L}$ it holds that $\mathit{p}⊬\neg \mathit{p}$ and $\neg \mathit{p}⊬\mathit{p}$ ,

A binary connective ∧ which is a ⊢-conjunction: for every set $\mathcal{T}$ of formulas and formulas $\mathit{\psi }\mathrm{,}\mathit{\varphi }$ it holds that $\mathcal{T}⊢\mathit{\psi }\wedge \mathit{\varphi }$ iff $\mathcal{T}⊢\mathit{\psi }$ and $\mathcal{T}⊢\mathit{\varphi }$ .

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

3

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

• A binary connective ⊃ is called a ⊢-deductive implication if for every set $\mathcal{T}$ of formulas and formulas $\mathit{\psi }\mathrm{,}\mathit{\varphi }$ it holds that $\mathcal{T}\mathrm{,}\mathit{\psi }⊢\mathit{\varphi }$ iff $\mathcal{T}⊢\mathit{\psi }\supset \mathit{\varphi }$ .

We shall denote by $\bigwedge \mathrm{\Gamma }$ the conjunction of all the formulas in (the finite theory) Γ, and abbreviate the formula $\mathrm{(}\mathit{\psi }\supset \mathit{\varphi }\mathrm{)}\wedge \mathrm{(}\mathit{\varphi }\supset \mathit{\psi }\mathrm{)}$ by $\mathit{\psi }\leftrightarrow \mathit{\varphi }$ .

Definition 3.2

Let $\mathcal{L}$ be a propositional language, and let ⇒ be a symbol that does not appear in $\mathcal{L}$ . An $\mathcal{L}$ -sequent (or just a sequent) is an expression of the form $\mathrm{\Gamma }\Rightarrow \mathrm{\Delta }$ , where Γ and Δ are finite sets of formulas in $\mathcal{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 $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ , then, there is an effective way of drawing entailments: $\mathcal{T}⊢\mathit{\psi }$ iff for some finite subset $\mathrm{\Gamma }\subseteq \mathcal{T}$ there is a proof of the sequent $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ in the corresponding sequent calculus.

Definition 3.3

Let $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ be a logic with a corresponding sequent calculus $\mathsf{C}$ , and let $\mathcal{S}$ be a set of formulas in $\mathcal{L}$ . An $\mathsf{L}$ -argument based on $\mathcal{S}$ is an $\mathsf{L}$ -sequent of the form $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ , where $\mathrm{\Gamma }\subseteq \mathcal{S}$ , ⁴

4

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

that is provable in $\mathsf{C}$ . ⁵

5

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

We denote by ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ the set of all the $\mathsf{L}$ -arguments that are based on $\mathcal{S}$ .

In the notation of Definition 3.3, we have that:

Proposition 3.4

Let $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ be a propositional logic. Then $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ is in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ iff $\mathrm{\Gamma }⊢\mathit{\psi }$ for a finite $\mathrm{\Gamma }\subseteq \mathcal{S}$ .

Example 3.5

Consider Gentzen's sequent calculus LK (Figure 1), which is sound and complete for classical logic $\mathsf{CL}$ . In this case we have, for instance, that the sequent $\mathit{\psi }\supset \mathit{\varphi }\Rightarrow \neg \mathit{\psi }\vee \mathit{\varphi }$ is derivable in LK and so it belongs to ${\mathsf{Arg}}_{\mathsf{CL}}\mathrm{(}\mathcal{S}\mathrm{)}$ whenever $\mathcal{S}$ contains the formula $\mathit{\psi }\supset \mathit{\varphi }$ . Note, however, that this sequent is not derivable by any sequent calculus that is sound and complete for intuitionistic logic $\mathsf{IL}$ (e.g. Gentzen's LJ), thus it is not in ${\mathsf{Arg}}_{\mathsf{IL}}\mathrm{(}\mathcal{S}\mathrm{)}$ for any $\mathcal{S}$ .

Figure 1.

The proof system LK.

Proposition 3.6

For every logic $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ and a set $\mathcal{S}$ of formulas in $\mathcal{L}\mathrm{,}$ the set ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ is closed under the following rules: ⁶

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 $\{\mathit{\psi }\}$ ).

$\mathcal{S}$ -Reflexivity: For every finite $\mathrm{\Gamma }\subseteq \mathcal{S}$ and $\mathit{\psi }\in \mathrm{\Gamma }$ it holds that $\mathrm{\Gamma }\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$

$\mathcal{S}$ -Monotonicity: If $\mathrm{\Gamma }\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ and $\mathrm{\Gamma }\subseteq {\mathrm{\Gamma }}^{\prime }\subseteq \mathcal{S}\mathrm{,}$ then ${\mathrm{\Gamma }}^{\prime }\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$

$\mathcal{S}$ -Transitivity: If $\mathrm{\Gamma }\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ and ${\mathrm{\Gamma }}^{\prime }\mathrm{,}\mathit{\psi }\Rightarrow \mathit{\varphi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{,}$ then also $\mathrm{\Gamma }\mathrm{,}{\mathrm{\Gamma }}^{\prime }\Rightarrow \mathit{\varphi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$

Proof

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

Remark 3.1

The set ${\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ of the BH-arguments is not closed under any rule in Proposition 3.6. To see this consider for instance the set $\mathcal{S}=\{\mathit{p}\mathrm{,}\mathit{q}\mathrm{,}\neg \mathit{p}\vee \mathit{q}\mathrm{,}\neg \mathit{q}\vee \mathit{p}\}$ . Then $⟨\{\mathit{p}\mathrm{,}\neg \mathit{p}\vee \mathit{q}\}\mathrm{,}\mathit{q}⟩\in {\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ and $⟨\{\mathit{q}\mathrm{,}\neg \mathit{q}\vee \mathit{p}\}\mathrm{,}\mathit{p}⟩\in {\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ , however $⟨\{\mathit{p}\mathrm{,}\neg \mathit{p}\vee \mathit{q}\mathrm{,}\neg \mathit{q}\vee \mathit{p}\}\mathrm{,}\mathit{p}⟩\notin {\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ , since its support set is not minimal. Thus ${\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ is not $\mathcal{S}$ -transitive. The fact that $⟨\{\mathit{p}\mathrm{,}\neg \mathit{p}\vee \mathit{q}\mathrm{,}\neg \mathit{q}\vee \mathit{p}\}\mathrm{,}\mathit{p}⟩\notin {\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ (while $⟨\{\mathit{p}\}\mathrm{,}\mathit{p}⟩\in {\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ ) also shows that ${\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ is not $\mathcal{S}$ -monotonic and that it is not $\mathcal{S}$ -reflexive. ⁷

7

Note that ${\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ is cautiously $\mathcal{S}$ -reflexive: $⟨\{\mathit{\psi }\}\mathrm{,}\mathit{\psi }⟩\in {\mathit{Args}}_{\mathsf{BH}}\mathrm{(}\mathcal{S}\mathrm{)}$ for a consistent formula $\mathit{\psi }\in \mathcal{S}$ .

Remark 3.2

Let $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ be a logic and $\mathcal{S}$ a set of formulas in $\mathcal{L}$ . Then $\mathcal{S}$ -Transitivity can be strengthened as follows:

If $\mathrm{\Gamma }\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ and ${\mathrm{\Gamma }}^{\prime }\mathrm{,}\mathit{\psi }⊢\mathit{\varphi }$ for a finite ${\mathrm{\Gamma }}^{\prime }\subseteq \mathcal{S}$ , then $\mathrm{\Gamma }\mathrm{,}{\mathrm{\Gamma }}^{\prime }\Rightarrow \mathit{\varphi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ .

Note that unlike $\mathcal{S}$ -Transitivity, in the rule above ψ may not belong to $\mathcal{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 $\mathrm{\Gamma }\nRightarrow \mathit{\psi }$ the elimination (or, the discharging) of the argument $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ . Alternatively, if a sequent is denoted by s, its discharged counterpart will sometimes be denoted by $\bar{\mathit{s}}$ .

Definition 4.1

Let ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ be a set of $\mathsf{L}$ -arguments, $\mathsf{C}$ a sound and complete sequent calculus for $\mathsf{L}$ . A sequent elimination rule (or attack rule) is a Gentzen-type rule $\mathcal{R}$ of the following form: $${\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow {\mathrm{\Delta }}_1\mathrm{,}\dots \mathrm{,}{\mathrm{\Gamma }}_{\mathit{n}}\Rightarrow {\mathrm{\Delta }}_{\mathit{n}}}{{\mathrm{\Gamma }}_{\mathit{n}}\nRightarrow {\mathrm{\Delta }}_{\mathit{n}}}}.$$ We say that $\mathcal{R}$ is ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ -applicable, alternatively: $\mathsf{L}$ -applicable or just applicable (with respect to θ), if there is an $\mathcal{L}$ -substitution θ such that $\mathit{\theta }\mathrm{(}{\mathrm{\Gamma }}_1\mathrm{)}\Rightarrow \mathit{\theta }\mathrm{(}{\mathrm{\Delta }}_1\mathrm{)}$ and $\mathit{\theta }\mathrm{(}{\mathrm{\Gamma }}_{\mathit{n}}\mathrm{)}\Rightarrow \mathit{\theta }\mathrm{(}{\mathrm{\Delta }}_{\mathit{n}}\mathrm{)}$ are in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ and for each $1\mathrm{<}\mathit{i}\mathrm{<}\mathit{n}$ , $\mathit{\theta }\mathrm{(}{\mathrm{\Gamma }}_{\mathit{i}}\mathrm{)}\Rightarrow \mathit{\theta }\mathrm{(}{\mathrm{\Delta }}_{\mathit{i}}\mathrm{)}$ is $\mathsf{C}$ -provable. In this case we shall say that $\mathit{\theta }\mathrm{(}{\mathrm{\Gamma }}_1\mathrm{)}\Rightarrow \mathit{\theta }\mathrm{(}{\mathrm{\Delta }}_1\mathrm{)}$ $\mathcal{R}$ -attacks $\mathit{\theta }\mathrm{(}{\mathrm{\Gamma }}_{\mathit{n}}\mathrm{)}\Rightarrow \mathit{\theta }\mathrm{(}{\mathrm{\Delta }}_{\mathit{n}}\mathrm{)}$ .

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 $\mathsf{C}$ , as long as $\mathsf{C}$ is sound and complete for $\mathsf{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 $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ and $\mathsf{L}$ -arguments in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ , an argument ${\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1$ is an $\mathsf{L}$ -defeater of an argument ${\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2$ if ${\mathit{\psi }}_1⊢\neg \bigwedge {\mathrm{\Gamma }}_2$ . In the presence of a ⊢-deductive implication ⊃ in $\mathcal{L}$ , this means that $⊢{\mathit{\psi }}_1\supset \neg \bigwedge {\mathrm{\Gamma }}_2$ , and so $\Rightarrow {\mathit{\psi }}_1\supset \neg \bigwedge {\mathrm{\Gamma }}_2$ is an $\mathsf{L}$ -argument in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ . It follows that attacks by defeaters may be represented by the following sequent elimination rule (relative to $\mathsf{L}$ ): $$\text{Defeat:}{\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1\Rightarrow {\mathit{\psi }}_1\supset \neg \bigwedge {\mathrm{\Gamma }}_2{\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\nRightarrow {\mathit{\psi }}_2}}.$$

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

Proposition 4.2

Let ${\mathit{A}}_1=⟨{\mathrm{{\rm Y}}}_1\mathrm{,}{\mathit{\sigma }}_1⟩$ and ${\mathit{A}}_2=⟨{\mathrm{{\rm Y}}}_2\mathrm{,}{\mathit{\sigma }}_2⟩$ be two BH-arguments. Then ${\mathit{A}}_1$ is a defeater of ${\mathit{A}}_2$ in the sense of Definition 2.3 iff the rule Defeat defined above is $\mathsf{CL}$ -applicable with respect to a substitution θ, where $\mathit{\theta }\mathrm{(}{\mathrm{\Gamma }}_{\mathit{i}}\mathrm{)}={\mathrm{{\rm Y}}}_{\mathit{i}}$ and $\mathit{\theta }\mathrm{(}{\mathit{\psi }}_{\mathit{i}}\mathrm{)}={\mathit{\sigma }}_{\mathit{i}}\mathrm{,}$ $\mathit{i}=1\mathrm{,}2$ .

Proof

Since ${\mathit{A}}_{\mathit{i}}$ are BH-arguments it holds that ${\mathrm{{\rm Y}}}_{\mathit{i}}{⊢}_{\mathit{cl}}{\mathit{\sigma }}_{\mathit{i}}$ for $\mathit{i}=1\mathrm{,}2$ and so the sequents ${\mathrm{{\rm Y}}}_{\mathit{i}}\Rightarrow {\mathit{\sigma }}_{\mathit{i}}$ are LK-provable ( $\mathit{i}=1\mathrm{,}2$ ). Moreover, since ${\mathit{A}}_1$ is a defeater of ${\mathit{A}}_2$ , it holds that ${⊢}_{\mathit{cl}}{\mathit{\sigma }}_1\supset \neg \bigwedge {\mathrm{{\rm Y}}}_2$ , thus $\Rightarrow {\mathit{\sigma }}_1\supset \neg \bigwedge {\mathrm{{\rm Y}}}_2$ is also LK-provable. It follows that the rule Defeat is $\mathsf{CL}$ -applicable with respect to a substitution θ such that $\mathit{\theta }\mathrm{(}{\mathrm{\Gamma }}_{\mathit{i}}\mathrm{)}={\mathrm{{\rm Y}}}_{\mathit{i}}$ and $\mathit{\theta }\mathrm{(}{\mathit{\psi }}_{\mathit{i}}\mathrm{)}={\mathit{\sigma }}_{\mathit{i}}$ ( $\mathit{i}=1\mathrm{,}2$ ). Conversely, let ${\mathit{A}}_1=⟨{\mathrm{{\rm Y}}}_1\mathrm{,}{\mathit{\sigma }}_1⟩$ and ${\mathit{A}}_2=⟨{\mathrm{{\rm Y}}}_2\mathrm{,}{\mathit{\sigma }}_2⟩$ be BH-arguments and suppose that the rule Defeat is $\mathsf{CL}$ -applicable with respect to a substitution θ such that $\mathit{\theta }\mathrm{(}{\mathrm{\Gamma }}_{\mathit{i}}\mathrm{)}={\mathrm{{\rm Y}}}_{\mathit{i}}$ and $\mathit{\theta }\mathrm{(}{\mathit{\psi }}_{\mathit{i}}\mathrm{)}={\mathit{\sigma }}_{\mathit{i}}$ ( $\mathit{i}=1\mathrm{,}2$ ). Then the attacking condition of this rule is LK-provable, which means that ${\mathit{\sigma }}_1{⊢}_{\mathit{cl}}\neg \bigwedge {\mathrm{{\rm Y}}}_2$ , and so ${\mathit{A}}_1$ is a defeater of ${\mathit{A}}_2$ 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. $$\text{Compact Defeat:}{\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow \neg \bigwedge {\mathrm{\Gamma }}_2{\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\nRightarrow {\mathit{\psi }}_2}}$$

Definition 4.3

We say that an attack rule ${\mathcal{R}}_1$ $\mathsf{L}$ -implies an attack rule ${\mathcal{R}}_2$ , if for every set of formulas $\mathcal{S}$ , whenever ${\mathcal{R}}_2$ is ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ -applicable its conclusion is produced by ${\mathcal{R}}_1$ (with respect to ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ ). Formally: whenever $\mathrm{\Gamma }\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ ${\mathcal{R}}_2$ -attacks ${\mathrm{\Gamma }}^{\prime }\Rightarrow {\mathit{\psi }}^{\prime }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ there is $\mathrm{\Gamma }\Rightarrow \mathit{\varphi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ that ${\mathcal{R}}_1$ -attacks ${\mathrm{\Gamma }}^{\prime }\Rightarrow {\mathit{\psi }}^{\prime }$ . ⁸

8

Gorogiannis & Hunter (2011) consider a stricter implication between attacks, in which $\mathit{\varphi }=\mathit{\psi }$ .

The Attack rules ${\mathcal{R}}_1$ and ${\mathcal{R}}_2$ are said to be $\mathsf{L}$ -equivalent, if each one of them $\mathsf{L}$ -implies the other.

From an argumentative point of view, the fact that a rule ${\mathcal{R}}_1$ implies a rule ${\mathcal{R}}_2$ intuitively means that any attack that is producible using ${\mathcal{R}}_2$ can be reproduced using ${\mathcal{R}}_1$ by means of an attacking argument with the same support set.

Proposition 4.4

For every logic $\mathsf{L}\mathrm{,}$ Compact Defeat is $\mathsf{L}$ -equivalent to Defeat.

Proof

To show that Compact Defeat implies Defeat assume that the three conditions of Defeat hold with respect to ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ . Since $\Rightarrow {\mathit{\psi }}_1\supset \neg \bigwedge {\mathrm{\Gamma }}_2$ is derivable, it holds that $⊢{\mathit{\psi }}_1\supset \neg \bigwedge {\mathrm{\Gamma }}_2$ . Thus, since ⊃ is a ⊢-deductive implication, ${\mathit{\psi }}_1\supset \neg \bigwedge {\mathrm{\Gamma }}_2$ . This, together with the assumption that ${\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1$ is derivable (and so it is an argument in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ ), imply by Remark 3.2 that ${\mathrm{\Gamma }}_1\Rightarrow \neg \bigwedge {\mathrm{\Gamma }}_2$ is an argument in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ , and so by Definition 3.3 it is derivable in the underlying sequent calculus. It follows that ${\mathrm{\Gamma }}_2\nRightarrow {\mathit{\psi }}_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, $\neg \bigwedge {\mathrm{\Gamma }}_2⊢\neg \bigwedge {\mathrm{\Gamma }}_2$ , and so, since ⊃ is a ⊢-deductive implication, $⊢\neg \bigwedge {\mathrm{\Gamma }}_2\supset \neg \bigwedge {\mathrm{\Gamma }}_2$ . We thus have that the sequent $\Rightarrow \neg \bigwedge {\mathrm{\Gamma }}_2\supset \neg \bigwedge {\mathrm{\Gamma }}_2$ is derivable in the underlying sequent calculus. It follows that ${\mathrm{\Gamma }}_2\nRightarrow {\mathit{\psi }}_2$ is producible by Defeat, and so Defeat indeed implies Compact Defeat.

Attacks by direct defeaters. Direct defeat with respect to an arbitrary logic $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ and a set ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ of $\mathsf{L}$ -arguments based on $\mathcal{S}$ , means that ${\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1$ is an $\mathsf{L}$ -direct defeater of ${\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2$ if ${\mathit{\psi }}_1⊢\neg \mathit{\gamma }$ for some $\mathit{\gamma }\in {\mathrm{\Gamma }}_2$ . Thus, a direct defeat attack may be expressed by the following sequent elimination rule: $$\text{Direct Defeat:}{\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1\Rightarrow {\mathit{\psi }}_1\supset \neg \mathit{\varphi }{\mathrm{\Gamma }}_2\mathrm{,}\mathit{\varphi }\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\mathrm{,}\mathit{\varphi }\nRightarrow {\mathit{\psi }}_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 ${\mathit{A}}_1=⟨{\mathrm{{\rm Y}}}_1\mathrm{,}{\mathit{\sigma }}_1⟩$ and ${\mathit{A}}_2=⟨{\mathrm{{\rm Y}}}_2\mathrm{,}{\mathit{\sigma }}_2⟩$ be two BH-arguments. Then ${\mathit{A}}_1$ is a direct defeater of ${\mathit{A}}_2$ in the sense of Definition 2.3 iff the rule Direct Defeat defined above is $\mathsf{CL}$ -applicable with respect to a substitution θ where $\mathit{\theta }\mathrm{(}{\mathrm{\Gamma }}_{\mathit{i}}\mathrm{)}={\mathrm{{\rm Y}}}_{\mathit{i}}$ and $\mathit{\theta }\mathrm{(}{\mathit{\psi }}_{\mathit{i}}\mathrm{)}={\mathit{\sigma }}_{\mathit{i}}\mathrm{,}$ $\mathit{i}=1\mathrm{,}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: $$\text{Compact Direct Defeat:}{\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow \neg \mathit{\varphi }{\mathrm{\Gamma }}_2\mathrm{,}\mathit{\varphi }\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\mathrm{,}\mathit{\varphi }\nRightarrow {\mathit{\psi }}_2}}.$$

Proposition 4.6

For every logic $\mathsf{L}\mathrm{,}$ Compact Direct Defeat is $\mathsf{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 $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ we first have to define logical equivalence in $\mathsf{L}$ . A natural way to do so is to require that ψ and φ are logically equivalent in $\mathsf{L}$ iff $\mathit{\psi }⊢\mathit{\varphi }$ and $\mathit{\varphi }⊢\mathit{\psi }$ . Using a ⊢-deductive implication ⊃ and a ⊢-conjunctive connective ∧, this means that $⊢\mathrm{(}\mathit{\psi }\supset \mathit{\varphi }\mathrm{)}\wedge \mathrm{(}\mathit{\varphi }\supset \mathit{\psi }\mathrm{)}$ , that is, that $\mathit{\psi }\leftrightarrow \mathit{\varphi }$ is a theorem of $\mathsf{L}$ . It follows that attacks by undercuts are represented by the following sequent elimination rule: $$\text{Undercut:}{\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1\Rightarrow {\mathit{\psi }}_1\leftrightarrow \neg \bigwedge {\mathrm{\Gamma }}_2^{\prime }{\mathrm{\Gamma }}_2\mathrm{,}{\mathrm{\Gamma }}_2^{\prime }\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\mathrm{,}{\mathrm{\Gamma }}_2^{\prime }\nRightarrow {\mathit{\psi }}_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: $$\text{Direct Undercut:}{\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1\Rightarrow {\mathit{\psi }}_1\leftrightarrow \neg {\mathit{\gamma }}_2{\mathrm{\Gamma }}_2\mathrm{,}{\mathit{\gamma }}_2\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\mathrm{,}{\mathit{\gamma }}_2\nRightarrow {\mathit{\psi }}_2}}.$$ Similarly, attacks by canonical undercuts may be represented as follows: $$\text{Canonical Undercut:}{\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1\Rightarrow {\mathit{\psi }}_1\leftrightarrow \neg \bigwedge {\mathrm{\Gamma }}_2{\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\nRightarrow {\mathit{\psi }}_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: $$\begin{array}{cc}\hfill \text{Rebuttal:}& {\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1\Rightarrow {\mathit{\psi }}_1\leftrightarrow \neg {\mathit{\psi }}_2{\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\nRightarrow {\mathit{\psi }}_2}}\mathrm{,}\hfill \\ \hfill \text{Defeating Rebuttal:}& {\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1\Rightarrow {\mathit{\psi }}_1\supset \neg {\mathit{\psi }}_2{\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\nRightarrow {\mathit{\psi }}_2}}.\hfill \end{array}$$

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 $\mathcal{S}$ -arguments, as the premises of these conditions are not necessarily included in $\mathcal{S}$ . ⁹

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.

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 $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ be a propositional logic, where $\mathcal{L}$ has a ⊢-conjunction ∧. Then: (a) Defeating Rebuttal is $\mathsf{L}$ -equivalent to Rebuttal, (b) Undercut $\mathsf{L}$ -implies Canonical Undercut and Direct Undercut, (c) Canonical Undercut is $\mathsf{L}$ -equivalent to Defeat, (d) Direct Defeat is $\mathsf{L}$ -equivalent to Direct Undercut.

Proof

Part (a) follows from the fact that both rules are $\mathsf{L}$ -equivalent to Compact Rebuttal. Part (b) follows from the fact that Undercut holds in particular when ${\mathrm{\Gamma }}_2$ is a singleton (in which case Direct Undercut is obtained) and when ${\mathrm{\Gamma }}_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 $\mathsf{L}$ is classical logic, Defeat implies Direct Defeat, since in LK the sequent $\Rightarrow \mathit{\psi }\supset \neg \bigwedge \mathrm{\Gamma }$ is derivable from $\Rightarrow \mathit{\psi }\supset \neg \mathit{\gamma }$ for any $\mathit{\gamma }\in \mathrm{\Gamma }$ . 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 $\mathsf{O}$ that represents obligations and the defined modal operator $\mathsf{P}$ (where $\mathsf{P}=\neg \mathsf{O}\neg$ ) 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 $\mathit{\phi }\wedge \mathit{\psi }$ . 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 $\mathit{m}\supset \mathsf{O}\neg \mathit{f}$ and $\mathrm{(}\mathit{m}\wedge \mathit{a}\mathrm{)}\supset \mathsf{O}\mathit{f}$ . Now, in case one is indeed served asparagus ( $\mathit{m}\wedge \mathit{a}$ ) we expect to derive the (unconditional) obligation to eat with fingers ( $\mathsf{O}\mathit{f}$ ) rather than to not eat with fingers ( $\mathsf{O}\neg \mathit{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 $\{\mathit{m}\wedge \mathit{a}\mathrm{,}\mathrm{(}\mathit{m}\wedge \mathit{a}\mathrm{)}\supset \mathsf{O}\mathit{f}\}\Rightarrow \mathsf{O}\mathit{f}$ attacks the argument $\{\mathit{m}\mathrm{,}\mathit{m}\supset \mathsf{O}\neg \mathit{f}\}\Rightarrow \mathsf{O}\neg \mathit{f}$ . Here, arguments are obtained by a sequent calculus for standard deontic logic $\mathsf{SDL}$ , which extends LK by the following inference rules for the modal operators: (Below, we denote $\mathsf{O}\mathrm{\Gamma }$ for $\{\mathsf{O}\mathit{\varphi }\mid \mathit{\varphi }\in \mathrm{\Gamma }\}$ ) $$\text{KR:}{\displaystyle \frac{\mathrm{\Gamma }\Rightarrow \mathit{\varphi }}{\mathsf{O}\mathrm{\Gamma }\Rightarrow \mathsf{O}\mathit{\varphi }}}\text{DR:}{\displaystyle \frac{\mathrm{\Gamma }\Rightarrow \mathit{\varphi }}{\mathsf{O}\mathrm{\Gamma }\Rightarrow \neg \mathsf{O}\neg \mathit{\varphi }}}.$$ The aforesaid attack rule may be formalised as follows: $$\text{Specifity:}{\displaystyle \frac{\mathrm{\Gamma }\mathrm{,}\mathit{\varphi }\supset \mathit{\psi }\Rightarrow \mathit{\psi }\mathrm{\Gamma }\Rightarrow \mathit{\varphi }{\mathrm{\Gamma }}^{\prime }\Rightarrow {\mathit{\varphi }}^{\prime }\mathit{\varphi }\Rightarrow {\mathit{\varphi }}^{\prime }\mathit{\psi }\Rightarrow \neg {\mathit{\psi }}^{\prime }{\mathrm{\Gamma }}^{\prime }\mathrm{,}{\mathit{\varphi }}^{\prime }\supset {\mathit{\psi }}^{\prime }\Rightarrow {\mathit{\psi }}^{\prime }}{{\mathrm{\Gamma }}^{\prime }\mathrm{,}{\mathit{\varphi }}^{\prime }\supset {\mathit{\psi }}^{\prime }\nRightarrow {\mathit{\psi }}^{\prime }}}.$$ This rule aims at formalising the principle of specificity. It states that when two sequents ${\mathrm{\Gamma }}^{\prime }\Rightarrow {\mathit{\psi }}^{\prime }$ and $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ 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 $\mathit{m}\mathrm{,}\mathit{m}\supset \mathsf{O}\neg \mathit{f}\Rightarrow \mathsf{O}\neg \mathit{f}$ in light of the more specific sequent $\mathit{m}\wedge \mathit{a}\mathrm{,}\mathrm{(}\mathit{m}\wedge \mathit{a}\mathrm{)}\supset \mathsf{O}\mathit{f}\Rightarrow \mathsf{O}\mathit{f}$ .

Some variations of Specificity are given below (where ${\mathsf{NN}}^{\prime }\in \{\mathsf{OO}\mathrm{,}\mathsf{OP}\mathrm{,}\mathsf{PO}\}$ ): ¹⁰

10

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

$$\begin{array}{c}{\mathsf{NN}}^{\prime }-\mathrm{Spec}{\displaystyle \frac{\mathrm{\Gamma }\mathrm{,}\mathit{\varphi }\supset \mathsf{N}\mathit{\psi }\Rightarrow \mathsf{N}\mathit{\psi }\mathrm{\Gamma }\Rightarrow \mathit{\varphi }{\mathrm{\Gamma }}^{\prime }\Rightarrow {\mathit{\varphi }}^{\prime }\mathit{\varphi }\Rightarrow {\mathit{\varphi }}^{\prime }\mathit{\psi }\Rightarrow \neg {\mathit{\psi }}^{\prime }{\mathrm{\Gamma }}^{\prime }\mathrm{,}{\mathit{\varphi }}^{\prime }\supset {\mathsf{N}}^{\prime }{\mathit{\psi }}^{\prime }\Rightarrow {\mathsf{N}}^{\prime }{\mathit{\psi }}^{\prime }}{{\mathrm{\Gamma }}^{\prime }\mathrm{,}{\mathit{\varphi }}^{\prime }\supset {\mathsf{N}}^{\prime }{\mathit{\psi }}^{\prime }\nRightarrow {\mathsf{N}}^{\prime }{\mathit{\psi }}^{\prime }}}\mathrm{,}\hfill \\ {\mathsf{NN}}^{\prime }-\mathrm{SpecNeg}\hfill \\ {\displaystyle \frac{\mathrm{\Gamma }\mathrm{,}\mathit{\varphi }\supset \mathsf{N}\mathit{\psi }\Rightarrow \neg \mathrm{(}{\mathit{\varphi }}^{\prime }\supset {\mathsf{N}}^{\prime }{\mathit{\psi }}^{\prime }\mathrm{)}\mathrm{\Gamma }\Rightarrow \mathit{\varphi }{\mathrm{\Gamma }}^{\prime }\Rightarrow {\mathit{\varphi }}^{\prime }\mathit{\varphi }\Rightarrow {\mathit{\varphi }}^{\prime }\mathit{\psi }\Rightarrow \neg {\mathit{\psi }}^{\prime }{\mathrm{\Gamma }}^{\prime }\mathrm{,}{\mathit{\varphi }}^{\prime }\supset {\mathsf{N}}^{\prime }{\mathit{\psi }}^{\prime }\Rightarrow {\mathit{\psi }}^{\prime }}{{\mathrm{\Gamma }}^{\prime }\mathrm{,}{\mathit{\varphi }}^{\prime }\supset {\mathsf{N}}^{\prime }{\mathit{\psi }}^{\prime }\nRightarrow {\mathit{\psi }}^{\prime }}}.\hfill \end{array}$$ For instance, $\mathsf{PO}$ -Spec models permission as derogation (Stolpe, 2010): a permission may suspend a more general obligation.

4.3. Relevant attacks

When $\mathsf{L}$ is a logic in which any formula follows from a contradiction (in particular, if $\mathsf{L}$ is classical logic, $\mathsf{CL}$ ), any sequent is attacked according to each rule in Figure 2. Thus, for instance, when $\mathsf{L}=\mathsf{CL}$ , $\mathcal{S}=\{\mathit{p}\mathrm{,}\neg \mathit{p}\mathrm{,}\mathit{q}\}$ , and the attack rule is Undercut, the sequent $\mathit{q}\Rightarrow \mathit{q}$ is attacked by the (classically valid) sequent $\mathit{p}\mathrm{,}\neg \mathit{p}\Rightarrow \neg \mathit{q}$ , although – intuitively – q is not really related to the inconsistency in $\mathcal{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. $\mathit{p}\mathrm{,}\neg \mathit{p}\mathrm{,}\mathit{q}\Rightarrow \neg \mathit{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 $\mathcal{L}$ , and denote by $\mathsf{Atoms}\mathrm{(}\mathrm{\Gamma }\mathrm{)}$ the set of atomic formulas that appear in (some formula of) Γ.

Γ is relevant to ψ, if $\mathsf{Atoms}\mathrm{(}\mathrm{\Gamma }\mathrm{)}\cap \mathsf{Atoms}\mathrm{(}\{\mathit{\psi }\}\mathrm{)}=\varnothing$ implies that $\mathrm{\Gamma }=\varnothing$ . A non-empty set Γ is irrelevant to a (non-empty) set Δ if $\mathsf{Atoms}\mathrm{(}\mathrm{\Gamma }\mathrm{)}\cap \mathsf{Atoms}\mathrm{(}\mathrm{\Delta }\mathrm{)}=\varnothing$ .

Γ is a most compact support for ψ (with respect to a logic $\mathsf{L}$ and a set of assertions $\mathcal{S}$ ), if $\mathrm{\Gamma }\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ and there is no ${\mathrm{\Gamma }}^{\prime }$ with $\mathsf{Atoms}\mathrm{(}{\mathrm{\Gamma }}^{\prime }\mathrm{)}⊊\mathsf{Atoms}\mathrm{(}\mathrm{\Gamma }\mathrm{)}$ such that ${\mathrm{\Gamma }}^{\prime }\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ . ¹¹

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.

We denote by $\mathit{mcs}\mathrm{(}\mathit{\psi }\mathrm{)}$ the set of all formulas $\mathit{\sigma }\in \mathrm{{\rm Y}}$ such that ϒ is a most compact support for ψ (with respect to $\mathsf{L}$ and $\mathcal{S}$ ). ¹²

12

For instance, when $\mathsf{L}=\mathsf{CL}$ and $\mathcal{S}=\{\mathit{p}\mathrm{,}\mathit{q}\}$ , we have that $\mathit{p}\mathrm{,}\mathit{q}\in \mathit{mcs}\mathrm{(}\mathit{p}\vee \mathit{q}\mathrm{)}$ .

Let $\mathcal{R}$ be an elimination rule in Figure 2, in which ${\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1$ attacks ${\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2$ . The relevant variant of $\mathcal{R}$ is the application of $\mathcal{R}$ with the side conditions (i.e. a restriction on the application of $\mathcal{R}$ ) that ${\mathrm{\Gamma }}_1\subseteq \mathit{mcs}\mathrm{(}{\mathit{\psi }}_1\mathrm{)}$ and ${\mathrm{\Gamma }}_1$ is relevant to ${\mathrm{\Gamma }}_2$ .

Example 4.10

Relevant Undercut is defined as follows: $$[\text{R-Ucut}]{\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1{\mathit{\psi }}_1\Rightarrow \neg \bigwedge {\mathrm{\Gamma }}_2\neg \bigwedge {\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_1{\mathrm{\Gamma }}_2\mathrm{,}{\mathrm{\Gamma }}_2^{\prime }\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\mathrm{,}{\mathrm{\Gamma }}_2^{\prime }\nRightarrow {\mathit{\psi }}_2}}$$ provided that ${\mathrm{\Gamma }}_1$ is included in $\mathit{mcs}\mathrm{(}{\mathit{\psi }}_1\mathrm{)}$ and it is relevant to ${\mathrm{\Gamma }}_2$ . Thus, for instance, when $\mathsf{L}=\mathsf{CL}$ and $\mathcal{S}=\{\mathit{p}\mathrm{,}\neg \mathit{p}\mathrm{,}\mathit{q}\}$ , each one of the the sequents $\mathit{p}\mathrm{,}\mathit{q}\Rightarrow \mathrm{(}\mathit{p}\vee \neg \mathit{q}\mathrm{)}$ and $\mathit{p}\mathrm{,}\mathit{q}\Rightarrow \neg \neg \mathrm{(}\mathit{p}\vee \neg \mathit{q}\mathrm{)}$ attacks according to this rule the sequent $\neg \mathit{p}\mathrm{,}\mathit{q}\Rightarrow \neg \mathrm{(}\mathit{p}\vee \neg \mathit{q}\mathrm{)}$ . Note, however, that unlike in the case of Undercut, according to Relevant Undercut $\mathit{p}\mathrm{,}\neg \mathit{p}\Rightarrow \neg \mathit{q}$ does not attack $\mathit{q}\Rightarrow \mathit{q}$ , since $\{\mathit{p}\mathrm{,}\neg \mathit{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 ${\mathcal{S}}_1=\{\mathit{p}\mathrm{,}\mathit{p}\to \mathit{r}\mathrm{,}\mathit{p}\wedge \mathit{q}\wedge \mathit{r}\mathrm{,}\neg \mathit{r}\}$ . In this case, the sequent $\neg \mathit{r}\Rightarrow \neg \mathit{r}$ is attacked according to [R-Ucut] only by $\mathit{p}\mathrm{,}\mathit{p}\to \mathit{r}\Rightarrow \mathit{r}$ and not by $\mathit{p}\wedge \mathit{q}\wedge \mathit{r}\Rightarrow \mathit{r}$ , since the latter is not in $\mathit{mcs}\mathrm{(}\mathit{r}\mathrm{)}$ relative to ${\mathcal{S}}_1$ . Moreover, the transition from ${\mathcal{S}}_1$ to its clausal form ${\mathcal{S}}_2=\{\mathit{p}\mathrm{,}\mathit{p}\to \mathit{r}\mathrm{,}\mathit{q}\mathrm{,}\mathit{r}\mathrm{,}\neg \mathit{r}\}$ , which keeps the two sets equivalent according to classical logic, has some implications on the attack relation, since $\neg \mathit{r}\Rightarrow \neg \mathit{r}$ is now attacked according to [R-Ucut] by $\mathit{r}\Rightarrow \mathit{r}$ and not by $\mathit{p}\mathrm{,}\mathit{p}\to \mathit{r}\Rightarrow \mathit{r}$ , which in turn does not belong to $\mathit{mcs}\mathrm{(}\mathit{r}\mathrm{)}$ relative to ${\mathcal{S}}_2$ . It follows that relevant attacks are sensitive to the syntactic structure of the underlying set of assertions. ¹³

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.

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 $\mathit{p}\mathrm{,}\mathit{q}\Rightarrow \mathit{p}\vee \mathit{q}$ a stronger argument for $\mathit{p}\vee \mathit{q}$ than $\mathit{p}\Rightarrow \mathit{p}\vee \mathit{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 ${\mathrm{\Gamma }}_1\Rightarrow \mathit{\psi }$ on ${\mathrm{\Gamma }}_2\Rightarrow \neg \mathit{\psi }$ cannot stem only from the fact that $|{\mathrm{\Gamma }}_1|\mathrm{>}|{\mathrm{\Gamma }}_2|$ (where $|\mathrm{\Gamma }|$ denotes the size of Γ), since in this case the argument $\mathit{p}\mathrm{,}\mathit{p}\to \mathit{q}\Rightarrow \mathit{q}$ could be attacked by an argument like $\mathit{p}\mathrm{,}\mathit{p}\to \mathit{r}\mathrm{,}\mathit{r}\to \mathit{q}\Rightarrow \mathit{q}$ or even by $\mathit{r}\mathrm{,}\mathit{p}\mathrm{,}\mathit{p}\to \mathit{q}\Rightarrow \mathit{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: $${\displaystyle \frac{{\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1\Rightarrow {\mathit{\psi }}_1\leftrightarrow \neg {\mathit{\psi }}_2{\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2}{{\mathrm{\Gamma }}_2\nRightarrow {\mathit{\psi }}_2}}\text{if}|{\mathrm{\Gamma }}_1\cap \mathit{mcs}\mathrm{(}{\mathit{\psi }}_1\mathrm{)}|⩾|{\mathrm{\Gamma }}_2\cap \mathit{mcs}\mathrm{(}{\mathit{\psi }}_2\mathrm{)}|\mathrm{,}$$ where $\mathit{mcs}\mathrm{(}\mathit{\psi }\mathrm{)}$ is the set of the most compact supports of ψ, defined in Definition 4.9.

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

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

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

.

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 $\mathcal{S}$ , based on a logic $\mathsf{L}$ and a set $\mathsf{AttackRules}$ of sequent elimination rules, is the pair ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}=⟨{\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{,}\mathcal{A}⟩$ , where $\mathcal{A}\subseteq {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\times {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ and $\mathrm{(}{\mathit{s}}_1\mathrm{,}{\mathit{s}}_2\mathrm{)}\in \mathcal{A}$ iff there is $\mathcal{R}\in \mathsf{AttackRules}$ such that ${\mathit{s}}_1$ $\mathcal{R}$ -attacks ${\mathit{s}}_2$ .

In what follows, somewhat abusing the notations, we shall sometimes identify $\mathcal{A}$ with $\mathsf{AttackRules}$ .

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 ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}=⟨{\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{,}\mathcal{A}⟩$ be a sequent-based logical argumentation framework (for the set $\mathcal{S}$ , based on the logic $\mathsf{L}$ ), and let $\mathcal{E}\subseteq {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ . We say that $\mathcal{E}$ attacks an argument (sequent) s if there is an argument ${\mathit{s}}^{\prime }\in \mathcal{E}$ that attacks s (i.e. $\mathrm{(}{\mathit{s}}^{\prime }\mathrm{,}\mathit{s}\mathrm{)}\in \mathcal{A}$ ). The set of arguments that are attacked by $\mathcal{E}$ is denoted ${\mathcal{E}}^{+}$ . We say that $\mathcal{E}$ defends s if $\mathcal{E}$ attacks every argument ${\mathit{s}}^{\prime }$ that attacks s. The set $\mathcal{E}$ is called conflict-free if it does not attack any of its elements (i.e. ${\mathcal{E}}^{+}\cap \mathcal{E}=\varnothing$ ), $\mathcal{E}$ is called admissible if it is conflict-free and defends all of its elements, and $\mathcal{E}$ is complete if it is admissible and contains all the arguments that it defends. Now:

The minimal complete subset of ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ is the grounded extension of ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ ,

A maximal complete subset of ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ is a preferred extension of ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ ,

A complete subset $\mathcal{E}$ of ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ that attacks every argument in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\setminus \mathcal{E}$ is a stable extension of ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ .

Below, we denote by $\mathsf{Cmpl}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{)}$ (respectively, by $\mathsf{Grnd}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{)}$ , $\mathsf{Prf}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{)}$ , $\mathsf{Stbl}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{)}$ ) the set of all the complete (respectively, all the grounded, preferred, stable) extensions of ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ .

The induced entailment relations are now defined as follows:

Definition 5.3

Let ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}=⟨{\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{,}\mathcal{A}⟩$ be a sequent-based logical argumentation framework (for the set $\mathcal{S}$ of formulas and a logic $\mathsf{L}$ ), and suppose that $\mathsf{Sem}\in \{\mathsf{Grnd}\mathrm{,}\mathsf{Prf}\mathrm{,}\mathsf{Stbl}\}$ .

$\mathcal{S}|{\sim }_{\mathsf{L}\mathrm{,}\mathcal{A}\mathrm{,}\mathsf{Sem}}^{\forall }\mathit{\psi }$ if every extension $\mathcal{E}\in \mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{)}$ contains an argument of the form $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ . ¹⁵

15

Recall that by the definition of ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ , this implies that $\mathrm{\Gamma }\subseteq \mathcal{S}$ .

In this case we say that ψ skeptically follows from $\mathcal{S}$ according to $\mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{)}$ .

$\mathcal{S}|{\sim }_{\mathsf{L}\mathrm{,}\mathcal{A}\mathrm{,}\mathsf{Sem}}^{\exists }\mathit{\psi }$ if there is some extension $\mathcal{E}\in \mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{)}$ that contains an argument of the form $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ . In this case we say that ψ credulously follows from $\mathcal{S}$ according to $\mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{)}$ . ¹⁶

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.

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 $|{\sim }_{\mathsf{L}\mathrm{,}\mathcal{A}\mathrm{,}\mathsf{Sem}}$ to denote either $|{\sim }_{\mathsf{L}\mathrm{,}\mathcal{A}\mathrm{,}\mathsf{Sem}}^{\forall }$ or $|{\sim }_{\mathsf{L}\mathrm{,}\mathcal{A}\mathrm{,}\mathsf{Sem}}^{\exists }$ . Similarly, we use the notation $|\sim$ 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 ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ -based entailments by $\mathcal{S}|{\sim }_{\mathsf{L}\mathrm{,}\mathcal{A}\mathrm{,}\mathsf{Sem}}^{\sqcap }\mathit{\psi }$ if there is an argument $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ that belongs to every extension $\mathcal{E}\in \mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{)}$ . Clearly, it holds that if $\mathcal{S}|{\sim }_{\mathsf{L}\mathrm{,}\mathcal{A}\mathrm{,}\mathsf{Sem}}^{\sqcap }\mathit{\psi }$ then $\mathcal{S}|{\sim }_{\mathsf{L}\mathrm{,}\mathcal{A}\mathrm{,}\mathsf{Sem}}^{\forall }\mathit{\psi }$ . 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 ${\mathcal{S}}_1=\{\mathit{p}\mathrm{,}\neg \mathit{p}\mathrm{,}\mathit{q}\}$ that is based on classical logic $\mathsf{CL}$ , and whose only attack rule is Relevant Undercut (see Example 4.10). It is easy to see that no argument in ${\mathsf{Arg}}_{\mathsf{CL}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}$ attacks the argument $\mathit{q}\Rightarrow \mathit{q}$ , and so ${\mathcal{S}}_1|{\sim }_{\mathsf{CL}\mathrm{,}\mathrm{R}\text{-}\mathrm{Ucut}}\mathit{q}$ . On the other hand, $\mathit{P}\Rightarrow \mathit{p}$ and $\neg \mathit{p}\Rightarrow \neg \mathit{p}$ attack each other, therefore ${\mathcal{S}}_1|{\nsim }_{\mathsf{CL}\mathrm{,}\mathrm{R}\text{-}\mathrm{Ucut}}\mathit{p}$ and ${\mathcal{S}}_1|{\nsim }_{\mathsf{CL}\mathrm{,}\mathrm{R}\text{-}\mathrm{Ucut}}\neg \mathit{p}$ .

Example 5.6

Consider the set ${\mathcal{S}}_2=\{\mathit{p}\mathrm{,}\mathit{q}\mathrm{,}\neg \mathrm{(}\mathit{p}\wedge \mathit{q}\mathrm{)}\}$ . When classical logic is the base logic none of the formulas in ${\mathcal{S}}_2$ is derivable, since according to $\mathsf{CL}$ each pair of assertions in ${\mathcal{S}}_2$ attack the third one by (Relevant) Undercut.

Suppose now that the base logic is Priest's 3-valued paraconsistent logic $\mathsf{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 $\Rightarrow \mathit{p}\mathrm{,}\neg \mathit{p}$ and the negation rules in Figure 3.

Figure 3.

Negation rules for $\mathsf{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 $\mathsf{CL}$ is the base logic. Indeed, in $\mathsf{LP}$ sequents of the form $\mathit{p}\mathrm{,}\neg \mathrm{(}\mathit{p}\wedge \mathit{q}\mathrm{)}\Rightarrow \neg \mathit{q}$ are not derivable. It follows that while $\neg \mathrm{(}\mathit{p}\wedge \mathit{q}\mathrm{)}\Rightarrow \neg \mathrm{(}\mathit{p}\wedge \mathit{q}\mathrm{)}$ is still attacked in $\mathsf{LP}$ (by $\mathit{p}\mathrm{,}\mathit{q}\Rightarrow \mathit{p}\wedge \mathit{q}$ ), $\mathit{p}\Rightarrow \mathit{p}$ and $\mathit{q}\Rightarrow \mathit{q}$ are not attacked.

Example 5.7

Let us recall the set ${\mathcal{S}}_3=\{\mathit{m}\mathrm{,}\mathit{a}\mathrm{,}\mathit{m}\supset \mathsf{O}\neg \mathit{f}\mathrm{,}\mathrm{(}\mathit{m}\wedge \mathit{a}\mathrm{)}\supset \mathsf{O}\mathit{f}\}$ of Example 4.8. Suppose that $\mathsf{SDL}$ is the base logic and OO-SpecNeg is the single attack rule. We observe that, as expected, one concludes the following:

${\mathcal{S}}_3|{\nsim }_{\mathsf{SDL}\mathrm{,}\mathsf{OO}\text{-}\mathrm{SpecNeg}}\mathsf{O}\neg \mathit{f}$ . This is because one cannot derive $\mathsf{O}\neg \mathit{f}$ , since the sequent $\mathit{m}\mathrm{,}\mathit{m}\supset \mathsf{O}\neg \mathit{f}\Rightarrow \mathsf{O}\neg \mathit{f}$ is attacked by $\mathit{m}\mathrm{,}\mathit{a}\mathrm{,}\mathrm{(}\mathit{m}\wedge \mathit{a}\mathrm{)}\supset \mathsf{O}\mathit{f}\Rightarrow \neg \mathrm{(}\mathit{m}\supset \mathsf{O}\neg \mathit{f}\mathrm{)}$ .

${\mathcal{S}}_3|{\nsim }_{\mathsf{SDL}\mathrm{,}\mathsf{OO}\text{-}\mathrm{SpecNeg}}\mathsf{O}\mathit{f}$ . Indeed, the sequent $\mathit{m}\mathrm{,}\mathit{a}\mathrm{,}\mathrm{(}\mathit{m}\wedge \mathit{a}\mathrm{)}\supset \mathsf{O}\mathit{f}\Rightarrow \mathsf{O}\mathit{f}$ is not attacked by an argument in ${\mathsf{Arg}}_{\mathsf{SDL}}\mathrm{(}{\mathcal{S}}_3\mathrm{)}$ . ¹⁷

17

It is important to note that $\mathit{m}\mathrm{,}\mathit{a}\mathrm{,}\mathrm{(}\mathit{m}\wedge \mathit{a}\mathrm{)}\supset \mathsf{O}\mathit{f}\Rightarrow \mathsf{O}\mathit{f}$ is attacked by $\mathsf{SDL}$ -derivable arguments (such as $\mathit{m}\mathrm{,}\mathit{m}\supset \mathsf{O}\neg \mathit{f}\mathrm{,}\mathit{m}\mathrm{,}\mathit{a}\mathrm{,}\mathrm{(}\mathit{m}\wedge \mathit{a}\mathrm{)}\supset \mathsf{O}\neg \mathit{f}\Rightarrow \neg \mathrm{(}\mathrm{(}\mathit{m}\wedge \mathit{a}\mathrm{)}\supset \mathsf{O}\mathit{f}\mathrm{)}$ ), but none of them is in ${\mathsf{Arg}}_{\mathsf{SDL}}\mathrm{(}{\mathcal{S}}_3\mathrm{)}$ .

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 $|\sim$ . In what follows, we fix a (sequent-based) logical argumentation framework ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}=⟨{\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}\mathrm{,}\mathcal{A}⟩$ for a set $\mathcal{S}$ of $\mathcal{L}$ -formulas, based on a logic $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ with a sound and complete sequent calculus $\mathsf{C}$ , and where $\mathcal{A}$ is the set of attacks obtained by the sequent elimination rules in $\mathsf{AttackRules}$ (that is, $\mathrm{(}{\mathit{s}}_1\mathrm{,}{\mathit{s}}_2\mathrm{)}\in \mathcal{A}$ iff there is $\mathcal{R}\in \mathsf{AttackRules}$ and ${\mathit{s}}_1$ $\mathcal{R}$ -attacks ${\mathit{s}}_2$ ).

Proposition 5.8

If ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ is conflict-free with respect to ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ then $\mathcal{S}|\sim \mathit{\psi }$ iff $\mathcal{S}⊢\mathit{\psi }$ .

Proof

If there are no attacks between arguments in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ , no attack rule in $\mathsf{AttackRules}$ is applicable, and so the single extension of ${\mathcal{AF}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ is ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ . It follows, then, that $\mathcal{S}|\sim \mathit{\psi }$ iff there is a $\mathsf{C}$ -derivation of $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ for some $\mathrm{\Gamma }\subseteq \mathcal{S}$ . Since $\mathsf{C}$ is sound and complete for $\mathsf{L}$ , the latter is a necessary and sufficient condition for $\mathrm{\Gamma }⊢\mathit{\psi }$ , and so (by the monotonicity of $\mathsf{L}$ ) it is a necessary and sufficient condition for $\mathcal{S}⊢\mathit{\psi }$ . ¹⁸

18

In case that $\mathcal{S}$ is infinite, compactness of $\mathsf{L}$ should be assumed along the proof.

The next result is an immediate corollary of Proposition 5.8:

Corollary 5.9

If $\mathsf{AttackRules}=\varnothing$ then $|\sim$ and ⊢ coincide.

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

Proposition 5.10

If $\mathcal{S}|\sim \mathit{\psi }$ then $\mathcal{S}⊢\mathit{\psi }$ .

Proof

If $\mathcal{S}|\sim \mathit{\psi }$ then in particular there is a sequent $\mathrm{\Gamma }\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ for some $\mathrm{\Gamma }\subseteq \mathcal{S}$ . Thus, there is a proof in $\mathsf{C}$ for $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ , and so $\mathrm{\Gamma }⊢\mathit{\psi }$ . By the monotonicity of $\mathsf{L}$ we have that $\mathcal{S}⊢\mathit{\psi }$ .

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

Corollary 5.11

$|\sim$ is cautiously reflexive: for every formula ψ such that $\mathit{\psi }⊬\neg \mathit{\psi }$ it holds that $\mathit{\psi }|\sim \mathit{\psi }$ . ¹⁹

19

Note that the condition is indeed required here. For instance, in an argumentation framework based on $\mathsf{CL}$ and Undercut it holds that $\mathit{p}\wedge \neg \mathit{p}|{\nsim }_{\mathsf{CL}\mathrm{,}\mathrm{Ucut}}\mathit{p}\wedge \neg \mathit{p}$ . (Indeed, according to any semantics considered here $\mathit{p}\wedge \neg \mathit{p}\Rightarrow \mathit{p}\wedge \neg \mathit{p}$ is undefended, since it is attacked by $\Rightarrow \neg \mathrm{(}\mathit{p}\wedge \neg \mathit{p}\mathrm{)}$ , and the latter is not attacked by any other sequent since its left-hand side is empty).

Corollary 5.12

For every atom p it holds that $\mathit{p}|\sim \mathit{p}$ .

Proof

By Corollary 5.11 and the fact that since ¬ is a negation, for every p it holds that $\mathit{p}⊬\neg \mathit{p}$ .

Despite of the last two corollaries, (all) the examples above show that $|\sim$ may not be reflexive. These examples also show that in general $|\sim$ is not monotonic either. For instance, when $\mathsf{C}=\mathit{LK}$ and $\mathcal{A}$ consists of any of the attack rules in Figure 2, we have that $\mathit{p}|\sim \mathit{p}$ while $\mathit{p}\mathrm{,}\neg \mathit{p}|\nsim \mathit{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 $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ be a propositional logic.

A set $\mathcal{T}$ of formulas (in $\mathcal{L}$ ) is called ⊢-consistent if there exists a formula ψ (in $\mathcal{L}$ ) such that $\mathcal{T}⊬\mathit{\psi }$ .

We say that $\mathsf{L}$ is uniform, if for every two sets of formulas ${\mathcal{T}}_1\mathrm{,}{\mathcal{T}}_2$ and formula ψ we have that ${\mathcal{T}}_1⊢\mathit{\psi }$ when ${\mathcal{T}}_1\mathrm{,}{\mathcal{T}}_2⊢\mathit{\psi }$ and ${\mathcal{T}}_2$ is a ⊢-consistent theory that has no atomic formulas in common with ${\mathrm{\Gamma }}_1\cup \{\mathit{\psi }\}$ .

Remark 5.3

By Łos-Suzsko Theorem (Łos & Suzsko, 1958), a finitary propositional logic $⟨\mathcal{L}\mathrm{,}⊢⟩$ 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 $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ be a uniform logic, and let $\mathsf{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 ${\mathcal{S}}_1|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{\psi }$ and ${\mathcal{S}}_2$ is a ⊢-consistent set of formulas that is irrelevant (in the sense of Definition 4.9) to ${\mathcal{S}}_1\mathrm{,}$ then ${\mathcal{S}}_1\mathrm{,}{\mathcal{S}}_2|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{\psi }$ . ²⁰

20

Recall that by Notation 5.4 this means that the proposition holds for every entailment of the form $|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}\mathrm{,}\mathsf{Sem}}^{\mathit{\pi }}$ considered in Definition 5.3, where $\mathsf{L}$ and $\mathsf{R}$ are as defined in the proposition, $\mathsf{Sem}$ is any of the standard argumentation semantics considered in this paper, and $\mathit{\pi }\in \{\forall \mathrm{,}\exists \}$ .

Proof

First, we show the following lemma:

Lemma 5.15

No argument in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}$ is attacked, according to the rules in $\mathsf{R}\mathrm{,}$ by an argument in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\cup {\mathcal{S}}_2\mathrm{)}-{\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}$ .

Proof

In the notations of Definition 5.2, we have to show that ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}\cap {\mathrm{(}{\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\cup {\mathcal{S}}_2\mathrm{)}-{\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}\mathrm{)}}^{+}=\varnothing$ . Indeed, assume for contradiction that some $\mathrm{{\rm Y}}\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\cup {\mathcal{S}}_2\mathrm{)}-{\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}$ $\mathsf{R}$ -attacks some $\mathrm{\Gamma }\Rightarrow \mathit{\varphi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}$ , and let $\mathit{\delta }\in \mathrm{{\rm Y}}\cap {\mathcal{S}}_2$ (such a δ exists, otherwise $\mathrm{{\rm Y}}\subseteq {\mathcal{S}}_1$ and so $\mathrm{{\rm Y}}\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}$ ). In particular, $\mathit{\delta }\in \mathit{mcs}\mathrm{(}\mathit{\psi }\mathrm{)}$ , and so there is a sequent $\mathrm{\Delta }\Rightarrow \mathit{\psi }$ that $\mathcal{R}$ -attacks $\mathrm{\Gamma }\Rightarrow \mathit{\varphi }$ for some $\mathcal{R}\in \mathsf{R}$ and where Δ is a most compact support for ψ that contains δ.

Suppose first that $\mathcal{R}$ is one of the defeat rules. In this case $\mathit{\psi }=\neg \bigwedge {\mathrm{\Gamma }}^{\prime }$ , where ${\mathrm{\Gamma }}^{\prime }\subseteq \mathrm{\Gamma }$ . Since ${\mathcal{S}}_2$ is ⊢-consistent, by the uniformity of $\mathsf{L}$ we have that $\mathrm{\Delta }\cap {\mathcal{S}}_1\Rightarrow \neg \bigwedge {\mathrm{\Gamma }}^{\prime }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}$ , but since $\mathsf{Atoms}\mathrm{(}\mathrm{\Delta }\cap {\mathcal{S}}_1\mathrm{)}⊊\mathsf{Atoms}\mathrm{(}\mathrm{\Delta }\mathrm{)}$ (as $\mathit{\delta }\in \mathrm{\Delta }$ ), this contradicts the assumption that Δ is a most compact support for ψ.

Suppose now that $\mathcal{R}$ is one of the undercut rules. In this case both of $\mathit{\psi }\Rightarrow \neg \bigwedge {\mathrm{\Gamma }}^{\prime }$ and $\neg \bigwedge {\mathrm{\Gamma }}^{\prime }\Rightarrow \mathit{\psi }$ are $\mathsf{C}$ -derivable for some ${\mathrm{\Gamma }}^{\prime }\subseteq \mathrm{\Gamma }$ . Now, the application of Remark 3.2 on $\mathrm{\Delta }\Rightarrow \mathit{\psi }$ and $\mathit{\psi }\Rightarrow \neg \bigwedge {\mathrm{\Gamma }}^{\prime }$ yields that $\mathrm{\Delta }\Rightarrow \neg \bigwedge {\mathrm{\Gamma }}^{\prime }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\cup {\mathcal{S}}_2\mathrm{)}$ . Hence, by the uniformity of $\mathsf{L}$ and since ${\mathcal{S}}_2$ is ⊢-consistent, $\mathrm{\Delta }\cap {\mathcal{S}}_1\Rightarrow \neg \bigwedge {\mathrm{\Gamma }}^{\prime }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}$ . By Remark 3.2 again and the fact that $\neg \bigwedge {\mathrm{\Gamma }}^{\prime }\Rightarrow \mathit{\psi }$ is $\mathsf{C}$ -derivable, we get that $\mathrm{\Delta }\cap {\mathcal{S}}_1\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}$ . Once again, this is a contradiction to the choice of Δ as a most compact support for ψ, since $\mathsf{Atoms}\mathrm{(}\mathrm{\Delta }\cap {\mathcal{S}}_1\mathrm{)}⊊\mathsf{Atoms}\mathrm{(}\mathrm{\Delta }\mathrm{)}$ .

The proof of Proposition 5.14 now proceeds as follows: By the lemma above, the addition of irrelevant information $\mathrm{(}{\mathcal{S}}_2\mathrm{)}$ to existing information $\mathrm{(}{\mathcal{S}}_1\mathrm{)}$ does not produce more attacks on existing arguments, and so every Sem-extension ${\mathcal{E}}_1\in \mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}\mathrm{)}$ is included in some Sem-extension ${\mathcal{E}}_2\in \mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\cup {\mathcal{S}}_2\mathrm{)}\mathrm{)}$ . We also get the converse, since in our case the arguments in $\mathcal{E}\cap \mathrm{(}{\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\cup {\mathcal{S}}_2\mathrm{)}-{\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}\mathrm{)}$ do not defend the arguments in $\mathcal{E}$ , and so if $\mathcal{E}\in \mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\cup {\mathcal{S}}_2\mathrm{)}\mathrm{)}$ then ${\mathcal{E}}_2\cap {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}\in \mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}\mathrm{)}$ . Suppose then that ${\mathcal{S}}_1|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{\psi }$ . This means that every [some] extension ${\mathcal{E}}_1\in \mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\mathrm{)}\mathrm{)}$ contains an argument of the form $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ where $\mathrm{\Gamma }\subseteq {\mathcal{S}}_1$ , and so every [some] extension ${\mathcal{E}}_2\in \mathsf{Sem}\mathrm{(}{\mathcal{AF}}_{\mathsf{L}}\mathrm{(}{\mathcal{S}}_1\cup {\mathcal{S}}_2\mathrm{)}\mathrm{)}$ contains an argument of the form $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ where $\mathrm{\Gamma }\subseteq {\mathcal{S}}_1$ (thus $\mathrm{\Gamma }\subseteq {\mathcal{S}}_1\cup {\mathcal{S}}_2$ ). This implies that ${\mathcal{S}}_1\mathrm{,}{\mathcal{S}}_2|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{\psi }$ .

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 $|\sim$ 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 $\mathrm{(}\mathit{p}\mathrm{,}\neg \mathit{p}⊬\mathit{q}$ for $\mathit{p}\ne \mathit{q}\mathrm{)}$ then so is $|\sim$ .

Proof

By Proposition 5.10, $\mathcal{S}|\nsim \mathit{\psi }$ when $\mathcal{S}⊬\mathit{\psi }$ . Thus, if $\mathit{p}\mathrm{,}\neg \mathit{p}⊬\mathit{q}$ then $\mathit{p}\mathrm{,}\neg \mathit{p}|\nsim \mathit{q}$ as well, and so $|\sim$ is paraconsistent.

Next, we consider crash resistance.

Definition 5.17

Let $\mathcal{S}$ be a set of $\mathcal{L}$ -formulas such that $\mathsf{Atoms}\mathrm{(}\mathcal{S}\mathrm{)}⊊\mathsf{Atoms}\mathrm{(}\mathcal{L}\mathrm{)}$ .

$\mathcal{S}$ is called contaminating for $|\sim$ , if for every set $\mathcal{T}$ that is irrelevant for $\mathcal{S}$ and for every formula ϕ, it holds that $\mathcal{S}|\sim \mathit{\phi }$ iff $\mathcal{S}\mathrm{,}\mathcal{T}|\sim \mathit{\phi }$ .

$|\sim$ is crash-resistant if there is no set of formulas that is contaminating for $|\sim$ .

Proposition 5.18

Let $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ be a uniform logic that has the variable sharing property (so it resists irrelevant information: $\mathcal{S}⊬\mathit{\psi }$ when ψ is irrelevant to $\mathcal{S}\mathrm{)}$ . Then, in the notations of Proposition 5.14, $|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}$ is crash resistant.

Proof

Suppose for a contradiction that there is a set $\mathcal{S}$ that is contaminating for $|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}$ . Let p be an atom that does not appear in $\mathcal{S}$ . Then $\mathcal{S}⊬\mathit{p}$ and by Proposition 5.10, $\mathcal{S}|{\nsim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{p}$ . Since $\mathcal{S}$ is contaminating we have that $\mathcal{S}\mathrm{,}\mathit{p}|{\nsim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{p}$ . On the other hand, by Corollary 5.12, $\mathit{p}|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{p}$ , and so by Proposition 5.14, $\mathcal{S}\mathrm{,}\mathit{p}|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{p}$ — a contradiction.

Proposition 5.19

Let $\mathsf{L}=⟨\mathcal{L}\mathrm{,}⊢⟩$ be a logic with a ⊢-deductive ⊃. Suppose that

$\mathsf{L}$ has the variable sharing property for consistent sets (if $\mathcal{S}$ is ⊢-consistent and ψ is irrelevant to $\mathcal{S}$ then $\mathcal{S}⊬\mathit{\psi }\mathrm{)}\mathrm{,}$ and that

$\mathsf{L}$ is consistency-enforcing $\mathrm{(}⊢\neg \bigwedge \mathrm{\Gamma }$ whenever a finite Γ is ⊢-inconsistent $\mathrm{)}.$

Let $\varnothing \ne \mathsf{R}\subseteq \{$ Defeat, Compact Defeat, Undercut, Canonical Undercut, Compact Undercut}. Then, $|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}$ is crash resistant.

Proof.First we show:

Lemma 5.20

For any $\mathcal{S}$ and any $\mathit{s}=\mathrm{{\rm Y}}\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ such that ϒ is ⊢-inconsistent there is a ${\mathit{s}}^{\prime }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}-{\mathsf{Arg}}_{\mathsf{L}}{\mathrm{(}\mathcal{S}\mathrm{)}}^{+}$ that $\mathsf{R}$ -attacks s.

Proof

Since ϒ is ⊢-inconsistent, by (2), ${\mathit{s}}^{\prime }=\Rightarrow \neg \bigwedge \mathrm{{\rm Y}}\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ . It is easy to see that ${\mathit{s}}^{\prime }$ $\mathcal{R}$ -attacks s for all $\mathcal{R}\in \mathsf{R}$ and that ${\mathit{s}}^{\prime }$ is not attacked in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ .

Suppose for a contradiction that there is a set $\mathcal{S}$ that is contaminating for $|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}$ . Let p be an atom that does not appear in $\mathcal{S}$ . By (1), for every $\mathrm{{\rm Y}}\Rightarrow \mathit{p}\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ , ϒ is ⊢-inconsistent. By Lemma 5.20 we have $\mathcal{S}|{\nsim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{p}$ and hence by the supposition also $\mathcal{S}\mathrm{,}\mathit{p}|{\nsim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{p}$ . To see that $\mathcal{S}\mathrm{,}\mathit{p}|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{p}$ , suppose that $\mathrm{{\rm Y}}\Rightarrow \mathit{\psi }\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\cup \{\mathit{p}\}\mathrm{)}$ $\mathsf{R}$ -attacks $\mathit{p}\Rightarrow \mathit{p}$ . Then $\mathit{\psi }\Rightarrow \neg \mathit{p}\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\cup \{\mathit{p}\}\mathrm{)}$ and by transitivity, $\mathrm{{\rm Y}}\Rightarrow \neg \mathit{p}\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\cup \{\mathit{p}\}\mathrm{)}$ . If $\mathit{p}\notin \mathrm{{\rm Y}}$ , ϒ is ⊢-inconsistent by (1). If $\mathit{p}\in \mathrm{{\rm Y}}$ then $\mathrm{{\rm Y}}-\{\mathit{p}\}\Rightarrow \mathit{p}\supset \neg \mathit{p}\in {\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\mathrm{)}$ and again ϒ is ⊢-inconsistent by (1). By Lemma 5.20, then, $\mathrm{{\rm Y}}\Rightarrow \mathit{\psi }$ is attacked by some non-attacked sequent in ${\mathsf{Arg}}_{\mathsf{L}}\mathrm{(}\mathcal{S}\cup \{\mathit{p}\}\mathrm{)}$ . It follows that $\mathit{p}\Rightarrow \mathit{p}$ is defended by $\mathcal{S}\cup \{\mathit{p}\}$ and hence $\mathcal{S}\mathrm{,}\mathit{p}|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{R}}\mathit{p}$ . Thus $\mathcal{S}$ is cannot be contaminating for $|{\sim }_{\mathsf{L}\mathrm{,}\mathsf{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

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

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 $⟨\mathrm{\Gamma }\mathrm{,}\mathit{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 $\mathit{\psi }\Rightarrow \mathit{\psi }$ with Left-Weakening, Supposition is Reflexivity, Conditionalisation is [ $\Rightarrow \supset$ ], 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 $\mathrm{\Gamma }\Rightarrow \mathit{\psi }$ , and defeasible arguments, denoted by $\mathrm{\Gamma }\hookrightarrow \mathit{\psi }$ , one may define attack rules of the following form: $${\displaystyle \frac{{\mathrm{\Gamma }}_1\hookrightarrow {\mathit{\psi }}_1{\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2\dots {\mathrm{\Gamma }}_{\mathit{n}-1}\Rightarrow {\mathit{\psi }}_{\mathit{n}-1}{\mathrm{\Gamma }}_{\mathit{n}}\hookrightarrow {\mathit{\psi }}_{\mathit{n}}}{{\mathrm{\Gamma }}_{\mathit{n}}\hookrightarrow ̸{\mathit{\psi }}_{\mathit{n}}}}.$$ The rule above expressed that (an argument obtained from the defeasible schema) ${\mathrm{\Gamma }}_1\hookrightarrow {\mathit{\psi }}_1$ attacks (an argument obtained from the defeasible schema) ${\mathrm{\Gamma }}_{\mathit{n}}\hookrightarrow {\mathit{\psi }}_{\mathit{n}}$ , provided that the conditions in $\{{\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2\mathrm{,}\dots \mathrm{,}{\mathrm{\Gamma }}_{\mathit{n}-1}\Rightarrow {\mathit{\psi }}_{\mathit{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 $\mathrm{\Gamma }\Rightarrow \mathit{p}$ for any finite sequence Γ of literals that contains p and in which the first appearance of p precedes any appearance of $\neg \mathit{p}$ . Another possibility is to employ multisets in the sequents, for example, for representing majority considerations. Thus, one may state that $\mathrm{\Gamma }\Rightarrow \mathit{p}$ holds whenever the number of appearances of p in a multiset Γ of literals is strictly bigger than the number of appearances of $\neg \mathit{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: $$\begin{array}{cc}\hfill \text{Permutation:}& {\displaystyle \frac{{\mathrm{\Gamma }}_1\mathrm{,}\mathit{\psi }\mathrm{,}\mathit{\phi }\mathrm{,}{\mathrm{\Gamma }}_2\Rightarrow \mathrm{\Delta }}{{\mathrm{\Gamma }}_1\mathrm{,}\mathit{\phi }\mathrm{,}\mathit{\psi }\mathrm{,}{\mathrm{\Gamma }}_2\Rightarrow \mathrm{\Delta }}}{\displaystyle \frac{\mathrm{\Gamma }\Rightarrow {\mathrm{\Delta }}_1\mathrm{,}\mathit{\psi }\mathrm{,}\mathit{\phi }\mathrm{,}{\mathrm{\Delta }}_2}{\mathrm{\Gamma }\Rightarrow {\mathrm{\Delta }}_1\mathrm{,}\mathit{\phi }\mathrm{,}\mathit{\psi }\mathrm{,}{\mathrm{\Delta }}_2}}\mathrm{,}\hfill \\ \hfill \text{Contraction:}& {\displaystyle \frac{{\mathrm{\Gamma }}_1\mathrm{,}\mathit{\psi }\mathrm{,}\mathit{\psi }\mathrm{,}{\mathrm{\Gamma }}_2\Rightarrow \mathrm{\Delta }}{{\mathrm{\Gamma }}_1\mathrm{,}\mathit{\psi }\mathrm{,}{\mathrm{\Gamma }}_2\Rightarrow \mathrm{\Delta }}}{\displaystyle \frac{\mathrm{\Gamma }\Rightarrow {\mathrm{\Delta }}_1\mathrm{,}\mathit{\psi }\mathrm{,}\mathit{\psi }\mathrm{,}{\mathrm{\Delta }}_2}{\mathrm{\Gamma }\Rightarrow {\mathrm{\Delta }}_1\mathrm{,}\mathit{\psi }\mathrm{,}{\mathrm{\Delta }}_2}}.\hfill \end{array}$$

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 ${\mathrm{\Gamma }}_1\Rightarrow \mathrm{(}{\mathrm{\Gamma }}_2\Rightarrow \mathit{\psi }\mathrm{)}$ may be intuitively understood by ‘if ${\mathrm{\Gamma }}_1$ were true, one would argue that ${\mathrm{\Gamma }}_2\Rightarrow \mathit{\psi }$ ’ and the hypersequent ${\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1\mid {\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2$ may be understood (again, intuitively) as a disjunction, at the meta-level, of the arguments ${\mathrm{\Gamma }}_1\Rightarrow {\mathit{\psi }}_1$ and ${\mathrm{\Gamma }}_2\Rightarrow {\mathit{\psi }}_2$ .