Numérotation Gödel - Gödel numbering

En logique mathématique , une numérotation de Gödel est une fonction qui attribue à chaque symbole et formule bien formée d'un langage formel un nombre naturel unique , appelé son nombre de Gödel . Le concept a été utilisé par Kurt Gödel pour la preuve de ses théorèmes d'incomplétude . ( Gödel 1931 )

Une numérotation Gödel peut être interprétée comme un codage dans lequel un numéro est attribué à chaque symbole d'une notation mathématique , après quoi une séquence de nombres naturels peut alors représenter une séquence de symboles. Ces séquences de nombres naturels peuvent à nouveau être représentées par des nombres naturels uniques, 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 attributions plus générales de nombres naturels à des objets mathématiques.

Vue d'ensemble simplifiée

Gödel a noté que les déclarations au sein d'un système peuvent être représentées par des nombres naturels. La signification de ceci était que les propriétés des déclarations - telles que leur vérité et leur mensonge - équivaudraient à déterminer si leurs nombres de Gödel avaient certaines propriétés. Les nombres impliqués peuvent en effet être très longs (en termes de nombre de chiffres), mais ce n'est pas un obstacle; tout ce qui compte, c'est que nous puissions montrer que de tels nombres 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 numéro unique, de manière à pouvoir convertir mécaniquement les formules et les nombres de Gödel. Il existe manifestement de nombreuses façons d'y parvenir. Compte tenu de toute déclaration, le nombre vers lequel il est converti est appelé son numéro de Gödel. Un exemple simple est la façon dont l'anglais est stocké sous forme de séquence de nombres dans les ordinateurs utilisant ASCII ou Unicode :

  • Le mot BONJOUR est représenté par (72,69,76,76,79) en ASCII décimal .
  • La formule logique x=y => y=x est représentée par (120,61,121,32,61,62,32,121,61,120) en utilisant l'ASCII décimal.

Encodage de Gödel

variables numériques variables de propriété ...
symbole 0 s ¬ ( ) x 1 x 2 x 3 ... P 1 P 2 P 3 ...
Nombre 1 3 5 7 9 11 13 17 19 23 ... 289 361 529 ...
Encodage original de Gödel

Gödel a utilisé un système basé sur la factorisation des nombres premiers . Il a d'abord attribué un nombre naturel unique à chaque symbole de base dans le langage formel de l'arithmétique avec lequel il traitait.

Pour coder une formule entière, qui est une séquence de symboles, Gödel a utilisé le système suivant. Étant donné une séquence d'entiers positifs, le codage Gödel de la séquence est le produit des n premiers nombres premiers élevés à leurs valeurs correspondantes dans la séquence:

Selon le théorème fondamental de l'arithmétique , tout nombre (et, en particulier, un nombre obtenu de cette manière) peut être uniquement factorisé en facteurs premiers , il est donc possible de récupérer la séquence d'origine à partir de son nombre de Gödel (pour tout nombre donné n symboles à encoder).

Gödel a spécifiquement utilisé ce schéma à deux niveaux: premièrement, pour coder des séquences de symboles représentant des formules, et deuxièmement, pour coder des séquences de formules représentant des preuves. Cela lui a permis de montrer une correspondance entre les énoncés sur les nombres naturels et les énoncés sur la prouvabilité des théorèmes sur les nombres naturels, l'observation clé de la preuve. ( Gödel 1931 )

Il existe des moyens plus sophistiqués (et plus concis) de construire une numérotation Gödel pour les séquences .

Exemple

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

Manque d'unicité

Une infinité de numérotations Gödel différentes sont possibles. Par exemple, en supposant qu'il y ait K symboles de base, une numérotation de Gödel alternative pourrait être construite en mappant de manière inversible cet ensemble de symboles (par, par exemple, une fonction inversible h ) à l'ensemble de chiffres d'un système numérique bijectif base- K . Une formule constituée d'une chaîne de n symboles serait alors mappée au nombre

En d'autres termes, en plaçant l'ensemble des K symboles de base dans un ordre fixe, de sorte que le -ème symbole corresponde uniquement au -ème chiffre d'un système numérique de base bijective- K , chaque formule peut servir comme le chiffre même de son propre numéro Gödel.

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

Application à l'arithmétique formelle

Récursion

On peut utiliser la numérotation de Gödel pour montrer comment les fonctions définies par la récursivité de cours de valeurs sont en fait des fonctions récursives primitives .

Exprimer des déclarations et des preuves par des nombres

Une fois qu'une numérotation de Gödel pour une théorie formelle est établie, chaque règle d'inférence de la théorie peut être exprimée en fonction des nombres naturels. Si f est le mappage de Gödel et r est une règle d'inférence, alors il devrait y avoir une fonction arithmétique g r d'entiers naturels telle que si la formule C est dérivée des formules A et B par une règle d'inférence r , ie

ensuite

Ceci est vrai pour la numérotation Gödel utilisée, et pour toute autre numérotation où la formule codée peut être récupérée arithmétiquement à partir de son numéro de Gödel.

Ainsi, dans une théorie formelle telle que l'arithmétique de Peano dans laquelle on peut faire des déclarations sur les nombres et leurs relations arithmétiques les uns avec les autres, on peut utiliser une numérotation 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 concernant les propriétés de cohérence et d'exhaustivité des systèmes formels .

Généralisations

Dans la théorie de la calculabilité , le terme «numérotation de Gödel» est utilisé dans des contextes plus généraux que celui décrit ci-dessus. Il peut faire référence à:

  1. Toute affectation des éléments d'un langage formel à des nombres naturels de telle sorte que les nombres puissent ê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 d'un objet mathématique dénombrable, tel qu'un groupe dénombrable , à des nombres naturels pour permettre une manipulation algorithmique de l'objet mathématique.

En outre, le terme de numérotation de Gödel est parfois utilisé lorsque les «nombres» attribués sont en fait des chaînes, ce qui est nécessaire lorsque l'on considère des modèles de calcul tels que les machines de Turing qui manipulent des chaînes plutôt que des nombres.

Ensembles Gödel

Les ensembles de Gödel sont parfois utilisés dans la théorie des ensembles pour coder des formules, et sont similaires aux nombres de Gödel, sauf que l'on utilise des ensembles plutôt que des nombres pour faire l'encodage. Dans les cas simples, lorsque l'on utilise un ensemble héréditaire fini pour coder des formules, cela équivaut essentiellement à l'utilisation de nombres de Gödel, mais un peu plus facile à définir car la structure arborescente des formules peut être modélisée par la structure arborescente des ensembles. Les ensembles Gödel peuvent également être utilisés pour coder des formules dans des langages infinis .

Voir également

Les références

  • Gödel, Kurt (1931), «Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I» (PDF) , Monatshefte für Mathematik und Physik , 38 : 173–198, archivé de l'original (PDF) le 11/04/2018 , récupéré 07/12/2013 .
  • La preuve de Gödel par Ernest Nagel et James R. Newman (1959). Ce livre fournit une bonne introduction et un résumé de la preuve, avec une grande section consacrée à la numérotation de Gödel.

Lectures complémentaires