Stanford Encyclopedia of Philosophy
This is a file in the archives of the Stanford Encyclopedia of Philosophy.

Dialogical Logic

First published Thu Mar 5, 2009

The expression dialogical logic refers to a research tradition that can be traced back to Greek antiquity, when logic was conceived as the systematic study of dialogues in which two parties exchange arguments over a central claim. In its modern form, dialogical logic uses concepts of game theory to design dialogue games that provide a semantics for a wide range of logical systems. The modern approach, originally developed in the context of constructive mathematics and logic, has proved to be fruitful for the study, comparison and combination of various logical systems, such as paraconsistent, free, modal, and substructural logics.

1. Historical Overview

The dialogical approach to logic stems from the introduction of game-theoretical concepts in the definition of fundamental logical notions. A historical sketch of the relations between logic and games can be found in the entry on logic and games, and a detailed account can be found in Lorenz (2001). Dialogical logic, as we know it today, comes from Paul Lorenzen in the his work on the operative approach to constructive logic and mathematics. Lorenzen's dialogical approach was invented as a solution to some of the problems of the operative program. (For details on operative logic, see Lorenzen (1955)). In particular, the operative notion of derivation, which is essential to the definition of the operative notion of proposition, is, in general, undecidable. Furthermore, even if the derivation predicate were decidable, a serious problem would remain: defining a proposition via the notion of proof has the strange consequence that undecided propositions are not propositions at all. To address these problems, Lorenzen and Lorenz proposed the concept of dialogue:

Fully spelled out it means that for an entity to be a proposition there must exist a dialogue game associated with this entity, i.e., the proposition A, such that an individual play of the game where A occupies the initial position, i.e., a dialogue D(A) about A, reaches a final position with either win or loss after a finite number of moves according to definite rules: the dialogue game is defined as a finitary open two-person zero-sum game. (Lorenz 2001)

To briefly sketch the central concept, let us say that dialogues are games where what is at stake is a formula. The set of rules is designed in such a way that the formula is valid (in some definite sense of the term) iff the player defending the formula has a winning strategy in the game. An important aspect of constructivity in dialogical logic is obvious in this definition: infinity plays no role, i.e., it does not rely on a quantification over the set of models. The dialogical notion of proof is based on the notion of game, and, as mentioned in the quote above, dialogue games are finitary.

The dialogical approach yielded a semantics for intuitionistic and classical logic. Landmark publications include: Lorenzen (1958); Lorenz (1961); Stegmüller (1964); Lorenzen and Lorenz (1978); and Felscher (1985). The progressive clarification of the main concepts during the 70s opened the way, from the 80s up to present times, to an active research programme. During this period, Rahman and collaborators developed the original ideas into a conceptual framework that, for reasons the following sections will set out, proved useful for studying, comparing and combining non-classical logics (see Rückert 2001).

Another tradition in dialogical logic developed in parallel with the just-described one, with occasional and fruitful contacts with dialogical logic. The parallel tradition consists of the study of concrete dialogues, such as those that occur, for example, in natural languages. The aim of the parallel tradition was the study of the underlying logical regularities of these concrete dialogues. This tradition includes (to name but a few) the new rhetoric of Perelman (Perelman & L. Olbrechts-Tyteca 1958), Toulmin's argumentation theory (Toulmin 1958), Barth and Krabbe's theory of dialogue (Barth & Krabbe 1982), and Woods' work in argumentation theory (Woods et al. 2000). There has recently been an effort to bridge the two traditions of dialogical logic, especially in the context of the logical analysis of legal and more generally nonmonotonic reasoning. For more on these efforts, see, Prakken (2005).

2. Formal Dialogues

Dialogues provide a way to specify the semantics of a given logic. This section is devoted to a formal description of the rules of dialogical games for first-order logic in both its classical and intuitionistic versions. A detailed account of these rules can be found in Rahman & Keiff (2004) and Rahman & Tulenheimo (2006). For a textbook presentation (in French), see Fontaine & Redmond (2008). We first define a language, FO[τ], as the result of enriching a first-order language over vocabulary τ with the following metalogical symbols:

  1. two force symbols, ? and !;
  2. the symbols L, R, ∨, ∀x/c, ∃x (where x and c stand, respectively, for any variable and any constant of the vocabulary τ);
  3. two labels, O and P (standing for the players, Opponent and Proponent, respectively).

An expression of our language is either a first-order formula or one of the symbols listed above under (ii.). A dialogically signed expression is a triple ⟨X, f, e⟩, where X is a label, f is a force symbol and e is an expression. For convenience we write X-f-e. The intended meaning of such expressions is that player X played a move corresponding to expression e, and this move has to be considered as an attack (?) or a defence (!). We use X and Y as variables ranging on {O, P}, always assuming that X ≠ Y. It should be emphasized that it is not necessary to conceive the players of dialogical games as empirical human beings involved in a concrete game. They are often best seen as idealized agents, described by a strategy function, even if the connection with actual epistemic subjects is an important part of the dialogical foundation of meaning.

2.1 Rules for dialogical games

Let us now introduce the rules of the dialogical games. There are two kinds of such rules. Particle rules abstractly describe the way a formula can be attacked and defended, according to its main connective. Structural rules, on the other hand, specify the general organization of the game.

2.1.1 Particle Rules

A particle rule (also known as an argumentation form) abstractly describes the way a formula of a given main connective may be objected to, and how to answer the objection. By definition, an argumentation form is a tuple consisting of (1) an assertion, (2) a set of attacks, (3) a set of defences, and (4) a relation specifying for each attack the corresponding defence(s). Argumentation forms are abstract in the sense that, in their definition, no reference is made to the context of argumentation in which the rule is applied (understood as a situation in a process of argumentation, e.g., as the set of argument moves made before the assertion for which the particle rule is defined). The particle rules thus constitute the local semantics of a logic, for they determine the dialogical meaning of each logical constant but say nothing about the way this meaning may be related to anything else. Yet the local semantics given by the particle rules are intrinsically dependent of the notion of dialogue, since they describe sequences of language acts.

In the following tables, A and B are formulas and A[x/c] denotes the formula resulting from the substitution of c for any free occurrence of the variable x in A. Notice that there is no argumentation form for atomic formulas.

∧ ∨ ¬
Assert X-!-A∧B X-!-A∨B X-!-¬A
Attack Y-?-L or Y-?-R Y-?-∨ Y-!-A
Defend X-!-A resp. X-!-B X-!-A or X-!-B —

→ ∀ ∃
Assert X-!-A→B X-!-∀xA X-!-∃xA
Attack Y-!-A Y-?-∀x/c
for any c that Y chooses 		Y-?-∃
Defend X-!-B X-!-A[x/c] X-!-A[x/c]
for any c that X chooses

In the context of a dialogue, a pair consisting of an attack and the corresponding defence is called a round. The attack is said to open the round, and the defence to close it.

The explication of these rules is fairly obvious. Disjunction and conjunction differ only by the player who has the choice of the immediate subformula with which the game will proceed: in a conjunction, the challenger may choose, confident that either disjunct can be refuted; in a disjunction the choice lies with the defender. Thus, to defend a conjunction, a player must be able to defend any of the conjuncts, while in the case of a disjunction, it is sufficient to be able to defend one of the disjuncts. The rules are similar in the case of quantifiers: when attacking a universal quantifier, the challenger can choose the instantiation he fancies for the bound variable. When the assertion is existentially quantified, the defender chooses the instantiation. There is admittedly something less immediately intuitive in the case of negation and implication. In both cases, the attack bears a defence force (!). One may convince himself this is indeed correct by considering the following: in a dialectical situation, the only way to attack the assertion ¬A is to assert A, and be prepared to defend this assertion. Thus there is no proper defence against such an attack, but it may be possible to counterattack the assertion of A. Along the same lines, to challenge an implication essentially amounts to providing a proof of the antecedent and claiming that the other player will fail to build a proof of the consequent from it. The defence against such an attack then consists of a proof of the consequent. As underlined in the historical overview, dialogical logic was born in the context of constructivism, so it is not a surprise that the attack against ¬A and A→B is the same: the constructive negation of A reads as A→⊥.

It should be noted that this phenomenon is by no means a trifle: as will be shown later, stipulations about the way the Proponent can make use of the assertive content of such attacks by the Opponent are precisely what yields a variety of dialogical systems corresponding to (e.g.) minimal logic, intuitionistic logic, free logics, or paraconsistent logics (see Section 3: Dialogues for Non-Classical Notions of Validity and the supplementary document Some Dialogical Systems for Non-Classical Logics.).

Another way to understand the particle rules is to think of them as describing the evolution of the state of the (structurally unspecified) dialogue. States of the dialogue contain information on the formula about which the debate is running and on the mapping of roles (challenger and defender) onto the set of players. Let A ∈ FO[τ]. Let C={c0, c1, …} be a set of individual constants. A state of the dialogue for A is a triple S=⟨ρ, σ, Φ⟩ where:

Note that the player label of Φ is independent of the role distribution defined by ρ, i.e., the player that asserts a formula in a dialogue may be either challenger or defender. We say that the state of the dialogue S2 = ⟨ρ2, σ2, Φ2⟩ is reachable from the state S1 = ⟨ρ1, σ1, Φ1⟩ iff S2 follows from S1 as a result of the players making the moves stipulated by the corresponding particle rules, in the roles determined by ρ1. The player whose role is challenger (?) states an attack, the other (!) states a defence. Thus particle rules tell us what states of the dialogue are reachable from a given state S1 = ⟨ρ1, σ1, Φ1⟩, according to the main connective in the formula B in Φ1. What follows is a recursive definition of the reachability relation between states. As already mentioned, ρ1−1(!) denotes the player defending the formula at stake in the corresponding state of the dialogue (i.e., under a specified role assignment), and ρ1−1(?) denotes the challenger of this formula. Let Φ1 = ρ1−1(!)-B. S2 = ⟨ρ2, σ2, Φ2⟩ is reachable from the state

S1 = ⟨ρ1, σ1, ρ1−1(!)-B⟩

if S2 satisfies the following:

Particle rule for conjunction. If B is of the form C∧D, then both S2 and S3 are reachable, namely:

S2 = ⟨ρ1, σ1, ρ1−1(!)-C⟩
S3 = ⟨ρ1, σ1, ρ1−1(!)-D⟩

according to the choice of ρ1−1(?), between the two attacks ?-L and ?-R. The role assignment is not altered.

Particle rule for disjunction. If B is of the form C∨D, then both S2 and S3 are reachable, namely:

S2 = ⟨ρ1, σ1, ρ1−1(!)-C⟩
S3 = ⟨ρ1, σ1, ρ1−1(!)-D⟩

according to the choice of ρ1−1(!), after an attack ?-∨ of ρ1−1(?). The role assignment is not altered.

Let us now turn to the less obvious rules for negation and implication.

Particle rule for negation. If B is of the form ¬C, then

S2 = ⟨ρ1′, σ1, ρ1′−1(!)-C⟩

Notice that the distribution of roles is inverted (ρ1′), so that in the new state of the dialogue, the player that was previously challenger of ¬C is now defender of C. Nevertheless, the move ρ1′−1(!)-C is an attack.

Particle rule for implication. If B is of the form C→D, then

S2 = ⟨ρ1′, σ1, ρ1′−1(!)-C⟩

Again, to attack an implication amounts to being prepared to defend its antecedent, so it should be noted that the move ρ1′−1(!)-C counts as an attack. The game will then proceed, up to the choice of ρ1′−1(?), according to the relevant particle rule for C, or to a new state of the dialogue

S3 = ⟨ρ1, σ1, ρ1−1(!)-D⟩

Note that the role assignment has changed again (to ρ1′′=ρ1), so that the player defending C→D in S1 is now defending D in S3.

Particle rules for the quantifiers present no difficulty: as for disjunction and conjunction, the only difference is the player who chooses the instantiation of the bounded variable.

Particle rule for universal quantifier. If B is of the form ∀xC(x), then

S2 = ⟨ρ1, σ1[x/c], ρ1−1(!)-C(x)⟩

where ci is a constant chosen by ρ1−1(?) when attacking with ?-∀x/ci, and σ1[x/ci] stipulates that the occurrences of x that were bound by the quantifier are now to be interpreted as ci.

Particle rule for existential quantifier. If B is of the form ∃xC(x), then

S2 = ⟨ρ1, σ1, ρ1−1(!)-C(x)⟩

where ci is a constant chosen by ρ1−1(!) when defending against the attack ?-∃ of ρ1−1(?), and σ1[x/ci] stipulates that the occurrences of x that were bound by the quantifier are now to be interpreted as ci.

2.1.2 Structural rules

In the same way as particle rules describe the local meaning of the logical constants, structural rules determine their global semantics. As is the case in the context of substructural logics, the notion of proof in a given dialogue system is determined by the structural rules. Structural rules thus describe the way an argumentation is built, which means they are responsible for the general organization of the dialogues. The structural rules are meant to organize the application of the particle rules in such a way that the set of moves resulting from the application of the rules to an initial formula (called the thesis) yields a dialogue that can be seen as a valid argument for the thesis. There is, of course, a wide range of notions of validity, but here we are particularly interested in logical validity. So the rules should be designed in such a way that a certain type of completion of the dialogue for a given thesis constitutes a proof of its logical validity. But it should be noted that other normative concepts could be used to shape the structural rules, e.g., adequacy to idealized empirical argumentation, like it is in, for example, legal argumentation theory. See the end of Section 2.2.2 for some general comments on the formulation of structural rules.

As will be emphasized in the next section, the notion of proof in the context of logical dialogues is based on the existence of a winning strategy for the Proponent. This will be reflected in the definitions we use. A dialogue can be thought of as a set of dialogical games, which are in turn sequences of dialogically signed expressions X-f-e. Dialogical games are structured as a tree, the root of which is constituted by a (possibly empty) sequence of premises together with the thesis of the dialogue in the final position. Splits in the dialogue tree are generated by the propositional choices of the Opponent. Any possible attack by the Opponent against a conjunction, any possible defence of a disjunction, and either possible reaction in the case of an attack by the Proponent against a conditional he defends (counterattack or defence) will generate a new branch in the dialogue tree. No move of the Proponent will open a new branch. A completed dialogue tree will thus contain all the Opponent's possible choices.

As already mentioned, a dialogue is a set of sequences of dialogically signed expressions. All sequences have as a common root a (possibly empty) sequence of premises, together with the thesis. All other members of the games are termed moves, and we say that a player makes a move. According to the player making the move, we talk about P-moves or O-moves. Any move is either an attack or a defence. The particle rules stipulate exactly which of the moves are to be counted as attacks. Obviously, any move which is not an attack is a defence. A move X-f-e is said to have a propositional content iff e is a first-order formula (e ∈ FO[τ]). D(A) denotes the dialogue with, as a thesis, a move of the form P-!-A, and we say that D(A) is a dialogue for A. There exists a dialogue for A iff A ∈ FO[τ]. Premises of a dialogue must have a propositional content, and are moves of the form O-!-A occurring at the beginning of the dialogue. D(A;A1, …, An) denotes a dialogue for A with premises of propositional content A1, …, An. Δ1, …, Δn denote the dialogical games that are members of D(A). Δ1[n] denotes the n-th member of the sequence Δ1, and we talk of the rank n of the move Δ[n]: when writing down a dialogue, one keeps track of the assertion/attack relation by adding an extra label to the attack moves, namely the rank of the assertion attacked. This will become clear in the examples.

Now let us state the structural rules.

SR-0: Starting Rule.
For any Δ ∈ D(A), the thesis has position 0:

Δ[0]=P-!-A

For any n > 0 and for any Δ ∈ D(A) such that Δ[n] exists, if n is even then Δ[n] denotes a P-move and otherwise denotes an O-move. If the set of premises is not empty, then all the dialogical games contain it. Let A0, …, Ai be the propositional content of the premises. Then for all Δ ∈ D(A), Δ begins with i terms of rank H0, …, Hi such that Δ[H0] = O-!-A0, …, Δ[Hi]=O-!-Ai.These moves are the premises of the dialogue D(A). The set of all premises of D(A) together with the thesis is called the root of D(A).

Any move following the thesis is a reaction to a previous move by the other player, and must comply with all the structural and particle rules of the dialogue.

SR-1i: Intuitionistic Round Closure Rule.
Whenever player X is to play, he can attack any move of Y in so far as the other rules let him do so, or defend against the last attack of Y (i.e., the attack in the game with the highest rank), provided he has not already defended against it. A player may postpone a defence as long as there are attacks he can put forth.
SR-1c: Classical Round Closure Rule.
Whenever player X is to play, he can attack any move of Y in so far as the other rules let him do so, or defend against any attack of Y (even the ones against which he has already defended). In other terms, players can play again earlier defences (which makes sense when another move is available).

Notice that the rules of a dialogical system cannot include both SR-1i and SR-1c (see Section 2.2).

SR-2: Branching Rule For Dialogical Games.
Let Δ ∈ D(A) be a dialogical game of even length (that is, where O is to play). There are three cases in which Δ will be extended in such a way that it will generate two distinct (new) games Δ1 and Δ2. Let n be the length of Δ and m be the number of premises of D(A), then for all i ∈ {H0, …, Hm,0, …, n}, Δ1[i]=Δ2[i].

  1. Assume for some m such that 0<m<n, Δ[m]= O-!-B∨C and Δ[n]= P-?-∨. Then O may choose to extend Δ to Δ1 and Δ2 with two moves:
    Δ1[n+1]= O-!-B
    Δ2[n+1]= O-!-C
  2. Assume that Δ [n]= P-!-B∧C. Then O may choose to extend Δ to Δ1 and Δ2 with two moves:
    Δ1[n+1]= O-?-L
    Δ2[n+1]= O-?-R
  3. Assume for some m such that 0<m<n, Δ [m]= O-!-B→C and Δ[n]= P-!-B. Then O may choose to extend Δ to Δ1 and Δ2 with two moves:
    Δ1[n+1]= O-?-…

    Here the dots stand for an attack corresponding to the relevant particle rule, according to formula B.

    Δ2[n+1]= O-!-C

No other game situation will generate distinct dialogical games, i.e., in any other case, the next move will be Δ[n+1]. Actually, one could make SR-2 symmetric, and let P generate new games too. But, as the following rule will show, it is always strategically the best choice for P to stay in the same context.

Notice that the explicit reference to logical constants here is just a convenient way to give a formally precise account of the notion of O-choice. Actually, a general formulation (although less precise) for this rule would be: any game situation were O is to play and has to chose between several moves will generate a distinct game for every choice available to O.

SR-3a: Winning Rule For Dialogical Games.
A dialogical game Δ ∈ D(A) is said to be closed iff there is some atomic formula which has been played by both players. More precisely, Δ is closed iff there are two integers m and n and an atomic formula α ∈ Sub(A)∪{A} such that the propositional content of Δ[m] is α and is identical to the propositional content of Δ[n], and exactly one of {Δ[m], Δ[n]} is a P-move (the other one being, consequently, an O-move). A dialogical game is open iff it is not closed.

A dialogical game is finished iff it is closed or the rules do not allow any further move by the player who has to move. Let Δ be a finished game. If Δ is closed, the player who stated the thesis (i.e., P according to rule SR-0) wins it, otherwise he loses it. A finished game cannot be extended.

SR-4: Shifting Rule.
Let Δ, Δ′ ∈ D(A) be two distinct dialogical games. Assume O has chosen to play in Δ. O may switch to Δ′ iff he has lost the game Δ. In other words, O cannot switch to another game before the game he is playing is closed.

Notice that D(A) can be seen as a sequence of games, in the sense that the order in which O chooses to play the different dialogical games of the dialogue yields a different course for the dialogue. Such an order on the games of a dialogue D(A) is called a play of D(A). ⟨D(A), p⟩ denotes the play p of dialogue D(A).

SR-3b: Winning Rule for Dialogical Plays.
Let ⟨D(A), p⟩ be a play p of D(A) of the form p=⟨Δ0, …, Δn, Δ⟩. ⟨D(A), p⟩ is finished iff all games Δ0, …, Δn are closed and Δ is finished. ⟨D(A), p⟩ is closed iff it is finished and Δ is closed. P wins the play ⟨D(A), p⟩ iff ⟨D(A), p⟩ is closed, otherwise O wins.
SR-5: Formal Use of Atomic Formulas.
Let ⟨D(A), p⟩ be a dialogical play. Δi[m] is a move previous to Δi[n] iff m<n. An atomic formula α is said to be introduced in a play ⟨D(A), p⟩ by move Δi[n] iff (i) α is the propositional content of Δi[n]; (ii) there is no previous move Δi[m] such that α is the propositional content of Δi[m]. That is, an atomic formula is introduced by a move if it has not been played in a previous move of the play.

P cannot introduce atomic formulas. That is, P can make a move whose propositional content is an atomic formula α in a play p of D(A) iff O introduced α in a previous move. Atomic formulas cannot be attacked.

Because of the formal restriction, the game for quantifiers is asymmetric, in the sense that any time he can, O will try to introduce a new constant (in order to prevent P from using the information O already conceded); and for dual reasons, P will always try to use the constants already conceded. Some important aspects of the meaning of the SR-5 rule are discussed in the second example of Section 2.3.

To state the next rule, we first need some definitions.

Definition: Strict Repetitions

A constant is said to be used by a player if the player chooses it to attack a universal quantifier or to defend an existential quantifier. A constant is said to be new if it is used by a player and has not been used by either player in a previous move.

Let Δ[m] X-?-e be an attack against some previous move Δ[n]. We say that Δ[m] is a strict repetition iff either (i) there exists some move Δ[k] such that n<k<m, and Δ[k] is an attack against Δ[n] with an expression e identical to the expression in Δ[m]; or (ii) Δ[m] is an attack against an universal quantifier asserted in Δ[n], introducing a new constant, and there exists some move Δ[k] such that n<k<m, and Δ[k] also attacks Δ[n] introducing a new constant.

Let Δ[m] X-!-e be a defence against some previous attack Δ[n]. We say that Δ[m] is a strict repetition iff either (i) there exists some move Δ[k] such that n<k<m, and Δ[k] is a defence against Δ[n] with an expression e identical to the one in Δ[m]; or (ii) Δ[m] is a defence of an existential quantifier, introducing a new constant, and there exists some move Δ[k] such that n<k<m, and Δ[k] defends the same quantifier, also by introducing a constant which was new at k.

Nothing else is a strict repetition.

We can now state the next rule, which has classical and intuitionistic variants corresponding respectively to SR-1c and SR-1i:

SR-6c: Classical No-Delaying-Tactics Rule.
No strict repetition is allowed.
SR-6i: Intuitionistic No-Delaying-Tactics Rule.
If O has introduced an atomic formula which can be now used by P, then P may perform a repetition of an attack. No other type of repetition is allowed.

2.2 Dialogues as logic

The rules of the dialogical games are defined, but now the question is: how do such games relate to logic in the first place? In the tradition of dialogical logic, it is usual to define validity using the notion of winning strategy for the Proponent.

A strategy for player X in a dialogical game is a function taking histories (i.e., sequences of moves of the game whose first member is the thesis (or the set of premises and the thesis) and such that all subsequent moves comply with the rules) where the last move is a Y-move as arguments, and (legal) X-moves as values. In other terms, a strategy is a function that tells to a player what to do according to what has previously happened in the game. A strategy in this sense must tell X what to do against any possible sequence of Y-moves (i.e., in all possible histories). A winning strategy for X is a strategy such that X will win the game if he makes all his moves according to the strategy. Notice that the relevant arguments for a winning strategy for X are sequences of moves that differ in the Y-moves, since the X-moves are determined by the strategy itself.

The structural rules, in the version presented here, are conceived with the purpose of reflecting the notion of strategy in the way the (global) game is organised. Indeed, P cannot win a play of D(A) unless he is able to win the game against all possible moves by O: each dialogical game is defined by a sequence of choices of O, so the set of all the games is the set of all possible O-choices in the dialogue. Thus we can define the notion of validity without explicit reference to strategy:

Definition (Validity):

A first-order sentence A is said to be dialogically valid if all dialogical games belonging to the dialogue D(A) are closed.

More generally, we can define a notion of (dia)logical consequence:

Definition (Dialogical Consequence):

A first-order sentence A is said to be a dialogical consequence of a finite set Γ={A0, …, An} of first-order sentences if all dialogical games belonging to the dialogue D(A), whose root consists of a set of premises of propositional content A0, …, An and A as a thesis, are closed.

An interesting philosophical property of the dialogical approach is that the difference between notions of logical consequence is expressed as a difference in the structural rules. This feature is exemplified by the set of rules presented in the previous section. If one takes the whole set except SR-1i, then it can be shown that an FO sentence is dialogically valid iff it is a valid sentence of FO classical logic. If, on the other hand, one takes the whole set of rules except SR-1c and SR-6c, then an FO sentence is dialogically valid iff it is a valid sentence of FO intuitionistic logic.

To see how such characterization theorems can be proved, observe that the states of the game as described in the particle rules correspond exactly to the tableau rules for the same connectives when embedded in a dialogue. For a thorough introduction to tableau methods, see d'Agostino et al (1999). The O-signed formulas of the states of the dialogue correspond to T-labeled formulas of the tableaux, while P-formulas correspond to the F-labeled formulas. Now observe that the branching rules of dialogical games correspond to the branching rules of tableaux: dialogical games split when O defends a disjunction (T-A∨B), attacks a P-conjunction (F-A∧B), or reacts to an attack against his assertion of a conditional (T-A→B). The match between quantifier rules can be seen thus: when O defends an existential quantifier (T-∃xA) or attacks a universal quantifier (F-∀xA), his best option is to prevent P from using atomic formulas he himself conceded previously in the game (remember the formal restriction SR-5) so any time he can, he will introduce a new constant. Intuitionistic tableaux are a little more complicated, for the set of formulas to which the expansion rules can be applied is a subset of the formulas on the branch, so a marking device is needed in order to keep track of what formulas are available at a given stage of the tree-building process. Complete descriptions and proofs can be found in Rahman (1993). An earlier formulation of the proofs related to natural deduction and sequent calculus can be found in Haas (1980), and Felscher (1985). As to Haas (1980) Felscher remarks “it seems that the technical gaps contained in this work are only minor and can actually be filled”, (1985, p. 351).

2.2.1 Dialogues and tableaux

When considering dialogues for validity, there is a straightforward way to transform a dialogue into a tableau and back. Thus the difference is not so much technical, but rather philosophical. It is also twofold. First, as already noted, dialogue systems are not necessarily intended to capture a notion of validity. Concrete plays of the dialogical games could include errors, fallacies, failure in proof search, etc. Thus the dialogues that do characterize a definite notion of validity can be seen as an abstraction from concrete, empirical dialogue games. This leads to the second point: it has been claimed (e.g., in Lorenzen & Lorenz 1978) that the genetic link between concrete dialogues and validity dialogues explain why the rules of validity games are the way they are. Extrapolating from this point, one would say then that the dialogical approach offers a philosophical standpoint that also gives an explanation of the tableaux rules.

The last point is of particular interest. The branchings that occur in a tableau proof receive a natural explanation in a dialogical perspective, namely in terms of strategies. Actually, one can show that a tableau proof is a reduct of the extensive form of the dialogical game, where O's choices are the only ones that are taken into account. Such a reduct is useful since it exhibits the winning strategy: P has a winning strategy if, and only if, any leaf of the tree is a P move. To see the connection with the usual tableau closure rule, consider the following. The propositional content of such a move can only be an atomic formula (else there would be challenges available to O), and the formal restriction warrants that the same atomic formula has been introduced by O earlier in the same branch.

It is thus possible to understand tableau proofs as a form of metalogical reasoning about a game, whose features determine and explain the form of the tableau rules.

2.2.2 Structural rules and logical pluralism

From the dialogical perspective, as already noted, differences between logical systems are conceived as differences in the sets of structural rules. In this respect, dialogues are akin to the substructural approach (see the entry on substructural logics). This feature has a philosophical importance that has been elaborated in J. C. Beall and G. Restall's series of papers dedicated to logical pluralism (e.g., see Restall 2002). Quine argues that it makes no sense to talk about a plurality of logics, because this plurality is just linguistic, not logical. Changing the meaning of the logical constants amounts to simply changing the subject, i.e., changing of idiom. Now, says Quine, when a translation suggests that a speaker is making use of another notion of logical consequence between the assertions he makes, Occam's razor (in the form of the Charity Principle) tells us that it is more parsimonious to consider that our translation of what the speaker says is incorrect, rather than the speaker making use of another logic. So logical changes are just linguistic changes (e.g., paraconsistent negation is, in this view, not talking about the meaning of “not”, but rather about some other indigenous connective), and there cannot be any controversy about the meaning of the logical constants. But from a dialogical point of view, in so far as local semantics (i.e., the introduction/elimination rules, or, dialogically, the particle rules) stay untouched, there seem to be strong grounds to the claim that we are indeed talking about the same language. So the different sets of structural rules actually define different theories of inference, and there seem to be no unquestionable grounds for the claim that one of them is the only correct one.

There is no general theory of the way structural rules should be formulated, and there is no unique language in which all possible structural rules should be expressed. There are, nevertheless, some regular patterns that may be worth noting. There is a core of structural rules that remain fairly unchanged from one system to another: these rules define what a game is, who the players are, the order of the moves and what a winning move is (i.e., rules SR-0, 2, 3a, 3b, 4). The structural rules that are altered in order to produce the dialogical systems overviewed in Section 3 are those that remain. They stipulate which moves can be attacked, when a defence can be made, and what can be asserted by the players. Now, with the exception of the modal systems, many of the dialogical systems in the literature are subclassical, in the sense that the set of valid formulas of these systems is a subset of the set of classically valid formulas. A typical modus operandi to produce a subclassical system is to modify the rules in order to restrict the moves available to the Proponent, thus restricting the set of his winning strategies (i.e., of the dialogically valid formulas). Section 3 contains various detailed examples of such restriction-generated systems, and the interested reader may also consult the supplementary document Some Dialogical Systems for Non-Classical Logics. Details of the connection between structural rules of Gentzen-Style sequent calculi and their dialogical counterparts are given in Section 4.

2.2.3 Dialogues, constructivity and the procedural aspect of proofs

As a legacy from the philosophical stance of the fathers of the dialogical approach, the systems of dialogical logic are usually constructive procedures to prove the validity of formulas. Let the length of a dialogue be the sum of the length of all its finished games. Notice that, in the case of propositional logic, the SR-6 rules ensure that dialogues for a finite root (i.e., a root consisting of a finite set of premises and a thesis, all being formulas of finite length) are of finite length. Indeed, each attack/defence pair in a game eliminates one connective from the formula at stake, in the sense that the game will proceed with respect to a strict subformula of the formula which has been attacked and defended. So after finitely many such pairs, the game will finish, reaching the atoms of the formulas in the root of the dialogue, which (according to SR-5) cannot be attacked, since all attacks and defences allowed by SR-6 have been performed. Finitely many moves of such a game will yield a splitting between exactly two finite games, and so on. So the length of the whole dialogue is finite. This property is conserved in all the non-classical variants of propositional logic presented in Section 3 and the supplementary document Some Dialogical Systems for Non-Classical Logics, and plays an important role in the GTS-style dialogues of Section 5.

Nevertheless, this doesn't mean that every system of dialogical logic will constitute a constructive decision procedure. For instance, one can give dialogue rules for second-order logic using lambda-abstraction, and such a system would not be a decision procedure. The reason is that even though one could prove the system sound and complete (i.e., that there is a winning strategy for P in a dialogue for a second order formula A iff A is valid), there is no way to systematically define such a winning strategy. The finding of the strategy requires from P what one could see as a “creative” step, in the sense that there is no mechanical way to compute all the moves of an arbitrary strategy.

Being essentially procedural, dialogues well capture the dynamic aspects of logic. It was already stated that the point of using dialogues to give a semantics to intuitionistic logic: the SR-1i rule amounts to requiring of P that at any stage of the game he is able to provide grounds for his assertions without having to rely on later concessions of O (i.e., attacks against a negation or a conditional). (See the third example in Section 2.3.) Fruitful research in the context of legal reasoning has shown that dialogues can be devised where some of the rules of the dialogue can be discussed and modified within the very process of the dialogue. V and F operators of connexive dialogical logic provide an example of the way a change in the rules can be coded in the syntax (see Section 4 of supplementary document the Some Dialogical Systems for Non-Classical Logics).

2.3 Examples

Let us examine some concrete examples of how a dialogue is built in the case of simple formulas. A dialogical proof of validity is written in the form of a table, with as a main division one column for O and one for P. Each line of a table bears one move of the corresponding player. Each of the two (O and P) columns is divided in three: the outer sub-column bears the rank label of the move; when the move is an attack, the inner sub-column bears the rank of the attacked move; finally, the centre sub-column indicates the dialogical expression contained in the move. An attack and the corresponding defence (when it is performed) are written on the same line. Thus a completed line represents a closed round.

Let us begin with a contingent formula.

The Opponent Wins
O P
(α∨β)→α 0
1 (α∨β) 0 α 4
3 α 1 ?v 2
3′ β

Here the Opponent makes a redundant move, namely conceding that α holds to defend the disjunction asserted in 1. Move 4 closes this dialogical game, then O has the right to switch to a new game with 3′, where he wins. P has to move, and there is nothing to attack or defend. This play of the game is finished and not closed; O wins, the formula is not valid.

Let us now turn to the proof of a simple tautology, a proof which is almost trivial, and yet displays some of the most important aspects of dialogical proof theory.

Classical proof for α→α
O P
α→α 0
1 α 0 α 2
3 ?α 2   !α 6
5 !α 3 ?α 4

This basic dialogue contains just one game, including moves 0 to 2. The dialogue is obviously closed. Now, such a dialogical proof features a dynamics in the flow of information that is proper to game semantics of the dialogical kind. One way to make this flow explicit is to extend the game with some (abstract sketch of) dialectical reasoning about the atomic formula. This is what is informally noted here as moves 3 to 6. Those moves are not a part of the actual dialogue but a representation of the following considerations. The justification of the assertion of a complex sentence in a dialogue is given with respect to its subsentences. The process is recursive, and eventually stops when reaching atomic sentences. Now the justification of such atomic assertions is not considered in the formulation of the game when one wants to capture the notion of validity. The formal rule says that whatever concept of justification for atomic sentences is good enough for O will suffice for P. But there is more to say within a game-theoretical framework about the connection between formal dialogues and other kind of argumentation processes where atomic sentences are justified. Such processes are precisely what we refer to with !α.

In 3, the Opponent asks on what grounds the Proponent asserted the atom α. Now the Proponent's answer is a counterattack (move 4). P's strategy for grounding his assertion that α holds can be paraphrased thus: “I don't have my own justification, but whatever grounds you assumed when you asserted α are good enough for me”. This so-called copycat strategy is the core of the formal restriction (SR-5). From this point of view, atoms are nothing but unknown or arbitrary formulas, for which the proof strategy may even not be known. SR-5 structurally reflects the existence of an abstract strategy, which is a winning strategy regardless of the concrete nature or shape of the proof of the relevant atom.

The following example illustrates the insights that dialogical logic offers on the difference between classical and intuitionistic logic:

Classical proof for the Excluded Middle
O P
α ∨ ¬α 0
1 ?v 0 ¬α 2
3 α        
1′ [?v] 0 α 4

To defend against attack 1, P has to choose ¬α, because the other disjunct is an atom that he cannot state before O has conceded it. In attacking the negation in 3, O concedes the means to defend the other disjunct. With classical rules, P can make use of this information to defend again in 4 and win. Such a defence is not allowed in intuitionistic logic, which takes seriously the procedural nature of the proof. P's defence in 2 will lead to a loss because P has to choose without knowing which disjunct he has a proof for. When he eventually gets the information to justify a choice, it will be too late intuitionistically.

The following example illustrates the importance of the flow of information within a proof.

Classical proof
O P
∃x(Px→∀xPx) 0
1 ?∃ 0 Pc1→∀xPx 2
3 Pc1 2   ∀xPx 4
5 ?∀/c2 4 Pc2 8
Pc2→∀xPx 6
7 Pc2 6

The decisive move is the defence 6, where P defends again against attack 1, bearing in mind the constant chosen by O in his attack 5. O's attack in 7 gives P the right atom in order to defend against 5. The dialogue system for free logic shows the importance of taking the choice of an interpretation for variables as an explicit move.

3. Dialogues for Non-Classical Notions of Validity

As has been mentioned already, dialogical logic has converted itself into a conceptual framework of sufficient generality to be able to express, combine and compare a number of diverse notions of validity of logical inference. Actually, the idea of dialogical logic as a general framework emerged during the late 1990s, and represents a radical change from the strict constructivism of the origins. Here, we shall concentrate on two examples, namely the dialogical systems for normal modal logics and for linear logic. See the supplementary document the Some Dialogical Systems for Non-Classical Logics for dialogical systems for free, paraconsistent and connexive logics.

3.1 Modal dialogues

Modal dialogues are developed in Rahman and Rückert (1997). See the entry on Modal Logic for an overview.

Let us extend our vocabulary with two modal operators, □ and ♢, which as usual we intend to read as (alethic) necessity (resp. possibility). In order to define the particle rules for such operators, we must first adjust the syntax of the dialogical moves. One can see modalities as making explicit the context in which an assertion is made. In this perspective, modal dialogues should exhibit in the syntax the contextual nature of the moves. A modal (dialogically signed) formula thus has the form X-f-e-ν where X and f are the same as usual, ν is a label (i.e., a string of integers, which will be explained later) denoting the dialogical context, and e is an expression of our enriched language, including, for any label ν, an expression of the form □/ν. Particle rules for modalities are stated in the following table:

Assert X-!-□A-ν X-!-♢A-ν
Attack Y-?-□/ν′-ν
where ν′ is a dialogical context chosen by Y 		Y-?-♢-ν
Defend X-!-A-ν′ X-!-A-ν′
where ν′ is a dialogical context chosen by Y

Particle rules can also be defined with respect to the accessibility relation between states of the modal game, which are tuples of the form: S=⟨ρ, σ, Φ, λ⟩, where ρ and σ are the same as usual, Φ is a modal formula, and λ is an assignment of dialogical contexts to formulas.

Let S1 = ⟨ρ, σ, ρ−1(!)-□A , λ⟩. S2 is accessible from S1 iff

S2 = ⟨ρ, σ, ρ−1(!)-A, λA/ν⟩

where λA/ν denotes the result of extending λ assigning context ν to the formula A. S2 is reached after an attack ρ−1(?)-□/ν, where ν is a dialogical context chosen by ρ−1(?).

Let S1 = ⟨ρ, σ, ρ−1(!)-♢A, λ⟩. S2 is accessible from S1 iff

S2 = ⟨ρ, σ, ρ−1(!)-A, λA/ν⟩

where λA/ν denotes the result of extending λ assigning context ν to the formula A. S2 is reached after an attack ρ−1(?)-♢. ν is a dialogical context chosen by ρ−1(!).

Since the development of the possible worlds semantics for modal logic, differences between modal logics are usually understood as differences in the properties of the accessibility relation in Kripke models. Now, this relation is dialogically captured by the structural rules stipulating, in the context of a modal game, what labels can be used by the players in order to attack and defend modal assertions. Let us be more precise. The syntax of such labels obeys the following:

  1. they consist of a finite string of integers: ν=x0.x1. … .xn separated by dots;
  2. there is one distinguished context, the original context, denoted by the label 1;
  3. the set of labels is semi-ordered by a relation of succession, forming a tree, and made explicit in this way: if ν denotes a dialogical context, then ν.i (for i=1 to n) denote the n successors of ν.

The original context has rank 1. For any context of rank n, its successors have rank n+1. We say that a player uses a label when he chooses this label to attack a □ operator or to defend a ♢ operator. A player introduces a label ν, and a label is new iff the player uses the label in some move Δ[n] and there is no previous move Δ[m] in the same game where ν is used.

It is important here to keep in mind that modal dialogues feature two distinct tree structures. First, a dialogical game is a tree whose branches are plays of the game, and a branching occurs when O has a choice between different moves. Second, the dialogical contexts are structured as a tree, where a branch is a chain of contexts connected by a successor relation. The contexts of the dialogical expressions in a single play of a dialogical game may well be structured as a branching tree with the original context as a root.

Some of the structural rules have to be rephrased along the following lines:

Let us now give the structural rules that will specifically yield a dialogical notion of validity that is sound and complete with respect to the principal normal modal systems.

SR-7: Formal Use of Modal Labels.
O may introduce a context any time the other rules let him do so. P cannot introduce a context, and his choices when opening a context are restricted by the adequate (SR-8) rule which reconstructs the properties of the accessibility relation particular to the modal dialogical logic in question.

For the label accessibility rule, the idea is straightforward. The minimal K-accessibility relation is expressed by letting P use the label of a successor of the context he is playing in, provided of course that O already conceded its existence (introduced it). Reflexivity amounts to letting P choose the label of the context he is already playing in. Symmetry is captured by assuming that when a context has access to a successor, then this context is accessible from the successor. Transitivity frees P from the obligation to choose an immediate successor (or predecessor in the presence of symmetry). The formulation of the structural rule for the following systems is just the result of a combination of these notions. Remember that P's choices of labels are restricted by SR-7.

SR-8K: Label Accessibility for K.
P may choose any dialogical label that has been introduced by O of rank +1 relative to the context he is playing in.
SR-8T: Label Accessibility for T.
P may either choose the dialogical label of the context he is playing in, or he may choose any dialogical label that has been introduced by O of rank +1 relative to the label of the context he is playing in.
SR-8B: Label Accessibility for B.
P may either choose the dialogical label of the context he is playing in, or he may choose any dialogical label that has been introduced by O of rank -1 or +1 relative to the label of the context he is playing in.
SR-8S4: Label Accessibility for S4.
P may either choose the dialogical label of the context he is playing in, or choose any dialogical context that has been introduced by O of any rank superior to the context he is playing in.
SR-8S5: Label Accessibility for S5.
P may choose any dialogical label that has been introduced by O.

In the case of a serial accessibility relation, characteristic of the system D, the formal rule SR-7 is inadequate: if we want to capture the fact that any context has access to at least another one, then we clearly need to let P make use of this assumption without needing any previous concession by O. In this case, just one modal rule is needed.

SR-7D: Label Accessibility for D.
P may choose any dialogical label that has been introduced by O of rank +1 relative to the label of the context he is playing in. If and only if there is no such context available, P may introduce a context of rank +1 relative to the context he is playing in.

Actually, the only if part of the condition in SR-7D is redundant, for it is P's strategical interest to try to stay in the contexts given by O because of the formal restriction (SR-5). This restriction ensures that every move in the dialogues with the (SR-7D) rule strictly corresponds to what can be assumed about a serial model.

3.1.1. Hybrid dialogues

Blackburn (2001) presents a natural way of bringing together hybrid modal logics and dialogues. The hybridization of a modal language amounts to extending its expressive power in such a way that it becomes possible to refer in the object language to a particular state of the model (see e.g., Blackburn 2000). One of the salient virtues of hybrid languages is their ability to express straightforwardly a wide range of frame conditions with object-language formulas. Investigators of dialogical proof systems welcomed the suggested techniques, which proved particularly useful in the context of temporal dialogues (Rahman, Gorisse & Damien 2004) or non-normal modal dialogics (Rahman 2002). Hybridization made it possible to devise a special kind of abductive dialogue where the Proponent searches for the minimal frame conditions to yield a winning strategy for a given formula (Keiff 2004).

3.2 Linear logic

See the entry on Linear Logic for a general overview of the field. Linear game semantics were introduced by Blass (1992), then further developed by various people including Abramsky, Jagadesan, Hyland, Girard himself (the founder of linear logic) and Japardize. Lorenz/Lorenzen-style dialogues were introduced in Rahman (2002).

Following the inventor of linear logic, one could say that the fundamental intuition at the root of the field is the following: the subject matter of logic is interaction, or rather the “well hidden geometrical structure” of it (see Girard 1999). This notion is declined in two principal ideas (see e.g., Blass 1998): the conception of negation as a role switch and of the occurrence of a formula in a proof as a (bounded) resource. As first shown in Blass (1992), game semantics is a natural setting for these ideas.

Linear negation is the same as dialogical negation: it consists of a role switch between the players.

Localization of formulas: the conceptual framework of linear logic is akin to the Brouwer-Heyting-Kolmogorov approach of a semantics of proofs. To this conception of proofs as objects, linear logic adds the computation-driven intuition that each occurrence of the same formula in a proof must be taken as a distinct resource for the inference process. The basic idea stems from the consideration that the occurrence of a formula in a proof is located somewhere, and that one should take seriously the differences in location. Hence the linear logical consequence relation is resource-sensitive. Weakening, expansion and contraction rules are rejected, for they say respectively that a redundant premise can be added in a derivation, that a given premise can always be used twice, and that two distinct tokens of the same premise type can be considered the same. In a sequent Σ ⊢ A, Σ denotes a multiset of formulas (i.e., a set together with a function giving for each member of the set the number of its occurences in the set, to the effect that {A} and {A, A} denote the same set, but different multisets).

In the dialogical framework, each move is an action. It is therefore very natural to consider that two distinct moves are different actions, consuming different resources, even when the two moves have the same propositional content. More precisely,

•  An atomic O-formula has been used iff this formula is the propositional content of a P-move. Atomic P-formulas are used by the very move in which they appear.

•  A complex formula A has been used iff all the possible aggressive and defensive moves related to A have been stated.

This general definition will be made more precise when we state the particle rules for linear connectives. In order to keep track of the use of formulas in the course of the dialogue, one may use a bracketing device: once a formula has been used, its propositional content is bracketed. This allows us to formulate a notion of linear validity:

Linear validity: A formula A is linearly valid iff there is a closed dialogue for P-!-A such that the propositional content of any move has been used (and therefore is bracketed).

Linear particles offer a very fine-grained perception of the way pieces of information are combined in a proof (which is one of the main points of Substructural Logic). Let us take an example: the two multiplicative particles. We will follow the notation used in Blass (1992). Multiplicative conjunction, (⊗), known as tensor, has the following Gentzen-style particle rules:

Γ ⊢ A     Δ ⊢ B
Γ, Δ ⊢ A⊗B
Γ, A, B, Δ ⊢ C
Γ, A⊗B, Δ ⊢ C

All the information contained in the premises is conserved in the conclusion, and nothing else is added (except the relevant particle). Compare with the following rules for multiplicative disjunction (⅋), known as par:

Γ ⊢ Δ, A, B, Λ
Γ ⊢ Δ, A ⅋ B, Λ
Γ, A ⊢ Δ     B, Λ ⊢ Π
Γ, A ⅋ B, Λ ⊢ Δ, Π

The meanings of the two multiplicative particles are obviously dual to each other. Both pieces of information A and B are present in the premises. The main difference lies in the geometry of the proof: the introduction of tensor on the right of a sequent needs two premises, while par needs two premises when introduced on the left. Now from the dialogical point of view, these rules have to be read analytically, i.e., bottom up, and a two-premises rule means a splitting in the corresponding dialogue. Such splittings are captured by a notion of context. Linear dialogues are contextual in a sense akin to modal dialogues. In other terms, the flow of information within the proof is constrained by an explicit structure of contexts, ordered by a relation of subordination. As in the modal case, the introduction of a new context will always be a consequence of the Opponent's choices. The Proponent will stay in the same context as long as he can.

A sequent Γ ⊢ A is the statement that from assumptions Γ, one could infer conclusion A. From the dialogical point of view, assumptions are the Opponent's concessions, while conclusions are the Proponent's claims. Thus, the rules above indicate that splitting for tensor occurs when it is asserted by the Proponent, so the dialogical particle rule will let the challenger choose the context where the dialogue will proceed. Dually, par will generate a splitting when asserted by the Opponent, thus the particle rule will let the defender choose the context.

Now, the splitting between contexts can have a slightly different dialogical meaning. Consider the three rules for additive conjunction (∧):

Γ ⊢ A     Γ ⊢ B
Γ ⊢ A ∧ B
Γ, A, Δ ⊢ C
Γ, A ∧ B, Δ ⊢ C
Γ, B, Δ ⊢ C
Γ, A ∧ B, Δ ⊢ C

As in the case of multiplicative conjunction, the challenger will choose the context, but here the assumptions contained in the context are the same. To understand the difference, notice that there are two rules of left-introduction. Dialogically, this means that when the Opponent has asserted A∧B, there are two distinct games available to the Proponent (one where the Opponent will defend A and one where he will defend B). In the same way, the two premises of the rule of right-introduction correspond to two distinct games. They are jointly mentioned in the same rule since the choice between them lies with the challenger, which happens to be the Opponent, so the validity of the conclusion, i.e., a winning strategy for the Proponent, must include a winning strategy in both games.

The occasions where a choice of context is needed will be determined by the particle rules, but a structural rule is needed first in order to regulate the opening of contexts in a dialogue.

SR-11: Linear Contexts Rule.
Only O may open new dialogical contexts. P may choose for his moves between dialogical contexts that have already been opened.

Now, the previous notions immediately call for a rephrasing of the formal rule SR-5:

SR-12: Formal Use of Linear Atoms.
O may assert atomic formulas whenever he needs to (but according to the particle rules and the other structural rules). P may assert an atomic formula a in a dialogical context ν iff O has asserted a in the dialogical context μ before, ν is a subcontext of μ, and a has not been used up yet (i.e., does not occur between square brackets).

For the sake of brevity, we will concentrate on the multiplicative fragment of linear logic, i.e., which connectives are tensor (⊗), par (⅋), linear implication (⊸), and negation (¬).

Particle rules for the multiplicative connectives are defined with respect to states of the linear game, which are tuples of the form: S=⟨ρ, σ, Φ, λ⟩, where ρ and σ are as usual, Φ is a linear formula, and λ is an assignment of dialogical contexts to formulas.

Concerning tensor, the challenger will choose the conjunct to be defended and the context where it should be defended.

Particle rule for tensor:
Let S1 = ⟨ρ, σ, ρ−1(!)-A⊗B, λφ/ν⟩, where λφ/ν assigns context ν to the formula ρ−1(!)-A⊗B. Both S2 and S3 are accessible from S1:

S2 = ⟨ρ, σ, ρ−1(!)-A, λA/μ⟩

where λA/μ denotes the result of extending λ by assigning context μ to the formula A. S2 is reached after an attack ρ−1(?)-R/μ, where μ is a dialogical subcontext of ν chosen by ρ−1(?).

S3 = ⟨ρ, σ, ρ−1(!)-B, λB/π⟩

where λB/π denotes the result of extending λ by assigning context π to the formula B. S2 is reached after an attack ρ−1(?)-L/π, where π is a dialogical subcontext of ν chosen by ρ−1(?).

The bracketing device will be as follows: the expression A⊗B is considered used and is bracketed iff both states S2 and S3 have been reached.

With par, the defender will choose the disjunct to be defended and the context where it should be defended. He will nevertheless have to defend both disjuncts. Here lies one of the main points that make dialogical semantics essential to linear logic. The multiplicative disjunction has “conjunctive features”, as Girard (1999) puts it: a proof of A⅋B involves a proof of A and a proof of B. Now the main difference between conjunction and disjunction in a dialogue is the player (ρ−1(!) or ρ−1(?)) who chooses how the game will proceed. What makes par a disjunction is thus the fact that it is the defender who has the choice of the order in which the proofs are given and the context where they will be given. These considerations lead to the following particle rule for par:

Particle rule for par.
Let S1 = ⟨ρ, σ, ρ−1(!)-A⅋B, λφ/ν⟩, where λφ/ν assigns context ν to the formula ρ−1(!)-A⅋B. Both S2 and S3 are accessible from S1, according to the choice of ρ−1(!):

S2 = ⟨ρ, σ, ρ−1(!)-A, λA/μ⟩

where λA/μ denotes the result of extending λ by assigning context μ to the formula A. S2 is reached after an attack ρ−1(?)-⅋. μ is a dialogical subcontext of ν chosen by ρ−1(!).

S3 = ⟨ρ, σ, ρ−1(!)-B, λB/π⟩

where λB/π denotes the result of extending λ by assigning context π to the formula B. S2 is reached after an attack ρ−1(?)-L/π, where π is a dialogical subcontext of ν chosen by ρ−1(!).

The expression A⅋B is considered used and is bracketed iff both states S2 and S3 have been reached.

As already noted, linear negation is essentially the usual dialogical negation, i.e., a role switch, that we noted using a priming on ρ. There is no contextual change.

Particle rule for linear negation.
Let S1 = ⟨ρ, σ, ρ−1(!)-¬A, λφ/ν⟩, where λφ/ν assigns context ν to the formula ρ−1(!)-¬A. S2 is accessible from S1 iff:

S2 = ⟨ρ′, σ, ρ′−1(!)-A, λA/ν⟩

The expression ¬A is considered used and is bracketed iff state S2 has been reached.

Linear implication is defined as ¬A⅋B, which makes it a multiplicative connective. If one insists on giving it a particle rule, then it will be as follows.

Particle rule for linear implication.
Let S1 = ⟨ρ, σ, ρ−1(!)-A⊸B, λφ/ν⟩, where λφ/ν assigns context ν to the formula ρ−1(!)-A⊸B. S2 is accessible from S1 iff:

S2 = ⟨ρ′, σ, ρ′−1(!)-A, λA/μ⟩

where λA/μ denotes the result of extending λ by assigning context μ to the formula A and μ is a dialogical subcontext of ν chosen by ρ−1(!). The game may then proceed, according to the choice of ρ−1(!), according to the relevant particle rule for the formula A, or to the following state of the game:

S3 = ⟨ρ, σ, ρ−1(!)-B, λB/π⟩

where λB/π denotes the result of extending λ by assigning context π to the formula B, where π is a dialogical subcontext of ν chosen by ρ−1(!).

The expression A⊸B is considered used and is bracketed iff both states S2 and S3 have been reached.

For a discussion of paraconsistent, free, and connexive logics, see the supplementary document Some Dialogical Systems for Non-Classical Logics.

4. Proof-Theoretical Aspects of Dialogues

One of the strengths of dialogues is the intuitivity of the strategy building when writing a proof. The freedom that players enjoy when choosing the next move may obscure the connection between the structural rules of dialogues and the structural rules of Gentzen-style sequent calculi (see Substructural logics). There is nevertheless a clear correspondence, that we will make explicit now for the main structural rules.

Exchange: (commutativity of premise combination) a player can attack any move of the other, and P can use O's concessions, regardless of the order of these moves. Dropping exchange forces players to follow the order of the moves as well as the order of subformulas in conjunctions (i.e., the challenger should attack a conjunction first with ?L and then with ?R). Furthermore, a concession by O is available for P iff P already used all the previous concessions. To see why such a restriction is needed, consider a dialogue for the formula (α→(β→γ))→(β→(α→γ), which is valid if, and only if, the logic features exchange.

A proof using exchange (move 6)
O P
(α→(β→γ))→(β→(α→γ)) 0
1 α→(β→γ) 0 β→ (α→γ) 2
3 β 2 α→γ 4
5 α 4 γ 10
7 β→γ 1 α 6
9 γ 7 β 8

Clearly, P has a winning strategy because he is allowed to use O's concessions in any order he pleases. Were he to follow the order of the concessions, no move would be available to him at 6, and the formula would not be valid.

Contraction: the contraction rule says that when two occurrences of a formula are present in a sequent, one of them can be eliminated. In the dialogues, proceeding from the conclusion down to its subformulas, contraction must be seen as corresponding to the possibility for the Proponent to use twice a formula conceded by the Opponent. Dropping it calls for a marking system in order to keep track of the concessions that have been used, as described in the linear dialogues.

A proof using contraction (moves 4 and 6)
O P
(α→(α→β))→(α→β) 0
1 (α→(α→β)) 0 (α→β) 2
3 α 2 β 8
5 (α→β) 1 α 4
7 β 5 α 6

Weakening: this structural rule allows the introduction of redundant premises, and has been one of the targets of Relevance Logic. In the dialogues, weakening corresponds to the fact that not all the concessions of the Opponent have to be actually used by the Proponent in the proof (i.e., either attacked or, in the case of an atom, used to defend against an attack). As explained in Section 3.2, dialogical systems without weakening should feature a syntactic way of marking the use of a premise.

A proof using weakening
O P
(α∧β)→α 0
1 ([α]2∧β) 0 α 4
3 [α]4 2 ?R 2

In this example, the concession of α in move 3 is used in move 4 (as shown by the brackets), but move 2 only uses half of the concession in move 1. The concession of β is redundant, P has a winning strategy only if the rules allow for weakening (i.e., there is no rule requiring all concessions to be used in order to win).

Expansion: in a sequent calculus where weakening is absent, expansion allows the addition of another occurrence of a formula whenever there is already one in a sequent. From a dialogical point of view, expansion amounts to considering that the use of one occurrence of a premise uses all the other occurrences.

5. From Proof to Models and Back (Dialogues and GTS)

Game-theoretical semantics (GTS) is a well-known approach to semantics for natural and formal languages, originating in the work of Jaakko Hintikka (see Hintikka & Sandu (1997) for a general presentation). The fact that GTS and dialogical logic are sisters has been widely acknowledged. The differences between the original approaches have been discussed too: while GTS relates to the study of truth in a model, dialogical logic explores the possibilities of a certain type of proof-theoretical approach to validity. Despite a close relationship between the two approaches, no thorough analysis of their interaction had been undertaken until Rahman & Tulenheimo 2006, with the exception of an excellent paper by Esa Saarinen (1978).

In Rahman & Tulenheimo 2006, this task is carried out systematically. More precisely, Rahman and Tulenheimo have worked out for classical propositional logic and classical first-order logic an exact connection between ‘intuitionistic dialogues with hypotheses’ and semantic games. Actually, it is not that surprising since the former can be thought of as implementing an intuitionistic proof theory supplemented with an axiom schema of the excluded middle.

The main result at the interface between dialogical logic and GTS is that the existence of a winning strategy for P in a dialogue D(A, H1, …, Hn) corresponding to a sentence A with a finite number of hypotheses Hi expressing those instances of the third excluded which are relevant to that sentence, gives rise to a family of Eloise’s winning strategies in semantic games G(A, M), one strategy for each model M; and, conversely, it is shown how to construct a winning strategy for Proponent in the dialogue D(A, H1, …, Hn) out of Eloise’s winning strategies in games G(A, M). A definition of the notion of ‘relevant instances of the excluded middle’ is given below, for propositional and first-order logic. In the latter case, a variant of the usual version is preferred. The proofs are constructive in the sense that it is explicitly shown how a strategy for one type of game is built using a strategy for the other type of game. One corollary of the paper is that each disjunct of the hypotheses of the dialogue at stake yields the dialogical version of truth in a model. Actually the central idea of the paper is based on the notion of material dialogues, which furnishes the dialogical version of the satisfiability of a formula relative to a model.

In fact, there are two rather straightforward approaches one can assume; they give rise to what are known as ‘alethic’ and ‘material’ dialogues (see e.g., Rahman & Keiff 2004). As dialogues are designed for dealing with validity, some additional ingredient must be introduced into dialogues in order to make them capable of dealing with material truth. Alethic dialogues are simply obtained by relativizing a dialogue to a model. Hence a part of the specification of an alethic dialogue in the case of propositional logic will be a valuation function, and in the case of first-order logic a τ-structure for an appropriate vocabulary τ.

By contrast, the idea behind material dialogues is to avoid having an extra component to dialogues (such as a specification of a model); they are meant to do with the resources of dialogues proper (which are designed for dealing with validity), and the idea is to ‘approximate’ characterization of truth by adding a sufficient amount of additional hypotheses − taken to be initial concessions of Opponent − which would serve to specify a model by using the resources of the object language only.

What is a sufficient amount, then? In the case of propositional logic, when discussing the truth of a formula A, any relevant model can be specified in terms of propositional formulas, namely literals (positive or negative atomic formulas). Moreover, it suffices to specify a finite number of such literals. The relevant models are identified by going through all propositional atoms pi appearing in A (there are only finitely many of these atoms) and choosing, for all i, either pi or its negation ¬pi. Those are the instances of the excluded middle relevant to the material truth of the formula at stake in the propositional case. In this way any relevant model—any truth-value distribution—can be specified.

For first-order logic, this approach has the obvious downside that in general there is no way of capturing a τ-structure in terms of a finite number of first-order sentences. Take for example a {P}-structure M with an infinite domain M = {di : i < ω}, where P is unary. To exhaustively describe M in terms of first-order sentences, we need an infinite list ⟨li : i < ω⟩ of literals, where li := Pci, if di ∈ PM, and li := ¬Pci, if di ∉ >PM. (By stipulation, the constant ci stands for the element di.)

Mathematically there is of course nothing problematic about such infinite lists of hypotheses. But one desideratum in designing dialogues typically is that it should be possible to think of them as humanly manageable, ideally temporal processes. Such a process cannot really begin by going through an infinity of hypotheses. This is why material dialogues with an infinity of hypotheses should be considered unsatisfactory. So what can we do? A solution to this dilemma, found by Tero Tulenheimo, has been developed in Rahman & Tulenheimo (2005): given a vocabulary of one unary relation symbol P, a relevant piece of finite information that the models of classical first-order logic must satisfy, is expressed by this sentence:

∀x(Px∨¬Px).

That is, whatever the value c of x, the instance Pc ∨ ¬Pc of tertium non datur must hold. What type of question concerning the sentence ∀x(Px ∨ ¬Px) should we ask in order for the answer to identify a (possibly infinite) model? Clearly, we should ask Opponent to choose a Skolem function for this sentence. No finite amount of questions of the type ?-∀ x/c will reveal this information, if there are infinitely many values for x available. On the other hand, a Skolem function

f : {c0, c1, …} → {left, right}

expressly says, for each possible value ci of x, which of the disjuncts Opponent considers as being satisfied by ci. This is exactly what it means to specify a model of vocabulary {P} with the domain {c0, c1, …}.

Now for a finite vocabulary τ, the finite information we use for specifying a model will be extracted from the sentences

∀x1…∀xn(Rx1, …, xn ∨ ¬Rx1, …, xn),

one for each R ∈ τ of arity n. We introduce a new mode of question, which enables one to ask about a Skolem function for an operator. xhere denotes a finite sequence of variables x1, …, xn, and ∀xstands for ∀x1…∀xn. When asked about a sentence of the form ∀x(Rx ∨ ¬Rx), the question

??-∨

must be answered by providing a second-order object, namely a Skolem function

f : {ci : i < ω} → {left, right}

for the unique token of the disjunction ∨ appearing in ∀x(Rx ∨ ¬Rx). (The double ‘?’ indicates that the answer should be a second-order object.) If O asserts that f is such a function, P is able to read the interpretation of the relation symbol R from the function f. P can draw all kinds of inferences from it, for instance check whether the relation symbol is satisfied by at least one tuple, by checking whether left ∈ Im(f) or not.

The way in which we extract a model from the sentences ∀x(Rx ∨ ¬Rx) is by taking them as initial concessions of O, and asking the question of ??-∨ with respect to each sentence. The questions ??-∨ give rise to the following new structural rule:

SR-15: Skolem Function Rule.
If O has conceded that f is a Skolem function for ∨ in

∀x(Rx ∨ ¬Rx),

then O must also, if asked, concede all instances of this second-order concession. That is, for any tuple c interpreting the variables x, he must concede Rc, if f(c) = left, and ¬Rc, if f(c) = right. Accordingly, after O has replied using some f to a question ??-∨, P is always entitled to pose the question

?-f/c

for any tuple c, asking O to confirm that indeed he concedes that the tuple c satisfies the disjunct f(c). O has no real choice for his answer: the reply is fully predetermined by his choice of f and the requirement that O must be coherent in his replies.

Further investigations on the phenomena of imperfect information in dialogues can be found in Rahman & Dégremont (2006).

Bibliography

Other Internet Resources

Related Entries

logic: and games | logic: connexive | logic: free | logic: independence friendly | logic: linear | logic: modal | logic: paraconsistent | logic: substructural