Comments on Introduction aux mathématiques constructives : 1. un peu de théorie des ensembles

En fait, j'ai la réponse, ce n'est pas prouvable. Sur le nLab <URL:https://ncatlab.org/nlab/show/surjection#in_dependent_type_theory>, il est mentionné que ça implique UIP/K, sans plus d'explications (or l'extensionnalité fonctionnelle toute seule n'implique certainement pas UIP). J'ai su le prouver dans un cas particulier, reste à simplifier parce que j'ai probablement cherché beaucoup trop compliqué, et à faire le cas général, mais je suis déprimé et crevé, donc j'en reste là pour maintenant.

(Enfin, quand même, youhou parce que c'est la première fois que j'arrive vraiment à prouver quelque chose en théorie des types à l'aide d'une intuition géométrique d'homotopie…)

Axiom funext :
forall (A B : Type) (f f' : A -> B),
(forall x, f x = f' x) -> f = f'.

Definition surjective {A B : Type} (f : A -> B) :=
forall y, exists x, y = f x.

Definition epi {A B : Type} (f : A -> B) :=
forall (C : Type) (g g' : B -> C),
((fun x => g (f x)) = (fun x => g' (f x))) -> g = g'.

Lemma surjections_are_epi {A B : Type} (f : A -> B) :
surjective f -> epi f.
Proof.
intros H_surj C g g' H_eq. apply funext.
intros y. destruct (H_surj y) as [x Hx].
rewrite Hx. change ((fun x => g (f x)) x = (fun x => g' (f x)) x).
rewrite H_eq. reflexivity.
Qed.

Axiom epis_are_surjective :
forall (A B : Type) (f : A -> B),
epi f -> surjective f.

Lemma epi_convenience {A B : Type} (f : A -> B) :
epi f ->
forall (C : Type) (g g' : B -> C),
(forall x, g (f x) = g' (f x)) -> g = g'.
Proof.
intros H_epi C g g' H_eq. apply funext in H_eq. apply H_epi, H_eq.
Qed.

Definition eq_functoriality
{X Y : Type} {x1 x2 : X} (E : x1 = x2) (f : X -> Y) : f x1 = f x2
:= match E in (_ = x2') return (f x1 = f x2') with eq_refl _ => eq_refl (f x1) end.

Lemma eq_functoriality_id
{X : Type} {x1 x2 : X} (E : x1 = x2) : eq_functoriality E (fun x => x) = E.
Proof.
destruct E. reflexivity.
Qed.

Lemma eq_functoriality_const
{X Y : Type} {x1 x2 : X} (E : x1 = x2) (y : Y) : eq_functoriality E (fun x => y) = eq_refl y.
Proof.
destruct E. reflexivity.
Qed.

Definition concat {X : Type} {x1 x2 x3 : X} (E1 : x1 = x2) (E2 : x2 = x3) : x1 = x3
:= match E2 in (_ = x3') return (x1 = x3') with eq_refl _ => E1 end.

Definition rev {X : Type} {x1 x2 : X} (E : x1 = x2) : x2 = x1
:= match E in (_ = x2') return (x2' = x1) with eq_refl _ => eq_refl x1 end.

Lemma concat_assoc {X : Type} {x1 x2 x3 x4 : X} (E1 : x1 = x2) (E2 : x2 = x3) (E3 : x3 = x4)
: concat E1 (concat E2 E3) = concat (concat E1 E2) E3.
Proof.
destruct E1, E2, E3. reflexivity.
Qed.

Lemma concat_id_left {X : Type} {x1 x2 : X} (E : x1 = x2) : concat (eq_refl x1) E = E.
Proof.
destruct E. reflexivity.
Qed.

Lemma concat_rev_right {X : Type} {x1 x2 : X} (E : x1 = x2)
: concat E (rev E) = eq_refl x1.
Proof.
destruct E. reflexivity.
Qed.

Lemma concat_rev_left {X : Type} {x1 x2 : X} (E : x1 = x2)
: concat (rev E) E = eq_refl x2.
Proof.
destruct E. reflexivity.
Qed.

Lemma concat_inj_right {X : Type} {x1 x2 x3 : X} (E1 E2 : x1 = x2) (E3 : x2 = x3)
: concat E1 E3 = concat E2 E3 -> E1 = E2.
Proof.
intros H.
replace E1 with (concat E1 (concat E3 (rev E3))).
replace E2 with (concat E2 (concat E3 (rev E3))).
repeat rewrite concat_assoc. rewrite H. reflexivity.
rewrite concat_rev_right. reflexivity.
rewrite concat_rev_right. reflexivity.
Qed.

Lemma concat_inj_left {X : Type} {x1 x2 x3 : X} (E1 : x1 = x2) (E2 E3 : x2 = x3)
: concat E1 E2 = concat E1 E3 -> E2 = E3.
Proof.
intros H.
replace E2 with (concat (concat (rev E1) E1) E2).
replace E3 with (concat (concat (rev E1) E1) E3).
repeat rewrite <- concat_assoc. rewrite H. reflexivity.
rewrite concat_rev_left. apply concat_id_left.
rewrite concat_rev_left. apply concat_id_left.
Qed.

Proposition subsingleton_K
{X : Type} {H_subsingleton : forall x1 x2 : X, x1 = x2}
{x : X} (E : x = x) : E = eq_refl x.
Proof.
set (f := fun (u : unit) => x).
assert (f_surj : surjective f). { intros y. exists tt. apply H_subsingleton. }
assert (f_epi : epi f). { apply surjections_are_epi, f_surj. }
set (g := fun (x : X) => x).
set (g' := fun (y : X) => x).
assert (H : forall u : unit, g (f u) = g' (f u)). { intros []. reflexivity. }
apply (epi_convenience f f_epi) in H.
rewrite <- (eq_functoriality_id E). fold g.
rewrite <- (eq_functoriality_const E x). fold g'.
set (general_functoriality := fun (h : X -> X) => concat (H_subsingleton x (h x)) (concat (eq_functoriality E h) (H_subsingleton (h x) x))).
assert (H2 : general_functoriality g = general_functoriality g'). { rewrite H. reflexivity. }
unfold general_functoriality, g, g' in H2.
apply concat_inj_left in H2. apply concat_inj_right in H2.
apply H2.
Qed.

@Thierry : Bonne question ! Elle ressemble pas mal à ma question <URL:https://mathoverflow.net/questions/486335/diaconescus-theorem-in-type-theory-without-propositional-extensionality>.

Je suis à peu près sûr que non (« toute fonction simplifiable à droite est surjective » n'est pas prouvable en Coq avec seulement l'extensionnalité fonctionnelle et pas l'extensionnalité propositionnelle), mais je ne sais pas le prouver. Le problème principal étant que je ne comprends pas les modèles qui ne satisfont pas l'extensionnalité propositionnelle. Mais la personne de pseudo « aws » donne dans les commentaires sur cette question MathOverflow une référence pour un modèle de réalisabilité qui fait ça, il faudrait peut-être regarder par là.

En essayant de comprendre si la propriété « toute fonction simplifiable à droite est surjective » est prouvable en Coq/Rocq (et avec quels éventuels axiomes), j'ai l'impression qu'en théorie des types, les deux occurrences de raisonnement classique que tu mentionnes en rouge dans ta première preuve n'ont pas le même statut : le « donc » à la fin utilise le tiers exclu propositionnel (en Coq : forall p: Prop, p \/ ~p), mais le « [1 sur y] et 0 ailleurs » suppose que l'égalité sur Y est décidable (en Coq : forall x y: Y, {x = y} + {x <> y}). Une façon qui me paraît naturelle de se passer de cette décidabilité donne d'ailleurs un intermédiaire entre ta preuve classique et ta preuve constructive nº2 : on prend Z=Ω (autrement dit, Prop), et g':y'↦y=y'. On se retrouve alors à devoir prouver que False = (y = f x), alors qu'on a seulement ~(y = f x), ce qui requiert l'axiome d'extensionnalité propositionnelle (forall A B, (A <-> B) -> A = B). En utilisant l'idée de ta preuve constructive nº2, on se passe du tiers exclu, mais on a toujours besoin de l'extentionnalité propositionnelle. Je me demande s'il existe une façon de s'en passer.

Je ne comprends pas en quoi un sous-singleton n'est pas exactement un singleton. Par définition il est habité car ∃x∈E, et il est trivial de prouver que poyr deux éléments quelconques y et y', y = x = y'.
Donc il est havité et sous-terminal, donc c'est un singleton. Ou j'ai très mal compris cette entrée.

Ok, merci c'est très clair et instructif. Ce qui me manquait (outre la maîtrise des règles pour établir une quantification existentielle), c'était cette distinction entre l'admissibilité de l'admettre pour les ensembles via la variable x mais pas pour leurs propriétés.

@Dyonisos : Un ∃ prend la forme « ∃ <variable>, <formule> », signifiant « il existe <variable> qui vérifie <formule> », ou bien par raccourci de notation, « ∃ <variable> ∈ <ensemble>, <formule> », signifiant « il existe <variable> dans <ensemble> qui vérifie <formule> », ce qui est équivalent à « ∃ <variable>, <variable> ∈ <ensemble> et <formule> » soit « il existe <variable> tel que <variable> appartient à <ensemble> et vérifie <formule> ». Exemples : ∃ x, ∀ y, y ∉ x affirme l'existence d'un ensemble qui est vide, et ∃ x ∈ ∅, ⊤ dit que l'ensemble vide a un élément (et est donc fausse).

La formule ∃ {● : p} n'a pas de sens, elle n'est pas bien formée, de même que « il existe quatre » ne veut rien dire en français (tu peux dire « il existe un chat », avec un article indéfini, mais pas « il existe le chat Grosminet » avec un article défini, par contre tu peux dire « il existe un chat qui s'appelle Grosminet »).

En revanche, la formule ∃ x, x ∈ {● : p} (il existe x tel que x appartient à {● : p}), ou encore ∃ x ∈ {● : p}, ⊤ (il existe x dans {● : p} tel que « vrai »), est bien formée, et est justement équivalente à p, c'est tout l'intérêt de la construction. Et elle ne pose aucun problème même si on est en logique du premier ordre, car on se place dans la théorie des ensembles, qui permet bien de parler de {● : p} et d'appartenance ∈, et de quantifier sur les ensembles.

On peut très bien quantifier à l'intérieur de n'importe ensemble, c'est parfaitement autorisé, on ne peut juste pas nativement quantifier sur les propriétés des ensembles (mais ce n'est pas grave car on s'en sort en quantifiant juste sur les ensembles d'ensembles, qui sont en fait la même chose que les ensembles en général).

@Ruxor : Bon, si ça t'agace que j'en rajoute à tes explications, n'hésite pas à le dire. (Flashback de souvenirs de lycée où il m'est arrivé de répondre spontanément à la place du prof aux questions posées par d'autres élèves, à des moments pas forcément appropriés, ce qui a causé quelques froncements de sourcils…)

J'ai oublié de répondre à l'histoire du non-non-séparé mais oui, tu as raison, ce serait une mauvaise idée de dire ça, je n'avais pas réalisé.

Et en me relisant, je ne suis plus si enthousiasmé par ma version du théorème d'involution de Higgs ('fin, c'est juste une bête reformulation, quoi, même si ma preuve Coq est joliment symétrique), mais bon, reste que ça me semble lumineux maintenant alors que c'était complètement obscur à la première lecture. Une partie de l'effet psychologique, c'est que j'ai une intuition de Prop en Coq, alors que j'ai zéro intuition du classificateur de sous-objet dans un topos, je connais à peine la définition. (Au passage, le `Require Import RelationClasses.` n'est pas nécessaire, j'ai oublié de le supprimer.)

Je crois que je comprends désormais l'essentiel par rapport à mes difficultés antérieures. C'est vraiment cool d'avoir passé du temps à m'expliquer. Il y a un tout dernier point où j'ai une idée que je crois juste sans en être tout à fait certain. Pour expliciter pourquoi je pensais que l'expression {● : p} était davantage un terme qu'une proposition, j'ai, dans un décalque sauvage du langage courant, utilisé une formule comme ∃ {● : p}. Or, si je ne me trompe pas dans l'interprétation de la portée des remarques de Jeanas sur les contraintes liées au fait qu'on évolue dans un contexte de logique du premier ordre, je me dit qu'en fait justement on ne peut pas quantifier existentiellement dans un ensemble défini en relation avec une proposition. De la sorte, ça pourrait entrer en résonance avec l'idée qu'on se donne un ensemble permettant plus ou moins de manipuler tout de même des propositions, mais sans cet élément essentiel des propositions qu'est la valeur de vérité de p. C'est juste ?

Thanks !

@ Ruxor et jeanas : ok merci pour toutes ces précisions. Encore une remarque @ jeanas : quand tu écris " le {● : p} est une conversion d'une proposition en un ensemble qui représente sa valeur de vérité", est-ce qu'il faut tout de même considérer que {● : p} s'apparente davantage à un terme qu'à une proposition ? Après tout, si je pense ou écris "cheval" ou "Père Noël", ce n'est ni vrai ni faux, ça dépend de la façon dont ces termes vont fonctionner dans une proposition. Et c'est comme ça que je comprends que {●} est un terme, on n'a pas écrit par exemple ∃ {●} qui lui est soit vrai soit faux en logique classique. Mais alors pourquoi ne pas penser qu'on n'a pas écrit par exemple ∃ {● : p} mais seulement {● : p}, pas une proposition mais un terme, et, dès lors, qu'est-ce que ça signifie réellement que de convertir une proposition dans un terme ?? Un ensemble qui représente sa valeur de vérité, ça reste un concept, une idée, pas une proposition susceptible d'être soit vraie soit fausse, non ?

@Dyonisos : Une intuition que je peux rajouter, pour donner un peu de recul sur le « mais pourquoi diable », c'est que la théorie des ensembles se fait dans une logique (appelée logique du premier ordre) qui est plutôt faible. Du coup, on compense la faiblesse de cette logique par une théorie très forte (la théorie, c'est les axiomes qu'on se donne), et certaines choses qu'on ne peut pas avoir au niveau logique, on les obtient par une traduction dans les ensembles.

Typiquement, la logique du premier ordre te permet d'écrire « pour tout objet x, … » mais pas « pour toute propriété P des objets, … ». Par exemple, dans l'arithmétique de Peano, qui est une théorie du premier ordre qui parle des entiers, tu peux écrire « pour tout entier n, 2(n+1) = 2n + 2 », mais tu ne peux pas écrire le principe de récurrence « pour toute propriété P des entiers, (P(0) et (pour tout n, P(n) ⇒ P(n+1)) ⇒ pour tout n, P(n) ». En théorie des ensembles, on ne peut toujours pas quantifier sur les propriétés, mais on se rattrape parce que comme on a un ensemble des entiers, on a aussi l'ensemble de ses parties (grâce aux axiomes), et donc on peut quantifier sur les ensembles d'entiers, ce qui est essentiellement la même chose que de quantifier sur les propriétés des entiers.

Et ici, c'est la même idée : le {● : p} est une conversion d'une proposition en un ensemble qui représente sa valeur de vérité (l'informaticien en moi a envie de dire que c'est une sorte de réification), ce qui permet ensuite, par exemple, de parler de fonctions de cet ensemble dans lui-même, parce que la logique est trop faible pour pouvoir parler « nativement » de fonctions qui transforment les valeurs de vérité.

@Ruxor : D'ailleurs, en voulant expliciter ça, je me suis rendu compte que le théorème d'involution de Higgs paraît plus élégant et compréhensible en théorie des types plutôt que dans IZF.

En Coq, les sous-ensembles se codent par des propriétés des éléments, donc un élément de Ω = P({●}) va être un prédicat unit → Prop (en assimilant {●} au type singleton unit), mais unit -> Prop est clairemement isomorphe à Prop. Donc Ω est en fait Prop. Maintenant, on a le problème usuel des quotients : quand on a deux éléments de Prop ≅ unit -> Prop qui « devraient » être égaux parce que ce sont « les mêmes sous-ensembles », parce qu'ils retiennent tous les deux unit ou ne le retiennent pas, on ne peut pas prouver qu'ils sont égaux car il faudrait l'égalité entre les témoins de preuve. On peut s'en débarrasser en postulant l'extensionnalité propositionnelle ((P <-> Q) -> P = Q), mais si on voit plutôt Prop comme un setoïde muni de l'équivalence, la condition d'injectivité de f devient (f P <-> f Q) -> (P <-> Q), et d'autre part, la compatibilité qui fait que f est bien une fonction du setoïde dans lui-même est (P <-> Q) -> (f P <-> f Q), qui se trouve être l'implication inverse. Bref, les hypothèses combinées se traduisent par la condition (P <-> Q) <-> (f P <-> f Q), i.e., f préserve les équivalences dans les deux sens.

Remarque par ailleurs que pour prouver une équivalence A <-> B, on peut clairement le faire en supposant A \/ B, i.e., en supposant A puis en supposant B.

Le lemme dit : f P -> (P <-> f (f P)). De fait, si je suppose f P et P, j'obtiens l'équivalence P <-> f P (les deux étant vrais), que je peux remonter en f P <-> f (f P), et en mettant bout-à-bout, j'obtiens P <-> f (f P). De même, si j'ai f P et f (f P), je mets bout-à-bout f P <-> f (f P) et sa version descendue P <-> f P pour obtenir P <-> f (f P).

Maintenant, prouvons le théorème P <-> f (f P). J'utilise la même astuce sur les équivalences, et à dans chaque cas, le lemme me permet d'utiliser un niveau f^n(P) pour prouver l'équivalence entre le niveau d'en-dessous et le niveau d'au-dessus. Le seul truc, c'est que si j'ai P, je ne peux pas descendre d'un niveau, donc je commence par tout monter d'un niveau en prouvant plutôt f P <-> f (f (f P)), et là, ça marche.

Ce qui donne :

```
Require Import RelationClasses.

Lemma equiv_assume_either_side (A B : Prop) : (A -> (A <-> B)) -> (B -> (A <-> B)) -> (A <-> B).
Proof. tauto. Qed.

Theorem Higgs_involution (f : Prop -> Prop) :
(forall P Q, (P <-> Q) <-> (f P <-> f Q)) -> (forall P, P <-> f (f P)).
Proof.
intro preserve.
assert (down : forall P Q, (P <-> Q) -> (f P <-> f Q)) by apply preserve.
assert (up : forall P Q, (f P <-> f Q) -> (P <-> Q)) by apply preserve.
assert (lemma : forall P, f P -> (P <-> f (f P))). {
intros. apply equiv_assume_either_side; intro.
* assert (f P <-> f (f P)) by (apply down; tauto). tauto.
* assert (P <-> f P) by (apply up; tauto). tauto.
}
intro. apply up. apply equiv_assume_either_side; intro.
* apply down. apply lemma. tauto.
* apply up. apply lemma. tauto.
Qed.
```

Merci ! Non, pour moi du moins, le problème ne venait pas du tout de ce que tu évoques à la fin avec l'ensemble vide comptant comme ensemble authentique pour les mathématiques modernes. L'origine, c'est la façon dont tu utilises une écriture qui t'es familière et que je découvre, et que comme je m'appuie essentiellement sur les phrases en français que je comprends mieux pour me donner la perche sémantique du saut dans ces formules, ça crée des contre-sens, comme la projection d'un sens imaginaire à partir de l'idée de "vérification" et surtout j'étais passé trop vite sur {●} en le lisant d'emblée avec un sens existentiel et non comme un terme. C'est ça qui reste un peu difficile parce que, selon vos réponses, parfois c'est nettement du côté d'un terme, d'autres ça semble inclure une portée d'existence.
Ainsi quand tu écris qu'en mathématiques classiques " « l'ensemble valant {●} si p est vrai et ∅ si p est faux » ", ça peut je trouve être compris comme la description du terme {●} et en même temps c'est clair que les deux branches de l'alternative renvoient à des positions d'existence (j'ai alors l'impression qu'on formule une proposition qui est soit vraie ou fausse, au lieu de commencer par 'l'ensemble valant', ce qui le maintient du côté de sa compréhension comme un terme, j'ai l'impression que c'est strictement équivalent à dire "l'ensemble vaut
{●} si p est vrai et ∅ si p est faux'.
Ce que tu dis sur l'existence en tant qu'ensemble de l'ensemble vide, c'est vrai que c'était une source d'erreurs pour moi en oubliant ça mais pas à l'avant-plan, non c'est surtout bien distinguer ce qui relève d'un ensemble qu'on pose comme terme ou bien qu'on fait insérer dans une proposition qui est vraie ou fausse qui n'est pas évident, en tout cas pour moi.

En relisant ta réponse et les remarques antérieures de Ruxor, je vois que dans
{● : p}, dans ma dernière remarque, j'avais oublié de prendre suffisamment en compte le :. Ok je saisis que c'est une manière de désigner de nouveau {●} quand p est vrai au lieu de renvoyer à l'ensemble vide. Mais, puisqu'il n'est jamais question dans l'écriture de ces deux ensembles d'asserter la vérité de {●}, son existence, mais toujours de le considérer comme un ensemble, pourquoi recourir à ce détour {● : p} quand p est vrai au lieu de simplement {●} ? C'est ça qui au final reste pour moi un peu mystérieux.

@ jeanas : Tout au contraire ! Il n'y a pas matière à se comprendre puisque tu maîtrises le sens de la notation et que je me trompais donc c'est à moi de profiter de tes éclaircissements et. Je vois mieux. Je me disais aussi après avoir posté que {●}, comme il n'y a pas le E inversé symbole de l'existence devant, devait sans doute ne pas être pris comme une proposition posant l'existence de cet ensemble. Donc c'est un terme, comme un mot à faire fonctionner dans une phrase, et alors il n'est pas surprenant qu'il n'y ait pas de valeur de vérité dans cette seule écriture, ça c'est bon, et c'est ce qui causait le gros de mes méprises.
Ce n'est pas encore très transparent ce qu'est p pour moi mais quand je recoupe avec l'explicitation antérieure de Ruxor, j'en viens à me dire que c'est une manière quand on écrit {● : p} de dire que p est vrai à partir du moment où justement ça vérifie cet ensemble mais que {● : p} pourrait désigner un ensemble vide avec un p qui est faux. Bref c'est effectivement très loin de ce que j'avais cru être le sens à ma première lecture. C'est bizarre parce que Ruxor l'avait écrit dès le départ mais comme je mésinterprétais {●}, mon cerveau allait dans un autre sens pour souder ce que je croyais être l'affirmation de l'existence d'un ensemble unique et le sens véritable, celui donné par l'explication, dans quelque chose d'incohérent.
Mais ce sont des tournures de sens qui n'ont pas, à ce dont j'ai l'impression, d'équivalent dans les phrases usuelles du français, c'est sans doute absurde de vouloir maîtriser cet aspect sans être familiarisé avec l'ensemble de ce jeu de langage, comme un coup dans une partie d'échecs sans être familier des règles dans leur globalité.
Ainsi on a envie de dire mais que procure le fait d'avoir un ensemble figurant un ensemble à un élément (sans en affirmer l'existence, je ne fais plus l'erreur) à côté d'une proposition vraie ou fausse. Comme la proposition p ne fait nullement référence à l'ensemble qui est à sa gauche, en quoi a-t-on progressé dans une forme de pensée au lieu de former un ensemble de termes hétéroclites et indifférents l'un à l'autre ? Et c'est là où je pense que comprendre c'est équivalent à être capable à maîtriser cette notation dans sa globalité.

@Dyonisos : Aïe… j'ai l'impression qu'on ne va pas réussir à se comprendre 🙁

C'est dans ce genre de situations que ce serait mille fois plus facile de discuter de vive voix plutôt que d'échanger message sur message en essayant de deviner quelle est la confusion à dénouer… Bon, j'essaie encore une fois de clarifier brièvement certaines choses.

1. La formule {●} n'affirme pas l'existence d'un ensemble contenant uniquement l'élément ●, elle représente simplement cet ensemble (techniquement, c'est un terme, pas une proposition). De même que 4 n'est pas « l'affirmation que le nombre quatre existe », c'est juste la notation pour le nombre quatre.

2. Tu as l'air de penser que quand on écrit {● : p}, ça construit une proposition p qui est liée à l'ensemble {●} (« une proposition vraie qui fixe la valeur de {●} »). Non, p, c'est une proposition quelconque que tu as déjà. Par exemple, pour p, tu peux prendre « 2+2 = 4 », ou « 2+2 = 5 », ou « l'hypothèse de Riemann est vraie », propositions qui n'ont rien à voir avec l'ensemble {●}, et dont la première est vraie, la seconde fausse, et la troisième, on ne sait pas (cf. le commentaire de Ruxor du 2024-07-05T13:11:05+0200 où il donne les exemples {● : 0=0} et {● : 0 = 1}).

3. « c'est une manière d'écrire la même chose qu'au départ » → Non, l'ensemble {● : p} n'est pas la même chose que {●}, ou plutôt pas toujours. Si p est fausse, c'est l'ensemble vide ∅, et si p est vraie, c'est l'ensemble {●}. Mais constructivement, comme on ne peut pas affirmer gratuitement que p est fausse ou vraie, on ne peut pas prouver que {● : p} vaudra toujours ∅ ou {●}.

Merci ! Je regarderai ça à tête reposée.

Je peux sans doute reformuler plus clairement le point sur lequel je dois faire quelque part une erreur de compréhension. Voici les deux sens dans lesquels je comprenais les formules de l'exemple avancé :

{●}: il existe un ensemble comprenant l'élément unique noté point noir.
{● : p} : au début je ne comprenais pas parce que j'avais l'impression qu'avec la phrase évoquant la vérification on incluait la proposition assertant la vérité de
{●} comme une condition de sa vérité et ça j'ai bien saisi que c'était faux. Et je pensais avoir compris en gros en considérant que par condition de compréhension qui n'est pas une condition réelle de la vérité assertée, c'est une manière d'écrire la même chose qu'au départ (il existe un ensemble comprenant l'élément unique noté point noir) en ajoutant à côté qu'il y a une proposition vraie qui l'asserte et qui fixe sa valeur de vérité.
Et, évidemment, on ne voit pas alors l'utilité réelle de ce p, tout semble déjà dit avec {●} et c'est ce que je pensais être conforté avec l'idée que {●} n'est pas du tout une variable, que sa valeur est fixe. La manière que j'avais de faire sens de cet ajout, c'était de me dire que l'intuitionniste constructiviste a une réticence à emprunter des formules où une vérité est posée de manière absolue, indépendamment des moyens de l'obtenir/de la construire.
Très prosaïquement, sans doute que l'erreur était logée dans la compréhension des formules {●} et {● : p}

@ jeanas et ruxor : je n'ai pas repéré d'écart entre ce qui me semblait avoir (finalement compris) et vos remarques ! Je n'ai bien entendu à aucun moment estimé que la notation intuitionniste qu'en somme je découvrais devait être réformée ou était incorrecte. Ce que j'ajoutais avec l'aspect de la vérité correspondance, c'était dans mon esprit plus ou moins une glose du passage où Ruxor écrivait :
Ce qui rend la chose un peu déroutante dans « {● : p} » c'est que ‘●’ est fixé et n'apparaît pas comme variable (p n'a pas de variable, donc dire que ● « vérifie » p c'est juste dire que p est vrai), mais c'est quand même la même chose."

Je ne vois pas ce qu'ajoute comme information le p au premier ensemble {●} dont on était parti, et il me semblait que c'était parce que d'un point de vue classique on n'a pas besoin de cette condition de compréhension : je recite ruxor : "
"p n'a pas de variable, donc dire que ● « vérifie » p c'est juste dire que p est vrai" donc pourquoi ne pas faire un pas de plus et ajouter que "dire que p est vrai, c'est juste dire p".
Mais je m'aperçois qu'en fait il y a bien une méprise de compréhension de ma part parce que j'interchange p et ●. Comme je ne suis pas du tout accoutumé à ce jeu d'écriture/notation, dès le début dans l'exemple explicitant de Ruxor, ça contrecarre ma manière de m'en faire une image mentale intuitive en suivant ces symboles. Ainsi quand il pose un ensemble initial {●}, tel que je le comprends, écrire ceci c'est déjà l'affirmer et donc poser sa valeur de vérité dans la proposition p (pour moi p est une manière d'écrire {●} est vrai et c'est peut-être là que je me trompe, parce qu'alors je ne vois pas ce qu'on a vraiment ajouté à ce dont est parti à savoir {●}). Je pensais que ce genre d'ajout propre à l'écriture constructionniste avait à voir avec la réticence à parler d'une vérité "en l'air", dissociée de nos moyens de la saisir mais là encore je me suis peut-être trompé. Ce n'est pas grave, j'ai quand même appris beaucoup de choses !

Quand tu écris « "P n'est pas vrai" est la même chose que "P est faux" » en sous-entendant que "P n'est pas faux" n'est pas la même chose que "P est vrai", cela m'a fait me demander si Kaamelott (épisode 28 du livre I) n'est pas lui aussi une introduction à la logique intuitionniste.
Ou, tout au moins, si on peut utiliser cette référence pour que des élèves se souviennent plus facilement de cette propriété essentielle de la logique intuitionniste.

@Ruxor : Est-ce que tu aurais une référence **à peu près compréhensible** pour en savoir plus sur les topos ? Et notamment sur la manière précise dont la vérité d'une formule se définit dans un topos ? J'ai regardé <URL:https://arxiv.org/abs/2204.00948>, que tu conseilles dans le billet sur le topos effectif, mais « The remaining translation rules are more involved, as detailed by (Mac Lane and Moerdijk, 1992, Section VI.7); we do not list them here for the case of a general topos E, but we will state them in the next sections for several specific toposes. », et le bouquin cité est un pavé de 650 pages (comme tous les bouquins qui s'intitulent « Introduction to X »…).

@Dyonisos : Désolé de jouer un peu au rabat-joie, mais j'ai l'impression qu'il y a encore une certaine confusion dans ce que tu écris, ou alors je n'ai pas bien compris ce que tu veux dire.

La notation {x ∈ truc | machin} est parfaitement valable en théorie des ensembles classique comme intuitionniste, et {● : machin} veut juste dire {x ∈ {●} | machin}, simplement la notation {x ∈ truc | machin} n'a aucun intérêt en logique classique quand machin ne dépend pas de x. Mais il n'y a pas vraiment de différence de notation, juste une différence dans l'intérêt des notations.

Et je ne suis pas sûr de comprendre précisément ton passage sur la vérité tarskienne, mais il peut être éclairant de rappeler qu'à l'intérieur d'un raisonnement constructif, dire « P », c'est effectivement la même chose que dire « P est vraie » (le « est vraie » n'a pas d'autre définition), aucune différence avec la logique classique de ce point de vue. Comme ce n'est peut-être pas très clair dit comme ça, voici un exemple de raisonnement qui n'est pas valable :

Soit f : ℕ → ℕ. Par définition d'une fonction en théorie des ensembles, f est égale à son graphe {(x, f(x)), x ∈ ℕ}. Comme je suis en train de raisonner en logique intuitionniste, je peux extraire de f un algorithme qui décide si une paire (x, y) vérifie y = f(x). Je peux donc construire l'algorithme qui prend x et qui teste successivement les paires (x, 0), (x, 1), … jusqu'à trouver f(x). Ainsi, f est calculable. J'ai donc prouvé en logique intuitionniste que toute fonction ℕ → ℕ est calculable.

Ce raisonnement est invalide parce qu'à l'intérieur du raisonnement constructif, une fonction ou un ensemble ne vient pas automatiquement avec un algorithme. Ce n'est qu'une fois qu'on a terminé une preuve constructive entière, en la regardant depuis le niveau méta, qu'on peut en extraire un algorithme.

Est-ce tes "propriétés mystifiantes" de l'ensemble ordonné Ω peuvent être décrites dans un langage plus ordinaire, plus éloigné de la logique.

Je voudrais un énoncé comme "Si un cadre vérifie… alors toute fonction telle que f(1) = 1 vérifie p <= f(p)…" ou idem avec le théorème d'involution.

En fait, dans cette notation, j'ai l'impression qu'il y a déjà beaucoup de ce qui est "contre-intuitif" dans l'intuitionnisme constructiviste. Car, quand tu écris que " dire que ● « vérifie » p c'est juste dire que p est vrai", j'ai en moi l''envie de répondre : "mais dire que p est vrai, c'est juste dire p" (et donc ici
●) à la manière décitationnaliste et déflationniste de Tarski, d'où sans doute une bonne part de l'étrangeté du recours à ce type de formule.

@ Ruxor : oui c'est très éclairant (et intéressant) ! Un élément que j'en retiens est que la manière d'écrire du constructivisme intuitionniste exprime déjà la conception de ne parler de la vérité de l'objet mathématique qu'en rapport étroit avec la façon dont on peut y penser/le construire : cf le 'je mets" du "je mets l'élément untel dans l'ensemble si p est vrai" alors qu'en mathématique plus classique dans la notation même on fait fond sur l'idée d'une vérité indépendamment de nos opérations cognitives. Encore merci pour ces éclaircissements !

Je dirais tout bêtement « non-non-séparé », vu que je dis aussi (et j'ai entendu, ou lu, je ne sais plus) « non-non-traduction » pour la ¬¬-traduction.

OK ^^ Je disais spontanément "double-neq séparé". Enfin, deubeulnékséparé.

Comment prononces-tu "(¬¬)-séparé" ?

@ jeanas : ok c’est saisi ! ( je sentais bien que ça provenait du sens de la notation qui m’échappait)

Je reformule/pinaille de nouveau : pourquoi ne peut-on pas dire que l'ensemble des éléments de {●} qui vérifie p dans l'exemple que tu as formulé, c'est juste lui-même, sans y inclure p ? A vrai dire, ça me semble même tautologique de s'exprimer ainsi, je ne saisis pas en quoi l'adjonction d'une proposition vraie concernant l'ensemble qu'on s'est donné conduit à inclure cette proposition dans l'ensemble lui-même pour qu'il "vérifie" p. C'est ce que je tentais d'exprimer avec l'idée de vérité-correspondance : je ne vois pas le rapport entre l'hypothèse de cette vérité et l'opération de l'inclure dans l'ensemble la vérifiant. Il n'y a aucun doute que c'est une question de familiarité/maîtrise avec ce langage ensembliste mais ça va très (trop?) vite pour qui ne le maîtrise pas suffisamment en amont de ta lecture.

> Ok merci ! Persiste une difficulté pour moi parce que je ne suis pas du tout rôdé à ce langage. Ainsi dès que dans ton exemple tu inclus p comme un élément de l'ensemble vérifiant p, mon intuition (ou plutôt mon jeu de langage) a du mal.

Là, il doit y avoir une confusion sur les notations. Quand Ruxor écrit {● : p}, le p n'est pas un élément de l'ensemble, seul le ● peut l'être. Traduit avec la notation {x ∈ machin | truc} habituelle (p.ex. celle de « ℝ⁺ = {x ∈ ℝ | x ≥ 0} »), le {● : p} veut dire {x ∈ {●} | p}, simplement la particularité un peu troublante ici est que la propriété après le |, à savoir p, ne dépend pas de x.

> et je pensais que c'était vrai en général, cette relation entre un ensemble non vide et l'impossibilité d'affirmer qu'il a un élément, pas juste pour l'intuitionniste !

Je crois que le souligné rouge est justement fait pour marquer que c'est vrai classiquement mais pas intuitionnistement.

Classiquement, c'est clair qu'un ensemble non-vide a un élément. C'est quelque chose qu'on utilise absolument tout le temps, par exemple quand on dit « Soit S l'ensemble des éléments qui vérifient ceci et cela… Supposons S = ∅, alors… contradiction. Donc S contient un élément x ∈ S. Soit alors y = f(x), … » Peu importe la preuve exacte, la logique classique est celle des maths habituelles, et ce raisonnement est clairement valable en maths habituelles.

Ok merci ! Persiste une difficulté pour moi parce que je ne suis pas du tout rôdé à ce langage. Ainsi dès que dans ton exemple tu inclus p comme un élément de l'ensemble vérifiant p, mon intuition (ou plutôt mon jeu de langage) a du mal. Comme je me représente la vérité comme une relation de correspondance, une image correcte de l'état de choses représenté, je ne vois pas pourquoi je dois inclure la proposition vraie elle-même dans ce dont elle est l'image pour qu'elle soit vraie (ou fausse d'ailleurs). Mais c'est peut-être expliqué dans la suite de ton billet que je vais creuser.
@ jeanas : oui ça je savais que pour un intuitionniste il n'y a pas de sens à parler d'un existant mathématique s'il est découplé de toute constructibilité. En ce sens je comprends la position. Mais en fait j'ai alors peut-être fait une erreur d'interprétation : dans le fil de la lecture, le passage survenait ainsi :

"Mais la notion d'ensemble non-vide, i.e., d'ensemble vérifiant ¬(E=∅), elle, n'a que très peu d'intérêt constructif : un ensemble E est non-vide s'il vérifie ¬¬∃x.(x∈E) ou, ce qui revient au même ¬∀x.¬(x∈E), mais on ne peut pas faire grand-chose avec un ensemble non-vide : notamment, on ne peut pas affirmer qu'un ensemble non-vide a un élément."

et je pensais que c'était vrai en général, cette relation entre un ensemble non vide et l'impossibilité d'affirmer qu'il a un élément, pas juste pour l'intuitionniste !Bref je n'avais pas assez fait attention à l' "intérêt constructif" évoqué qui doit réserver cette idée précisément à l'intuitionniste. C'est sans difficulté de compréhension particulière si cette idée ne s'étend pas à la logique "classique".

@Dyonisos (Ruxor t'a répondu, mais je me permets de le redire différemment en tant que personne pas encore frappée de la malédiction de la connaissance sur ce sujet) :

En logique intuitionniste, dès que tu vois une affirmation de la forme « il existe x tel que », tu mets ta lecture sur pause, tu oublies tes réflexes logiques, et tu réfléchis (et même chose pour « A ou B »).

Si tu veux prouver ça de manière constructive, il va falloir exhiber le x en question. Si tu sais juste qu'un ensemble est non-vide, ça ne te donne strictement aucune information sur ce qu'il contient. Donc tu ne peux pas affirmer qu'il a un élément (= il existe un élément qui est dedans), parce que pour le faire, tu serais obligé de construire cet élément, de le donner explicitement, et tu n'as aucun moyen de le faire. Logiquement, ça coince, comme l'a expliqué Ruxor, parce que le passage de ¬¬∃ x, x ∈ S à ∃ x, x ∈ S est une élimination de la double négation, pas valable intuitionnistement. Mais on n'a pas besoin de réfléchir aux étapes du raisonnement formel pour voir immédiatement que ça doit forcément coincer quelque part.

Ça demande un peu d'habitude de raisonner en logique intuitionniste (personnellement, c'est la pratique de Coq qui m'a le plus aidé à prendre de l'aisance). Au début, on est un peu noyé, à se demander à chaque étape quelle règle de déduction on est en train d'appliquer et si elle n'utilise pas le tiers exclu. Mais avec un peu d'habitude, on voit vite ce qu'on a le droit de faire ou de ne pas faire, et on apprend à reconnaître rapidement quelles étapes d'un raisonnement intuitionniste risquent de poser problème (par rapport à un raisonnement classique). Et notamment, à se demander dès qu'on voit un « il existe x » : comment je vais le construire ?

Zut ! Le début était fort clair et très intéressant et le sujet recoupe un intérêt ancien de ma part avec des lectures (trop complexes eu égard à mon absence de bases) y ayant trait. Mais je ne comprends pas ton assertion soulignée selon laquelle on ne pas affirmer qu'un ensemble non-vide a un élément ! Je suis sûr qu'elle est vraie avec la maîtrise du sens des notions en jeu mais…pourquoi ?