On va introduire la notion de vérité, parfois méconnue en dehors de la logique mathématique, mais utile pour comprendre les théorèmes de Gödel. On va voir que la vérité est une notion mathématique, assez intuitive, mais qui ne se formalise pas dans des théories aussi simples que celles dans lesquelles se formalise la démontrabilité : il faut un minimum de théorie des ensembles, alors que la démontrabilité se contente de l'arithmétique. La notion de vérité que l'on va utiliser se définit mathématiquement (mais dans une théorie plus forte que celle étudiée). Le vocabulaire utilisé correspond à l'intuition, la notion est très commode. Mais il n'est pas besoin d'attribuer une valeur excessive à cette notion pour l'utiliser. Par exemple, Gödel construit effectivement un énoncé dont on montre qu'il est vrai dans N, ce que l'on peut interpréter par « on sait le prouver dans une théorie plus forte que celle de départ ».
Les théorèmes de Gödel portent sur des théories pouvant formaliser suffisamment d'arithmétique ; pour simplifier, on se limite de surcroît dans ce paragraphe aux théories arithmétiques, c'est-à-dire aux théories qui ne parlent que des entiers.
Alors que la démontrabilité est définie par rapport à une théorie, un système d'axiomes, la vérité est définie relativement à un modèle, une structure mathématique : un ensemble muni de lois et relations. Si dans une théorie un énoncé peut être indécidable, dans un modèle un énoncé est vrai ou faux, pas d'autre alternative. Nous allons dans la suite nous intéresser à la vérité dans le modèle standard de l'arithmétique, les entiers que «tout le monde connaît», que l'on note N. C'est une structure tellement intuitive que ces précisions peuvent paraître superflues. Mais justement le théorème d'incomplétude de Gödel montre l'existence de structures mathématiques qui ressemblent étrangement aux entiers, par exemple elles vérifient tous les axiomes de l'arithmétique de Peano y compris la récurrence, mais qui ne sont pas les entiers usuels, puisqu'elles vérifient un énoncé faux dans N. En effet, si G est une formule indécidable dans T, prenons l'arithmétique de Peano pour T, nous avons vu à la section précédente que les théories T + G et T + non G sont cohérentes. Cela signifie, d'après le théorème de complétude du même Gödel, que ces théories ont chacune un modèle. Ces deux modèles ne satisfont pas les mêmes énoncés : ils ne peuvent être identiques. L'un d'entre eux au moins n'est donc pas le modèle standard. Quand on démontre le théorème de Gödel, on sait d'ailleurs lequel des deux énoncés est vrai dans le modèle standard (sachant que la théorie T est cohérente). Le fait que l'on sache qu'un énoncé est vrai dans le modèle N, sans savoir le démontrer dans la théorie arithmétique de Peano, signifie simplement qu'on sait le démontrer dans une théorie arithmétique plus forte, que l'on n'a pas forcément cherché à expliciter.
À l'époque où Gödel démontre son théorème, la notion de vérité n'est pas vraiment formalisée, même si elle est connue de ce dernier, puisqu'il a démontré en 1929 le théorème de complétude. La définition utilisée actuellement est due à Alfred Tarski, on la trouve dans un article publié en 1956.
Définissons la vérité dans N. Le langage a pour seul symbole de constante 0, pour seuls symboles de fonction s (la fonction successeur, qui ajoute 1), + et ×, pour seul symbole de relation en plus de l'égalité, le symbole d'inégalité ≤.
Le modèle standard se définit simplement : les seuls éléments de l'ensemble de base du modèle sont les entiers usuels, tous décrits par les termes du langage de la forme s ... s 0 (où s est le signe pour la fonction successeur, "ajouter 1"), c’est-à-dire la notation unaire bien connue qui correspond à l'idée primitive d'entier. Les termes du langage sont essentiellement des polynômes à plusieurs variables et à coefficients entiers positifs, les formules atomiques, qui sont les énoncés élémentaires, sans symbole logique, des égalités ou inégalités polynomiales. Pour définir le modèle il reste à décrire les formules atomiques closes, c’est-à-dire sans variable, vraies et fausses.
On définit facilement la vérité dans N des égalités et inégalités polynomiales sur les entiers (pas de variable !) notés de cette façon, et on peut même le faire mécaniquement, c’est-à-dire que la vérité des énoncés atomiques (égalités et inégalités polynomiales closes) est décidable au sens algorithmique. Les algorithmes en jeu sont essentiellement ceux de l'addition et de la multiplication en base 1, conceptuellement plus simples que ceux que l'on enseigne à l'école primaire pour la base 10 (bien que probablement plus fastidieux à utiliser).
À partir de là, on a défini le modèle, et donc on a la définition par induction de la vérité d'une formule quelconque dans ce modèle. Sans rentrer dans la définition formelle, observons quelques cas particuliers. Tout d'abord la vérité des formules closes sans quantificateurs reste décidable : on peut se ramener à des conjonctions et disjonctions d'égalités et d'inégalités (≠ et ≤) polynomiales. Passons aux quantificateurs, un énoncé du genre ∃x(P(x)=Q(x)) où P et Q sont des polynômes à une seule variable, est vrai quand on peut trouver un entier n tel que P(n)=Q(n). Remarquez que s'il existe un tel entier, une machine pourra le trouver, en essayant les entiers les uns après les autres par ordre croissant. Mais la machine ne s'arrêtera pas s'il n'existe pas de tel entier. Il n'y a pas d'évidence que la vérification de telles formules est algorithmiquement décidable (et elle ne l'est pas).
La situation est « pire » pour le quantificateur universel : un énoncé du genre ∀ x(P(x)=Q(x)) est vrai si pour chaque entier n, l'égalité P(n)=Q(n) est vraie : c'est bien défini, mais, si l'on suit la définition, cela demande une infinité de vérifications ! On voit bien la différence entre vérité et démontrabilité. Une preuve est nécessairement finie, et de plus on doit pouvoir reconnaître mécaniquement une preuve formelle. Pour démontrer un énoncé universel tel que celui-ci, habituellement on fait une récurrence. Sommairement, une preuve par récurrence est une façon finie de représenter une infinité de vérifications. La récurrence peut se « déplier » de façon à construire une infinité de preuves, une pour chaque entier. Cependant la récurrence introduit une certaine uniformité dans ces preuves. Il n'y a aucune évidence qu'ainsi l'on puisse capturer la vérité dans N de tous les énoncés universels, et le théorème de Gödel montre justement que ce n'est pas le cas. L'énoncé de Gödel, qui est vrai dans N et non démontrable est justement un énoncé universel, appelons le ∀ x H(x). Prenons le cas de l'arithmétique de Peano. Quand on définit précisément l'énoncé, on montre que pour chaque entier n, H(n) est prouvable dans l'arithmétique de Peano. Mais on ne peut pas démontrer ∀ x H(x).
Remarquons que, quand on a un moyen mécanique de décider la vérité dans N de certaines classes d'énoncés, par exemple les énoncés sans quantificateurs, on a en particulier une preuve de ces énoncés, ou de leurs négations, au sens non formel de cette notion, sans faire forcément attention à la théorie dans laquelle se dérive cette preuve. Dans les cas abordés ci-dessus, ces preuves se dérivent effectivement dans les théories pour lesquelles on peut démontrer les théorèmes de Gödel.
Rappelons que si l'on démontre un énoncé à partir d'énoncés vrais dans un modèle, l'énoncé obtenu est vrai dans ce modèle, et que, dans un modèle, un énoncé (une formule close) est soit vrai soit faux. Par conséquent la théorie des énoncés vrais dans N est close par déduction et complète. On déduit immédiatement du premier théorème d'incomplétude que
et donc, la vérité étant close par déduction
C'est un théorème d'incomplétude, plus faible cependant que le premier théorème d'incomplétude de Gödel, car il s'applique à moins de théories, les hypothèses étant nettement plus fortes. Par ailleurs on ne peut le formaliser directement dans l'arithmétique, pour en déduire le second théorème d'incomplétude. Tel quel il se déduit d'ailleurs du Théorème de Tarski (1933), qui est plus facile à démontrer que celui de Gödel. Comme l'énoncé G non démontrable est vrai dans N et que la théorie ne démontre que des énoncés vrais dans N, la négation de cet énoncé n'est pas non plus démontrable. Par ailleurs comme la théorie T a un modèle, elle est cohérente.
Il est possible cependant de donner une assertion sous cette forme qui soit vraiment équivalente à celle démontrée par Gödel. On peut en effet préciser dans l'énoncé du théorème la complexité logique de l'énoncé G ci-dessus. Alors, plutôt que de supposer que tous les axiomes de la théorie, et donc finalement tous ses théorèmes, sont vrais dans N, on peut se contenter d'une hypothèse sur les axiomes de la théorie qui a pour conséquence que tous les théorèmes de la complexité logique de la négation de G sont vrais dans N. C'est le cas justement de l'hypothèse de cohérence que faisait Gödel (explicitée dans une note en bas de page ultérieure). Une telle assertion est donnée à la fin du paragraphe diagonalisation dans la suite de l'article.