David Madore's WebLog: La réalisabilité de Kleene (comme prélude au topos effectif)

Interrompons un petit peu la succession de rants au sujet du covid pour parler un peu de maths. Je déterre pour le terminer un vieux texte que j'avais commencé il y a environ deux ans et que j'avais abandonné, mais auquel je repense parce que j'ai reréfléchi à des questions adjacentes. Le but est ici de définir un concept à cheval entre la logique et la calculabilité qui s'appelle la réalisabilité de Kleene. Plus tard (un jour, si j'en trouve le temps et la patience) j'aimerais parler du topos effectif, et comme le topos effectif contient (généralise, donne un cadre catégorique à) la réalisabilité de Kleene, il sera utile que j'aie au moins écrit à ce sujet avant, même si en principe on n'a pas besoin de passer par cette étape intermédiaire. [Ajout : le billet sur le topos effectif est ici.]

Tout ceci a un rapport avec la logique intuitionniste : j'ai déjà écrit un post de blog à ce sujet, qu'il peut être utile d'avoir lu, mais il faut admettre qu'il est extrêmement brouillon et mal structuré. En tout état de cause, il n'est pas nécessaire de savoir ce que c'est que la logique intuitionniste pour comprendre la définition de la réalisabilité de Kleene. (Le principal prérequis à ce qui va suivre est de savoir les bases de la calculabilité : ce qu'est une machine de Turing — ou toute autre représentation des fonctions partielles calculables —, et savoir qu'on peut les encoder par des entiers naturels ; donc comprendre une expression comme le résultat de l'exécution de la machine de Turing codée par l'entier e sur l'entier n en entrée. c'est-à-dire l'image de n par la e-ième fonction calculable partielle, qui sera noté e•n ci-dessous.) Néanmoins, comme la réalisabilité de Kleene est compatible avec les règles de la logique intuitionniste (elle réalise tous les théorèmes de l'arithmétique de Heyting), et est inspirée par (et rend rigoureux) les principes (informels) de Brouwer-Heyting-Kolmogorov, c'est bien d'en avoir au moins une idée ; cette connexion avec la logique intuitionniste sera encore plus forte dans le topos effectif : on peut dire sommairement qu'un topos est une sorte de « monde mathématique alternatif » régis par les lois de la logique intuitionniste (et le topos effectif est un tel monde où la calculabilité joue un rôle central et notamment toutes les fonctions ℕ→ℕ sont calculables).

Mais le but de cette entrée-ci n'est pas de décrire le topos effectif (pas qu'il soit très long à définir, mais ça devient long si on veut en dire le minimum pour que ce soit intéressant). C'est de présenter une notion plus ancienne, la réalisabilité de Kleene, qui sert de fondement ou de prolégomène à la construction du topos effectif. Je dois avouer que le sens profond de cette notion m'échappe encore, et j'ai vaguement l'impression que personne ne la comprend aussi profondément qu'il voudrait ; je ne sais même pas bien ce que Kleene cherchait à faire en introduisant cette notion. Mais superficiellement, l'idée est qu'on définit une notion que je vais noter n ⊪ φ, lire n réalise φ, entre un entier naturel n et une formule logique φ de l'arithmétique du premier ordre (je vais rappeler ce que c'est plus bas), et dont le sens intuitif est que n apporte une sorte de témoignage(?) algorithmique de la véracité de φ (néanmoins, on va voir que φ n'est pas forcément vraie dans le monde classique, et il va s'agir d'expliquer le rapport entre ces notions).

Le rapport avec le topos effectif sera notamment que les énoncés arithmétique du premier ordre qui sont réalisables (au sens où il existe un n qui les réalise) seront exactement ceux qui seront vrais dans le topos effectif. En particulier, la réalisabilité permet de faire un pont vers la logique intuitionniste, même en partant de la logique classique : on n'a pas besoin de savoir ce qu'est la logique intuitionniste ni comment elle fonctionne pour définir la relation n ⊪ φ, mais une fois qu'on l'a définie, on constate qu'elle fonctionne de façon fondamentalement intuitionniste en φ (et notamment, réaliser la double négation ¬¬φ n'est pas du tout pareil que réaliser φ). Par ailleurs, la relation n ⊪ φ est elle-même une formule logique (avec une variable n de plus que la formule de départ), on peut se demander sous quelle condition elle-même est réalisable, ou démontrable (ou démontrablement réalisable), etc., et les réponses sont assez satisfaisantes.

Avant de donner la définition, je dois rappeler des choses sur la logique, qu'on peut sans doute se contenter de lire en diagonale parce que ce qui suit est vraiment standard et peu surprenant.

D'abord, qu'est-ce que c'est qu'une formule de l'arithmétique du premier ordre ? Il s'agit d'une formule fabriquée à partir des connecteurs logiques et de quantificateurs qui ne peuvent porter que sur les entiers naturels. En voici une définition plus précise :

Pour commencer, un terme (de l'arithmétique du premier ordre) est une expression formée à partir d'un stock illimité de variables (que j'appellerai généralement k, ℓ, m, n, p, q, etc.) et des constantes représentant les entiers naturels (0, 1, 2, etc.) au moyen des opérations de somme (+), produit (×, souvent noté par simple concaténation) et, pour me simplifier la vie, d'élévation à la puissance (↑, souvent noté en plaçant le deuxième argument en exposant du premier) ; une formule atomique (de l'arithmétique du premier ordre) est celle exprimant l'égalité entre deux termes, par exemple m=2n ou p^k+q^k=n^k sont des formules atomiques ; mettons qu'on accepte aussi comme atomiques les formules d'inégalité, comme i≤j, cela me simplifiera aussi la vie ; les variables libres d'une formule atomique sont toutes les variables qui y apparaissent (par exemple, dans m=2n, il y a deux variables libres, m et n). Une formule (de l'arithmétique du premier ordre) est définie inductivement de la façon suivante : (A) toute formule atomique est une formule, ainsi que les formules ⊤ (tautologiquement vraie, qu'on peut considérer comme synonyme de 0=0 si on préfère) et ⊥ (tautologiquement fausse, qu'on peut considérer comme synonyme de 0=1 si on préfère), (B) si φ et ψ sont deux formules, alors φ∧ψ (conjonction logique), φ∨ψ (disjonction logique) et φ⇒ψ (implication logique) en sont, et leurs variables libres sont celles de φ et de ψ, ainsi que ¬φ (négation de φ, qu'on considérera comme une abréviation pour φ⇒⊥) qui a les mêmes variables libres que φ, et (C) si φ est une formule alors ∀n.φ et ∃n.φ sont des formules ayant les variables libres de φ sauf n (notons qu'elle avait parfaitement le droit de ne pas figurer dans φ, par exemple ∃n.(0=0) est une formule légitime — et d'ailleurs vraie). Il faudrait ajouter des parenthèses dans ce que je viens d'écrire pour éviter les ambiguïtés d'écriture, mais je vais supposer que mon lecteur saura le faire sans plus d'explication. Par ailleurs, il faudrait définir la substitution d'un terme pour une variable libre : si φ(n) désigne une formule ayant possiblement la variable libre n, et si t est un terme, alors φ(t) désigne la substitution de t pour la variable n (là où elle est libre, donc pas à l'intérieur d'éventuels quantificateurs ∀n ni ∃n).

Si t est un terme ne faisant pas intervenir la variable n, on utilise les notations ∀n≤t.φ et ∃n≤t.φ comme abréviations (sucre syntaxique) de ∀n.(n≤t ⇒ φ) et ∃n.(n≤t ∧ φ). Une formule dont tous les quantificateurs sont de cette forme est dite (arithmétique) à quantificateurs bornés ou (arithmétique) Δ₀. L'intérêt des formules à quantificateurs bornés est que leur véracité peut se tester de façon « finitaire » (si on veut, on a un algorithme qui, donnée une formule à quantificateur bornés, termine de façon certaine en temps fini en renvoyant vrai ou faux selon que la formule est vraie ou fausse).

Une formule n'ayant aucune variable libre est appelée un énoncé.

Ensuite, j'ai besoin de deux notions de codage classiques. Premièrement, on peut coder (=représenter) les couples d'entiers naturels par des entiers naturels : pour ça, je choisis une bijection ℕ²→ℕ calculable (et même primitive récursive, disons (p,q)↦2^p(2q+1)−1 pour fixer les idées) dont je note ⟨p,q⟩ l'image du couple (p,q). Deuxièmement, j'ai aussi besoin de coder (=représenter) les machines de Turing (ou toute autre façon de représenter les fonctions calculables partielles ℕ⇢ℕ) par des entiers naturels. Il y a plusieurs notations vaguement standard pour désigner l'exécution de la e-ième machine de Turing (i.e., celle codée par l'entier naturel e) sur l'entier n, c'est-à-dire l'image de n par la e-ième fonction calculable partielle : on note ça parfois Φ_e(n) (voire φ_e(n), mais j'ai choisi la lettre ‘φ’ pour désigner des formules logiques donc je ne peux pas), parfois {e}(n), ce qui est une notation franchement pourrie ; une notation plus rare, mais moins problématique, et c'est celle que je vais utiliser, est e•n (cf. ci-dessous pour l'écriture formelle de cette expression dans l'arithmétique du premier ordre). J'écrirai e•n↓ pour signifier que e•n est défini, y compris dans des expressions comme e•n↓=v (de nouveau, cf. ci-dessous).

Bref, ⟨p,q⟩ désignera le couple (p,q) codé sous forme d'un entier naturel, et e•n désignera le résultat de l'exécution du programme codé par l'entier naturel e sur l'entier naturel n passé en entrée (et peut donc ne pas être définie si le programme en question n'est pas correct, ou si son exécution ne termine pas, ou si le résultat n'est pas un entier naturel correct).

L'opération e•n ne fait pas partie du langage de l'arithmétique, mais on peut l'y définir : c'est-à-dire que l'affirmation l'exécution du programme [codé par] e sur l'entrée n termine et renvoie la valeur v (qu'on peut abréger e•n↓=v) peut s'écrire comme une formule de l'arithmétique du premier ordre. Pour être même un chouïa plus précis, il existe une formule T(e,n,x), le prédicat T de Kleene, qu'on peut écrire explicitement mais je ne le ferai pas, et qui est même à quantificateurs bornés (Δ₀ : cf. ci-dessus), dont le sens intuitif est l'exécution du programme e sur l'entrée n termine avec pour trace d'exécution x (la trace d'exécution étant le détail de tous les calculs qu'a fait, par exemple, la machine de Turing désignée par e) ; et une fonction U(x) dont on peut supposer — et je le ferai — que c'est simplement la projection x=⟨t,v⟩ ↦ v sur la seconde coordonnée, qui transforme une trace d'exécution x en le résultat v renvoyé par le calcul. Ainsi, e•n↓ (l'exécution du programme e sur l'entrée n termine) s'écrit/signifie ∃x.T(e,n,x) ; et e•n↓=v (l'exécution du programme e sur l'entrée n termine et renvoie v) s'écrit/signifie ∃t.(T(e,n,⟨t,v⟩)).

★ Voici maintenant la définition de la réalisabilité de Kleene, par induction sur la complexité de la formule réalisée :

lorsque φ est une formule atomique (y compris ⊤ ou ⊥), n ⊪ φ signifie simplement φ (i.e., que φ est vraie) : autrement dit, n'importe quel entier naturel réalise une formule atomique vraie, et aucun entier naturel ne réalise une formule atomique fausse ;
on a n ⊪ (φ∧ψ) lorsque n=⟨p,q⟩ où p ⊪ φ et q ⊪ ψ : autrement dit, les entiers naturels qui réalisent une conjonction sont ceux qui codent un couple formé d'un réalisateur de chaque terme de la conjonction ;
on a n ⊪ (φ∨ψ) lorsque n=⟨0,p⟩ où p ⊪ φ ou bien n=⟨1,q⟩ où q ⊪ ψ : autrement dit, les entiers naturels qui réalisent une disjonction sont ceux qui codent un couple dont le premier membre indique quel terme de la disjonction est réalisé et le second le réalise ;
on a n ⊪ (φ⇒ψ) lorsque, pour tout p tel que p ⊪ φ, on a (n•p↓) ⊪ ψ : autrement dit, les entiers naturels qui réalisent une implication sont ceux qui codent un programme (une fonction calculable (partielle)) qui, quand on lui fournit en entrée un entier p réalisant l'antécédent de l'implication, termine en temps fini et renvoie un entier réalisant la conclusion ;
en particulier (puisque ¬φ signifie φ⇒⊥ et qu'aucun entier ne réalise ⊥), on a n ⊪ ¬φ (pour n'importe quel n) lorsqu'il n'existe aucun entier p tel que p ⊪ φ ;
on a n ⊪ ∀x.φ(x) lorsque, pour tout k, on a (n•k↓) ⊪ φ(k) (ou, pour être tout à fait précis, (n•k↓) ⊪ φ(‘k’) où ‘k’ désigne la constante qui désigne l'entier naturel k, et φ(‘k’) la substitution de cette constante pour x dans la formule φ(x)) : autrement dit, les entiers naturels qui réalisent une quantification universelle sont ceux qui codent une fonction calculable (totale) qui, quand on lui fournit en entrée un entier k, renvoie un entier réalisant l'instance φ(k) en question de la formule universellement quantifiée ;
on a n ⊪ ∃x.φ(x) lorsque n=⟨k,p⟩ où p ⊪ φ(k) (ou, pour être tout à fait précis, p ⊪ φ(‘k’) comme dans le point précédent) : autrement dit, les entiers naturels qui réalisent une quantification existentielle sont ceux qui codent un couple dont le second membre un entier réalisant l'instance de la formule existentiellement quantifiée donnée par le premier membre.

Pour être tout à fait exact, je définis par les mêmes clauses énumérées ci-dessus deux variantes de la réalisabilité : il y a une notion dans l'univers mathématique, si j'ose dire, ambiant (n étant un entier naturel et φ une formule de l'arithmétique du premier ordre, n ⊪ φ a le sens défini par les clauses ci-dessus), et il y a une réalisabilité formalisée qui consiste à voir les clauses ci-dessus elles-mêmes dans l'arithmétique du premier ordre, c'est-à-dire qu'on va définir, par exemple, n ⊪ (φ∧ψ) comme la formule ∃n.(n=⟨p,q⟩ ∧ (p⊪φ) ∧ (q⊪ψ)) et ainsi de suite. Il n'y a pas forcément besoin de distinguer ces deux notions, mais il est important de noter que la réalisabilité peut être formalisée, et donc que n ⊪ φ est elle-même une formule de l'arithmétique du premier ordre (pour n une variable libre n'apparaissant pas libre dans φ). (Ce n'est pas tellement différent de la formalisation de la notion de démonstration : l'affirmation φ est démontrable dans l'arithmétique de Peano, par exemple, est un énoncé arithmétique lorsque φ en est un : cf. ici pour plus d'explications.)

On lit n ⊪ φ en disant que n réalise φ ou que φ est réalisée par n, et ∃n.(n⊪φ) en disant que φ est réalisable.

Je souligne que même si classiquement, φ⇒ψ signifie simplement (¬φ)∨ψ, la réalisabilité de ces deux formules est définie de façon très différente. C'est un signe que la réalisabilité ne respecte pas les règles de la logique classique (elle respectera celles, un peu plus faibles, de la logique intuitionniste), je vais y revenir mais je le signale d'ores et déjà.

Maintenant, si φ est un énoncé, on peut s'interroger sur le lien entre un certain nombre de choses :

la véracité de φ (i.e., φ, c'est-à-dire, φ est vrai),
la démontrabilité de φ dans tel ou tel système formel de l'arithmétique, par exemple l'arithmétique de Peano ou bien celle de Heyting (cf. plus loin),
la réalisabilité de φ, c'est-à-dire l'existence d'un n tel que n ⊪ φ (ce qui revient à la véracité de l'énoncé arithmétique du premier ordre ∃n.(n⊪φ)),
la démontrabilité de la réalisabilité de φ, là aussi, dans tel ou tel système formel,
mais on pourrait continuer : la réalisabilité de la réalisabilité de φ ? la réalisabilité de la démontrabilité de φ ?

(Je rappelle à toutes fins utiles que χ est vrai signifie simplement χ, c'est juste une périphrase linguistique, éventuellement avec un changement de niveau de méta… Donc la véracité de la démontrabilité de φ c'est juste la démontrabilité de φ, la véracité de la réalisabilité de φ, c'est juste la réalisabilité de φ, etc.)

Essayons d'y voir un peu plus clair dans ce bordel. Ce qui va suivre va être technique, mais j'espère que même une lecture en diagonale présente un certain intérêt.

La réalisabilité de φ a certainement un rapport avec la véracité de celle-ci. Pour commencer, si φ est atomique, c'est exactement comme ça qu'on a défini n ⊪ φ : cela signifie simplement φ (et ça ne dépend pas de n). Mais on peut faire mieux : si φ est une formule Δ₀ (c'est-à-dire à quantificateurs bornés et donc algorithmiquement testable, cf. ci-dessus), alors elle est réalisable si et seulement si elle est vraie, et plus précisément, il existe un algorithme qui prend la formule φ en entrée et des entiers à substituer à ses variables libres, termine toujours en temps fini, et renvoie soit faux si la formule est fausse (pour ces valeurs), auquel cas elle est irréalisable, et, sinon, renvoie un entier qui la réalise. Cet algorithme est assez transparent par induction sur la complexité de φ (par exemple, quand on l'applique sur φ∨ψ, il va s'appliquer récursivement sur φ puis sur ψ et, si l'un d'eux est réalisable par un entier n, renvoyer le couple ⟨0,n⟩ ou ⟨1,n⟩ selon le cas, tandis que dans le cas contraire il va renvoyer faux ; quand on l'applique sur ∀n≤t.φ(n), il va tester φ(n) pour toutes les valeurs jusqu'à t, et, si elle est toujours vraie, renvoyer une fonction qui à n≤t associe un entier réalisant φ(n), tandis que si elle et fausse, il renvoie faux).

Bon, mais c'est pour une formule à quantificateurs bornés — et donc algorithmiquement testable — que, comme je viens de l'expliquer, la réalisabilité est simplement équivalente à la véracité.

Qu'en est-il de la formule e•n↓ (l'exécution du programme e sur l'entrée n termine) dont je rappelle qu'elle se formalise en ∃x.T(e,n,x) où T(e,n,x), le « prédicat T de Kleene » est à quantificateurs bornés ? Un entier réalisant cette formule est un couple ⟨x,p⟩ où x est une trace d'exécution de la machine de Turing e et p réalise la formule T(e,n,x) attestant ce fait — d'après ce qu'on vient de dire, un tel entier existe si et seulement si la formule T(e,n,x) est vraie, donc là aussi, la formule e•n↓ est réalisable si et seulement si elle est vraie.

Et qu'en est-il de la formule ¬(e•n↓) (l'exécution du programme e sur l'entrée n ne termine jamais) ? D'après ce qu'on a expliqué sur la réalisation d'une négation et d'après ce qu'on vient de dire, ¬(e•n↓) est réalisable (et elle l'est, alors, par n'importe quel entier) si et seulement si e•n↓ n'est pas réalisable, ce qui se produit si et seulement si e•n↓ est fausse, c'est-à-dire si et seulement si ¬(e•n↓). Encore une fois, la formule ¬(e•n↓) est réalisable si et seulement si elle est vraie.

Mais considérons maintenant l'énoncé suivant : ∀e.∀n.((e•n↓) ∨ ¬(e•n↓)) qui affirme que toute machine de Turing e, exécutée sur une entrée n quelconque, soit termine, soit ne termine pas. Classiquement, c'est une tautologie logique, donc, elle est certainement vraie. Mais un entier qui réaliserait cette formule coderait un programme prenant e puis n en entrée et renverrait un entier réalisant la disjonction, ce qui, d'après la définition de la réalisation d'une disjonction et d'après les deux paragraphes précédents, revient essentiellement à dire si e•n↓ ou non. Bref, réaliser cette formule revient à décider le problème de l'arrêt des machines de Turing. Ce qui n'est pas possible. Donc cette formule, bien que tautologiquement vraie, n'est pas réalisable.

Mais du coup, la négation de cette formule, ¬∀e.∀n.((e•n↓) ∨ ¬(e•n↓)), elle, est réalisable (par n'importe quel entier !), et pourtant, elle est tautologiquement fausse. Le lien entre réalisabilité et vérité est donc cassé ; ou encore, on voit que la réalisabilité semble parler de la vérité dans un monde un peu différent.

Maintenant, pour se rassurer un peu, la réalisabilité vérifie les règles de la logique intuitionniste. Je peux par exemple définir celles-ci de la façon suivante :

axiomes du calcul propositionnel : les formules P⇒P, P⇒Q⇒P et (P⇒Q⇒R)⇒(P⇒Q)⇒P⇒R (noter que ‘⇒’ s'associe à droite, c'est-à-dire que P⇒Q⇒R se parenthèse implicitement comme P⇒(Q⇒R)) sont des axiomes quelles que soient les formules P,Q,R, ainsi que P⇒Q⇒P∧Q, P∧Q⇒P et P∧Q⇒Q, et aussi P⇒P∨Q, Q⇒P∨Q et (P⇒R)⇒(Q⇒R)⇒P∨Q⇒R, et enfin ⊤ et ⊥⇒P ; on rappelle par ailleurs que ¬P est traité comme une abréviation pour P⇒⊥ ;
règle de modus ponens : de P⇒Q et P on peut déduire Q ;
axiomes du calcul des prédicats : la formule (∀x.P(x))⇒P(t) est un axiome, quel que soit la formule P(x) et le terme t, où on a noté P(t) le résultat de la substitution de t à la variable libre x dans la formule P(x) ; de même, P(t)⇒∃x.P(x) est un axiome ;
règles de généralisation : de Q⇒P(x), où P et Q sont deux formules où la variable x n'apparaît pas libre dans Q on peut déduire Q⇒∀x.P(x) ; et de P(x)⇒Q, avec la même restriction (x pas libre dans Q), on peut déduire (∃x.P(x))⇒Q ;
axiomes de l'égalité : ∀x.(x=x) est un axiome, ainsi que ∀x.∀y.((x=y)⇒(y=x)) et que ∀x.∀y.(x=y ⇒ P(x)⇒P(y)) quelle que soit la formule P(x) et en notant P(y) la même formule après substitution de la variable libre x en y (une autre variable).

Tout ça est réalisable au sens où on peut trouver des entiers naturels qui réalisent les axiomes (et même « uniformément », c'est-à-dire qu'on n'a pas besoin de regarder ce qui se cache dans les P et compagnie) et que si les prémisses d'une règle de déduction sont réalisables la conclusion l'est aussi (et même uniformément et algorithmiquement, c'est-à-dire qu'on calcule un entier réalisant la conclusion de façon algorithmique à partir d'entiers réalisant les prémisses). À titre d'exemple, un entier réalisant l'axiome (P⇒R) ⇒ (Q⇒R) ⇒ P∨Q ⇒ R est donné par un programme qui prend en entrée un entier m (supposé réaliser P⇒R) et renvoie un programme qui prend en entrée un entier n (supposé réaliser Q⇒R) et renvoie un programme qui prend en entrée un entier ℓ (supposé réaliser P∨Q) et écrit ℓ sous la forme ⟨k,u⟩ et, si k=0, renvoie m•u tandis que que si k=1, il renvoie n•u (les autres valeurs de k ne devraient pas apparaître et peu importe ce qu'on fait, par exemple une boucle infinie) ; bon, dans la suite, je parlerai d'un programme qui prend en entrée m puis n puis ℓ (sous-entendu : de façon curryfiée) plutôt que de répéter ces formules lourdingues de programme qui prend en entrée m et renvoie un programme qui prend en entrée n et renvoie un programme qui prend en entrée ℓ que je viens d'utiliser.

Une chose qui n'est pas réalisable en général est la loi de Peirce ((P⇒Q)⇒P)⇒P dont l'addition aux système d'axiomes ci-dessus transformerait la logique intuitionniste en logique classique. En effet, si c'était le cas, l'énoncé ∀e.∀n.((e•n↓) ∨ ¬(e•n↓)), qui est une tautologique de la logique classique, serait réalisable, et on a expliqué que ce n'est pas le cas.

Sont également réalisables les axiomes de l'arithmétique de Heyting, qui sont les mêmes que ceux de l'arithmétique de Peano, disons (je ne sais pas si la présentation que je fais ci-dessous est le meilleur choix possible, mais il me semble bien que ceci devrait fonctionner) :

¬(0=1), ainsi que tous les axiomes 0+1=1, 1+1=2, 2+1=3, 3+1=4, etc. (ou bien on ne garde que 0+1=1 et on considère 2, 3, 4, etc., comme des abréviations de langages pour 1+1, (1+1)+1, ((1+1)+1)+1, etc.) ;
∀n.¬(n+1=n) ;
l'axiome d'injectivité du successeur : ∀m.∀n.(m+1=n+1 ⇒ m=n) ;
l'axiome de récurrence : P(0) ⇒ (∀n.(P(n)⇒P(n+1))) ⇒ ∀n.P(n) pour toute formule P(n), en notant P(0) et P(n+1) les substitutions évidentes ;
la définition de l'addition : ∀n.(n+0=n) et ∀k.∀n.(n+(k+1)=(n+k)+1) ;
la définition de la multiplication : ∀n.(n·0=0) et ∀k.∀n.(n·(k+1)=(n·k)+n) ;
la définition de l'exponentiation : ∀n.(n↑0=1) et ∀k.∀n.(n↑(k+1)=(n↑k)·n) ;
la définition de l'ordre : ∀n.(n≤n) et ∀k.∀n.(n≤k ⇒ n≤(k+1)) et ∀n.¬(n+1≤n) ; on peut ensuite décider que n<k est une abréviation de n+1≤k, et que k≥n et k>n sont simplement des écritures différentes de n≤k et n<k (c'est-à-dire de n+1≤k).

(Pour que ce soit bien clair : l'arithmétique de Heyting HA et l'arithmétique de Peano PA ont les mêmes axiomes arithmétiques, que je viens de lister, la seule différence est que l'arithmétique de Heyting opère en logique intuitionniste, définie plus haut, tandis que l'arithmétique de Peano opère en logique classique, qui s'obtient en ajoutant la loi de Peirce ou le principe du tiers exclu.)

La plupart de ces axiomes sont triviaux à réaliser (par exemple, ∀m.∀n.(m+1=n+1 ⇒ m=n) est réalisé par le programme qui prend en entrée un entier m puis n puis k (ce dernier supposé réaliser m+1=n+1) et renvoie n'importe quoi). Le seul qui demande un tout petit peu de programmation est celui de la récurrence : on peut réaliser P(0) ⇒ (∀n.(P(n)⇒P(n+1))) ⇒ ∀n.P(n) par un programme qui prend en entrée un entier m (supposé réaliser P(0)) puis e (supposé réaliser ∀n.(P(n)⇒P(n+1))) puis n et renvoie h(n−1, h(n−2, h(n−3,… h(1, h(0,m))…))) où je note abusivement h(r,v) pour (h•r)•v (l'application curryfiée de h à r puis v).

Il résulte de ce qui vient d'être dit que tous les théorèmes de l'arithmétique de Heyting sont réalisables.

C'est déjà un résultat remarquable : il implique notamment que toute fonction définissable démontrablement totale de l'arithmétique de Heyting est nécessairement calculable au sens de Church-Turing, c'est-à-dire que si on a une formule P(x,y) telle que ∀x.∃!y.P(x,y) soit un théorème de l'arithmétique de Heyting (où comme d'habitude ∃!y.Q(y) signifie ∃y.(Q(y) ∧ ∀z.(Q(z)⇒z=y))) alors la fonction x ↦ (l'unique y tel que P(x,y)) qu'elle définit est automatiquement calculable : en effet, on vient de voir qu'il existe un entier qui le réalise, et cet entier est un programme qui prend x et renvoie notamment y. (Ce qu'on appellera ECT₀ ci-dessous sera une sorte d'extension de cette idée.)

En particulier, remarquons qu'on vient de démontrer un résultat d'indépendance : il n'est pas possible dans l'arithmétique de Heyting que toute machine de Turing s'arrête ou ne s'arrête pas, ∀e.∀n.((e•n↓) ∨ ¬(e•n↓)), ou d'ailleurs ∀x.((x•x↓) ∨ ¬(x•x↓)), puisque cet énoncé n'est pas réalisable ; ou, si on veut, on ne peut pas affirmer que la formule P(x,y) := (y=1 ∧ (x•x↓)) ∨ (y=0 ∧ ¬(x•x↓)) (censée définir la fonction qui à x associe 1 si x•x↓ et 0 si ¬(x•x↓)) vérifie ∀x.∃!y.P(x,y).

Néanmoins, il existe des énoncés qui sont réalisables et qui ne sont pas des théorèmes de l'arithmétique de Heyting : j'ai déjà donné l'exemple de ¬∀e.∀n.((e•n↓) ∨ ¬(e•n↓)) (qui ne peut donc pas être un théorème de l'arithmétique de Heyting car ce serait, en particulier, un théorème de l'arithmétique de Peano, ce qui n'est certainement pas le cas car en logique classique elle est trivialement réfutable). Mais il y a « essentiellement » un schéma d'axiomes qui « explique » la différence entre les énoncés réalisables et les théorèmes de l'arithmétique de Heyting.

Avant d'énoncer ce principe, on définit la notion de formule presque négative : je rappelle qu'une formule Δ₀ est une formule dont tous les quantificateurs sont bornés (et qui est donc, en pratique, algorithmiquement testable) ; une formule Σ₁ est une formule obtenue à partir d'une formule Δ₀ en ajoutant (éventuellement) des quantificateurs existentiels devant (par exemple, e•n↓, c'est-à-dire le e-ième programme termine sur l'entrée n, est Σ₁ et c'est en quelque sorte « la seule » parce que tout peut s'y ramener) ; et une formule presque négative (resp. négative) est une formule construite à partir des formules Σ₁ (resp. Δ₀) au moyen des connecteurs ‘∧’, ‘⇒’ (donc aussi ‘¬’ si on veut) et ‘∀’. Disons de façon très grossière que les formules négatives, ou, dans une moindre mesure, presque négatives, sont celles qui n'ont « pas de contenu constructif ». Il faudra que je parle un peu plus longuement des ces notions, mais dans le principe qui suit on peut déjà se contenter de regarder le cas de la formule triviale D(x):=⊤.

Le schéma d'axiomes suivant est réfutable dans l'arithmétique de Peano (même pour D(x):=⊤), mais, on va expliquer pourquoi, il est cohérent avec l'arithmétique de Heyting :

Thèse de Church-Turing étendue (ECT₀) : (∀x.(D(x)⇒∃y.(P(x,y)))) ⇒ ∃e.∀x.(D(x)⇒P(x,(e•x↓))) (où, comme expliqué avant, P(x,(e•x↓)) se formalise comme ∃t.∃y.(T(e,x,⟨t,y⟩) ∧ P(x,y)) avec T le prédicat T de Kleene) : ici P(x,y) est une formule quelconque des variables x et y, et D(x) est une formule presque négative. Autrement dit, ce principe affirme que n'importe quelle relation P(x,y) qui est totale en x sur un domaine D presque négatif contient le graphe d'une fonction e calculable définie sur ce domaine.

Ceci est classiquement faux (même avec D(x):=⊤) comme le démontre l'exemple de la formule exprimant le problème de l'arrêt, disons P(x,y) := (y=1 ∧ (x•x↓)) ∨ (y=0 ∧ ¬(x•x↓)), qui est démontrablement non calculable : ce qui ne marche pas en arithmétique de Heyting c'est qu'on ne peut pas démontrer ∀x.∃y.(P(x,y)), ce qui reviendrait à démontrer ∀x.((x•x↓) ∨ ¬(x•x↓)) (et le même exemple montre que, même dans l'arithmétique de Heyting, on ne peut pas se passer d'une hypothèse comme D(x) est presque négative, car sinon prendre ∃y.(P(x,y), c'est-à-dire (x•x↓) ∨ ¬(x•x↓), pour D(x) ferait quand même marcher cet exemple). Néanmoins, (chaque instance de) ECT₀ est réalisable : donné e qui réalise ∀x.(D(x)⇒∃y.(P(x,y))), ce même e, à peine modifié, convient pour attester ∃e.∀x.(D(x)⇒P(x,(e•x↓))) ; le fait que D soit presque négative sert à assurer que si elle est vraie alors elle est réalisable.

Il faut que j'introduise encore un dernier axiome : le principe de Markov (MP) : (∀x.(R(x)∨¬R(x))) ⇒ (¬¬∃x.R(x)) ⇒ ∃x.R(x).

Celui-ci est une tautologie en logique classique (alors qu'ECT₀ était, au contraire, réfutable). Intuitivement, son sens est que si pour chaque x on sait reconnaître si R(x) est vrai ou faux, et s'il ne peut pas être faux pour chaque x (noter que ¬¬∃x.R(x) peut se réécrire ¬∀x.¬R(x) si on préfère), alors on peut trouver un x pour lequel il est vrai. Cette explication donne aussi une clé pour réaliser MP : à savoir, le programme qui prend en entrée un entier e (supposé réaliser ∀x.(R(x)∨¬R(x))) puis un entier arbitraire (supposé réaliser (¬¬∃x.R(x)), mais ceci est sans intérêt parce que ça n'apporte rien), puis effectue une boucle infinie sur les entiers naturels x, en évaluant à chaque fois e•x jusqu'à en trouver un qui soit de la forme ⟨0,v⟩ (où v est censé réaliser R(x)), et il renvoie alors ⟨x,v⟩ (censé réaliser ∃x.R(x)). Le principe de Markov est donc réalisable… à condition qu'on y croie, justement (parce qu'on a utilisé le principe de Markov dans ce qu'on vient de dire, pour conclure que la boucle infinie termine ; i.e., j'ai démontré que MP est réalisable en utilisant MP, alors que pour ECT₀ je n'avais utilisé que l'arithmétique de Heyting pour montrer sa réalisabilité).

Tout ceci étant dit, on a les résultats suivants, qui éclaircissent considérablement la manière dont la réalisabilité est axiomatisable :

Théorème (Dragalin & Troelstra indépendamment pour l'essentiel) : en notant HA pour l'arithmétique de Heyting, et ECT₀ (thèse de Church-Turing étendue) et MP (principe de Markov) les axiomes explicités ci-dessus, et enfin par Σ⊢P l'affirmation P est démontrable (est un théorème) dans la théorie Σ, on a :

HA ⊢ (φ ⇔ ∃n.(n⊪φ)) pour φ une formule presque négative quelconque, i.e., c'est un théorème de l'arithmétique de Heyting HA qu'une formule φ presque négative est vraie si et seulement si elle est réalisable ; ceci vaut encore pour une formule presque négative existentiellement quantifiée (i.e. de la forme ∃x.ψ(x) avec ψ(x) presque négative) ;
or, quelle que soit φ, la formule n⊪φ est (démontrablement équivalente dans HA à une formule) presque négative ; donc :
(Nelson) la réalisabilité est idempotente, c'est-à-dire que ∃m.(m⊪∃n.(n⊪φ))) équivaut (démontrablement dans HA) à ∃n.(n⊪φ) ;
HA+ECT₀ ⊢ (φ ⇔ ∃n.(n⊪φ)) pour φ une formule quelconque, i.e., c'est un théorème de HA+ECT₀ qu'une formule φ est vraie si et seulement si elle est réalisable ;
(HA+ECT₀ ⊢ φ) ⇔ (HA ⊢ ∃n.(n⊪φ)) pour φ une formule quelconque, i.e., φ est démontrablement réalisable dans HA si et seulement si elle est démontrable dans HA+ECT₀ ; par ailleurs, si c'est le cas, le n peut être explicité, c'est-à-dire que c'est encore équivalent à ∃n.(HA⊢(n⊪φ)) (ceci est un fait général concernant l'arithmétique de Heyting : HA ⊢ ∃n.ψ(n) si et seulement si ∃n.(HA⊢ψ(n))) ;
la même chose vaut encore en ajoutant MP : (HA+ECT₀+MP ⊢ φ) ⇔ (HA+MP ⊢ ∃n.(n⊪φ)) pour φ une formule quelconque, i.e., φ est démontrablement réalisable dans HA+MP si et seulement si elle est démontrable dans HA+ECT₀+MP ; de nouveau, si c'est le cas, le n peut être explicité, c'est-à-dire que c'est encore équivalent à ∃n.(HA+MP⊢(n⊪φ)) ;
(Jeřabek) (HA+ECT₀+MP+SLEM ⊢ φ) ⇔ (PA ⊢ ∃n.(n⊪φ)) pour φ une formule quelconque, où PA est l'arithmétique de Peano, et SLEM le schéma du tiers exclu χ∨¬χ pour tous les énoncés (= formules sans variables libres) χ, i.e., φ est démontrablement réalisable dans l'arithmétique de Peano si et seulement si elle est démontrable dans HA+ECT₀+MP+SLEM.

(On peut aussi signaler les faits suivant : toute formule presque négative est démontrablement dans HA+MP équivalente à une formule négative. Et pour la complétude, on pourrait aussi mentionner que les énoncés comme HA ⊢ φ sont Σ₁, et notamment presque négatifs, donc réalisables si et seulement si ils sont vrais.)

Bon, il y a beaucoup de choses là-dedans, toutes ne sont pas également intéressantes, mais la principale chose à retenir c'est quand même que les formules qui sont démontrablement réalisables sont celles qui sont démontrables à partir de ECT₀ (je résume ainsi un peu approximativement les trois derniers points), donc, en quelque sorte, la réalisabilité nous fournit un univers dans lequel on a ECT₀ (et on a MP si on a MP dans l'univers ambiant).

On commence à toucher ici aux limites de cet outil purement arithmétique qu'est la réalisabilité : pour explorer ce monde parallèle, on a envie de se poser des questions du genre est-ce que toutes les fonctions ℕ→ℕ sont calculables par machine de Turing ?, qui est quand même une question/affirmation plus claire que ce bizarre schéma ECT₀, mais que l'arithmétique ne permet pas de formaliser parce qu'elle ne sait parler que d'entiers naturels, pas de fonctions ℕ→ℕ ni de parties de ℕ.

Même pour se poser des questions sur les principes purement de logique propositionnelle qui sont satisfaits par la réalisabilité (comme je l'avais mentionné ici, (¬(p₁∧p₂) ∧ (¬p₁⇒(q₁∨q₂)) ∧ (¬p₂⇒(q₁∨q₂))) ⇒ ((¬p₁⇒q₁) ∨ (¬p₁⇒q₂) ∨ (¬p₂⇒q₁) ∨ (¬p₂⇒q₂)) et ((¬¬p₁⇔(¬p₂∧¬p₃)) ∧ (¬¬p₂⇔(¬p₃∧¬p₁)) ∧ (¬¬p₃⇔(¬p₁∧¬p₂)) ∧ ((¬p₁⇒(¬p₁∨¬p₃)) ⇒ (¬p₂∨¬p₃)) ∧ ((¬p₂⇒(¬p₂∨¬p₁)) ⇒ (¬p₃∨¬p₁)) ∧ ((¬p₃⇒(¬p₃∨¬p₂)) ⇒ (¬p₁∨¬p₂))) ⇒ (¬p₁ ∨ ¬p₂ ∨ ¬p₃) sont réalisables quelles que soient les formules qu'on met à la place des variables propositionnelles qui apparaissent dans ce que je viens d'écrire) se heurte à la limitation qu'on n'a pas défini la réalisabilité pour de telles formules. On pourrait bricoler quelque chose (on peut dire qu'une formule faisant intervenir des variables propositionnelles est réalisable lorsque, quelle que soit la partie de ℕ substituée à chacune de ses variables propositionnelles, il y a un entier qui la réalise étant entendu que les variables propositionnelles sont réalisées précisément par les entiers qui appartiennent à la partie qu'on leur a substitué), mais ce ne serait pas tellement plus simple que de définir le topos effectif qui donnera un sens à toutes sortes de types d'objets du même coup (entiers naturels, variables propositionnelles = valeurs de vérité, mais aussi fonctions sur les entiers naturels, parties des entiers naturels, nombres réels, parties de la droite réelle, etc.).

Je m'arrête ici, cette entrée est déjà assez longue et probablement trop technique comme ça. Il y aurait évidemment énormément d'autres choses à dire, mais je pense que la façon de continuer est vraiment de définir le topos effectif, et je ne vais pas me lancer dedans maintenant. [Ajout : le billet sur le topos effectif est ici.]