Une sémantique pour langages logiques qui interprète la vérité d'une formule dans un modèle comme l'existence d'une stratégie gagnante dans un jeu d'évaluation associé entre deux joueurs (Vérifieur et Falsificateur) ; connecteurs et quantificateurs sont traduits en règles de jeu gouvernant choix et conditions de victoire.

Principe

La vérité est donnée de manière opérationnelle par l'existence de stratégies gagnantes : les quantificateurs existentiels correspondent à des coups du Vérifieur choisissant des témoins, les universels aux choix du Falsificateur, la conjonction au choix par le Falsificateur d'un conjunct à contester, la disjonction au choix par le Vérifieur d'une disjonction, et la négation au renversement des rôles.

Démonstration

Évaluer la formule ∃x∀y R(x,y) dans une structure M : le jeu d'évaluation voit le Vérifieur choisir un élément a pour x ; ensuite le Falsificateur choisit b pour y ; le Vérifieur gagne si R(a,b) est vraie. L'existence d'une stratégie du Vérifieur qui assure la victoire contre toutes les réponses du Falsificateur équivaut à M ⊨ ∃x∀y R(x,y).

Mauvaise application

Considérer les stratégies gagnantes comme des preuves formelles de vérité sans distinguer stratégies uniformes et témoins existentiels non uniformes, ou appliquer des règles de jeu naïves à des logiques dont les connecteurs n'admettent pas d'interprétation locale de coup (p.ex. certaines modalités probabilistes) sans adapter le jeu.

Conséquence

Offre un compte rendu intuitif et souvent constructif de la vérité qui clarifie la dépendance des choix, permet l'analyse du contenu informationnel et des stratégies (p.ex. logiques d'indépendance) et relie les notions sémantiques à des problèmes algorithmiques de recherche.

Inversion

Contraste avec la sémantique compositionnelle tarskienne : au lieu d'attribuer des valeurs de vérité par induction sur la structure syntaxique, la Sémantique Des Jeux réduit la vérité à l'existence de stratégies gagnantes — inverser ce point de vue met en lumière les perspectives opérationnelles vs. dénotationnelles.

Limite

S'applique naturellement aux logiques dont les connecteurs et quantificateurs admettent des interprétations par coups locaux ; les extensions (p.ex. logiques à point fixe, probabilistes ou à ressources limitées) demandent des jeux adaptés ou une notion enrichie de stratégie pour rendre la sémantique visée.

Tension sémantique

Tension avec les approches proof-théoriques (vérité comme démontrabilité) et les approches purement model-théoriques, notamment sur l'uniformité et la constructivité des témoins : la Sémantique Des Jeux met l'accent sur les stratégies tandis que d'autres privilégient évaluations ou dérivations.

Synthèse

La Sémantique Des Jeux reconstruit la vérité comme résultat d'un concours structuré de l'information : spécifier des règles de coups locales pour les constructions syntaxiques produit des jeux dont les stratégies gagnantes encodent précisément les conditions sémantiques de vérité.