Dialogical Logic
Dialogical logic is an approach to logic in which the meaning of the logical constants (connectives and quantifiers) and the notion of validity are explained in game-theoretic terms. The meaning of each logical constant (such as “and”, “or”, “implies”, “not”, “every”, et ainsi de suite) is given in terms of how assertions containing these logical constants can be attacked and defended in an adversarial dialogue. Dialogues are described as two-player games between a proponent and an opponent. A dialogue starts with an assertion made by the proponent. This assertion can then be attacked according to its logical form by the opponent. Depending upon the kind of attack, the proponent can now either defend against, or attack, the opponent’s move. The two players alternate until one player is unable to make another move. Dans ce cas, 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, c'est, 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 des matières
Introduction
Argumentation Forms and the Meaning of Logical Constants
Dialogues for Intuitionistic Logic
Définition
Examples
Winning Strategies and Validity
Winning Strategies
Examples
First-Order Winning Strategies
Tertium Non Datur and the Principle of Non-Contradiction
Dialogical Validity and Completeness
Winning Strategies as Proofs
Dialogues for Classical Logic
Examples
Classical Dialogical Validity and Completeness
Origins and Recent Developments
Références et lectures complémentaires
1. Introduction
Dialogical logic comprises three main constituents:
(J’ai) Argumentation forms. The meaning of the logical constants (like “implies”, par exemple) is given by so-called argumentation forms. An argumentation form describes in terms of two possible kinds of moves, called attack and defense, how assertions containing a certain logical constant in main position can be attacked and defended. Par exemple, 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. De plus,, 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. C'est, 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, par exemple.
2. Argumentation Forms and the Meaning of Logical Constants
Argumentation forms are formulated for an extended first-order language. The first-order language consists of formulas , which are constructed from atomic formulas with the logical constants (conjunction; “and”), (disjunction; “or”), (implication; “implies”), (negation; “not”), (universal quantifier; “every”) et (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 first-order formula is
This language is extended by using , , , (for terms ) and as special symbols (that contain a preceding question mark). De plus,, the signatures and stand for the two players proponent and opponent, respectivement. 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
et
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). et , où , 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 , respectivement. 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 . Informellement, 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 . Informellement, 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 . Informellement, 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. Informellement, 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 . Informellement, 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 , par exemple) 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 , c'est, the formula resulting from substituting for (all occurrences of) dans . Informellement, someone claiming that “there exists an object with property ” has only to be able to present one object (denoted by the term , par exemple) 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. Par exemple, 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. Par exemple, 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. En particulier, 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.
À. Définition
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 non-atomic 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 for are 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. Donc, if an already defended attack is repeated, then condition 3 does not prohibit that this new occurrence of the attack can be defended once, aussi. 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 . En particulier, the moves and do not amount to the same because of condition 1. The argumentation forms, d'autre part, are completely symmetric with respect to and , c'est, the argumentation forms are player-independent.
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, c'est, 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 non-atomic 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 . Ici, 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, c'est, 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. Si, cependant, 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 first-order 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. En outre, 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, respectivement. This dialogue for the formula
is therefore neither won by nor does it end with an opponent move.
En résumé, 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, aussi. The notion of winning a dialogue is itself not sufficient for making a distinction concerning the validity of a formula.
4. Winning Strategies and Validity
In dialogical logic the central logical notion of validity is explained in terms of the game-theoretic notion of strategy. A strategy determines each move of a player. The crucial notion for validity is that of winning proponent strategy. Dialogical validity of a formula consists in the existence of a winning proponent strategy for that formula.
À. 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 (c'est, 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 (c'est, 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 (c'est, 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 .
En général, 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) et (right branch). The proponent wins both resulting dialogues: can neither make another move after (left dialogue) nor after (right dialogue). Ainsi, this tree is a winning proponent strategy.
c. First-Order Winning Strategies
Winning strategies for quantifier-free formulas are always finite trees, whereas winning strategies for first-order formulas can in general be trees of countably infinitely many finite branches. An example is the following winning proponent strategy for the first-order formula :
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. Toutefois, the number of these immediate successor nodes can only be finite, and there is thus no more infinite ramification within winning proponent strategies.
Par exemple, the infinite winning proponent strategy indicated above is reduced to the following finite winning proponent strategy:
The restrictions (J’ai) et (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 player-independent argumentation forms for and by the following player-dependent argumentation forms:
The argumentation forms and contain the condition that the variable is new. They are thus history-dependent 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 player-independent argumentation forms for and , d'autre part, are not history-dependent.
Winning proponent strategies for the resulting dialogues can then be restricted as follows: Only one successor node for a node at even depth has to be considered if
the symbolic attack 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.
Encore, further moves according to other argumentation forms may be possible. The resulting winning proponent strategies are finite. The use of the player-dependent argumentation forms has therefore technical advantages. Toutefois, from a conceptual point of view, player-independent argumentation forms might be preferable.
d. Tertium Non Datur and the Principle of Non-Contradiction
The proponent does not have a winning strategy for every formula. An example is the instance of tertium non datur. There is only one possible dialogue, à savoir:
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.
D'autre part, there is a winning proponent strategy for each instance of the principle of non-contradiction, . 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 non-contradiction there is a winning proponent strategy because can attack repeatedly. En logique classique, tertium non datur and the principle of non-contradiction are equivalent, while in intuitionistic logic only the principle of non-contradiction holds. For the dialogues considered, this distinction rests upon the fact that 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.
Donc, 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. C'est, 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, aussi. The completeness result implies that also validity is closed under uniform substitution. C'est, 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. Sur cette vue, 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, par exemple, 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, et, 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 . C'est, 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 .
3′. An attack 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.
À. 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, respectivement). 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′, respectivement, is necessary to obtain classical logic. Sinon, there would not be winning proponent strategies for (all instances of) either tertium non datur or the principle of double negation elimination, which are both principles of classical logic.
b. Classical Dialogical Validity and Completeness
The dialogical notion of classical validity is defined as follows:
A formula A is called classically valid if there is a classical winning
proponent strategy for A.
The following completeness theorem holds:
A formula A is classically valid if and only if A is provable in
classical logic.
A proof of this theorem for a sequent calculus for classical logic can be found in Sørensen and Urzyczyn [2006].
A dialogical formulation of classical logic has thus been obtained by a modification of the dialogue conditions for intuitionistic dialogues. This means that one can obtain dialogical formulations of different logics by changing the rules of the dialogue games.
6. Origins and Recent Developments
The dialogical approach to logic was first proposed by Lorenzen in 1958 (Lorenzen [1960]; see also Lorenzen [1961]) for intuitionistic logic as well as for classical logic. That the dialogical approach as such cannot be taken as a foundation of intuitionistic logic is obvious, since a dialogical notion of classical validity can be obtained by modifying the dialogue conditions given for intuitionistic logic. If one wants to obtain a dialogical foundation for intuitionistic logic, it is therefore necessary to give a justification for the special kind of dialogues needed for intuitionistic logic. Such a justification has been proposed by Felscher [2002] (first published in 1986); it is based on the notions of contention, hypothesis and relevance.
The dialogical approach has been extended to several non-classical logics, including modal logic and linear logic; for an overview see Rahman and Keiff [2005] and Keiff [2011]. A dialogical setting for the interpretation of implications as rules has been considered by Piecha and Schroeder-Heister [2012]. Dialogical logic can thus provide a common basis for discussing different kinds of logics.
7. Références et lectures complémentaires
Andreas Blass. A Game Semantics for Linear Logic. Annals of Pure and Applied Logic, 56:183–220, 1992.
Presents a dialogue semantics for linear logic. Starting point for game-theoretic developments in computer science.
Walter Felscher. Dialogues, Strategies, and Intuitionistic Provability. Annals of Pure and Applied Logic, 28:217–254, 1985.
Constructive completeness proof for intuitionistic logic.
Walter Felscher. Dialogues as a Foundation for Intuitionistic Logic. In D. M. Gabbay and F. Guenthner, editors, Manuel de logique philosophique, 2e édition, Volume 5, pages 115–145. Intelligent, 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. O. Krabbe. Dialogue Foundations. Aristotelian Society Supplementary Volume, 75:17–49, 2001.
Critical discussion between Hodges and Krabbe on dialogues as a foundation for logic.
Laurent Keiff. Dialogical Logic. In E. N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Stanford University, Summer 2011 edition, 2011.
Overview on dialogical logic, including dialogues for modal, linear and other non-classical logics. The presentation uses an alternative formalization of dialogical logic.
Erik C. O. Krabbe. Dialogue Logic. In D. M. Gabbay and J. Woods, editors, Handbook of the History of Logic, Volume 7: Logic and the Modalities in the Twentieth Century, pages 665–704. Elsevier North-Holland, Amsterdam, 2006.
Traces the historical development of dialogical logic. Contains a useful bibliography.
Kuno Lorenz. Basic Objectives of Dialogue Logic in Historical Perspective. In Rahman and H. Rückert, editors, New Perspectives in Dialogical Logic, volume 127 of Synthese, pages 255–263. Springer, Berlin, 2001.
Describes the development of dialogical logic in historical context, with emphasis on the notion of dialogue-definiteness.
Paul Lorenzen. Logik und Agon. In Atti del XII Congresso Internazionale di Filosofia (Venezia, 12–18 Settembre 1958), volume 4, pages 187–194. Sansoni Editore, Firenze, 1960.
First proposal of dialogues as a means to explain intuitionistic logic and classical logic.
Paul Lorenzen. Ein dialogisches Konstruktivitätskriterium. In Infinitistic Methods. Proceedings of the Symposium on Foundations of Mathematics (Warsaw, 2–9 September 1959), pages 193–200. Pergamon Press, Oxford/London/New York/Paris, 1961.
Dialogical explanation of the meaning of logical constants and of the meaning of inductive definitions.
Thomas Piecha and Peter Schroeder-Heister. Implications as Rules in Dialogical Semantics. In M. Peliš and V. Puncochár, editors, The Logica Yearbook 2011, pages 211–225. Publications du Collège, Londres, 2012.
Formulates dialogical semantics for implications-as-rules approach.
Shahid Rahman and Laurent Keiff. On How to Be a Dialogician. In D. Vanderveken, editor, Logic, Thought and Action, volume 2 of Logic, Epistemology, and the Unity of Science, pages 359–408. Springer, Dordrecht, 2005.
Survey of dialogical formulations of a variety of logics.
Morten Heine Sørensen and Paweł Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, New York, 2006.
Contains a completeness proof for classical dialogues.
Wolfgang Stegmüller. Remarks on the completeness of logical systems relative to the validity-concepts of P. Lorenzen and K. Lorenz. Notre Dame Journal of Formal Logic, 5:81–112, 1964.
Contains a comparison of the dialogical approach to semantics with the Bolzano-Tarski approach.
Informations sur l’auteur
Thomas Piecha
Messagerie: [email protected]
University of Tübingen
Allemagne
