Mesure de l'étendue des propriétés, distinctions ou structures qu'un langage logique ou un formalisme donné peut définir ou capturer sur une classe de structures ; on le compare souvent en vérifiant si les formules d'un langage se traduisent dans un autre en conservant la vérité sur toutes les structures considérées.

Principe

Le pouvoir expressif est déterminé par les constructions syntaxiques disponibles (quantificateurs, quantification sur ensembles/fonctions, opérateurs de point fixe, opérateurs modaux) et par l'interaction de ces constructions avec la classe de modèles et les relations intégrées ; des constructions supplémentaires augmentent typiquement ce qui peut être défini mais influencent d'autres propriétés.

Démonstration

La logique du premier ordre ne peut pas exprimer la connexité d'un graphe, tandis que la logique monadique du second ordre (MSO) ou la FO avec clôture transitive le peuvent ; ainsi MSO ou FO+TC ont un pouvoir expressif supérieur pour cette propriété sur les graphes.

Mauvaise application

Assimiler un pouvoir expressif supérieur à une meilleure adéquation pratique : des langages plus expressifs peuvent être indécidables ou informatiquement infaisables, de sorte que le choix d'un langage exige un compromis entre expressivité, décidabilité et concision.

Conséquence

La connaissance du pouvoir expressif oriente le choix des logiques pour la spécification et la vérification, précise les propriétés capturables et sous-tend des résultats liant fragments logiques et classes de complexité (correspondances en complexité descriptive).

Inversion

Faible expressivité : un langage trop faible pour définir les propriétés visées, ce qui oblige soit à enrichir le langage, soit à accepter l'inexpressibilité et à recourir à d'autres méthodes de spécification.

Limite

Dépend du domaine (graphes, ordres, arithmétique), de l'autorisation de signatures préétablies (ordre, arithmétique) et de la sémantique (structures finies vs infinies) ; les comparaisons doivent préciser la classe de structures et la méthode de traduction.

Tension sémantique

Tension entre pouvoir expressif et traitabilité algorithmique ou clarté conceptuelle : des constructions expressives supplémentaires peuvent raccourcir les spécifications mais les rendre plus difficiles à analyser, et deux langages peuvent être incomparables, chacun capturant des intuitions différentes.

Synthèse

Le pouvoir expressif évalue ce qu'un langage peut dire des structures en reliant ressources syntaxiques et définissabilité sémantique : c'est un axe pratique et théorique pour choisir et comparer des formalismes, toujours pondéré par la décidabilité, la concision et les modèles visés.