对于解读哥德尔不完全性定理，理解“真理”与“可证明性”以及它们之间的关系是关键。

法国逻辑学家Jean-Yves Girard主持法语翻译哥德尔1931年的原文（Le théorème de Godel,Ernest Nagel, James R. Newman, Kurt Godel, Jean-Yves Girard），在“符号领域或还原论的失败”一文中，Jean-Yves Girard谈到“真理”与“可证明性”。

一，译文

符号领域或还原论的失败 

- Jean-Yves Girard

1. 真理和可证明性

在下文中，T表示一个未指定的数学理论；哥德尔曾使用Principia System，但现在人们宁愿采取所谓的Peano算术，甚至是集合论。事实上，T的选择对建立程序至关重要；另一方面，对于反驳来说，T允许的抽象方法越多，结果就越有说服力。

如果P是一个可判定的语句，那么 

i）P真意味着在T中的形式可证明性。

ii）P假意味着在T中的形式可反驳性。

为了验证这一断言，让我们注意到，我们有一个判定P的机械程序。一切机械的东西都是可以形式化的：在T的公理中，只要有一些反映导致判定P的计算的东西就足够了。如果这一论证被认为不具有说服力，我们可以写一个程序，这是用一种具有严格语法的语言来完成的，它在某种程度上是一个形式系统。

现在让Q = ∃x ∃y P(x,y)是一个存在陈述；那么

iii) 如果Q是真的，那么它在T中是可以形式证明的。

事实上，说Q是真的，意味着P(x,y)对于某个选择x=n，y=m来说是真的，所以P(n,m)是可以证明的；然后，逻辑规则允许我们在T中形式连接∃x ∃y P(x,y)。

让R=∀x∀y S(x,y)是一个全称陈述；那么 

iv) 如果T是一致的，并且R在T中是可以形式证明的，那么R就是真的。

事实上，R的否定Q是存在的；如果R是假的，那么根据iii）Q在T中是可以被证明的，而T证明R和它的否定将是矛盾的。

如果没有额外的假设，就不可能说明真和可证明之间的其他一般关系。例如，如果T是Peano的算术，T的公理是真的，逻辑规则保留了真，所以T的所有定理都是真的。这种说法的认识论价值是有限的，因为Peano公理的选择正是因为我们相信它们的真理。

也不排除（这也是哥德尔定理所要确定的），一个为真的全称陈述是无法证明的：事实上，这样一个陈述的无限验证过程无法通过形式上的证明来反映，本质上是有限的。

二，原文

Le théorème de Godel 

Ernest Nagel, James R. Newman, Kurt Godel, Jean-Yves Girard

p156

1. Vérité et prouvabilité

Dans ce qui suit, T désigne une théorie mathématique non spécifiée ; Godel avait utilisé le système des Principia, mais, de nos jours, on prendrait plutôt l’arithmétique dite Peano, voire la théorie formelle des ensembles. En fait, le choix de T aurait été crucial pour établir le programme ; par contre, pour une réfutation, plus T permet de méthodes abstraites, plus le résultat est convaincant.

Si P est un énoncé décidable, alors 

i) la vérité de P implique sa démontrabilité formelle dans T,

ii) la fausseté de P implique sa réfutabilité formelle dans T.

Pour vérifier cette assertion, remarquons que nous disposons d’un procédé mécanique pour décider P. Tout ce qui est mécanique est formalisable : il suffit d’avoir parmi les axiomes de T de quoi refléter les calculs qui mènent à la décision de P. Si cet argument n’est pas jugé convaincant, pension à l’écriture d’un programme, qui se fait au moyen d’un langage à la syntaxe rigide, et qui est bien à sa faon un système formel.

Soit maintenant Q = ∃x ∃y P(x,y) un énoncé existentiel ; alors

iii) si Q est vrai, alors il est formellement démontrable dans T.

En effet, dire que Q est vrai veut dire que P(x,y) est vrai pour un certain choix x=n, y=m, et donc P(n,m) est démontrable ; les règles logiques permettent alors d’enchainer formellement ∃x ∃y y P(x,y) dans T.

Soit enfin R = ∀x ∀y S(x,y) un énoncé universel ; alors 

iv) si T est consistante et si R est formellement démontrable dans T, alors R est vraie.

En effet, la négation Q de R est existentielle; si R était fausse, alors d’après iii) Q serait démontable dans T, et T prouvant R et sa négation serait contradictoire.

Il n’est pas possible - sans hypothèse supplémentaire - d’énoncer d’autres relations générales entre vrai et prouvable. Par exemple, si T est l’arithmétique de Peano, les axiomes de T sont vrais, les règles logiques préservent la vérité, donc tous les théorèmes de T sont vrais. La valeur épistémologique d’une telle remarque est limitée, vu que les axiomes de Peano ont été précisément choisis parce que nous croyons à leur vérité.

Il n’est pas non plus exclu (et c’est ce que va établir le théorème d Godel) qu’un énoncé universel vrai ne sont pas prouvable : en effet, le processus infini de vérification d’un tel énoncé ne peut pas être reflété par une démonstration formelle, finie par essence.