Dialogical Logic

Dialogical logic is an approach to logic in which the meaning of the logical constants (connectives and quantifiers) and the notion of validity are explained in game-theoretic terms. The meaning of each logical constant (such as “and”, “or”, “implies”, “not”, “every”, and so forth) is given in terms of how assertions containing these logical constants can be attacked and defended in an adversarial dialogue. Dialogues are described as two-player games between a proponent and an opponent. A dialogue starts with an assertion made by the proponent. This assertion can then be attacked according to its logical form by the opponent. Depending upon the kind of attack, the proponent can now either defend against, or attack, the opponent’s move. The two players alternate until one player is unable to make another move. In this case, the dialogue is won by the other player who made the last move. An assertion made in the initial move by the proponent is said to be valid, if the proponent has a winning strategy for it, that is, if the proponent can win every dialogue for each possible move made by the opponent. The dialogical approach was initially worked out for intuitionistic logic and for classical logic; it has been extended to other logics, among them modal logic and linear logic.

Introduction
Argumentation Forms and the Meaning of Logical Constants
Dialogues for Intuitionistic Logic
1. Definition
2. Examples
Winning Strategies and Validity
Dialogues for Classical Logic
1. Examples
2. Classical Dialogical Validity and Completeness
Origins and Recent Developments
References and Further Reading

1. Introduction

Dialogical logic comprises three main constituents:

(i) Argumentation forms. The meaning of the logical constants (like “implies”, for example) is given by so-called argumentation forms. An argumentation form describes in terms of two possible kinds of moves, called attack and defense, how assertions containing a certain logical constant in main position can be attacked and defended. For example, the argumentation form for “implies” says that if one player asserts “ $A$ implies $B$ ”, then the other player can attack this assertion by claiming $A$ , which can in turn be defended by the first player by claiming $B$ . This reflects how logical constants are understood in everyday argumentation: someone arguing for “ $A$ implies $B$ ” has to be able to argue for $B$ when being granted that $A$ .

(ii) Dialogues. A dialogue is a single game played by two players, called proponent and opponent. The proponent moves first by making an assertion. Then players alternate moves. Each move has to be made according to an argumentation form. In addition, certain rules or conditions are imposed, which go beyond what has been laid down in the argumentation forms. An example of such a rule is that a defense against a certain attack cannot be repeated. There are rules that hold for both players as well as rules that restrict only one of the two players. An example for the latter is the rule that a statement containing no logical constant can only be asserted by the proponent after it has already been asserted by the opponent, whereas the opponent can assert such a statement at any time, if allowed by an argumentation form and not prohibited by other conditions. The proponent wins a dialogue if the opponent cannot make another move.

(iii) Winning strategies. The notion of winning strategy for dialogue games provides the dialogical notion of validity or, depending on the point of view, of provability. In dialogical logic, an assertion is called valid if there exists a winning proponent strategy for it. That is, an assertion is valid if the proponent can always win a dialogue for it, no matter what moves are made by the opponent. Depending on the conditions specifying the kind of dialogues which are played, there may or may not be a winning proponent strategy for a given assertion. This means that by changing the rules of the dialogue games one can obtain different notions of validity, such as intuitionistic validity or classical validity, for example.

2. Argumentation Forms and the Meaning of Logical Constants

Argumentation forms are formulated for an extended first-order language. The first-order language consists of formulas $A, B, \ldots, A_1,\ldots$ , which are constructed from atomic formulas $a, b, c, \ldots$ with the logical constants $\wedge$ (conjunction; “and”), $\vee$ (disjunction; “or”), $\rightarrow$ (implication; “implies”), $\neg$ (negation; “not”), $\forall$ (universal quantifier; “every”) and $\exists$ (existential quantifier; “there is”), together with terms $t$ , which can be variables $x,y,\ldots$ , and auxiliary signs “ $($ ”, “ $)$ ” and “ $,$ ”. The atomic formulas can be relation symbols of arbitrary arity taking terms as arguments. An example for a first-order formula is

$\forall x \exists y (a(x,y) \rightarrow b(x))$

This language is extended by using $?1$ , $?2$ , $?\!\vee$ , $?t$ (for terms $t$ ) and $?\exists$ as special symbols (that contain a preceding question mark). In addition, the signatures $P$ and $O$ stand for the two players proponent and opponent, respectively. An expression $e$ is either a formula or a special symbol. For each expression $e$ there is a $P$ -signed expression $P\, e$ and an $O$ -signed expression $O\, e$ . These signed expressions are called moves in general. Examples for moves are

$P\, \forall x \exists y (a(x,y) \rightarrow b(x))$

and

$O\, ?\!\vee$

A signed expression is called assertion if the expression is a formula; it is called symbolic attack if the expression is a special symbol (there is no such thing as a symbolic defense). $X$ and $Y$ , where $X \neq Y$ , are used as variables for $P$ and $O$ .

For each logical constant there is one argumentation form, which determines how a formula, with the respective logical constant as main constant, that is asserted by $X$ can be attacked by $Y$ , and how this attack can be defended by $X$ (if possible):

$\begin{array}{rlll} \wedge: & \text{assertion}: & X\, A_1 \wedge A_2 & \\ & \text{attack}: & Y\, ?i & (Y \text{ chooses } i = 1 \text{ or } i = 2)\\ & \text{defense}: & X\, A_i & \\ &\\ \vee: & \text{assertion}: & X\, A_1 \vee A_2 & \\ & \text{attack}: & Y\, ?\!\vee & \\ & \text{defense}: & X\, A_i & (X \text{ chooses } i = 1 \text{ or } i = 2)\\ &\\ \rightarrow: & \text{assertion}: & X\, A \rightarrow B & \\ & \text{attack}: & Y\, A & \\ & \text{defense}: & X\, B & \\ &\\ \neg: & \text{assertion}: & X\, \neg A & \\ & \text{attack}: & Y\, A & \\ & \text{defense}: & \mathit{no\ defense} & \\ &\\ \forall: & \text{assertion}: & X\, \forall x A(x) & \\ & \text{attack}: & Y\, ?t & (Y \text{ chooses the term } t)\\ & \text{defense}: & X\, A(x)[t/x] & \\ &\\ \exists: & \text{assertion}: & X\, \exists x A(x) & \\ & \text{attack}: & Y\, ?\exists & \\ & \text{defense}: & X\, A(x)[t/x] & (X \text{ chooses the term } t) \end{array}$

The argumentation form for $\wedge$ says that an assertion of the form $A_1 \wedge A_2$ made by player $X$ can be attacked by the other player $Y$ by choosing one of the two conjuncts $A_1$ and $A_2$ . This is expressed by $Y$ stating the special symbol $?1$ or $?2$ , respectively. This attack can then be defended by player $X$ by asserting the conjunct $A_1$ or the conjunct $A_2$ according to the choice of $Y$ . A concrete instance of this argumentation form is the following:

$\begin{array}{l}P\, \neg a \wedge (b \vee a)\\O\, ?2\\P\, b \vee a\end{array}$

Here the proponent $P$ has asserted the conjunction $\neg a \wedge (b \vee a)$ . This is attacked by the opponent $O$ choosing the second conjunct $b \vee a$ , indicated by stating the special symbol $?2$ . The proponent defends against this attack by asserting the second conjunct $b \vee a$ . Informally, someone claiming “ $A_1$ and $A_2$ ” has to be able to argue for $A_1$ and for $A_2$ ; an opponent can thus ask for any of the two.

For disjunctions of the form $A_1 \vee A_2$ asserted by player $X$ , the attack by the other player $Y$ is indicated by the special symbol $?\!\vee$ . The defending player $X$ chooses one of the two disjuncts $A_1$ and $A_2$ . Informally, someone claiming “ $A_1$ or $A_2$ ” has only to be able to argue for one of the two disjuncts, and can therefore choose to argue for $A_1$ or for $A_2$ , if the claimed disjunction is questioned.

In the case of implications $A \rightarrow B$ asserted by player $X$ , the attacking player $Y$ asserts the antecedent $A$ of the implication, and the defending player $X$ asserts the consequent $B$ . Informally, someone claiming “ $A$ implies $B$ ” has to be able to argue for $B$ whenever $A$ is given as an assumption.

Negated assertions $\neg A$ made by player $X$ can only be attacked, namely by the other player $Y$ asserting $A$ . There is no defense against such an attack. Informally, when claiming that “ $A$ is not the case”, one has to be able to argue against $A$ .

The argumentation form for the universal quantifier $\forall$ says that an assertion of the form $\forall x A(x)$ made by player $X$ can be attacked by player $Y$ by choosing a term $t$ in the symbolic attack $Y\, ?t$ . Player $X$ can then defend by asserting the formula $A(x)[t/x]$ , where the term $t$ chosen by $Y$ is substituted for (all occurrences of) the variable $x$ in the formula $A(x)$ , also written $A(t)$ . Informally, someone claiming that “every object has the property $A$ ” has to be able to show for any object that it has the property $A$ . An opponent can thus ask for any object (denoted by the term $t$ , for example) whether it has the property $A$ . This has then to be answered by an argument for $A(t)$ .

For existential assertions of the form $\exists x A(x)$ made by player $X$ , the attack by the other player $Y$ is indicated by the special symbol $?\exists$ . The defending player $X$ chooses a term $t$ and asserts the formula $A(x)[t/x]$ , that is, the formula resulting from substituting $t$ for (all occurrences of) $x$ in $A(x)$ . Informally, someone claiming that “there exists an object with property $A$ ” has only to be able to present one object (denoted by the term $t$ , for example) with the property $A$ , and can thus choose to argue for $A(t)$ , when the claimed existence of such an object is questioned.

The argumentation forms give thus an explanation of the meaning of the logical constants by saying how assertions, which contain the respective logical constant in main position, are used in argumentations between the two players proponent $P$ and opponent $O$ . This explanation is intended to capture how assertions are used according to their logical form in actual argumentations.

In the literature, argumentation forms are also called particle rules or logical rules.

3. Dialogues for Intuitionistic Logic

Dialogical logic was at first developed for intuitionistic logic and for classical logic.

Classical logic is usually based on the principle of bivalence. Each assertion is either true or false, and the truth value of a compound assertion is determined by the truth values of its constituents. For example, the meaning of the logical constant $\wedge$ is given by saying that assertions of the form $A \wedge B$ have the truth value “true” if both conjuncts $A$ and $B$ have the truth value “true”; otherwise the truth value of $A \wedge B$ is “false”.

Intuitionistic logic is not based on bivalence. Instead of employing truth values, the intuitionistic meaning of logical constants is usually explained in terms of proofs or transformations of proofs. For example, the meaning of $\wedge$ is explained by saying that an assertion of the form $A \wedge B$ has a proof if and only if both $A$ and $B$ have a proof. An implication $A \rightarrow B$ has a proof if and only if one is in possession of a construction that transforms any proof of the antecedent $A$ into a proof of the consequent $B$ . The classical principle of tertium non datur ( $A \vee \neg A$ ) is rejected in intuitionistic logic, and other classical principles such as double negation elimination ( $\neg\neg A \rightarrow A$ ) do not hold. The set of intuitionistic theorems is a subset of the set of classical theorems. In particular, $A \rightarrow B$ is not equivalent to $\neg A \vee B$ in intuitionistic logic, whereas it is in classical logic. In intuitionistic logic, implication ( $\rightarrow$ ) is a genuine logical constant; it cannot be expressed by using other logical constants such as negation ( $\neg$ ) and disjunction ( $\vee$ ).

Dialogical formulations can be given for both classical logic and intuitionistic logic. The difference between these formulations is made by different notions of dialogue, specified by certain conditions. Dialogues for intuitionistic logic are defined next. Dialogues for classical logic will be dealt with below, in Section 5. The argumentation forms underlying these notions do not differ; they are the same for both logics.

a. Definition

Dialogues for intuitionistic logic are defined with respect to the given argumentation forms to be finite or infinite sequences of moves satisfying the following dialogue conditions:

The first move is made by the proponent $P$ with the assertion of a non-atomic formula, and proponent $P$ and opponent $O$ alternate moves as determined by the argumentation forms.
$P$ may assert an atomic formula only if it has been asserted by $O$ before.
If there is more than one open attack, then only the last one may be defended.
(An attack is open if it has not been defended yet. Attacks made according to the argumentation form for $\neg$ are always open, since there is no defense against them.)
An attack may be defended at most once.
A $P$ -signed formula may be attacked at most once.

These conditions are also called structural rules or frame rules in the literature. They are here given only informally. Condition 3 refers to one occurrence of an attack, and condition 4 refers to one occurrence of a $P$ -signed formula. Hence, if an already defended attack is repeated, then condition 3 does not prohibit that this new occurrence of the attack can be defended once, too. This holds likewise for an already attacked $P$ -signed formula. If this formula is again asserted by $P$ , then condition 4 does not prohibit that this new occurrence can be attacked once as well.

It can be observed that proponent and opponent are not interchangeable. This is only due to conditions 1 and 4, which are asymmetric for $P$ and $O$ . In particular, the moves $X\, A$ and $Y\, \neg A$ do not amount to the same because of condition 1. The argumentation forms, on the other hand, are completely symmetric with respect to $P$ and $O$ , that is, the argumentation forms are player-independent.

The proponent wins a dialogue for a formula $A$ if the dialogue is finite, begins with the move $P\, A$ and ends with a move of $P$ such that $O$ cannot make another move, that is, every move that $O$ could make according to the argumentation forms violates at least one of conditions 0 to 4.

b. Examples

Dialogues are written with position numbers on the left and with comments on the right. The comments make explicit what kind of move is made (attack or defense) and to which preceding move a move refers to. In this notation, moves have the format

$\langle\text{position number}\rangle \langle\text{signed expression}\rangle \langle\text{comment}\rangle$

The following is a dialogue for the formula $a \rightarrow (b \rightarrow a)$ :

$\begin{array}{rll}0. & P\, a \rightarrow (b \rightarrow a) & \\1. & O\, a & (\text{attack on }0)\\2. & P\, b \rightarrow a & (\text{defense against }1)\\ 3. & O\, b & (\text{attack on }2)\\ 4. & P\, a & (\text{defense against }3)\end{array}$

The dialogue starts with the assertion of the formula $a \rightarrow (b \rightarrow a)$ by the proponent $P$ in the initial move at position 0. This initial move is attacked by the opponent $O$ at position 1 with the assertion of the antecedent $a$ of the implication asserted by $P$ at position 0. The attack is thus made according to the argumentation form for $\rightarrow$ . In the next move at position 2, the proponent defends against this attack according to the argumentation form for $\rightarrow$ by asserting the consequent $b \rightarrow a$ of the attacked implication $a \rightarrow (b \rightarrow a)$ . The implication $b \rightarrow a$ is attacked by $O$ at position 3 by asserting its antecedent $b$ . This attack is defended by $P$ at position 4 by asserting $a$ , the consequent of $b \rightarrow a$ . Here $P$ is allowed to assert the atomic formula $a$ , since $O$ has asserted $a$ before (compare condition 1). These last moves are also made according to the argumentation form for $\rightarrow$ . The opponent cannot make another move, since atomic formulas cannot be attacked (there are only argumentation forms for non-atomic assertions), and $O$ cannot repeat attacks due to condition 4. The dialogue is thus won by $P$ .

The following is a dialogue for the formula $\neg a \vee (a \rightarrow a)$ :

$\begin{array}{rll}0. & P\, \neg a \vee (a \rightarrow a)\\1. & O\, ?\!\vee & (\text{attack on }0)\\2. & P\, \neg a & (\text{defense against }1)\\3. & O\, a & (\text{attack on 2})\end{array}$

The initial move is attacked by $O$ with the symbolic attack $O\, ?\!\vee$ according to the argumentation form for $\vee$ . This attack can be defended by $P$ either by asserting the left disjunct $\neg a$ or by asserting the right disjunct $a \rightarrow a$ . Here, the proponent chooses the former in the defense move at position 2. This is attacked by $O$ with the assertion of $a$ according to the argumentation form for $\neg$ . The dialogue is not won by $P$ , and $P$ cannot make another move: the atomic formula $a$ cannot be attacked, there is no defense against attacks on negated formulas, and due to condition 3 it is not possible to defend against the attack $O\, ?\!\vee$ again.

Another dialogue for the same formula $\neg a \vee (a \rightarrow a)$ is obtained if $P$ defends against the attack $O\, ?\!\vee$ by choosing to assert the right disjunct $a \rightarrow a$ instead of the left disjunct at position 2:

$\begin{array}{rll}0. & P\, \neg a \vee (a \rightarrow a)\\1. & O\, ?\!\vee & (\text{attack on }0)\\2. & P\, a \rightarrow a & (\text{defense against }1)\\3. & O\, a & (\text{attack on }2)\\4. & P\, a & (\text{defense against }3)\end{array}$

At position 3, the opponent attacks $a \rightarrow a$ by asserting its antecedent $a$ , which $P$ defends against at position 4 with the assertion of the consequent $a$ . This dialogue is finite and ends with a move of $P$ such that $O$ cannot make another move, that is, this dialogue is won by $P$ .

These two dialogues for the formula $\neg a \vee (a \rightarrow a)$ show that for a valid formula there can be dialogues which are won by $P$ as well as dialogues which are not won by $P$ , although every possible move has been made. There are also invalid formulas for which this is the case. An example is $a \wedge (a \rightarrow a)$ . If $O$ attacks this formula with $O\, ?2$ , then $P$ wins the dialogue: the defense $P\, a \rightarrow a$ is attacked with $O\, a$ , which $P$ defends against with $P\, a$ as final move. If, however, $O$ attacks with $O\, ?1$ , then $P$ cannot make another move, since the first conjunct $a$ , which is an atomic formula, cannot be asserted because of condition 1.

A dialogue for the first-order formula $\neg\forall x\neg a(x) \rightarrow \exists x a(x)$ is the following:

$\begin{array}{rll}0. & P\, \neg\forall x\neg a(x) \rightarrow \exists x a(x)\\1. & O\, \neg\forall x\neg a(x) & (\text{attack on }0)\\2. & P\, \forall x\neg a(x) & (\text{attack on }1)\\3. & O\, ?t_1 & (\text{attack on }2)\\4. & P\, \neg a(t_1) & (\text{defense against }3)\\5. & O\, a(t_1) & (\text{attack on }4)\end{array}$

Instead of defending against $O$ ‘s attack (made at position 1) with $P\, \exists x a(x)$ at position 2, the proponent attacks $O$ ‘s assertion of $\neg\forall x\neg a(x)$ by asserting $\forall x\neg a(x)$ , according to the argumentation form for $\neg$ . At position 3, the opponent attacks according to the argumentation form for $\forall$ by choosing the term $t_1$ in the symbolic attack $O\, ?t_1$ , which $P$ defends against by asserting $\neg a(t_1)$ at position 4. The opponent attacks this according to the argumentation form for $\neg$ with $a(t_1)$ in the last move. Note that there are now two open attacks made by $O$ : the one at position 1 and the one in the last move. Due to condition 2, only the last of the two may be defended. Thus the proponent cannot catch up with the defense $P\, \exists x a(x)$ of $O$ ‘s attack made at position 1, and according to the argumentation form for $\neg$ there is no defense to the last move. The proponent can only repeat the attack made at position 2, which leads to an infinite dialogue where a sequence of moves like

$\begin{array}{rll}n. & P\, \forall x\neg a(x) & (\text{attack on }1)\\n+1. & O\, ?t & (\text{attack on }n)\\n+2. & P\, \neg a(t) & (\text{defense against }n+1)\\n+3. & O\, a(t) & (\text{attack on }n+2)\end{array}$

is repeated endlessly; the opponent may choose a different term $t$ in each repetition. Note that repeated attacks on the same move are prohibited only for $O$ , while for $P$ there is no such restriction. Hence $P$ can repeatedly attack the move $O\, \neg\forall x\neg a(x)$ (made at position 1) with the move $P\, \forall x\neg a(x)$ , starting the loop. Furthermore, each occurrence of an attack is defended at most once, and each occurrence of a $P$ -signed formula is attacked at most once, in accordance with conditions 3 and 4, respectively. This dialogue for the formula

$\neg\forall x\neg a(x) \rightarrow \exists x a(x)$

is therefore neither won by $P$ nor does it end with an opponent move.

In summary, it can be observed that there are valid formulas for which there are finite dialogues that are not won by $P$ as well as dialogues that are won by $P$ , there are invalid formulas for which the same is the case, and there can be infinite dialogues, too. The notion of winning a dialogue is itself not sufficient for making a distinction concerning the validity of a formula.

4. Winning Strategies and Validity

In dialogical logic the central logical notion of validity is explained in terms of the game-theoretic notion of strategy. A strategy determines each move of a player. The crucial notion for validity is that of winning proponent strategy. Dialogical validity of a formula consists in the existence of a winning proponent strategy for that formula.

a. Winning Strategies

A player $X$ has a winning strategy if for every move made by the other player $Y$ player $X$ can make another move, such that each resulting play of the game (that is, each resulting dialogue) is eventually won by $X$ . In dialogical logic one is usually only interested in winning strategies for the proponent $P$ . A winning proponent strategy for a formula $A$ is a tree $S$ whose branches are dialogues for $A$ won by $P$ , where the nodes are the moves, such that

$S$ has the move $P\, A$ as root node (with depth 0),
if the depth of a node is odd (that is, if the node is an opponent move), then it has exactly one successor node (which is a proponent move),
if the depth of a node is even (that is, if the node is a proponent move), then it has as many successor nodes as there are possible moves for $O$ at this position.

b. Examples

The following dialogue, which has been discussed above, is already a winning proponent strategy for the formula $\neg a \vee (a \rightarrow a)$ :

This winning proponent strategy has only one branch, which is the dialogue shown. The root node

$P\, \neg a \vee (a \rightarrow a)$

has only one successor, since the move $O\, ?\!\vee$ is the only possible move for $O$ . This node at depth 1 has exactly one successor node, namely the move $P\, a \rightarrow a$ at depth 2. This in turn has again only one successor node, namely the move $O\, a$ at depth 3, since no other opponent moves are possible. Its one successor node is $P\, a$ , which has no successor as there are no possible opponent moves. The dialogue is won by $P$ , and all possible opponent moves have been taken into account. This single branch tree is thus a winning proponent strategy for the formula $\neg a \vee (a \rightarrow a)$ .

In general, winning proponent strategies have more than one branch. If there are several opponent moves possible after a proponent move, then there will be a branch for each of the possible opponent moves. Consider the following winning proponent strategy for the formula $(\neg a \vee b) \rightarrow (a \rightarrow b)$ :

$\begin{array}{rlcl}0. &\hspace{5em} & P\, (\neg a \vee b) \rightarrow (a \rightarrow b) &\\1. & & O\, \neg a \vee b & (\text{attack on }0)\\2. & & P\, a\ \rightarrow b & (\text{defense against }1)\\3. & & O\ a & (\text{attack on }2)\\4. & & P?\!\vee & (\text{attack on }1)\end{array}}$

$\begin{array}{lll|ll}5. & O\, \neg a & (\text{defense against }4)\, & O\, b & (\text{defense against }4)}\\{6. & P\, a & (\text{attack on }5) & P\, b & (\text{defense against }3)}\end{array}$

This tree of signed expressions has two branches. After the move $P\, ?\!\vee$ at depth 4 there are two possible moves for $O$ , yielding the two successor nodes $O\, \neg a$ (left branch) and $O\, b$ (right branch). The proponent wins both resulting dialogues: $O$ can neither make another move after $P\, a$ (left dialogue) nor after $P\, b$ (right dialogue). Thus, this tree is a winning proponent strategy.

c. First-Order Winning Strategies

Winning strategies for quantifier-free formulas are always finite trees, whereas winning strategies for first-order formulas can in general be trees of countably infinitely many finite branches. An example is the following winning proponent strategy for the first-order formula $\neg\exists x a(x) \rightarrow \forall x \neg a(x)$ :

$\begin{array}{rcl}0. & \hspace{3em} P\, \neg\exists x a(x) \rightarrow \forall x \neg a(x) \hspace{3em}&\\1. & O\, \neg\exists x a(x) & (\text{attack on }0)\\2. & P\, \forall x \neg a(x) & (\text{defense against }1)\end{array}$

$\begin{array}{rl|l|l|ll}3. & O\, ?t_1 & O\, ?t_2 & O\, ?t_3 & \ldots\hspace{.85em} & (\text{attack on }2)\\4. & P\, \neg a(t_1) & P\, \neg a(t_2) & P\, \neg a(t_3) & \ldots & (\text{defense against }3)\\ 5. & O\, a(t_1) & O\, a(t_2) & O\, a(t_3) & \ldots & (\text{attack on }4)\\ 6. & P\, \exists x a(x) & P\, \exists x a(x) & P\, \exists x a(x) & \ldots & (\text{attack on }1)\\ 7. & O\, ?\exists & O\, ?\exists & O\, ?\exists & \ldots & (\text{attack on }6)\\ 8. & P\, a(t_1) & P\, a(t_2) & P\, a(t_3) & \ldots & (\text{defense against }7)\end{array}$

The move $P\, \forall x \neg a(x)$ at depth 2 has countably infinitely many successor nodes, since for each choice of a term $t_i$ (for natural numbers $i$ ) the symbolic attack $O\, ?t_i$ is a possible move. For pairwise distinct terms $t_i$ the tree therefore has infinitely many branches (indicated by “ $\ldots$ ”), where each branch is a dialogue won by $P$ .

Such infinite winning strategies can be avoided by using the following restrictions with respect to winning proponent strategies:

If the depth of a node is even, and the symbolic attack $O\, ?y$ on the move $P\, \forall x A(x)$ is a possible move, where $y$ is a new variable in this branch, then $O\, ?y$ is the only immediate successor node that is an attack on $P\, \forall x A(x)$ .
If the depth of a node is even, $P\, ?\exists$ is an attack on an assertion $O\, \exists x A(x)$ , and the move $O\, A(x)[y/x]$ is a possible defense against this attack, where $y$ is a new variable in this branch, then $O\, A(x)[y/x]$ is the only immediate successor node that is a defense against $P\, ?\exists$ .

There may be further possible moves, which are not attacks on $P\, \forall x A(x)$ or defenses against $P\, ?\exists$ . In this case the node at even depth has more than one immediate successor node. However, the number of these immediate successor nodes can only be finite, and there is thus no more infinite ramification within winning proponent strategies.

For example, the infinite winning proponent strategy indicated above is reduced to the following finite winning proponent strategy:

$\begin{array}{rll}0. & P\, \neg\exists x a(x) \rightarrow \forall x \neg a(x) & \\ 1. & O\, \neg\exists x a(x) & (\text{attack on }0)\\ 2. & P\, \forall x \neg a(x) & (\text{defense against }1)\\ 3. & O\, ?y & (\text{attack on }2)\\ 4. & P\, \neg a(y) & (\text{defense against }3)\\ 5. & O\, a(y) & (\text{attack on }4)\\ 6. & P\, \exists x a(x) & (\text{attack on }1)\\ 7. & O\, ?\exists & (\text{attack on }6)\\ 8. & P\, a(y) & (\text{defense against }7)\end{array}$

The restrictions (i) and (ii) have the effect that in winning strategies only one of the possible attacks $O\, ?t$ (for each term $t$ ) on $P\, \forall x A(x)$ or defenses $O\, A(x)[t/x]$ (for each term $t$ ) against $P\, ?\exists$ has to be taken into account, namely one where the term $t$ is a new variable, whereas in winning strategies which are not thus restricted one has to consider the corresponding moves for each term $t$ , including variables. It can be shown that a restricted winning strategy can always be extended to an unrestricted one.

Infinite ramifications in winning strategies can also be avoided by replacing the player-independent argumentation forms for $\forall$ and $\exists$ by the following player-dependent argumentation forms:

$\begin{array}{rlll}\forall_{P}: & \text{assertion}: & P\, \forall x A(x) & \\ & \text{attack}: & O\, ?y & (\text{variable }y\text{ is new})\\ & \text{defense}: & P\, A(x)[y/x] & \\ \\ \forall_{O}: & \text{assertion}: & O\, \forall x A(x) & \\ & \text{attack}: & P\, ?t & (P\text{ chooses the term }t)\\ & \text{defense}: & O\, A(x)[t/x] & \\ \\ \exists_{P}: & \text{assertion}: & P\, \exists x A(x) & \\ & \text{attack}: & O\, ?t & (O\text{ chooses the term }t)\\ & \text{defense}: & P\, A(x)[t/x] &\\ \\ \exists_{O}: & \text{assertion}: & O\, \exists x A(x) & \\ & \text{attack}: & P\, ?\exists & \\ & \text{defense}: & O\, A(x)[y/x] & (\text{variable }y\text{ is new})\end{array}$

The argumentation forms $\forall_{P}$ and $\exists_{O}$ contain the condition that the variable $y$ is new. They are thus history-dependent in the sense that the possibility of a move $O\, ?y$ or $O\, A(x)[y/x]$ in a dialogue depends on whether the variable $y$ has already occurred in this dialogue. The player-independent argumentation forms for $\forall$ and $\exists$ , on the other hand, are not history-dependent.

Winning proponent strategies for the resulting dialogues can then be restricted as follows: Only one successor node for a node at even depth has to be considered if

the symbolic attack $O\, ?y$ according to the argumentation form $\forall_{P}$ is a possible opponent move,
the symbolic attack $O\, ?t$ according to the argumentation form $\exists_{P}$ is a possible opponent move,
or the opponent move defending a symbolic attack $P\, ?\exists$ according to the argumentation form $\exists_{O}$ is a possible move.

Again, further moves according to other argumentation forms may be possible. The resulting winning proponent strategies are finite. The use of the player-dependent argumentation forms has therefore technical advantages. However, from a conceptual point of view, player-independent argumentation forms might be preferable.

d. Tertium Non Datur and the Principle of Non-Contradiction

The proponent does not have a winning strategy for every formula. An example is the instance $a \vee \neg a$ of tertium non datur. There is only one possible dialogue, namely:

$\begin{array}{rll}0. & P\, a \vee \neg a & \\ 1. & O\, ?\!\vee & (\text{attack on }0)\\ 2. & P\, \neg a & (\text{defense against }1)\\ 3. & O\, a & (\text{attack on }2)\end{array}$

which is not won by $P$ . At position 2, the proponent can only defend against $O$ ‘s symbolic attack $O\, ?\!\vee$ by choosing to assert the right disjunct $\neg a$ . Choosing the left disjunct is not an option due to condition 1. Due to condition 4, the opponent cannot repeat the symbolic attack $O\, ?\!\vee$ at position 3; the only possible move for $O$ is to attack $P\, \neg a$ with $O\, a$ . This attack can neither be defended nor can it be attacked, and another defense against the already defended symbolic attack $O\, ?\!\vee$ is ruled out by condition 3.

On the other hand, there is a winning proponent strategy for each instance of the principle of non-contradiction, $\neg (A \wedge \neg A)$ . Consider the following winning proponent strategy for $\neg(a \wedge \neg a)$ :

$\begin{array}{rll} 0. & P\, \neg(a \wedge \neg a) & \\ 1. & O\, a \wedge \neg a & (\text{attack on }0)\\ 2. & P\, ?1 & (\text{attack on }1)\\ 3. & O\, a & (\text{defense against }2)\\ 4. & P\, ?2 & (\text{attack on }1)\\ 5. & O\, \neg a & (\text{defense against }4)\\ 6. & P\, a & (\text{attack on }5)\end{array}$

Here it is essential that $P$ can attack the same assertion repeatedly. The opponent’s assertion of $a \wedge \neg a$ at position 1 is attacked by $P$ first at position 2 by choosing the first conjunct, and again at position 4, now by choosing the second conjunct. Both attacks are necessary for having a winning proponent strategy.

There is no winning proponent strategy in the case of tertium non datur, since $P$ cannot defend against the attack on $a \vee \neg a$ repeatedly, while in the case of the principle of non-contradiction there is a winning proponent strategy because $P$ can attack $a \wedge \neg a$ repeatedly. In classical logic, tertium non datur and the principle of non-contradiction are equivalent, while in intuitionistic logic only the principle of non-contradiction holds. For the dialogues considered, this distinction rests upon the fact that $P$ can repeatedly attack but not repeatedly defend against an assertion.

To sum up, there are formulas for which there exists a winning proponent strategy, and there are formulas for which this is not the case. A given formula can also have more than one winning proponent strategy.

e. Dialogical Validity and Completeness

The dialogical notion of validity is defined as follows:

A formula $A$ is called valid if there is a winning proponent strategy for $A$ .

That this dialogical notion of validity corresponds exactly to intuitionistic provability is the content of the following completeness result:

A formula $A$ is valid if and only if $A$ is provable in intuitionistic logic.

Hence, for the dialogues defined by conditions 0 to 4, one obtains a dialogical formulation of intuitionistic logic.

Provability is closed under uniform substitution of formulas for atomic formulas. That is, if a formula $A$ is provable in intuitionistic logic, then each substitution instance $A'$ , obtained by uniformly substituting formulas for atomic formulas in $A$ , is provable in intuitionistic logic, too. The completeness result implies that also validity is closed under uniform substitution. That is, if there is a winning proponent strategy for $A$ , then there are winning proponent strategies for each instance $A'$ of $A$ that is the result of a uniform substitution of formulas for atomic formulas in $A$ .

f. Winning Strategies as Proofs

Dialogues can also be viewed as constituents of a proof system. On this view, the proofs of a formula $A$ are the winning proponent strategies for $A$ . Completeness is then formulated as an equivalence theorem for winning proponent strategies and proofs in a given proof system such as, for example, sequent calculus:

There is a winning proponent strategy for $A$ if and only if $A$ is provable in sequent calculus for intuitionistic logic.

A constructive proof of this theorem has been given by Felscher [1985] by showing that there are algorithms transforming any winning proponent strategy for a formula $A$ into a proof of $A$ in sequent calculus for intuitionistic logic, and, the other way round, transforming any proof of $A$ into a winning proponent strategy for $A$ .

5. Dialogues for Classical Logic

A dialogical rendering of classical logic is obtained by relaxing conditions 2 and 3 for the proponent $P$ , while keeping them for the opponent $O$ . That is, conditions 2 and 3 are replaced by the following conditions:

2′. If there is more than one open attack by $P$ , then only the last one may be defended by $O$ .

3′. An attack by $P$ may be defended by $O$ at most once.

For $P$ this means that if there is more than one open attack made by $O$ , then $P$ may defend against any of these attacks (instead of only the last one), and $P$ can defend against attacks made by $O$ repeatedly.

No changes are made to the argumentation forms. Classical dialogues are defined with respect to them to be finite or infinite sequences of moves made according to conditions 0, 1, 2′, 3′ and 4.

Classical winning proponent strategies for a formula $A$ are defined as before in the case of intuitionistic logic, but with the notion of dialogue replaced by the notion of classical dialogue.

a. Examples

There is a classical winning proponent strategy for the formula $a \vee \neg a$ . It consists in the following classical dialogue:

$\begin{array}{rll} 0. & P\, a \vee \neg a & \\ 1. & O\, ?\!\vee & (\text{attack on }0)\\ 2. & P\, \neg a & (\text{defense against }1)\\ 3. & O\, a & (\text{attack on }2)\\ 4. & P\, a & (\text{defense against }1)\end{array}$

At position 2, the proponent can defend against $O$ ‘s symbolic attack $O\, ?\!\vee$ only by asserting the right disjunct $\neg a$ , since the atomic left disjunct $a$ has not been asserted by $O$ yet (compare condition 1). But due to the replacement of condition 3 by condition 3′, the proponent can defend against this attack again at position 4, now by asserting the left disjunct $a$ , which has been asserted by $O$ at the preceding position 3.

There is a classical winning proponent strategy for the formula $\neg\neg a \rightarrow a$ , an instance of the intuitionistically invalid principle of double negation elimination. It consists in the following classical dialogue:

$\begin{array}{rll} 0. & P\, \neg\neg a \rightarrow a & \\ 1. & O\, \neg\neg a & (\text{attack on }0)\\ 2. & P\, \neg a & (\text{attack on }1)\\ 3. & O\, a & (\text{attack on }2)\\ 4. & P\, a & (\text{defense against }1)\end{array}$

The last move is possible due to the replacement of condition 2 by condition 2′. At position 3 there are two open attacks by $O$ (made at positions 1 and 3, respectively). Condition 2 would prohibit $P$ ‘s defense against the first attack, since this is not the last open attack. But condition 2′ enables $P$ to defend against any earlier open attack. At position 4, the proponent can thus defend against $O$ ‘s first attack by asserting the consequent $a$ of the attacked implication $\neg\neg a \rightarrow a$ .

These two examples show that the replacement of both conditions 2 and 3 by conditions 2′ and 3′, respectively, is necessary to obtain classical logic. Otherwise, there would not be winning proponent strategies for (all instances of) either tertium non datur or the principle of double negation elimination, which are both principles of classical logic.

b. Classical Dialogical Validity and Completeness

The dialogical notion of classical validity is defined as follows:

A formula A is called classically valid if there is a classical winning
proponent strategy for A.

The following completeness theorem holds:

A formula A is classically valid if and only if A is provable in
classical logic.

A proof of this theorem for a sequent calculus for classical logic can be found in Sørensen and Urzyczyn [2006].

A dialogical formulation of classical logic has thus been obtained by a modification of the dialogue conditions for intuitionistic dialogues. This means that one can obtain dialogical formulations of different logics by changing the rules of the dialogue games.

6. Origins and Recent Developments

The dialogical approach to logic was first proposed by Lorenzen in 1958 (Lorenzen [1960]; see also Lorenzen [1961]) for intuitionistic logic as well as for classical logic. That the dialogical approach as such cannot be taken as a foundation of intuitionistic logic is obvious, since a dialogical notion of classical validity can be obtained by modifying the dialogue conditions given for intuitionistic logic. If one wants to obtain a dialogical foundation for intuitionistic logic, it is therefore necessary to give a justification for the special kind of dialogues needed for intuitionistic logic. Such a justification has been proposed by Felscher [2002] (first published in 1986); it is based on the notions of contention, hypothesis and relevance.

The dialogical approach has been extended to several non-classical logics, including modal logic and linear logic; for an overview see Rahman and Keiff [2005] and Keiff [2011]. A dialogical setting for the interpretation of implications as rules has been considered by Piecha and Schroeder-Heister [2012]. Dialogical logic can thus provide a common basis for discussing different kinds of logics.

7. References and Further Reading

Andreas Blass. A Game Semantics for Linear Logic. Annals of Pure and Applied Logic, 56:183–220, 1992.
- Presents a dialogue semantics for linear logic. Starting point for game-theoretic developments in computer science.
Walter Felscher. Dialogues, Strategies, and Intuitionistic Provability. Annals of Pure and Applied Logic, 28:217–254, 1985.
- Constructive completeness proof for intuitionistic logic.
Walter Felscher. Dialogues as a Foundation for Intuitionistic Logic. In D. M. Gabbay and F. Guenthner, editors, Handbook of Philosophical Logic, 2nd Edition, Volume 5, pages 115–145. Kluwer, Dordrecht, 2002.
- Explains the basic concepts of dialogical logic, gives an overview on the literature on dialogues, and develops an argumentative foundation for a certain kind of dialogues as a basis for intuitionistic logic.
Wilfrid Hodges and Erik C. W. Krabbe. Dialogue Foundations. Aristotelian Society Supplementary Volume, 75:17–49, 2001.
- Critical discussion between Hodges and Krabbe on dialogues as a foundation for logic.
Laurent Keiff. Dialogical Logic. In E. N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Stanford University, Summer 2011 edition, 2011.
- Overview on dialogical logic, including dialogues for modal, linear and other non-classical logics. The presentation uses an alternative formalization of dialogical logic.
Erik C. W. Krabbe. Dialogue Logic. In D. M. Gabbay and J. Woods, editors, Handbook of the History of Logic, Volume 7: Logic and the Modalities in the Twentieth Century, pages 665–704. Elsevier North-Holland, Amsterdam, 2006.
- Traces the historical development of dialogical logic. Contains a useful bibliography.
Kuno Lorenz. Basic Objectives of Dialogue Logic in Historical Perspective. In Rahman and H. Rückert, editors, New Perspectives in Dialogical Logic, volume 127 of Synthese, pages 255–263. Springer, Berlin, 2001.
- Describes the development of dialogical logic in historical context, with emphasis on the notion of dialogue-definiteness.
Paul Lorenzen. Logik und Agon. In Atti del XII Congresso Internazionale di Filosofia (Venezia, 12–18 Settembre 1958), volume 4, pages 187–194. Sansoni Editore, Firenze, 1960.
- First proposal of dialogues as a means to explain intuitionistic logic and classical logic.
Paul Lorenzen. Ein dialogisches Konstruktivitätskriterium. In Infinitistic Methods. Proceedings of the Symposium on Foundations of Mathematics (Warsaw, 2–9 September 1959), pages 193–200. Pergamon Press, Oxford/London/New York/Paris, 1961.
- Dialogical explanation of the meaning of logical constants and of the meaning of inductive definitions.
Thomas Piecha and Peter Schroeder-Heister. Implications as Rules in Dialogical Semantics. In M. Peliš and V. Puncochár, editors, The Logica Yearbook 2011, pages 211–225. College Publications, London, 2012.
- Formulates dialogical semantics for implications-as-rules approach.
Shahid Rahman and Laurent Keiff. On How to Be a Dialogician. In D. Vanderveken, editor, Logic, Thought and Action, volume 2 of Logic, Epistemology, and the Unity of Science, pages 359–408. Springer, Dordrecht, 2005.
- Survey of dialogical formulations of a variety of logics.
Morten Heine Sørensen and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, New York, 2006.
- Contains a completeness proof for classical dialogues.
Wolfgang Stegmüller. Remarks on the completeness of logical systems relative to the validity-concepts of P. Lorenzen and K. Lorenz. Notre Dame Journal of Formal Logic, 5:81–112, 1964.
- Contains a comparison of the dialogical approach to semantics with the Bolzano-Tarski approach.

Author Information

Thomas Piecha
Email: thomas.piecha@uni-tuebingen.de
University of Tübingen
Germany

Internet Encyclopedia of Philosophy

Dialogical Logic

Table of Contents

1. Introduction

2. Argumentation Forms and the Meaning of Logical Constants

3. Dialogues for Intuitionistic Logic

a. Definition

b. Examples

4. Winning Strategies and Validity

a. Winning Strategies

b. Examples

c. First-Order Winning Strategies

d. Tertium Non Datur and the Principle of Non-Contradiction

e. Dialogical Validity and Completeness

f. Winning Strategies as Proofs

5. Dialogues for Classical Logic

a. Examples

b. Classical Dialogical Validity and Completeness

6. Origins and Recent Developments

7. References and Further Reading

Author Information

An encyclopedia of philosophy articles written by professional philosophers.