💻 computer science

Two Remarks about Game Semantics of Classical Logic

Cet article présente et explique deux remarques inédites de Stefano Berardi relatives à la sémantique des jeux de la logique classique.

Auteurs originaux : Thierry Coquand

Publié 2026-03-05

📖 5 min de lecture🧠 Analyse approfondie

CC BY 4.0

Auteurs originaux : Thierry Coquand

Article original sous licence CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Ceci est une explication générée par l'IA de l'article ci-dessous. Elle n'a pas été rédigée ni approuvée par les auteurs. Pour une précision technique, consultez l'article original. Lire la clause de non-responsabilité complète

🎮 Le Grand Jeu de la Logique : Deux remarques de Stefano Berardi

Imaginez que la logique mathématique n'est pas une suite de règles sèches, mais un grand jeu d'échecs ou un débat animé entre deux joueurs. C'est ce qu'on appelle la "sémantique des jeux".

Dans cet article, Thierry Coquand rend hommage à son ami et collègue Stefano Berardi en partageant deux de ses idées (non publiées) qui ont changé la façon dont nous voyons ce jeu, surtout quand on parle de la logique classique (celle qui accepte que "A ou non-A" soit toujours vrai, même si on ne sait pas lequel est vrai).

Voici les deux grandes idées, expliquées avec des métaphores.

1. Le Débat Infini et le "Regard" Éternel 🕰️

Le contexte :
Dans ce jeu, il y a deux joueurs :

Éloïse (qui cherche à prouver qu'une chose existe, comme un trésor).
Abélard (qui cherche à prouver le contraire, comme un détective sceptique).

Parfois, Éloïse peut faire une erreur, dire "Je choisis ce chemin", puis se rendre compte que Abélard a une meilleure réponse. Elle a alors le droit de faire demi-tour (backtrack) et de changer d'avis. C'est comme si elle pouvait effacer une partie de l'histoire pour recommencer.

Le problème :
Si le jeu dure éternellement (une infinité de coups), comment savoir qui gagne ? Qui est responsable de ce débat sans fin ?

L'idée de Stefano (La remarque n°1) :
Stefano a remarqué quelque chose de très élégant : même dans un débat infini, il existe une structure cachée.
Imaginez que vous regardez le film de ce débat en accéléré. Stefano dit qu'on peut toujours identifier un fil conducteur unique (une séquence de coups) qui traverse tout le temps.

L'analogie : Imaginez un labyrinthe infini. Même si vous vous perdez et faites des détours, il existe un "chemin principal" invisible qui relie le début à l'infini.
Le résultat : Ce chemin unique nous dit exactement qui est le responsable de l'infini. Est-ce Éloïse qui ne trouve jamais la sortie, ou Abélard qui refuse de se rendre ?
Pourquoi c'est génial : Cela permet de prolonger le jeu au-delà de l'infini (ce qu'on appelle le "transfini"). On peut dire : "À l'infini, le joueur X a vu ceci, donc il doit faire ce mouvement". C'est comme donner un "regard éternel" (un view infini) au joueur qui a perdu ou gagné le débat.

2. Le Piège de la "Continuité" : Gagner contre un adversaire trop gentil 🎭

Le contexte :
Dans la logique classique, on veut parfois prouver des choses en utilisant des fonctions (des machines qui transforment des nombres). Pour que la preuve soit valide, on suppose souvent que l'adversaire (Abélard) est "continu".

L'analogie : Un adversaire "continu" est comme un cuisinier qui ne peut goûter qu'un petit morceau de la soupe pour décider si elle est salée. Il ne peut pas connaître toute la recette d'un coup ; il doit y aller étape par étape.

L'idée de Stefano (La remarque n°2) :
Stefano a trouvé un piège magnifique. Il a montré qu'il existe des formules mathématiques fausses (des mensonges) pour lesquelles Éloïse peut tout de même gagner, à condition que son adversaire soit "continu" (gentil et limité).

L'histoire du mensonge : Imaginez une formule qui dit : "Il existe une fonction magique qui est partout égale à 1, sauf en un point où elle est 0". C'est faux (une telle fonction n'existe pas vraiment dans ce contexte).
La stratégie d'Éloïse : Éloïse joue avec une fonction qui est toujours 1. Abélard, pour la battre, doit trouver le point où elle est 0. Mais comme il est "continu", il ne peut tester qu'un point à la fois.
- Éloïse dit : "Je suis 1 partout".
- Abélard teste le point 0. Éloïse change sa fonction après le test pour dire "Ah, en fait, au point 0, je suis 0 !".
- Abélard teste le point 1. Éloïse change encore sa fonction.
- Comme Abélard avance lentement (étape par étape), Éloïse peut toujours le devancer et changer la règle du jeu juste avant qu'il ne touche au vrai point faible.
Le résultat surprenant : Éloïse gagne ! Elle prouve une chose fausse, simplement parce que son adversaire n'a pas assez de puissance de calcul pour voir le "tout" d'un coup.

La leçon profonde :
Cela nous apprend que la logique basée sur l'idée que "l'adversaire est limité" (continuité) ne suffit pas toujours pour définir ce qui est "vrai" ou "réalisable".

Si vous jouez contre un humain (limité), vous pouvez gagner un jeu truqué.
Mais si vous jouez contre un dieu omniscient (qui voit tout d'un coup), vous perdrez.
Conclusion : La "vérité" en logique dépend de la puissance de calcul de ceux qui jouent. Ce n'est pas absolu.

🏁 En résumé

Cet article nous dit deux choses importantes sur la façon dont nous pensons la vérité mathématique :

L'ordre dans le chaos : Même dans un débat infini et confus, il existe toujours un fil conducteur unique qui nous dit qui a raison ou tort. C'est une structure géométrique cachée.
La force fait la loi : Parfois, on peut "prouver" des mensonges si l'on joue contre un adversaire qui ne voit pas l'ensemble de la situation (un adversaire "continu"). Cela nous rappelle que la logique n'est pas juste une affaire de règles abstraites, mais aussi de ressources (temps, mémoire, puissance de calcul).

Stefano Berardi nous a appris à regarder ces jeux non pas comme de simples calculs, mais comme des interactions vivantes où l'histoire, le temps et la mémoire jouent un rôle crucial. C'est une vision très humaine de la logique !

1. Problématique

L'article s'intéresse à la sémantique des jeux pour la logique classique, en particulier dans le cadre d'un calcul propositionnel infini. Le problème central est de comprendre la relation entre les stratégies de jeu (où un joueur peut « revenir en arrière » ou backtrack) et la validité logique, ainsi que les limites de ces interprétations.

Plus spécifiquement, l'auteur examine deux aspects critiques :

La nature des séquences d'interaction infinies et la possibilité d'étendre la notion de « vue » (view) à des séquences transfinies.
La validité de l'interprétation par réalisabilité modifiée pour la logique classique (HA $\omega$ ) : une stratégie gagnante contre un adversaire « continu » suffit-elle à garantir la vérité d'une formule ? L'article met en lumière le fait que certaines formules fausses peuvent posséder de telles stratégies, remettant en cause la suffisance de l'argument de continuité pour caractériser la sémantique de réalisabilité.

2. Méthodologie

L'approche repose sur une sémantique de jeu à information parfaite entre deux joueurs :

$\exists$ loise (le joueur existentiel) : cherche à prouver la formule.
$\forall$ belard (le joueur universel) : cherche à la réfuter.

La particularité de ce cadre (par rapport à la logique intuitionniste) est que $\exists$ loise a le droit de faire des retours en arrière (backtracking). Cela modélise l'idée qu'elle apprend de l'environnement (les réponses de $\forall$ belard) et peut ajuster ses choix.

L'analyse technique utilise :

Des arbres $\land\lor$ pour représenter les formules.
La notion de séquence d'interaction (définie par une paire $(V, \phi)$ où $\phi$ enregistre à quel coup précédent répond le coup actuel).
L'analyse géométrique de ces séquences via des segments et des vues (views).
Des contre-exemples constructifs impliquant des stratégies de choix dénombrable et des fonctions définies par oracle.

3. Contributions Clés et Résultats

L'article présente deux remarques majeures de Stefano Berardi :

Première Remarque : Extension Transfinie des Séquences d'Interaction

Dans les travaux antérieurs [4], il a été démontré (en utilisant la logique classique) que toute séquence d'interaction infinie contient une sous-suite infinie de coups spécifiques.

Théorème 1 (Berardi) : Il existe une unique suite infinie $n_k < n_{k+1}$ telle que $n_k + 1 = \phi(n_{k+1})$ et que les segments $S(n_k)$ forment une partition de $[0, \omega[$ .
Signification : Cette unicité est cruciale. Elle permet d'identifier exactement quel joueur est responsable de l'infini du débat. Si une partie ne se termine jamais, l'un des joueurs a une « vue » à l'étape $\omega$ (l'ensemble $\{n_k\}$ ).
Conséquence : Cela permet d'étendre la notion de séquence d'interaction au-delà de $\omega$ (transfini), en définissant un coup $\phi(\omega)$ basé sur cette vue unique. Cela affine l'analyse de la terminaison des débats (et donc de l'élimination des coupes).

Deuxième Remarque : Limites de la Continuité en Réalisabilité Modifiée

L'auteur examine l'interprétation par réalisabilité modifiée de HA $\omega$ (arithmétique de Heyting avec choix dénombrable).

Le contexte : Dans [2], une stratégie gagnante pour $\exists$ loise contre un adversaire « continu » (qui n'utilise qu'une information finie sur la fonction jouée) était utilisée pour justifier la validité de formules comme le choix dénombrable.
Le contre-exemple (Formule $\ast$ ) : Berardi observe qu'il existe une formule fausse de HA $\omega$ $ω$ :
$\bigvee_f \bigwedge_x \bigvee_y (f(x) = 0 \land f(y) \neq 0)$
Cette formule affirme l'existence d'une fonction $f$ $f$ qui prend la valeur 0 et une valeur non nulle. Bien que fausse (car une fonction constante 0 ou constante 1 contredit cela), elle admet une stratégie gagnante pour $\exists$ $\exists$ loise contre tout adversaire continu.
- Stratégie de $\exists$ loise : Elle construit progressivement une fonction $f$ qui vaut 0 aux points $0, 1, \dots, n-1$ et 1 ailleurs. Si $\forall$ belard répond avec un $x < n$ , elle gagne. Si $\forall$ belard est continu, il finira par répondre avec un $x < n$ pour un $n$ assez grand.
L'interaction infinie : Si l'on oppose cette stratégie ( $A_1$ $A_{1}$ ) à la stratégie de la négation de la formule ( $B_1$ $B_{1}$ ), on obtient un débat infini.
- $A_1$ construit une suite de fonctions $f_0, f_1, f_2, \dots$ en modifiant la valeur de $f$ aux points $0, 1, 2, \dots$ .
- $B_1$ répond toujours en demandant la valeur de $f$ au point $n$ actuel.
- Le débat ne se termine jamais, ce qui signifie qu'il n'y a pas d'élimination de coupe pour ce cas.

4. Signification et Implications

Insuffisance de la Continuité : Ce résultat démontre que l'argument de continuité (le fait qu'un adversaire ne puisse utiliser qu'une information finie) est insuffisant à lui seul pour caractériser la sémantique de réalisabilité. Une stratégie peut gagner contre tout adversaire continu tout en correspondant à une formule fausse. La sémantique de réalisabilité nécessite donc des contraintes supplémentaires au-delà de la simple continuité.
Asymétrie et Croyance Fausse : L'article compare ce phénomène aux travaux de S. Soloviev sur la fonction d'Ackermann. Si un joueur possède plus de ressources de calcul (ou une asymétrie de pouvoir), il peut « piéger » l'autre joueur dans une croyance à une fausseté (comme dans l'exemple de la fonction d'Ackermann où une stratégie primitive récursive peut être battue par une stratégie plus forte sur une formule fausse).
Raffinement de l'Analyse des Coupes : La première remarque offre un outil plus fin pour analyser la terminaison des preuves et l'élimination des coupes, en identifiant précisément la structure de l'infini dans les débats non terminés.

Conclusion

Cet article, basé sur les insights de Stefano Berardi, clarifie les fondements de la sémantique des jeux pour la logique classique. Il établit que l'extension transfinie des vues est possible et nécessaire pour comprendre les débats infinis, et surtout, il met en garde contre l'interprétation naïve de la réalisabilité modifiée : la capacité à gagner contre un adversaire continu ne garantit pas la vérité logique, révélant ainsi des limites subtiles dans la connexion entre calculabilité, continuité et vérité formelle.