David Madore's WebLog: Sur le topos effectif

Codages et rappels de calculabilité

☞ Codage des couples et des fonctions calculables

Comme dans cette entrée passée, j'ai besoin de deux notions classiques dans le contexte de la calculabilité. D'abord, le fait qu'il est possible de coder de façon calculable des couples d'entiers naturels sous la forme d'entiers naturels, et je noterai ⟨p,q⟩ le code du couple (p,q) (c'est-à-dire que (p,q) ↦ ⟨p,q⟩ est une bijection calculable fixée entre ℕ² et ℕ). Ensuite, le fait qu'il est possible de coder les programmes (machines de Turing, ou toute autre façon de représenter les fonctions calculables partielles ℕ⇢ℕ) par des entiers naturels : pour e,n deux entiers naturels, je noterai e•n (d'autres gens écrivent φ_e(n) ou {e}(n)) le résultat de l'exécution du programme codé par e sur l'entrée n, si ce résultat est bien défini (notamment, si le programme termine en temps fini), i.e., la valeur en n de la e-ième fonction calculable partielle, si définie. J'écrirai e•n↓ pour dire que cette valeur est bien définie. (Il n'y aura pas de risque de confusion avec la multiplication parce que je n'aurai pas besoin de parler de multiplication.)

☞ La notation λ pour les programmes

Inversement, je noterai λm.(truc calculable en m) pour désigner (l'entier codant) un programme (peu importe lequel exactement) qui renvoie le truc calculable question quand on lui passe la valeur m en argument (par exemple, λm.m² désigne un programme prenant m en entrée et renvoyant m², c'est-à-dire une implémentation de la fonction calculable m ↦ m² : on a donc (λm.m²)•n = n² pour tout n). Je n'hésiterai pas à écrire λ⟨p,q⟩.(truc calculable en p et q) si j'ai besoin d'une fonction de deux variables fournies sous forme de couple. Par exemple, l'existence d'une machine de Turing universelle signifie qu'il existe u∈ℕ tel que e•n = u•⟨e,n⟩ pour tous e,n∈ℕ (c'est-à-dire, un programme tel que, quand on lui fournit en entrée un autre programme e et un paramètre n, simule l'exécution de e sur n et renvoie le résultat correspondant, s'il est défini), et on peut noter ce u comme λ⟨e,n⟩.(e•n).

Petite remarque terminologique : je travaille en logique classique (de façon externe, i.e., dans mes définitions ; le topos effectif aura une logique intuitionniste en interne, mais ma description externe est classique), mais j'utiliserai quand même le terme habité pour dire non vide, parce que je trouve qu'il est plus élégant.

Opérations sur 𝒫(ℕ)

Ces préliminaires étant faits, voici maintenant une définition qui n'est pas bien compliquée, mais qui sous-tend toute la construction du topos effectif :

☞ Les opérations ⊓, ⊔ et ⇛ sur 𝒫(ℕ)

Si P et Q sont deux parties de ℕ, j'introduis les notations pour trois autres parties de ℕ :

• P⊓Q l'ensemble des ⟨p,q⟩ pour p∈P et q∈Q, i.e., les codes des couples dont la première composante est dans P et la seconde dans Q (c'est donc juste l'image du produit cartésien P×Q par la fonction codage des couples) ;
• P⊔Q l'ensemble des ⟨0,p⟩ pour p∈P et des ⟨1,q⟩ pour q∈Q, i.e., la réunion disjointe d'une copie {0}⊓P de P et d'une copie {1}⊓Q de Q ;
• P⇛Q l'ensemble des e∈ℕ tels que pour tout p∈P on ait e•p↓∈Q (ceci signifiant que d'une part e•p est défini et d'autre part que l'entier en question appartient à Q), i.e., les codes des programmes qui, si on leur fournit un élément de P en entrée terminent en temps fini et renvoient un élément de Q.

Notons que, telles quelles, ces opérations sur 𝒫(ℕ) ne sont pas très agréables, par exemple les deux premières ne sont même pas associatives — la troisième non plus bien sûr, mais là c'était attendu. Bien sûr, il y a une bijection calculable assez évidente entre P⊓(Q⊓R) et (P⊓Q)⊓R (consistant à envoyer ⟨p,⟨q,r⟩⟩ sur ⟨⟨p,q⟩,r⟩), par exemple, mais ce n'est pas exactement ça qui va nous concerner (je ferai néanmoins la convention que P⊓Q⊓R désigne, disons, (P⊓Q)⊓R pour éviter de multiplier les parenthèses).

(Un peu plus bas, j'utiliserai aussi occasionnellement — en la rappelant — la notation P≡Q pour l'ensemble (P⇛Q)⊓(Q⇛P) des codes de couples formés d'un élément de P⇛Q et d'un élément de Q⇛P. Ce n'est pas idéal parce qu'il s'agit là d'une partie de ℕ et pas d'une relation d'équivalence ; mais Unicode n'a pas de symbole LEFT RIGHT TRIPLE ARROW.)

Intuitivement, si on imagine que P est un ensemble de « témoignages » qu'une certaine affirmation P est vraie, et Q un ensemble de témoignages d'une autre affirmation Q, alors P⊓Q, P⊔Q et P⇛Q correspondent en gros à des « témoignages » des opérations logiques P∧Q (conjonction : « et » logique), P∨Q (disjonction : « ou » logique) et P⇒Q (implication) entre les deux affirmations en question (par exemple, pour témoigner que P∧Q est vrai, j'apporte un témoignage de P et un témoignage de Q, et c'est exactement ce qui définit P⊓Q ; de façon plus subtile, pour témoigner que P⇒Q est vrai, je fournis une façon calculable de transformer un témoignage de P en un témoignage de Q). Cette façon de présenter les choses est inspirée par l'interprétation de Brouwer-Heyting-Kolmogorov de la logique intuitionniste (cf. ce que j'en racontais ici par exemple) : je répète qu'il s'agit d'une explication informelle, mais elle sert à motiver les définitions qui suivent, et j'utiliserai le terme de témoignage pour faire référence à ce type de vision intuitive.

Tel quel, donc, l'ensemble 𝒫(ℕ) des parties de ℕ, muni des opérations ⊓,⊔,⇛ (et ℕ,∅) que je viens de définir, n'a pas une structure très intéressante, même si elle rappelle au moins vaguement les connecteurs logiques ∧,∨,⇒ (auxquels on peut ajouter ⊤,⊥) : en quelque sorte, le principe du topos effectif est de transformer ça en une vraie structure, qui tient lieu de valeurs de vérité.

Il peut être intéressant de se persuader comme exercice préalable que, si φ est une tautologie du calcul propositionnel intuitionniste — voir ici et plus précisément ici pour une explication de ce terme — en plusieurs variables P₁,…,P_r, alors il existe n∈ℕ (dépendant uniquement de φ, mais pas de P₁,…,P_r) tel que, quels que soient les parties P₁,…,P_r de ℕ, si on substitue P₁,…,P_r à P₁,…,P_r, et qu'on remplace en même temps ∧,∨,⇒,⊤,⊥ par ⊓,⊔,⇛,ℕ,∅ respectivement, l'entier n appartienne à la partie ainsi formée. Par exemple, (l'entier codant) le programme λn.n réalisant la fonction identité sera dans P⇛P pour tout P, et de même λp.λq.p sera dans P⇛(Q⇛P) pour tous P,Q. (On peut voir tout ceci comme une version de la correspondance de Curry-Howard si on veut, mais noter que dans ce que je viens de dire il n'y a pas vraiment de typage ni de preuves. [Ajout : je renvoie à ce billet ultérieur pour une explication de la correspondance de Curry-Howard.]) On peut remarquer au passage que la loi de Peirce ((P⇛Q)⇛P)⇛P (qui définit la logique classique), elle, ne correspond pas à une partie habitée par un même n pour tous P,Q (même s'il s'avère qu'elle est effectivement habitée pour tous P,Q, mais ce n'est pas la question), ce qui suggère d'ores et déjà que, si logique il y a, elle sera intuitionniste.

[Ajout : voir ce billet ultérieur sur la réalisabilité propositionnelle pour toutes sortes d'explications sur ces opérations ‘⊓’, ‘⊔’ et ‘⇛’ et leur rapport avec la logique.]

Objets du topos effectif, et assemblées

☞ Objets du topos effectif

Un objet du topos effectif est la donnée d'un ensemble X (parfois appelé le porteur de l'objet), et d'une fonction E:X²→𝒫(ℕ) (parfois appelée la fonction d'égalité-existence) qui à un couple (x,y) d'éléments de X associe un ensemble E(x,y) d'entiers naturels, vérifiant certaines conditions supplémentaires que je vais dire plus bas (l'existence de s et t).

Quelques remarques avant d'énoncer ces conditions supplémentaires. D'abord, ce que j'ai noté E(x,y) est souvent noté ⟦x=y⟧ (j'insiste : c'est une partie de ℕ). Je vais préférer la notation E(x,y) tant que je n'ai pas introduit ⟦φ⟧ en général. Intuitivement il faut sans doute penser aux éléments de E(x,y) comme des témoignages de l'égalité entre x et y et de leur existence respective dans l'objet considéré (et notamment à ceux de E(x,x) comme des témoignages de l'existence de x dans l'objet considéré).

☞ Assemblées

Ensuite, beaucoup d'objets qu'on sera amenés à considérer sont d'un type très particulier (et plus simple à manier), à savoir qu'on a E(x,y) = ∅ dès que x≠y, si bien que ces objets particuliers sont simplement définis par la donnée d'un ensemble E(x,x), généralement juste noté E(x), pour chaque x∈X. On parle d'assemblées pour ces objets particuliers :

Une assemblée est donc la donnée d'un ensemble X, et d'une fonction E:X→𝒫(ℕ) (parfois appelée fonction d'existence), qu'on étend en une fonction X²→𝒫(ℕ) (d'égalité-existence) en posant E(x,x) = E(x), et E(x,y) = ∅ dès que x≠y (on, si on préfère, E(x,y) = {n∈E(x) | x=y} dans tous les cas), ce qui permet de considérer les assemblées comme des objets particuliers du topos effectif. (La condition supplémentaire sur l'existence de s et t expliquée plus bas est automatique pour une assemblée. Par ailleurs, en fait, tout objet du topos effectif sera, en un certain sens, un quotient d'une assemblée.)

Notons, a contrario, que certains auteurs ajoutent à la définition d'un objet du topos effectif la condition que E(x,x) est habité pour tout x, sachant que si E(x,x) = ∅, on aura forcément E(x,y) = ∅ et E(y,x) = ∅ pour tout y, et on pourra retirer de X cet élément x inutile sans rien perdre (cela donnera un objet isomorphe). Je vais essayer d'être agnostique sur cette question, c'est-à-dire que je n'exige pas cette condition, mais je vais quand même essayer de décrire les constructions de certains objets de manière à la préserver.

☞ Conditions sur les objets

Ma définition d'un objet du topos effectif n'était pas complète, et il faut donc que je la termine en énonçant les conditions supplémentaires :

Les conditions pour que (X,E) soit un objet du topos effectif sont les suivantes : il existe des entiers naturels s,t tels que pour tous x,y∈X on ait s ∈ E(x,y)⇛E(y,x) et que pour tous x,y,z∈X on ait t ∈ (E(x,y)⊓E(y,z))⇛E(x,z). Autrement dit, on demande il existe des programmes s,t∈ℕ tels que :

• quels que soient x,y∈X et n ∈ E(x,y) on ait s•n↓ (le programme termine) et s•n ∈ E(y,x),
• quels que soient x,y,z∈X et p ∈ E(x,y) et q ∈ E(y,z) on ait t•⟨p,q⟩↓ (le programme termine) et t•⟨p,q⟩ ∈ E(x,z).

Intuitivement, s est un « témoignage » de la symétrie de l'égalité, et t est un « témoignage » de sa transitivité. Si on fournit à s un témoignage de l'égalité de deux éléments, il vous renvoie un témoignage de l'égalité en sens inverse, et de façon analogue, t prend des témoignages de deux égalités enfilées et renvoie un témoignage de l'égalité des extrêmes.

☞ Dissipation de malentendus possibles

Je souligne bien les faits suivants :

• La donnée de s et t ne fait pas partie de la donnée de l'objet du topos effectif, on demande juste que ces données existent (autrement dit, on demande que ⋂_x,y∈X (E(x,y)⇛E(y,x)) et ⋂_x,y,z∈X ((E(x,y)⊓E(y,z))⇛E(x,x)) soient habités mais on ne fixe pas un élément dedans).
• Les programmes s et t ne prennent pas les éléments x,y,z en entrée (on voit d'ailleurs mal comment ils pourraient : ce sont des éléments d'un ensemble n'ayant pas de codage particulier), juste des éléments de E(x,y) et compagnie (autrement dit, intuitivement, s doit fabriquer un « témoignage » de y=x à partir d'un « témoignage » de x=y, sans avoir x,y eux-mêmes à sa disposition : si l'objet permet de distinguer les éléments individuels, ça ne peut être qu'en prévoyant des témoignages différents pour chacun),
• Il n'y a pas de demande de réflexivité, uniquement de symétrie et transitivité : la raison à ça est que, intuitivement, les éléments de E(x,y) servent à la fois à témoigner que x et y existent (et donc, en fait, à les désigner !) qu'à témoigner de leur égalité, d'où le terme de fonction d'égalité-existence que j'utilise. (En gros, ceci est à rapprocher du fait que, pour définir un quotient d'un sous-ensemble X₀ d'un ensemble X, on peut se contenter de donner une relation d'équivalence sur X₀, ce qui, sur X, se voit comme une relation symétrique et transitive, mais pas forcément réflexive puisque X₀ est justement l'ensemble des x en relation avec eux-mêmes, ou, en fait, en relation avec n'importe quoi, ce qui motive la remarque qui suit.) On remarquera notamment qu'à partir d'un élément n de E(x,y) (pour n'importe quel y) on peut en fabriquer un de E(x,x), à savoir t•⟨n,s•n⟩ (et notamment, si E(x,x) est vide, forcément tous les E(x,y) sont vides : un tel x est alors inutile et peut être omis de X).
• L'existence de s,t (comme dans la définition d'un objet) est automatique pour une assemblée (je rappelle qu'une assemblée est un objet tel que E(x,y) = ∅ dès que x≠y) : pour s on peut prendre λn.n codant la fonction identité, et pour t on peut prendre le programme λ⟨p,q⟩.p renvoyant la première composante d'un couple (ou la seconde, ça n'a pas d'importance). Donc une assemblée est juste la donnée d'un ensemble X et d'une fonction E:X→𝒫(ℕ), sans contrainte supplémentaire.

Quelques exemples d'objets

☞ Exemples d'objets en vrac

Quelques exemples importants d'objets (dont beaucoup, mais pas tous, seront des assemblées) :

• L'ensemble vide, ou objet initial, noté 0 ou ∅, est juste l'objet défini par X=∅ (et E est forcément la fonction vide).
• Le singleton, ou objet terminal, généralement noté 1, est défini par X={●} (singleton, peu importe de quoi), avec E(●,●)=ℕ, disons (on pourrait aussi prendre E(●,●)={0}, ou n'importe quoi d'habité, les objets seraient au final isomorphes). C'est, bien sûr une assemblée (comme l'exemple précédent, d'ailleurs).
• L'objet des naturels, que je noterai N, qui est l'assemblée définie par X=ℕ, avec E(n)={n}, c'est-à-dire E(n,n)={n} et E(m,n)=∅ lorsque m≠n. Cet objet va jouer un rôle extrêmement important dans le topos effectif, et c'est bien lui qui correspond aux entiers naturels « internes » dans un sens que j'expliquerai plus loin.
• On peut définir des objets 2=1⊎1, 3=1⊎1⊎1, soit comme des coproduits (cf. ci-dessous), soit comme les parties évidentes de l'objet des naturels (ces deux approches seront de toute façon isomorphes une fois qu'on aura défini la notion de morphisme). Par exemple, 2 peut être vu comme l'assemblée portée par l'ensemble {0,1} avec E(n)={n} pour n∈{0,1}.
• Si X est un ensemble quelconque, on définit l'objet co-constant de valeur X, noté ∇X, de la façon suivante. Son porteur est X, et c'est une assemblée avec E(x)=ℕ pour tout x∈X, c'est-à-dire E(x,x)=ℕ et E(x,y)=∅ lorsque x≠y. Cela ne change rien (on obtiendra des objets isomorphes) si on remplace ℕ par, disons, {0}, mais le point crucial pour la définition d'un objet co-constant est que ce soit toujours le même ensemble habité. On prendra garde (notamment, si on sait ce qu'est un topos de Grothendieck, ceci est une source possible d'erreur) que les objets 2 (point précédent) et ∇2 sont extrêmement différents.
• Le classificateur de sous-objet ou objet des valeurs de vérité, noté Ω, qui est l'objet défini par X=𝒫(ℕ) (l'ensemble des parties de ℕ), avec E(P,Q) égal à (P⇛Q) ⊓ (Q⇛P). (J'ai dit qu'on pouvait noter ça P≡Q, mais je souligne de nouveau que c'est une partie de ℕ, pas une relation d'équivalence ; je souligne aussi ces « témoignages d'égalité » de P et Q dans Ω sont simplement des données d'un programme transformant un élément de P en un élément de Q et d'un programme transformant un élément de Q en un élément de P, il n'y a pas d'exigence que ce soient des bijections réciproques ou quoi que ce soit de ce genre.) Comme cet objet Ω n'est pas une assemblée, il faut vérifier l'existence de s et t : pour s on peut prendre λ⟨u,v⟩.⟨v,u⟩ (programme qui inverse les deux composantes du codage d'un couple) ; pour t, il faut faire un peu plus d'efforts : quelque chose comme λ⟨⟨u,v⟩,⟨u′,v′⟩⟩.⟨u′∘u,v∘v′⟩ où m∘n désigne la composée λk.(m•(n•k)) (noter que u,v,u′,v′ sont respectivement dans P⇛Q, Q⇛P, Q⇛R et P⇛R dans cette histoire).
• Si (X,E) et (Y,F) sont deux objets du topos effectif, on définit leur produit (X×Y,G) de la façon suivante. Son porteur est le produit X×Y des porteurs des deux objets dont on est parti. La fonction d'égalité-existence G:(X×Y)²→𝒫(ℕ) associe à ((x₁,y₁),(x₂,y₂)) l'ensemble E(x₁,x₂) ⊓ F(y₁,y₂). Il est facile de construire les programmes s et t témoignant la symétrie et la transitivité pour le produit à partir de ceux des deux facteurs : je laisse ça en exercice.
• Si (X,E) et (Y,F) sont deux objets du topos effectif, on définit leur coproduit (X⊎Y,G) de la façon suivante. Son porteur est la réunion disjointe X⊎Y des porteurs des deux objets dont on est parti. La fonction G:(X⊎Y)²→𝒫(ℕ) associe à (z₁,z₂) l'ensemble {0}⊓E(z₁,z₂) (des couples ⟨0,p⟩ avec p∈E(z₁,z₂)) si z₁,z₂ sont tous deux dans X, ou bien l'ensemble {1}⊓F(z₁,z₂) (des couples ⟨1,q⟩ avec q∈F(z₁,z₂)) si z₁,z₂ sont tous deux dans Y, ou enfin ∅ si l'un est dans X et l'autre dans Y. Là aussi, il est facile de construire les témoins de symétrie et de transitivité.
• L'objet des réels, qui est l'assemblée définie de la façon suivante. On appelle suite de Cauchy récursive explicite une suite calculable (r_n) de rationnels tels que |r_n − r_n+1| ≤ 2⁻⁽ⁿ⁺¹⁾ et réel calculable la limite d'une telle suite. L'objet des réels est alors l'assemblée (X,E) où X est l'ensemble des réels calculables et où E(x), pour x un réel calculable, est l'ensemble des entiers naturels codant un programme calculant une suite de Cauchy récursive explicite de limite x, c'est-à-dire l'ensemble des a∈ℕ tels que a•n=⟨p_n,q_n⟩ où (r_n=p_n/q_n) est une suite de Cauchy explicite de limite x. (Je reviendrai plus bas sur la question de pourquoi c'est bien ainsi qu'il faut comprendre les nombres réels dans le topos effectif.)

☞ Le réduit ensembliste

J'ai défini ci-dessus une construction ∇ prenant un ensemble X et fabriquant un objet ∇X du topos effectif. Il est intéressant d'avoir une construction en sens inverse : si (X,E) est un objet du topos effectif, appelons X₀ l'ensemble des éléments « utiles » de X, c'est-à-dire les x tels que E(x,x) soit habité, et définissons une relation ~ sur X₀ par x~y lorsque E(x,y) est habité : cette relation est réflexive (par définition de X₀), symétrique (par l'existence de s) et transitive (par l'existence de t) : on appelle Γ(X,E) le quotient X₀/~ de X₀ par elle, et on l'appelle le réduit ensembliste de (X,E). Pour une assemblée, bien sûr, la relation ~ est triviale (c'est juste l'identité), et le réduit ensembliste est simplement l'ensemble X₀ des éléments utiles de l'assemblée. Mais on peut remarquer, par exemple, que, pour Ω le classificateur de sous-objet défini ci-dessus, Γ(Ω) est simplement l'ensemble à deux éléments formé de la classe de l'ensemble vide et de la classe de n'importe quel ensemble habité.

Une remarque pour les gens qui savent ce que sont les faisceaux et les topos de Grothendieck : la construction Γ que je viens de définir, et qui s'avérera former un foncteur, c'est même le foncteur X ↦ Hom(1,X), peut être considéré comme le foncteur sections globales. Mais une différence cruciale, et qui peut être perturbante si on a l'habitude des topos de Grothendieck, est qu'alors que dans ces derniers le foncteur sections globales Γ a un adjoint à gauche qui est le foncteur faisceau constant, ici le foncteur réduit ensembliste Γ a un adjoint à droite, à savoir le foncteur ∇, et c'est la raison pour laquelle je parle d'objet co-constant pour l'image de ce dernier (le terme constant est plus standard, mais me semble mauvais). En termes plus sophistiqués : alors que les topos de Grothendieck sont munis d'un morphisme géométrique vers le topos des ensembles, ici on a un morphisme géométrique (qui est même un plongement) depuis le topos des ensembles vers le topos effectif.

Relations fonctionnelles et morphismes

Les objets du topos effectif étant définis, il s'agit de définir les morphismes entre eux. Là c'est un petit peu pénible, parce qu'il s'agit de prendre des classes d'équivalences de relations fonctionnelles (mais heureusement il y a des cas importants où la définition se simplifie, et je vais expliquer cette simplification après la définition générale).

☞ Relations fonctionnelles entre objets

Supposons donc donnés (X,E) et (Y,F) sont deux objets du topos effectif. On appelle relation fonctionnelle entre ces deux objets la donnée d'une fonction G:X×Y→𝒫(ℕ) telle qu'il existe des éléments d,r,u,v (entiers naturels, codant des programmes) suivants :

• d ∈ G(x,y)⇛(E(x,x)⊓F(y,y)) quels que soient x∈X et y∈Y, autrement dit, d prend en entrée un élément de G(x,y) et renvoie (le code d')un couple formé d'un élément de E(x,x) et d'un élément de F(y,y),
• r ∈ (E(x,x′)⊓G(x,y)⊓F(y,y′))⇛G(x′,y′) quels que soient x,x′∈X et y,y′∈Y, autrement dit, r prend en entrée (le code d')un triplet formé d'un élément de E(x,x′), de G(x,y) et de F(y,y′), et renvoie un élément de G(x′,y′),
• u ∈ (G(x,y)⊓G(x,y′))⇛F(y,y′) quels que soient x∈X et y,y′∈Y, autrement dit, u prend en entrée (le code d')un couple formé d'un élément de G(x,y) et de G(x,y′), et renvoie un élément de F(y,y′),
• v ∈ E(x,x)⇛⋃_y∈YG(x,y) quel que soit x∈X, autrement dit, v prend en entrée un élément de E(x,x) et renvoie un élément d'un certain G(x,y) (pour un certain y∈Y).

J'insiste sur l'ordre des quantificateurs : on demande l'existence d'un d,r,u,v tel(s) que pour tous les x,y,… quantifiés, on ait les propriétés demandées. C'est-à-dire, si on veut, que d ∈ ⋂_x∈X,y∈Y (G(x,y)⇛(E(x,x)⊓F(y,y))) (l'élément d n'a pas le droit de dépendre de x ni y) et de façon analogue pour les autres.

Intuitivement, les éléments de G(x,y) sont des « témoignages » du fait que la fonction qu'on est en train de définir envoie x sur y (ou plutôt, que (x,y) est dans le graphe) : l'élément d témoigne du fait que le graphe n'est constitué que de couples qui existent bien, l'élément r témoigne du fait qu'il est compatible aux égalités sur X et Y, l'élément u témoigne du fait qu'il s'agit d'un graphe fonctionnel, et l'élément v témoigne du fait qu'il est total.

De nouveau, je souligne d'une part que la donnée de d,r,u,v ne fait pas partie de la donnée de la relation fonctionnelle, on demande juste leur existence, et d'autre part que les différents x et y ne sont pas passés en argument à ces programmes (comment le pourraient-ils ?), pas plus que y n'est renvoyé par v. La relation fonctionnelle est juste la donnée de la fonction G telle que (des) d,r,u,v existent.

☞ Identité et composition des relations fonctionnelles

Pour donner au moins un exemple dès ce stade, pour n'importe quel objet (X,E), la fonction E définit une relation fonctionnelle de l'objet vers lui-même, appelée relation identité. La vérification de l'existence de d,r,u,v est facile : pour d on peut par exemple prendre λn.⟨t•⟨n,s•n⟩,t•⟨s•n,n⟩⟩, par exemple (où λn.truc désigne le programme prenant n en entrée et renvoyant truc, et où s et t sont comme garantis par la définition des objets), vu que comme je l'ai déjà signalé, t•⟨n,s•n⟩ fournit un élément de E(x,x) si n est dans E(x,y) ; l'existence de r et u est de même une application simple de la symétrie et la transitivité (si je ne me suis pas trompé, λ⟨m,n,ℓ⟩.t•⟨s•m,t•⟨n,ℓ⟩⟩ convient pour r, et λ⟨m,n⟩.t•⟨s•m,n⟩ convient pour u) ; quant à v on peut simplement prendre l'identité (je veux dire, λn.n).

Comment compose-t-on les relations fonctionnelles ? Supposons qu'on ait trois objets, (X,E), (Y,F) et (Z,G), et deux relations fonctionnelles H de (X,E) vers (Y,F) et K de (Y,F) vers (Z,G), et on cherche à définir K∘H de (X,E) vers (Z,G). Ce sera simplement (x,z) ↦ ⋃_y∈Y (H(x,y)⊓K(y,z)). (Intuitivement, donc, un « témoignage » du fait que K∘H envoie x sur z est (le code d')un couple formé d'un témoignage du fait que H envoie x sur y et d'un témoignage du fait que K envoie y sur z : de nouveau, je souligne que y n'est pas encodé dans ces témoignages, d'ailleurs comment le pourrait-il.)

☞ Équivalence des relations fonctionnelles, morphismes

Telle quelle, cette composition des relations fonctionnelles n'est pas très agréable (par exemple, composer avec ce que j'ai appelé la relation identité ne redonne pas exactement la relation donnée, et la composition n'est pas associative), mais cela va s'arranger en passant au quotient :

On dit que deux relations fonctionnelles G,G′:X×Y→𝒫(ℕ) entre les mêmes deux objets (X,E) et (Y,F) du topos effectif sont équivalentes lorsqu'il existe un entier naturel ⟨p,q⟩ qui appartienne à (G(x,y)⇛G′(x,y))⊓(G′(x,y)⇛G(x,y)) pour tous x∈X et y∈Y (bref, la relation d'équivalence est : ⋂_x∈X,y∈Y ((G(x,y)⇛G′(x,y))⊓(G′(x,y)⇛G(x,y))) est habité).

Un morphisme (X,E) → (Y,F) dans le topos effectif est alors une classe d'équivalence, pour la relation qu'on vient de définir, de relations fonctionnelles. L'identité et la composition des morphismes est définie par le relation identité et la composition des relations fonctionnelles que j'ai définie précédemment. Il faudrait, bien sûr, vérifier que la composition est compatible avec la relation d'équivalence, et que la composition des morphismes est associative (c'est-à-dire que la composition des relations fonctionnelles est associative à équivalence près) et que l'identité se comporte bien comme l'identité. (Je ne le ferai pas, mais ce n'est pas spécialement difficile, ce sont des exercices assez idiots de passages des témoignages. Par exemple, c'est essentiellement l'existence de l'élément r qui assure que la composition d'un morphisme par l'identité donne bien le morphisme en question.)

Un isomorphisme, bien sûr, est un morphisme (X,E) → (Y,F) entre objets tel qu'il existe un morphisme (Y,F) → (X,E) tel que la composée dans les deux sens fasse l'identité sur l'objet en question. Notons que la définition de la réciproque d'un isomorphisme est très simple sur les relations fonctionnelles : la réciproque de G:X×Y→𝒫(ℕ) et la fonction Y×X→𝒫(ℕ) donnée par (y,x) ↦ G(x,y), et la question de si G définit un isomorphisme s'exprime simplement par le fait que ceci définit bien une relation fonctionnelle (c'est l'existence de u et v qui est en question, celle de d et r étant claire).

L'objet des morphismes (Hom interne) et l'objet des sous-objets

☞ L'objet des morphismes

Pour aller plus loin, si (X,E) et (Y,F) sont deux objets du topos effectif, on définit non seulement un ensemble Hom((X,E), (Y,F)) des morphismes (X,E) → (Y,F) (je viens de le faire : ce sont les relations fonctionnelles modulo équivalence), mais même un objet Hom((X,E), (Y,F)) du topos effectif, qu'on appelle l'objet des morphismes (X,E) → (Y,F) ou Hom interne (ou Hom souligné). Il s'agit de l'objet dont l'ensemble porteur est l'ensemble Z des relations fonctionnelles entre (X,E) et (Y,F), muni de la fonction H:Z²→𝒫(ℕ) définie par :

• H(G,G′) := H_d(G) ⊓ H_r(G) ⊓ H_u(G) ⊓ H_v(G) ⊓ K(G,G′) si G,G′ sont deux fonctions X×Y→𝒫(ℕ), où :
• en s'inspirant de la définition d'une relation fonctionnelle :
  • H_d(G) := ⋂_x∈X,y∈Y (G(x,y)⇛(E(x,x)⊓F(y,y)))
  • H_r(G) := ⋂_{x,x′∈X,y,y′∈Y} ((E(x,x′)⊓G(x,y)⊓F(y,y′))⇛G(x′,y′))
  • H_u(G) := ⋂_{x∈X,y,y′∈Y} ((G(x,y)⊓G(x,y′))⇛F(y,y′))
  • H_v(G) := ⋂_x∈X (E(x,x)⇛⋃_y∈YG(x,y))
  — et de plus, comme dans la définition de l'équivalence des relations fonctionnelles :
• K(G,G′) := ⋂_x∈X,y∈Y ((G(x,y)⇛G′(x,y))⊓(G′(x,y)⇛G(x,y)))

— essayons d'expliquer un peu mieux cette définition. Les ensembles H_d(G), H_r(G), H_u(G), H_v(G) sont les ensembles des d,r,u,v dans la définition d'une relation fonctionnelle, autrement dit, ce sont les ensembles dont la définition d'une relation fonctionnelle garantit qu'ils sont habités (si G est bien une relation fonctionnelle), intuitivement ce sont les témoignages respectifs du fait que le graphe de G est constitué de couples qui existent, compatible à l'égalité, fonctionnel et total. Quant à K(G,G′), il est constitué des témoignages du fait que G et G′ sont équivalents. Noter que j'ai défini H(G,G′) asymétriquement comme H_d(G) ⊓ H_r(G) ⊓ H_u(G) ⊓ H_v(G) ⊓ K(G,G′), mais j'aurais tout aussi bien pu mettre H_d(G) ⊓ H_r(G) ⊓ H_u(G) ⊓ H_v(G) ⊓ H_d(G′) ⊓ H_r(G′) ⊓ H_u(G′) ⊓ H_v(G′) ⊓ K(G,G′), parce qu'à partir d'un élément e de K(G,G′) et d'un élément de n'importe quel H_*(G) on va pouvoir en fabriquer un (et ce, de façon algorithmique !) dans le H_*(G′) correspondant en composant par les éléments de G(x,y)⇛G′(x,y) et G′(x,y)⇛G(x,y) qui nous sont donnés dans e. De toute façon, il faut bien faire ce genre de vérifications pour fabriquer les éléments s et t dont l'existence est exigée pour que Hom((X,E), (Y,F)) soit un objet. Noter aussi que j'aurais pu définir Z comme l'ensemble de toutes les fonctions X×Y→𝒫(ℕ) (pas juste les relations fonctionnelles), puisque si G ou G′ n'est pas une relation fonctionnelle, de toute manière, l'un des ensembles H_*(G) va être vide et du coup H(G,G′) aussi ; mais j'ai promis de construire mes objets en évitant les éléments « inutiles ».

Le rapport entre l'objet Hom((X,E), (Y,F)) que je viens de définir et le « bête » ensemble Hom((X,E), (Y,F)) des morphismes (X,E) → (Y,F), c'est que si je note (Z,H) le premier, alors le second est ce que j'ai appelé plus haut son réduit ensembliste Γ(Z,H), et c'est immédiat d'après les définitions.

☞ Une remarque sur Hom(1,X)

Peut-être que je devrais faire une digression, ne serait-ce que pour dissiper une confusion possible, sur le cas de Hom(1,X) et Hom(1,X), où 1 désigne l'objet singleton (objet terminal que j'ai défini plus haut), lorsque X est un objet du topos effectif. L'objet Singl(X) := Hom(1,X), qu'on peut appeler objet des singletons de X, est isomorphe à l'objet X dont on est parti, mais sa présentation (je veux dire, son ensemble porteur et sa fonction d'égalité-existence) est a priori bien différente, son porteur étant possiblement bien plus gros que celui de X. (Précisément, le porteur de Singl(X,E), tel que je l'ai défini, est l'ensemble X^♯ des fonctions S:X→𝒫(ℕ) (enfin {●}×X→𝒫(ℕ) mais on me permettra de simplifier) tels que ⋂_x∈X (S(x)⇛E(x,x)) et ⋂_x,x′∈X ((S(x)⊓E(x,x′))⇛S(x′)) et ⋂_x,x′∈X ((S(x)⊓S(x′))⇛E(x,x′)) et ⋃_x∈X S(x) soient tous habités. Et la relation fonctionnelle X × X^♯ → 𝒫(ℕ) définissant l'isomorphisme (X,E) → Singl(X,E) est (x,S) ↦ S(x).) Bref, j'insiste sur le fait que cet objet des singletons Singl(X) := Hom(1,X) est, par rapport à X, un objet isomorphe mais présenté différemment : il est généralement sans gravité de les identifier, mais parfois il peut y avoir un intérêt de faire référence à la présentation précise qui est faite ici. Ainsi, il est clair que Hom(1,X) est le réduit ensembliste ΓHom(1,X) de Hom(1,X), mais ce qui n'est pas complètement évident, même si c'est quand même vrai, c'est que c'est aussi celui ΓX de X. Plus bas je vais donner une description différente de Hom(…) et Hom(…), pour certains types particuliers d'objets, dans laquelle Hom(1,X) sera non seulement isomorphe à X mais aura la même présentation : ce n'est pas grave d'avoir deux descriptions de Hom(1,X) si les objets sont de toute façon isomorphes. Néanmoins, la présentation particulière écrite ici peut avoir son intérêt et on peut retenir ce concept d'objet des singletons, et c'est pour ça que j'introduis cette notation Singl(X) pour cette présentation précise.

☞ Les sous-objets et l'objet des sous-objets

Tant qu'à faire, mentionnons aussi l'ensemble des sous-objets et l'objet des sous-objets d'un objet, parce que c'est un peu pareil que l'ensemble des morphismes et l'objet des morphismes, mais en légèrement plus facile parce qu'il n'y a qu'un objet impliqué. Supposons que (X,E) soit un objet du topos effectif. Considérons l'ensemble Z des fonctions P:X→𝒫(ℕ) telles qu'il existe d,r entiers naturels vérifiant d ∈ P(x)⇛E(x,x) quel que soit x∈X, et r ∈ (E(x,x′)⊓P(x))⇛P(x′) quels que soient x,x′∈X (comme dans la définition d'une relation fonctionnelle, mais en plus simple). On appelle ensemble des sous-objets de (X,E) le quotient de Z par la relation d'équivalence K(P,Q) est habité, où K:Z²→𝒫(ℕ) désigne la fonction définie par K(P,Q) := ⋂_x∈X ((P(x)⇛Q(x))⊓(Q(x)⇛P(x))). Quant à l'objet des sous-objets, c'est l'objet dont l'ensemble porteur est Z (ou même l'ensemble de toutes les fonctions X→𝒫(ℕ) si on n'a pas peur d'avoir des éléments inutiles), muni de la fonction H:Z²→𝒫(ℕ) définie par :

• H(P,Q) := H_d(P) ⊓ H_r(P) ⊓ K(P,Q) si P,Q sont deux fonctions X→𝒫(ℕ), où :
• comme ci-dessus :
  • H_d(P) := ⋂_x∈X (P(x)⇛E(x,x))
  • H_r(P) := ⋂_x,x′∈X ((E(x,x′)⊓P(x))⇛P(x′))
  — et de plus, là aussi comme ci-dessus :
• K(P,Q) := ⋂_x∈X ((P(x)⇛Q(x))⊓(Q(x)⇛P(x)))

Un sous-objet de (X,E), défini par P:X→𝒫(ℕ) comme ci-dessus, se voit lui-même comme un objet (X₀,E₀) où X₀ est l'ensemble des x de X tels que P(x) soit habité, et où E₀(x,x′) := P(x) ⊓ E(x,x′), muni d'un morphisme d'inclusion (X₀,E₀) → (X,E) défini par la relation fonctionnelle X×X₀→𝒫(ℕ) donnée par la même formule que E₀. Par ailleurs, on peut vérifier (et ce sera essentiellement le cas numéroté (2) dans l'énumération ci-dessous) que l'ensemble et l'objet des sous-objets de X sont identifiables à l'ensemble Hom(X,Ω) et à l'objet Hom(X,Ω) des morphismes de X vers le classificateur de sous-objet défini plus haut : on parle de fonction indicatrice du sous-objet pour le morphisme X → Ω qui lui correspond. Notons notamment que Ω lui-même s'identifie à l'objet des sous-objets de l'objet singleton.

Image d'un morphisme, quotient d'un objet

☞ Image d'un morphisme

Il est sans doute aussi pertinent de définir la notion d'image d'un morphisme du topos effectif : si (X,E) et (Y,F) sont deux objets et G:X×Y→𝒫(ℕ) une relation fonctionnelle définissant un morphisme entre eux, l'image du morphisme est (Y₀,F₀) où Y₀ est l'ensemble des y∈Y tel qu'il existe un x∈X pour lequel G(x,y) soit habité, et où F₀(y,y′) := F(y,y′) ⊓ ⋃_x∈X G(x,y). Ceci se voit naturellement comme un sous-objet de Y (défini par la fonction Y→𝒫(ℕ) donnée par y ↦ F(y,y) ⊓ ⋃_x∈X G(x,y), disons). Et on a bien sûr la factorisation du morphisme d'origine (X,E) → (Y,F) comme composée du morphisme (X,E) → (Y₀,F₀) évident et du morphisme d'inclusion (Y₀,F₀) → (Y,F) du sous-objet image qu'on vient de définir.

☞ Objet quotient

La notion de quotient par une relation d'équivalence fonctionne aussi assez naturellement : si R est un sous-objet de X², qui est réflexif, symétrique et transitif en tant que relation, c'est-à-dire que X = (X,E) est un objet et que R est représenté par R:X²→𝒫(ℕ) tel qu'il existe des entiers naturels habitant dans ⋂_x,y∈X (E(x,y)⇛R(x,y)) (témoignant que la relation est compatible à l'égalité sur X et, notamment, réflexive), dans ⋂_x,y∈X (R(x,y)⇛R(y,x)) (témoignant que la relation est symétrique) et dans ⋂_x,y,z∈X ((R(x,y)⊓R(y,z))⇛R(x,x)) (témoignant que la relation est transitive), alors on définit un objet X/R qui n'est autre que (X,R), c'est-à-dire le même ensemble porteur X muni de fonction R définissant la relation donnée en tant que relation d'égalité-existence. (Et cette même fonction R définit aussi le morphisme X→(X/R) qu'on peut appeler surjection canonique. Et on peut vérifier que tout morphisme X→Y qui est surjectif au sens où F(y,y)⇛⋃_x∈XG(x,y) est habité avec les notations évidentes/usuelles, décrit Y comme quotient de X par la relation définie par (y,y′) ↦ ⋃_x∈X (G(x,y)⊓G(x,y′)).) Bref, les quotients sont simples à décrire, ou, peut-être plus précisément, ils ont été mis dans la description des objets dès le début. (D'ailleurs, à ce stade, on peut légitimement dire, et facilement vérifier, que tout objet (X,E) du topos effectif est le quotient d'une assemblée, à savoir celle qui est définie par le porteur X et la fonction d'existence x ↦ E(x,x).)

Une remarque sur la représentation des sous-objets

☞ Sous-objets et éléments « qui existent »

Faisons à ce stade une remarque sur la représentation des sous-objets qui est peut-être inutilement technique ou subtile mais qui m'a beaucoup embrouillé donc je pense que c'est quand même la peine de l'expliciter. Commençons par dire les choses informellement. Il y a diverses variations possibles autour de la présentation de l'ensemble ou de l'objet des sous-objets de (X,E). Pour expliquer l'idée, imaginez qu'en théorie des ensembles vous ayez représenté un ensemble comme sous-ensemble X₀ d'un ensemble X : pour représenter un sous-ensemble de X₀, on peut soit préférer l'approche on se donne un sous-ensemble de X qui est inclus dans X₀ (i.e., dont les éléments doivent appartenir à X₀), soit l'approche on se donne un sous-ensemble de X modulo égalité sur X₀ (i.e., en quotientant par la relation d'équivalence avoir les mêmes éléments de X₀) : la seconde approche peut sembler plus compliquée, mais elle ne l'est pas forcément si, de toute manière on va faire intervenir un quotient dans l'histoire. Dans la définition que j'ai donnée ci-dessus d'un sous-objet, j'ai demandé l'existence de d ∈ P(x)⇛E(x,x) qui « témoigne » du fait que tous les éléments que j'ai mis dans le sous-objet « existent vraiment » ; si au lieu de ça je me dis que je vais essentiellement ignorer P(x) lorsque x n'existe pas vraiment (i.e., considérer qu'un témoignage d'appartenance au sous-objet est sans valeur s'il n'est pas accompagné d'un témoignage d'existence de l'élément en question), je vais laisser tomber la demande d'existence de d et, à la place, modifier la définition de H. Bref, j'arrive à ce qui suit :

On peut parfois préférer la présentation suivante de l'objet des sous-objets de (X,E) (la présentation est différente, mais l'objet obtenu sera isomorphe) : on considère l'ensemble Z˜ de toutes les fonctions X→𝒫(ℕ), et on le munit de la fonction d'égalité-existence suivante : H˜(P,Q) := ⋂_x,y∈X (E(x,y) ⇛ ((P(x)⇛Q(y))⊓(Q(y)⇛P(x)))). Il y a deux idées qui jouent pour justifier que c'est « la même chose » que la définition précédente : d'une part on a fusionné ce qui était noté H_r(P) et K(P,Q) ci-dessus, ce qui n'est pas spécialement subtil (on se convainc facilement que H˜(P,Q) ≡ (H_r(P)⊓K(P,Q)) est habité par un entier naturel indépendant de tout), mais pour ce qui est de H_d(P), l'explication est celle faite au paragraphe précédent : au lieu d'exiger que les témoignages d'appartenance au sous-objet portent sur des éléments qui existent vraiment, on ne tient compte que de ceux qui existent vraiment. L'isomorphisme entre les deux représentations est essentiellement obtenue en envoyant Q tel que dans la seconde représentation sur x ↦ E(x,x) ⊓ Q(x) tel que dans la première. (C'est-à-dire que pour obtenir une représentation du sous-objet dans la première représentation on accompagne tout témoignage (élément de Q(x)) d'appartenance au sous-objet d'un témoignage (élément de E(x,x)) du fait que l'élément concerné existe vraiment. Pour être parfaitement précis, l'isomorphisme entre les deux définitions de l'objet de sous-objets est donné par la fonction Z×Z˜→𝒫(ℕ) qui envoie (P,Q) sur H_d(P) ⊓ H˜(P,Q).)

Si on a trouvé confusants les deux paragraphes précédents, on peut retenir ceci : lorsqu'on parle du sous-objet de (X,E) défini par Q:X→𝒫(ℕ), si on a un doute sur la définition employée, il vaut mieux comprendre ça comme celui défini par x ↦ E(x,x) ⊓ Q(x) (au pire, la redondance de E(x,x) ne sera pas grave, mais au mieux cela corrigera une ambiguïté possible sur la définition d'un sous-objet).

En fait, la même double représentation se pose pour les relations fonctionnelles que pour les sous-objets, puisqu'une relation entre X et Y n'est autre qu'un sous-objet de X×Y, mais tout le monde a l'air d'accord pour prendre la représentation stricte (celle qui impose que les couples existent vraiment, donc qui demande l'existence de d) dans la représentation des relations fonctionnelles, alors que ce n'est pas le cas pour les sous-objets. Néanmoins, le fait de convertir une fonction g:X→Y en relation par E(x,x) ⊓ F(g(x),y) dans les circonstances que je vais expliquer dans un instant peut être vu comme un avatar du même phénomène.

Simplification de la représentation des morphismes

Bon, la notion de morphisme dans le topos effectif est fastidieuse parce que ce sont des classes d'équivalence de relations fonctionnelles. Pour certains types d'objets particuliers, on peut simplifier un peu la définition en représentant les morphismes par des (classes de) fonctions entre les ensembles porteurs :

☞ Morphismes définis par des fonctions entre ensembles porteurs

Si (X,E) et (Y,F) sont deux objets du topos effectif, et si g:X→Y est une fonction entre les ensembles porteurs correspondants, on peut espérer définir une relation fonctionnelle G:X×Y→𝒫(ℕ) par G(x,y) := E(x,x) ⊓ F(g(x),y). L'existence de d et u dans la définition d'une relation fonctionnelle est alors automatique (et facile à vérifier) : l'existence de r et v ne l'est pas, mais elles se simplifient à demander l'existence d'un entier naturel (qu'on peut abusivement encore noter r) appartenant à E(x,x′)⇛F(g(x),g(x′)) pour tous x,x′∈X. Lorsque c'est le cas, on peut dire que la relation fonctionnelle G (ou le morphisme qu'elle définit) est portée par la fonction g. Il y a trois cas importants où toute relation fonctionnelle G entre (X,E) et (Y,F) est portée par une fonction X→Y :

1. C'est le cas si E(x,x) est un singleton pour tout x∈X. (En effet, en appelant v l'élément de ⋂_x∈X (E(x,x)⇛⋃_y∈YG(x,y)) dont l'existence est garantie par la définition d'une relation fonctionnelle, si x∈X, et si n est l'élément de E(x,x), supposé unique par hypothèse de ce point, il existe y∈Y tel que v•n soit dans G(x,y), et si on choisit g(x) comme un tel y, il est facile de voir que G est équivalente à la relation portée par g.) Ce cas s'applique notamment lorsque la source est un objet co-constant ∇X sur un ensemble X, c'est-à-dire l'assemblée avec E(x)={0} pour tout x∈X (on peut poser E(x)=ℕ, ça ne change rien parce que ça donne un objet isomorphe, même s'il est alors moins évident que le cas décrit ici s'applique).
2. C'est aussi le cas si (Y,F) est le classificateur de sous-objet Ω ou, plus généralement, un objet des sous-objets. (Traitons pour simplifier les notations le cas de Ω = (𝒫(ℕ), K) où K(P,Q) := (P⇛Q)⊓(Q⇛P), qu'il sera plus commode de noter P≡Q (attention ceci est une partie de ℕ). On se donne une relation fonctionnelle G:X×𝒫(ℕ)→𝒫(ℕ), et soient d,r,u,v dont l'existence est garantie par la définition des relations fonctionnelles. On définit g:X→𝒫(ℕ) par g(x):=G(x,ℕ). Donné x∈X, si n∈E(x,x), on sait que v•n ∈ G(x,P) pour un certain P∈𝒫(ℕ). Le point crucial est de trouver, de façon calculable en n, un élément dans P≡g(x). Or à partir de r on construit aisément un élément dans (P≡Q)⇛G(x,Q) pour tout Q, à savoir quelque chose comme λm.(r•⟨n,v•n,m⟩), et à partir de u un élément dans G(x,Q)⇛(P≡Q) pour tout Q, quelque chose comme λm.u•⟨v•n,m⟩ ; maintenant, le couple de deux choses que je viens de décrire nous fournit un élément dans (P≡Q)≡G(x,Q) pour tout Q, et notamment dans (P≡ℕ)≡g(x) ; mais par ailleurs il est facile de trouver un élément dans P≡(P≡ℕ) pour tout P, quelque chose comme ⟨λm.⟨λi.0,λj.m⟩,λ⟨k,ℓ⟩.(ℓ•0)⟩, ce n'est pas bien passionnant, et de « composer » ces choses pour fabriquer à partir des éléments de éléments trouvés dans P≡(P≡ℕ) et dans (P≡ℕ)≡g(x) un élément de P≡g(x) comme annoncé. On vérifie alors que G est équivalente à la relation portée par g car on a essentiellement trouvé un élément dans (E(x)⊓(g(x)≡Q)) ≡ G(x,Q) pour tous x∈X et Q∈𝒫(ℕ).)
3. C'est encore le cas si F(y,y′)=∅ quand y≠y′, c'est-à-dire lorsque la cible est une assemblée, si tant est qu'on a supprimé de X les éléments inutiles c'est-à-dire ceux pour lesquels E(x,x)=∅. (En effet, dans ce cas, on vérifie facilement grâce au u et au v de la définition d'une relation fonctionnelle que toute relation fonctionnelle G:X×Y→𝒫(ℕ) doit avoir G(x,y) habité pour exactement un y∈Y, et on peut appeler g(x) l'élément en question.)

Dans ces trois cas, la relation d'équivalence entre fonctions se simplifie aussi : on a g≈g′ lorsqu'il existe un entier naturel e qui appartienne à E(x,x)⇛F(g(x),g′(x)) pour tout x∈X, et les morphismes (X,E) → (Y,F) sont donc (dans les trois cas qu'on vient de décrire) les quotients des fonctions g:X→Y pour lesquelles il existe un même élément r appartenant à E(x,x′)⇛F(g(x),g(x′)) pour tous x,x′, par la relation que je viens de dire.

☞ Objet des morphismes simplifié

De plus, la simplification porte non seulement sur l'ensemble Hom((X,E), (Y,F)) des morphismes (X,E) → (Y,F) mais aussi sur l'objet Hom((X,E), (Y,F)) du topos effectif que j'ai défini plus haut : dans chacun des trois cas que j'ai énumérés, on peut le décrire comme l'objet dont l'ensemble porteur est l'ensemble Z des fonctions X→Y (telles qu'il existe r comme dit plus haut, mais de toute façon son existence sera imposée dans les faits), muni de la fonction H:Z²→𝒫(ℕ) définie par :

• H(g,g′) := H_r(g) ⊓ K(g,g′) si g,g′ sont deux fonctions X→Y, où :
• come ci-dessus :
  • H_r(g) := ⋂_x,x′∈X (E(x,x′)⇛F(g(x),g(x′)))
  — et de plus, là aussi comme ci-dessus :
• K(g,g′) := ⋂_x∈X (E(x,x)⇛F(g(x),g′(x)))

Mais on peut préférer la version plus concise suivante (qui lui est équivalente) : H˜(g,g′) := ⋂_x,x′∈X (E(x,x)⇛F(g(x),g′(x′))).

Si on se rappelle la notation Singl(Y) que j'ai introduite ci-dessus pour l'objet des singletons de Y, c'est-à-dire pour une présentation bien particulière (le Hom(1,Y) avec la description originale de Hom) d'un objet qui s'avère, en fait, être isomorphe à Y, il peut être intéressant de noter que Singl(Y) (essentiellement parce qu'il est un sous-objet de l'objet des sous-objets de Y) tombe sous le coup du deuxième cas de mon énumération. Ceci permet de décrire les morphismes X→Y, qui sont les mêmes que les morphismes X→Singl(Y) puisque les objets sont isomorphes, comme des fonctions du porteur X de X vers le porteur Y^♯ de Y. Je ne suis pas franchement persuadé que ce soit plus simple que la présentation originale des morphismes, mais c'est une présentation alternative possible, et c'est celle qui est proposée dans l'article de Bernardet & Lengrand, A simple presentation of the effective topos (ici sur l'arXiv) que j'ai évoquée tout au début. (Ils notent El(Y) ce que je note Singl(Y).)

☞ Morphismes vers une assemblée et entre assemblées

Le cas (3) énuméré ci-dessus est encore plus sympathique : si (Y,F) est une assemblée, et si tant est qu'on a supprimé de X les éléments inutiles c'est-à-dire ceux pour lesquels E(x,x)=∅, non seulement un morphisme (X,E) → (Y,F) est défini par une application g:X→Y, mais il n'y a pas non plus à quotienter : la relation d'équivalence devient triviale. Les morphismes (X,E) → (Y,F) dont la cible est une assemblée et dont la source est telle que E(x,x) soit habité pour tout x sont donc juste donnés par les fonctions g:X→Y pour lesquelles E(x,x′) habité implique g(x)=g(x′) et de puis il existe un même élément r appartenant à E(x,x′)⇛F(g(x)) pour tous x,x′. Quant à Hom((X,E), (Y,F)), il est lui-même une assemblée, avec pour porteur l'ensemble des fonctions g comme on vient de dire, et la fonction d'existence H_r(g) := ⋂_x,x′∈X (E(x,x′)⇛F(g(x))).

Et pour simplifier encore un peu les choses si à la fois (X,E) et (Y,F) sont deux assemblées (toujours si tant est qu'on a supprimé de X les éléments inutiles c'est-à-dire que E(x) est habité pour tout x), les morphismes (X,E) → (Y,F) sont alors les fonctions g:X→Y telles qu'il existe un même élément appartenant à E(x)⇛F(g(x)) pour tout x. Quant à Hom((X,E), (Y,F)), il est une assemblée avec pour porteur l'ensemble des fonctions g comme on vient de dire, et la fonction H_r(g) := ⋂_x∈X (E(x)⇛F(g(x))). Ce cas est très important car énormément d'objets intéressant du topos effectif sont des assemblées.

Quelques exemples de morphismes

☞ Exemples de morphismes en vrac

Je peux maintenant donner (dans un ordre sans doute pas idéal) quelques exemples plus ou moins intéressants de morphismes dans le topos effectif :

• Si N désigne l'objet des naturels, c'est-à-dire l'assemblée dont le porteur est ℕ avec E(n)={n}, les morphismes N→N s'identifient aux fonctions g:ℕ→ℕ pour lesquelles il existe un élément v appartenant à {n}⇛{g(n)} pour tout n, c'est-à-dire que v•n = g(n). Autrement dit, il s'agit exactement des fonctions g:ℕ→ℕ calculables. (Ceci ne montre pas encore que dans le topos effectif, toute fonction des entiers naturels vers les entiers naturels est calculable, parce qu'il faut vérifier — et commencer par expliquer ce que ça veut dire ! — que N correspond vraiment aux entiers naturels et que par ailleurs la notion de calculabilité interne coïncide bien avec la notion de calculabilité externe. Mais c'est néanmoins vrai, et le point que je viens de dire est central.)
• En particulier, parmi les morphismes N→N, on mentionnera la fonction successeur, définie comme on se l'imagine par la fonction g(n)=n+1. On peut aussi mentionner les fonction addition et multiplication N²→N, où N² est le produit de l'objet des naturels avec lui-même, c'est-à-dire l'assemblée porté par ℕ² avec comme fonction d'existence G:ℕ²→𝒫(ℕ) la fonction (m,n) ↦ {⟨m,n⟩}. On peut d'ailleurs aussi donner comme exemple de morphisme la fonction de codage des paires elle-même, qui définit un isomorphisme N²→N. Plus généralement, on peut considérer les morphismes N^k→N (où k est un entier naturel), et ils s'identifient avec les fonctions calculables ℕ^k→ℕ.
• Non seulement l'ensemble Hom(N,N) des morphismes N→N correspond à l'ensemble des fonctions calculables ℕ→ℕ, mais l'objet Hom(N,N) est l'assemblée portée par l'ensemble de telles fonctions, et où la fonction d'existence H(g), si g est une telle fonction, est l'ensemble des (codes des) programmes qui implémentent la fonction g. (Et on a l'énoncé analogue évident pour Hom(N^k,N).)
• Les morphismes N→2, où 2 désigne l'objet 1⊎1, ou, ce qui revient au même, l'assemblée portée par {0,1} avec E(n)={n}, sont, de même qu'au point précédent, identifiables aux fonctions calculables ℕ→{0,1}, i.e., aux parties décidables de ℕ. En revanche, les morphismes N→∇2, où ∇2 désigne l'objet co-constant porté par {0,1}, c'est-à-dire l'assemblée sur {0,1} avec E(n)=ℕ (ou {0}, ça ne change rien), cette fois, sont toutes les fonctions ℕ→{0,1}, parce que la condition devient triviale (on peut prendre λm.0 pour v). Ceci montre que 2 et ∇2 sont vraiment différents ; dans le même genre, on peut vérifier qu'il y a quatre morphismes 2→∇2, mais les seuls morphismes ∇2→2 sont les constants.
• Les morphismes 1→Ω correspondent aux parties de ℕ modulo la relation d'équivalence qui identifie P et Q lorsque (P⇛Q) ⊓ (Q⇛P) est habité. Mais en fait c'est facile de voir que toutes les parties habitées sont équivalentes pour cette relation, donc il n'y a que deux morphismes 1→Ω, celui décrit par la partie vide (qu'on peut appeler le faux) et celui décrit par n'importe quelle partie habitée (qu'on peut appeler le vrai). De même, il n'y a que quatre morphismes 2→Ω, huit morphismes 3→Ω, etc. Du coup, on pourrait s'imaginer que Ω est plus ou moins la même chose que 2, mais il n'en est rien !
• Les morphismes N→Ω correspondent aux fonctions ℕ→𝒫(ℕ) (qu'on peut aussi voir comme des parties de ℕ², si on préfère) : il n'y a pas de contrainte sur la fonction, en revanche on quotiente par la relation qui identifie deux fonctions P,Q : ℕ→𝒫(ℕ) lorsqu'il existe e qui appartienne à {n} ⇛ ((P(n)⇛Q(n)) ⊓ (Q(n)⇛P(n))) pour tout n, c'est-à-dire, plus concrètement, un programme qui prend en entrée n et renvoie (le code d')un couple formé d'un élément de (P(n)⇛Q(n)) et d'un élément de (Q(n)⇛P(n)). À titre d'exemple, le problème de l'arrêt, ou plus exactement P(⟨e,n⟩) := {m} où m une trace d'exécution de e•n si cette valeur est définie, et ∅ sinon, définit un morphisme N→Ω (ou, si on veut, un sous-objet de N) qui n'est pas un morphisme N→2 (i.e., qui ne se factorise pas par 2→Ω).
• Un morphisme ∇2→Ω (où ∇2 désigne l'objet co-constant porté par {0,1}) correspondent aux couples (P₀,P₁) de parties de ℕ modulo la relation d'équivalence qui identifie (P₀,P₁) et (Q₀,Q₁) lorsque (P₀≡Q₀) ∩ (P₁≡Q₁) (noter le symbole intersection au milieu) est habité, où (P≡Q) désigne la partie (P⇛Q) ⊓ (Q⇛P). Ceci est à distinguer des morphismes 2→Ω (où 2 désigne l'objet 1⊎1, cf. ci-dessus) qui correspondent aux couples (P₀,P₁) de parties de ℕ modulo la relation d'équivalence qui identifie (P₀,P₁) et (Q₀,Q₁) lorsque (P₀≡Q₀) ⊓ (P₁≡Q₁) (noter cette fois le symbole ‘⊓’ au milieu) est habité. Bref, dans le cas des morphismes 2→Ω, la relation d'équivalence se donne le droit de témoigner l'équivalence de P₀ et Q₀ de manière différente de celle de P₁ et Q₁, et comme on l'a fait remarquer plus haut, du coup, il y a exactement quatre morphismes 2→Ω (selon que chacune des parties (P₀,P₁) est habitée ou non), alors que dans le cas des morphismes ∇2→Ω, la relation d'équivalence impose un même témoignage pour l'équivalence de P₀ et Q₀ et celle de P₁ et Q₁. On peut vouloir traiter l'exercice consistant à identifier la fonction indicatrice du sous-objet 2→∇2 en tant que morphisme ∇2→Ω (réponse : c'est le couple ({0},{1}), cf. la remarque après ces exemples), ou la fonction indicatrice du sous-objet de Ω défini par ce morphisme-là ; un autre exercice consisterait à montrer qu'il y a une infinité non dénombrable de morphismes ∇2→Ω (enfin, je crois…).
• Tant qu'à faire, on a un morphisme Ω→∇2 intéressant, représenté par la fonction envoyant ∅ ∈ 𝒫(ℕ) sur 0 ∈ {0,1} et toute autre partie sur 1.
• Mentionnons quelques morphismes Ω²→Ω importants : la conjonction (qu'on peut noter ‘∧’ ou ‘⊓’, je ne sais pas ce qui est le plus logique à ce stade) est définie par la fonction 𝒫(ℕ)²→𝒫(ℕ) que nous avons notée ⊓, la disjonction (notée ‘∨’ ou ‘⊔’) par la fonction (⊔):𝒫(ℕ)²→𝒫(ℕ), et l'implication (notée ‘⇒’ ou ‘⇛’) par la fonction (⇛):𝒫(ℕ)²→𝒫(ℕ). (Pour vérifier que ★ définit bien un morphisme Ω²→Ω, où ‘★’ désigne l'un de ‘⊓’,‘⊔’,‘⇛’, il s'agit essentiellement de vérifier que ((P₁≡P₂)⊓(Q₁≡Q₂))⇛((P₁★Q₁)≡(P₂★Q₂)) est habité par un même entier pour tous P₁,P₂,Q₁,Q₂, où comme d'habitude U≡V désigne (U⇛V)⊓(U⇛V) qui tient lieu de fonction d'égalité-existence sur Ω. Dans les trois cas c'est facile.)
• Si (X,E) et (Y,F) sont deux objets du topos effectif, on a défini leur produit (X×Y,G) au moyen de la fonction G:(X×Y)²→𝒫(ℕ) donnée par ((x₁,y₁),(x₂,y₂)) ↦ E(x₁,x₂) ⊓ F(y₁,y₂). On considère les deux relations fonctionnelles Π_x:(X×Y)×X→𝒫(ℕ) et Π_y:(X×Y)×Y→𝒫(ℕ) données par ((x,y),z) ↦ E(x,z) et ((x,y),z) ↦ F(y,z), et celles-ci définissent deux morphismes π_x : (X×Y,G) → (X,E) et π_y : (X×Y,G) → (Y,F) qu'on peut appeler la première projection et la seconde projection.
• On a dit que Hom(N,N) était décrit par l'assemblée portée par l'ensemble Tot des fonctions calculables ℕ→ℕ, et où la fonction d'existence H:Tot→𝒫(ℕ) associe à une telle fonction l'ensemble H(g) des (codes des) programmes qui l'implémentent. On peut alors considérer les morphismes Hom(N,N) → N : ce sont les fonctions F:Tot→ℕ calculables, c'est-à-dire telles qu'il existe un élément r dans H(g)⇛{F(g)} pour tout g∈Tot, autrement dit, il doit y avoir un programme qui calcule F(g) à partir d'un (quelconque !) programme implémentant g (soit : r•e = F(g) pour tout e tel que e•n=g(n) pour tout n). Un résultat important de calculabilité, le théorème de Kreisel-Lacombe-Shoenfield (voir ce fil Twitter et celui-ci qui le cite pour plus d'explications et des références) affirme qu'une telle fonction F ne peut faire que calculer un nombre fini de valeurs de g (et donc ne dépendre que de ce nombre fini de valeurs ; de plus, ce nombre est calculable en fonction des codes des programmes calculant F et g) : si on veut, ce sont les fonctions F calculables par une machine de Turing à oracle à qui on fournit g comme oracle. Quant à Hom(Hom(N,N),N), c'est l'assemblée portée par l'ensemble des fonctions Tot→ℕ calculables, avec une fonction d'existence qui à F associe l'ensemble des codes des r qui l'implémentent ou, si on préfère, des codes des machines de Turing à oracle qui calculent F(g) en fonction d'un oracle donnant g.

☞ Quelques remarques sur 2 → ∇2 → Ω

(Cette suite de remarques est sans doute mal placée, elle est probablement plus claire si on a lu la partie sur la réalisabilité avant, mais comme elle fait vraiment suite aux exemples qui précèdent, je ne sais pas où la mettre.)

Il est intéressant de prendre le temps de bien comprendre les trois objets 2 (le coproduit 1⊎1), ∇2 (l'objet co-constant) et Ω (le classificateur de sous-objet) et la manière dont ils s'imbriquent, c'est-à-dire les morphismes 2→∇2→Ω qui font de 2 et ∇2 des sous-objets de Ω, le premier étant lui-même un sous-objet du second. Le morphisme 2→∇2 dont je parle est celui porté par la fonction qui envoie 0 sur 0 et 1 sur 1, tandis que le morphisme ∇2→Ω (ou la composée 2→Ω) est celui porté par la fonction qui envoie 0 sur ∅ et 1 sur ℕ (ou sur {0}, c'est équivalent). Mais on peut aussi considérer les fonctions indicatrices ∇2→Ω de 2→∇2, et Ω→Ω de ∇2→Ω ou de 2→Ω : la première (la fonction indicatrice ∇2→Ω de 2→∇2) est portée par la fonction envoyant 0 sur {0} et 1 sur {1} ; la deuxième (la fonction indicatrice Ω→Ω de ∇2→Ω) est portée par la fonction qui à P associe (P≡∅)∪(P≡ℕ) (noter le symbole union ‘∪’ ici), tandis que la troisième (la fonction indicatrice Ω→Ω de 2→Ω) est portée par la fonction qui à P associe (P≡∅)⊔(P≡ℕ). Mais on peut préférer la fonction équivalente ((P⇛∅)⇛∅)⇛P pour la deuxième (ce sont les programmes qui, si P est habité, doivent renvoyer un élément de celui-ci quand on les applique à un élément quelconque), et (P⇛∅)⊔P pour la troisième : ceci nous permet d'identifier ∇2 à {p∈Ω | (¬¬p)⇒p} (les valeurs de vérité régulière) avec la notation {⋯} qui sera introduite plus bas, et 2 à {p∈Ω | (¬p)∨p}.

Cette différence entre 2, ∇2 et Ω se voit aussi sur l'ensemble des morphismes de N vers l'un des trois : on a affaire à trois sortes de sous-objets de N : comme on l'a dit ci-dessus, les morphismes N→2 sont en bijection avec les parties décidables de ℕ, les morphismes N→∇2 avec les parties quelconques de ℕ, et les morphismes N→Ω avec les fonctions ℕ→𝒫(ℕ) en identifiant P,Q : ℕ→𝒫(ℕ) lorsqu'il existe e qui appartienne à ⋂_n∈ℕ ({n} ⇛ (P(n)≡Q(n))) (et on identifie une partie E de ℕ, vue comme un morphisme N→∇2, avec le morphisme N→Ω qui à n associe ℕ si n∈E et ∅ si n∉E). J'ai mentionné plus haut le problème de l'arrêt, à savoir le morphisme N→Ω (ou le sous-objet de N) défini par P(⟨e,n⟩) := {m} où m une trace d'exécution de e•n si cette valeur est définie, et ∅ sinon : ce n'est pas complètement évident (c'est essentiellement le principe de Markov dont je parlerai plus loin), mais ce morphisme est équivalent à celui défini par Q(⟨e,n⟩) := ℕ si e•n↓, et ∅ sinon (en effet, un élément de Q(⟨e,n⟩) ⇛ P(⟨e,n⟩) est obtenu en simulant l'exécution de e sur n jusqu'à ce qu'elle termine, ce qui va bien être le cas puisqu'on nous a donné un élément de Q(⟨e,n⟩) qui l'assure) : ce point montre que le morphisme N→Ω se factorise par ∇2, i.e., le sous-objet de N ainsi défini correspond bien au problème de l'arrêt classique (la partie {⟨e,n⟩ | e•n↓} de ℕ). Néanmoins, on peut trouver des morphismes N→Ω qui ne se factorisent vraiment pas par ∇2, par exemple en associant à ⟨e,n⟩∈ℕ la partie {1} si e•n↓ et {0} sinon : en tant que sous-objet de N il s'agit de la réunion du problème de l'arrêt qu'on vient de définir et du complémentaire de ce dernier — classiquement, cette réunion donne juste ℕ, mais dans le topos effectif, on a affaire à un sous-objet de N qui ne se factorise même pas par ∇2.

(Néanmoins, il existe une rétraction naturelle de l'inclusion ∇2→Ω, à savoir le morphisme Ω→∇2 qui envoie ∅ sur 0 et toute partie habitée sur 1 : la composée Ω→∇2→Ω est l'application « non non », qui envoie P sur (P⇛∅)⇛∅. Donc en particulier, à tout sous-objet de N donné par sa fonction indicatrice N→Ω on peut associer une partie de ℕ correspondant à composer la fonction indicatrice avec le Ω→∇2 en question ; mais il y a une perte d'information dans l'histoire.)

Définition de la réalisabilité

Supposons que φ soit une formule logique (c'est-à-dire formée à partir des connecteurs logiques ‘∧’, ‘∨’, ‘⇒’, ‘⊤’, ‘⊥’ et des quantificateurs ‘∀’, ‘∃’) dans laquelle chaque variable (libre ou quantifiée) est typée par un objet du topos effectif (i.e., on lui a associé un tel objet, appelé le « type » de la variable), et supposons de plus que pour toute variable libre t de type X dans φ on se soit donné un élément x de l'ensemble porteur de X (qu'on dira substitué à la variable, et on notera abusivement φ(x) l'association en question)[#3]. On définit alors une partie ⟦φ⟧ de ℕ, qu'on appelle entiers naturels réalisant φ ou réalisateurs de φ (intuitivement, les « témoignages » de la véracité de φ, mais qu'on peut aussi considérer comme une sorte de valeur de vérité de φ), par induction sur la complexité de φ de la façon énumérée ci-dessous. On notera aussi n ⊪ φ pour dire n ∈ ⟦φ⟧, c'est-à-dire n réalise φ.

[#3] Pour dire les choses de façon plus précise (mais pas forcément plus claire ?), si φ(t₁,…,t_k) est une formule ayant des variables libres t₁,…,t_k de types respectifs X₁,…,X_k et si x₁,…,x_k sont des éléments des ensembles X₁,…,X_k porteurs de X₁,…,X_k, on définit une partie ⟦φ(x₁,…,x_k)⟧ de ℕ (ou, si on préfère voir les choses comme ça, on définit une fonction ⟦φ(t₁,…,t_k)⟧ : X₁×⋯×X_k→𝒫(ℕ)) par la définition inductive qui suit.

☞ Définition inductive de ⟦φ⟧

La définition de ⟦φ⟧ est la suivante :

• ⟦φ∧ψ⟧ = ⟦φ⟧ ⊓ ⟦ψ⟧ : 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 ;
• ⟦φ∨ψ⟧ = ⟦φ⟧ ⊔ ⟦ψ⟧ : 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 ;
• ⟦φ⇒ψ⟧ = ⟦φ⟧ ⇛ ⟦ψ⟧ : autrement dit, les entiers naturels qui réalisent une implication sont ceux qui codent un programme 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 ;
• ⟦⊤⟧ = ℕ : autrement dit, tout entier réalise le vrai ;
• ⟦⊥⟧ = ∅ : autrement dit, aucun entier ne réalise le faux ;
• ⟦∀t∈X. φ(t)⟧ = ⋂_x∈X (E(x,x)⇛⟦φ(x)⟧) si φ(t) est une formule ayant une variable libre t de type X := (X,E) : autrement dit, les entiers naturels qui réalisent une quantification universelle sont ceux qui codent un programme qui, quand on lui fournit en entrée un entier k d'un E(x,x) quelconque, termine en temps fini et renvoie un entier réalisant l'instance φ(x) en question de la formule dans laquelle on a substitué ce x pour la variable universellement quantifiée t ;
• ⟦∃t∈X. φ(t)⟧ = ⋃_x∈X (E(x,x)⊓⟦φ(x)⟧) si φ(t) est une formule ayant une variable libre t de type X := (X,E) : autrement dit, les entiers naturels qui réalisent une quantification existentielle sont ceux qui codent un couple dont le premier membre appartient à E(x,x) pour un certain x et dont le second membre réalise l'instance φ(x) en question de la formule dans laquelle on a substitué ce x pour la variable existentiellement quantifiée t.

☞ Réalisabilité des formules atomiques

Bon, telle quelle la définition n'est pas complète, parce que je n'ai pas décrit les formules atomiques, et j'ai été assez évasif sur ce qu'elles étaient. Voici quelques cas possibles :

• ⟦x=x′⟧ = E(x,x′) si ‘=’ désigne ici la relation d'égalité entre deux variables dont le type est un même objet (X,E), et si x,x′ sont deux éléments de l'ensemble X (porteur de cet objet) substitués à ces deux variables (l'égalité n'est admise qu'entre deux variables de même type) ;
• ⟦y=g(x)⟧ = G(x,y) si g est un symbole de constante introduit pour désigner un morphisme fixé (X,E) → (Y,F) représenté par une relation fonctionnelle G:X×Y→𝒫(ℕ) et si x,y sont des éléments des ensembles porteurs X,Y substitués aux variables de types respectifs (X,E), (Y,F) ; la même définition ⟦y=g(x)⟧ = G(x,y) vaut aussi si g est cette fois substitué à une variable de type Hom((X,E), (Y,F)) (c'est-à-dire qu'on peut considérer u=f(t) comme une relation de trois variables, t de type X, u de type Y, et f de type Hom(X,Y)) ;
• ⟦x∈P⟧ = P(x) si x∈X et P:X→𝒫(ℕ) sont substitués respectivement à une variable de type (X,E) et une variable de type l'objet des sous-objets de (X,E).

On devrait sans doute aussi introduire une règle (assez évidente, quoique possiblement cryptique) permettant de transformer en formule logique une variable de type Ω : ⟦P⟧ = P si P∈𝒫(ℕ) est substitué à une variable de type Ω. (On peut considérer que c'est un cas particulier du dernier point en considérant Ω comme l'objet des sous-objets du singleton.)

Inversement, si φ(t) est une formule ayant une variable libre x de type X := (X,E), on définit un sous-objet de X, noté {t∈X | φ(t)}, représenté par la fonction X→𝒫(ℕ) donnée par x↦⟦φ(x)⟧ (c'est-à-dire plutôt x↦E(x,x)⊓⟦φ(x)⟧ pour les raisons que j'ai expliquées plus haut), qu'on peut aussi voir comme sa fonction indicatrice, qui est un morphisme X → Ω (je ne sais pas bien comment le noter, mais je suppose que x↦⟦φ(x)⟧ est le plus logique).

Je devrais peut-être ajouter la précision que partout où j'ai noté t∈X certains préfèrent — et c'est arguäblement plus soigneux — noter quelque chose comme t:X, parce que c'est vrai que t est une variable de type X, pas un élément de X (lequel est un objet du topos effectif, pas un ensemble). Mais bon, ce genre d'abus de notations est quand même très courant, il est justifié dès lors qu'on prétend voir le topos comme un monde ensembliste, et je ne pense pas qu'il puisse causer des confusions sérieuses.

‣ On dit que φ est réalisable, ou simplement qu'elle est vraie dans le topos effectif, ou que le topos effectif vérifie φ, lorsque ⟦φ⟧ est habitée, c'est-à-dire lorsqu'il existe un n tel que n ⊪ φ (je l'ai dit plus haut mais je le répète : un tel n est appelé un réalisateur de φ, même si je préfère penser à un « témoignage »).

Si on a lu mon billet précédent sur le sujet de la réalisabilité, il faut savoir que la réalisabilité que je viens de définir pour le topos effectif généralise celle que j'avais définie dans ce billet, plus exactement cette dernière revient exactement au cas où toutes les variables ont le type type N (i.e., où on se restreint à la logique du premier ordre sur les entiers naturels). Mais l'intérêt du topos effectif est qu'on peut parler de bien d'autres choses que des entiers naturels.

Quelques faits réalisés dans le topos effectif

☞ Réalisabilité et logique

La réalisabilité est compatible avec les règles de la logique intuitionniste (plus exactement, la logique intuitionniste d'ordre supérieur, mais je n'ai pas vraiment envie de définir ce que c'est précisément), c'est-à-dire que si ψ découle de φ et que φ est réalisable, alors ψ l'est. (Dans le cas purement propositionnel, c'est-à-dire si toutes les variables ont pour type Ω, c'est l'exercice que j'avais proposé juste après avoir introduit les notations ⊓,⊔,⇛.) Lorsqu'on applique ces règles, on dit qu'on effectue un raisonnement interne dans (en l'occurrence) le topos effectif.

[Ajout : encore une fois, je renvoie à ce billet ultérieur pour beaucoup plus d'explications sur la réalisabilité propositionnelle, et notamment des exemples de formules purement propositionnelles qui sont réalisables, i.e. valables dans le topos effectif, sans pour autant être démontrables en calcul propositionnel intuitionniste.]

☞ Réalisabilité et arithmétique (récurrence)

En outre, le topos effectif vérifie les axiomes de Peano pour N, c'est-à-dire un certain nombre de choses évidentes mais surtout le principe de récurrence :

• ∀p∈Ω^N. ((p(0) ∧ ∀n∈N.(p(n)⇒p(n+1))) ⇒ ∀n∈N.(p(n)))

— où j'ai noté N pour l'objet des naturels, et Ω^N pour Hom(N,Ω).

Comme ceci fournira un bon exemple du fonctionnement de la réalisabilité, essayons d'expliquer un peu précisément pourquoi la formule écrite ci-dessus est bien réalisable (et de voir à quoi ressemble un entier qui la réalise). D'après la définition de ⟦∀⋯⟧, on doit trouver un élément qui appartient à E(p,p)⇛⟦⋯⟧ pour tout p dans l'ensemble porteur de Hom(N,Ω). En fait, ici, l'élément de E(p,p) fourni ne nous apportera aucune information utile, donc on va l'ignorer. Il s'agit donc de trouver un (même) élément ρ qui réalise (p(0) ∧ ∀n∈N.(p(n)⇒p(n+1))) ⇒ ∀n∈N.(p(n)) pour tout p:ℕ→𝒫(ℕ). Ce programme ρ va prendre en entrée le codage d'un couple formé d'un élément de p(0) (enfin, de ⟦p(0)⟧, mais comme je l'ai écrit ci-dessus, pour une variable de type Ω on se permet d'omettre ces parenthèses) et d'un élément de ⟦∀n∈N.(p(n)⇒p(n+1))⟧, et on doit en retour en fournir un de ⟦∀n∈N.(p(n))⟧. Bon, maintenant, ⟦∀n∈N.(p(n))⟧ = ⋂_n∈ℕ ({n}⇛p(n)) (en notant quelque peu abusivement ‘n’ à la fois pour la variable dans la formule et pour l'entier naturel qu'on lui substitue ; le {n} là-dedans vient de la fonction d'existence sur l'assemblée N). Ici {n} nous apporte une information cruciale sur l'élément passé en argument, à savoir, sa valeur. Bref, on cherche à fabriquer un programme qui va prendre en argument un élément n et qui va renvoyer un élément de p(n) (mais je rappelle qu'on n'a aucun accès à p). Comme on nous a fourni en entrée un élément de p(0) et une fonction qui, donnée un n, renvoie un élément de p(n)⇒p(n+1), il suffit d'itérer cette dernière n fois sur le premier. Autrement dit, le programme ρ prend en entrée ⟨z,γ⟩ (avec z∈p(0) et γ∈⟦∀n∈N.(p(n)⇒p(n+1))⟧) et renvoie un programme qui prend en entrée n et effectue une boule, pour k allant de 0 à n−1, de remplacer z par (γ•k)•z (ce qui fournit un élément de p(k+1)) et finalement renvoie le z en question (qui est dans p(n)).

Bon, tout ça était un peu fastidieux à dire, mais l'idée est que pour réaliser le principe de récurrence, on utilise une fonction qui récurre, ce qui est à la fois heureux (et conforme à l'idée qu'on peut se faire de la correspondance de Curry-Howard) et finalement assez facile. En fait, pour dire que N est bien l'objet des entiers naturels dans le topos effectif, il y a une formulation un peu plus catégorique (pour laquelle je renvoie à ici et là).

Je devrais peut-être, en revanche, insister sur le fait que, si on sait ce que ça veut dire, N n'est pas le coproduit d'un nombre dénombrable de copies de 1 (d'ailleurs, ce dernier n'existe même pas dans le topos effectif) : un tel hypothétique objet X aurait la propriété que se donner un morphisme X→Y revient à se donner une infinité dénombrable de morphismes 1→Y, et ce n'est certainement pas le cas qu'un morphisme N→N revient à se donner une infinité dénombrable de morphismes 1→N, parce que le premier décrit une fonction calculable ℕ→ℕ alors que le second correspond à une fonction quelconque ℕ→ℕ.

Bref, le topos effectif vérifie non seulement les énoncés de pure logique mais aussi ceux de l'arithmétique intuitionniste (précisément, l'arithmétique de Heyting d'ordre supérieur, mais je n'ai pas vraiment envie de rentrer dans les détails ; disons de façon vague, les choses qui sont démontrables à partir des axiomes de Peano dans le cadre de la logique intuitionniste).

☞ Principe de Markov

Mais le topos effectif vérifie des énoncés qui ne sont pas de la pure logique intuitionniste ni même des conséquences logiques des axiomes de Peano (et qui ne sont pas valables dans n'importe quel topos). Par exemple, l'énoncé suivant, appelé principe de Markov (le fils Andrej Markov, pas son père du même nom et qui est connu pour les chaînes de Markov), bien qu'il ne soit pas démontrable en pure logique intuitionniste à partir des axiomes de Peano, est réalisable, et fournira un autre exemple intéressant pour montrer comment fonctionne la réalisabilité :

• ∀p∈Ω^N. (((∀n∈N. (p(n)∨¬p(n))) ∧ ¬¬∃n∈N.(p(n))) ⇒ ∃n∈N.(p(n)))

— où de nouveau j'ai noté N pour l'objet des naturels, et Ω^N pour Hom(N,Ω). En français, le principe de Markov affirme que si on a une propriété p des entiers naturels et que cette propriété est décidable (c'est-à-dire que pour tout n la propriété est vraie ou fausse), et s'il est impossible que la propriété soit fausse pour tout n (noter que ¬¬∃n.p(n) est logiquement équivalent à ¬∀n.¬p(n), donc on peut préférer la lire comme ça), alors il y a un n pour laquelle elle est vraie. L'argument intuitif justifiant le principe de Markov dans un monde de type « calculabilité » est qu'on peut tester successivement si p(0) est vrai, puis p(1), puis p(2) et ainsi de suite, en continuant tant que c'est faux : la décidabilité de p(n) nous permet de faire chaque test, et l'hypothèse qu'il est impossible que la propriété soit fausse pour tout n assure que le processus va finir par terminer, auquel cas on aura trouvé un n vérifiant p(n). Maintenant expliquons comment transformer cet argument intuitif en une preuve de la réalisabilité du principe de Markov dans le topos effectif :

D'après la définition de ⟦∀⋯⟧, on doit trouver un élément qui appartient à E(p,p)⇛⟦⋯⟧ pour tout p dans l'ensemble porteur de Hom(N,Ω). Comme précédemment, l'élément de E(p,p) fourni ne nous apportera aucune information utile, donc on va l'ignorer. Il s'agit donc de trouver un (même) élément μ qui réalise ((∀n∈N. (p(n)∨¬p(n))) ∧ ¬¬∃n∈N.(p(n))) ⇒ ∃n∈N.(p(n)) pour tout p:ℕ→𝒫(ℕ). Ce programme μ va prendre en entrée le codage d'un couple formé d'un élément de ⟦∀n∈N. (p(n)∨¬p(n))⟧ et d'un élément de ⟦¬¬∃n∈N.(p(n))⟧, et on doit en retour en fournir un de ⟦∃n∈N.(p(n))⟧. Le premier argument est un programme qui, donné n∈ℕ, renvoie un élément de ⟦(p(n)∨¬p(n))⟧ = ⟦p(n)⟧ ⊔ ⟦¬p(n)⟧, c'est-à-dire, concrètement, qu'il nous fournit soit un élément de p(n), soit l'assurance qu'il n'en existe pas (rappelons que ⟦¬p(n)⟧ = ⟦(p(n))⇒⊥⟧ est simplement ℕ si p(n) est vide, et ∅ si p(n) est habité, donc un élément de ce truc est une assurance que p(n) est vide). Le second argument fourni à notre μ n'est pas intéressant à utiliser, seule son existence est utile : c'est une assurance que ⟦∃n∈N.(p(n)))⟧ est habité (mais sans nous en donner d'élément, i.e. de vrai témoignage : ça c'est justement ce que notre programme doit faire). Le programme μ fonctionne ainsi : il fait une boule infinie pour n parcourant les entiers naturels et, pour chacun, utilise le premier argument fourni pour soit obtenir un élément de p(n) soit l'assurance qu'il n'y en a pas. Dès qu'il trouve un n et un élément de p(n), il renvoie le( codage du couple formé de)s deux comme élément de ⟦∃n∈N.(p(n))⟧ = ⋃_n∈ℕ {n}⊓(p(n)). Le programme ainsi décrit termine toujours en temps fini, car chaque itération de la boucle termine et que la boucle elle-même termine puisqu'on a l'assurance que ⟦∃n∈N.(p(n)))⟧ est habité. Bref, on a décrit comment réaliser le principe de Markov.

(Et de façon appropriée, le programme que je viens de décrire pour réaliser le principe de Markov, que j'ai appelé ‘μ’ pour Markov, coïncide essentiellement avec l'opérateur μ de Kleene, c'est-à-dire l'opérateur de recherche non bornée, celui qui permet de faire des boucles infinies comme on vient de le décrire : l'assurance que la boucle va un jour terminer suffit à trouver de façon calculable le point où la boucle finit, voilà essentiellement ce que dit le principe de Markov ou l'existence de l'opérateur μ de Kleene, et c'est un des principes fondamentaux de la calculabilité à la Church-Turing.)

☞ Choix dénombrable pour les naturels

Au rayon des principes vérifiés par le topos effectif, cela vaut aussi la peine de mentionner l'axiome du choix dénombrable pour les naturels, c'est-à-dire l'énoncé suivant :

• ∀p∈Ω^N×N. ((∀m∈N.∃n∈N.p(m,n)) ⇒ (∃u∈N^N.∀m∈N.p(m,u(m))))

La réalisabilité de ce principe est presque triviale : quel que soit p (et sans demander quoi que ce soit à son sujet ni en dépendre), il s'agit de transformer de façon calculable un entier réalisant ∀m∈N.∃n∈N.p(m,n) en un autre réalisant ∃u∈N^N.∀m∈N.p(m,u(m)). Or le premier, appliqué à un m∈ℕ renvoie un n∈ℕ et un entier réalisant p(m,n) : à des transformations essentiellement triviales près, c'est justement ce qu'on voulait. c'est-à-dire un programme calculant une fonction u:ℕ→ℕ qui, quand on lui fournit un m∈ℕ renvoie un entier réalisant p(m,u(m)).

☞ Thèse de Church-Turing et principe de continuité de Brouwer

Je n'ai pas le temps ni la patience de décrire en détails d'autres principes vérifiés par le topos effectif, mais il y en a au moins deux que je dois évoquer parce qu'ils sont particulièrement célèbres et justifient au moins une partie de l'intérêt porté à ce topos précis :

• La thèse de Church-Turing (interne) : ∀f∈N^N. ∃e∈N. ∀n∈N. ∃m∈N. (T(e,n,m) ∧ U(m)=f(n)), où T,U sont le prédicat T de Kleene et la fonction de décodage correspondante, c'est-à-dire en gros que T(e,n,m) signifie le programme e termine sur l'entrée n et m en est une trace d'exécution et U(m) est la valeur de retour du programme, si bien que l'existence de m tel que T(e,n,m) ∧ U(m)=v signifie exactement que e•n↓ et e•n=v, si bien que le principe dit ∀f∈N^N. ∃e∈N. ∀n∈N. (e•n↓=f(n)), mais l'intérêt technique de T,U est qu'on peut les exprimer de façon tout à fait explicite en arithmétique (comme des fonctions primitives récursives si on sait ce que ça veut dire) et donc on obtient une formule de l'arithmétique (d'ailleurs du premier ordre à part pour le ∀f∈N^N initial), ce qui permet d'appliquer mes définitions générales de la réalisabilité. Bref, la thèse de Church-Turing interne affirme que, de façon interne dans le topos effectif, toutes les fonctions des entiers naturels vers les entiers naturels sont calculables au sens de Church-Turing. Et un programme qui réalise ça est donné, essentiellement, par une machine de Turing universelle : le programme va prendre un témoignage d'existence de f, dont on a déjà expliqué dans la description de Hom(N,N) que c'était le code d'un programme implémentant f et le renvoyer lui-même pour témoigner de l'existence de e, ainsi qu'un programme qui prend n en entrée, qui simule l'exécution de e sur n, et qui renvoie la trace d'exécution m de cette simulation.

• Le principe de continuité de Brouwer (pour les fonctions de N^N vers N) : ∀F∈N^(NN). ∀u∈N^N. ∃n∈N. ∀v∈N^N. (u↾n=u↾n ⇒ F(u)=F(v)) où u↾n=u↾n signifie ∀k<n. (u(k)=v(k)). Autrement dit, toute fonction F de N^N vers N est continue en tout point u au sens où il existe un n tel que si v coïncide avec u sur ses n premières valeurs alors elle a la même image par F. Le point-clé ici est que F de type N^(NN) (c'est-à-dire Hom(Hom(N,N),N)) va être témoigné par le code d'un programme qui l'implémente, et qui ne peut dépendre que d'un nombre fini de valeurs de u (cf. mes remarques plus haut au sujet de Hom(Hom(N,N),N)), et pour calculer n on va utiliser la partie effective du théorème de Kreisel-Lacombe-Shoenfield évoqué plus haut pour avoir une borne calculable sur le nombre de valeurs de u dont l'exécution de F(u) dépend.

Remarques sur le point de vue interne

☞ Travailler comme sur des ensembles (intuitionnistes)

Notons que le topos effectif (et en fait, n'importe quel topos, mais comme je n'ai pas défini ce concept je ne peux parler que du topos effectif) permet de donner un sens non seulement à des énoncés, comme ci-dessus, portant sur les entiers, les prédicats sur les entiers, les suites d'entiers, les fonctions sur les suites d'entiers, etc., mais aussi aux constructions ensemblistes élémentaires habituelles : par exemple, j'ai expliqué ci-dessus que pour φ une formule logique en une variable libre de type X on peut définir un sous-objet {x∈X | φ(x)} d'un objet X (à travers la fonction X→𝒫(ℕ) donnée par x↦⟦φ(x)⟧), qu'on peut voir soit comme un morphisme X→Ω (sa fonction indicatrice, essentiellement une réécriture de φ) soit comme un morphisme X₀→X (cf. les explications plus haut sur la notion de sous-objet). On dispose donc des constructions ensemblistes usuelles : produit cartésien, union disjointe, partie définie par une formule, ensemble des parties (à travers l'objet des sous-objets). Les isomorphismes X→Y coïncident avec les morphismes qui sont naïvement bijectifs (au sens où ∀y∈Y. ∃!x∈X. (f(x)=y) avec la définition usuelle de ‘∃!’). Les morphismes X→Y s'identifient sans problème aux sous-objets de X×Y dont la projection sur la première coordonnée est un isomorphisme (i.e., une bijection), bref, la théorie des ensembles élémentaire (en gros, tant qu'on ne commence pas à utiliser l'axiome du Remplacement et tant qu'on ne tient pas à l'identité des ensembles mais seulement à ce qui vaut à bijection près), tant qu'elle est formulée en logique intuitionniste, s'applique sans surprise dans le topos effectif (et en fait dans n'importe quel topos, c'est essentiellement le principe d'un topos).

☞ Raisonnements internes vs. raisonnements externes

Ceci signifie que pour démontrer une propriété dans le topos effectif (et en fait, mutatis mutandis, dans n'importe quel topos), on a souvent deux moyens : soit on effectue un raisonnement « externe », classique, portant sur les objets et morphismes du topos vus comme des objets mathématiques classiques (donc par exemple les objets du topos effectif sont des couples (X,E) comme on l'a déjà dit, yada yada) ; soit on effectue un raisonnement « interne », c'est-à-dire qu'on applique les règles de raisonnement à l'intérieur du topos, auquel cas les objets du topos se présentent comme des ensembles et les morphismes du topos comme des applications, et il faut utiliser la logique intuitionniste. Le raisonnement interne est souvent plus facile (même s'il requiert d'utiliser la logique intuitionniste, donc d'être familier avec elle) parce que c'est plus facile de manipuler un ensemble qu'une donnée compliquée comme un couple (X,E) muni de témoins de symétrie et de transitivité ; cependant, parfois, le raisonnement interne n'est pas possible, car le topos vérifie des propriétés qui ne découlent pas de pure logique (ou alors il faut partir d'axiomes comme le principe de Markov, mais même comme ça, il me semble qu'on ignore si le topos effectif est axiomatisable à partir d'un nombre fini d'axiomes ; en tout cas, moi, je l'ignore). Bien sûr, parfois le raisonnement interne et le raisonnement externe vont se correspondre assez bien, et on a tendance à commettre des abus de langage, qui risquent d'être source de confusion quand on n'a pas l'habitude, mais qui sont quand même bien pratiques, en ne disant pas très clairement à quel niveau on se place, ou en passant un peu légèrement de l'un à l'autre.

Quoi qu'il en soit, c'est cette possibilité de raisonner « en interne » qui justifie qu'on utilise librement des termes comme fonction (ou application) et partie (ou sous-ensemble), voire ensemble, pour les morphismes et sous-objets et objets respectivement, ce qui serait certainement abusif dans une catégorie générale, mais se défend tout à fait dans un topos (au moins si on décide de le regarder sous le point de vue « interne », parce qu'en interne ce sont des fonctions, parties et ensembles).

Les nombres réels (de Cauchy et de Dedekind)

☞ Réels de Cauchy

Une fois qu'on dispose du vocabulaire standard de la théorie des ensembles, on peut mener des constructions comme celle des nombres réels. Une fois défini l'objet des rationnels Q, qui ne pose aucune difficulté particulière (disons qu'on choisit un codage calculable de ℚ par ℕ et on définit Q comme N avec les opérations transportées de façon évidentes), on cherche à construire les nombres réels. De façon générale, dans un topos (enfin, dans un « topos avec entiers naturels »), même si je ne chercherai pas à définir ce que c'est, on peut définir l'objet des réels de Dedekind et l'objet des réels de Cauchy, ou plus exactement les différentes saveurs de réels de Cauchy (parce qu'il y a plein de subtilités à leur sujet), ainsi nommés parce qu'ils imitent les deux grandes constructions classiques des nombres réels par les coupures de Dedekind et par les suites de Cauchy : alors que dans la théorie des ensembles classique, les constructions de Dedekind et de Cauchy coïncident, dans un topos général, les réels de Cauchy sont une partie des réels de Dedekind (et les réels de Cauchy eux-mêmes définissent différents ensembles inclus les uns dans les autres, les plus restrictifs étant ce que j'appelle ci-dessous les réels de Cauchy explicites et que d'autres appellent réguliers) ; néanmoins, dans le topos effectif (de même que dans la théorie des ensembles classique, mais pour des raisons, si j'ose dire, différentes), il se trouve que ces différentes constructions donnent la même chose : les réels de Cauchy et les réels de Dedekind du topos effectif sont la même chose (enfin, sont isomorphes), et il n'y a pas non plus de différence entre les différentes sortes de réels de Cauchy. Je peux essayer d'expliquer un petit peu pourquoi.

L'objet des réels de Cauchy explicites est défini comme le quotient de l'ensemble des suites de Cauchy explicites dans Q, c'est-à-dire les éléments (r_n) de Q^N tels que ∀n∈N. |r_n−r_n+1|≤2⁻⁽ⁿ⁺¹⁾, par la relation d'équivalence la différence explicitement tend vers 0, c'est-à-dire (r_n)~(r′_n) lorsque ∀n∈N. |r_n−r′_n|≤2⁻⁽ⁿ⁻¹⁾ (si au lieu de mettre une borne explicite comme je l'ai fait ici on mettait un ∀k∈N. ∃m∈N. ∀n≥m. |r_n−r_n+1|≤2^−k et de façon analogue dans la relation d'équivalence, on obtiendrait les réels de Cauchy tout court, mais encore une fois dans le topos effectif il se trouve que ça ne changera rien).

Explicitement décrit, l'objet qu'on obtient ainsi est celui que j'ai déjà évoqué plus haut : on peut le voir comme l'assemblée dont le porteur est l'ensemble des réels calculables, avec comme fonction d'existence la fonction qui à un réel calculable associe l'ensemble de tous les codes de programmes calculant une suite de Cauchy récursive explicite de limite le réel en question : c'est plus ou moins un reflet fidèle de la définition que je viens de donner (à ceci près qu'on fait porter l'objet par l'ensemble des réels calculables, pour obtenir une assemblée, au lieu de l'ensemble des suites de Cauchy récursives explicites de rationnels quitte à ce que de toute façon la fonction d'égalité-existence ne dépende que de la limite).

☞ Réels de Dedekind

L'objet des réels de Dedekind, lui, est défini comme l'ensemble des couples (S,T) de parties de Q telles que :

1. S et T sont habités : ∃r∈Q.(r∈S) et ∃r∈Q.(r∈T) ;
2. S est un ensemble inférieur (c'est-à-dire qu'il contient tout rationnel plus petit qu'un de ses éléments) et T est un ensemble supérieur (c'est-à-dire qu'il contient tout rationnel plus grand qu'un de ses éléments) : ∀r∈Q.∀r′∈Q.(r′<r ⇒ r∈S ⇒ r′∈S) et ∀r∈Q.∀r′∈Q.(r′>r ⇒ r∈T ⇒ r′∈T) ;
3. S est ouvert au sens où il contient un élément plus grand que n'importe quel élément donné, et T est ouvert au sens où il contient un un élément plus petit que n'importe quel élément donné : ∀r∈Q.(r∈S ⇒ ∃r′∈Q.(r′>r ∧ r′∈S)) et ∀r∈Q.(r∈T ⇒ ∃r′∈Q.(r′<r ∧ r′∈T)) ;
4. tout élément de S est strictement plus petit que tout élément de T : soit ∀s∈Q.∀t∈Q.((s∈S ∧ t∈T) ⇒ (s<t)) ;
5. si un rationnel est strictement plus petit qu'un autre, alors soit le plus petit est dans S, soit le plus grand est dans T : soit ∀s∈Q.∀t∈Q.((s<t) ⇒ (s∈S ∨ t∈T)).

(En plus clair, l'objet des réels de Dedekind est le sous-objet du produit cartésien de l'objet des sous-objets de Q avec lui-même défini par la conjonction des formules ci-dessus sur le couple (S,T). Cette définition est valable dans n'importe quel topos.)

Il faut bien sûr comprendre S comme l'ensemble des rationnels strictement plus petits que le réel qu'on cherche à définir, et T comme l'ensemble des rationnels strictement plus grands (c'est exactement ce qu'ils sont en interne). La donnée est, d'ailleurs, redondante, et chacun de S et de T détermine l'autre, mais il est plus agréable de se donner les deux car c'est plus symétrique.

☞ Équivalence des réels de Cauchy et de Dedekind

Comme je l'ai suggéré plus haut, il se trouve que dans le topos effectif (mais pas dans un topos plus général), ces deux notions, réels de Dedekind et réels de Cauchy explicites, donnent le même objet R. Esquissons un argument de pourquoi. Donné un réel de Cauchy explicite, représenté par une suite (r_n) (calculable, de Cauchy explicite), on lui associe une coupure de Dedekind (S,T) en définissant S comme {s∈Q | ∃n∈N. (s < r_n−2⁻ⁿ)} de façon interne, c'est-à-dire, de façon externe, par la fonction ℚ→𝒫(ℕ) qui à s associe {n∈ℕ | s < r_n−2⁻ⁿ}, et T de façon analogue comme {t∈Q | ∃n∈N. (t > r_n+2⁻ⁿ)}. Toutes les propriétés des coupures de Dedekind sont alors claires (la moins évidente est la (e) : donnés s,t tels que s<t, on trouve un n tel que t−s > 2⁻⁽ⁿ⁻¹⁾, et alors on a soit s < r_n−2⁻ⁿ soit t > r_n+2⁻ⁿ : ce raisonnement peut être tenu de façon interne ou de façon externe comme on préfère : de façon interne, il est d'ailleurs valable dans n'importe quel topos, tandis que de façon externe ce que je viens de dire nous donne essentiellement un réalisateur de (e)). Réciproquement, donné un réel de Dedekind (S,T), on obtient un réel de Cauchy explicite essentiellement en utilisant essentiellement les propriétés (a) et (e) pour montrer que pour tout n il existe s de S et t de T tels que t−s ≤ 2⁻ⁿ (tout ceci étant dit en interne). En effet, d'après (a) on peut trouver un rationnel dans S et un rationnel dans T, quitte à les écarter un peu (par (b)) on peut supposer qu'ils sont distincts de 2^−k pour un certain k entier relatif, on coupe l'intervalle en question en 2^n−k+1 intervalles de même longueur, et pour chacun, (e) permet de conclure que soit la borne de gauche est dans S (et alors, par (b), tous les précédents le sont aussi) soit celle de droite est dans T (et alors, par (b), tous les suivants le sont aussi), ce qui, collectivement, nous permet de dire que parmi les 2^n−k+1+1 rationnels formant les extrémités des intervalles, disons u₀,…,u_2^n−k+1 (régulièrement espacés de 2⁻⁽ⁿ⁺¹⁾), il y a un 0<ℓ<2^n−k+1 tel que tous les u_i pour i<ℓ soient dans S et tous les u_i pour i>ℓ soient dans T (et on ne dit rien sur u_ℓ) : alors u_ℓ−1 et u_ℓ+1 sont dans S et T respectivement, et sont distants de 2⁻ⁿ. (Tout ce raisonnement était fait en interne, mais en externe cela va revenir à dire qu'on peut algorithmiquement trouver ces deux éléments à partir de n et de réalisateurs des diverses propriétés des réels de Dedekind.) On peut alors choisir un s_n et un t_n comme je viens de dire (en interne, ceci utilise l'axiome du choix dénombrable pour les naturels — enfin, pour les rationnels, mais ça revient au même —, axiome que j'ai décrit plus haut ; en externe, c'est à peu près évident car l'axiome en question est à peu près évident dans le topos effectif), et la suite (s_n+1), disons, est une suite de Cauchy explicite, et d'ailleurs strictement croissante, qui tend vers le réel de Dedekind donné.

☞ Autres remarques sur les réels

L'addition ou la soustraction sur les réels de Cauchy s'obtient, comme on l'imagine, en ajoutant ou en soustrayant les suites terme à terme, en décalant d'un cran pour avoir l'inégalité explicite demandée. Pour la multiplication il faut travailler un tout petit peu plus pour obtenir la bonne borne explicite, mais bon, il n'est pas très difficile de fabriquer une approximation à 2⁻ⁿ près de x⁢y si on s'est donné des façons d'en fabriquer une à 2⁻ⁿ près de x et y séparément. La comparaison peut présenter des subtilités dans un topos général, mais ici il n'y en a guère, essentiellement grâce au principe de Markov : les réels strictement positifs sont ceux représentés par les suites (r_n) de Cauchy explicites telles qu'il existe un n avec r_n > 2⁻ⁿ (et symétriquement pour les négatifs), et les réels positifs au sens large par les suites telles que pour tout n on ait r_n ≥ 2⁻ⁿ (et symétriquement pour les négatifs). Un réel est alors positif au sens large si et seulement si il n'est pas strictement négatif (ceci est vrai dans n'importe quel topos), mais aussi, il est strictement positif si et seulement si il n'est pas négatif au sens large (ceci n'est pas général, et est essentiellement une conséquence du principe de Markov permettant de passer de ¬¬∃n∈N. r_n > 2⁻ⁿ à ∃n∈N. r_n > 2⁻ⁿ) ; ces affirmations valent bien sûr aussi bien en échangeant positif et négatif.

On peut ensuite se poser toutes sortes de questions d'analyse élémentaire sur cet objet R des réels dans le topos effectif. Par exemple, de même qu'on avait un principe de continuité de Brouwer pour les fonctions N^N → N, on en a un pour les fonctions R→R, toutes les fonctions réelles sont continues, à savoir ∀F∈R^R. ∀u∈R. ∀m∈N. ∃n∈N. ∀v∈R. (|u−v|<1/n ⇒ |F(u)−F(v)|<1/m) — c'est-à-dire que dans le topos effectif toute fonction réelle est continue (l'idée intuitive étant essentiellement la même que pour les fonctions N^N → N : si on arrive à calculer F(u) à partir de u, on doit bien pouvoir le faire à partir d'une approximation de celui-ci). Néanmoins, je ne veux pas trop rentrer dans toutes ces questions car il faudrait en dire plus sur les réels en maths intuitionniste, ce que je prévois de faire dans un autre billet. Disons juste que l'analyse dans le cadre du topos effectif est essentiellement l'analyse constructive de l'école russe dont le Andrej Markov est le principal représentant.

Quelques sortes d'objets particuliers

(Cette courte section n'a pas vraiment de raison de se trouver ici, mais je n'ai pas vraiment de meilleur idée d'endroit où la mettre.)

☞ Objets discrets et modestes

Attention, cependant, si le topos effectif contient des objets décidément « effectifs », comme N ou R, il contient aussi des choses qui ne le sont pas du tout, comme ∇ℕ (on se convainc facilement que les morphismes ∇ℕ→∇ℕ dans le topos effectif s'identifient aux fonctions ℕ→ℕ quelconques, et d'ailleurs Hom(∇ℕ,∇ℕ) s'identifie à ∇(ℕ^ℕ)). Il n'est pas évident de définir ce qu'est un « objet effectif », même s'il y a différents candidats. Par exemple, les objets discrets sont les quotients (par une relation d'équivalence) des sous-objets de N, ou, ce qui revient au même, les objets qu'on peut présenter de la forme (X,E) avec E(x,x)∩E(y,y)=∅ lorsque x≠y ; les objets modestes, quant à eux, sont ceux qu'on peut présenter comme des assemblées discrètes.

☞ Objets séparés

Je devrais aussi mentionner les objets séparés (ou plus exactement, ¬¬-séparés), qui sont ceux pour lesquels la formule ∀x,y∈X. ((¬¬((x=y))) ⇒ (x=y)) est réalisée. En fait, de façon plus simple, les objets séparés sont exactement (ceux qu'on peut présenter comme) les assemblées.

☞ Objets uniformes

Les objets de type ∇X (que j'ai qualifiés de co-constants) sont en quelque sorte ceux qui ne sont pas du tout « effectifs », les plus éloignés des objets discrets ou modestes ; on peut aussi considérer leurs quotients par une relation d'équivalence, appelés objets uniformes. On peut montrer qu'un objet est uniforme si et seulement si il est isomorphe à un (X,E) pour lequel ⋂_x∈X E(x,x) est habité. À titre d'exemple, le classificateur de sous-objet Ω est uniforme (le même programme réalise P≡P pour tout P∈𝒫(ℕ) ; et, de fait, Ω est un quotient de ∇(𝒫(ℕ)) par la relation d'équivalence donnée essentiellement par ≡).

Le modèle de McCarty (de la théorie des ensembles intuitionniste)

☞ La construction de McCarty dans le topos effectif

Si on veut aller plus loin sur l'aspect ensembliste, on peut aussi chercher à construire dans le topos effectif un univers, appelé modèle de McCarty, de la théorie des ensembles intuitionniste (précisément, la théorie IZF, que je ne chercherai pas à définir précisément, mais qui est l'équivalent le plus naturel de ZF en logique intuitionniste) : en gros il s'agit d'imiter la construction de la hiérarchie de von Neumann (itération de l'ensemble des parties sur tous les ordinaux, ou du moins sur beaucoup d'ordinaux), sauf qu'on ne dispose pas des moyens d'itérer de façon transfinie dans le topos effectif, donc on doit un peu mettre les mains dans le « cambouis ».

On définit par récurrence transfinie sur l'ordinal α un ensemble W_α et une fonction E_α:(W_α)²→𝒫(ℕ) définissant un objet W_α = (W_α, E_α) du topos effectif, avec des inclusions W_β ⊆ W_α si β≤α, et E_β égal à la restriction de E_α à (W_β)², et pour δ ordinal limite, W_δ est la réunion des W_β où β<δ, avec E_δ est la réunion des E_β où β<δ (c'est-à-dire leur unique extension commune à W_δ), de la manière suivante :

• W₀ est l'ensemble vide (si bien que W₀ est l'objet initial) ; et W₁={∅}, qu'on va munir de E₁(∅,∅)=ℕ (si bien que W₁ est l'objet terminal) ;
• W_α+1 est l'ensemble 𝒫(W_α×ℕ) des parties de W_α×ℕ, qu'on identifie à des fonctions W_α→𝒫(ℕ), et la fonction d'égalité-existence E_α+1 associe à (u,v)∈(W_α+1)² la partie ⋂_x,y∈Wα (E_α(x,y) ⇛ ((u(x)⇛v(y))⊓(v(y)⇛u(x)))) (on a signalé plus haut que ceci fait de W_α+1 une présentation de l'objet des sous-objets de W_α) ;
• le fait de considérer W_α+1 comme l'ensemble 𝒫(W_α×ℕ) permet de voir tous les 𝒫(W_β×ℕ) pour β<α comme des sous-ensembles de lui (sur les fonctions W_β→𝒫(ℕ), cela revient à les prolonger par la valeur ∅ en-dehors de W_β), et c'est ainsi que W_α+1 contient W_β+1, donc finalement W_α ;
• et de même, la formule E_α+1(u,v) = ⋂_x,y∈Wα (E_α(x,y) ⇛ ((u(x)⇛v(y))⊓(v(y)⇛u(x)))) donnée plus haut étend la valeur de E_α(u,v) si u,v sont dans W_α, car si x,y (indices de l'intersection) sont dans un W_β pour β<α la valeur de l'ensemble intersecté est la même dans la formule pour E_α+1(u,v) que pour E_β+1(u,v) (puisque E_α(x,y) = E_β(x,y)), tandis que s'ils ne sont pas dans un tel ensemble, alors u(x) et v(y) valent ∅ et le terme intersecté est ℕ dans la formule pour E_α+1(u,v) et absent de celle pour E_β+1(u,v).

L'inclusion W_β ⊆ W_α si β≤α (et le fait que E_β égal à la restriction de E_α à (W_β)²) permet de voir W_β comme un sous-objet de W_α. J'ai mentionné que W_α+1 est l'objet des sous-objets de W_α : ceci nous donne une relation d'appartenance (∊) : W_α×W_α+1→Ω.

Si on dispose d'un ordinal λ « suffisamment sympathique », disons un cardinal inaccessible, ou si on est prêt à ignorer les difficultés ensemblistes et à appeler λ la classe de tous les ordinaux, alors W_λ = (W_λ, E_λ) muni de la relation (∊) vérifie un bon bout de la théorie des ensembles : si λ est inaccessible ou qu'on a ignoré les difficultés ensemblistes et considéré la classe de tous les ordinaux, on obtient un modèle de la théorie des ensembles intuitionniste IZF, appelé modèle de McCarty, qui peut aussi être décrit ab ovo sans aucune référence au topos effectif (cf. l'article de Charles McCarty, Realizability and recursive set theory (1986)), ce qui permet, si on préfère ça à la logique d'un topos, d'utiliser la réalisabilité dans le contexte d'une théorie des ensembles.

☞ Une remarque technique sur les limites inductives filtrantes

Caveat/digression : On peut être tenté de penser que, pour δ ordinal limite, W_δ est la limite inductive des W_β où β<δ, et c'est ce que je croyais fermement avant de commencer à écrire ce billet, mais maintenant je ne sais pas si c'est le cas. Il n'est donc pas clair dans quelle mesure on peut décrire les W_α de façon essentiellement interne dans le topos effectif, c'est-à-dire sans passer par une construction explicite des objets comme des ensembles munis d'un prédicat d'égalité-existence. Il y a certes une construction de W_λ, due à Joyal et Moerdijk comme quelque chose comme la ZF-algèbre λ-complète libre (une ZF-algèbre λ-complète (V,≤,succ) étant essentiellement un objet (V,≤) partiellement ordonné — ce qu'il faut imaginer être une sorte d'inclusion, et pour W_λ ce sera l'inclusion — dans laquelle les bornes supérieures « λ-petites » existent, et muni d'un morphisme « successeur » succ:V→V — ce qu'il faut imaginer comme une fonction de formation des singletons, et pour W_λ ce sera ça ; l'objet W_λ muni de son ordre d'inclusion et fonction singleton a alors une propriété universelle, c'est-à-dire que c'est l'objet libre pour ces structures) ; mais ça ne constitue pas vraiment une construction interne, il me semble. (Il n'est pas automatique que n'importe quel topos donne naissance à un modèle d'IZF selon une construction de ce genre, parce que le topos peut très bien manquer d'ordinaux ou de possibilité, mais c'est « souvent » le cas qu'il n'est pas difficile de la mener.) Bref, la réponse à tout ça est peut-être dans le livre de Joyal & Moerdijk, Algebraic Set Theory (1995), mais elle m'échappe largement.

La seconde algèbre de Kleene et le topos de la réalisabilité fonctionnelle

☞ La première algèbre de Kleene

Toute la construction du topos effectif est basée sur la structure suivante : l'ensemble ℕ des entiers naturel muni d'un codage pour les paires (p,q) ↦ ⟨p,q⟩ et, surtout, d'une application partielle (e,n) ↦ e•n (on parle parfois de première algèbre de Kleene pour cette opération partielle sur ℕ) à partir desquelles on a construit, sur 𝒫(ℕ) les opérations ⊓,⊔,⇛ qui permettent essentiellement d'interpréter la logique intuitionniste. Peut-on mettre autre chose à la place de ℕ ?

☞ La seconde algèbre de Kleene

Cette « première algèbre de Kleene » (ℕ,•) représente l'idée de la calculabilité de Church-Turing : on représente les fonctions partielles calculables ℕ ⇢ ℕ (définies sur un ensemble calculablement énumérable) par des entiers naturels, et on note e•n la valeur en n (si elle est définie) de la fonction partielle calculable codée par l'entier e. La « seconde algèbre de Kleene » (ℕ^ℕ,•) est basée sur une idée analogue, mais où on représente les fonctions partielles continues ℕ^ℕ ⇢ ℕ^ℕ (définies sur un ensemble G_δ) par des éléments de ℕ^ℕ. Reste à expliquer précisément comment coder ces choses, mais c'est globalement plus simple que définir les machines de Turing.

Si ε est un élément de ℕ^ℕ, c'est-à-dire une fonction (totale !) ℕ→ℕ, on va définir une fonction partielle F_ε de ℕ^ℕ vers ℕ (fonction continue encodée par la fonction ε) de la façon suivante. Supposons que α ∈ ℕ^ℕ, considérons les préfixes ⟨⟩, ⟨α(0)⟩, ⟨α(0),α(1)⟩, ⟨α(0),α(1),α(2)⟩, etc., encodés sous forme d'entiers naturels, et considérons les images m₀,m₁,m₂,… par ε de ces entiers naturels. On cherche le plus petit k (s'il existe) tel que la valeur m_k := ε(⟨α(0),α(1),…,α(k−1)⟩ soit >0, et on pose alors F_ε(α) = m_k − 1. Intuitivement, il faut comprendre les choses ainsi : on va soumettre à la fonction ε les préfixes successifs de α, encodés sous forme d'entiers naturels, et la fonction ε retourne soit 0 pour dire j'ai besoin de plus de valeurs pour me décider soit un entier m>0 pour dire en fonction de ces valeurs, je décide que la valeur retournée est m−1 (le décalage de 1 est juste dû au fait qu'on a réservé la valeur 0 pour dire je n'ai pas encode décidé). La fonction F_ε : ℕ^ℕ ⇢ ℕ ainsi définie est continue par construction (une fonction F de ℕ^ℕ vers ℕ est continue lorsque pour tout α il existe k tel que la valeur F(α) ne change pas si on remplace α par un autre élément qui a le même préfixe de longueur k) et définie sur un ouvert de ℕ^ℕ, et réciproquement, toute fonction continue ℕ^ℕ ⇢ ℕ définie sur un ouvert peut être exprimée sous cette forme. Maintenant pour passer des fonctions ℕ^ℕ ⇢ ℕ aux fonctions ℕ^ℕ ⇢ ℕ^ℕ, on va définir Φ_ε : ℕ^ℕ ⇢ ℕ^ℕ (fonction partielle) de la façon suivante : donnée α ∈ ℕ^ℕ, si on note i::α la fonction α à laquelle on a préfixé un i (autrement dit, 0↦i et j↦α(j−1) si j>0), on appelle Φ_ε(α) la fonction i ↦ F_ε(i::α) si F_ε(i::α) est définie pour tout i, et non définie sinon. La fonction Φ_ε : ℕ^ℕ ⇢ ℕ^ℕ ainsi définie est continue par construction (une fonction H de ℕ^ℕ vers ℕ^ℕ est continue lorsque pour tout α et tout i il existe k tel que le préfixe de longueur i de H(α) ne change pas si on remplace α par un autre élément qui a le même préfixe de longueur k) et définie sur un G_δ, c'est-à-dire une intersection dénombrable d'ouverts, et réciproquement, toute telle fonction est de cette forme.

Bref, le modèle de calcul sous-jacent c'est des machines infinies dont le programme est donné par une suite infinie ε d'instructions qui à chaque donnée possible d'une entrée i et d'un préfixe de longueur k de α associe optionnellement une valeur (ou sinon, l'indication qu'il faut chercher avec un préfixe plus long), et, si la valeur est définie pour tout i, ceci définit la fonction image de α.

On pose ε•α := Φ_ε(α). Ceci définit une opération partielle • sur ℕ^ℕ, qu'on appelle la seconde algèbre de Kleene, qu'on peut encore enrichir d'une fonction de codage des paires ℕ^ℕ × ℕ^ℕ → ℕ^ℕ, (p,q) ↦ ⟨p,q⟩ (par exemple en décidant que ⟨p,q⟩ prend en 2i la valeur p(i) et en 2i+1 la valeur q(i)) mais celle-ci n'est pas vraiment importante. Cette seconde algèbre de Kleene a énormément de propriétés semblables avec la première (par exemple, on peut chercher à prouver l'existence d'une « machine universelle », c'est-à-dire un υ∈ℕ^ℕ tel que ε•α = υ•⟨ε,α⟩ pour tous ε,α∈ℕ^ℕ : cela revient juste à montrer que la fonction (ε,α) ↦ ε•α est continue sur un G_δ).

☞ Le topos de la réalisabilité fonctionnelle

On peut ensuite refaire toute la définition du topos effectif (à commencer par celle des opérations ⊓,⊔,⇛) en remplaçant 𝒫(ℕ) par 𝒫(ℕ^ℕ) partout. Par exemple, une assemblée sera la donnée d'un ensemble porteur X, et d'une fonction E:X→𝒫(ℕ^ℕ), tandis qu'un objet plus général sera la donnée d'un ensemble porteur X et d'une fonction E:X²→𝒫(ℕ^ℕ) tels qu'il existe s,t∈ℕ^ℕ tels que quels que soient x,y∈X et α ∈ E(x,y) on ait s•α↓ (la fonction est définie) et s•α ∈ E(y,x), et que quels que soient x,y,z∈X et α ∈ E(x,y) et β ∈ E(y,z) on ait t•⟨α,β⟩↓ et t•⟨α,β⟩ ∈ E(x,z), et la définition des morphismes est modifiée de façon analogue, ainsi que celle de la réalisabilité (⟦φ⟧ est une partie de ℕ^ℕ, c'est-à-dire que les réalisateurs sont des éléments de ℕ^ℕ). La structure ainsi définie s'appelle le topos de la réalisabilité fonctionnelle. Il est beaucoup plus proche du topos des ensembles (i.e., des mathématiques classiques habituelles) : notamment, son objet N des entiers naturels, qui est l'assemblée portée par ℕ avec la fonction d'existence E(n) = {fonction constante de valeur n}, a exactement la même arithmétique du premier ordre que la théorie classique standard ; et le hom interne Hom(N,N) est l'assemblée portée par ℕ^ℕ avec la fonction d'existence E(α) = {α} et ne se limite pas aux fonctions calculables ; néanmoins, le principe de continuité de Brouwer pour les fonctions de N^N vers N vaut, donc on a ici affaire à un monde où toutes les fonctions de N vers N ne sont pas calculables, mais néanmoins toutes les fonctions de N^N vers N sont continues. Le classificateur de sous-objet Ω est bien sûr l'objet défini par X=𝒫(ℕ^ℕ), avec E(P,Q) égal à (P⇛Q) ⊓ (Q⇛P).

Le topos de Kleene-Vesley et le treillis de Medvedev

☞ Le topos de Kleene-Vesley

Mais un autre topos très important, qui est intermédiaire entre le topos effectif et le topos de la réalisabilité fonctionnelle que je viens de définir, est le topos de Kleene-Vesley. Pour l'expliquer, je dois commencer par dire que si on fait ce que je viens d'expliquer pour le topos de la réalisabilité fonctionnelle mais qu'au lieu de prendre l'ensemble ℕ^ℕ de toutes les fonctions ℕ→ℕ on prend juste celles qui sont calculables (au sens de Church-Turing) on obtient de nouveau le topos effectif (enfin, on obtient une catégorie équivalente au topos effectif) : ça ce n'est pas difficile (en gros, parce que l'opération que j'ai notée ‘•’ sur ℕ^ℕ préserve les fonctions calculables, et même, on peut la calculer à partir des numéros de programmes qui réalisent les deux fonctions à composées). Donc si on prend tout ℕ^ℕ on obtient le topos de la réalisabilité fonctionnelle, et si on prend les fonctions calculables ℕ→ℕ on obtient le topos effectif. Mais on peut faire quelque chose d'hybride entre les deux : on utilise 𝒫(ℕ^ℕ) dans les définitions, mais, au final, pour les réalisateurs qui témoignent de la véracité de quelque chose, on exige qu'ils soient calculables au sens de Church-Turing. C'est ainsi qu'est défini le topos de Kleene-Vesley :

Spécifiquement, un objet du topos de Kleene-Vesley est la donnée d'un ensemble porteur X et d'une fonction E:X²→𝒫(ℕ^ℕ) tels qu'il existe s,t∈ℕ^ℕ calculables au sens de Church-Turing tels que (la suite est comme pour le topos de la réalisabilité fonctionnelle) quels que soient x,y∈X et α ∈ E(x,y) on ait s•α↓ (la fonction est définie) et s•α ∈ E(y,x), et que quels que soient x,y,z∈X et α ∈ E(x,y) et β ∈ E(y,z) on ait t•⟨α,β⟩↓ et t•⟨α,β⟩ ∈ E(x,z) ; autrement dit, on ajoute juste la condition que s et t soient calculables. De même pour la définition des morphismes : on appelle relation fonctionnelle entre deux objets (X,E) et (Y,F) la donnée d'une fonction G:X×Y→𝒫(ℕ^ℕ) telle qu'il existe des éléments d,r,u,v∈ℕ^ℕ calculables au sens de Church-Turing vérifiant les conditions demandées pour le topos effectif, mutatis mutandis (en gros remplacer ℕ par ℕ^ℕ partout, la condition de calculabilité ne portant que sur l'existence de d,r,u,v) ; et on dit que deux relations fonctionnelles G,G′ sont équivalentes lorsqu'il existe p,q calculables au sens de Church-Turing qui appartiennent à (G(x,y)⇛G′(x,y))⊓(G′(x,y)⇛G(x,y)) pour tous x∈X et y∈Y. Enfin, pour la réalisabilité, la définition de ⟦φ⟧ comme partie de ℕ^ℕ est la même que pour le topos de la réalisabilité fonctionnelle, mais au final on ne dit que φ est réalisable que s'il a un réalisateur calculable au sens de Church-Turing. L'objet des entiers naturels et le classificateur de sous-objet sont exactement les mêmes objets que pour le topos de la réalisabilité fonctionnelle ; en fait, le hom interne entre deux objets est construit comme dans le topos de la réalisabilité fonctionnelle, c'est le hom externe qui diffère.

Ce topos de Kleene-Vesley a à la fois des rapports avec le topos de la réalisabilité fonctionnelle et avec le topos effectif (il y a un foncteur « logique » vers le premier, et trois foncteurs successivement adjoints avec le second). Pour en savoir plus, on peut consulter le livre de van Oosten cité au début, ainsi que la thèse de Lars Birkedal, Developing Theories of Types and Computability via Realizability (1999) que je n'ai fait que survoler.

☞ Le treillis de Medvedev comme valeurs de vérité du topos de Kleene-Vesley

Mentionnons tout de même une chose pour conclure sur ce topos de Kleene-Vesley : alors que dans le topos effectif comme dans le topos de la réalisabilité fonctionnelle il n'y a que deux morphismes 1→Ω (deux « valeurs de vérité globales »), à savoir le vrai (représenté par n'importe quel ensemble habité) et le faux (représenté par le vide), dans le topos de Kleene-Vesley les choses sont très différentes. Considérons sur 𝒫(ℕ^ℕ) une relation de préordre (i.e., réflexive et transitive) ‘≼’ définie ainsi : P≼Q lorsque P⇒Q est réalisable dans le topos de Kleene-Vesley, i.e., que P⇛Q est habité par un élément calculable au sens de Church-Turing, c'est-à-dire, lorsqu'il existe ε ∈ ℕ^ℕ calculable tel que pour pour tout α∈P on ait ε•α↓∈Q (ceci signifiant que d'une part ε•α est défini et d'autre part que l'élément en question appartient à Q) ; ou, si on veut éviter de faire référence à l'opération ‘•’ sur ℕ^ℕ, cela équivaut à dire qu'il existe une machine de Turing à oracle qui, quand on lui fournit un élément quelconque α de P comme oracle, définit une fonction totale ℕ→ℕ (i.e., termine sur toute entrée dans ℕ) et que la fonction en question est dans Q. La relation d'équivalence associée à ‘≼’ (i.e., P≼Q et Q≼P, ce qui revient à dire, P≡Q est habité par un élément calculable) définit l'équivalence des relations fonctionnelles 1→Ω dans le topos de Kleene-Vesley, c'est-à-dire que Hom(1,Ω) y est le quotient de 𝒫(ℕ^ℕ) par cette relation, naturellement muni de l'ordre partiel défini par ‘≼’. Il se trouve que cette structure a un nom classique et a été étudiée en calculabilité bien avant les topos de réalisabilité : c'est le treillis de Medvedev ou treillis des degrés de difficulté (à ceci près que l'ordre est inversé : la plupart des auteurs définissent un ordre pour lequel la classe du vide est le plus grand élément, parce que c'est le plus difficile, et la classe de {f} avec f:ℕ→ℕ calculable quelconque, ou de ℕ^ℕ, est le plus petit élément, parce que c'est le plus facile ; comme défini ci-dessus, c'est le contraire, la classe du vide est le plus petit élément parce que c'est le faux du topos, et la classe d'un singleton calculable, ou de ℕ^ℕ, est le plus grand élément parce que c'est le vrai) ; pour en savoir plus sur le treillis de Medvedev (et son rapport avec les degrés de Turing et de Mučnik), je renvoie par exemple à l'article de Peter Hinman, A survey of Mučnik and Medvedev degrees (Bull. Symbolic Logic 18 (2012) 161–229), qu'on trouve librement disponible sur l'arXiv.