NOTOC
En logique mathématique, le théorème de Tarski, ou théorème de non définissabilité de Tarski, s'énonce informellement ainsi :On ne peut définir dans le langage de l'arithmétique la vérité des énoncés de ce langage.
On s'intéresse ici aux formules du premier ordre sur le langage « 0, s, +, ×, ≤ » vraies sur les entiers. Il s'agit de l'arithmétique vraie (ou la vérité dans N : les nombres entiers positifs). On suppose que le langage est récursif : ce qui est le cas quand les symboles primitifs, « 0, s, +, ×, ≤ » pour l'arithmétique de Peano, sont en nombre fini.
Sans entrer dans le détail, les langages des théories que l'on utilise habituellement en mathématique sont récursifs.
Le théorème s'appuie sur les travaux de Gödel, qui, pour la preuve de ses théorèmes d'incomplétude, montre que l'on peut coder les formules par des nombres entiers. Le codage des formules peut se faire de la même façon que pour le théorème d'incomplétude de Gödel. On note ⌈F⌉ le code d'une formule F du langage ; ⌈F⌉ est donc un entier. L'ensemble des entiers qui sont des codes de formules, comme l'ensemble des entiers qui sont des codes d'énoncés (formules closes, sans variables libre) se définissent dans l'arithmétique. On s'intéresse alors à l'ensemble C des codes des formules vraies dans N.
Définir un ensemble de nombres entiers dans le langage de l'arithmétique, c'est trouver une formule de ce langage à une variable libre qui n'est vérifiée que par les entiers de cet ensemble. Par exemple la formule
il existe un y tel que x = y+y, qui a pour seule variable libre x, définit l'ensemble des entiers pairs.
On peut remarquer que dans un langage dénombrable, on ne pourra jamais définir qu'un ensemble dénombrable de sous-ensembles de N, c'est l'argument essentiel pour le théorème de Löwenheim-Skolem. Or d'après un
résultat bien connu de Cantor, l'ensemble des sous-ensembles de N n'est pas dénombrable. On sait donc que tous les sous-ensembles de N ne peuvent être définissables.
Ici, on s'intéresse à définir l'ensemble C des codes des formules vraies dans N.