Une théorie est décidable s'il existe un algorithme qui, pour toute phrase de la langue de la théorie, détermine en temps fini si cette phrase est conséquence de la théorie (c'est‑à‑dire si elle appartient à l'ensemble des théorèmes de la théorie).

Principe

Effectivité de la théorèmabilité : la décidabilité exige que l'ensemble des phrases démontrables à partir de la théorie soit un ensemble décidable (calculable), de sorte que la théorèmabilité soit vérifiable mécaniquement et non seulement récursivement énumérable ou semi-décidable.

Démonstration

Exemple : l'arithmétique de Presburger (la théorie des entiers avec l'addition) est décidable ; la théorie des corps réels clos est décidable parce que l'élimination des quantificateurs réduit les phrases à des assertions sans quantificateurs vérifiables algorithmiquement ; de nombreuses théories dotées de l'élimination des quantificateurs ou d'un fort contrôle des quantificateurs sont décidables.

Mauvaise application

Penser que la décidabilité implique une faisabilité pratique : une théorie décidables peut avoir une complexité computationnelle extrêmement élevée rendant la recherche de preuves impraticable ; ou supposer que la décidabilité se conserve sous des extensions de langue ou d'axiomes sans vérifier les effets sur la calculabilité.

Conséquence

La décidabilité fournit une procédure effective pour décider la théorèmabilité, ce qui permet le raisonnement automatisé, la classification algorithmique des phrases et la vérification reproductible de propriétés ; elle interagit aussi avec la théorie de la complexité pour caractériser la faisabilité pratique.

Inversion

Une théorie indécidable ne possède aucun algorithme décidant la théorèmabilité : des systèmes arithmétiques suffisamment expressifs en sont des exemples, ce qui impose des limites intrinsèques à l'automatisation.

Limite

La décidabilité dépend du choix de la langue, de la signature et des axiomes ; une théorie peut être décidable dans une langue mais indécidable après ajout de symboles ou d'axiomes. Il faut distinguer décidabilité, semi-décidabilité (énumérabilité récursive) et complétude, qui est une notion distincte.

Tension sémantique

Tension entre décidabilité, complétude et axiomatisabilité : la complétude porte sur les valeurs de vérité des phrases, l'axiomatisabilité sur l'énumérabilité récursive des axiomes ; la décidabilité exige une procédure effective pour l'ensemble complet des conséquences et se situe donc à l'intersection de l'expressivité logique et des contraintes de calculabilité.

Synthèse

Une théorie décidable est celle dont les conséquences logiques sont mécaniquement et de façon fiable déterminables : elle transforme la théorèmabilité en un fait algorithmique plutôt qu'en une possibilité théorique, permettant la vérification automatique et le calcul concret dans des applications model-théoriques et algébriques.