Résultat formel établissant qu'aucun langage formel suffisamment expressif (par exemple capable de représenter l'arithmétique élémentaire) ne contient une formule qui définisse correctement et uniformément le prédicat de vérité pour les phrases de ce même langage.

Principe

Lorsqu'un langage peut encoder sa propre syntaxe et effectuer des opérations arithmétiques de base, toute tentative de définir la « vérité » depuis l'intérieur conduit à des constructions autoréférentielles qui empêchent l'existence d'une formule de vérité totale et cohérente.

Démonstration

En arithmétique du premier ordre, on montre que si une formule Vrai(x) valait exactement pour les nombres de Gödel des phrases vraies, le lemme diagonal fournit une phrase qui affirme sa propre fausseté par rapport à Vrai, engendrant une contradiction ou l'incapacité de Vrai(x) à être correcte.

Mauvaise application

Prétendre que le théorème interdit toute discussion interne de la vérité et interdire l'usage d'un métalangage, ou affirmer qu'il s'applique à des langages faibles (comme le calcul propositionnel) incapables de coder la syntaxe requise.

Conséquence

Il oblige à traiter la vérité comme un concept défini dans un métalangage plus riche, ou à employer des prédicats de vérité stratifiés ou des hiérarchies de langages plutôt qu'un prédicat unique interne et universel.

Inversion

Si un langage pouvait définir en son sein un prédicat de vérité complet sans contradiction, de nombreux arguments d'indcomplétude et d'indéfinissabilité s'effondreraient, abolissant la séparation entre langage objet et métalangage.

Limite

S'applique aux langages capables d'arithmétisation et d'autoréférence suffisante (par exemple l'arithmétique de Peano). Il ne concerne pas les langages propositionnels finis ni les fragments incapables de représenter la numérotation de Gödel.

Tension sémantique

La tension est entre la notion sémantique intuitive de vérité (propriété globale des phrases) et la notion formelle de définissabilité à l'intérieur d'un langage ; la vérité résiste à une spécification entièrement interne tandis que la démontrabilité peut l'être.

Synthèse

Le théorème de Tarski trace une limite fondamentale : les langages capables d'exprimer leur propre syntaxe ne peuvent pas fournir en leur sein un prédicat de vérité complet et correct, obligeant à recourir à un métalangage ou à restreindre la vérité.