Cet article ne cite pas suffisamment ses sources (avril 2023).

Si vous disposez d'ouvrages ou d'articles de référence ou si vous connaissez des sites web de qualité traitant du thème abordé ici, merci de compléter l'article en donnant les références utiles à sa vérifiabilité et en les liant à la section « Notes et références ».

En pratique : Quelles sources sont attendues ? Comment ajouter mes sources ?

En logique mathématique, un codage de Gödel (ou numérotation de Gödel) est une fonction qui attribue à chaque symbole et formule bien-formée de certains langages formels un entier naturel unique, appelé son code de Gödel, ou numéro de Gödel. Le concept a été utilisé par Kurt Gödel pour la preuve de ses théorèmes d'incomplétude^[1].

Un codage de Gödel peut être interprété comme un codage dans lequel un numéro est attribué à chaque symbole d'une notation mathématique, après quoi une séquence d'entiers naturels peut alors représenter une séquence de symboles. Ces séquences d'entiers peuvent encore être représentées par des entiers naturels isolés, facilitant leur manipulation dans les théories formelles de l'arithmétique.

Depuis la publication de l'article de Gödel en 1931, le terme « numérotation de Gödel » ou « code de Gödel » a été utilisé pour désigner des assignations plus générales d'entiers naturels à des objets mathématiques.

Gödel a noté que les déclarations dans un système peuvent être représentées par des entiers naturels. La signification de cela était que les propriétés des déclarations—telles que leur vérité et leur fausseté—équivaudraient à déterminer si leurs code de Gödel avaient certaines propriétés. Les nombres impliqués pourraient être très long (en termes de nombre de chiffres), mais ce n'est pas une barrière ; tout ce qui compte, c'est que nous pouvons montrer que ces chiffres peuvent être construits.

En termes simples, nous concevons une méthode par laquelle chaque formule ou déclaration qui peut être formulée dans notre système obtient un nombre unique, de telle sorte que nous pouvons nous convertir mécaniquement entre les formules et les nombres de Gödel. De toute évidence, il existe de nombreuses façons de le faire. Compte tenu de toute déclaration, le numéro auquel il est converti est connu sous le nom de son numéro de Gödel. Un exemple simple est la façon dont les langues sont stockées comme une suite de nombres dans des ordinateurs utilisant ASCII ou Unicode :

• Le mot HELLO est représenté par 72-69-76-76-79 en utilisant ASCII.
• L'énoncé logique x=y => y=x est représenté par 120-61-121-32-61-62-32-121-61-120 en utilisant ASCII.

Gödel a utilisé un système basé sur la factorisation en nombre premier. Il a d'abord attribué un entier naturel unique à chaque symbole de base dans le langage formel de l'arithmétique.

Pour coder une formule entière, qui est une séquence de symboles, Gödel a utilisé le système suivant. Une suite finie ${\displaystyle (x_{1},x_{2},x_{3},...,x_{n})}$ d'entiers strictement positifs, est codée par le produit des n premiers nombres premiers élevés à leurs valeurs correspondantes dans la suite :

${\displaystyle \mathrm {enc} (x_{1},x_{2},x_{3},\dots ,x_{n})=2^{x_{1}}\cdot 3^{x_{2}}\cdot 5^{x_{3}}\cdots p_{n}^{x_{n}}.\,}$

Le théorème fondamental de l'arithmétique assure que deux suites finies distinctes ont deux codes distincts, et il est donc possible de retrouver la suite à partir de son code.

Gödel a utilisé ce schéma à deux niveaux : d'abord pour coder des suites de symboles représentant des formules, puis pour coder des suites de formules représentant des preuves. Cela lui a permis d'exprimer par un énoncé arithmétique, modulo codage, la prouvabilité d'un énoncé arithmétique, un élément nécessaire de la preuve.

Dans la numérotation spécifique de Gödel utilisée par Nagel et Newman, le code de Gödel pour le symbole « 0 » est 6 et le code Gödel pour le symbole « = » est 5. Ainsi, dans leur système, le nombre de Gödel de la formule « 0 = 0 » est 2⁶ × 3⁵ × 5⁶ = 243 000 000.

Une numérotation de Gödel n'est pas unique, car pour toute preuve utilisant les codes de Gödel, il existe une infinité de façons dont ces nombres pourraient être définis.

Par exemple, en supposant qu'il y ait des symboles de base K, un codage de Gödel alternative pourrait être construite en associant de manière invariable cet ensemble de symboles (par exemple, une fonction inversible h) à l'ensemble des chiffres d'un système de numération bijectif K. Une formule composée d'une chaîne de n symboles ${\displaystyle s_{1}s_{2}s_{3}\dots s_{n}}$ serait alors associée au numéro

${\displaystyle h(s_{1})\times K^{(n-1)}+h(s_{2})\times K^{(n-2)}+\cdots +h(s_{n-1})\times K^{1}+h(s_{n})\times K^{0}.}$

En d'autres termes, en plaçant l'ensemble de K symboles de base dans un ordre fixe, de sorte que le i^th symbole correspond uniquement au i^th nombre d'un système de numération bijectif K, chaque formule peut servir, tout comme le nombre même, de son propre code de Gödel.

Par exemple, la numérotation décrite ici a K = 10000.

Une fois qu'un codage de Gödel pour une théorie formelle est établi, chaque règle d'inférence de la théorie peut s'exprimer comme une fonction sur les entiers naturels. Si f est le mappage de Gödel et si la formule C peut être dérivée des formules A et B par une règle d'inférence r; c'est-à-dire.

${\displaystyle A,B\vdash _{r}C,\ }$

Alors il devrait y avoir une fonction arithmétique g_r  d'entiers naturels tels que

${\displaystyle g_{r}(f(A),f(B))=f(C).\ }$

Cela est vrai pour le codage de Gödel utilisé et pour tout autre codage où la formule codée peut être récupérée arithmétiquement à partir de son code.

Ainsi, dans une théorie formelle telle que l'arithmétique de Peano dans laquelle on peut faire des affirmations sur les nombres et leurs relations arithmétiques, on peut utiliser un codage de Gödel pour faire indirectement des déclarations sur la théorie elle-même. Cette technique a permis à Gödel de prouver les résultats sur les propriétés de cohérence et d'exhaustivité des systèmes formels.

En théorie de la calculabilité, le terme « codage de Gödel » est utilisé dans des cas plus généraux que celui décrit ci-dessus. Il peut se référer à:

1. Toute affectation des éléments d'un langage formel à des entiers naturels de telle sorte que les nombres peuvent être manipulés par un algorithme pour simuler la manipulation d'éléments du langage formel.
   
2. Plus généralement, une affectation d'éléments à partir d'un objet mathématique dénombrable, tel qu'un groupe dénombrable, à des entiers naturels permettant une manipulation algorithmique de l'objet mathématique.
   

En outre, le terme de codage de Gödel est parfois utilisé^{[réf. nécessaire]} lorsque ce sont des chaînes de caractères qui servent de codes, ce qui est nécessaire lorsque l'on considère des modèles de calcul tels que des machines de Turing qui manipulent des chaînes, plutôt que des nombres.

Les ensembles de Gödel^{[réf. nécessaire]} sont parfois utilisés en théorie des ensembles pour coder les formules, et sont similaires aux codes de Gödel, sauf que l'on utilise des ensembles plutôt que des nombres pour effectuer l'encodage. Dans les cas simples, lorsqu'on utilise un ensemble héréditairement fini pour coder des formules, cela est essentiellement équivalent à l'utilisation des codes de Gödel, mais un peu plus facile à définir, car la structure arborescente des formules peut être modélisée par l'arborescence des ensembles. Les ensembles de Gödel peuvent également être utilisés pour coder des formules dans des logiques infinies.

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Gödel numbering » (voir la liste des auteurs).

• Codage de Church
• Théorèmes d'incomplétude de Gödel
• Complexité de Kolmogorov

• Gödel's Proof par Ernest Nagel et James R. Newman (1959). Ce livre contient une introduction et un résumé de la preuve, avec une grande section consacrée au codage de Gödel.
• Gödel, Escher, Bach: an Eternal Golden Braid, by Douglas Hofstadter. This book defines and uses an alternative Gödel numbering.
• I Am a Strange Loop by Douglas Hofstadter. This is a newer book by Hofstadter that includes the history of Gödel's numbering.
• Visualizing the Turing Tarpit. Uses Gödel numbering to encode programs.

• Portail de la logique
• Portail de l'informatique théorique
• Portail des mathématiques