Logique dialogique

La logique dialogique est une approche de la logique dans laquelle la signification des constantes logiques (connecteurs et quantificateurs) et la notion de validité sont expliquées en termes de théorie des jeux. La signification de chaque constante logique (comme « et », "ou", "implique", "pas", "chaque", et ainsi de suite) est donné en termes de la manière dont les assertions contenant ces constantes logiques peuvent être attaquées et défendues dans un dialogue contradictoire. Les dialogues sont décrits comme des jeux à deux entre un partisan et un adversaire.. Un dialogue commence par une affirmation faite par le promoteur. Cette affirmation peut alors être attaquée selon sa forme logique par l'opposant. Selon le type d'attaque, le promoteur peut désormais soit se défendre contre, ou attaquer, le coup de l'adversaire. Les deux joueurs alternent jusqu'à ce qu'un joueur ne puisse plus effectuer un autre mouvement.. Dans ce cas, le dialogue est gagné par l'autre joueur qui a fait le dernier coup. Une affirmation faite lors du déménagement initial par le promoteur est considérée comme valide., si le promoteur a une stratégie gagnante pour cela, c'est, si le promoteur peut gagner chaque dialogue pour chaque mouvement possible effectué par l'adversaire. L'approche dialogique a été initialement élaborée pour la logique intuitionniste et pour la logique classique; il a été étendu à d'autres logiques, parmi eux la logique modale et la logique linéaire.

Table des matières
Introduction
Formes d'argumentation et signification des constantes logiques
Dialogues pour la logique intuitionniste
Définition
Exemples
Stratégies gagnantes et validité
Stratégies gagnantes
Exemples
Stratégies gagnantes de premier ordre
Le tiers n’est pas donné et le principe de non-contradiction
Validité dialogique et exhaustivité
Des stratégies gagnantes comme preuves
Dialogues pour la logique classique
Exemples
Validité et exhaustivité dialogiques classiques
Origines et développements récents
Références et lectures complémentaires
1. Introduction

La logique dialogique comprend trois éléments principaux:

(J’ai) Formulaires d'argumentation. La signification des constantes logiques (comme "implique", par exemple) est donné par les formes dites d'argumentation. Une forme d'argumentation décrit en termes de deux types de mouvements possibles, appelé attaque et défense, comment les assertions contenant une certaine constante logique en position principale peuvent être attaquées et défendues. Par exemple, la forme d'argumentation pour « implique » dit que si un joueur affirme « implique », alors l'autre joueur peut attaquer cette affirmation en réclamant , qui peut à son tour être défendu par le premier joueur en réclamant . Cela reflète la façon dont les constantes logiques sont comprises dans l'argumentation quotidienne: quelqu'un qui plaide pour « implique » doit être capable de plaider pour que l'on lui accorde que .

(Ii) Dialogues. Un dialogue est un jeu unique joué par deux joueurs, appelés promoteur et opposant. Le promoteur agit d'abord en faisant une affirmation. Ensuite, les joueurs alternent leurs mouvements. Chaque mouvement doit être effectué selon une forme d'argumentation. De plus,, certaines règles ou conditions sont imposées, qui vont au-delà de ce qui a été prévu dans les formes argumentatives. Un exemple d'une telle règle est qu'une défense contre une certaine attaque ne peut pas être répétée.. Il existe des règles qui s'appliquent aux deux joueurs ainsi que des règles qui ne restreignent qu'un seul des deux joueurs.. Un exemple de ce dernier cas est la règle selon laquelle une déclaration ne contenant aucune constante logique ne peut être affirmée par le proposant qu'après avoir déjà été affirmée par l'opposant., que l'opposant peut faire valoir une telle déclaration à tout moment, si cela est permis par un formulaire d’argumentation et non interdit par d’autres conditions. Le promoteur gagne un dialogue si l'adversaire ne peut pas faire un autre mouvement.

(iii) Stratégies gagnantes. La notion de stratégie gagnante pour les jeux de dialogue fournit la notion dialogique de validité ou, selon le point de vue, de prouvabilité. En logique dialogique, une assertion est dite valide s'il existe une stratégie de promoteur gagnante pour elle. C'est, une affirmation est valable si son promoteur peut toujours gagner un dialogue pour elle, peu importe les mouvements effectués par l'adversaire. En fonction des conditions précisant le type de dialogues joués, il peut y avoir ou non une stratégie gagnante pour une assertion donnée. Cela signifie qu'en changeant les règles des jeux de dialogue on peut obtenir différentes notions de validité, comme la validité intuitionniste ou la validité classique, par exemple.

2. Formes d'argumentation et signification des constantes logiques

Les formes d'argumentation sont formulées pour un langage étendu du premier ordre. Le langage du premier ordre est constitué de formules , qui sont construits à partir de formules atomiques avec les constantes logiques (conjonction; "et"), (disjonction; "ou"), (implication; "implique"), (négation; "pas"), (quantificateur universel; "chaque") et (quantificateur existentiel; "il y a"), avec les termes , qui peuvent être des variables , et panneaux auxiliaires "", "" et "". Les formules atomiques peuvent être des symboles de relation d'arité arbitraire prenant des termes comme arguments. Un exemple de formule du premier ordre est

Ce langage est étendu en utilisant , , , (pour les termes ) et comme symboles spéciaux (qui contiennent un point d'interrogation précédent). De plus,, les signatures et représentent les deux joueurs partisan et adversaire, respectivement. Une expression est soit une formule, soit un symbole spécial. Pour chaque expression il y a une expression -signée et une expression -signée . Ces expressions signées sont appelées mouvements en général. Des exemples de mouvements sont

et

Une expression signée est appelée assertion si l'expression est une formule; on parle d'attaque symbolique si l'expression est un symbole spécial (il n'y a pas de défense symbolique). et , où , sont utilisés comme variables pour et .

Pour chaque constante logique, il existe une forme d'argumentation, qui détermine comment une formule, avec la constante logique respective comme constante principale, qui est affirmé par peut être attaqué par , et comment cette attaque peut être défendue par (si possible):

La forme d'argumentation pour dit qu'une affirmation de la forme faite par un joueur peut être attaquée par l'autre joueur en choisissant l'une des deux conjonctions et . Ceci est exprimé en indiquant le symbole spécial ou , respectivement. Cette attaque peut alors être défendue par le joueur en faisant valoir la conjonction ou la conjonction selon le choix de . Un exemple concret de cette forme d’argumentation est le suivant:

Ici, le promoteur a affirmé la conjonction . Ceci est attaqué par l'adversaire choisissant la deuxième conjonction , indiqué en indiquant le symbole spécial . Le promoteur se défend contre cette attaque en affirmant la deuxième conjonction . Informellement, quelqu'un qui prétend « et » doit être capable d'argumenter pour et pour ; un adversaire peut ainsi demander n'importe lequel des deux.

Pour les disjonctions de la forme affirmée par le joueur , l'attaque de l'autre joueur est indiquée par le symbole spécial . Le joueur défenseur choisit l'un des deux disjoints et . Informellement, quelqu'un qui prétend « ou » n'a qu'à pouvoir argumenter en faveur de l'une des deux disjonctions, et peut donc choisir de plaider pour ou pour , si la disjonction revendiquée est remise en question.

En cas d'implications affirmées par le joueur , le joueur attaquant affirme l'antécédent de l'implication, et le joueur défenseur affirme la conséquence . Informellement, quelqu'un qui prétend « implique » doit être capable d'argumenter chaque fois que cela est donné comme hypothèse.

Les assertions niées faites par le joueur ne peuvent être attaquées que, à savoir par l'autre joueur affirmant . Il n'y a aucune défense contre une telle attaque. Informellement, en affirmant que « ce n’est pas le cas », il faut pouvoir argumenter contre .

La forme d'argumentation du quantificateur universel dit qu'une affirmation de la forme faite par le joueur peut être attaquée par le joueur en choisissant un terme dans l'attaque symbolique. . Le joueur peut alors se défendre en affirmant la formule , où le terme choisi par est remplacé par (toutes les occurrences de) la variable dans la formule , également écrit . Informellement, quelqu'un qui prétend que « chaque objet a la propriété » doit être capable de démontrer pour tout objet qu'il a la propriété . Un adversaire peut ainsi demander n'importe quel objet (désigné par le terme , par exemple) s'il possède la propriété . Il faut alors répondre à cette question par un argument en faveur .

Pour les assertions existentielles de la forme faites par le joueur , l'attaque de l'autre joueur est indiquée par le symbole spécial . Le joueur défenseur choisit un terme et fait valoir la formule , c'est, la formule résultant de la substitution de (toutes les occurrences de) dans . Informellement, quelqu'un qui prétend qu '«il existe un objet doté d'une propriété» n'a qu'à pouvoir présenter un seul objet (désigné par le terme , par exemple) avec la propriété , et peut ainsi choisir de plaider en faveur , lorsque l'existence prétendue d'un tel objet est remise en question.

Les formes d'argumentation donnent ainsi une explication du sens des constantes logiques en disant comment les assertions, qui contiennent la constante logique respective en position principale, sont utilisés dans les argumentations entre les deux acteurs partisan et adversaire . Cette explication vise à comprendre comment les assertions sont utilisées selon leur forme logique dans les argumentations réelles..

Dans la littérature, les formes d'argumentation sont également appelées règles de particules ou règles logiques.

3. Dialogues pour la logique intuitionniste

La logique dialogique a d'abord été développée pour la logique intuitionniste et pour la logique classique.

La logique classique repose généralement sur le principe de bivalence. Chaque affirmation est vraie ou fausse, et la valeur de vérité d'une assertion composée est déterminée par les valeurs de vérité de ses constituants. Par exemple, la signification de la constante logique est donnée en disant que les assertions de la forme ont la valeur de vérité « vrai » si les deux sont conjointes et ont la valeur de vérité « vrai »; sinon la valeur de vérité de est « fausse ».

La logique intuitionniste n'est pas basée sur la bivalence. Au lieu d'employer des valeurs de vérité, la signification intuitionniste des constantes logiques est généralement expliquée en termes de preuves ou de transformations de preuves. Par exemple, le sens de s'explique en disant qu'une assertion de la forme a une preuve si et seulement si les deux ont une preuve. Une implication a une preuve si et seulement si l'on est en possession d'une construction qui transforme toute preuve de l'antécédent en preuve du conséquent. . Le principe classique du tiers n'est pas donné () est rejeté dans la logique intuitionniste, et d'autres principes classiques tels que l'élimination de la double négation () ne tiens pas. L'ensemble des théorèmes intuitionnistes est un sous-ensemble de l'ensemble des théorèmes classiques. En particulier, n'est pas équivalent à en logique intuitionniste, alors que c'est en logique classique. En logique intuitionniste, implication () est une véritable constante logique; il ne peut pas être exprimé en utilisant d'autres constantes logiques telles que la négation () et disjonction ().

Des formulations dialogiques peuvent être données à la fois pour la logique classique et la logique intuitionniste. La différence entre ces formulations est faite par des notions différentes de dialogue, spécifié par certaines conditions. Les dialogues pour la logique intuitionniste sont définis ensuite. Les dialogues pour la logique classique seront traités ci-dessous, dans la section 5. Les formes d'argumentation qui sous-tendent ces notions ne diffèrent pas; ils sont les mêmes pour les deux logiques.

À. Définition

Les dialogues pour la logique intuitionniste sont définis par rapport aux formes d'argumentation données comme étant des séquences de mouvements finies ou infinies satisfaisant les conditions de dialogue suivantes:

Le premier pas est fait par le promoteur avec l'affirmation d'une formule non atomique, et les mouvements alternés du partisan et de l'opposant, déterminés par les formes d'argumentation.
peut affirmer une formule atomique seulement si elle a été affirmée auparavant.
S'il y a plus d'une attaque ouverte, alors seul le dernier peut être défendu.
(Une attaque est ouverte si elle n'a pas encore été défendue. Les attaques menées selon la forme d'argumentation pour sont toujours ouvertes, puisqu'il n'y a aucune défense contre eux.)

Une attaque peut être défendue au maximum une fois.
Une formule signée peut être attaquée au maximum une fois.

Ces conditions sont également appelées règles structurelles ou règles-cadres dans la littérature.. Ils ne sont ici donnés que de manière informelle. La condition 3 fait référence à une occurrence d'attaque, et la condition 4 fait référence à une occurrence d'une formule -signée. Donc, si une attaque déjà défendue est répétée, alors la condition 3 n'interdit pas que cette nouvelle occurrence de l'attaque puisse être défendue une fois, aussi. Cela vaut également pour une formule -signée déjà attaquée. Si cette formule est à nouveau affirmée par , alors la condition 4 n'interdit pas que cette nouvelle occurrence puisse également être attaquée une fois.

On peut constater que partisan et opposant ne sont pas interchangeables.. Ceci est uniquement dû aux conditions 1 et 4, qui sont asymétriques pour et . En particulier, les mouvements et ne reviennent pas au même à cause de la condition 1. Les formes argumentatives, d'autre part, sont complètement symétriques par rapport à et , c'est, les formes d'argumentation sont indépendantes du joueur.

Le promoteur remporte un dialogue pour une formule si le dialogue est fini, commence par le mouvement et se termine par un mouvement tel qu'il ne peut pas faire un autre mouvement, c'est, chaque mouvement qui pourrait être effectué selon les formes d'argumentation viole au moins une des conditions 0 à 4.

b. Exemples

Les dialogues sont écrits avec des numéros de position à gauche et des commentaires à droite. Les commentaires précisent quel type de mouvement est effectué (attaque ou défense) et à quel coup précédent un coup se réfère. Dans cette notation, les mouvements ont le format

Ce qui suit est un dialogue pour la formule :

Le dialogue commence par l'affirmation de la formule par le promoteur lors du mouvement initial à la position 0.. Ce coup initial est attaqué par l'adversaire en position 1 avec l'affirmation de l'antécédent de l'implication affirmée par en position 0. L’attaque se fait donc selon la forme argumentative de . Au prochain coup en position 2, le promoteur se défend contre cette attaque selon la forme argumentative pour en affirmant la conséquence de l'implication attaquée . L'implication est attaquée par en position 3 en affirmant son antécédent . Cette attaque est défendue par en position 4 en affirmant , la conséquence de . Ici, il est permis d'affirmer la formule atomique , depuis, il a déjà affirmé (comparer la condition 1). Ces derniers mouvements sont également effectués selon la forme d'argumentation pour . L'adversaire ne peut pas faire un autre mouvement, puisque les formules atomiques ne peuvent pas être attaquées (il n'y a que des formes d'argumentation pour les assertions non atomiques), et ne peut pas répéter les attaques en raison de la condition 4. Le dialogue est ainsi gagné par .

Ce qui suit est un dialogue pour la formule :

Le coup initial est attaqué par l'attaque symbolique selon la forme argumentative de . Cette attaque peut être défendue soit en affirmant la disjonction de gauche, soit en affirmant la disjonction de droite. . Ici, le promoteur choisit le premier dans le mouvement de défense en position 2. Ceci est attaqué par l'affirmation selon laquelle selon la forme d'argumentation pour . Le dialogue n'est pas gagné par , et je ne peux pas faire un autre mouvement: la formule atomique ne peut pas être attaquée, il n'y a aucune défense contre les attaques sur les formules niées, et en raison de la condition 3, il n'est pas possible de se défendre à nouveau contre l'attaque.

Un autre dialogue pour la même formule est obtenu si on se défend contre l'attaque en choisissant d'affirmer la disjointe droite au lieu de la disjointe gauche en position 2:

Au poste 3, l'adversaire attaque en faisant valoir son antécédent , qui se défend en position 4 avec l'affirmation du conséquent . Ce dialogue est fini et se termine par un mouvement de tel qui ne peut pas faire un autre mouvement, c'est, ce dialogue est gagné par .

Ces deux dialogues pour la formule montrent que pour une formule valable il peut y avoir des dialogues qui se gagnent aussi bien que des dialogues qui ne se gagnent pas par , bien que tous les mouvements possibles aient été faits. Il existe également des formules invalides pour lesquelles c'est le cas. Un exemple est . Si attaque cette formule avec , puis gagne le dialogue: la défense est attaquée avec , qui se défend avec comme coup final. Si, cependant, attaques avec , alors je ne peux pas faire un autre mouvement, depuis la première conjonction , qui est une formule atomique, ne peut pas être affirmé en raison de la condition 1.

Un dialogue pour la formule du premier ordre est le suivant:

Au lieu de se défendre contre l'attaque de (fait à la position 1) avec en position 2, le promoteur attaque l’affirmation de en affirmant , selon la forme d'argumentation pour . Au poste 3, l'adversaire attaque selon la forme argumentative en choisissant le terme dans l'attaque symbolique , qui se défend en affirmant en position 4. L'adversaire attaque ceci selon la forme d'argumentation pour avec dans le dernier coup. Notez qu'il y a maintenant deux attaques ouvertes effectuées par : celui en position 1 et celui du dernier coup. En raison de la condition 2, seul le dernier des deux peut être défendu. Ainsi le promoteur ne peut rattraper la défense de l’attaque effectuée en position 1, et selon la forme d'argumentation car il n'y a pas de défense contre le dernier coup. Le promoteur ne peut répéter que l'attaque effectuée à la position 2, qui mène à un dialogue infini où une séquence de mouvements comme

se répète sans fin; l'adversaire peut choisir un terme différent à chaque répétition. Notez que les attaques répétées sur le même mouvement sont interdites uniquement pour , alors qu'il n'y a pas une telle restriction. Par conséquent, peut attaquer le mouvement à plusieurs reprises (fait à la position 1) avec le déménagement , démarrer la boucle. En outre, chaque occurrence d'une attaque est défendue au plus une fois, et chaque occurrence d'une formule -signée est attaquée au plus une fois, conformément aux conditions 3 et 4, respectivement. Ce dialogue pour la formule

n'est donc ni gagné par ni ne se termine par un coup adverse.

En résumé, on peut observer qu'il existe des formules valables pour lesquelles il existe des dialogues finis qui ne se gagnent pas ainsi que des dialogues qui se gagnent par , il existe des formules invalides pour lesquelles il en va de même, et il peut y avoir des dialogues infinis, aussi. La notion de victoire dans un dialogue ne suffit pas en elle-même à distinguer la validité d'une formule..

4. Stratégies gagnantes et validité

En logique dialogique, la notion logique centrale de validité est expliquée en termes de la notion de stratégie de la théorie des jeux.. Une stratégie détermine chaque mouvement d'un joueur. La notion cruciale de validité est celle de la stratégie du promoteur gagnant.. La validité dialogique d'une formule consiste en l'existence d'une stratégie du proposant gagnant pour cette formule..

À. Stratégies gagnantes

Un joueur a une stratégie gagnante si, pour chaque mouvement effectué par l'autre joueur, il peut effectuer un autre mouvement., de telle sorte que chaque jeu résultant du jeu (c'est, chaque dialogue résultant) est finalement gagné par . Dans la logique dialogique, on ne s'intéresse généralement qu'aux stratégies gagnantes pour le promoteur. . Une stratégie gagnante pour une formule est un arbre dont les branches sont des dialogues gagnés par , où les nœuds sont les mouvements, tel que

a le déplacement comme nœud racine (avec profondeur 0),
si la profondeur d'un nœud est impaire (c'est, si le nœud est un coup adverse), alors il a exactement un nœud successeur (ce qui est une démarche de promoteur),
si la profondeur d'un nœud est paire (c'est, si le nœud est un promoteur, déplacez-vous), alors il a autant de nœuds successeurs qu'il y a de mouvements possibles à cette position.
b. Exemples

Le dialogue suivant, ce qui a été discuté ci-dessus, est déjà une stratégie gagnante pour la formule :

Cette stratégie du proposant gagnant n’a qu’une seule branche, quel est le dialogue montré. Le nœud racine

n'a qu'un seul successeur, puisque le mouvement est le seul mouvement possible pour . Ce nœud en profondeur 1 a exactement un nœud successeur, à savoir le déplacement en profondeur 2. Celui-ci n'a à son tour qu'un seul nœud successeur, à savoir le déplacement en profondeur 3, puisqu'aucun autre mouvement de l'adversaire n'est possible. Son seul nœud successeur est , qui n'a pas de successeur car il n'y a aucun mouvement adverse possible. Le dialogue est gagné par , et tous les mouvements possibles de l'adversaire ont été pris en compte. Cet arbre à branche unique est donc une stratégie gagnante pour la formule .

En général, les stratégies des promoteurs gagnants comportent plus d’une branche. S'il y a plusieurs coups d'adversaire possibles après un coup de promoteur, alors il y aura une branche pour chacun des mouvements possibles de l'adversaire. Considérez la stratégie suivante du proposant gagnant pour la formule :

Cet arbre d'expressions signées a deux branches. Après le déplacement en profondeur 4, il y a deux déplacements possibles pour , donnant les deux nœuds successeurs (branche gauche) et (branche droite). Le promoteur remporte les deux dialogues résultants: ne peut ni faire un autre mouvement après (dialogue de gauche) ni après (bon dialogue). Ainsi, cet arbre est une stratégie de promoteur gagnante.

c. Stratégies gagnantes de premier ordre

Les stratégies gagnantes pour les formules sans quantificateur sont toujours des arbres finis, alors que les stratégies gagnantes pour les formules du premier ordre peuvent en général être des arbres d'une infinité de branches finies. Un exemple est la stratégie du proposant gagnant suivante pour la formule de premier ordre :

Le mouvement en profondeur 2 a une infinité de nœuds successeurs, puisque pour chaque choix d'un terme (pour les nombres naturels ) l'attaque symbolique est un mouvement possible. Pour des termes deux à deux distincts, l'arbre a donc une infinité de branches (indiqué par ""), où chaque branche est un dialogue gagné par .

De telles stratégies gagnantes infinies peuvent être évitées en utilisant les restrictions suivantes en ce qui concerne les stratégies gagnantes des promoteurs.:

Si la profondeur d'un nœud est paire, et l'attaque symbolique en mouvement est un mouvement possible, où est une nouvelle variable dans cette branche, est alors le seul nœud successeur immédiat qui constitue une attaque contre .
Si la profondeur d'un nœud est paire, est une attaque contre une assertion , et le mouvement est une défense possible contre cette attaque, où est une nouvelle variable dans cette branche, est alors le seul nœud successeur immédiat qui constitue une défense contre .

Il peut y avoir d'autres mouvements possibles, qui ne sont pas des attaques ou des défenses contre . Dans ce cas, le nœud à même profondeur a plus d'un nœud successeur immédiat. Toutefois, le nombre de ces nœuds successeurs immédiats ne peut être que fini, et il n'y a donc plus de ramifications infinies dans les stratégies des promoteurs gagnants.

Par exemple, la stratégie de proposant gagnant infini indiquée ci-dessus se réduit à la stratégie de proposant gagnant fini suivante:

Les restrictions (J’ai) et (Ii) ont pour effet que dans les stratégies gagnantes, une seule des attaques possibles (pour chaque terme ) sur ou défenses (pour chaque terme ) contre il faut en tenir compte, à savoir celui où le terme est une nouvelle variable, alors que dans les stratégies gagnantes qui ne sont pas ainsi restreintes, il faut considérer les mouvements correspondants pour chaque terme , y compris les variables. On peut montrer qu’une stratégie gagnante restreinte peut toujours être étendue à une stratégie sans restriction..

Des ramifications infinies dans les stratégies gagnantes peuvent également être évitées en remplaçant les formes d'argumentation indépendantes du joueur par et par les formes d'argumentation suivantes, dépendantes du joueur.:

L'argumentation se forme et contient la condition selon laquelle la variable est nouvelle. Ils sont donc dépendants de l'histoire dans le sens où la possibilité d'un mouvement ou d'un dialogue dépend du fait que la variable soit déjà survenue dans ce dialogue.. L’argumentation indépendante du joueur se forme pour et , d'autre part, ne dépendent pas de l'histoire.

Les stratégies des promoteurs gagnants pour les dialogues qui en résultent peuvent ensuite être restreintes comme suit: Un seul nœud successeur pour un nœud à profondeur égale doit être pris en compte si

l'attaque symbolique selon la forme argumentative est un coup possible de l'adversaire,
l'attaque symbolique selon la forme argumentative est un coup possible de l'adversaire,
ou le mouvement de l'adversaire défendant une attaque symbolique selon la forme d'argumentation est un mouvement possible.

Encore, d'autres mouvements selon d'autres formes d'argumentation peuvent être possibles. Les stratégies des promoteurs gagnants qui en résultent sont limitées. L’utilisation des formes d’argumentation dépendantes du joueur présente donc des avantages techniques. Toutefois, d'un point de vue conceptuel, des formes d'argumentation indépendantes du joueur pourraient être préférables.

d. Le tiers n’est pas donné et le principe de non-contradiction

Le promoteur n'a pas de stratégie gagnante pour chaque formule. Un exemple est l'instance de tertium non datur. Il n'y a qu'un seul dialogue possible, à savoir:

ce qui n'est pas gagné par . Au poste 2, le promoteur ne peut se défendre contre l'attaque symbolique de ' qu'en choisissant d'affirmer le droit disjoint . Choisir la disjointe gauche n'est pas une option en raison de la condition 1. En raison de la condition 4, l'adversaire ne peut pas répéter l'attaque symbolique en position 3; le seul mouvement possible est d'attaquer avec . Cette attaque ne peut ni être défendue ni être attaquée, et une autre défense contre l'attaque symbolique déjà défendue est exclue par la condition 3.

D'autre part, il existe une stratégie de promoteur gagnante pour chaque cas du principe de non-contradiction, . Considérez la stratégie suivante du promoteur gagnant pour :

Ici, il est essentiel de pouvoir attaquer la même assertion à plusieurs reprises.. L’affirmation de l’adversaire en position 1 est attaquée d’abord en position 2 en choisissant la première conjonction, et encore en position 4, maintenant en choisissant la deuxième conjointe. Les deux attaques sont nécessaires pour avoir une stratégie de promoteur gagnante.

Il n’existe pas de stratégie gagnante dans le cas du tertium non datur, car il ne peut pas se défendre contre l'attaque répétée, alors que dans le cas du principe de non-contradiction, il existe une stratégie du promoteur gagnant car il peut attaquer à plusieurs reprises. En logique classique, le troisième n'est pas donné et les principes de non-contradiction sont équivalents, alors que dans la logique intuitionniste seul le principe de non-contradiction tient. Pour les dialogues considérés, cette distinction repose sur le fait qu'il peut attaquer de manière répétée mais pas se défendre de manière répétée contre une assertion.

Pour résumer, il existe des formules pour lesquelles il existe une stratégie de promoteur gagnante, et il y a des formules pour lesquelles ce n'est pas le cas. Une formule donnée peut également avoir plusieurs stratégies de promoteur gagnantes.

e. Validité dialogique et exhaustivité

La notion dialogique de validité est définie comme suit:

Une formule est dite valide s’il existe une stratégie gagnante du proposant pour .

Que cette notion dialogique de validité corresponde exactement à la prouvabilité intuitionniste est le contenu du résultat de complétude suivant:

Une formule est valide si et seulement si elle est prouvable en logique intuitionniste.

Donc, pour les dialogues définis par les conditions 0 à 4, on obtient une formulation dialogique de logique intuitionniste.

La prouvabilité est fermée sous substitution uniforme des formules par des formules atomiques. C'est, si une formule est prouvable en logique intuitionniste, alors chaque instance de substitution , obtenu en substituant uniformément des formules aux formules atomiques dans , est prouvable en logique intuitionniste, aussi. Le résultat de complétude implique que la validité est également fermée sous substitution uniforme. C'est, s'il existe une stratégie de promoteur gagnante pour , alors il y a des stratégies gagnantes pour chaque exemple qui est le résultat d'une substitution uniforme de formules par des formules atomiques dans .

f. Des stratégies gagnantes comme preuves

Les dialogues peuvent également être considérés comme les constituants d'un système de preuve. Sur cette vue, les preuves d'une formule sont les stratégies gagnantes du proposant pour . L'exhaustivité est ensuite formulée comme un théorème d'équivalence pour gagner des stratégies et des preuves de promoteur dans un système de preuve donné tel que, par exemple, calcul séquentiel:

Il existe une stratégie gagnante pour savoir si et seulement si est prouvable dans le calcul séquentiel pour la logique intuitionniste.

Une preuve constructive de ce théorème a été donnée par Felscher [1985] en montrant qu'il existe des algorithmes transformant toute stratégie gagnante pour une formule en une preuve de calcul séquentiel pour la logique intuitionniste, et, l'inverse, transformer toute preuve en une stratégie de promoteur gagnante pour .

5. Dialogues pour la logique classique

Un rendu dialogique de la logique classique est obtenu en assouplissant les conditions 2 et 3 pour le proposant , tout en les gardant pour l'adversaire . C'est, les conditions 2 et 3 sont remplacées par les conditions suivantes:

2′. S'il y a plus d'une attaque ouverte par , alors seul le dernier peut être défendu par .

3′. Une attaque par peut être défendue par au plus une fois.

Car cela signifie que s'il y a plus d'une attaque ouverte effectuée par , puis peut se défendre contre n'importe laquelle de ces attaques (au lieu de seulement le dernier), et peut se défendre contre les attaques lancées à plusieurs reprises.

Aucune modification n'est apportée aux formulaires d'argumentation. Les dialogues classiques sont définis par rapport à eux comme des séquences finies ou infinies de mouvements effectués selon les conditions 0, 1, 2′, 3′ et 4.

Les stratégies classiques du proposant gagnant pour une formule sont définies comme précédemment dans le cas de la logique intuitionniste., mais avec la notion de dialogue remplacée par la notion de dialogue classique.

À. Exemples

Il existe une stratégie classique du promoteur gagnant pour la formule . Il s'agit du dialogue classique suivant:

Au poste 2, le promoteur ne peut se défendre contre l’attaque symbolique qu’en affirmant le droit disjoint , puisque la disjonction de la gauche atomique n'a pas encore été affirmée (comparer la condition 1). Mais du fait du remplacement de la condition 3 par la condition 3′, le promoteur peut à nouveau se défendre contre cette attaque en position 4, maintenant en affirmant la gauche disjointe , qui a été affirmé par à la position précédente 3.

Il existe une stratégie classique du promoteur gagnant pour la formule , un exemple du principe intuitionnistement invalide de l'élimination de la double négation. Il s'agit du dialogue classique suivant:

Le dernier coup est possible grâce au remplacement de la condition 2 par la condition 2′. En position 3, il y a deux attaques ouvertes par (effectué aux positions 1 et 3, respectivement). La condition 2 interdirait la défense contre la première attaque, puisque ce n'est pas la dernière attaque ouverte. Mais la condition 2′ permet de se défendre contre toute attaque ouverte antérieure. Au poste 4, le promoteur peut ainsi se défendre contre la première attaque en affirmant la conséquence de l'implication attaquée .

Ces deux exemples montrent que le remplacement des deux conditions 2 et 3 par les conditions 2' et 3', respectivement, est nécessaire pour obtenir la logique classique. Sinon, il n’y aurait pas de stratégies gagnantes pour les promoteurs (toutes les instances de) soit le tertium non datur, soit le principe de l'élimination de la double négation, qui sont tous deux des principes de logique classique.

b. Validité et exhaustivité dialogiques classiques

La notion dialogique de validité classique est définie comme suit:

Une formule A est dite classiquement valide s'il existe une formule gagnante classique
stratégie du promoteur pour A.

Le théorème de complétude suivant est valable:

Une formule A est classiquement valide si et seulement si A est prouvable dans
logique classique.

Une preuve de ce théorème pour un calcul séquentiel pour la logique classique peut être trouvée dans Sørensen et Urzyczyn [2006].

Une formulation dialogique de la logique classique a ainsi été obtenue par une modification des conditions de dialogue pour les dialogues intuitionnistes.. Cela signifie qu'on peut obtenir des formulations dialogiques de logiques différentes en changeant les règles des jeux de dialogue..

6. Origines et développements récents

L'approche dialogique de la logique a été proposée pour la première fois par Lorenzen en 1958. (Lorenzen [1960]; Alors vois Lorenzen [1961]) pour la logique intuitionniste ainsi que pour la logique classique. Il est évident que l’approche dialogique en tant que telle ne peut être considérée comme le fondement d’une logique intuitionniste., puisqu'une notion dialogique de validité classique peut être obtenue en modifiant les conditions de dialogue données pour la logique intuitionniste. Si l'on veut obtenir un fondement dialogique pour la logique intuitionniste, il est donc nécessaire de justifier le type particulier de dialogues nécessaires à la logique intuitionniste. Une telle justification a été proposée par Felscher [2002] (publié pour la première fois en 1986); il repose sur les notions de contention, hypothèse et pertinence.

L'approche dialogique a été étendue à plusieurs logiques non classiques, y compris la logique modale et la logique linéaire; pour un aperçu, voir Rahman et Keiff [2005] et Keiff [2011]. Un cadre dialogique pour l'interprétation des implications en tant que règles a été envisagé par Piecha et Schroeder-Heister [2012]. La logique dialogique peut ainsi fournir une base commune pour discuter de différents types de logiques..

7. Références et lectures complémentaires
Andreas Blass. Une sémantique de jeu pour la logique linéaire. Annales de logique pure et appliquée, 56:183-220, 1992.
Présente une sémantique de dialogue pour la logique linéaire. Point de départ des développements de la théorie des jeux en informatique.
Walter Felscher. Dialogues, Stratégies, et prouvabilité intuitionniste. Annales de logique pure et appliquée, 28:217-254, 1985.
Preuve constructive d'exhaustivité pour la logique intuitionniste.
Walter Felscher. Les dialogues comme fondement de la logique intuitionniste. En D. M. Gabbay et F.. Günthner, éditeurs, Manuel de logique philosophique, 2e édition, Tome 5, pages 115 à 145. Intelligent, Dordrecht, 2002.
Explique les concepts de base de la logique dialogique, donne un aperçu de la littérature sur les dialogues, et développe une base argumentative pour un certain type de dialogues comme base d'une logique intuitionniste.
Wilfrid Hodges et Erik C.. O. Crabe. Fondements du dialogue. Volume supplémentaire de la Société Aristotélicienne, 75:17-49, 2001.
Discussion critique entre Hodges et Krabbe sur les dialogues comme fondement de la logique.
Laurent Keiff. Logique dialogique. En E. N. Zalta, éditeur, L'Encyclopédie de philosophie de Stanford. Université de Stanford, Édition été 2011, 2011.
Aperçu de la logique dialogique, y compris les dialogues pour modal, logiques linéaires et autres logiques non classiques. La présentation utilise une formalisation alternative de la logique dialogique.
Érik C.. O. Crabe. Logique des dialogues. En D. M. Gabbay et J.. les bois, éditeurs, Manuel d'histoire de la logique, Tome 7: Logique et modalités au XXe siècle, pages 665 à 704. Elsevier Hollande du Nord, Amsterdam, 2006.
Retrace le développement historique de la logique dialogique. Contient une bibliographie utile.
Kuno Lorenz. Objectifs fondamentaux de la logique du dialogue dans une perspective historique. Dans Rahman et H.. Rückert, éditeurs, Nouvelles perspectives dans la logique dialogique, tome 127 de Synthèse, pages 255 à 263. Springer, Berlin, 2001.
Décrit le développement de la logique dialogique dans un contexte historique, en mettant l'accent sur la notion de dialogue-définition.
Paul Lorenzen. Logique et agonie. Dans Actes du XIIe Congrès international de philosophie (Venise, 12-18 septembre 1958), tome 4, pages 187 à 194. Éditeur Sansoni, Florence, 1960.
Première proposition de dialogues comme moyen d'expliquer la logique intuitionniste et la logique classique.
Paul Lorenzen. Un critère de constructivité dialogique. Dans les méthodes infinitives. Actes du Symposium sur les fondements des mathématiques (Varsovie, 2-9 septembre 1959), pages 193 à 200. Presse Pergame, Oxford/Londres/New York/Paris, 1961.
Explication dialogique de la signification des constantes logiques et de la signification des définitions inductives.
Thomas Piecha et Peter Schroeder-Heister. Implications comme règles dans la sémantique dialogique. Dans M. Peliš et V. Punisseur, éditeurs, L'Annuaire Logica 2011, pages 211 à 225. Publications du Collège, Londres, 2012.
Formule une sémantique dialogique pour l'approche des implications en tant que règles.
Shahid Rahman et Laurent Keiff. Sur comment être un dialoguiste. En D. Vanderveken, éditeur, Logique, Pensée et action, tome 2 de Logique, Épistémologie, et l'unité de la science, pages 359 à 408. Springer, Dordrecht, 2005.
Enquête sur les formulations dialogiques de diverses logiques.
Morten Heine Sørensen et Paweł Urzyczyn. Conférences sur l'isomorphisme de Curry-Howard, volume 149 des Études de Logique et des Fondements des Mathématiques. Elsevier, New York, 2006.
Contient une preuve d'exhaustivité pour les dialogues classiques.
Wolfgang Stegmüller. Remarques sur la complétude des systèmes logiques relatifs aux concepts de validité de P. Lorenzen et K.. Lorenz. Notre Dame Journal de logique formelle, 5:81-112, 1964.
Contient une comparaison de l'approche dialogique de la sémantique avec l'approche Bolzano-Tarski.

Informations sur l’auteur

Thomas Piécha
Messagerie: [email protected]
Université de Tübingen
Allemagne