Les systèmes de logiques de Turing basés sur les ordinaux

D'après "Systems of Logic based on Ordinals" de Alan M. Turing.

Le théorème de Gödel montre que chaque système de logique (système formel) est incomplet, mais il indique aussi comment, à partir d'un système L, un système plus complet L' peut être obtenu. En répétant le processus, on obtient une suite de systèmes de plus en plus complets L, L1 = L', L2 = L1', ... On peut contruire une logique L omega dans laquelle les théorèmes démontrables sont la totalité des théorèmes démontrables à l'aide des logiques L, L1, L2, ... On peut ensuite construire L 2 omega à partir de L omega de la même façon qu'on a construit L omega à partir de L. De cette façon on peut associer un système de logique à tout ordinal constructif. On peut se demander si un système de logique de ce type est complet en ce sens que à chaque problème A correspond un ordinal alpha tel que A est puisse être résolu au moyen de la logique L alpha.

Le calcul des conversions. Représentations de Gödel.

Le "Calcul des conversions" (lambda-calcul) de Church permet une plus grande clarté et simplicité d'expression.

On définit la notion d'expression bien formée (EBF) à laquelle est associée des variables libres et/ou liées. Une EBF est soit :

Une EBF est dite en forme normale si elle n'a pas de partie de la forme {lambda V [M]}(N) ni de la forme {{delta}(M)}(N) où M et N n'ont pas de variable libre.

On dit qu'une EBF est immédiatement convertible en une autre si elle peut être obtenue :

Une formule A est dite convertible en une autre formule B (abrégé en "A conv B") s'il existe une suite finie de conversions immédiate permettant de passer d'une formule à l'autre.

Notations :

On introduit les abréviations : ainsi que S -> lambda u f x . f(u(f,x))

Si n représente un entier positif, S(n) est convertible en une formule qui représente son successeur.

Si f est une fonction d'entiers positifs ayant pour valeur des entiers positifs et qu'il y a une EBF F ne contenant pas delta telle que pour tout entier positif n, F(n) est convertible en la formule représentant f(n), alors on dit que f(n) est lambda-definissable ou formellement définissable, et que F définit formellement f(n).

On introduit l'abréviation X+Y -> {lambda a b f x . a(f,b(f,x))}(X,Y)

On dit qu'une EBF G énumère la suite G(1), G(2), ... et toute autre suite dont les termes sont convertibles en ceux de cette suite.

Quand une formule est convertible en une autre qui est en forme normale, on dit que la seconde est la forme normale de la première.

On a les théorèmes suivants concernant les formes normales :

Calculabilité effective. Abréviation de traitement.

Une fonction est dite "effectivement calculable" si ses valeurs peuvent être trouvées par un processus purement mécanique.

On introduit une EBF w avec la propriété w(m,n) conv r si r est le plus grand entier positif, s'il existe, pour lequel m puissance r divise n et r = 1 sinon. On introduit aussi Dt avec les propriétés :

Théorèmes arithmétiques

On appellera théorème arithmétique un théorème de la forme "theta(x) s'annulle pour un nombre infini de nombres naturels x" où theta(x) est une fonction primitive récursive.

Une forme alternative pour les théorèmes arithmétiques est "four tout nombre naturel x il existe un nombre naturel y tel que phi(x,y) s'annulle" où phi(x,y) est primitive récursive.

La question de la vérité d'un énoncé de la forme "f(x) s'annulle-t-elle pour tout x" ou f(x) est une fonction calculable peut être réduite à une question sur la vérité d'un théorème arithmétique, mais la réciproque est fausse.

Tout théorème arithmétique est équivalent à un énoncé de la forme "A(n) est convertible en 2 pour toute EBF n représentant un entier positif", A étant une EBF déterminée par le théorème. A est alors dit dual. De tels énoncés sont réductibles à des théorèmes arithmétiques.

Un type de problème qui n'est pas arithmétique

Suppo sons que nous disposons d'un oracle permettant de résoudre les problèmes arithmétiques. Cet oracle ne peut être une machine. A l'aide de cet oracle nous pouvons fabriquer un nouveau type de machine, les o-machines, ayant parmi leurs opérations de bases la résolution d'un problème arithmétique donné.

La question est-ce qu'une de ces machines imprime une infinité de 0 ou 1 n'est pas un problème arithmétique.

Les théorèmes syntaxique en tant que théorèmes arithmétiques

Considérons une nouvelle règle qui produit uniquement des formules démontrables au sens originel. Considérons une énumération des formules démontrables. Soit phi(r)la RGD de la r-ième formule de l'énumération. Soit psi(r) la RDG de la r-ième formule obtenue par la nouvelle règle Les énoncés de la forme
(r) (existe s) [psi(r) = phi(s)]
sont arithmétiques.

Formules logiques

Une formule L est appelée formule logique ou logique si elle vérifie la propriélé : si A est une formule telle que L(A) conv 2, alors A est dual, c'est à dire A(n) conv 2 pour toute EBF n représentant un entier positif.
Si L est une logique, l'ensemble des formules A telles que L(A) conv 2 est appelé l'extension de L.
Il existe une formule X telle que, si M a une forme normale, n'a pas de variable libre et n'est pas convertible en 2, alors X(M) conv 1, mais si M conv 2, alors X(M) conv 2.
Si L est une logique, alors lambda x . X(L(x)) est aussi une logique dont l'extension est la même que celle de L, et qui a la propriété que si A n'a pas de variable libre, alors {lambda x . X(L(x))}(A) est soit toujours convertible en 1 ou en 2 soit n'a pas de forme normale. Une logique avec cette propriété sera dite standardisée.
On dira qu'une logique L' est au moins aussi complète qu'une logique L si l'extension de L est un sous-ensemble de l'extension de L'. La logique L' est plus complète que la logique L si l'extension de L est un sous-ensemble propre de l'extension de L'.
Supposons qu'on a un ensemble de règles qui permettent de démontrer que des formules sont duales, c'est-à-dire qu'on a un système de logique symbolique dans lequel les propositions démontrées expriment le fait que certaines formules sont duales. Alors on peut trouver une formule logique dont l'extension consiste en les formules qui peuvent être démontrées duales par ces règles, autrement dit il y a une règle pour obtenir la formule logique à partir du système de logique symbolique. En fait le système de logique nous permet d'obtenir une fonction calculable d'entiers positifs dont les valeurs parcourent les RDG des formules démontrables au moyen des règles données. Par le théorème d'équivalence des fonctions calculables et lambda-définissables, il existe une formule J telle que J(1), J(2), ... sont les RDG de ces formules. Posons maintenant :

W -> lambda j v . P (lambda u . delta (j(u), v), 1, I, 2)

Alors W(J) est une logique qui possède les propriétés requises.
Réciproquement, il existe une formule W' telle que si L est une logique, alors W'(L) énumère l'extension de L, car il existe une formule Q telle que Q(L,A,n) conv 2 si et seulement si L(A) est convertible en 2 en moins de n étapes. On pose alors :

W' = lambda l n . form (w (2, P(lambda x . Q (l, Q (l, form (w(2,x)), w(3,x)), n)))
Dans le cas où on a une logique symbolique dont les propositions peuvent être interprétées comme des propositions arithmétiques mais ne sont pas exprimées sous forme de dualité de formules, on a encore une formule logique correspondante, mais sa relation avec la logique symbolique n'est pas si simple.
Nous nous intéresserons principalement aux questions de complétude.
On dit qu'une formule logique L est complète si son extension inclut toutes les formules duales, autrement dit elle permet de démontrer tous les théorèmes arithmétiques vrais. Le théorème de Gödel entraine qu'aucune formule logique n'est complète.
Soit Y une EBF telle que Y(n) est une logique pour tout entier positif n. Les formules de l'extension de Y(n) sont énumérées par W(Y(n)) et les extensions combinées de ces logiques par :

lambda r . (Y (w(2,r), w(3,r)))

Si on pose

Gamma -> lambda y . W' (lambda r . W (y, w(2,r), w(3,r))))

alors Gamma(Y) est une logique dont l'extension est l'extension combinée de Y(1), Y(2), Y(3), ...

A toute EBF L on peut associer une EBF V(L) telle qu'une condition nécessaire et suffisante pour que L soit une formule logique est que V(L) soit duale. Soit Nm une EBF qui énumère toutes les formules avec des formes normales et pas de variables libres. Alors la condition pour que L soit une logique est que L(Nm(r),s) conv 2 pour tous entiers positifs r, s, c'est-à-dire que lambda a . L(Nm(w(2,a), w(3,a)) soit dual.
On peut poser :

V -> lambda l a . l (Nm (w(2,a)), w(3,a))

Ordinaux

On définit une série D(x) munie d'une relation d'ordre G(x,y) par D et G vérifiant (7.1) : La série est dite bien ordonnée et la relation d'ordre est appelée un ordinal si toute sous-série non vide a un premier terme, c'est-à-dire si :

(D') {(existe x) (D'(x)) & (x) (D'(x) => D(x)) => (existe z) (y) [D'(z) & (D'(y) => G(z,y) v z=y)]} (7.2)

Cette condition est équivalente à celle selon laquelle toute sous-suite descendante se termine :

(x) {D'(x) => D(x) & (existe y) (D'(y) & G(y,x))} => (x) (~D'(x)) (7.3)

La relation d'ordre G(x,y) est dite similaire à G'(x,y) s'il existe une bijection entre les séries transformant une relation en l'autre.

Les relations d'ordre sont considérées comme appartenant au même ordinal si et seulement si elles sont similaires.

On aimerait nommer tous les ordinaux mais ça n'est pas possible, car la classe des ordinaux n'est pas dénombrable. Les restrictions qu'on impose sont :

D et G peuvent alors être décrits par une seule EBF Omega avec les propriétés : Etant donné les conditions auxquelles D(x) et G(x,y) sont soumis, Omega satisfait aussi : Si une formule Omega satisfait ces conditions, alors il existe des fonctions propositionnelles correspondantes D(x) et G(x,y). On dit alors que Omega est une formule ordinale si elle satisfait les conditions (a) - (f).
Il s'ensuit que Dt est une formule ordinale représentant omega.

On définit :

On définit une relation d'ordre partielle <, la notion de fomule ordinale C-K (pour Church-Kleene) et la notion de représentation d'ordinaux par des formules : On représente un ordinal représenté par A par Xi A. On écrit A <= B pour A < B ou A conv B.

Si phi est une propriété telle que

alors phi(A) pour toute formule ordinale C-K A.

On a les théorèmes suivants :

Logiques ordinales

Une logique ordinale est une EBF Lambda telle que Lambda(Omega) est une formule logique si Omega est une formule ordinale.

Voyons maintenant comment on peut obtenir des logiques ordinales.

Supposons qu'on a une classe W de systèmes logiques, et une méthode qui permet, à partir d'un système C de W, d'obtenir un nouveau système C' de W tel que les formules démontrables par C' incluent celles démontrables par C. Soit un système valide C0 de W. Supposons enfin que, étant donnée une suite calculable C1, C2, ... de systèmes de W, le "système limite" appartient aussi à W. Dans ces circonstances, on peut construire une logique ordinale. Associons des entiers positifs aux systèmes de sorte que à chaque C correszpond un entier positif m_C et que m_C décrit complètement les règles de procédure de C. Alors il existe une EBF K telle que K(m_C) conv m_C' pour tout C de W, et il existe une EBF Theta telle que, si D(r) conv m_C pour tout entier positif r, alors Theta(D) conv m_C, où C est le système limite ce C1, C2, ... A chaque système C de W on peut associer une formule logique L_C, la relation entre eux est que si G est une formule de W et le théorème arithmétique correspondant à G affirme que B est dual, alors L_C(B) conv 2 si et seulement si G est démontrable dans C. Alors il existe une EBF G telle que G(m_C) conv L_C pour tout C de W. Soit N -> lambda a . G (a(Theta,K,M_C0)). Alors N(A) est une formule logique pour toute formule ordinale C-K A, et si A < B, alors N(B) est plus complète que N(A), pourvu qu'il existe des formules démontrables dans C' mais pas dans C pour tout C valide de W.

On peut maintenant considérer des classes particulières W de systèmes. Pour W on prend la classe des systèmes des Principia Mathematica en leur adjoignant des ensembles d'axiomes.

A tout système C de W on peut associer une fonction primitive récursive P_c(m,n) signifiant "m est la RDG d'une démonstration de la formule dont la RDG est n". On appelle la formule de récursion correspondante Proof_C[x_0,y_0] (c'est-à-dire Proof_C[f(m)0,f(n)0] est démontrable si P_C(m,n) est vrai, et sa négation est démontrable sinon.C' est alors obtenu à partir de C en lui ajoutant toutes les formules de la forme

(existe x_0) Proof_C [x_0, f(m)0] => F

où m est la RDG de F.

Questions de complétude

Le but des logiques ordinales est d'éviter autant que possible les effets du théorème de Gödel qui entraine qu'il est impossible d'obtenir une formule logique complète ou un système de logique complet. Mais on peut à partir d'un système donné en obtenir un plus complet par adjonction en tant qu'axiomes de formules non démontrables dans le système d'origine, et on peut obtenir un système encore plus complet par répétition de ce processus, et ainsi de suite. La répétition de ce processus donne un nouveau système pour chaque formule ordinale C-K.

Une logique ordinale Lambda est dite invariante jusqu'à un ordinal alpha si pour toutes formules ordinales Omega, Omega' représentant le même ordinal inférieur à alpha, l'extension de Lambda(Omega) est identique à l'extension de Lambda(Omega'). Une logique ordinale est invariante si elle est invariante jusqu'à chaque ordinal représenté par une formule ordinale.

On peut montrer qu'il existe des logiques ordinales complètes, mais il n'existe pas de logique ordinale invariante complète.

On a les théorèmes d'incomplétude suivants :

L'hypothèse du continu. Une disgression.

L'hypothèse du continu affirme que 2 puissance aleph_0 = aleph_1, en d'autres termes, si omega_1 est le plus petit ordinal alpha supérieur à omega tel qu'une série avec le type d'ordre alpha ne peut pas être mis en bijection avec les entiers positifs, alors les ordinaux inférieurs à omega_1 peuvent être mis en bijection avec les entiers positifs.

Le but des logiques ordinales

Le raisonnement mathématique peut être vu comme l'exercice d'une combinaison de 2 facultés : l'intuition et l'ingéniosité.

Etant donnée l'impossibilité de trouver une logique formelle qui élimine complètement la nécessité d'utiliser l'intuition, on se tourne vers des systèmes de logique non constructifs dans lesquels les étapes d'une démonstrations ne sont pas tous mécaniques, certains étant intuitifs. Un exemple de logique non constructive est donné par toute logique ordinale.

Logiques ordinales de Gentzen

Pour prouver la consistance d'un certain système de logique formelle, Gentzen a utilisé le principe d'induction transfinie sur les ordinaux inférieurs à epsilon_0 et a suggéré qu'une induction transfinie menée suffisemment loin suffirait à résoudre tous les problèmes de consistance.