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.
Argumentation is the study of how jointly acceptable conclusions can be reached from a collection of arguments. In recent years, logic-based approaches for analysing and evaluating arguments, sometimes called logical (or deductive) argumentation, have been largely studied, yielding a variety of formal methods for argumentation-based reasoning (see, for instance, the reviews in Chesñevar, Maguitman, and Loui, 2000; Prakken and Vreeswijk, 2002). The goal of this paper is to provide an abstract, proof theoretical investigation of logical argumentation. Our starting point is that an argument is a pair of a finite set of formulas (Γ, the support set) and a formula (ψ, the conclusion), expressed in an arbitrary propositional language, such that the latter follows, according to some underlying logic, from the former. This abstract approach gives rise to Gerhard Gentzen's well-known notion of a sequent (Gentzen, 1934), extensively used in the context of proof theory. Accordingly, an argument is associated with a sequent of the form and logical argumentation boils down to the exposition of formalised methods for reasoning with these syntactical objects.
This paper is a revised and extended version of Arieli (2013), where a sequent-based approach to logical argumentation is realised in the following two aspects:
Arguments as sequents.
We show that sequents are useful for representing logical arguments since they can be regarded as specific kinds of judgments. This has the obvious benefit that proof theoretical approaches may be used in the context of argumentation theory. For instance, well-studied sequent calculi may be incorporated for producing arguments in an automated way. Moreover, some restrictions in previous definitions of logical arguments, like minimality and consistency of support sets (see, e.g. Besnard & Hunter, 2001, 2009), may now be lifted, allowing for a more flexible way of expressing arguments, which also simplifies their identification.
Attacks as sequent elimination rules.
We show that interactions between arguments (expressed by attack relations) can by represented in terms of Gentzen-style rules of inference. This induces a general and uniform approach not only for introducing arguments, but also for eliminating them. Furthermore, in addition to known attack relations that are ‘imported’ to our framework (which are discussed in Arieli, 2013), we also introduce new types of attack relations, like attacks incorporating different kinds of modal operators, quantitative measurements, and attacks that are based on relevance considerations, implementing the well-known principle of variable sharing from relevance logics (Dunn and Restall, 2002) and applying it for argumentation reasoning.
Keeping our sequent-based setting generic and modular allows us to accommodate different types of languages and logics, including non-classical ones. This enables the use of different substructural logics, including paraconsistent logics (da Costa, 1974) that support robust methods of handling conflicts among arguments, and deontic logics (Aqvist, 2002) that incorporate modalities for modelling normative reasoning and handling problematic cases in which there are conflicts among norms.
The rest of this paper is organised as follows: in the next section we review some basic notions behind logical argumentation and introduce some related notations. Then, in Sections 3 and 4 we re-examine these notions and suggest some proof theoretical substitutes. This allows us to introduce, in Section 5, the notion of sequent-based logical argumentation frameworks, admitting different languages, logics, and inducing a family of entailment relations. The latter can be used for simulating existing entailments of logical argumentation and for introducing new ones. In Section 5 we illustrate reasoning with these entailments in different contexts and consider (also in the Appendix of the paper) some of their basic properties. Finally, in Section 6 we refer to some related work and in Section 7 we conclude.
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.1Dung, 1995
An argumentation framework is a pair , where Args is an enumerable set of elements, called arguments, and is a relation on whose instances are called attacks.
Let be a standard propositional language, an enumerable set of formulas in , and the consequence relation of classical logic (for ). An argument in the sense of Besnard and Hunter (BH-argument, for short), formed by , is a pair , where ψ is a formula in and Γ is a minimally consistent subset of (where minimisation is with respect to set inclusion), such that . 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.
Let and be two BH-arguments.
is a defeater of if .
is a direct defeater of if there is such that .
is an undercut of if there is such that and .
is a direct undercut of if there is s.t. and .
is a canonical undercut of if and .
is a rebuttal of if and .
is a defeating rebuttal of if .
Let . Then is an BH-argument (formed by ) which is a (direct) defeater and a (direct and canonical) undercut of the BH-argument . Note, further, that while q follows according to classical logic from , the pair is not a BH-argument, since its support set is not classically consistent.
Let be the (countably infinite) set of BH-arguments formed by , and let be a binary relation on , obtained by at least one of the conditions described in Definition 2.3. Then the pair 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 are excluded since their supports are not minimal, although one may consider a stronger support for than, say, , since the set logically implies every minimal support of . Moreover, the size of is bigger than that of , and this may be relevant when quantitative considerations are involved (see Section 4.4).1,2
Consistency. The requirement that the support set Γ of an argument should be consistent may be irrelevant for some logics, at least when consistency is defined by satisfiability. Indeed, in logics such as Priest's three-valued logic (Priest, 1989) or Belnap's four-valued logic (Belnap, 1977), every set of formulas in the language of is satisfiable.
Complexity. From a more pragmatic point of view, the involvement of minimally consistent subsets of the underlying knowledge-base poses serious questions on the computational viability of identifying arguments and generating them. Indeed, deciding the existence of a minimal subset of formulas that implies the consequent is already at the second level of the polynomial hierarchy (see Eiter & Gottlob, 1995). For first-order languages the problem is more severe, since arguments may not be generated in an effective way.
Our conclusion, then, is that what really matters for an argument, is that (i) its consequent would logically follow, according to the underlying logic, from the support set, and that (ii) there would be an effective way of constructing and identifying it. In what follows we therefore adhere to the following principles:
(1) Supports and consequents of arguments are solely determined by the logic.
(2) Arguments are syntactical objects that are effectively computable by a formal system that is related to the logic, and are refutable by the attack relation of the argumentation system.
For the first item we indicate what a logic is (Definition 3.1). The first part of the second item corresponds to the primary goal of proof theory, so notations and machinery are borrowed from that area (Definitions 3.2 and 3.3).
We denote by an arbitrary propositional language having a countably infinite set of atomic formulas. In what follows (possibly primed or indexed) denote arbitrary theories (sets of formulas) in , and (possibly primed or indexed) denote finite theories in . Given a language , we fix a corresponding logic (sometimes called the base logic or the core logic), defined as follows.
A (propositional) logic for a language is a pair , where ⊢ is a (Tarskian) consequence relation for , that is, a binary relation between sets of formulas and formulas in , satisfying the following conditions:
In the sequel we shall exclude trivial consequence relations, that is, we shall assume that for distinct atoms p and q.
In what follows we assume that contains the following connectives:
A unary connective ¬ which is a ⊢-negation: for every atomic formula p of it holds that and ,
A binary connective ∧ which is a ⊢-conjunction: for every set of formulas and formulas it holds that iff and .
Also, when has an implication connective ⊃, we shall assume that it is deductive with respect to the base consequence relation:3
A binary connective ⊃ is called a ⊢-deductive implication if for every set of formulas and formulas it holds that iff .
We shall denote by the conjunction of all the formulas in (the finite theory) Γ, and abbreviate the formula by .
Let be a propositional language, and let ⇒ be a symbol that does not appear in . An -sequent (or just a sequent) is an expression of the form , where Γ and Δ are finite sets of formulas in .
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 , then, there is an effective way of drawing entailments: iff for some finite subset there is a proof of the sequent in the corresponding sequent calculus.
Let be a logic with a corresponding sequent calculus , and let be a set of formulas in . An -argument based on is an -sequent of the form , where ,4 that is provable in .5 We denote by the set of all the -arguments that are based on .
In the notation of Definition 3.3, we have that:
Let be a propositional logic. Then is in iff for a finite .
Consider Gentzen's sequent calculus LK (Figure 1), which is sound and complete for classical logic . In this case we have, for instance, that the sequent is derivable in LK and so it belongs to whenever contains the formula . Note, however, that this sequent is not derivable by any sequent calculus that is sound and complete for intuitionistic logic (e.g. Gentzen's LJ), thus it is not in for any .
For every logic and a set of formulas in the set is closed under the following rules:6
-Reflexivity: For every finite and it holds that
-Monotonicity: If and then
-Transitivity: If and then also
By Proposition 3.4, -Reflexivity (respectively, -Monotonicity, -Transitivity) follows from the reflexivity (respectively, the monotonicity, transitivity) of ⊢.
The set of the BH-arguments is not closed under any rule in Proposition 3.6. To see this consider for instance the set . Then and , however , since its support set is not minimal. Thus is not -transitive. The fact that (while ) also shows that is not -monotonic and that it is not -reflexive.7
Let be a logic and a set of formulas in . Then -Transitivity can be strengthened as follows:
If and for a finite , then .
Note that unlike -Transitivity, in the rule above ψ may not belong to .
4.Attacks as sequent elimination rules
In order to represent attack relations we introduce rules for excluding arguments (i.e. sequents) in the presence of counter arguments. We call such rules sequent elimination rules, or attack rules. The obvious advantage of representing attacks by sequent elimination rules is that the form of such rules is similar to that of the construction rules, and both types of rules are expressed by the same syntactical objects. This allows us to uniformly identify and generate arguments and attacks by the same sequent-manipulation systems.
Typical conditions of attack rules consist of three ingredients: the attacking argument (the first sequent in the rule's prerequisites), the attacked argument (the last sequent in the rule's prerequisites), and the conditions for the attack (the other prerequisites). Conclusions of sequent elimination rules will be the elimination of the attacked argument. In the sequel, we denote by the elimination (or, the discharging) of the argument . Alternatively, if a sequent is denoted by s, its discharged counterpart will sometimes be denoted by .
Let be a set of -arguments, a sound and complete sequent calculus for . A sequent elimination rule (or attack rule) is a Gentzen-type rule of the following form:
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 , as long as is sound and complete for .
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 and -arguments in , an argument is an -defeater of an argument if . In the presence of a ⊢-deductive implication ⊃ in , this means that , and so is an -argument in . It follows that attacks by defeaters may be represented by the following sequent elimination rule (relative to ):
In the particular case where the underlying logic is classical logic , this rule is a sequent-based encoding of a defeater attack in the sense of Definition 2.3:
Let and be two BH-arguments. Then is a defeater of in the sense of Definition 2.3 iff the rule Defeat defined above is -applicable with respect to a substitution θ, where and .
Since are BH-arguments it holds that for and so the sequents are LK-provable (). Moreover, since is a defeater of , it holds that , thus is also LK-provable. It follows that the rule Defeat is -applicable with respect to a substitution θ such that and (). Conversely, let and be BH-arguments and suppose that the rule Defeat is -applicable with respect to a substitution θ such that and (). Then the attacking condition of this rule is LK-provable, which means that , and so is a defeater of in the sense of Definition 2.3.
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.
We say that an attack rule -implies an attack rule , if for every set of formulas , whenever is -applicable its conclusion is produced by (with respect to ). Formally: whenever -attacks there is that -attacks .8 The Attack rules and are said to be-equivalent, if each one of them -implies the other.
From an argumentative point of view, the fact that a rule implies a rule intuitively means that any attack that is producible using can be reproduced using by means of an attacking argument with the same support set.
For every logic Compact Defeat is -equivalent to Defeat.
To show that Compact Defeat implies Defeat assume that the three conditions of Defeat hold with respect to . Since is derivable, it holds that . Thus, since ⊃ is a ⊢-deductive implication, . This, together with the assumption that is derivable (and so it is an argument in ), imply by Remark 3.2 that is an argument in, and so by Definition 3.3 it is derivable in the underlying sequent calculus. It follows that 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, , and so, since ⊃ is a ⊢-deductive implication, . We thus have that the sequent is derivable in the underlying sequent calculus. It follows that is producible by Defeat, and so Defeat indeed implies Compact Defeat.
Attacks by direct defeaters. Direct defeat with respect to an arbitrary logic and a set of-arguments based on , means that is an -direct defeater of if for some . Thus, a direct defeat attack may be expressed by the following sequent elimination rule:
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:
Let and be two BH-arguments. Then is a direct defeater of in the sense of Definition 2.3 iff the rule Direct Defeat defined above is -applicable with respect to a substitution θ where and .
Similar to that of Proposition 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:
For every logic Compact Direct Defeat is -equivalent to Direct Defeat.
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 we first have to define logical equivalence in . A natural way to do so is to require that ψ and φ are logically equivalent in iff and . Using a ⊢-deductive implication ⊃ and a ⊢-conjunctive connective ∧, this means that , that is, that is a theorem of . It follows that attacks by undercuts are represented by the following sequent elimination rule:
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:
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:
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 -arguments, as the premises of these conditions are not necessarily included in .9
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.
Let be a propositional logic, where has a ⊢-conjunction ∧. Then: (a) Defeating Rebuttal is -equivalent to Rebuttal, (b) Undercut -implies Canonical Undercut and Direct Undercut, (c) Canonical Undercut is -equivalent to Defeat, (d) Direct Defeat is-equivalent to Direct Undercut.
Part (a) follows from the fact that both rules are -equivalent to Compact Rebuttal. Part (b) follows from the fact that Undercut holds in particular when is a singleton (in which case Direct Undercut is obtained) and when 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.
Further relations between the elimination rules introduced above may be obtained under further assumptions on the underlying logics. For instance, when is classical logic, Defeat implies Direct Defeat, since in LK the sequent is derivable from for any . Similar considerations show that in this case Defeat also implies Undercut and Defeating Rebuttal.
4.2.Attacks incorporating modalities
The fact that our approach is language-independent enables us to apply it in different scenarios and for a variety of purposes. One of them, demonstrated in Straßer & Arieli (2014), applies sequent-based logical argumentation for modelling normative reasoning in the context of deontic logic (Aqvist, 2002). The idea is to reason with and about norms such as obligations, imperatives, permissions, etc. This is usually formalised by the primitive modal operator that represents obligations and the defined modal operator (where ) that represents permissions.
A paradigmatic instance for normative reasoning is so-called factual detachment, saying that if ϕ holds, and there is a commitment to ψ conditional on ϕ, then there is a commitment to ψ. Another instance is aggregation: if there is a norm to bring about ϕ and another norm to bring about ψ then there should be a norm to bring about . Allowing for unrestricted factual detachment or unrestricted aggregation is problematic in cases in which norms conflict. As shown in Straßer & Arieli (2014) and demonstrated next, attack rules in the context of sequent-based argumentation are useful for representing and handling such conflicts.
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 and . Now, in case one is indeed served asparagus () we expect to derive the (unconditional) obligation to eat with fingers () rather than to not eat with fingers (). 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 attacks the argument . Here, arguments are obtained by a sequent calculus for standard deontic logic , which extends LK by the following inference rules for the modal operators: (Below, we denote for )
Some variations of Specificity are given below (where ):10
When is a logic in which any formula follows from a contradiction (in particular, if is classical logic, ), any sequent is attacked according to each rule in Figure 2. Thus, for instance, when , , and the attack rule is Undercut, the sequent is attacked by the (classically valid) sequent , although – intuitively – q is not really related to the inconsistency in .
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. ). 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.
Let Γ be a set of formulas and ψ a formula in a language , and denote by the set of atomic formulas that appear in (some formula of) Γ.
Γ is relevant to ψ, if implies that . A non-empty set Γ is irrelevant to a (non-empty) set Δ if .
Γ is a most compact support for ψ (with respect to a logic and a set of assertions ), if and there is no with such that .11 We denote by the set of all formulas such that ϒ is a most compact support for ψ (with respect to and ).12
Let be an elimination rule in Figure 2, in which attacks . The relevant variant of is the application of with the side conditions (i.e. a restriction on the application of ) that and is relevant to .
Relevant Undercut is defined as follows:
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 . In this case, the sequent is attacked according to [R-Ucut] only by and not by , since the latter is not in relative to . Moreover, the transition from to its clausal form , which keeps the two sets equivalent according to classical logic, has some implications on the attack relation, since is now attacked according to [R-Ucut] by and not by , which in turn does not belong to relative to . It follows that relevant attacks are sensitive to the syntactic structure of the underlying set of assertions.13 We refer to Avron (2014) for an in-depth discussion on the relevance principle and corresponding logics.
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 a stronger argument for than , 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 on cannot stem only from the fact that (where denotes the size of Γ), since in this case the argument could be attacked by an argument like or even by , whose support sets are bigger, but are certainly not stronger.
A rebuttal attack rule for capturing 'stronger support due to more relevant evidence' may be formalized as follows:
To see an application of this rule, consider the set and suppose that the underlying logic is classical logic. Then attacks according to the above rule the sequent (but not the other way around), since its relevant evidential support for is bigger than the relevant evidence the other sequent has for supporting .
We conclude Section 4 with a general observation about its realm.
Our purpose in this section was to exemplify the wide range of attack relations that can be expressed by sequent-based rules. How to choose the most appropriate attacks for specific needs is beyond the scope of this paper (mainly due to its generality and the fact that many context-dependent considerations are involved in the study of well-behaved attacks, among which are the language of the arguments and the type of the underlying logic). However, the suitability of attack relations for specific settings is an important issue that should be verified when it comes to applications. To see this we recall Remark 4.5 and the result by Gorogiannis & Hunter (2011) that in the scope of standard propositional languages and classical logic canonical undercuts and rebuttals yield complete extensions (see Definition 5.2) whose arguments have mutually inconsistent conclusions.
For assuring the well-behaviour of attack relations one may need to refer to rationality postulates tailored to the specific logic under consideration (like those specified by Caminada & Amgoud (2007)). This may trigger the introduction of additional machinery such as preference orderings over arguments, as described, for example, in Modgil & Prakken (2013)14.
5.Sequent-based argumentation frameworks and their entailments
By Sections 3 and 4 we can now consider argumentation frameworks (Definition 2.1) whose arguments are sequents and whose attacks are obtained by sequent elimination rules. We call these structures sequent-based logical argumentation frameworks.
A (sequent-based) logical argumentation framework for a set of formulas , based on a logic and a set of sequent elimination rules, is the pair , where and iff there is such that -attacks .
In what follows, somewhat abusing the notations, we shall sometimes identify with.
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.
Let be a sequent-based logical argumentation framework (for the set , based on the logic ), and let . We say that attacks an argument (sequent) s if there is an argument that attacks s (i.e. ). The set of arguments that are attacked by is denoted . We say that defends s if attacks every argument that attacks s. The set is called conflict-free if it does not attack any of its elements (i.e. ), is called admissible if it is conflict-free and defends all of its elements, and is complete if it is admissible and contains all the arguments that it defends. Now:
The minimal complete subset of is the grounded extension of ,
A maximal complete subset of is a preferred extension of ,
A complete subset of that attacks every argument in is a stable extension of .
Below, we denote by (respectively, by , , ) the set of all the complete (respectively, all the grounded, preferred, stable) extensions of .
The induced entailment relations are now defined as follows:
Let be a sequent-based logical argumentation framework (for the set of formulas and a logic ), and suppose that .
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 to denote either or . Similarly, we use the notation whenever a statement applies to each of the entailment relations in Definition 5.3.
A more cautious approach to skeptical reasoning would be to define -based entailments by if there is an argument in that belongs to every extension . Clearly, it holds that if then . In what follows we shall concentrate on the entailments of Definition 5.3.
Let us consider a sequent-based argumentation system for that is based on classical logic , and whose only attack rule is Relevant Undercut (see Example 4.10). It is easy to see that no argument in attacks the argument , and so . On the other hand, and attack each other, therefore and .
Consider the set . When classical logic is the base logic none of the formulas in is derivable, since according to each pair of assertions in attack the third one by (Relevant) Undercut.
Suppose now that the base logic is Priest's 3-valued paraconsistent logic (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 and the negation rules in Figure 3.
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 is the base logic. Indeed, in sequents of the form are not derivable. It follows that while is still attacked in (by ), and are not attacked.
Let us recall the set of Example 4.8. Suppose that is the base logic and OO-SpecNeg is the single attack rule. We observe that, as expected, one concludes the following:
. This is because one cannot derive , since the sequent is attacked by .
. Indeed, the sequent is not attacked by an argument in .17
It is important to note at this point that the reasoning mechanism, depicted in the last examples, is reinforced by corresponding derivation procedures. Such derivations are dynamic in nature, as sequents may not only be introduced during a derivation, but may also be retracted. This brings about a deviation in the standard definition of derivability in Gentzen-type proof systems. We postpone the discussion about this to another paper. The interested reader is referred to Arieli & Straßer (2014) for some definitions and preliminary discussions on this matter.
Next, we consider some basic properties of . In what follows, we fix a (sequent-based) logical argumentation framework for a set of -formulas, based on a logic with a sound and complete sequent calculus , and where is the set of attacks obtained by the sequent elimination rules in (that is, iff there is and -attacks).
If is conflict-free with respect to then iff .
If there are no attacks between arguments in , no attack rule in is applicable, and so the single extension of is . It follows, then, that iff there is a -derivation of for some . Since is sound and complete for , the latter is a necessary and sufficient condition for , and so (by the monotonicity of ) it is a necessary and sufficient condition for .18
The next result is an immediate corollary of Proposition 5.8:
If then and ⊢ coincide.
As the examples above show, and ⊢ are different. In the general case, we have:
If then .
If then in particular there is a sequent for some . Thus, there is a proof in for , and so . By the monotonicity of we have that .
Proposition 5.8 implies, in particular, the following results for all the attack relations considered previously in this paper:
is cautiously reflexive: for every formula ψ such that it holds that .19
For every atom p it holds that .
By Corollary 5.11 and the fact that since ¬ is a negation, for every p it holds that .
Despite of the last two corollaries, (all) the examples above show that may not be reflexive. These examples also show that in general is not monotonic either. For instance, when and consists of any of the attack rules in Figure 2, we have that while .
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:
Let be a propositional logic.
A set of formulas (in ) is called ⊢-consistent if there exists a formula ψ (in ) such that .
We say that is uniform, if for every two sets of formulas and formula ψ we have that when and is a ⊢-consistent theory that has no atomic formulas in common with .
By Łos-Suzsko Theorem (Łos & Suzsko, 1958), a finitary propositional logic is uniform iff it has a single characteristic matrix (see also Urquhart, 2001). Thus, for instance, the logics in this paper are uniform.
Let be a uniform logic, and let be a set of attack rules in Relevant Compact Defeat, Relevant Compact Direct Defeat, Relevant Undercut, Relevant Direct Undercut, and Relevant Canonical Undercut. If and is a ⊢-consistent set of formulas that is irrelevant (in the sense of Definition 4.9) to then .20
First, we show the following lemma:
No argument in is attacked, according to the rules in by an argument in .
In the notations of Definition 5.2, we have to show that . Indeed, assume for contradiction that some -attacks some , and let (such a δ exists, otherwise and so ). In particular, , and so there is a sequent that -attacks for some and where Δ is a most compact support for ψ that contains δ.
Suppose first that is one of the defeat rules. In this case , where . Since is ⊢-consistent, by the uniformity of we have that , but since (as ), this contradicts the assumption that Δ is a most compact support for ψ.
Suppose now that is one of the undercut rules. In this case both of and are -derivable for some . Now, the application of Remark 3.2 on and yields that . Hence, by the uniformity of and since is ⊢-consistent, . By Remark 3.2 again and the fact that is -derivable, we get that . Once again, this is a contradiction to the choice of Δ as a most compact support for ψ, since .
The proof of Proposition 5.14 now proceeds as follows: By the lemma above, the addition of irrelevant information to existing information does not produce more attacks on existing arguments, and so every Sem-extension is included in some Sem-extension . We also get the converse, since in our case the arguments in do not defend the arguments in , and so if then . Suppose then that . This means that every [some] extension contains an argument of the form where , and so every [some] extension contains an argument of the form where (thus ). This implies that.
In the Appendix we show that, assuming that the base logic satisfies some simple properties, the cautious form of monotonicity in Proposition 5.14 holds also for frameworks with non-relevant attack rules (see Propositions A.2 and A.3).
We conclude this section by checking two properties of that assure proper handling of inconsistent information: paraconsistency (da Costa, 1974) and crash resistance (Caminada, Carnielli, & Dunne, 2012). We start with the former.
If ⊢ is paraconsistent for then so is .
By Proposition 5.10, when . Thus, if then as well, and so is paraconsistent.
Next, we consider crash resistance.
Let be a set of -formulas such that .
is called contaminating for , if for every set that is irrelevant for and for every formula ϕ, it holds that iff .
is crash-resistant if there is no set of formulas that is contaminating for .
Let be a uniform logic that has the variable sharing property (so it resists irrelevant information: when ψ is irrelevant to . Then, in the notations of Proposition 5.14, is crash resistant.
Suppose for a contradiction that there is a set that is contaminating for . Let p be an atom that does not appear in . Then and by Proposition 5.10, . Since is contaminating we have that . On the other hand, by Corollary 5.12, , and so by Proposition 5.14, — a contradiction.
Let be a logic with a ⊢-deductive ⊃. Suppose that
(1) has the variable sharing property for consistent sets (if is ⊢-consistent and ψ is irrelevant to then and that
(2) is consistency-enforcing whenever a finite Γ is ⊢-inconsistent
Let Defeat, Compact Defeat, Undercut, Canonical Undercut, Compact Undercut}. Then, is crash resistant.
Proof.First we show:
For any and any such that ϒ is ⊢-inconsistent there is a that -attacks s.
Since ϒ is ⊢-inconsistent, by (2), . It is easy to see that -attacks s for all and that is not attacked in .
Suppose for a contradiction that there is a set that is contaminating for . Let p be an atom that does not appear in . By (1), for every , ϒ is ⊢-inconsistent. By Lemma 5.20 we have and hence by the supposition also . To see that , suppose that -attacks . Then and by transitivity, . If , ϒ is ⊢-inconsistent by (1). If then and again ϒ is ⊢-inconsistent by (1). By Lemma 5.20, then, is attacked by some non-attacked sequent in . It follows that is defended by and hence . Thus is cannot be contaminating for .
Different approaches to logical argumentation have been introduced in the literature, including formalisms that are based on classical logic (Besnard & Hunter, 2001, 2009), defeasible reasoning (Governatori, Maher, Antoniou, & Billington, 2004; Pollock, 1991, 1995; Simari & Loui, 1992) abstract argumentation and the ASPIC+ framework (Modgil & Prakken, 2014; Prakken, 2010), assumption-based argumentation (Dung, Kowalski, & Toni, 2006), default logic (Prakken, 1993), situation calculus (Brewka, 2001), and so forth.
The starting point of this paper is Besnard and Hunter's approach to logical argumentation (Besnard & Hunter, 2001, 2009), which we believe is a successful way of representing deductive reasoning in argumentation-based environments (we refer to Besnard & Hunter, 2009 for some comparisons of this approach to other logic-based approaches, in particular the above-mentioned work on defeasible reasoning). Our work extends this approach in several ways: first, the usual conditions of minimality and consistency of supports are abandoned. This offers a simpler way of producing arguments and identifying them (also for systems that are not formulated in a Gentzen-type style).21 Second, arguments are produced and are withdrawn by rules of the same style, allowing for a more uniform way of representing the frameworks and computing their extensions. Third, our approach is logic-independent. This allows in particular to rely on a classical as well as on a non-classical logic, and so, for instance, paraconsistent formalisms may be used for improving consistency-maintenance.
Another sequent-based approach to logical argumentation has been proposed by Pollock (1991, 1995), where arguments are sequences of sequents of the form , obtained by generic inference rules (Input, Reason, Supposition, Conditionalisation, and Dilemma), and organised in inference graphs. Unlike the present approach, Pollock distinguishes between defeasible and conclusive (strict) arguments, where only defeasible arguments can be attacked.
The ingredients of Pollock's setting may be simulated in our setting. First, in the presence of a calculus like LK, Pollock's rules are translatable into our representation. For instance, Input is the Axiom with Left-Weakening, Supposition is Reflexivity, Conditionalisation is , and Dilemma is reasoning by cases. Second, it is not difficult to adjust our setting for accommodating two (or more) kinds of arguments. In the presence of strict argument, denoted by , and defeasible arguments, denoted by , one may define attack rules of the following form:
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 for any finite sequence Γ of literals that contains p and in which the first appearance of p precedes any appearance of . Another possibility is to employ multisets in the sequents, for example, for representing majority considerations. Thus, one may state that holds whenever the number of appearances of p in a multiset Γ of literals is strictly bigger than the number of appearances of 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:
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 may be intuitively understood by ‘if were true, one would argue that ’ and the hypersequent may be understood (again, intuitively) as a disjunction, at the meta-level, of the arguments and .
1 Clearly, the argument A may be split into two BH-arguments, and , but in general such rewriting requires further processing and might cause a blowup in the number of arguments.
2 Another argument that is sometimes pleaded for set-inclusion minimisation is that it reduces the number of attacks. Again, it is disputable whether set-inclusion minimisation is the right principle for assuring this property, since, for instance, the singletons and , supporting (e.g. in classical logic) the claim , 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 becomes more exposed to attacks than .
3 The availability of an implication connective is not required – see Remark 4.3.
4 Following the usual convention, we shall omit set-brackets from the left-hand sides of sequents.
5 Obviously, for the definition of an -argument it does not matter which of the calculi that are sound and complete for is chosen.
6 Following the usual conventions, we use commas in a sequent for denoting the union operation, and omit curly brackets of singletons (i.e. we write ψ instead of ).
7 Note that is cautiously -reflexive: for a consistent formula .
8 Gorogiannis & Hunter (2011) consider a stricter implication between attacks, in which .
9 To reduce the amount of notations, we use the same names for the rules with and without the implication connective. This will not cause ambiguity in what follows.
10 Note that ‘-Spec’ or ‘-SpecNeg’ variants would not be sensible, since permissions with incompatible content do not conflict in any intuitive sense.
11 Note that this condition does not imply a subset-minimality of Γ, but rather assures that Γ does not contain information that is irrelevant (in the sense of Item (a)) for its conclusion.
12 For instance, when and , we have that .
13 On the other hand, relevant attack rules have some desirable properties that are not necessarily shared by other rules, like being invariant with respect to irrelevant information – see Lemma 5.15.
14 See also the conclusion of this paper for a short discussion on implementing preferences in sequents.
15 Recall that by the definition of , this implies that .
16 Similar entailment relations may of-course be defined for other semantics of abstract argumentation frameworks, such as semi-stable semantics (Caminada, 2006), ideal semantics (Dung, Mancarella, & Toni, 2007), eager semantics (Caminada, 2007), and so forth.
17 It is important to note that is attacked by -derivable arguments (such as ), but none of them is in .
18 In case that is infinite, compactness of should be assumed along the proof.
19 Note that the condition is indeed required here. For instance, in an argumentation framework based on and Undercut it holds that . (Indeed, according to any semantics considered here is undefended, since it is attacked by , and the latter is not attacked by any other sequent since its left-hand side is empty).
20 Recall that by Notation 5.4 this means that the proposition holds for every entailment of the form considered in Definition 5.3, where and are as defined in the proposition, is any of the standard argumentation semantics considered in this paper, and .
Conflict of interest disclosure statement
No potential conflict of interest was reported by the authors.
Christian Straßer's research was supported by the Alexander von Humboldt Foundation and the German Ministry for Education and Research.
Amgoud L., & Besnard P. (2009). Bridging the gap between abstract argumentation systems and logic. Proc. SUM'09, LNCS, Vol. 5785. Heidelberg: Springer, pp. 12–27.
Amgoud L., & Besnard P. (2010). A formal analysis of logic-based argumentation systems. Proc. SUM'10, LNCS, Vol. 6379. Heidelberg: Springer, pp. 42–55.
Aqvist L. (2002). Deontic logic. In D. M. Gabbay and F. Guenthner (Eds.), Handbook of philosophical logic (Vol. 8, pp. 147–264). Dordrecht: Kluwer.
Arieli O. (2013). A sequent-based representation of logical argumentation. Proc. CLIMA'13, LNCS, Vol. 8143. Heidelberg: Springer, pp. 69–85.
Arieli O., & Straßer C. (2014). Dynamic derivations for sequent-based deductive argumentation. Proc. COMMA'14, Frontiers in artificial intelligence and applications, Vol. 266, IOS Press, pp. 89–100.
Avron A. (1987). A constructive analysis of RM. Journal of Symbolic Logic, 52, 939–951. doi: 10.2307/2273828
Avron A. (2014). What is relevance logic? Annals of Pure and Appied Logic, 165, 26–48. doi: 10.1016/j.apal.2013.07.004
Batens D. (2007). A universal logic approach to adaptive logics. Logica Universalis, 1, 221–242. doi: 10.1007/s11787-006-0012-5
Belnap N. D. (1977). A useful four-valued logic. In M. Dunn and G. Epstein (Eds.), Modern uses of multiple-valued logics (pp. 7–37). Dordrecht: Reidel Publishing.
Besnard P., Grégoire É., Piette C., & Raddaoui B. (2010). MUS-based generation of arguments and counter-arguments. Proc. IRI'10, IEEE, pp. 239–244.
Besnard P., & Hunter A. (2001). A logic-based theory of deductive arguments. Artificial Intelligence, 128, 203–235. doi: 10.1016/S0004-3702(01)00071-6
Besnard P., & Hunter A. (2009). Argumentation based on classical logic. In I. Rahwan and G. R. Simari (Eds.), Argumentation in artificial intelligence (pp. 133–152). Dordrecht: Springer.
Brewka G. (2001). Dynamic argument systems: A formal model of argumentation processes based on situation calculus. Journal of Logic and Computation, 11, 257–282. doi: 10.1093/logcom/11.2.257
Brünnler K. (2010). Nested sequents (PhD thesis). University of Bern.
Caminada M.W.A. (2006). Semi-stable semantics. Proc. COMMA'06, IOS Press, pp. 121–130.
Caminada M.W.A. (2007). Comparing two unique extension semantics for formal argumentation: ideal and eager. Proc. BNAIC'07, 81–87.
Caminada M.W.A., & Amgoud L. (2007). On the evaluation of argumentation formalisms. Artificial Intelligence, 171, 286–310. doi: 10.1016/j.artint.2007.02.003
Caminada M.W.A., Carnielli W.A., & Dunne P.E. (2012). Semi-stable semantics. Journal of Logic and Computation, 22, 1207–1254. doi: 10.1093/logcom/exr033
Chesñevar C.I., Maguitman A.G., & Loui R.P. (2000). Logical models of argument. ACM Computing Surveys, 32, 337–383. doi: 10.1145/371578.371581
da Costa N.C.A. (1974). On the theory of inconsistent formal systems. Notre Dame Journal of Formal Logic, 15, 497–510. doi: 10.1305/ndjfl/1093891487
Dung P.M. (1995). On the acceptability of arguments and its fundamental role in nonmonotonic reasoning, logic programming and n-person games. Artificial Intelligence, 77, 321–357. doi: 10.1016/0004-3702(94)00041-X
Dung P.M., Kowalski R., & Toni F. (2006). Dialectic proof procedures for assumption-based, admissible argumentation. Artificial Intelligence, 170, 114–159. doi: 10.1016/j.artint.2005.07.002
Dung P.M., Mancarella P., & Toni F. (2007). Computing ideal sceptical argumentation. Artificial Intelligence, 171, 642–674. doi: 10.1016/j.artint.2007.05.003
Dunn J.M., & Restall G. (2002). Relevance logic. In D. Gabbay & F. Guenther (Eds.), Handbook of philosophical logic (Vol. 6, pp. 1–136). Dordrecht: Kluwer.
Efstathiou V., & Hunter A. (2011). Algorithms for generating arguments and counterarguments in propositional logic. International Journal of Approximate Reasoning, 52, 672–704. doi: 10.1016/j.ijar.2011.01.005
Eiter T., & Gottlob G. (1995). The complexity of logic-based abduction. ACM Journal, 42, 3–42. doi: 10.1145/200836.200838
Gentzen G., Investigations into logical deduction. In German. An English translation appears in ‘The collected works of Gerhard Gentzen’, edited by M.E. Szabo, North-Holland, 1969. (1934).
Gorogiannis N., & Hunter A. (2011). Instantiating abstract argumentation with classical logic arguments: Postulates and properties. Artificial Intelligence, 175, 1479–1497. doi: 10.1016/j.artint.2010.12.003
Governatori G., Maher M.J., Antoniou G., & Billington D. (2004). Argumentation semantics for defeasible logic. Journal of Logic and Computation, 14, 675–702. doi: 10.1093/logcom/14.5.675
Horty J.F. (1994). Moral dilemmas and nonmonotonic logic. Journal of Philosiphical Logic, 23, 35–65. doi: 10.1007/BF01417957
Łos J., & Suzsko R. (1958). Remarks on sentential logics. Indagationes Mathematicae, 20, 177–183.
Modgil S., & Prakken H. (2013). A general account of argumentation with preferences. Artificial Intelligence, 195, 361–397. doi: 10.1016/j.artint.2012.10.008
Modgil S., & Prakken H. (2014). The ASPIC+ framework for structured argumentation: A tutorial. Argument and Computation, 5, 31–62. doi: 10.1080/19462166.2013.869766
Pollock J.L. (1987). Defeasible reasoning. Cognitive Science, 11, 481–518. doi: 10.1207/s15516709cog1104_4
Pollock J.L. (1991). A theory of defeasible reasoning. International Journal of Intelligent Systems, 6, 33–54. doi: 10.1002/int.4550060103
Pollock J.L. (1992). How to reason defeasibly. Artificial Intelligence, 57, 1–42. doi: 10.1016/0004-3702(92)90103-5
Pollock J. (1995). Cognitive carpentry. A blueprint for how to build a person. Cambridge, MA: MIT Press.
Prakken H. (1993). An argumentation framework in default logic. Annals of Mathematics and Artificial Intelligence, 9, 93–132. doi: 10.1007/BF01531263
Prakken H. (1996). Two approaches to the formalisation of defeasible deontic reasoning. Studia Logica, 57, 73–90. doi: 10.1007/BF00370670
Prakken H. (2010). An abstract framework for argumentation with structured arguments. Argument and Computation, 1, 93–124. doi: 10.1080/19462160903564592
Prakken H., & Vreeswijk G. (2002). Logical systems for defeasible argumentation. In D. Gabbay and F. Guenthner (Eds.), Handbook of philosophical logic (Vol. 4, pp. 219–318). Dordrecht: Kluwer.
Priest G. (1989). Reasoning about truth. Artificial Intelligence, 39, 231–244. doi: 10.1016/0004-3702(89)90027-1
Simari G.R., & Loui R.P. (1992). A mathematical treatment of defeasible reasoning and its implementation. Artificial Intelligence, 53, 125–157. doi: 10.1016/0004-3702(92)90069-A
Stolpe A. (2010). A theory of permission based on the notion of derogation. Journal of Applied Logic, 8, 97–113. doi: 10.1016/j.jal.2010.01.001
Straßer C. (2014). Adaptive logics for defeasible reasoning. Applications in argumentation, normative reasoning and default reasoning. Heidelberg: Springer.
Straßer C., & Arieli O. (2014). Sequent-based argumentation for normative reasoning. Proc. DEON'14, LNAI, Vol. 8554. Heidelberg: Springer, pp. 224–240.
Urquhart A. (2001). Many-valued logic. In D. Gabbay and F. Guenthner (Eds.), Handbook of philosophical logic (Vol. II, pp. 249–295). Dordrecht: Kluwer.
Wu Y. (2012). Between argument and conclusion. Argument-based approaches to discussion, inference and uncertainty (PhD thesis). University of Luxembourg.
Appendix. Some further results about the restricted monotonicity of
Below we show that under some (rather intuitive) requirement on the base logic , restricted monotonicity with respect to relevant attacks (Proposition 5.3) may be generalised to other attack rules. For this, we first need to introduce some new terminology.
Let be a propositional logic.
We say that is consistency-enforcing, if for every finite set of -formulas Γ that is not ⊢-consistent it holds that .
We say that is -expanding, if implies that for every finite set that contains Γ.
In what follows we consider sequent elimination rules representing premise attacks (prem-attacks, for short), that is: all the forms of defeat and undercut in Figure 2. In addition, we assume that a given set of prem-attacks rules contains at least one of the rules Defeat, Compact Defeat, Undercut, Compact Undercut, or Canonical Undercut.
The main results of this Appendix are then the following:
Let be a uniform, -expanding and consistency-enforcing logic, a set of prem-attacking rules, and a semantics which is either complete, grounded, preferred or stable. If and is irrelevant to then .
Let be a uniform, -expanding and consistency-enforcing logic, a set of prem-attacking rules, and a semantics which is either complete, grounded or preferred (The question whether this proposition holds also for stable semantics is left for future work.). If and is irrelevant to then .
Note that, unlike Proposition 5.14, in the propositions above need not be ⊢-consistent.
To show the Propositions A.2 and A.3, we need a few lemmas. The first lemma holds in every argumentation framework with a set of unattacked arguments.
Let be the framework restricted to . Then .
To see that , suppose that . Then . Since is conflict-free, necessarily , and so . Suppose now that defends in an argument . If defends A also in then by the completeness of , . If does not defend A in , then there is a that -attacks A, but. However, since , there is a such that C -attacks B. But , so , which contradicts the assumption that . We have thus shown that every argument that is defended by in is in . Let now and suppose some attacks A in . Clearly, B also attacks A in . By the completeness of in , B is attacked by some in . Since and , C also attacks B in . Hence, defends itself in . Altogether, we have shown that
To see that , suppose that . Note first that by the definition of , . Since is complete in , , and hence . We now show that . Clearly, is conflict-free in since the only attacks that are added by moving from (the attack relation of ) to are attacks between Args and and between and Args. Suppose now that defends in some . If also defends A in then . Otherwise, does not defend A in . By the conflict-freeness of and since , A cannot be in . Hence, , and so there is an -attacker B of A such that there is no such that C -attacks B. However, there must be a such that D-attacks B. This means that . However, since B -attacks A, , a contradiction. We have thus shown that whenever defends some then . Conversely, suppose that and some attacks A in . If then , since . In case , also , as . Thus, defends all of its elements. Altogether, we have shown that .
Lemma A.4 may be adjusted to any completeness-based semantics, that is, to every semantics such that implies and (Note that all the semantics considered in this paper are completeness-based.). Thus, for every framework , its induced framework as defined in Lemma A.4, and a completeness-based semantics , we have that .
Next, we fix some logic and a sequent-based argumentation framework , for which we use the following notations:
is of the form ,
is of the form where ϒ is ⊢-inconsistent}.
By Remark A.1 we conclude that every extension with respect to a completeness-based semantics of an argumentation framework whose base logic is consistency-enforcing (and whose elimination rules are prem-attacking), consists only of sequents whose premises are ⊢-consistent. Formally:
Let be a sequent-based argumentation framework where is consistency-enforcing and whose rules in are prem-attacks. Then for every completeness-based semantics and every it holds that .
Since has only prem-attack rules, . Since is consistency-enforcing, (This is due to the supposition that contains at least one of the rules Defeat, Compact Defeat, Undercut, Compact Undercut, or Canonical Undercut, mentioned at the beginning of the Appendix. This allows to derive the sequent where ϒ is ⊢-inconsistent.). Thus:
The next two lemmas present other properties that will be needed in the sequel.
Let be a uniform and consistency-enforcing logic, and let be a set of prem-attack rules. Suppose that is a set of -formulas that is irrelevant to a set of -formulas . If an argument -attacks an argument according to a rule then there is a formula such that the argument -attacks B.
Suppose that A -attacks B where .
Suppose first that is a direct prem-attacking rule (i.e. either Direct Defeat, Compact Direct Defeat, or Direct Undercut). In this case where . Hence, by Remark 3.2, is in . Since is ⊢-consistent (because so is ϒ), by the uniformity of , . Obviously, -attacks B.
Suppose now that is a compact prem-attacking rule (Compact Defeat, Compact Direct Defeat, Compact Undercut). Then for some . Again, by the uniformity of we have that . Clearly, -attacks B.
Suppose that is any other prem-attacking rule (that is, Undercut, Canonical Undercut, or Defeat). Then for some . By Remark 3.2, then, . Again, by the uniformity of , we have that . Clearly, -attacks B.
In each case, then, there is a formula such that the argument is in and -attacks B.
there is a such that B -attacks A for some .
Let be a sequent-based argumentation framework, where is an -expanding logic and is a set of prem-attack rules. Suppose that and that and are derivable sequents where and . Then:
(1) If then .
(2) If then where is any set containing ϒ and .
To see the first item, note that since is a complete extension, we only have to show that defends . Suppose then that -attacks where . We show that.
If is a direct prem-attack or (Compact) Undercut, then B also attacks A, and so .
In the other cases (Defeat, Compact Defeat, Canonical Undercut) is derivable. Since is -expanding, is derivable. By Remark 3.2, . Clearly, -attacks A and so . However, since has the same premise set as B, also .
For the second item, let be an argument in that -attacks for some . Again, we consider two cases.
If is a direct prem-attack or (Compact) Undercut, clearly B -attacks A.
Let be Defeat, Compact Defeat or Canonical Undercut. Then is derivable, and since is -expanding also is derivable. By Remark 3.2, . Clearly, -attacks A. By Item 1, .
In both cases there is an argument in that -attacks A, and so .
The main lemma for Propositions A.2 and A.3 is the following:
Let be a uniform, consistency-enforcing, and -expanding logic, and let be a set of prem-attack rules. If is irrelevant to then:
(1) If then .
(2) If then .
(3) If then .
(4) If then .
(5) If then .
(6) If there is such that .
(7) If there is such that .
(8) If and then .
Let , , and be as in the lemma.
Item 1: Obviously, . For the converse, let be an argument in . Then there is an argument that -attacks B. By Lemma A.6 (which is applicable here, since by Corollary A.5, ), there is an argument such that -attacks B. By Lemma A.8(1), , and so .
Item 2: Let . In particular, and all its subsets are conflict-free, thus is conflict-free. To see that is admissible, suppose that attacks some . Then, since is complete in , and hence . By Item 1, . Thus indeed defends itself. It remains to show that defends exactly itself. For this, suppose that defends some . Assume for a contradiction that and hence . Since is complete, does not defend A. Hence, there is an argument such that B -attacks A and . Suppose first that . Since is consistency-enforcing, there is an argument that attacks B. Since we have that, which is a contradiction to our assumption that . Hence, . By Lemma A.6 (which again is applicable here, since by Corollary A.5, ), there is a that -attacks A. Hence, since defends A, . But then by Lemma A.8(2), also and thus – a contradiction.
Item 3: Obviously is conflict-free in , since it is conflict-free in . Suppose that -attacks some . If then by Equation (A1) in the proof of Corollary A.5, and so (since is complete ). Suppose now . Thus, by Lemma A.6, there is an argument such that -attacks B. Since is admissible in , . Thus, by Lemma A.8(2), also. Hence, .
Item 4: Suppose for a contradiction that . Then there is a set which is complete in . Let . Since and , is not admissible in . Thus, either is not conflict-free or is not defended. Assume first that is not conflict-free. Hence, either there is some that attacks some , or there is some that attacks some . Suppose the first case. Since is defends itself, there is a that attacks A and hence we're in the second case. Note that by Corollary A.5, since is complete. Thus, by Item 1, there is an argument that attacks D. But this means that is not conflict-free – a contradiction. We have thus established that is conflict-free. Hence, is not defended. However, since by Item 3, , and since and is conflict-free, it is easy to see that is defended – a contradiction. Thus, we have established that is maximally admissible in , which means that .
Item 5: Let . Since is stable in , it is also complete and . Hence, either , which implies that (since ), or , which implies that (by the definition of and again since). In the latter case, by Item 1, . Since A is arbitrary in this shows that . By Item 2, is complete in . Thus, is stable in .
Item 6: Let . By Item 3, . The rest follows by the fact that if then there is a such that .
Item 7: Since is in particular complete in , by Item 6 there is an extension for which . The rest follows immediately by the fact that each complete extension is included in some preferred extension of the same framework.
Item 8: By Item 2, is complete in , and thus .
Now we can turn to the proofs of the main results of this Appendix:
Proof of Proposition A.2.
Suppose that , and let be an extension in . First, we treat grounded semantics. By our assumption, there is an argument in the grounded extension of . Thus, by Lemma A.9(8), is in the grounded extension of , that is, in . Thus . Suppose now that the semantics is either complete, preferred or stable. Again, by our assumption, there is an argument of the form in every element of . By Lemma A.9, , and so there is a sequent of the form in . In particular, contains a sequent of the form , and so .
Proof of Proposition A.3.
Suppose that . Hence, there is some extension in that contains a sequent of the form for some . By Lemma A.9, there is an extension in that contains the extension . Thus, is in , and so .
Let be a uniform, -expanding and consistency-enforcing logic, and let be a set of prem-attacking rules.
is crash resistant when is a complete, grounded, preferred or stable semantics.
is crash resistant when a complete, grounded or preferred semantics.
The proof of Item 1 (respectively, of Item 2) is similar to that of Proposition 5.18, using Proposition A.2 (respectively, Proposition A.3) instead of Proposition 5.14.