Abstract
In this paper, we explore the relation between an agent’s doxastic attitude and her arguments in support of a given claim. Our main contribution is the design of a logical setting that allows us reason about binary arguments which are either in favour or against a certain claim. This is a setting in which arguments and propositions are the basic building blocks so that the concept of argument-based belief emerges in a straightforward way. We work against the background of Dung’s abstract argumentation framework, extending it to a new setting in which we can study the formal properties of binary arguments as well as the larger structures they establish. This paper introduces a formal ‘two-dimensional’ language to talk about propositions and arguments, for which a sound and complete axiom system is provided.
1. Introduction
The literature on argumentation theory contains a number of different views on what a single argument is. The proposed definitions range from Toulmin’s six interrelated components (claim, data, warrant, backing, rebuttal, qualifier; Toulmin, Citation2003) to Dung’s abstract argumentation framework (Dung, Citation1995) where an argument is simply an abstract undefined entity, and what matters is the way it interacts with others (i.e. which ones it ‘attacks’ and which ones it ‘defends’). These abstract argumentation frameworks have proved to be useful for analysing different notions of acceptability of arguments. Intuitively, the arguments that matter are those that will ‘survive’ the full argumentation process, and the abstract argumentation frameworks provide different concepts and tools to identify them.
This process of identifying the ‘acceptable’ sets of arguments, evidence or justifications has historically played an important role in the definition of epistemic notions such as knowledge and belief. There is an extensive literature in (formal) epistemology on what ingredients are needed to provide a solid foundation for rational belief and knowledge. In terms of arguments, we provide a quote from Dung (Citation1995, p. 323):
[...] a statement is believable if it can be argued successfully against attacking arguments. In other words, whether or not a rational agent believes in a statement depends on whether or not [an] argument supporting this statement can be successfully defended against the counterarguments.
While Dung talks explicitly about the relationship between beliefs and arguments, it is surprising that no further details are provided in the referred paper.Footnote1 Neither has this topic received much attention within the literature on argumentation theory with a few exceptions including (Schwarzentruber, Vesic, and Rienstra, Citation2012) and Grossi and van der Hoek (Citation2014). One of the reasons for this might be that the abstract argumentation framework abstracts away too many elements. Among these elements, two play an essential role when attempting to define the agent’s belief. The first is the content of each argument; the second is the issue on which an argument attacks another. Without these ingredients, we lack the details to decide on whether one argument’s attack on another one is actually relevant to the claim at stake, or whether all the ‘acceptable’ arguments can back up the given claim.
This paper picks up this thread proposing a formal definition of the notion of beliefs in terms of the arguments the agent has in support of or against a given claim. In an argumentation on whether P, we stipulate that all the arguments are in support or against P. In this sense, we call them binary arguments. We start (Section 2) by recalling the basic definitions of abstract argumentation theory. Then (Section 3), we extend them with two elements. With the first we unveil a crucial characteristic of each (so far abstract) argument by indicating the propositions it supports; with the second we relativise the attack relation by making explicit the proposition on which a given argument attacks another. Then, we introduce a formal definition of an agent’s beliefs. The paper continues (Section 4) introducing a formal language for exploring the properties of this new notion, together with a sound and complete axiom system to reason about binary arguments. The work ends (Section 5) with a brief summary and further lines for research. The proofs of most propositions and theorems are provided in the Appendix A.1.
Related work Our logical setting in this paper ties in with the modal logic analysis of abstract argumentation notions provided in Grossi (Citation2010b), Grossi (Citation2010) and Grossi (Citation2012). Following that line, the work by Grossi and van der Hoek (Citation2014) comes closest to this paper as the authors also present a setting that combines both abstract arguments and an agent’s beliefs. Yet different from our approach is the fact that their notion of belief is taken as a basic component which is not defined in terms of the arguments involved. In a different but related direction, Schwarzentruber et al. (Citation2012) aims at describing not only the argumentation structure but also the information the agents have about it. Intuitively, an agent’s belief is based on what she knows/believes about the argumentation structure, so it is important to make the agent’s informational state explicit. Also related is the work in Dyrkolbotn (Citation2013), which uses graph theory tools (kernels and local kernels; cf. the propositional discourse logic of Dyrkolbotn and Walicki (Citation2014)) and modal languages for dealing with the acceptability of formulas that might ‘argue’ against each other, and also introduce three-valued models of belief induced by argumentation frameworks.
Other logic-technical approaches that can contribute to the study of argument-based beliefs includes not only the dialogical logic tradition (Lorenzen, Citation1958; Lorenz, Citation1961; Lorenzen & Lorenz, Citation1978, whose main motivations can be traced back to ancient Greece when logic was conceived as the systematic study of dialogues in which two parties exchange arguments over a central claim), but also the logics for reasoning about the (soft or hard) evidential basis of different attitudes ranging from knowledge to belief (Baltag, Renne, & Smets, Citation2014; Baltag, Renne, & Smets, Citation2012). The later direction builds further on the justification logic tradition (Artemov & Nogina, Citation2005; Artemov, Citation2008) in which reasons are explicitly represented in justification terms and on the work in dynamic epistemic logic (DEL) on representing different epistemic and doxastic attitudes and their dynamics (van Benthem, Citation2007; van Ditmarsch, van Der Hoek, & Kooi, Citation2007; Baltag & Smets, Citation2008; van Benthem, Citation2011). The work in *AiML2016 enhances these investigations by focussing on different types of models that connect evidence and beliefs, relating it to both the investigations in neighbourhood structures in *vanBenthem2012 and *vanBenthemFernandezPacuit2014 where beliefs are defined in terms of maximally consistent sets of evidence, and the recent work by (Baltag, Bezhanishvili, Özgün, and Smets, Citation2016a) on a topological semantics for evidence, evidence-based justifications, belief and knowledge.
2. Background on abstract argumentation theory
The argumentation framework of Dung (Citation1995) is known to abstract away from the internal structure of an argument, focusing instead of the way the arguments interact with one another. Here is the formal definition of its basic component, the so-called argumentation graph:
Definition 2.1:
[Argumentation Graph Dung (Citation1995)] An argumentation graph is a pair where
is a non-empty set of abstract arguments and
is a binary relation on
.
The relation is interpreted as an attack relation, with
read as ‘argument
attacks argument s’. This notion of attack can be extended to sets of arguments: a set
attacks an argument s, denoted by
, when there is an argument
in X that attacks s,
. We say that an argument
is defended by
when every argument attacking s is in turn attacked by an argument in X (i.e. when
implies
such that
).
This level of abstraction gives us insights about the position of each argument with respect to other arguments in the same structure. For example, in the graph whose diagram appears below, the arguments in do not attack each other (in Dung’s terminology, the set is called conflict-free). Also each member of X which is under attack is defended by X itself (the set is called self-acceptable), as
attacks
, but
attacks
.
The following characteristic functions are useful for defining argumentative-theoretic notions that allow us to formalise the reasons for ‘accepting’ a given set of arguments.
Definition 2.2:
[Defence and neutrality functions Grossi (Citation2012)] Let be an argumentation graph.
Given a set
, the defence function
returns the set of arguments in
defended by X:
Given a set
, the neutrality function
returns the set of arguments in
which are not attacked by X:
Figure shows some of the key notions discussed in Dung (Citation1995). Note that a stable extension is also a preferred extension (Lemma 15 in Dung (Citation1995)) and, by definition, a preferred extension is also complete, a complete extension is also admissible, and an admissible set is conflict-free and acceptable, but not vice versa.
Figure 1. Some key notions in abstract argumentation theory (Dung, Citation1995) (Table from Grossi, Citation2012).
![Figure 1. Some key notions in abstract argumentation theory (Dung, Citation1995) (Table from Grossi, Citation2012).](/cms/asset/50ef960b-0e97-4b08-8343-1527a2489b68/tncl_a_1457254_f0001_b.gif)
In this paper, a special class of argumentation graphs called uncontroversial (Dung, Citation1995, Definition 32) will play an important role.
Definition 2.3:
[Uncontroversial argumentation graphs] Given an argument in an argumentation graph
, let
(resp.,
) be the set of arguments in
such that
(
) if and only if there is a sequence of arguments
where
,
and
for any
and n is even (odd).
An argument in
is said to be controversial with respect to another argument s if
both attacks and defends s (i.e.
). An argumentation graph is uncontroversial if none of its arguments is controversial with respect to any argument.
As an example, consider the argumentation graph below: argument is controversial with respect to both
and
, as it attacks them (it attacks
by attacking one of
’s defender, namely
, and it attacks
directly) but also defends them (by attacking one of their attackers,
and
respectively).
It has been proved [Theorem 33]dung1995 that every uncontroversial argumentation graph is not only coherent (each preferred extension is also stable), but also relatively grounded (the intersection of all preferred extensions is the grounded extension). Here are two further results about uncontroversial argumentation graphs that will be useful for this work.
Proposition 2.1:
Given an uncontroversial argumentation graph and an argument s in
, there is an admissible set of arguments X with
if and only if
, with
the greatest fixed point of the function d.
Corollary 2.1:
Given any uncontroversial argumentation graph and any argument s in
, the union of all the preferred extensions is the greatest fixed point of the defence function d.
3. Making explicit the supported/attacked propositions
The abstract argumentation graphs provides us with tools for defining different notions of argument acceptability. However, as each argument is itself an abstract undefined entity, it is not possible to say whether an argument supports a given claim; similarly, it is also not possible to decide whether an attack between arguments is relevant to the claim at stake. Thus, there is not enough information to decide whether the argumentation structure as a whole ‘supports’ a given proposition or its negation.
3.1. Argumentation-support frame
Our new semantic structure extends an argumentation graph by providing the missing information about the main propositional content of the arguments. Moreover, it also adds a set of possible worlds to the structure, in order to define not only the propositions involved, but also the relationship between them. The result, called an argumentation-support frame, is defined below.
Definition 3.1:
[Argumentation-Support Frame (ASF)] An argumentation-support frame is a structure where
W is a non-empty set of possible worlds and
a non-empty set of arguments;
is an attack relation labelled by propositions
;
is a function assigning to each argument
a subset of W such that, for any
,
.
Intuitively, the set in
contains all the arguments available to our implicit agent, with each argument s supporting those propositions that are true in all worlds in f(s); thus, the set of propositions supported by
is given by
. The restriction
simply states that no argument supports a direct contradiction. With respect to attacks between arguments, there are now several attack relations, each one of them labelled by propositions
.Footnote2
For the interpretation,
indicates that s is attacked by
on whether P is the case.
In order to model the way a rational agent may reason about binary arguments, we impose the following conditions on the given frame structure:
(1) |
| ||||||||||||||||
(2) | if
| ||||||||||||||||
(3) | if |
Note that the interpretation of the labels on the attack relations indicates that only the binary argumentative reasoning of an agent is considered in our framework. Of course, we do not claim that the agent’s argumentative reasoning can only be on binary issues; still, for simplicity, those more general cases are left outside the range of our framework.
Here is an example of an argumentation-support frame.
Example 3.1:
Concerning an issue of ‘what kind of animal is the one in the picture’, suppose the agent has available the following three arguments (,
,
), each one of them supporting a possible answer (bird, mammal, reptile).
: The animal in the picture has wings, so it is a bird.
: The animal looks like a bat, so it is not a bird, it is a mammal.
: The animal looks like a pterosaur, so it is neither a bird nor a mammal, it is a reptile.
and the support function as
Figure shows the ASF, with some labels of the attack relation omitted. The reader can verify that it indeed satisfies the three conditions listed above.
3.2. Beliefs supported by arguments
Within an argumentation-support frame, it is possible to define a notion of belief in terms of the global behaviour of the involved arguments (which may be in conflict with one another). First, some useful definitions and observations.
3.2.1. Acceptable argument for P
A given ASF contains a set of argumentation graphs, one for each proposition
:
As advanced, the ‘binary argument’ requirements discussed above (Page 5) have an important consequence: the set contains only uncontroversial argumentation graphs.
Proposition 3.1:
Given an ASF , every
is an uncontroversial argumentation graph.
Proof It follows from the fact that, due to the properties should satisfy, each attack relation
in
(and thus the attack relation of each
) relates arguments that hold opposite stands on P’s truth value. Hence, given any argument s in
, while the set
contains only arguments that agree with s on P’s truth value (they are at an even distance), the set
contains only arguments that have s’s opposite views about P (they are at an odd distance). As no argument can support both P and
(recall that this is excluded by our frame condition
), no argument can be in the intersection of
and
, and thus
is uncontroversial.
Thus, the conditions of the attack relation imply the uncontroversiality of our argumentation framework. The readers can judge whether the conditions and its consequences are reasonable. For those who take controversiality to be an important feature of arguments, notice how our setting does not rule it out completely; the phenomena can occur, as long as it with respect to different issues.
Note how the only difference of the support-argumentation based graphs from the ones in Definition 2.1 is that each specifies what issue the argumentation is about. For example, the argumentation graph
represents a discussion on the issue of whether P is the case. This, together with the function f in
, allows us to define notions that are similar to those in abstract argumentation theory (see Figure ), now relative to specific propositions. Thus, we can provide the following definition.
Definition 3.2:
[Acceptable argument for P] Given an ASF and an argument s in
, s is an acceptable argument for P if and only if
(i.e. it supports P) and there is an admissible set of arguments X in
such that
(i.e. s belongs to a set of arguments that do not attack each other and defend themselves).
This is one of the key definitions of this paper: an argument is acceptable for a proposition P whenever the argument belongs to an admissible set in the argumentation graph for P. Then, by Proposition 2.1 and the uncontroversiality of support-argumentation based graphs, an argument is acceptable for P whenever the argument belongs to the greatest fixed point of the defence function d, .Footnote5
This gives us an advantage that Section 4 will make use of: within a formal language, it is possible to express this notion of acceptable argument in terms of truth-conditions involving a greatest fixed point, a concept for which there are formal tools available in the literature.
The proposition below reveals logical properties of the notion of acceptable argument.
Proposition 3.2:
Given any ASF and any argument s in
,
(a) | s is an acceptable argument for W; | ||||
(b) | if s is an acceptable argument for | ||||
(c) | it does not hold that ‘if the given s is an acceptable argument for |
Proof
(a) | No argument can attack another on W, as otherwise one of involved arguments would support | ||||
(b) | Since s is an acceptable argument for P, there is an admissible set X in | ||||
(c) | The diagram below (with the set of worlds supported by each argument listed next to each node) shows a counterexample, with |
3.2.2. Belief
With the notion of acceptable argument for a proposition P already defined, we propose the following argument-based definition for the notion of belief.
Definition 3.3:
[Belief] Given an ASF , the agent believes P in
if and only if there is an acceptable argument for P and there is no acceptable argument for
.
Because of its definition, the notion of belief inherits some properties (Proposition 3.2) from the notion of acceptable argument.
Corollary 3.1:
Given any ASF and any
,
(a) | the agent believes W; | ||||
(b) | if the agent believes P, then she also believes Q, for any | ||||
(c) | even if the agent believes P and believes Q, she may not believe |
Note how, in particular, there might be different reasons for the fact that beliefs in this setting are not closed under intersection (i.e. conjunction). A simple one is the fact that there may not be arguments supporting , even if there are arguments supporting P and arguments supporting Q. Moreover, even if there are arguments supporting both P and Q, the acceptability for arguments for
is evaluated neither in the argumentation graph
nor in
, but rather in
, a structure that might not contain acceptable arguments (for
). The counterexample presented for item (c) in the proof of Proposition 3.2 illustrates this situation and it also shows how there might be argumentation-support frames in which the agent believes
while also believing both P and Q. In the philosophical literature a number of discussions can be found on whether beliefs should be closed under conjunction, and arguments against it are often motivated by paradoxical situations such as e.g. the famous lottery paradox.
For a systematic way of exploring the properties of the defined notion of belief as well as other related argumentative theoretic notions, the following section proposes a logic to describe and reason about argumentation-support frameworks.
4. Argument-based belief logic
In this section, we present the argument-based belief logic. There have been some studies of abstract argumentation theory from the perspective of modal logic (Grossi, Citation2010b; Grossi, Citation2010; Grossi, Citation2012; Grossi, Citation2013; Grossi & van der Hoek, Citation2014). Especially in Grossi and van der Hoek (Citation2014), the relation between belief and argument is studied in a two-dimensional modal logic. However, in this two-dimensional modal logic, even when the authors study the interaction between beliefs and arguments, the very notion of belief itself is still defined by the doxastic relation rather than in terms of arguments. This aspect is different in the present work where belief emerges as a derived modality. Our logic also has a flavor of two-dimensional logic which is blended with ingredients from modal -calculus and configured to fit the need of characterising the notion of argument-based belief.
4.1. Syntax
Definition 4.1:
Let be a non-empty set of atomic propositions.
is the language generated by the following grammar:
where . Symbols
and
are abbreviations of
and
, respectively.
The language is divided into two parts. While -formulas (the
part of the language) are used to state facts about possible worlds,
-formulas (the
part) are dedicated to the description of arguments. When there is no need to make distinction,
is used to denote formulas in the whole language
.
As it will be seen, is a universal operator quantifying over possible worlds; it can be taken as an S5-knowledge operator. Analogously,
is a universal operator quantifying over arguments, so
states that, for all arguments,
is the case.Footnote6
Formulas of the form
state that the current argument supports
, and those of the form
state that all arguments which directly attack the current one on
satisfy
. Finally,
sates that the current argument is acceptable in the argumentation on
.
Remark 4.1:
The language allows interaction between - and
-formulas. For example,
expresses that there is an argument supporting p. However, the interaction between these two types of formulas is limited. For example, strings as
,
are not formulas of our language. In the first,
expresses a fact about possible worlds (it is an
-formula), so we cannot use it to describe arguments; in the second,
describes a property of certain arguments (it is a
-formula), and as such it is not a fact about possible worlds that can be supported by arguments.
4.2. Semantics
By adding a valuation function to the argumentation-support frame, we get the argumentation-support model, where formulas in can be evaluated.
Definition 4.2:
An argumentation-support model is a tuple where
is an argumentation-support frame and
is an valuation function which assigns to each atomic proposition a set of possible worlds (those in which it is true).
Let be an argumentation-support model, and define
(the subscript
will be omitted whenever possible).Footnote7
The truth of
is defined as follows:
Definition 4.3:
Given an argumentation-claim model ,
iff
iff
iff
and
iff for all
iff for all
iff
iff for any
such that
.
iff s is in an admissible set of arguments relative to
.
We say a formula is satisfied in an argumentation-support model
if there is a pair (w, s) in
such that
. A formula
is valid in
(
) if for any pair (w, s) in
we have
. Finally,
is valid in the whole class of argumentation-support models (
) if it is valid in every argumentation-support model.
Note how the -formula
expresses that the agent has an acceptable argument for a given
. Therefore, the notion of belief can be defined in
as follows:
As we have shown in Corollary 3.1, our notion of belief satisfies the following properties in the class of argumentation-support models:
Fact 4.1:
Thus, although the agent’s beliefs are closed upward (the validity of ), they are not closed under conjunction introduction (
is not valid). Moreover, beliefs are consistent and contain all validities.
Fact 4.2:
Note that the language allows us to express higher-order beliefs: and
are formulas in
. In fact, for our notion of belief, the following two properties hold:
Fact 4.3:
It is also worthwhile to notice how, by Propositions 2.1 and 3.1, we have an equivalent truth condition for in the argumentation-support models:
This paves the way for looking for a sound and complete axiom system for our logic, which will be presented next.
4.3. Axiom system
The following is an axiom system (called AB) for the argument-based belief logic. Axioms for indicate that this operator amounts to the greatest fixed point of d.
• | All the propositional tautologies. | ||||||||||||||||||||||
• | Modus ponens | ||||||||||||||||||||||
• | S5 and Necessitation rule for | ||||||||||||||||||||||
• | For
| ||||||||||||||||||||||
• | For
| ||||||||||||||||||||||
• | For
|
• | For
| ||||||||||||||||||||||||||||
• | Interaction between
| ||||||||||||||||||||||||||||
Interaction between
| |||||||||||||||||||||||||||||
• | interaction between
|
Theorem 4.1:
The system AB is sound and weakly complete for the argument-based belief logic.
Soundness follows from the fact9An element is a fixed point of a function
if and only if
. If a partial order
on D is also provided, x is a postfix point if
, and it is the greatest fixed point if it is greater or equal that any other fixed point. When f is defined over the powerset of a given set D, as the functions d and n above, a fixed point is defined as before, and the subset order over
can be used for defining the greatest fixed point. For more about fixed points, the reader is referred to Chapter 1 of Arnold and Niwinski (Citation2001). that axioms and rules in AD are valid and validity preserving, respectively10Note that
will play the role of the labels of attack relations in the quasi argumentation-support model.. We prove the validity of Axiom 3 as an example.
Proposition 4.1:
[Validity of Axiom 3]
Proof Given an argumentation-claim model , take a pair (w, s) where
holds. The first conjunct tells us that
, the second implies that
, and the third indicates that there is an argument
such that
and
. These three facts, together with condition (3), entail
, which implies that
For (weak) completeness, the general strategy is, as usual, to show that every consistent formula is satisfiable in a model. The outline of the proof is similar to the standard proof of completeness in the sense of using maximal consistent sets to build the model. However, the process and details of the whole proof are not fully straightforward, because the model is two-dimensional and the attack relations are labeled by different subsets of possible worlds which satisfy certain conditions. Moreover, the language includes an operator for the greatest fixed point of the defence function. Therefore, we stress some key points in our proof here. The full proof can be found in the appendix, but here are some important details.
First, notice that although the argumentation-support model is two-dimensional, the syntax restricts the interaction between these two dimensions. For example, strings as are not formulas in our language:
is an
-formula, but
is not. So
is a consistent set in our logic (with consistency defined, in the standard way, as the non-derivability of the always false
), even though no pair (w, s) in an argumentation-support model satisfies both
and
. This is a two-edged sword. On the one hand, it gives us the flexibility to construct maximal consistent sets for
-formulas and
-formulas separately and put them together in the model. On the other hand, we have to use some devious ways to ensure that the constructed model respects satisfiability.
Second, note that we need to construct the attack relations labelled by all subsets of possible worlds. However, we may not have enough information about them given the formulas in our hands, which are generated from the subformulas of a given formula . This means we can only construct the model partially. Therefore, we have to prove that any such kind of partial model (we call them quasi argumentation-support models in the proof as defined in Definition A) can be extended to a full and real argumentation-support model. Moreover, the extended model should be modally equivalent to the original model with respect to all the formulas we care about.
Third, the proof for the case of in the truth lemma is worth some attention. It is not as straightforward as other cases. We have to prove that the information about the greatest fixed point in the quasi argumentation-support models given by those maximally consistent sets matches the information given by the quasi argumentation-support models itself. The readers can find the details of how axiom Unfold and the inference rule R are applied in the proof.
Fourth, note that the model we build in the proof is finite, both in its set of worlds and in its set of arguments: thus, our logic has the finite model property. This, together with (i) the decidability of the ‘being a model’ property (the ‘binary argument’ requirements of Page 5 are decidable on finite models) , (ii) the enumerability of models ( is a binary relation on arguments for each subset of worlds P, and f is a function from arguments to sets of worlds), and (iii) the decidability of the semantic satisfiability conditions (the fixed point condition is decidable), shows that our logic is decidable.
4.4. Discussion
For space reasons, an extensive discussion on both concrete applications of the presented framework and, more generally, the idea of argument-based beliefs, are left out. Still, for applications, one can briefly mention Shi (Citation2016), where the logic is used not only to discuss the notion of distributed belief, but also to analyse a ‘two-player argumentation game’, illustrating how a single agent’s belief and the group’s distributed belief are decided by the corresponding argumentation. For a deeper discussion about using arguments (and, more generally, using evidence/justifications) for supporting beliefs, the reader is referred to Baltag et al. (Citation2014), *BaltagEtAl2016evidPP and (Shi, Smets, and Velázquez-Quesada, Citation2017).
5. Conclusion
We have provided the first steps in the analysis of beliefs based on binary arguments which either support a given propositional claim or its negation. We offered a complete axiom system for this logic and have shown that this logic is decidable. The proposition-labeled attack relation in our setting does come with a specific interpretation when we apply it to real argumentation scenarios. In particular the attack relation on wether proposition P holds, is to be interpreted as a direct attack on the conclusion of the reasoning that establishes P. If we refine the setting and allow indirect attacks that undermine for instance a given premise that leads up to a conclusion P, the setting we have presented needs to be further refined. Another aspect we have not explored in this paper deals with combined arguments of claims that together provide the support in favor or against their conjunction. The study of combined arguments ties in nicely with an ongoing project by the authors on a topological setting that provides a semantics for arguments (Shi et al., Citation2017), very much in the spirit of the topological semantics for evidence-based beliefs in Baltag et al. (Citation2016a). Moreover, a multi-agent extension of some of the ideas presented in this paper has been provided in Shi (Citation2016), in order to deal with argumentation games and the notion of distributed belief.
Acknowledgements
The authors are grateful for comments received from Johan van Benthem and Alexandru Baltag on earlier versions of this work.
Disclosure statement
No potential conflict of interest was reported by the authors.
Additional information
Funding
Notes
1 Still, as one reviewer correctly pointed out, Dung (Citation1995) addresses this connection indirectly, by showing that many of the major approaches to nonmonotonic reasoning in AI and logic programming, which can be understood as a form of reasoning that creates beliefs, are different forms of argumentation.
2 The idea of working with accessibility relations labelled by propositions is used in the literature on conditional logic and in particular in the context of logics for belief revision (Baltag & Smets, Citation2008; Baltag & Smets, Citation2006a; Baltag & Smets, Citation2006b).
3 The set denotes, as usual, the complement of P (i.e.
).
4 This interpretation can be justified by the fact that, while only states its ‘positive’ conclusion (‘it is a bird’),
and
take the time to explicitly reject other alternatives. Of course, changes in the paraphrasing might produce different interpretations. The point of the example is not to establish a unique formalisation of the given natural language scenario, but rather to show how our setting can be used to represent this and other similar situations.
5 Note how, by Corollary 2.1, is equal to the union of all the preferred extensions. This could suggest an alternative definition of this notion of acceptability, not in terms of the union of all preferred extensions (the greatest fixed point), but rather in terms of the intersection of them (which, by Dung, Citation1995, Theorem 33, is equal to the least fixed point of d). However, such intersection might be empty, and therefore no argument would be acceptable for P, even in the presence of preferred extensions containing arguments supporting P. For this reason, this paper will work with the notion of acceptability as defined above (Definition 3.2).
6 Still, expresses facts about possible worlds, as the (non-)existence of arguments with certain features (what
expresses) is not a feature of any specific argument.
7 A notational alternative for the worlds in which an -formula holds,
, would be to use
to represent a subset of
(as formulas are evaluated on pairs (w, s)), and then use projection functions to extract its W- and
-components. We stick to the use of
for denoting directly a subset of W, as the
-component of the set or pairs is not used.
8 The completeness proof is not related to the completeness proof for the -calculus (Walukiewicz, Citation2000); it is rather close to the completeness proofs for the until/since operators in temporal logics (Burgess, Citation1982) and the common knowledge operator in epistemic logics (Fagin, Moses, Vardi, & Halpern, Citation1995).
10 An element is a fixed point of a function
if and only if
. If a partial order
on D is also provided, x is a postfix point if
, and it is the greatest fixed point if it is greater or equal that any other fixed point. When f is defined over the powerset of a given set D, as the functions d and n above, a fixed point is defined as before, and the subset order over
can be used for defining the greatest fixed point. For more about fixed points, the reader is referred to Chapter 1 of Arnold and Niwinski (Citation2001).
11 Note that will play the role of the labels of attack relations in the quasi argumentation-support model.
References
- Arnold, A. & Niwinski, D. (2001). Rudiments of μ-calculus . Amsterdam: Elsevier.
- Artemov, S. N. (2008). The logic of justification. Review of Symbolic Logic , 1 (4), 477–513.
- Artemov, S. N. , & Nogina, E. (2005). Introducing justification into epistemic logic. Journal of Logic and Computation , 15 (6), 1059–1073.
- Baltag, A. , Bezhanishvili, N. , Özgün, A. & Smets, S. (2016a). Justified belief and the topology of evidence. In Väänänen, J. A. , Hirvonen, Å , & de Queiroz, R. J. G. B. (Eds.) Logic, Language, Information, and Computation -– 23rd International Workshop WoLLIC 2016. Proceedings volume . Lecture notes in computer science. (pp. 83–103). Heidelberg.
- Baltag, A. , Bezhanishvili, N. , Özgün, A. , & Smets, S. (2016b). Justified belief and the topology of evidence. Technical Report PP-2016-21, Institute for Logic, Language and Computation. Heidelberg.
- Baltag, A. , Fiutek, V. & Smets, S. (2016). Beliefs and evidence in justification models. Beklemishev, D.L. , & Mate, A. (Eds.), Advances in modal logic . College Publications. (pp. 156–176)
- Baltag, A. , Renne, B. , & Smets, S. (2012). The logic of justified belief change, soft evidence and defeasible knowledge. 19th Workshop on Logic. Language, Information and Computation , 7456 , 168–190.
- Baltag, A. , Renne, B. , & Smets, S. (2014). The logic of justified belief, explicit knowledge and conclusive evidence. Annals of Pure and Applied Logic , 165 (1), 49–81.
- Baltag, A. , & Smets, S. (2008). A qualitative theory of dynamic interactive belief revision. Texts in logic and games , 3 , 9–58.
- Baltag, A. , & Smets, S. (2006a). Conditional doxastic models: A qualitative approach to dynamic belief revision. In G. Mints & R. de Queiroz (Eds.), Proceedings WOLLIC 2006, Electronic Notes in Theoretical Computer Science , Vol. 165 (pp. 5–21).
- Baltag, A. , & Smets, S. (2006b). Dynamic belief revision over multi-agent plausibility models. In Bonanno, W.G. , & van der Hoek, W. (Eds.), Proceedings 7th Conference on Logic and the Foundations of Game and Decision (LOFT 2006) (pp. 11–16). Liverpool.
- Blackburn, P. , de Rijke, M. , & Venema, Y. (2001). Modal logic . Cambridge: Cambridge University Press.
- Burgess, J. P. (1982). Axioms for tense logic. i. ‘since’ and ‘until’. Notre Dame Journal of Formal Logic , 23 (4), 367–374.
- 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.
- Dyrkolbotn, S. (2013). On a formal connection between truth, argumentation and belief. In M. Colinet , S. Katrenko , & R. K. Rendsvig (Eds.), ESSLLI 2012 and ESSLLI 2013 Student Sessions. Selected Papers . Lecture notes in computer science (vol. 8601, pp. 69–90). Heidelberg.
- Dyrkolbotn, S. , & Walicki, M. (2014). Propositional discourse logic. Synthese , 191 (5), 863–899.
- Fagin, R. , Moses, Y. , Vardi, M. Y. , & Halpern, J. Y. (1995). Reasoning about knowledge . Cambridge: MIT Press.
- Grossi, D. (2010b). On the logic of argumentation theory . Toronto: Proceedings AAMAS 2010.
- Grossi, D. (2012). Fixpoints and iterated updates in abstract argumentation. Proceedings of 13th International Conference KR . Rome.
- Grossi, D. (2013). Abstract argument games via modal logic. Synthese , 190 , 5–29.
- Grossi, D. (2010). Argumentation in the view of modal logic. In P. McBurney , I. Rahwan , & S. Parsons (Eds.), Argumentation in Multi-Agent Systems -- 7th International Workshop, ArgMAS 2010 Revised, Selected and Invited Papers , Lecture notes in computer science (Vol. 6614, pp. 190–208). Heidelberg: Springer. 10.1007/978-3-642-21940-5\_12
- Grossi, D. , & van der Hoek, W. (2014). Justified beliefs by justified arguments. Proceedings of the 14th International Conference KR . Vienna.
- Knaster, B. (1928). Un théorème sur les fonctions d’ensembles. Annales de la Société Polonaise de Mathématiques , 6 , 133–134.
- Kozen, D. (1983). Results on the propositional mu-calculus. Theoretical Computer Science , 27 , 333–354.
- Lorenz, K. (1961). Arithmetik und Logik als Spiele (PhD thesis). Universität Kiel.
- Lorenzen, P. (1958). Logik und agon . Arti del XII Congresso Internationale de Filosofia, Venezia (pp. 187--194). Reprinted in Lorenzen and Lorenz (1978) (pp. 187–194). Venezia.
- Lorenzen, P. , & Lorenz, K. (1978). Dialogische logik . Darmstadt: Wissenschaftliche Buchgesellschaft.
- Schwarzentruber, F. , Vesic, S. , & Rienstra, T. (2012). Building an epistemic logic for argumentation . Proceedings JELIA’12 (pp. 359–371). Heidelberg.
- Shi, C. (2016). Multi-agent epistemic argumentation logic , ESSLLI 2016 Student Sessionb (pp. 111–122). Bozen-Bolzano.
- Shi, C. , Smets, S. , & Velázquez-Quesada, F. R. (2017). Argument-based belief in topological structures. In J. Lang (Ed.), Proceedings TARK 2017, volume 251 of Electronic proceedings in theoretical computer science (pp. 489–503). Open Publishing Association.
- Tarski, A. (1955). A lattice-theoretical theorem and its applications. Pacific Journal of Mathematics , 5 (2), 285–309.
- Toulmin, S. E. (2003). The uses of argument (2nd ed.). Cambridge: Cambridge University Press.
- van Benthem, J. (2007). Dynamic logic for belief revsion. Journal of applied non-classical logics , 12 (2), 129–155.
- van Benthem, J. (2011). Logical dynamics of information and interaction . Cambridge: Cambridge University Press.
- van Benthem, J. , Fernández-Duque, D. , & Pacuit, E. (2014). Evidence and plausibility in neighborhood structures. Annals of Pure and Applied Logic , 165 (1), 106–133.
- van Benthem, J. , Fernández-Duque, D. , & Pacuit, E. (2012). Evidence logic: A new look at neighborhood structures. In T. Bolander , T. Braüner , S. Ghilardi , & L. Moss (Eds.), Advances in modal logic , ( Vol. 9, pp. 97–118). London: King’s College.
- van Ditmarsch, H. , van Der Hoek, W. , & Kooi, B. (2007). Dynamic epistemic logic . Dordrecht: Springer.
- Walukiewicz, I. (2000). Completeness of kozen’s axiomatisation of the propositional μ-calculus. Information and Computation , 157 (1–2), 142–182.
Appendix 1
Proof of Proposition 2.1
Proof () The Knaster-Tarski fixpoint theorem (Knaster, Citation1928; Tarski, Citation1955) states that
is the union of all d’s postfix points,
.Footnote10
Hence, as any admissible set X is, by definition, a postfix point of d, we have
and thus
implies
.
() Take any
and define
; it is enough to show that X is an admissible set containing s, i.e.
,
and
. For the first, observe that any two arguments
are, by definition, also in
. Thus, each one of them is at an even distance from s, and hence cannot attack each other (as otherwise the attacker would be at an odd distance from s, which is impossible as
is uncontroversial). Therefore,
. For the second, take any argument x attacking some
. Since
, there must be
such that
(recall,
is a fixed point of d, so
); hence,
. But then, as
(by X’s definition) and
, it follows that
, that is,
(by X’s definition). Summarising, every argument x attacking some argument (
) in X is in turn attacked by an argument (
) that belongs to X; thus,
. For the third, since clearly
,
implies
.
Completeness of the AB system
In this section we show that for any ,
We first define the quasi argumentation-support model and then extend it to an argumentation-support model.
Definition A:
[Quasi Argumentation-Support Model] A quasi argumentation-support model is a structure
where
and V are defined as in the argumentation-support model, and X is closed under complement, i.e. if
, then
. Moreover, it satisfies a restricted version of the conditions we impose on the argumentation-support model:
For any
,
if and only if
.
For any
, if
,
either
or
; and
implies
.
For any
, if
and
, then
.
In words, a quasi argumentation-support model is simply an argumentation-support model that only ‘discusses’ propositions in X, and therefore only needs to satisfy the frame conditions relative elements of X. Clearly, any argumentation-support model is a quasi argumentation-support model; for the other direction, we have the follow proposition
Lemma A:
Any quasi argumentation-support model can be extended to an argumentation-support model.
Proof We define the relation for any
as follows:
We claim that the model generated by adding these attacking relations into is an argumentation-support model. To prove this claim, we only need to check that it satisfies the four frame conditions.
1: |
| ||||||||||||||||||||||||||||
2(a): | if | ||||||||||||||||||||||||||||
2(b): | if | ||||||||||||||||||||||||||||
3: | if
|
Given a formula , we define
in the following formula:
A set of formulas X is closed under single negation if and only if belongs to X whenever
.
Definition B:
Let X be a set of formulas. The set X is FL-closed if and only if it is closed under subformulas (e.g. if , then
) and it satisfies the following additional constraints:
if
, then
;
if
, then
.
Next, we build the canonical model starting by constructing maximal consistent sets. Given our two kinds of formulas, -formulas and
-formulas, an intricate coordination between them is required during the construction.
Definition C:
Let be a set of formulas. We define
as the smallest set containing
which is FL-closed and closed under single negations. And
is the smallest set containing
which satisfies the following two condition:
if
, then
and
;
if
, then
and
;
Definition D:
(Atoms) Let be a set of formulas.
A set of formulas
is an atom over
if it is a maximal consistent subsets of
. The set
contains all the atoms over
.
A set of formulas A is an
-atom over
if it is a maximal consistent subsets of
. The set
contains all
-atoms over
.
A set of formulas B is an
-atom over
if it is a maximal consistent subsets of
. The set
contains all
-atoms over
.
Fact A:
If A is an
-atom over
and B is a
-atom over
, then
is an atom over
;
If
is an atom over
, then
is an
-atom and
is a
-atom.
Proof For the first, we know that is AB-consistent; thus, we only need to prove that any X satisfying
is inconsistent. This is obvious, since any
with
is either an
-formula or
-formula. Without loss of generality we can assume it is an
-formula; since A is an
-atom over
, the set
must be AB-inconsistent. Thus, X is also AB-inconsistent.
For the second, suppose is not an
-atom. Since A is consistent, there is an
-formula
not in A such that
is still consistent, and thus
is also consistent. But
implies
, and thus this contradicts the maximality of
. Therefore,
must be an
-atom. The argument for
is similar.
Lemma B:
If and
is consistent, then there is a
such that
.
The proof of Lemma B, an analogue of Lindenbaum’s Lemma, follows the same argument as the proof of Lemma 4.83 of (Blackburn, de Rijke, and Venema, Citation2001). Together with the second fact of Fact A, it implies the following lemmas:
Lemma C:
If
and
is consistent, then there is a
such that
.
If
and
is consistent, then there is a
such that
.
We can now fix a formula and construct the canonical model for it, which will be proved to be a quasi argumentation-support model. Before doing so, here is first some useful notation.
Notation A:
Let X and be sets of formulas.
If X is finite, define
.
For any
, define the sets
If X is finite, define also
When
is a singleton
, the set
will be abbreviated as
.
Second, the following proof shows a property required by the definition of our canonical model.
Lemma D:
Given a consistent , there is
such that
and
.
Proof
The proof is divided into two cases.
First, if is an
-formula then, by Lemma C (a), there is an
-atom A such that
, due to its consistency. Note that
is consistent (otherwise,
, contradicting axiom D). Thus, by this and the fact that
(Lemma C (b)), there is a
-atom B such that
, which implies that
. By Fact A,
.
Second, if is a
-formula, suppose that there is no
such that
and
. Then there is no
-atom A such that
is consistent. (Otherwise,
can be extended to a
-atom by Lemma C (b), and by Fact A
is an atom over
: a contradiction.)
Now take the -formula
. It can be proved that
is consistent. (Otherwise,
, which implies that
. Since
and
, it follows that
, which implies that
is inconsistent; a contradiction.) Since
is an
-formula, from the first auxiliary result it follows that there is an atom over
, say
, such that
and
.
Next, take . It can be shown that
is an atom over
(i.e.
). So take the
-atom
. Our supposition implies the inconsistency of
, as we have shown at the beginning. However, this implies that
is inconsistent.
implies that
. By the definition of
,
. Thus, we have
. Since
is inconsistent, it follows that
is inconsistent, contradicting the
’s consistency.
Here is, then, the definition of the canonical model for .
Definition E:
[Canonical Model over ] Take any
satisfying both
and
(by Lemma D, such
exists). The canonical model over
is the structure
givenFootnote11 by
;
;
;
if and only if
is consistent;
for any
,
if and only if
is consistent;
We first prove four existence lemmas for ,
,
and
. During the proof, we will use the following abbreviations:
Lemma E:
In the canonical model, for any ,
if and only if there is an
-atom
such that
.
Proof Assume that where
. We show that
is consistent. Suppose not; then
. By applying the necessitation rule, we have
. By axiom 4 and 5 for
and
, we have
. By Axioms
1,
2 and
, we have
. Together with
, it implies
, a contradiction. Therefore, we can extend
to an
-atom over
,
, such that
. Moreover,
and
, so
.
For the other direction, assume there is a -atom
such that
. It follows immediately that
. (Otherwise, by
and axiom T for
, we have
, which contradicts the assumption
.)
Lemma F:
In the canonical model,
Proof As the direction is obvious, we focus on the
direction. Assume
but
; we will show that there is a
such that
. This amounts to show that
is consistent. Suppose not; then
. Since for any
, we have
so
. By
, it follows that
, which implies that
by the definition of
. However, this is contradictory to the assumption that
. So there must be a
such that
. Therefore,
.
Lemma G:
[Existence Lemma for -formulas] In the canonical model, for any
,
if and only if there is a
-atom
such that there is
such that
.
Proof Assume ; we will show that
can be extended to an
-atom
such that
is consistent. For this we follow the argument of (Blackburn et al. (Citation2001), Lemma 4.86) and construct an appropriate
-atom A by forcing choices. So, enumerate the formulas in
as
, and define
as
, with YN as above.
We first prove that is consistent. Suppose otherwise; then
and
. Thus,
, which implies that
. It follows that
and, since
, we have
.
In order to get a contradiction, we now proceed to prove that we also have . The proof can be divided into four parts specified as follows.
By Axiom I1,
. Together with the construction of DY and
, this implies that
. Thus,
.
By Axiom I1 and axiom 5 for
,
. Together with the construction of DN and
, this implies that
. Thus,
.
By Axiom I1 and Axiom
1,
. Together with the construction of EY and
, this implies that
. Hence,
.
By Axiom I1 and Axiom
2,
. Together with the construction of EN and
, this implies that
. Hence,
.
Now, in order to extend the consistent , suppose as an inductive hypothesis that
is defined such that
is consistent (
). Then
and thus . Therefore, either for
or for
, we have
is consistent. By choosing
to be the consistent expansion, and by letting A be
, we have that
is consistent.
Thus, suppose there is an -atom
such that
; then
is consistent, which implies that
is consistent. Since
and B is
-atom over
(and hence maximal consistent in
), we must have
.
Lemma H:
[Existence Lemma for -formulas] In the canonical model, for any
,
if and only if there is a
-atom
such that
and
.
Proof Assume ; we will show that
can be extended to an
-atom
such that
is consistent. We construct an appropriate
-atom
by forcing choices. Enumerate the formulas in
as
; define
as
.
Let . We first prove that
is consistent. Suppose not. By an argument similar to that in Lemma G, we can get
. By rule N for
, we have (1)
. However,
, since
. By Axiom I2,
, which implies that (2)
. But (1) and (2) lead to a contradiction, since
. Therefore,
is consistent.
The induction part to extend is similar to that in the proof of previous lemma, and so is this lemma’s other direction.
Now we are ready to prove the truth lemma.
Lemma I:
[Truth Lemma] Let be the canonical model over
. For any
,
Proof We proceed by induction on the degree of .
For
,
and
and
, so it is trivially satisfied. For atomic propositions p, we have
if and only if
if and only if
if and only if
.
For the Boolean cases, there are two cases: one for
-formula and one for
-formula. In both, the proof is routine.
For the four modal operators, the proof uses their respective existence lemmas. Here, as an example, we only deal with the universal modality on the set of arguments. Assume that
; by its truth definition, for any
,
. By induction hypothesis,
for any
, which implies that
. (Note that
and
imply
by Axiom I1, Axiom
1 and the constructions of both
and
, using similar arguments specified in (1)-(4) in Lemma A.6). Since
, we have
. For the other direction, use
.
For the case of
, the proof goes as follows. For the first direction, assume that
; define
and
. Let
denote
, and define
. We will use
to denote
. Claim one:
if and only if there is a
such that
.
Claim two: for any
we have
. Suppose not. Then
is consistent, which implies that
is consistent. So there must be one
such that
is consistent. Furthermore, there must be one
such that
is consistent. By the existence lemma for
, there must be one
such that
and
. However, this is impossible, since
by the definition of
. Therefore,
. Claim three:
. Suppose not. Then
is consistent. Thus there must be an
such that
is consistent, which implies that there is no
such that
is consistent. Hence, there is no
such that
. However, by Claim one and
, there is a
such that
. Since
, for any
such that
, there is
such that
. Because
,
. Hence
and
, which implies that
is consistent by
. Contradiction! Claim four:
. Suppose not. Then
is consistent, which implies that there is
such that
is consistent. By Claim two,
. By
, the consistency of
implies that
is consistent. Thus there must be a
such that
is consistent. However, this means that
. Since
, by Claim one, it follow that
, contradictory to the fact that
. Therefore,
. Claim five:
. By rule N for
on Claim three, we have
. Together with Claim four, it implies that
. By rule R on
we have
. Since
by the definition of
and
by the definition of GFP and the assumption that
, we have
. Recall that
. By
, we have
. Together with
, it follows that
, which gives us that
. For the other direction, assume
and take
. We first show that G is a postfix point for
, with
. Take any
. Since
, by Unfold we get
. If there is no Y such that
, then
. If there is Y such that
, take any of them. Since
,
. By maximality and
we have
so, by the existence lemma for
, there must be a set Z such that
and
. Thus,
, and therefore
. By the definition of
,
. By the inductive hypothesis,
. Thus,
, which means that
. Therefore, by the truth condition of
,
.
Lemma J:
For any in
, we have
.
Proof For any we have
. By the existence lemma for
, there is a
-atom
such that
. Therefore, for any
,
.
Lemma K:
For any and
, we have
if and only if
.
Proof This follows directly from axiom 1 and the fact that is closed under complement.
Lemma L:
For any and
, if
then either
or else
Proof From it follows that
is consistent. Thus,
is consistent, which implies that
and hence
. Together with axiom 2a,
, it implies that
.
Now take any , we will show that
implies
. Assume both
and
; from
it follows that
is consistent, so
is consistent by
. By
and
, we have
, and therefore,
.
It can be shown by similar argument that if then
.
Lemma M:
For any and
, if
and
, then
.
Proof Assume both and
. It follows that
. Thus, by axiom 2b we have
and hence, for any
such that
, we have
. Since
, we also have
. This implies that, for any
,
. Thus, for any
,
and therefore
.
Lemma N:
For any and
, if
and
, then
.
Proof Take and
. We claim that for any
,
. Suppose not. Then
is consistent, and thus
can be extended to an
-atom Y over
belonging to W. However. this contradicts
. Hence for any
,
. This implies that
.
Now, implies that
is consistent, and
implies that
. Together with
and Axiom 3, they imply that
is consistent. Therefore,
.
We have proved that the canonical model over ,
, is indeed a quasi argumentation-support model. By Lemma A, this structure can be extended to an argumentation-support model. It is only left to prove that this extension, denoted by
, indeed preserves the behaviour of the formulas we are interested in.
Lemma O:
For any ,
Proof The proof proceeds by induction on the degree of . The basic case is trivial, since the extension does not change V. The proof for other cases is also routine, as neither the support functions f nor the attack relations
for
are changed when building the extension.
Thus,
Theorem 1.1:
For any ,
Since by construction the set is finite for any
, it follows that both W and
in
are finite. Therefore, our completeness proof also gives us the finite model property, which implies that our logic is decidable.