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 pk+qk=nk 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)↦2p(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 queP⇒Q⇒R
se parenthèse implicitement commeP⇒(Q⇒R)
) sont des axiomes quelles que soient les formules P,Q,R, ainsi queP⇒Q⇒P∧Q
,P∧Q⇒P
etP∧Q⇒Q
, et aussiP⇒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 pourP⇒⊥
; - règle de modus ponens : de
P⇒Q
etP
on peut déduireQ
; - 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éduireQ⇒∀x.P(x)
; et deP(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.]