Définition
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).