Dialogical logic and abstract argumentation frameworks

Two weeks ago I was back in Lisbon for ECAI, and after having attended quite a few talks, tutorials, and workshops on dialogues and argumentation. This has caused me to start thinking about some alternative approaches to dialogical logic, which may or may not turn out to be fruitful in the long run, and I started writing up a blogpost about them. However, I got sidetracked and didn't finish the post until now. Argumentation frameworks (AFs) were introduced in Dung 1995. In their most basic form, an argumentation framework is a pair $\langle X,R\rangle$, where X is a set of arguments and R is a binary relation on X called an attack relation, specifying which arguments are attacks on other arguments. Both the arguments and the attack relation are considered atomic/basic; in an AF, there is no further structure to either, they are just given. AFs have been extended in various ways; one such way is by allowing arguments to attack not just other arguments but also the attack relations themselves. AFs with this functionality are called Extend Argumentation Frameworks. One can think of an attack on an attack relation as a defense against that attack. The notion of attacks and defense in the AF and EAFs parallels, at least superficially, the notion of attack and defense in dialogical logic, so the natural question that arises is whether EAFs could be used to model dialogical logic, and, if so, whether this would give us any new insights. To be more precise: For a given formula $\phi$ we can construct a directed graph $D_\phi$ where the nodes of $D_\phi$ are the subformulae of $\phi$ along with the symbolic attacks ?L, ?R, and ?, and there is an edge from node $x$ to node $x'$ if $x$ is an attack of $x'$, according to the set of particle rules in place. We can then extend this graph to one with edges between nodes and other edges, where there is an edge between node $x$ and edge $e$ iff $x$ is a defense of the attack represented by $e$. Once we've represented a dialogical formula this way, we need to answer the following questions to determine whether this representation is helpful or not: - Such a representation does not keep track of either the player making the move or the round in which it occurs. Do we need to add this information? - Does representing a dialogue in this way differ at all from the tree representation of winning strategies given by Felscher? - Are there properties of these graphs that are worth exploiting; that is, are there any correspondents between properties of the graph and the existence of a winning strategy for P? - If we do introduce labels for players and rounds, then how do we represent the structural rules in terms of constraints on the graphs? For example, D10 would say that for any propositional letter, the label for P must be larger than the label for O. Put this way, it makes me think that if we build in player and round information into the labeling of the edges, we're going to end up with something that is just isomorphic to Felscher's trees, and hence this will not provide us with any new insights. - Even so, it would be interesting to ask if all the (known) structural rules can be expressed as constraints on the labeling. References:

• 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.
• Modgil, S. 2009. "Reasoning about preferences in argumentation frameworks", Artificial Intelligence 173, nos. 9/10: 901-934.

Handling assumptions

I still have a half-written blog post from when I was in Lisbon last week, but I think it will have to wait, as now I'm thinking about something else, namely, how to handle assumptions in dialogical logic. While preparing a short note on the sound proof rules of N, I noticed that none of them have anything on the left-hand side of the turnstile; that is, none of the rules model anything like reasoning from assumptions. At this point, I have no idea if this is something specific to N, because we don't know enough about N, and how much of this is specific to the dialogical approach, which doesn't, on the face of it, allow for any type of reasoning from assumptions. Now what about IL and CL? They have dialogical characterizations and allow reasoning from assumptions, both in their ordinary semantics and in their proof theory. So why is it that they can be dialogically characterized, if ordinary structural/particle rules don't allow for assumptions? My suspicion is that it's because both logics satisfy a deduction theorem -- $\Gamma\vdash\phi$ iff $\vdash\Gamma\rightarrow\phi$, and hence you can "do away" with assumptions. Now, the fact that the proof rule from $\vdash\phi\rightarrow\psi$ infer $\vdash(\gamma\rightarrow\phi)\rightarrow(\gamma\rightarrow\psi)$ is not sound in N shows that N cannot have an ordinary deduction theorem, and so it is important to find a way to handle reasoning from assumptions in N in a dialogical way. Here is a naive approach, which I will ask Jesse to implement so I can test it via the website: - Fix a set of formulas $\Gamma$ such that Proponent can assert $\phi\in\Gamma$ at any time, as either an attack or as a defense. Essentially then $\Gamma\vDash\psi$ says "if you (Opponent) grant me (Proponent) the info in $\Gamma$, I can prove $\psi$ to you. Being that this is a naive approach, I do not know how well it will work. Luckily, since we know how reasoning from assumptions should work in IL and CL, we can use them as test cases for this approach.

Dialogues as decision procedures for intuitionistic logic

Using my code for playing dialogue games, I sometimes search (often prodded by Sara) for winning strategies for concrete formulas in concrete rulesets. Sara asked me today to try, using the so-called E-dialogue rules, to find a winning strategy for a certain formula of interest. The formula has the air of being superintuitionistically valid, and it has 15 connectives, so if there were a winning strategy, it probably would not be discovered without developing the tree to a pretty significant depth. In fact, for the formula that Sara asked about (the implication whose antecedent is the law of weak excluded middle and whose consequent is Scott's formula), a winning strategy (using the E rules) was discovered only at depth 13. She then wondered about the converse of this formula, and I set about developing the game tree to depth 11…12…13…14…with no success. We expect that the formula is actually intuitionistically invalid. My program can reveal that in only one way: by showing that the dialogue tree developed down to a certain depth is such that:

1. every leaf node is expanded (i.e., we considered extending the game at that point, but no moves could be made—we did everything we could within the depth limits), and
2. it is not the case that Proponent can win no matter what Opponent does

Sometimes, for simple formulas, one can develop the dialogue tree in such a way that we can recognize the invalidity in this way (my program returns NIL as the value for the WINNING-STRATEGY function). But such formulas seem to be the exception rather than the rule, at least for the kinds of formulas that interest Sara and me these days. What is more typical is that my exhaustive enumeration program simply fails to decide, at some finite depth, that the formula is invalid. I've coded things so that the program returns the Common Lisp keyword :DIALOGUE-TREE-TOO-SHALLOW, to indicate that the dialogue tree, developed to a certain depth, fails to satisfiy one of the aforementioned pair of conditions. This leads me to wonder about how dialogues could be used as decision procedures for propositonal intuitionistic logic. We know that propositional intuititionistic logic is decidable; in fact, its validity problem is PSPACE-complete. This suggests a tantalizing problem about E-dialogues, which are supposed to capture intuitionistic validity:

Main Problem: Find a decision procedure that operates on dialogue trees that, given a propositional formula φ, determine whether φ is intuitionistically valid.

The intention behind the qualifier “that operates on dialogue trees” is to rule out, as a solution to the problem, some decision procedure that takes φ totally ignores dialogue games by running some already available decision procedure, and then says YES or NO depending on the outcome of that decision procedure. Here are some related problems:

Side Problem 1: Find a computable function f such that, for all propositional formulas φ, Proponent has a winning strategy for φ iff Proponent has a winning strategy for φ of depth < f(φ).

That is, find a computable bound on the depth to which the dialogue tree needs to be developed so that we can determine whether Proponent has a winning strategy. It's quite possible that Side Problem 1 has no solution, even though the Main Problem is solvable. Here's another approach:

Side Problem 2: Find a computable predicate P of sequences s of dialogue moves (partial dialogues) for which P(s) holds iff Proponent cannot win in any continuation of s.

This is unsatisfying, because it's basically just a recapitulation of the Main Problem. But the aim of Side Problem 2 is to search for sound heuristics for when we can cut off the search for extensions to a dialogue. What's puzzling is that, on the one hand, presumably there is a solution to the Main Problem (though possibly not through Side Problem 1 or Side Problem 2), but, on the other hand, even with the experience Sara and I have developed through grinding out one dialogue game after the next, there is little intuition for how to solve it. (We are now exploring a “no repetition” heuristic, but we first need to give a proof that it is sound.) Could it be that, even though E-dialogues are supposed to be about intuitionistic validity, their computational properties are quite different from those of other formalisms for intuitionistic logic? Either possibility—yes or no—would be an important result about dialogues. (Note that the Main Problem here is methodologically similar to the composition problem that spurred us in the first place. As before, we seek a direct solution, involving only dialogue trees; we prefer to abstain from bringing in “foreign” methods to solve our problem. The point of this methodological insistence is not to dismiss the relations between dialogical logic and other logics; rather, the aim is to take dialogical logic seriously, at face value; it is trying to honor the idea that dialogues are supposed to be autonomous way of doing logic. If we cannot answer basic logical questions about dialogues without bringing some kind of translation into another framework, or if dialogues have logical features that, in light of their motivation, are curiosities, then this needs to be made clear.)

Rule neutrality, rule naturality

Last week the website for the Workshop on Dialogues, Inference, and Proof - Logical and Empirical Perspectives (DIPLEAP) was distributed to the preliminary list of participants, which means Jesse and I need to start thinking about what we'll present there. One of us will certainly introduce N and cover the material in our ICLA paper, as sort of a test run. But since we've finished up the proof of the positive answer to the composition problem for N, I've been thinking about some more philosophical issues relating to the dialogical approach, and I might speak on these instead. Now that we have at least one example of a positive composition problem solution that was proved directly through semantic (that is, dialogical) means, the pot of gold at the end of the rainbow would be to be able to isolate what it was about the rules set N that allowed us to give this positive solution, so that we could then identify other rules sets where we can be sure a positive solution can be given, even if the proof strategy may differ. The composition problem proof for N relied crucially on our theorem characterizing the forms of valid implications in N, and this theorem in turn exploited the fact that when Felscher's rules E, D11, and D12 are dropped, Opponent can repeat defenses as many times as he want, and thus draw out a dialogue infinitely (meaning that Proponent cannot win). This fact is part of what made finding the proof for the composition problem so difficult: Neither of us have any clear intuition or understanding of what the connection is between Opponent's ability to repeat defenses and the theorems of N. There doesn't appear to be any fundamental fact grounding the connection, which means that it is extremely difficult to exploit, because working with N still feels like reaching out in the dark, blind. If we cannot pick out specifically something about the N rules that can be generalized or extrapolated to other rules sets, then perhaps it is still possible to say something general, to find a criterion/a for rule sets or a class of rule properties that have some connection, stronger or weaker, with a positive solution to the composition problem. That is, can we isolate some 'natural' feature of rules that is connected to the composition problem? One way to go about answering this is to look at rule sets where negative solutions to the composition problem can be given. We give an example in our paper on N, just to show that such examples can be given: Change the rules for CL so that Proponent is now allowed to also assert atoms in defense of disjunctions. Then, $\vDash p\vee\neg p$ and $\vDash(p\vee\neg p)\rightarrow p$, but $\nvDash p$, and thus the set of formulas generated by this rule set is not a logic. This example may seem somewhat trivial, but it actually displays an interesting property: The new rule fails to be neutral in the sense that it encodes an exception for a particular type of formula. This concept of neutrality seems like one that might be fruitfully exploited. First, we isolate three senses in which rules (both particle and structural) can be neutral:

1. topic neutral (they do not favor one atom over another)
2. connective neutral (they do not favor one connective over another)
3. player neutral (they do not favor one player over another)

Then, we can ask: how much neutrality (a) is good and (b) can be had and obtain a logic? If neutrality turns out to be the right property to exploit, the latter question is the same as asking whether we can characterise when a rules set will have a positive solution to the composition problem on the basis of the neutrality of the rules involved. There are a few remarks that can be made at the outset. First, structural rules which are wholly player neutral will result in the inconsistent logic: Proponent has a winning strategy for every atom p, so at least some asymmetry/nonneutrality in the rules is required. This raises a question that I first became interested in in the cafe above the cafeteria on the campus in Ponta Delgada, which is how little player nonneutrality do we need in order to ensure that this does not follow? We already have reason to believe that D10 can be weakened, at least somewhat; Jesse has been investigating a variant of the D rules where Proponent can assert an atom if the corresponding literal has already been asserted by Opponent. The resulting rule set validates WEM but not LEM. (Thus, if this rule set generates a logic, then it is an SI-logic.) It is also likely that the particle rules cannot be wholly neutral: The fact that negations can only be attacked and not defended seems to be crucial. Investigating rule neutrality in these three ways has the advantage that neutrality is simply expressible, easy to determine, and has nice symmetry properties. However, the connection between neutrality of rules and their naturality is something which is much less clear, at this point. People working in the dialogical tradition who have tried to give philosophical justifications for the approach have appealed to the 'naturalness' of the rules (particularly the particle rules), and have argued that there is a connection between the dialogical rules and the way that people actually debate (see, for example, the first few pages of chapter 6 of Lorenzen's Constructive Philosophy), and that therefore the dialogical approach is philosophically preferable to others because it is somehow more natural. But what is 'natural'? Barthe & Krabbe, in From Axiom to Dialogue, after they have introduced rules for systematic dialectics and realistic dialectics (and before they discuss thoroughgoing dialectics, orderly dialectics, and dynamic dialectics), discuss the naturalness of the rules they've suggested:

In each case where we expect that the large majority of people can be brought to agree upon a certain rule as part of a formal_3 dialectics (provided they are explicitly confronted with it and made acquainted with the motivation given for it here or with a similar motivation), we shall say, for short, that we think it is a natural rule [p. 75].

If it is agreed that this is a reasonable definition of 'natural', then I think it can be argued that none of the dialogical rule sets are in fact natural. The motivation for many of the dialogical rule sets in the literature to date essentially boils down to "they work" -- a formal proof can be given showing that the rules do in fact correspond to the desired logic (or, in the case of N, that they correspond to a logic, even if that logic is one that was not set out in advance). The majority of people when confronted with this motivation are going to balk at being asked to accept the rules on that basis alone: They're going to ask, "Why do they work?" What is it about the rules that makes them correspond to a logic, much less the target logic isolated in advance? And now we're back to the original question: Are there any properties of rule or rule sets that correspond to positive solutions to the composition problem, and if so, what are they? And then neutrality of certain types presents itself again as a natural starting point for investigating answers.

Paper on NCL now available on the arXiv

Our first paper on NCL, “A curious dialogical logic and its composition problem”, submitted to the 4th Indian Conference on Logic and its Applications, is now available as a preprint on the arXiv repository.