<foo>
simply produces <foo>in the text).
<URL: http://somewhere.tld/ >
,
and it will be automatically made into a link.
(Do not try any other way or it might count as an attempt to spam.)mailto:
URI,
e.g. mailto:my.email@somewhere.tld
,
if you do not have a genuine Web site).
jeanas (2025-02-03T18:00:21Z)
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.
jeanas (2025-02-03T10:24:55Z)
@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à.
Thierry (2025-02-01T22:53:55Z)
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.
Ruxor (2024-07-23T09:01:34Z)
@Subbak: Pour parler de sous-singleton, il y a deux choses qui interviennent : un ensemble ambiant X, et une partie E de X qui sera qualifiée de sous-singleton de X. L'hypothèse caractérisant le sous-singleton, c'est ∃x∈X.∀y∈E.(y=x) : donc l'ensemble ambiant X est habité, en effet (à cause du « ∃x∈X »), mais on ne peut pas affirmer que la partie E l'est. Classiquement, les sous-singletons de X, ce sont exactement les {x} pour x∈X et la partie vide ∅ — sauf si X est lui-même vide, auquel cas il n'y a pas de sous-singleton du tout (même pas ∅). Après, ce n'est pas une notion super intéressante, et peut-être que j'ai eu tort de la mentionner (et d'ailleurs, beaucoup de gens traitent « sous-singleton » comme un synonyme de « sous-terminal » qui est la notion plus intéressante).
Subbak (2024-07-23T07:03:48Z)
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.
Dyonisos (2024-07-16T09:37:01Z)
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.
jeanas (2024-07-15T23:30:04Z)
@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.)
Dyonisos (2024-07-15T20:04:15Z)
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 ?
Dyonisos (2024-07-15T18:09:25Z)
Thanks !
Ruxor (2024-07-15T16:47:50Z)
@Dyonisos: {● : p} est bien un terme, représentant un ensemble. Son rapport avec la proposition p, c'est que p est équivalente à l'affirmation « {● : p} est habité », donc l'ensemble {● : p} permet de retrouver la proposition p qui a servi à le fabriquer (enfin, à équivalence près, c'est-à-dire, la valeur de vérité de p). L'intérêt de l'opération, c'est que même si la logique sur laquelle on travaille ne permet pas directement de manipuler les propositions (ça dépend des subtilités que j'ai glissées sous le tapis), la construction {● : p} permet quand même de l'utiliser en pratique comme un objet mathématique sur lequel on peut faire plein de constructions (le mettre dans un couple, le faire renvoyer à une fonction, etc.). En maths classiques, ça devient exactement à représenter les valeur de vérité par ‘0’ et ‘1’ (sauf que ce sont ∅ et {●} qui jouent ce rôle), mais en maths intuitionniste, l'ensemble Ω des ensembles de la forme {● : p} peut être « très gros » dans divers sens (mais c'est quand même bien pratique de pouvoir le considérer comme un ensemble).
Dyonisos (2024-07-15T15:31:05Z)
@ 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 ?
Ruxor (2024-07-15T15:09:00Z)
@Dyonisos: C'est vrai qu'il faut peut-être prendre conseil dans l'adage que « in mathematics you don't understand things: you just get used to them » et se contenter de décrire des règles de raisonnement valable. Les principales choses à savoir, ici, sont que ⓐ si X est un ensemble et P une formule logique avec possiblement x comme variable libre alors on peut former le terme {x∈X : P(x)}, qui désigne un ensemble, et ⓑ un y appartient à ce terme si et seulement si y∈X et P(y) ; et ⓒ par ailleurs que deux ensembles X et Y sont égaux si et seulement si ∀z. (z∈X ⇔ z∈Y) (axiome d'extensionnalité) ; par ailleurs, le terme {● : p} est juste un raccourci de langage pour {x∈{●} : p}. (NB : je ne prétends pas avoir listé ici tous les axiomes des fondements ensemblistes que j'utilise, sur lesquels je suis d'ailleurs resté délibérément vague, mais ce sont les principales choses à savoir.)
Ainsi, mon raisonnement pour prouver que « si Ⓗ tout ensemble est soit habité soit vide, alors la loi du tiers exclu vaut » se formule de façon quasi-formelle ainsi :
⁃ ① je considère p une formule quelconque ;
⁃ ② je forme l'ensemble {● : p} (c'est-à-dire {x∈{●} : p}, que j'ai le droit d'écrire d'après ⓐ) ;
⁃ ③ j'observe que (d'après ⓑ) y ∈ {● : p} équivaut à « y ∈ {●} et p est vrai » (pour rappel, « p est vrai » est juste une tournure de langage pour dire « p ») ;
⁃ ④ j'en déduis « si {● : p} est habité, alors p est vrai » (en effet, on vient de voir en ③ que si y ∈ {● : p}, alors p est vrai, d'où on déduit que si ∃y. (y ∈ {● : p}) alors p est vrai par la règle logique d'élimination du ‘∃’ et le fait que y n'apparaît pas dans p) ;
⁃ ⑤ dire que {● : p} = ∅ équivaut, par ⓒ, à dire que que ∀y. (y ∈ {● : p} ⇔ ⊥), autrement dit ∀y. ¬(y ∈ {● : p}) par pure logique, autrement dit ∀y. ¬(y∈{●} ∧ p), et en appliquant ça à y=● on obtient en conclut ¬p : ceci montre que « si {● : p} est vide alors p est faux » ;
⁃ ⑥ on vient donc de voir que si {● : p} est habité, alors p est vrai (point ④) et que si {● : p} est vide, alors p est faux (point ⑤) ;
⁃ ⑦ mais l'hypothèse Ⓗ appliquée à {● : p} dit que soit {● : p} est habité soit {● : p} est vide ;
⁃ ⑧ donc (en utilisant ⑥) l'hypothèse Ⓗ implique que p est vrai ou bien p est faux ;
⁃ ⑨ et comme était quelconque, ceci signifie que l'hypothèse Ⓗ implique la loi du tiers exclu (qui est un tabou constructif). ∎
(Ce n'est pas encore parfaitement formel, mais ce n'est plus très loin de l'être. Si je détaille encore plus ça va devenir franchement illisible, mais s'il y a un point qui reste obscur, je peux bien sûr le préciser.)
⁂
Maintenant, pour revenir à un niveau un peu plus informel, il faut peut-être que je précise aussi les choses suivantes :
‣ « l'ensemble {● : p} vaut {●} si p est vrai et ∅ si p est faux » → cette affirmation EST CORRECTE en maths constructives et (donc) aussi en maths classiques (je peux le prouver précisément s'il y a un doute, mais en gros c'est très analogue aux points ④ et ⑤ ci-dessus) ;
‣ l'expression « l'ensemble valant {●} si p est vrai et ∅ si p est faux » est légitime en maths classiques parce qu'il existe un UNIQUE ensemble valant {●} si p est vrai et ∅ si p est faux (l'existence résulte du point précédent, et l'unicité résulte de ⓒ et du fait que p et ¬p recouvrent tous les cas possibles : là aussi, je peux détailler au besoin) ;
‣ le problème avec l'expression « l'ensemble valant {●} si p est vrai et ∅ si p est faux » en maths constructives n'est pas qu'on ne peut pas prouver l'existence d'un tel ensemble (on peut la prouver : je viens de dire que {● : p} en est un), c'est qu'on ne peut pas prouver son UNICITÉ ; en effet, l'ensemble {● : ¬¬p} vaut lui aussi {●} si p est vrai et ∅ si p est faux, mais s'il est égal à {● : p} c'est que ¬¬p⇒p (toujours à cause de ⓒ).
Donc peut-être que c'est cet élément qui te manquait : pour pouvoir légitimement écrire « le foobar qui vérifie blah bloh bluh » (et raisonner après sur un objet bien défini) il faut montrer l'existence et l'unicité d'un tel foobar. La notation {x∈X : P(x)}, notamment, construit bien un ensemble des éléments de X vérifiant P(x), et cet ensemble est unique d'après ⓒ (toujours l'extensionnalité). (Bien sûr, s'il existe un foobar vérifiant blah bloh bluh et qu'on ne peut pas prouver qu'il est unique, on a quand même le droit de dire « soit x un foobar qui vérifie blah bloh bluh », mais on ne doit pas écrire « le » sauf quand on a l'unicité. Et pour appliquer le raisonnement que j'ai fait aux points ①–⑨, juste avoir « un ensemble valant {●} si p est vrai et ∅ si p est faux » ne suffirait pas.)
C'est très perturbant intuitivement que les ensembles {● : p} et {● : ¬¬p} soient tous les deux égaux à {●} si p est vrai et ∅ si p est faux, et qu'on ne puisse quand même pas affirmer qu'ils sont égaux (mais on peut affirmer qu'ils ne sont pas différents !). Je ne pense pas pouvoir expliquer mieux que ça, parce que je n'ai pas vraiment d'intuition sur la chose (sauf à sortir un topos de faisceaux). Mais ça mérite d'être écrit noir sur blanc.
jeanas (2024-07-15T11:29:04Z)
@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.
```
Dyonisos (2024-07-15T10:24:21Z)
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.
Ruxor (2024-07-15T07:25:28Z)
@Dyonisos: Il n'y a en effet aucune raison d'écrire « {● : p} » quand on sait que p est vrai : c'est pareil que {●}, donc autant écrire ça. De même, il n'y a aucune raison d'écrire « {● : p} » quand on sait que p est faux : c'est pareil que ∅, donc autant écrire ça. Or en logique classique, « p est vrai » et « p est faux » recouvrent tous les cas, donc en maths classiques on n'écrit normalement pas « {● : p} », on écrira plutôt « l'ensemble valant {●} si p est vrai et ∅ si p est faux » — c'est plus explicite et moins confus. Mais en maths constructives, cette tournure entre guillemets ne suffit pas à décrire un ensemble de façon unique parce qu'on ne peut pas affirmer que p est vrai ou bien faux (p∨¬p), c'est justement tout l'enjeu de la logique intuitionniste. En revanche, on a le droit (à des conditions fondationnelles qui ne sont pas le propos ici) d'écrire des choses comme {x : p(x)} (aussi noté {x | p(x)}, pour moi c'est exactement pareil), c'est-à-dire de décrire un ensemble en disant à quelle condition p(x) je mets l'élément x, et c'est ce procédé de construction qui est utilisé pour former {● : p}, même si c'est un cas un peu bizarre parce que x est fixé et que p(x) ne dépend de rien du tout.
Donc, pour le dire encore autrement : en écrivant {● : p}, je ne prends pas position sur la question de savoir si p est vrai : je dis juste « je construis un ensemble (sous-ensemble de {●}), dans lequel je mets mon élément de référence ● si et seulement si p est vrai ». Peut-être que cet ensemble sera habité (ce qui se produit exactement quand p est vrai) ; peut-être qu'il sera vide (ce qui se produit exactement quand p est faux) ; mais je ne dis rien de plus.
Juste un sanity check parce que j'essaie de deviner ce qui peut bloquer la compréhension et je me disais que le problème venait peut-être de là : pour les maths (contemporaines, au moins) l'ensemble vide ∅ est un ensemble comme les autres — ce n'est pas parce qu'il n'y a pas d'éléments dedans qu'il aurait moins d'existence que les autres. (Il n'existe pas d'élément DANS l'ensemble vide, mais l'ensemble vide, lui, existe parfaitement, et peut servir à former d'autres ensembles. D'ailleurs en théorie des ensembles classique et orthodoxe de Zermelo-Fraenkel tous les ensembles — donc tous les objets mathématiques — sont pour ainsi dire formés en empilant des couches d'accolades terriblement compliquées autour de l'ensemble vide à différents niveaux.) Dire qu'un ensemble existe veut juste dire qu'on l'a correctement décrit, qu'on a défini un objet qui a un sens. C'est un tout autre problème de se demander s'il existe des éléments DANS cet ensemble (ça c'est dire que l'ensemble est « habité », justement). En particulier, l'ensemble {● : p} existe toujours (i.e., cette notation est toujours permise et définit toujours un ensemble) ; mais il est habité si et seulement si p est vrai. (Peut-être que ce que je viens de dire était déjà totalement clair, mais ça ne fait sans doute pas de mal de mettre les point sur les ‘i’.)
Dyonisos (2024-07-15T04:50:44Z)
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.
Dyonisos (2024-07-15T03:16:48Z)
@ 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é.
jeanas (2024-07-14T17:03:49Z)
@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 {●}.
jeanas (2024-07-13T10:07:18Z)
Merci ! Je regarderai ça à tête reposée.
Dyonisos (2024-07-11T08:08:45Z)
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}
Dyonisos (2024-07-11T00:20:56Z)
@ 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 !
Ruxor (2024-07-09T16:43:59Z)
@jeanas (2024-07-07T14:29:00+0200):
Sur les topos en logique, il y a quelques suggestions sur <URL: https://mathoverflow.net/questions/445535/recommendations-to-learn-about-the-use-of-toposes-in-logic > (j'ai posté une des réponses mais les autres sont intéressantes aussi). Personnellement j'ai appris dans le MacLane & Moerdijk, et il n'est évidemment pas nécessaire de tout lire.
Par ailleurs, il faut souligner qu'il n'est souvent pas nécessaire de savoir ce qu'est qu'un topos en général : la quasi-totalité des contre-exemples qu'on fabrique en maths constructives, c'est soit avec un topos de faisceaux (sur un espace topologique ou une locale, plus rarement une topologie de Grothendieck) soit avec un topos de réalisabilité (c'est-à-dire une variante du topos effectif). Et donc ce qu'on va regarder c'est les faisceaux en question ou la réalisabilité en question, mais le mot « topos » sert surtout à faire chic en invoquant le fait que la logique se comporte comme on s'y attend.
Ruxor (2024-07-09T11:05:50Z)
PS : j'ai un peu étendu le passage du billet où je parle de {● : p}, dans l'espoir que ce soit plus clair comme ça.
Ruxor (2024-07-09T10:33:12Z)
@jeanas (2024-07-06T11:38:33+0200): Le problème à dire « non-non-séparé », c'est qu'on peut aussi dire simplement « séparé » (quand le contexte est clair, un ensemble « séparé » c'est un ensemble (¬¬)-séparé), et que, du coup, « non-non-séparé » introduit une ambiguïté : parce que dire qu'un foobar x est non-non-cromulent, ça veut dire qu'il vérifie ¬¬cromulent(x) ; or là, justement, si je ne m'abuse, n'importe quel ensemble est non-non-séparé (c'est-à-dire vérifie « ¬¬(l'ensemble est (¬¬)-séparé) »).
@Dyonisos: J'ai, comme jeanas, l'impression diffuse qu'il y a encore quelque chose qui n'est pas clair pour toi, mais je ne sais pas bien quoi. En tout cas nous sommes d'accord que « ● vérifie p » (sachant que ‘●’ n'apparaît pas dans p), « p est vrai » et juste « p », c'est exactement la même chose : la première formulation est utilisée parce que c'est comme ça que fonctionne la notation « {x∈E : P(x)} » ; quant à « est vrai », c'est une tournure complètement superfétatoire, mais qui clarifie un peu la syntaxe des phrases (mais je l'ai déjà dit et je le répète, dire « <machin> est vrai » ou dire <machin>, c'est exactement pareil).
@Nick Mandatory: C'est une question que je me pose aussi, et je n'ai pas de réponse satisfaisante (mais en même temps je ne sais pas la formuler de façon assez précise et satisfaisante pour la poser sur MathOverflow).
Ptitboul (2024-07-08T21:53:47Z)
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.
jeanas (2024-07-07T12:29:00Z)
@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.
Nick Mandatory (2024-07-06T21:01:46Z)
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.
Dyonisos (2024-07-06T13:35:08Z)
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.
Dyonisos (2024-07-06T13:25:22Z)
@ 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 !
jeanas (2024-07-06T09:38:33Z)
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.
A. Greg (2024-07-06T01:46:07Z)
OK ^^ Je disais spontanément "double-neq séparé". Enfin, deubeulnékséparé.
Ruxor (2024-07-05T21:49:54Z)
@A. Greg: Aucune idée. 😅 Quelque chose comme « séparé pour la topologie du non-non », je pense.
A. Greg (2024-07-05T21:18:45Z)
Comment prononces-tu "(¬¬)-séparé" ?
Ruxor (2024-07-05T11:13:21Z)
PS: Si c'est plus clair, je peux recopier une partie des explications dans le billet lui-même (reste à trouver le bon point où les insérer).
Ruxor (2024-07-05T11:11:05Z)
@Dyonisos:
Note que le commentaire de jeanas daté 2024-07-05T10:39:17+0200 a été posté avant le tien, mais modéré en même temps, donc tu ne l'as sans doute pas lu, et qu'il est pertinent pour répondre à ta question. Je le redis un peu à ma façon :
Quand j'écris « {● : p} » (le ‘:’, qui signifie « tel que » pourrait être un ‘|’, j'utilise ces deux notations de façon interchangeable), c'est la même notation que si j'écris « [0,1] = {x∈ℝ : 0≤x≤1} » : ce qui suit le ‘:’ est une formule logique qui définit une condition sous laquelle ce qui précède le ‘:’ est mis dans l'ensemble (c'est une condition de compréhension, si on veut). 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.
Exemples très simples :
‣ {● : 0=0} = {●} (l'ensemble des ● tels que 0=0 est {●} puisque, justement, 0=0, donc ● vérifie bien 0=0), et plus généralement, on a {● : p} = {●} si et seulement si p est vraie,
‣ {● : 0=1} = ∅ (l'ensemble des ● tels que 0=1 est vide puisque ¬(0=1), c'est-à-dire que ● ne vérifie pas 0=1), et plus généralement, on a {● : p} = ∅ si et seulement si p est fausse.
En maths classiques, on n'écrit jamais ce genre de choses {● : p} (même si techniquement on a le droit), parce qu'en maths classiques on va écrire « l'ensemble valant {●} si p est vrai et ∅ si p est faux », mais en maths constructives on ne peut pas faire cette distinction « machin si p est vrai et bidule si p est faux », et on est obligé de recourir à ce procédé par compréhension « je mets l'élément ● dans l'ensemble si p est vrai » qui, lui, est autorisé (donné un ensemble X on a le droit de former {x∈X : p(x)}, et c'est ce qu'on applique avec X={●} et p(x) ne faisant pas intervenir x).
Il ne s'agit donc pas de mettre p dans l'ensemble (tous les éléments de {● : p} sont, de toute manière, égaux à ●). Il s'agit d'utiliser p comme condition pour décider si on met ‘●’ dans l'ensemble.
Comme je l'explique plus bas dans le billet, cette construction {● : p} est juste une façon de « représenter » la valeur de vérité de p sous forme d'un ensemble, et on peut même être tenté de considérer que « c'est » (la valeur de vérité de) p. L'intérêt est de permettre de traduire sur les ensembles des choses qu'on peut dire sur les valeurs de vérité et vice versa : en l'occurrence, {● : p} est habité si et seulement si p vaut, et {● : p} est vide si et seulement si ¬p vaut (i.e., p est fausse), et du coup l'affirmation « si {● : p} n'est pas vide alors il est habité » devient « si ¬¬p alors p » : la construction sert exactement à obtenir cette équivalence.
Je pense que ceci est un bon exemple de construction extrêmement triviale en maths classiques, à tel point qu'elle en devient source de confusion (parce qu'en maths classiques c'est presque forcément une erreur d'écrire {x : p} si p ne fait pas intervenir x : techniquement on a le droit, mais en pratique ce n'est jamais utile d'écrire ça), et qu'il est donc difficile de comprendre en maths constructives (où non seulement la construction {● : p} est utile, mais l'ensemble Ω := 𝒫({●}) des parties de {●} est à la fois important et délicat à manier).
Donc, pédagogiquement, je ne sais pas forcément m'y prendre. Est-ce que ce qui précède éclaircit les choses ?
Dyonisos (2024-07-05T10:50:04Z)
@ jeanas : ok c’est saisi ! ( je sentais bien que ça provenait du sens de la notation qui m’échappait)
Dyonisos (2024-07-05T09:23:19Z)
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.
jeanas (2024-07-05T08:39:17Z)
> 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.
Dyonisos (2024-07-05T04:44:09Z)
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".
jeanas (2024-07-04T22:17:36Z)
@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 ?
Ruxor (2024-07-04T21:23:39Z)
@Dyonisos: Je l'explique en fait un peu plus loin en parlant de contre-exemples brouwériens, mais comme c'est sans doute mal dit, voici l'explication de façon plus explicite :
Soit {●} un ensemble ayant un unique élément noté ‘●‘. Soit p une affirmation (identifiée à sa valeur de vérité). Notons {● : p} l'ensemble des éléments de {●} vérifiant p, autrement dit l'ensemble qui contient ● si et seulement si p est vraie. Dire que cet ensemble est habité signifie que p est vraie. Dire qu'il n'est pas vide (i.e., qu'il est faux qu'il est vide), en revanche, signifie que p n'est pas fausse, i.e., ¬¬p. Donc affirmer que tout ensemble non vide est habité signifierait que ¬¬p ⇒ p pour tout p. C'est le principe d'élimination des doubles négations, qui équivaut au tiers exclu. Ne voulant pas admettre ce principe, on ne peut pas non plus admettre que tout ensemble non vide est habité.
(Enfin, ce que je viens de dire, c'est un contre-exemple brouwérien, qui justifie qu'on ne peut même pas postuler que tout ensemble non vide est habité, sauf à retomber sur la logique classique. Mais si la question est « pourquoi je n'arrive pas à le démontrer ? », disons que « S est vide » signifie « ¬∃x.(x∈S) », donc « S n'est pas vide » signifie « ¬¬∃x.(x∈S) », tandis que « S est habité » signifie « ∃x.(x∈S) ». En logique classique on peut passer de l'un à l'autre, par élimination de la double négation, mais en logique intuitionniste, ce raisonnement n'est pas permis.)
Dyonisos (2024-07-04T19:31:01Z)
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 ?