# Théorème de Tarski

En logique mathématique, le théorème de Tarski, ou théorème de non définissabilité de Tarski, s'énonce informellement ainsi :

## Explication de l'énoncé
### Formules vraies

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.

### Codage des formules

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 d'entier

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.

### Définir la vérité des énoncés

Ici, on s'intéresse à définir l'ensemble C des codes des formules vraies dans N. Autrement dit, définir la vérité des énoncés c'est avoir une formule V telle que
    A ⇔ V(⌈A⌉)
est vraie dans N pour tout énoncé A.

### Énoncé plus précis

Ainsi, le théorème de Tarski énonce précisément que, quel que soit le codage choisi,
ou plus formellement qu'il n'existe pas de formule V telle que
    A ⇔ V(⌈A⌉)
est vraie dans N pour tout énoncé A.

## Histoire

Alfred Tarski a énoncé et démontré ce théorème dans un article paru en polonais en 1933, puis traduit en allemand en 1936, qui est connu pour être le premier article à proposer des formalisations de la notion de vérité en mathématiques. Il semble cependant que Gödel, lors de ses recherches sur les théorèmes d'incomplétude, ait démontré ce théorème, dont la preuve est très semblable à celle de son premier théorème d'incomplétude tout en étant techniquement plus simple. Il l'a mentionné dans une lettre adressée à John von Neumann en 1931, selon une lettre ultérieure de Gödel lui-même. Il ajoutait qu'il tenait ce théorème pour « la vraie raison de l'existence d'énoncés indécidables dans les systèmes formels contenant l'arithmétique ». Gödel se serait refusé à parler de vérité dans son article de 1931, la notion à l'époque étant controversée.
Le théorème se généralise à tout langage récursif qui permet de définir le langage de l'arithmétique de Peano.

## Forme plus générale du théorème

Ici, on s'intéresse aux énoncés du langage vrais dans N. On peut donc définir mathématiquement cet ensemble, mais pour cela il faut une théorie dans un langage plus riche que celui d'origine. Par exemple on peut définir la vérité dans N en théorie des ensembles, ou plus simplement, en arithmétique du second ordre. Tarski parle d'un méta-langage, qui doit être nécessairement plus riche que le langage objet.

## La preuve du théorème

Comme la preuve du premier théorème d'incomplétude de Gödel, celle du théorème de Tarski utilise un argument diagonal qui fait apparaître un énoncé similaire au paradoxe du menteur.
La démonstration de Tarski est une démonstration par l'absurde. Ainsi, il a supposé l'existence d’une formule de l'arithmétique V(x) à une variable libre x qui définit la vérité, c'est-à-dire que l'équivalence suivante :
    A ⇔ V(⌈A⌉)
est vraie dans N pour tout énoncé A.
Par une diagonalisation identique à celle utilisée pour le premier théorème d'incomplétude de Gödel (en utilisant le prédicat de substitution), on obtient un énoncé D (qui dépend de V), et tel que l'équivalence suivante soit vraie dans N :
    D ⇔ ¬V(⌈D⌉) (le signe ¬ signifie la négation).
L'énoncé D affirme de lui-même qu'il est faux, c'est donc bien une formalisation du paradoxe du menteur. On aboutit à une contradiction, puisque, comme V est censée définir la vérité, on doit aussi avoir :
    D ⇔ V(⌈D⌉) vraie dans N.
On a obtenu l'énoncé D par diagonalisation à partir d'une formule arbitraire V là où, pour son théorème, Gödel utilise une formule qu'il a construite auparavant pour représenter la prouvabilité dans la théorie considérée.

## Source

Raymond Smullyan, Les théorèmes d'incomplétude de Gödel, Dunod, 2000 (ISBN 210005287X)