RÉCURSIVITÉ, logique mathématique

Indécidabilité et décidabilité

L'étude de l'indécidabilité des théories mathématiques relève de la théorie des fonctions récursives en deux sens : en premier lieu, car un résultat d'indécidabilité signifie qu'une certaine fonction, à savoir la fonction caractéristique de l'ensemble des théorèmes (modulo une bonne numération des formules du langage de la théorie), n'est pas récursive, et, en second lieu, car l'indécidabilité d'une théorie mathématique se démontre la plupart du temps en utilisant le théorème de transfert de A. Tarski qui utilise essentiellement le premier théorème de Gödel suivant lequel la théorie T₁ introduite au chapitre 2 est essentiellement indécidable. Pour qu'une théorie mathématique T dans un langage L soit indécidable, il suffit en effet de trouver un modèle M de T dans lequel on puisse « définir » (en un sens à préciser) un modèle (en général la structure standard <N, +, x> de l'arithmétique) d'une théorie essentiellement indécidable (principalement T₁). Ainsi, par exemple, la théorie des anneaux euclidiens, factoriels, commutatifs... est indécidable car, dans l'anneau Z, on peut définir (dans le langage des anneaux) la structure N. En effet, d'après le théorème de Lagrange suivant lequel tout nombre positif est somme de quatre carrés, on a, dans Z, l'équivalence :

dans laquelle le membre de droite est une formule du langage des anneaux, l'addition et la multiplication des entiers naturels étant définies par la restriction de l'addition et de la multiplication de Z aux éléments de Z vérifiant cette formule. On démontre ainsi de nombreux résultats : la théorie des relations binaires, la théorie des corps, la théorie des groupes, etc., sont indécidables (Par contre, la théorie des corps finis – c'est le théorème d'Ax et Kochen – et la théorie des groupes commutatifs sont des théories décidables.)

Les techniques utilisées pour démontrer la décidabilité d'une théorie mathématique ne relèvent pas, de la théorie des fonctions récursives et font appel en général à des résultats difficiles d'algèbre, d'arithmétique etc. (par exemple le théorème d'Ax et Kochen). Par contre, ces résultats sont intéressants à analyser du point de vue de la complexité des procédures de décision dont ils affirment l'existence. Or, il s'avère que toutes les théories décidables connues ont des procédures de décision qui peuvent demander, avant d'obtenir une réponse, un temps supérieur à l'âge de l'Univers ! Autrement dit, l'espoir d'utiliser ces procédures de décision pour démontrer par ordinateur des théorèmes de mathématiques est, malgré l'existence de telles procédures, illusoire. Citons au hasard quelques résultats illustrant ce point de vue. Soit T_P l'ensemble des formules écrites avec l'addition seulement et qui sont vraies dans N. Cet ensemble est décidable, mais on peut montrer que, pour tout programme de calcul de la fonction caractéristique de T_P, il existe une infinité de formules F telles que, si |F| désigne le nombre de symboles dont elle est constituée, il faudra que ce programme effectue au moins : 2^2ε.|F| (où ε est un nombre positif) étapes de calcul avant de donner une réponse. Si on considère maintenant l'ensemble des formules écrites avec l'addition et la multiplication et qui sont vraies dans R, on a un résultat analogue, mais, dans ce cas, la borne inférieure est plus faible et égale à 2^ε.|F| . Ainsi, bien que la théorie du premier ordre de l'addition et de la multiplication des réels soit décidable (théorème de A.  Tarski), dès que l'on veut vérifier la vérité ou la fausseté d'une formule assez longue, les algorithmes de décision peuvent demander un nombre d'étapes ou un temps fabuleux.[...]