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 gametheoretic 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 twoplayer 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.
Table of Contents
 Introduction
 Argumentation Forms and the Meaning of Logical Constants
 Dialogues for Intuitionistic Logic
 Winning Strategies and Validity
 Dialogues for Classical Logic
 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 socalled 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 “
implies
”, then the other player can attack this assertion by claiming
, which can in turn be defended by the first player by claiming
. This reflects how logical constants are understood in everyday argumentation: someone arguing for “
implies
” has to be able to argue for
when being granted that
.
(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 firstorder language. The firstorder language consists of formulas
, which are constructed from atomic formulas
with the logical constants
(conjunction; “and”),
(disjunction; “or”),
(implication; “implies”),
(negation; “not”),
(universal quantifier; “every”) and
(existential quantifier; “there is”), together with terms
, which can be variables
, and auxiliary signs “
”, “
” and “
”. The atomic formulas can be relation symbols of arbitrary arity taking terms as arguments. An example for a firstorder formula is
.
This language is extended by using
,
,
,
(for terms
) and
as special symbols (that contain a preceding question mark). In addition, the signatures
and
stand for the two players proponent and opponent, respectively. An expression
is either a formula or a special symbol. For each expression
there is a
signed expression
and an
signed expression
. These signed expressions are called moves in general. Examples for moves are
and
.
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).
and
, where
, are used as variables for
and
.
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
can be attacked by
, and how this attack can be defended by
(if possible):
The argumentation form for
says that an assertion of the form
made by player
can be attacked by the other player
by choosing one of the two conjuncts
and
. This is expressed by
stating the special symbol
or
, respectively. This attack can then be defended by player
by asserting the conjunct
or the conjunct
according to the choice of
. A concrete instance of this argumentation form is the following:
Here the proponent
has asserted the conjunction
. This is attacked by the opponent
choosing the second conjunct
, indicated by stating the special symbol
. The proponent defends against this attack by asserting the second conjunct
. Informally, someone claiming “
and
” has to be able to argue for
and for
; an opponent can thus ask for any of the two.
For disjunctions of the form
asserted by player
, the attack by the other player
is indicated by the special symbol
. The defending player
chooses one of the two disjuncts
and
. Informally, someone claiming “
or
” has only to be able to argue for one of the two disjuncts, and can therefore choose to argue for
or for
, if the claimed disjunction is questioned.
In the case of implications
asserted by player
, the attacking player
asserts the antecedent
of the implication, and the defending player
asserts the consequent
. Informally, someone claiming “
implies
” has to be able to argue for
whenever
is given as an assumption.
Negated assertions
made by player
can only be attacked, namely by the other player
asserting
. There is no defense against such an attack. Informally, when claiming that “
is not the case”, one has to be able to argue against
.
The argumentation form for the universal quantifier
says that an assertion of the form
made by player
can be attacked by player
by choosing a term
in the symbolic attack
. Player
can then defend by asserting the formula
, where the term
chosen by
is substituted for (all occurrences of) the variable
in the formula
, also written
. Informally, someone claiming that “every object has the property
” has to be able to show for any object that it has the property
. An opponent can thus ask for any object (denoted by the term
, for example) whether it has the property
. This has then to be answered by an argument for
.
For existential assertions of the form
made by player
, the attack by the other player
is indicated by the special symbol
. The defending player
chooses a term
and asserts the formula
, that is, the formula resulting from substituting
for (all occurrences of)
in
. Informally, someone claiming that “there exists an object with property
” has only to be able to present one object (denoted by the term
, for example) with the property
, and can thus choose to argue for
, 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
and opponent
. 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
is given by saying that assertions of the form
have the truth value “true” if both conjuncts
and
have the truth value “true”; otherwise the truth value of
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
is explained by saying that an assertion of the form
has a proof if and only if both
and
have a proof. An implication
has a proof if and only if one is in possession of a construction that transforms any proof of the antecedent
into a proof of the consequent
. The classical principle of tertium non datur (
) is rejected in intuitionistic logic, and other classical principles such as double negation elimination (
) do not hold. The set of intuitionistic theorems is a subset of the set of classical theorems. In particular,
is not equivalent to
in intuitionistic logic, whereas it is in classical logic. In intuitionistic logic, implication (
) is a genuine logical constant; it cannot be expressed by using other logical constants such as negation (
) and disjunction (
).
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
with the assertion of a nonatomic formula, and proponent
and opponent
alternate moves as determined by the argumentation forms.

may assert an atomic formula only if it has been asserted by
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 forare always open, since there is no defense against them.)
 An attack may be defended at most once.
 A
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
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
signed formula. If this formula is again asserted by
, 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
and
. In particular, the moves
and
do not amount to the same because of condition 1. The argumentation forms, on the other hand, are completely symmetric with respect to
and
, that is, the argumentation forms are playerindependent.
The proponent wins a dialogue for a formula
if the dialogue is finite, begins with the move
and ends with a move of
such that
cannot make another move, that is, every move that
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
.
The following is a dialogue for the formula
:
The dialogue starts with the assertion of the formula
by the proponent
in the initial move at position 0. This initial move is attacked by the opponent
at position 1 with the assertion of the antecedent
of the implication asserted by
at position 0. The attack is thus made according to the argumentation form for
. In the next move at position 2, the proponent defends against this attack according to the argumentation form for
by asserting the consequent
of the attacked implication
. The implication
is attacked by
at position 3 by asserting its antecedent
. This attack is defended by
at position 4 by asserting
, the consequent of
. Here
is allowed to assert the atomic formula
, since
has asserted
before (compare condition 1). These last moves are also made according to the argumentation form for
. The opponent cannot make another move, since atomic formulas cannot be attacked (there are only argumentation forms for nonatomic assertions), and
cannot repeat attacks due to condition 4. The dialogue is thus won by
.
The following is a dialogue for the formula
:
The initial move is attacked by
with the symbolic attack
according to the argumentation form for
. This attack can be defended by
either by asserting the left disjunct
or by asserting the right disjunct
. Here, the proponent chooses the former in the defense move at position 2. This is attacked by
with the assertion of
according to the argumentation form for
. The dialogue is not won by
, and
cannot make another move: the atomic formula
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
again.
Another dialogue for the same formula
is obtained if
defends against the attack
by choosing to assert the right disjunct
instead of the left disjunct at position 2:
At position 3, the opponent attacks
by asserting its antecedent
, which
defends against at position 4 with the assertion of the consequent
. This dialogue is finite and ends with a move of
such that
cannot make another move, that is, this dialogue is won by
.
These two dialogues for the formula
show that for a valid formula there can be dialogues which are won by
as well as dialogues which are not won by
, although every possible move has been made. There are also invalid formulas for which this is the case. An example is
. If
attacks this formula with
, then
wins the dialogue: the defense
is attacked with
, which
defends against with
as final move. If, however,
attacks with
, then
cannot make another move, since the first conjunct
, which is an atomic formula, cannot be asserted because of condition 1.
A dialogue for the firstorder formula
is the following:
Instead of defending against
‘s attack (made at position 1) with
at position 2, the proponent attacks
‘s assertion of
by asserting
, according to the argumentation form for
. At position 3, the opponent attacks according to the argumentation form for
by choosing the term
in the symbolic attack
, which
defends against by asserting
at position 4. The opponent attacks this according to the argumentation form for
with
in the last move. Note that there are now two open attacks made by
: 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
of
‘s attack made at position 1, and according to the argumentation form for
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
is repeated endlessly; the opponent may choose a different term
in each repetition. Note that repeated attacks on the same move are prohibited only for
, while for
there is no such restriction. Hence
can repeatedly attack the move
(made at position 1) with the move
, starting the loop. Furthermore, each occurrence of an attack is defended at most once, and each occurrence of a
signed formula is attacked at most once, in accordance with conditions 3 and 4, respectively. This dialogue for the formula
is therefore neither won by
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
as well as dialogues that are won by
, 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 gametheoretic 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
has a winning strategy if for every move made by the other player
player
can make another move, such that each resulting play of the game (that is, each resulting dialogue) is eventually won by
. In dialogical logic one is usually only interested in winning strategies for the proponent
. A winning proponent strategy for a formula
is a tree
whose branches are dialogues for
won by
, where the nodes are the moves, such that

has the move
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
at this position.
b. Examples
The following dialogue, which has been discussed above, is already a winning proponent strategy for the formula
:
This winning proponent strategy has only one branch, which is the dialogue shown. The root node
has only one successor, since the move
is the only possible move for
. This node at depth 1 has exactly one successor node, namely the move
at depth 2. This in turn has again only one successor node, namely the move
at depth 3, since no other opponent moves are possible. Its one successor node is
, which has no successor as there are no possible opponent moves. The dialogue is won by
, and all possible opponent moves have been taken into account. This single branch tree is thus a winning proponent strategy for the formula
.
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
:
This tree of signed expressions has two branches. After the move
at depth 4 there are two possible moves for
, yielding the two successor nodes
(left branch) and
(right branch). The proponent wins both resulting dialogues:
can neither make another move after
(left dialogue) nor after
(right dialogue). Thus, this tree is a winning proponent strategy.
c. FirstOrder Winning Strategies
Winning strategies for quantifierfree formulas are always finite trees, whereas winning strategies for firstorder formulas can in general be trees of countably infinitely many finite branches. An example is the following winning proponent strategy for the firstorder formula
:
The move
at depth 2 has countably infinitely many successor nodes, since for each choice of a term
(for natural numbers
) the symbolic attack
is a possible move. For pairwise distinct terms
the tree therefore has infinitely many branches (indicated by “
”), where each branch is a dialogue won by
.
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
on the move
is a possible move, where
is a new variable in this branch, then
is the only immediate successor node that is an attack on
.
 If the depth of a node is even,
is an attack on an assertion
, and the move
is a possible defense against this attack, where
is a new variable in this branch, then
is the only immediate successor node that is a defense against
.
There may be further possible moves, which are not attacks on
or defenses against
. 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:
The restrictions (i) and (ii) have the effect that in winning strategies only one of the possible attacks
(for each term
) on
or defenses
(for each term
) against
has to be taken into account, namely one where the term
is a new variable, whereas in winning strategies which are not thus restricted one has to consider the corresponding moves for each term
, 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 playerindependent argumentation forms for
and
by the following playerdependent argumentation forms:
The argumentation forms
and
contain the condition that the variable
is new. They are thus historydependent in the sense that the possibility of a move
or
in a dialogue depends on whether the variable
has already occurred in this dialogue. The playerindependent argumentation forms for
and
, on the other hand, are not historydependent.
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
according to the argumentation form
is a possible opponent move,
 the symbolic attack
according to the argumentation form
is a possible opponent move,
 or the opponent move defending a symbolic attack
according to the argumentation form
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 playerdependent argumentation forms has therefore technical advantages. However, from a conceptual point of view, playerindependent argumentation forms might be preferable.
d. Tertium Non Datur and the Principle of NonContradiction
The proponent does not have a winning strategy for every formula. An example is the instance
of tertium non datur. There is only one possible dialogue, namely
which is not won by
. At position 2, the proponent can only defend against
‘s symbolic attack
by choosing to assert the right disjunct
. Choosing the left disjunct is not an option due to condition 1. Due to condition 4, the opponent cannot repeat the symbolic attack
at position 3; the only possible move for
is to attack
with
. This attack can neither be defended nor can it be attacked, and another defense against the already defended symbolic attack
is ruled out by condition 3.
On the other hand, there is a winning proponent strategy for each instance of the principle of noncontradiction,
. Consider the following winning proponent strategy for
:
Here it is essential that
can attack the same assertion repeatedly. The opponent’s assertion of
at position 1 is attacked by
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
cannot defend against the attack on
repeatedly, while in the case of the principle of noncontradiction there is a winning proponent strategy because
can attack
repeatedly. In classical logic, tertium non datur and the principle of noncontradiction are equivalent, while in intuitionistic logic only the principle of noncontradiction holds. For the dialogues considered, this distinction rests upon the fact that
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
is called valid if there is a winning proponent strategy for
.
That this dialogical notion of validity corresponds exactly to intuitionistic provability is the content of the following completeness result:
A formula
is valid if and only if
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
is provable in intuitionistic logic, then each substitution instance
, obtained by uniformly substituting formulas for atomic formulas in
, 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
, then there are winning proponent strategies for each instance
of
that is the result of a uniform substitution of formulas for atomic formulas in
.
f. Winning Strategies as Proofs
Dialogues can also be viewed as constituents of a proof system. On this view, the proofs of a formula
are the winning proponent strategies for
. 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
if and only if
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
into a proof of
in sequent calculus for intuitionistic logic, and, the other way round, transforming any proof of
into a winning proponent strategy for
.
5. Dialogues for Classical Logic
A dialogical rendering of classical logic is obtained by relaxing conditions 2 and 3 for the proponent
, while keeping them for the opponent
. That is, conditions 2 and 3 are replaced by the following conditions:
2′. If there is more than one open attack by
, then only the last one may be defended by
.
may be defended by
at most once.
For
this means that if there is more than one open attack made by
, then
may defend against any of these attacks (instead of only the last one), and
can defend against attacks made by
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
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
. It consists in the following classical dialogue:
At position 2, the proponent can defend against
‘s symbolic attack
only by asserting the right disjunct
, since the atomic left disjunct
has not been asserted by
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
, which has been asserted by
at the preceding position 3.
There is a classical winning proponent strategy for the formula
, an instance of the intuitionistically invalid principle of double negation elimination. It consists in the following classical dialogue:
The last move is possible due to the replacement of condition 2 by condition 2′. At position 3 there are two open attacks by
(made at positions 1 and 3, respectively). Condition 2 would prohibit
‘s defense against the first attack, since this is not the last open attack. But condition 2′ enables
to defend against any earlier open attack. At position 4, the proponent can thus defend against
‘s first attack by asserting the consequent
of the attacked implication
.
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 nonclassical 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 SchroederHeister [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 gametheoretic 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 nonclassical 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 NorthHolland, 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 dialoguedefiniteness.
 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 SchroederHeister. 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 implicationsasrules 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 CurryHoward 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 validityconcepts 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 BolzanoTarski approach.
Author Information
Thomas Piecha
Email: thomas.piecha@unituebingen.de
University of Tübingen
Germany