Avant-propos
Le but ce de billet interminable est de donner (sans trop de prérequis, cf. plus bas) quelques explications, la définition, et quelques propriétés autour du topos effectif de Hyland. C'est un sujet sur lequel je m'étais promis de parler sur ce blog il y a un moment déjà. Je n'ai cependant pas vraiment suivi mon plan initial, qui était plutôt de faire d'abord une série de billets (en principe indépendant mais qu'il aurait été conseillé de lire dans l'ordre) pour expliquer au préalable l'idée générale du concept de topos et leur logique interne, puis les topos de faisceaux sur un espace topologique, avant d'en venir au topos effectif (que j'ai tendance à imaginer comme plus difficile à comprendre, mais peut-être que je me trompe, en fait). Seulement je me suis retrouvé (pour lire des choses sur un sujet connexe[#]) à ré-apprendre la définition du topos effectif après l'avoir oubliée pour la 42e fois environ, et j'ai pensé que la meilleure façon de la retenir et de m'assurer que j'en avais compris les bases, serait de me forcer à l'expliquer ici, autant que possible de mémoire, et, de fait, ça m'a permis de me rendre compte de plein de subtilités qui m'avaient d'abord échappé : voici pour la genèse de cette entrée, qui s'est évidemment avérée beaucoup plus longue qu'initialement prévue, et que sans doute personne ne lira mais ce n'est pas grave parce qu'elle m'aura servi à moi.
[#] En fait, pour
expliquer d'où je viens pour les gens qui connaissent déjà le sujet,
ces jours-ci j'essaie épisodiquement de comprendre trois articles que
je considère à la fois très intéressants et très importants (pas
tellement pour leurs résultats que pour le point de
vue, surtout s'agissant des deux derniers), et dont je reparlerai
sans doute une autre fois, d'un certain Takayuki Kihara :
① Degrees
of incomputability, realizability and constructive reverse
mathematics
,
② Lawvere-Tierney
topologies for computability theorists
et
③ Rethinking
the notion of oracle
(ils peuvent se lire indépendamment les
uns des autres et aussi indépendamment de la notion de topos effectif,
mais toutes ces choses s'éclairent nettement les unes les autres).
Notamment, les deux derniers articles suggèrent que la « bonne »
notion d'oracle en calculabilité est celle de topologie de
Lawvere-Tierney sur le topos de Kleene-Vesley, et donc j'essaie de me
faire une intuition du pourquoi et du comment.
[Ajout : à ce sujet,
voir ce billet ultérieur.]
Cette genèse peut aussi expliquer le style inhabituellement
brouillon, vu que j'avais commencé par me dire que j'allais juste
donner la définition et rien d'autre, et au fur et à mesure que je
l'écrivais je m'apercevais soit que je devais d'abord expliquer ceci
ou cela, soit qu'il fallait bien que je dise un mot sur telle chose
que j'avais mal comprise, ou simplement parce que je me suis dit que je
ne pouvais pas m'affranchir d'un bout d'explication intuitive pour
adoucir une présentation trop formelle. Bref, c'est un peu le bordel,
surtout que j'ai plusieurs fois changé l'ordre dans lequel je disais
certaines choses, et je n'exclus pas d'avoir commis des cercles vicieux
de références, mais j'espère que ce qui suit a quand même un intérêt,
surtout que ce n'est pas évident de trouver des textes où les choses
sont bien expliquées. (Notamment si on ne veut pas savoir ce qu'est
un tripos
— et personnellement je préfère ne pas avoir à savoir
ce qu'est un tripos
, donc je ne parlerai pas du tout de tripos
dans la suite.)
En plus de ça, je me suis très peu relu, et maintenant que ce billet est fini je n'ai plus vraiment le courage de le relire systématiquement. (Cet avertissement est valable pour toutes les entrées de ce blog, mais celle-ci est particulièrement propice à engendrer des fautes de frappe idiotes donc il y en a certainement à foison.)
Bref, je ne sais pas à quel point ce qui suit est compréhensible, mais j'ai fait un certain effort pour limiter les prérequis : en principe, pour l'essentiel de ce billet je ne suppose du lecteur qu'une familiarité avec la théorie élémentaire des ensembles et les rudiments de la calculabilité ; il n'est pas nécessaire, notamment, de savoir ce qu'est un topos (et d'ailleurs, je ne l'expliquerai pas, je me contente de définir le topos effectif), ni même une catégorie (mais ça doit quand même aider). Je suppose qu'on sait ce que c'est qu'une formule logique (connecteurs et quantificateurs, ce genre de choses), mais guère plus : il n'est pas vraiment nécessaire de savoir ce qu'est la logique intuitionniste, mais c'est utile, surtout à partir de la partie qui parle de réalisabilité, d'en avoir une certaine idée, et la lecture de ce billet ou surtout celui-là peuvent remplir ce prérequis faible. Je ne suppose pas non plus que le lecteur a lu mon précédent billet sur la réalisabilité, mais ça peut aider à motiver les définitions (le topos effectif est une généralisation de la réalisabilité de Kleene). Vers la fin du billet, je suppose la familiarité avec quelques concepts plus sophistiqués (coupures de Dedekind, ordinaux, des choses de ce genre), mais comme il s'agit de petits bouts assez indépendants les uns des autres, on doit pouvoir sauter ce qu'on ne comprend pas.
En tout cas, j'espère au moins avoir réussi à écrire quelque chose de plus clair que l'article Wikipédia ou celui du nLab.
Si on veut en savoir plus que ce qui est expliqué ici (ou corriger
les bêtises que j'aurai certainement écrites), le mieux est sans doute
de se tourner vers le livre de
van Oosten, Realizability: An Introduction to its
Categorical Side (2008), qui contient essentiellement tout ce
que je raconte ici, mais il vaut mieux sauter directement au
chapitre 3 si on ne veut pas entendre parler de tripos. On peut aussi
regarder l'article de Bernardet & Lengrand, A
simple presentation of the effective topos
(ici sur l'arXiv), même
si je ne suis pas persuadé que leur présentation soit vraiment
plus simple
que la version usuelle, elle a le mérite d'être
assez compacte et contenue. L'article original de Hyland
s'appelle The Effective Topos
, et il est paru
p. 165–216 dans les actes The L.E.J. Brouwer
Centenary Symposium édité par Troelstra &
van Dalen (1982) : en
voici une
version retypographiée
et le scan de
la version d'origine (disponible sur Sci Hub si vous n'y avez pas
accès par ce lien).
Ajout () : on me signale en
commentaire ce texte d'Ingo Blechschmidt (un chapitre
du livre Exploring mathematical objects from
custom-tailored mathematical universes édité par Oliveri,
Ternullo et Boscolo, qui est plutôt de portée philosophique) ; cela
semble en effet une bonne introduction : il développe de façon
pédagogique (et en commençant de façon très informelle) le point de
vue les topos comme des mondes mathématiques alternatifs
;
néanmoins, il ne donne pas une vraie définition du topos effectif
(juste comme une complétion de la catégorie des assemblées). Tant
qu'à faire, je peux aussi signaler
les notes
d'Andrej Bauer sur la réalisabilité, qui sont à l'état d'ébauche
au moment où j'écris : ce qui est là est très bien expliqué, mais
c'est encore incomplet, et notamment, il n'y a pas de définition du
topos effectif.
Ajout () : ce billet ultérieur sur diverses généralisations des degrés de Turing (et sur ce qui est, en fait, les topologies de Lawvere-Tierney sur le topos effectif), quoique indépendant de celui-ci, a néanmoins un rapport assez étroit.
Ajout () : ce billet ultérieur sur la réalisabilité propositionnelle (qu'on peut lire avant, ou après, ou indépendamment) a aussi un rapport étroit avec celui-ci, puisque la réalisabilité propositionnelle est la logique propositionnelle interne du topos effectif.
Table des matières
- Avant-propos
- Table des matières
- Motivation
- Préliminaires
- La définition du topos effectif
- Objets du topos effectif, et assemblées
- Quelques exemples d'objets
- Relations fonctionnelles et morphismes
- L'objet des morphismes (Hom interne) et l'objet des sous-objets
- Image d'un morphisme, quotient d'un objet
- Une remarque sur la représentation des sous-objets
- Simplification de la représentation des morphismes
- Quelques exemples de morphismes
- La réalisabilité des formules logiques : langage interne du topos effectif
- Autres topos apparentés
Motivation
☞ Un monde de la calculabilité
Bref, le but est de donner ci-dessous la définition du topos
effectif, c'est-à-dire des « objets » et des « morphismes » du topos
effectif, et ensuite de la « réalisabilité » des formules logiques
dont les variables sont « typées » par les objets du topos effectif.
(Tous les mots entre guillemets doivent être expliqués plus bas.)
Pour essayer de donner quand même un avant-goût de quoi il est
question avant de passer aux définitions proprement dites, un
objet du topos effectif va être une structure qui ressemble à un
ensemble, et un morphisme va ressembler à une application, mais l'idée
est de construire une sorte de monde mathématique alternatif (sujet
aux lois de la logique intuitionniste,
cf. ici et
surtout là), ça c'est en gros le
sens du mot topos
, mais ce topos précis ayant la propriété
remarquable que toute fonction des entiers vers eux-mêmes est
calculable (au sens de Church-Turing), d'où le terme
de effectif
, et accessoirement toute fonction réelle est
continue. (Ces affirmations étant certainement réfutables en
logique classique, il est nécessaire de passer à une logique plus
faible comme la logique intuitionniste pour espérer les rendre
possibles.)
☞ Vérité par témoignages
Toujours pour donner une idée très vague et en agitant les mains de
ce dont il va s'agir, le cœur de l'idée du topos effectif est
d'utiliser en quelque sorte, les parties de ℕ (i.e., les ensembles
d'entiers naturels) comme des sortes de valeurs de vérité (avec les
opérations ⊓,⊔,⇛ que je vais
définir ci-dessous
pour tenir lieu de la conjonction, de la disjonction, et de
l'implication logique). De façon un tout petit peu moins vague, pour
différentes sortes d'affirmations logiques, le topos effectif va
introduire une partie de ℕ (plus bas, je noterai ⟦φ⟧ pour
la « valeur de vérité » associée à une formule logique φ),
qu'on appellera l'ensemble de ses « réalisateurs » : le terme
classique est de dire que n réalise φ
pour dire que n appartient à la partie en question
(n ∈ ⟦φ⟧
), mais je préfère,
intuitivement, parler de témoignages
de la véracité
de φ.
Même si j'en suis juste à une explication très vague et informelle, profitons-en pour dissiper un malentendu possible dans l'idée qu'on peu se faire : la taille de la partie n'importe pas, il suffit de disposer d'un seul « témoignage » pour conclure que φ est valable dans le topos effectif ; ce n'est pas parce que la partie est plus grande qu'on conclut que l'affirmation est plus vraie, la seule chose qui importe est d'arriver à trouver un élément dedans : si ∅ représente le « faux », le « vrai » peut se représenter aussi bien par ℕ ou {0} ou {42}. Du coup, on peut se demander pourquoi il n'y a pas juste deux valeurs de vérité, le vide qui représente le faux, et n'importe quel ensemble habité[#2] qui représente le vrai, et de fait c'est bien le cas quand il n'y a aucun paramètre libre, mais dès que la partie dépend de paramètres, il va y avoir des parties habitées où il sera plus ou moins facile de trouver un élément. Dit comme ça, c'est désespérément vague, mais j'espère que ça aidera à comprendre un peu mieux les définitions précises qui vont suivre.
[#2] Le
mot habité
(pour un ensemble) signifie
simplement non-vide
. Je vais dire plus bas pourquoi je
l'utilise.
☞ Ensembles avec égalité-existence
Toujours de façon très vague, un objet du topos effectif sera la donnée (X,E) d'un ensemble X (au sens usuel) muni d'une « fonction d'égalité-existence », qui à un couple (x,y) d'éléments de X va associer une partie de ℕ qui indique la « valeur de vérité » du fait que x et y existent et sont égaux (on pourrait certainement séparer les deux rôles en une fonction d'existence et une fonction d'égalité, mais ce serait techniquement moins commode), cette fonction étant symétrique et transitive en un sens qu'on va expliquer plus bas (mais pas réflexive, parce que la réflexivité va servir à mesurer l'existence). Et un morphisme entre objets du topos effectifs est défini, en gros, par une fonction qui indique, de même, la « valeur de vérité » du fait que x est envoyé sur y par le morphisme. Maintenant il s'agit de rendre précises ces idées que je viens de dire de façon très vague.
Préliminaires
Avant de commencer vraiment, je dois introduire de rapides notations et préliminaires.
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 P1,…,Pr, alors il existe n∈ℕ (dépendant uniquement de φ, mais pas de P1,…,Pr) tel que, quels que soient les parties P1,…,Pr de ℕ, si on substitue P1,…,Pr à P1,…,Pr, 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.]
La définition du topos effectif
Passons maintenant à la définition des objets du topos effectif.
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 la même partie habitée de ℕ. 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 (rn) de rationnels tels que |rn − rn+1| ≤ 2−(n+1) etré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=⟨pn,qn⟩ où (rn=pn/qn) 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 évidemment dire, l'entier naturel λn.n qui code un programme implémentant l'identité).
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é
). Intuitivement, p « témoigne » du fait que
si G envoie x sur y
alors G′ le fait aussi, et q de la réciproque ;
ainsi, ⟨p,q⟩ témoigne du fait que G
et G′ envoie les mêmes éléments sur les mêmes éléments.
Comme le nom le suggère, ceci définit bien une relation d'équivalence (je veux dire, réflexive, symétrique et transitive) sur l'ensemble des relations fonctionnelles entre deux objets fixés. La vérification de ce fait est analogue à plein d'autres vérifications de ce genre que j'ai déjà données, donc je n'insiste pas.
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).
Conseil au lecteur
(ajouté ) : les passages qui suivent
contiennent pas mal de détails techniques qui risquent de noyer un peu
l'essence du propos, surtout que je tiens à différents endroits à
dire on peut voir les choses comme ceci… mais on peut aussi les
voir comme cela…
; je recommande de ne pas hésiter à lire en
diagonale si on a l'impression que je me perds dans les détails, et
d'arriver rapidement
aux exemples
de morphismes, quitte, si on veut en savoir plus, à revenir sur
les passages lus en diagonale.
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′) := Hd(G) ⊓ Hr(G) ⊓ Hu(G) ⊓ Hv(G) ⊓ K(G,G′) si G,G′ sont deux fonctions X×Y→𝒫(ℕ), où :
- en s'inspirant de la définition d'une relation fonctionnelle :
- Hd(G) := ⋂x∈X,y∈Y (G(x,y)⇛(E(x,x)⊓F(y,y)))
- Hr(G) := ⋂x,x′∈X,y,y′∈Y ((E(x,x′)⊓G(x,y)⊓F(y,y′))⇛G(x′,y′))
- Hu(G) := ⋂x∈X,y,y′∈Y ((G(x,y)⊓G(x,y′))⇛F(y,y′))
- Hv(G) := ⋂x∈X (E(x,x)⇛⋃y∈YG(x,y))
- 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 Hd(G), Hr(G), Hu(G), Hv(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 Hd(G) ⊓ Hr(G) ⊓ Hu(G) ⊓ Hv(G) ⊓ K(G,G′), mais j'aurais tout aussi bien pu mettre Hd(G) ⊓ Hr(G) ⊓ Hu(G) ⊓ Hv(G) ⊓ Hd(G′) ⊓ Hr(G′) ⊓ Hu(G′) ⊓ Hv(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.
Quelques propriétés, qui ne surprendront personne d'habitué à la théorie des catégories :
- Hom(X, Y×Z) s'identifie à Hom(X,Y) × Hom(X,Z) (où X,Y,Z sont trois objets du topos effectif et, dans la première partie, Y×Z est l'objet produit que j'ai défini plus haut, tandis que dans la deuxième partie, ‘×’ est un produit cartésien d'ensembles).
- Hom(X⊎Y, Z) s'identifie à Hom(X,Z) × Hom(Y,Z) (où X,Y,Z sont trois objets du topos effectif et, dans la première partie, X⊎Y est l'objet coproduit que j'ai défini plus haut).
- Hom(X, Hom(Y,Z)) s'identifie à Hom(X×Y, Z).
Ces identifiations sont, par ailleurs, naturelles au sens où — si on sait ce que ça signifie — ce sont des isomorphismes entre les foncteurs définis sur toutes les variables libres dans l'histoire.
☞ 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) := Hd(P) ⊓ Hr(P) ⊓ K(P,Q) si P,Q sont deux fonctions X→𝒫(ℕ), où :
- comme ci-dessus :
- Hd(P) := ⋂x∈X (P(x)⇛E(x,x))
- Hr(P) := ⋂x,x′∈X ((E(x,x′)⊓P(x))⇛P(x′))
- 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.
Par ailleurs, si on sait ce que ça veut dire, l'ensemble des
sous-objets que je viens de définir coïncide bien avec l'ensemble des
sous-objets au sens général de la théorie des catégories (c'est-à-dire
des classes d'équivalence de monomorphismes X′→X pour la
relation d'équivalence d'être isomorphes de façon compatible au
monomorphisme vers X). C'est ceci qui justifie la terminologie
de classificateur de sous-objet
pour Ω, et qui est une des
conditions essentielles dans la définition d'un topos
élémentaire
que je ne donne pas ici.
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é Hr(P) et K(P,Q) ci-dessus, ce qui n'est pas spécialement subtil (on se convainc facilement que H˜(P,Q) ≡ (Hr(P)⊓K(P,Q)) est habité par un entier naturel indépendant de tout), mais pour ce qui est de Hd(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 Hd(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 :
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).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∈𝒫(ℕ).)
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′) := Hr(g) ⊓ K(g,g′) si g,g′ sont deux fonctions X→Y, où :
- come ci-dessus :
- Hr(g) := ⋂x,x′∈X (E(x,x′)⇛F(g(x),g(x′)))
- 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 Hr(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 Hr(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 Nk→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(Nk,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 levrai
). 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.)
La réalisabilité des formules logiques : langage interne du topos effectif
Maintenant que j'ai défini le topos effectif, faut que je parle de la réalisabilité, qui permet de donner un sens aux formules logiques dans le topos effectif. (J'avais déjà défini la réalisabilité de Kleene dans ce billet, mais il n'est pas nécessaire de l'avoir lu — même si ça peut éclairer les choses — puisque de toute façon la définition qui suit va inclure celle de ce billet passé, à savoir le cas où toutes les variables sont des entiers naturels, c'est-à-dire ont pour type N.)
[Ajout : voir aussi ce billet ultérieur sur la réalisabilité propositionnelle c'est-à-dire le cas de formules n'impliquant que des variables de type Ω.]
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 φ(t1,…,tk) est une formule ayant des variables libres t1,…,tk de types respectifs X1,…,Xk et si x1,…,xk sont des éléments des ensembles X1,…,Xk porteurs de X1,…,Xk, on définit une partie ⟦φ(x1,…,xk)⟧ de ℕ (ou, si on préfère voir les choses comme ça, on définit une fonction ⟦φ(t1,…,tk)⟧ : X1×⋯×Xk→𝒫(ℕ)) 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∈NN.∀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∈NN.∀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∈NN. ∃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∈NN. ∃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∈NN
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 NN vers N) : ∀F∈N(NN). ∀u∈NN. ∃n∈N. ∀v∈NN. (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 NN 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
(rn) de QN
tels que
∀n∈N. |rn−rn+1|≤2−(n+1),
par la relation d'équivalence la différence explicitement tend
vers 0
, c'est-à-dire
(rn)~(r′n)
lorsque
∀n∈N. |rn−r′n|≤2−(n−1)
(si au lieu de mettre une borne explicite comme je l'ai fait ici on
mettait un
∀k∈N. ∃m∈N. ∀n≥m.
|rn−rn+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 :
- S et T sont habités : ∃r∈Q.(r∈S) et ∃r∈Q.(r∈T) ;
- 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) ;
- 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)) ;
- 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)) ;
- 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 (rn) (calculable, de Cauchy explicite), on lui associe une coupure de Dedekind (S,T) en définissant S comme {s∈Q | ∃n∈N. (s < rn−2−n)} de façon interne, c'est-à-dire, de façon externe, par la fonction ℚ→𝒫(ℕ) qui à s associe {n∈ℕ | s < rn−2−n}, et T de façon analogue comme {t∈Q | ∃n∈N. (t > rn+2−n)}. 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−(n−1), et alors on a soit s < rn−2−n soit t > rn+2−n : 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−n (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 2n−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 2n−k+1+1 rationnels formant les extrémités des intervalles, disons u0,…,u2n−k+1 (régulièrement espacés de 2−(n+1)), il y a un 0<ℓ<2n−k+1 tel que tous les ui pour i<ℓ soient dans S et tous les ui 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−n. (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 sn et un tn 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 (sn+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−n près de xy si
on s'est donné des façons d'en fabriquer une à
2−n 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 (rn) de
Cauchy explicites telles qu'il existe un n
avec rn > 2−n
(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 rn ≥ 2−n
(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. rn > 2−n
à
∃n∈N. rn > 2−n) ;
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 NN → N, on en a un
pour les fonctions R→R, toutes les fonctions réelles
sont continues
, à savoir
∀F∈RR. ∀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 NN → 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 :
- W0 est l'ensemble vide (si bien que W0 est l'objet initial) ; et W1={∅}, qu'on va munir de E1(∅,∅)=ℕ (si bien que W1 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.
Autres topos apparentés
Je veux finir ce billet interminable en évoquant un analogue ou
généralisation du topos effectif. La bonne notion ici est celle
de topos de réalisabilité
, mais je ne veux pas la définir (il
faudrait commencer par définir les algèbres combinatoires partielles,
et c'est assez emmerdant). Je vais juste me contenter d'un ou deux
cas particuliers.
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 mk
:= ε(⟨α(0),α(1),…,α(k−1)⟩
soit >0, et on pose
alors Fε(α)
= mk − 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 NN 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 NN 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.