Ce qu'interprètent les topos

Georges Abitbol · January 2018

Bonjour,

désolé pour le post fleuve. Pouvez-vous me dire si ce que je tente de faire plus bas a un intérêt, si ça a déjà été fait, et si oui, où ?

Le pourquoi :
En vue de répondre à la question (posée dans le fil : cliquez ici) de l'inexistence de fonctions non continues de $\mathbb{R}$ dans $\mathbb{R}$ sans tiers exclu, je me suis intéressé au langage de Mitchell-Bénabou (discussion dans ce fil : cliquez ici). Je me suis aperçu qu'à mes yeux, ce langage constituait plus une sémantique qu'une syntaxe (je considère que "langage" a le sens mathématique que lui donnent les livres classiques de logique, i.e. ensemble de phrases structurées muni de diverses "opérations logiques"), et je me suis demandé ce que les topos interprétaient vraiment.
La question me semble très importante : sans en avoir une réponse, que veut-on dire quand on dit que "les topos peuvent être considérés comme des univers d'ensembles, d'un point de vue intuitionniste" (slogan que j'ai lu à divers endroits et que je n'exclus pas de l'avoir involontairement déformé).

J'en suis venu à conclure que ce langage de Mitchell-Bénabou fournissait une interprétation (mot à qui je donne à peu près le sens qu'il a en théorie des modèles - à moins que je fasse un contresens) pour un certain langage que je vais appeler langage de la théorie typée-bridée des ensembles (en abrégé TTBE), et que je vais décrire ci-après. Attention, je n'affirme pas que c'est une trouvaille de ma part ; j'ai même l'impression que ceci est parfaitement compris de certains membres du forum. En tout cas, j'ai déploré le fait de ne pas avoir lu (ou voulu lire, peut-être) noir sur blanc ce que je vais écrire. Je rédige donc ce post en me disant que c'est utile d'écrire ce qui m'a manqué.

Signature du langage de la TTBE :
On se fixe un ensemble $U$, et on appelle ses éléments des types. On suppose qu'il est muni d'une application $\otimes : U \times U \rightarrow U$. Si on a deux types $A$ et $B$, on dit que $A\otimes B := \otimes(A,B)$ est le type produit de $A$ et de $B$. On suppose également que $U$ est muni d'une application $P : U \rightarrow U$. Si on a un type $A$, on dit que $P(A)$ est le type parties de $A$.
On suppose de plus qu'on a deux ensembles $S_=$ et $S_\in$ disjoints et tous deux disjoints de $U$, et deux bijections $U \rightarrow S_=$ et $U \rightarrow S_\in$. L'image de $A$ par la première est notée $=_A$ est est appelée symbole d'égalité du le type $A$, et on dit que son arité est $(A,A)$. L'image de $A$ par la deuxième est notée $\in_A$ et est appelée symbole d'appartenance du type $A$, et on dit que son arité est $(A,P(A))$.
On suppose enfin qu'on a deux ensembles disjoints et disjoints de tous les autres ci-dessus, $S^1_\pi$ et $S^2_\pi$une bijection $A\times B \rightarrow S^1_\pi$ et $A\times B \rightarrow S^2_\pi$. L'image de $(A,B)$ par la première est notée $\pi^1_{AB}$ et son image par la deuxième est notée $\pi^2_{AB}$. Ces images sont appelées, respectivement symbole de première projection et symbole de deuxième projection et sont considérés comme des symboles de fonction d'arité $A\otimes B \rightarrow A$ et $A \otimes B \rightarrow B$.
Enfin, on se donne une famille $(V_A)_{A \in U}$ d'ensembles deux à deux disjoints et disjoints de tout le reste. Si $A \in U$, on dit que $V_A$ est l'ensemble des variables de type $A$.

Définition des termes du langage de la TTBE :
Les termes du langage de la TTBE sont définis par induction :
- si $A \in U$, $x \in V_A$, alors $x$ est un terme de sorte $A$ ;
- si $A \in U$, $B \in U$, et si $y \in V_{A\otimes B}$, alors $\pi^1_{AB}(y)$ est un terme de sorte $A$ et $\pi^2_{AB}(y)$ en est un de sorte $B$.

Définition des formules du langage de la TTBE :
Les formules du langage de la TTBE sont définies par induction :
- si $A \in U$, et si $x$ et $y$ sont des termes de sorte $A$, alors $x =_A y$ est une formule ;
- si $A \in U$, et si $x$, $y$ sont des termes de sorte $A$ et $P(A)$, alors $x \in_A y$ est une formule ;
- si $P$ et $Q$ sont des formules, alors $A \wedge B$ et $A \vee B$, $A \Rightarrow B$ sont des formules ;
- si $A \in U$, si $x \in V_A$, et si $P$ est une formule, alors $\forall_A x P$ est une formule ;
- si $A \in U$, si $x \in V_A$, et si $P$ est une formule, alors $\exists_A x P$ est une formule.
On définit les variables libres d'une formule comme d'habitude, et on appelle formules closes les formules sans variables libres.

Interprétation du langage de la TTBE dans un topos :
Soit $T$ un topos dont l'ensemble des objets est $U$, et tel que pour tous $A,B \in U$, $A\otimes B$ est un produit de $A$ et de $B$ dans $T$, et où $P(A)$ est le truc du topos. Alors, à toute formule close est associée (via le langage de Mitchell-Bénabou) une flèche $1\rightarrow \Omega$, et on dit qu'une formule est valide dans $T$ si la flèche associée est la flèche $\top$.

Axiomes de la TTBE :
- les axiomes qui expriment que les symboles d'égalité vérifient la réflexivité, la transitivité, et la symétrie ;
- les axiomes qui expriment les "règles de la logique intuitionniste" ;
- les axiomes qui expriment que les $\pi^i$ doivent se comporter comme les projections d'un produit cartésien ;
- des axiomes qui donnent aux symboles d'appartenance ce qu'on attend d'eux, et c'est là que je galère.

Je vais essayer de faire l'exercice qui consiste à démontrer que les deux premiers groupes d'axiomes ci-dessus sont valides dans tous les topos, et je vous dirai si j'ai un problème.
Je voudrais donc un ensemble $A$ d'axiomes sur l'appartenance. Je voudrais que ceux-ci soient valides dans un maximum de topos élémentaires, et si possible tous. Mais bon, ici, c'est un peu à moi de choisir mes axiomes.
Je galère notamment à trouver un axiome qui remplacerait celui de la réunion. Celui qui me plaît, $\forall_{P(P(A))} a\ \exists_{P(A)} b\ \forall_{P(A)} z \ (z \in_{P(A)} a \Rightarrow z \subset_{P(A)} b)$ (où $x \subset_{P(A)} y$ abrège $\forall_A x \ (x \in_A y \Rightarrow x \in_A z)$, j'ai bien peur qu'il ne soit pas valide dans les topos où l'algèbre de Heyting sur $\Omega$ n'est pas complète... Sinon, on peut bien écrire un "axiome de réunion finie", mais c'est un peu tristounet, non ?

Bref, qu'en pensez-vous ?

moduloP · February 2018

Salut Georges,

Je tente un truc mais je n'ai pas trop compris ce que tu veux faire. Est-ce que tu peux me dire si j'ai pigé un peu la problématique que tu poses, et si tu vois des conneries dans ce que j'écris ? Normalement, je dis beaucoup de connerie même si j'essayes de faire attention :-D

Alors si j'ai bien compris, le premier point de l'exercice que tu veux faire consiste à vérifier que l'égalité vérifie les choses que l'on attend d'elle symétrie, transitivité et réflexivité.

J'explique ce que l'on entend par égalité, sinon on va nous prendre pour des fous voulant montrer que : $a=b \iff b =a$ :-D
Tu disposes d'un carré cartésien qui défini l'égalité : ici $=_Y$ est une application qu'il faut concevoir comme la fonction caractéristique du sous-objet diagonal de $Y$ dans $Y \times Y$. Il faut voir que cette application diagonal $id \times id$ est un monomorphisme (je n'ai pas fait la vérification)

$$
\xymatrix {
Y \ar@{->}[d]_{\Delta} \ar@{->}[r] & 1 \ar@{->}[d]^{ \text{True}}\\
Y \times Y \ar@{-->}[r]_{=_Y} &\Omega
}
$$

Elle est donné, cette application $=_Y$, comme l'unique flèche $ Y \times Y \to \Omega$ tel que le diagramme soit cartésien (j'ai un peu de mal à comprendre l'unicité, dans mon argument, après, je ne pense pas utilisé l'unicité ?)

Et tu prends deux flèches $f,g : X \to Y$ et tu dis que $f =_Y g$ lorsque $ =_Y \circ (f \times g) = \text{True}$, ce qui veut dire que la flèche $ =_Y \circ (f \times g)$ "passe par " $1$.

Et tu veux prouver que cette égalité $=_Y$ vérifie les conditions classiques de l'égalité. En fait, on peut montrer que cette égalité est exactement l'égalité i.e $f=g$ si et seulement si $ =_Y \circ (f \times g) = \text{True}$, et ça permet de conclure (c'est l'exercice 221 page 212 du cours ici).

D'un point de vue ensembliste, ça se voit bien : $f = g$ si et seulement si $[a \mapsto \chi(f(a),g(a)) ]=_{\text{Fonction}} 1$ avec $\chi : A \times A \to \{0,1\}$ la fonction caractéristique de la diagonale.

" Démonstration " :
sous l'hypothèse que $=_Y \circ (f \times g) = \text{True}$, je vais utiliser la propriété universelle du produit fibré, la flèche $f \times g : X \to Y \times Y$ et la flèche $1 : X \to 1$ vérifie $=_Y \circ (f \times g) = \text{True} \circ 1$ (c'est l'hypothèse) donc il existe une flèche (unique, en pointillé) $(f \times g) \times_\Omega 1 : X \to Y$ tel que $f \times g = \Delta \circ (f \times g) \times_\Omega 1$.
$$
\xymatrix {
X \ar@{->}[ddr]_{f \times g} \ar@{-->}[dr] \ar@{->}[rrd]^{1}&& \\
&Y \ar@{->}[d]^{\Delta} \ar@{->}[r] & 1 \ar@{->}[d]^{ \text{True}}\\
& Y \times Y \ar@{->}[r]_{=_Y} &\Omega
}
$$

Mais comme $\pi_1 \circ \Delta = \pi_2 \circ \Delta$ ($\pi$ c'est les projections selon les facteurs) ,on obtient :
$$
f = \pi_1 \circ (f \times g) = \pi_1 \circ \Delta \circ (f \times g) \times_\Omega 1 = \pi_2 \circ \Delta \circ (f \times g) \times_\Omega 1 = \pi_2 \circ (f \times g) = g
$$

Réciproquement, si $f =g$ alors $\Delta \circ f = f \times g$ car $\pi_1 \circ \Delta \circ f = f$ et $\pi_2 \circ \Delta \circ f = f= g$ (hypothèse), de sorte que le diagramme commute :
$$
\xymatrix {
X \ar@{->}[ddr]_{f \times g} \ar@{->}[dr]^f && \\
&Y \ar@{->}[d]^{\Delta} \ar@{->}[r] & 1 \ar@{->}[d]^{ \text{True}}\\
& Y \times Y \ar@{->}[r]_{=_Y} &\Omega
}
$$
et $=_Y \circ (f \times g)$ passe par $1$.

Une question, bon je pense que j'ai fais plus fleuve que toi :-D, dans le post de Claude ici le 3) on voit que Claude code les faces d'un cube comme des application $F : \{1,\dots,n\} \to \{ 0,1, \infty\}$, il faut considérer celà via le couple $(f^{-1} \{0,1\}, F_{\mid f^{-1} \{0,1\}})$, je pense qu'on peut voir les choses concernant le cube via un topos avec $\Omega = \{ 0,1, \infty \}$ ... trois valeurs de vérité ? J'ai trouvé, dans le livre de Saunders Mac Lane page 105-106 de Category for working mathematician, qui ressemble un peu mais je n'arrive pas à faire le lien !

GaBuZoMeu · February 2018

@GA :

Il y a deux choses :
1°) Les topos permettent d'interpréter tout langage du premier ordre. Les topos permettent aussi d'interpréter le langage de la théorie intuitionniste des types (ou arithmétique intuitionniste d'ordre supérieur) et fournissent une sémantique pour cette dernière. Je joins au message un article dont la première partie explicite cette affirmation.
2°) À un topos (ou une catégorie avec moins de structure) on peut associer son langage de Mitchell-Bénabou qui a un type de variable pour chaque objet du topos, un symbole fonctionnel pour chaque flèche, éventuellement des symboles de relation pour les sous-objets etc., (à préciser et affiner). Il y a bien sûr une interprétation canonique de ce langage dans le topos en question. On écrit des démonstrations avec des formules dans ce langage (dans un système de déduction correct) et on démontre ainsi des propriétés catégoriques, de manière peut-être plus proche des habitudes mathématiques qu'en raisonnant sur des diagrammes.

christophe c · February 2018

@GA: comme je te l'avais dit dans un autre fil, je te le redis là

GBZM a écrit:

Les topos permettent d'interpréter tout langage du premier ordre

Cette remarque est suffisante pour jouer et s'éclater car par exemple, ZFC est une théorie du premier ordre (et NBG est carrément à peu près la même théorie, mais ne contient "qu'un seul axiome").

Tu peux donc demander à ton topos préféré (et même à ta catégorie cartésienne fermée préférée***) si elle pense que ses modèles de ZF pensent que les chats miaulent par exemple :-D

*** à condition d'avoir initialisé avec "une" flèche "=" (tu peux prendre n'importe laquelle, mais évidemment, les réponses peuvent être exotiques si tu choisis une flèche que tu nommes "=" mais qui n'a rien de sympathiquement similaire avec une "bonne flèche =

GaBuZoMeu · February 2018

Je sais bien que $ZFC$ est une théorie du premier ordre.
Mais ça ne présente pas grand intérêt, à mon avis, de chercher des modèles de cette théorie du premier ordre dans un topos (un objet avec une relation binaire etc.). C'est en quelque sorte "contre nature".
Ce qui est bien plus pertinent est effectivement d'interpréter la théorie intuitionniste des types dans un topos, de la façon décrite par l'article que j'ai joint. C'est dans ce cadre qu'on construit alors un objet $\R$ (réels de Dedekind) et qu'on peut se demander si toute flèche $\R\to \R$ est une fonction continue.

Georges Abitbol · February 2018

@moduloP : Ca va me prendre un moment de tout lire

@GaBuZoMeu :

GBZM a écrit:

Les topos permettent d'interpréter tout langage du premier ordre.

C'est ce dont vous parlez après avec Christophe ? Effectivement, cela ne m'intéresse pas de considérer des "objets univers d'ensembles" dans des topos, au sens de l'internalisation (voir ici, sur nLab). Enfin, en tout cas, je ne pense pas que ça m'avance à quoi que ce soit pour ma question précise.

GBZM a écrit:

Les topos permettent aussi d'interpréter le langage de la théorie intuitionniste des types (ou arithmétique intuitionniste d'ordre supérieur) et fournissent une sémantique pour cette dernière.
(...)
C'est dans ce cadre qu'on construit alors un objet $\mathbf{R}$ (réels de Dedekind) et qu'on peut se demander si toute flèche $\mathbf{R}\rightarrow \mathbf{R}$ est une fonction continue.

Bon, ben là, je pense que c'est vraiment ça qui va m'intéresser.
1) Quand je tape "théorie intuitionniste des types", je ne tombe que sur des trucs en anglais qui disent que c'est Martin-Löf qui l'a inventée mais je trouve que l'article wikipédia n'est pas clair du tout.
2) Merci pour le document ! Ca ressemble à ce que je voudrais, mais pas tout à fait ! Pourquoi n'y a-t-il pas, pour des types $A$ et $B$, un type $A \otimes B$ qui serait le type des "couples de termes $A$ et $B$" ? Je voudrais bien qu'il y en ait, et qu'il y ait plus d'axiomes !
3) Pour cette histoire de fonctions continues, si la théorie intuitionniste des types est vraiment le truc que je voulais écrire dans mon premier post de ce fil, alors je voudrais arriver à démontrer que la phrase "il existe des fonctions $\mathbb{R} \rightarrow \mathbb{R}$ non continues" n'est pas démontrable en théorie intuitionniste des types.
En fait ce que je veux, c'est écrire soigneusement une théorie $T$, avec tous ses axiomes, qui, subjectivement, me paraisse ressembler à une "théorie intuitionniste des ensembles", et me rendre compte que ce que font MacLane et Moerdjik dans leur bouquin, c'est de démontrer que $T$ ne démontre pas l'existence de fonctions non continues.

GBZM a écrit:

Il y a bien sûr une interprétation canonique de ce langage dans le topos en question.

C'est un peu pour ça que je dis plus haut que je trouvais que le langage de Mitchell-Bénabou ressemblait plus pour moi à une sémantique qu'à une syntaxe !

4) Pourquoi choisis-tu de séparer tes points 1) et 2) ? N'est-ce pas en utilisant le langage de Mitchell-Bénabou qu'on fournit la sémantique de la théorie intuitionniste des types dans un topos ?

@Christophe : Cf ma réponse à GaBuZoMeu. Dans l'autre post, je n'avais pas très bien compris que ce tu voulais faire... Mais maintenant, j'ai compris (enfin, je pense, dis-moi si je me trompe !) : tu parles de prendre (à supposer qu'il existe !) un objet $U$ particulier d'un topos, et de prendre un sous-objet particulier $Appartenance$ de $U \times U$ le tout supposé satisfaire un certain nombre de choses de déclarer : le couple $(U,Appartenance)$ est un "univers d'ensembles interne à mon topos", et de regarder ce qui lui arrive. Ce n'est pas du tout ce que je veux faire !
Pour moi, tout (j'espère !) topos $T$ est lui-même ce "univers d'ensembles un peu bizarre", car il possède déjà une famille de sous-objets $\in_A$ de $A \times \Omega^A$ et c'est cette famille $(\in_A)_{A \in T}$ que je veux étudier. Tout ceci est, à mon sens, la sémantique d'un certain langage, que je cherche à expliciter. Et la théorie correspondante, c'est ce que tu évoquais quand tu disais que les topos ne peuvent pas parler d'énoncés à quantifications non bornées, ou quelque chose comme ça.

EDIT : Rajout d'un oubli gênant en gras !

christophe c · February 2018

GBZM a écrit:

Ce qui est bien plus pertinent est effectivement d'interpréter la théorie intuitionniste des types dans un topos, de la façon décrite par l'article que j'ai joint. C'est dans ce cadre qu'on construit alors un objet IR (réels de Dedekind) et qu'on peut se demander si toute flèche IR ---> IR est une fonction continue.

Sur le plan technique, je veux bien, mais sur un plan plus platonicien (je veux dire si on veut répondre à "est-ce que dans un "vrai" monde intuitionniste, on ne peut pas prouver l'existence de fonctions discontinues, etc") , c'est moins satisfaisant parce qu'il y a "peu de fonctions" toposiquement parlant (ou pour le dire plus correctement, rien n'assure qu'on les ait toutes en un sens suffisamment satisfaisant).

Bon, après, de par l'article de (Forman? 19980 je crois?), les topos de Grothendieck sont peut-être un peu plus satisfaisant? En bref, il y a des interrogations qui demeurent.

Je prends un exemple (je ne sais pas si c'est vrai). Admettons que $V^T$ **vérifie "il existe une fonction discontinue blabla" alors que la négation de cet énoncé est consistant toposiquement, la question est "quel paradigme parmi ces 2 donne la réponse la plus significative?".

** J'ai noté $V^T$ l'extension intuitionniste de l'univers $V$ où $T$ est une topologie au sens du forcing. Est-ce que toutes les fonctions de $V^T$ sont des flèches?

GaBuZoMeu · February 2018

@Georges, pour tes questions :

2) Pourquoi pas de type produit ?
On peut ajouter cette construction de types mais il n'y en a pas besoin, vu qu'il y a déjà une construction du "type des parties d'un produit de types".
Autrement dit si tu as un type $\tau_1$ et un type $\tau_2$, tu as par compréhension et extensionalité :
$$\vdash \exists! X\ \forall x\ (Xx\leftrightarrow \exists!y\ \exists!z\ xyz)$$
où $y$ est de type $\tau_1$, $z$ de type $\tau_2$, $x$ de type $[\tau_1,\tau_2]$ et $X$ de type $\tau_1,\tau_2$. Avec ça tu as tout ce qu'il faut (les projections sur chacun des facteurs, la propriété universelle ...). Dans la formulation avec termes d'abstraction, c'est le terme $\lambda x\ (\exists!y\ \exists!z\ xyz)$ de type $\tau_1,\tau_2$ qui joue le rôle du produit de types.

3) Je pense que tu voulais dire "Si la théorie intuitionniste des types démontre que le terme $f$ de type $[\R,\R]$ est une fonction totale de $\R$ dans $\R$, alors elle démontre aussi q:ue $f$ est continue". Ceci revient à dire que dans le topos initial avec objet des entiers naturels (section 1.2.3 du papier), toute flèche $\R\to \R$ est continue.

4) Non. Dans le langage de Mitchell-Bénabou associé à un topos, il y a un type pour chaque objet. Ce n'est pas le cas pour la théorie intuitionniste des types

@Christophe : désolé, je ne comprends pas trop ce que tu écris et je ne vois pas où tu vas.

Georges Abitbol · February 2018

@GaBuZoMeu : Ok pour 2). Pour 3), non, ce n'est pas ce que je voulais dire, je voulais vraiment dire ce que j'ai écrit. Pour 4), je ne comprends pas. Je vais lire plus tranquillement l'article, parce que j'ai peur d'avoir fait un contresens.

GaBuZoMeu · February 2018

Hum Georges, relis-toi. Tu voudrais vraiment démontrer "que la phrase "il existe des fonctions $\mathbb R\to \mathbb R$" n'est pas démontrable en théorie intuitionniste des types."

christophe c · February 2018

@GBZM, je suis hélas un peu pressé présentement, je vais être un poil plus rigoureux.

Soit $T$ une topologie. En notant, comme je l'ai souvent raconté $val([a\in b]):=$ la réunion des éléments $x$ de $T$ tels que $(a,x)\in b$, puis en définissant $val(A\to $ et $val(\forall xR(x))$ comme tu imagines on obtient un modèle vérifiant la logique intuitionniste et les axiomes de ZF sauf l'extensionnalité. Moyennant un petit quotientage routinier, on obtient un modèle de ZF (intuitionniste).

Cela fait deux cadres pour se demander si la théorie intuitionniste des ensembles démontre ceci ou cela. Et ce que je dis est que je ne sais pas s'ils sont équivalents pour par exemple répondre à GA sur l'énoncé qui l'intéresse (sur les fonctions continues).

Je n'ai jamais pris le temps de vérifier s'ils sont équivalents et ils ne me semblent pas que l'article de Forman répond de mémoire, mais je me trompe peut-être.

Remarque: ce que je raconte en italique est tout bêtement la notion de forcing découverte par Cohen.

GaBuZoMeu · February 2018

Désolé Christophe, je ne comprends pas ce que tu écris en italiques et je n'imagine rien (sauf comment définir la valeur de $A\to B$ comme ouvert d'une topologie si on a déjà les valeurs de $A$ et de $B$ comme ouverts de cette topologie).

Georges Abitbol · February 2018

@GaBuZoMeu : Hahahahaha, j'ai oublié "non continues" !

GaBuZoMeu · February 2018

Il me semble plausible de $HA_\omega$ ne sache prouver l'existence de quelque chose qu'en en fournissant un exemplaire (mais je n'en mettrais pas ma main au feu). Si c'est vrai, ce que tu voudrais démontrer n'est pas très loin de ce que je propose !

Georges Abitbol · February 2018

Je ne dois pas m'être bien exprimé. Dans le topos décrit par MacLane et Moerdjik dans leur livre, il est démontré que la phrase "toutes les fonctions sur les réels (de Dedekind) vers eux-mêmes sont continues" est vraie au sens de l'interprétation canonique de la phrase naturelle qui exprime ça dans le langage de Michell-Bénabou ; or, je vois ce dernier comme la sémantique d'un langage que j'appelle "langage de la TTBE" plus haut.

Maintenant, si je me choisis un ensemble $E$ quelconque d'énoncés du langage de la TTBE qui sont interprétés comme vrais dans le topos de MacLane et Moerdjik (ou même dans tous les topos), alors la discussion précédente démontre que $E$ ne démontre pas $\exists f : \mathbf{R} \rightarrow \mathbf{R}\quad f \mbox{ n'est pas continue}$, n'est-ce pas ?
Si j'arrivais à trouver un $E$ qui ressemble suffisamment à une sorte de ZF intuitionniste, je serais satisfait.

Est-ce que mon envie est claire ?

EDIT1 : Rajout du gras.
EDIT2 : Rajout de l'EDIT 1 :-D

GaBuZoMeu · February 2018

Fais attention à ce que tu écris. Si tu écris "$f$ est continue" alors que tu penses vraisemblablement écrire "$f$ n'est pas continue", ça ne rend pas la communication très facile.

Georges Abitbol · February 2018

Ouhlala misère... Lors de la rédaction de mes messages, je change souvent d'avis et de formulation, et j'oublie d'apporter les modifications nécessaires. Je me relirai, la prochaine fois, promis !

christophe c · February 2018

De mon téléphone paaardon j'ai sûrement laisse des posts sans réponse. @GBZM : tu sais aussi que val de "pour tout x R(x) est l'intérieur de l'intersection de tous les ouverts val de R(a) quand a parcourt tout l'univers.

Mais quand tu as parlé de HA indice oméga je ne sais pas si tu t'adressais à moi. Et je ne sais pas ce qu'est ce HA... (J'avoue c'est peut être une lacune).

christophe c · February 2018

Je suis un peu "overbooké" en ce moment

GaBuZoMeu · February 2018

$HA_{\omega}$ est la théorie intuitionniste des types, ou arithmétique intuitionniste d'ordre supérieur, ou autre nom, décrite dans le papier que j'ai attaché à un message plus haut.

christophe c · February 2018

Merci gbzm. Je vais essayer de télécharger le pdf. Sinon demain d'un PC je re essaierai . Mais je pense voir de quoi il s'agit.

christophe c · February 2018

Je suis allé voir le pdf et oui, j'avais bien compris. J'ai juste un peu de mal (enfin m'a fallu du temps) à capter que $[t_1,..,t_n]$ désignait $\Omega^{t_1\times t_2\times ...\times t_n}$ :-D où $\Omega$ est "le type des valeurs de vérité".

Bin, du coup tu as compris le forcing. Ca consiste juste à remplacer $\omega$ par $ON$ où $ON$ désigne la classe des ordinaux. Il n'y a rien de plus dans le forcing. (enfin le forcing traditionnel agit en logique classique bien sûr, mais rien n'interdit de le faire danser en logiques quelconques).

Ca me fait aussi penser que ton affirmation dont tu dis que tu dis que c'est "plausible" doit probablement avoir le mérite de posséder une réponse connue, avec probablement un article de recherche officiellement attaché et un auteur. Par contre, de là à trouver date et journal... Je serais tenté de dire que "sinon, ce serait un problème ouvert de première importance".

GaBuZoMeu · February 2018

Je ne vois pas quel est le sens de "remplacer $\omega$ par $ON$".

Sinon, pour le résultat que je juge plausible, je sais où il faudrait le chercher : dans la thèse de Girard. Mais, par contre, je ne sais pas si je l'ai encore et, si oui, où elle se trouve dans mes archives.

christophe c · February 2018

Merci pour le tuyau, je peux essayer de contacter des amis pour savoir si elle est en ligne sous une forme ou une autre. Pour dépasser $\omega$, c'est juste la hiérarchie cumulative (enfin je ne sais pas si c'est son vrai nom):

$W_{\alpha+1} := \Omega^{W_\alpha}$

$W_\alpha := \Omega ^{\cup_{\beta<\alpha} W_\beta }$ pour $\alpha$ limite.

Mais en fait, tout ceci suppose un univers "bien fondé" alors qu'il n'y en a nullement besoin, ni nullement besoin de faire des "constructions par récurrence ordinale", qui sont juste là pour "donner l'intuition de consistance".

In fine, on regarde les ensembles comme des noms de fonctions à valeurs dans $\Omega$ et pour appliquer un ensemble à un autre, on prend (par exemple) $a(b):=$ la borne sup des éléments $x$ de $\Omega$ tels que $(a,x)\in b$. (Il faut que $\Omega$ soit ordonné complet pour faire sens, mais dans tes contextes à toi par exemple, $\Omega$ est une algèbre de Heyting).

Dans le cas où $\Omega=\{vrai; faux\}$, ça revient juste à prendre les indicatrices plutôt que les ensembles.

christophe c · February 2018

@GBZM, j'ai oublié de préciser que je "sémantise" donc ne suis pas dans la démarche syntaxique que tu as utilisé (tu parles d'une théorie, j'ai répondu sans prévenir par des "modèles", pardon). Bon, je le précise surtout pour les lecteurs, toi, je pense que tu avais deviné ce tacite.

Dans le cas, pour "dépasser petit omega" avec des (gros) topos (ie de la même hauteur que l'univers par exemple), on peut de toute façon remplacer union par limite, mais n'étant pas un prof des limites et surtout des notations, j'ai répondu avec un "cup".

D'ailleurs, en tapant ces lignes, je m'aperçois que un énoncé comme le suivant exige probablement qu'on se place dans un topos (ou une catégorie) que l'on SUPPOSE "assez complète" (par exemple stable par "petites limites"):

Soit $C$ une catégorie, $E$ un objet de $C$ et $S$ un ensemble de flèches de but $E$. De plus on note $<<f \le g>>$ pour abréger $<<$ il existe une flèche $h$ allant de la source de f vers la source de g telle que $f= g\circ h>>$.
Sans même parler d'unicité, l'existence d'un plus petit minorant pour $S$ est rigolo. Je pense qu'on peut le prouver dans les topos ayant toutes les petites limites, mais comme j'ai mis "flèches" exprès à la place de monomorphismes :-D ... les diverses catégories où l'exercice est faisable donnent surement un exercice plus difficile qu'avec monomorphisme à la place de flèche dans l'énoncé

(Pour les lecteurs béotiens, on fait comme si les flèches sont des fonctions, leur image directe des ensembles et c'est une notion de "réunion" qui est évoquée ici en parlant du plus petit minorant).

christophe c · February 2018

Juste une remarque en passant: il y a au moins deux situations (+ une troisième amusante + une 4ième) où le fait d'avoir prouvé $\exists xR(x)$ va donner "presque" $a$ tel que $R(a)$.

1/ Quand la topologie est compacte, on sait qu'alors, dans chaque histoire il y a une liste finie $[a_1;\ldots;a_n]$ telle que : $$R(a_1) \cup \cdots \cup R(a_n) = Vrai$$
2/ Pour des topologies très spécifiques, on peut même se ramener à un singleton, sans pour autant les choisir classiques. Par exemple, on prend un ordinal $k$ et les ouverts sont les segments finaux de $k$. Dans ce cas, dans toute histoire, il y a $a$ tel que $R(a)$ a la valeur VRAI à lui tout seul.

3/ Si on prend un ordinal $k$ et la topologie composée par les segments initiaux, on obtient un modèle qui vérifie le buveur: C'est à dire l'énoncé : $$\forall R\exists x\forall y: [R(x)\to R(y)]$$
4/ Soit $E$ un ensemble, $e\in E$ et $T$ une topologie telle que tout élément $X$ de $T$ tel que $e\in X$ vérifie $X=E$ (par exemple situation 2). Appelons ça un espace goguenard. Est-ce que la classe des espaces goguenards est complète pour la logique intuitionniste ? Si oui, ton pari déclaré plausible est gagné (mais bon, ce sont quand-même des espaces bien particuliers :-D )

GaBuZoMeu · February 2018

Je ne vois pas du tout, mais alors pas du tout, la plausibilité du résultat dans les histoires topologiques, mais dans l'élimination des coupures, ou via CCH dans la normalisation forte démontrée par Girard dans sa thèse.

christophe c · February 2018

Oui bien sur je faisais juste des remarques un peu périphériques. Mais attentin j'ai toujours eentendu dire que JYG prouve la forte normalisation de F (îe l'arithmétique intuitionniste du SECOND ordre). Or ça entraine sa consistance. Idem chaque fois qu'on itére d'un ordre la consistencystrength augmente. Donc il faut SUPPOSER chaque fois platoniciennement un axiome plus fort donc la sémantique joue son rôle assez pleinement. Mais peut être a-t-il construit dans sa thèse un "truc" un peu uniforme.

Par contre par Tychonov et dedoublement s répétés je pense que la logique de la classe des compacts vérifie ton énoncé. Mais je ne sais pas où se situe cette logique entre l'intuitionnisme et le classique.

christophe c · February 2018

GBZM a écrit:

l'existence de quelque chose qu'en en fournissant un exemplaire

VS

GBZM a écrit:

mais dans l'élimination des coupures, ou via CCH dans la normalisation forte démontrée par Girard dans sa thèse.

En fait (hélas je suis un peu à la bourre tout le temps en ce moment, car je n'ai pas internet chez moi), je pense que tu as raison, mais que c'est beaucoup, beaucoup plus simple que la preuve de normalisation de F. C'est essentiellement dû, me semble-t-il, à la "nature" de la logique intuitionniste.

Bon , n'ayant que peu de temps, je résume:

1/ Les divers schémas de compréhension sont "blancs" en ce sens qu'on les réalise de l'extérieur avec le combinateur identité.
2/ En notant (disons que c'est un succédané CCH qui est faite pour la logique classique, sa partie intuitionniste est généralement considérée comme triviale et bien comprise):

2.1/ (A=>B) := ensemble des garanties g telles que pour tout h dans A, g*h est dans B
2.2/ $\forall xR(x):=$ ensemble des garanties qui sont dans tous les $R(a)$
2.3/ $\exists xR(x):=$ la réunion de $R(a)$
2.4/ etc, etc, avec "ou" et "et"

a priori, toute preuve d'un ensemble de garanties lu comme une phrase formelle sur le papier est une garantie appartenant à l'ensemble (à vérifier méticuleusement, mais seule le RPA fait "sauter" ce verrou je crois). Dès lors, une garantie se situant dans $\exists xR(x)$ se situe par définition dans l'un des $R(a)$, donc "prouve" $R(a)$, mais, il y a un poil (pas grand chose) à vérifier pour que réciproquement on obtienne que les garanties se retransforment en preuves.

L'élimination des coupures peut souvent se montrer un peu de la même façon, sauf que c'est souvent plus dure, puisque les ensembles ne sont pas des ensembles de termes "normaux". Ici ça ne compte pas vraiment me semble-t-il.

Ce qu'interprètent les topos

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 4