Formation accélérée, vrais fondements pour GG

christophe c
christophe c
dans Fondements et Logique
J'ouvre ce fil, mais ma dispo n'est pas si énoorme en ce moment, donc je vais taper vite et détailler plus tard.
Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi

Réponses

  • christophe c
    christophe c
    1/ Il était une fois des mots qu'on met les uns à côté des autres pour parler entre scientifiques

    2/ Arg, mais un jour on s'est aperçu qu'on avait besoin de variables liées pour parler, pcchiiitttt

    3/ Du coup, plein de gens se sont engouffrés dans ces horribles méandres, très excitantes (la liaison de variable) pour jeter brumes et ambiguités sur la science et son langage.

    4/ Mais mais mais, en fait, un gars (ou une fille, je ne sais pas qui, mais je me renseignerai) a remarqué judicieusement qu'on pouvait enlever les variable liées.

    5/ Et zalors, plus possible de tricher.

    6/ Règle de langage qui évite d'utiliser des variables liées, valables pour tout mot:

    6.1/ convention: [a b c] abrègera [(a b) c] (je ne serais pas obligé, c'est juste plus digeste). Les majuscules ci-dessous sont purement psychologiques.

    Règles de calcul:

    6.2/ K a b = a
    6.3/ C a b c = b (a c)
    6.4/ W a b = a b b

    6.5/ Exercice: fabrique des mots B; S; D; G, J juste en utilisant W;C;K qui sont tels que :

    B a b = b a ; G a b c = b a c ; D a b c = a (b c) ; S a b c = a c (b c); J a = a


    7/ Avec ces règles non seulement tu as toute la science, mais en plus sans utiliser de variables liées.

    8/ Evidemment, pas de $=$ ni de $\forall$. Snif. Faut donc les ajouter. Tu as donc 4 signes:

    8.1/ W; C; K; E

    8.2/ Pourquoi 4 et pas 5, vu que j'ai dit qu'il faut en ajouter 2?

    8.3/ Réponse: parce que $\forall = $ E (K K) :-D

    9/ Problème: c'est une théorie contradictoire.

    10/ Solution: tant mieux. Ce qui est consistant termine (on dit que ça "normalise"). C'est une des multiples version du théorème de Godel: quand tu as tout ce que tu voudrais avoir, tu as $0=1$. Autrement dit, le monde est connexe.

    11/ Tu te demandes peut-être pourquoi c'est contradictoire. Et bien toute fonction $f$ a un point fixe, donc en particulier "non" a un point fixe. f(C(WJ)f(C(WJ)f)) = C(WJ)f(C(WJ)f). Exercice.

    12/ Les points fixes des fonctions qui n'en ont pas sont très utiles, car une fois traduits en garantie ils permettent de générer des boucles, très importantes ne serait-ce qu'en informatique (mais pas que). Tu te vois programmer for i := 1 to 10^40 sans boucle?

    13/ Dans ce système, tu as toute la science. Une manière assez économique d'avoir vrai et faux est de déclarer que:

    13.1/ vrai := K
    13.2/ faux := KJ

    Pourquoi? Bin parce que comme "if a then b else c" s'écrit a b c.

    14.1/ "A et B" s'écrit A (KJ) B
    14.2/ "A ou B" s'écrit A K B
    14.3/ "A => B" s'écrit A B K
    14.4/ non(A) s'écrit A (KJ) K

    15/ Par exemple la transitivité de l'égalité appliquée sur $x,y,z$ c'est (Exy) ( (Eyz) (Exz) K ) K

    16/ J'en termine là. Tu veux savoir, j'imagine comment lier des variables, ie comment obtenir un mot M tel que par exemple :

    $$ M = (x\mapsto axbe(xa)) $$

    et bien je te donne le plan et je te laisse le faire seul:

    16.1/ Face à $x\mapsto (uv)$ tu:
    16.2/ cherches $u_1:=(x\mapsto u)$
    16.3/ cherches $u_2:=(x\mapsto v)$
    16.4/ renvoies $Su_1u_2$ comme trouvaille.

    (C'est un algo récursif) dont l'initialisation est : $(x\mapsto y) := Ky$ quand $y$ est une simple lettre autr que $x$ et $(x\mapsto x):=J$

    17/ Digère tout ça et écris l'hypothèse du continu (tu vas voir c'est très rapide). en guise d'exo.

    18/ Après je t'expliquerai pourquoi les gens se noient parce que "voudraient bien" que ce soit soit consistant (alors que c'est peine perdue)

    19/ Puis je te raconterai comment HoTT a dévoyé complètement ces choses toutes simples pour tenter de rendre consistant tout ça avec un typage qui prend tellement de place que ça leur prend 500 pages pour noyer le poisson (ie pour tenter de faire croire qu'il s'agit de "nouveaux fondement" alors qu'il ne s'agit que de banale CCH primitive bien connue face à laquelle ils ont décidé de mettre un bridage COLOSSAL (par sélection naturelle****) imbitable pour garantir la consistance. Autrement dit, il font de la bête théorie des ensembles, mais ils veulent en "garantir la consistance". Je ne parle même pas d'y croire, ils veulent "plusss" et n'ont pas compris Godel (ie la décroissance entre garanties de consistances et richesse de production)

    20/ Et enfin je te raconterai le défi (non gagné) que parfois ils utilisent pour faire de la pub en le prétendant gagné (qui consiste à dire qu'on peut tout faire***** avec $\circ$ et cacher le fait qu'on utilise en scrett $Kx\mapsto x$ (ie on donne un argument factice à manger à $K$ pour récupérer le $x$, mais ça, c'est exactement ... la manière de réaliser le RPA. Comme quoi, tout est bon dans le cochon, si on peut aller chercher une idée chez la concurrence et la dévoyer :-D ... )

    ***** la paradigme catégorique

    **** s'ils n'avaient pas croisé Girard, il n'est même pas dit qu'ils auraient vu qu'une autre version est contradictoire :-D A force de mettre ou d'enlever, on a la place géographique du typage qui prend toute la place.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • GG
    GG
    je te remercie cc de ta disponibilité, qui est toujours très grande. Mais je crois que j'ai un blocage psychologique, voire plus grave une rigidité mentale croissante (l'âge?). Mais bien entendu, je vais essayer de comprendre ce que je peux de tes interventions ..
  • christophe c
    christophe c
    De mon téléphone: en gros dans cette première partie il s'agit juste de démystifier l'utilisation des variables liées en maths en L’ÉLIMINANT purement et simplement. Rien de plus mais c'est déjà très important car psychologiquement se cacher derrière le alpha problème (renommage des var liées) rend EXTRÊMEMENT perméable aux arnaques. Une fois qu'on ne gère plus que de simples calculs, on "voit tout". Et est moins crédule.

    ZF, HoTT, tout ça c'est du flan. La seule vraie chose qui compte (découverte et "dramatique" pour certains) est qu’évidemment tu ne peux accéder à la profondeur des choses que dans des théories OBLIGATOIREMENT contradictoires et qu'il fait vivre avec. Et ON PEUT vivre avec. C’est juste se balader sur un diamètre de l'univers (de tous les possibles) , connexe qui va du vrai au faux, y a pire dans la vie que ce voyage. Les gens comme HoTT et d'autres qui refusent ce voyage et cherchent à construire un ouvert non vide qui est fermé et tout petit autour du vrai (de 0) dans le connexe [0,1] faut pas leur en vouloir et les laisser se perdre puisqu'ils produisent (l'échec fait produire). Mais bon, faut pas non plus se précipiter quand ils crient au loup.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Foys
    Foys
    christophe c il n'y a que toi qui travailles dans une théorie assumée contradictoire...
    Les gens ne sont pas à la fois morts et vivants et la science s'est donnée pour but de dire ce qui se passe (le monde réel est non contradictoire *)

    Tu dis en gros "tout le monde travaille dans ma théorie sauf les naïfs" (faux!!), "ma théorie est contradictoire", "donc les gens travaillent dans une théorie contradictoire"

    Les énoncés de mr tout le monde sont typés.



    [size=x-small]* Pour anticiper un argument prévisible, même en MQ, une phrase quantique -qui n'est jamais, même dans les acceptions les plus extrêmes, qu'un sous-espace fermé d'un espace de Hilbert complexe- n'est jamais égale à son orthogonal quand l'espace est non réduit à zéro).[/size]
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Foys
    Foys
    recommendations d' amendements:

    -on introduit des types (règles à mettre)
    -un type atomique "$prop$"
    -des lettres de type $\Rightarrow,\wedge,\vee$ de type $prop \to prop \to prop$
    -une lettre "$\neg$" de type $prop \to prop$
    -pour certains types $\tau$ (liste à choisir à l'avance) des lettres $\overline {\forall}^{\tau}$ et $\overline{\exists} ^{\tau}$ de type $(\tau \to prop) \to prop$.

    -Pour tout type $\sigma$ dans les types de la liste choisie et $P$ de type $\sigma \to prop$,
    $\forall (x:\tau):P$ abrège $\overline {\forall}^{\tau}(x \mapsto P)$ et $\exists (x:\tau):P$ abrège $\overline {\exists}^{\tau}(x \mapsto P)$

    -Les objets de type "$prop$" s'appellent des phrases (ou énoncés etc).

    -axiomes à mettre

    Ah le choix de combinateurs retenus est peu pratique et en plus il est possible que des objets ne copiant ou n'effaçant aucun argument ne puissent pourtant s'écrire sans recours à $K,W$
    (d'où ma préférence personnelle pour des systèmes comme S (ou W),K,I (id), B:=x,y,z -> x(yz) et C:= x,y,z -> x z y etc).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • Foys
    Foys
    Contrairement à un cliché répandu, ZFC est typée et "$\N\in 2$" est une phrase bien typée correcte (avec $\N$ et $2$ de type $Set$ et $\in$ de type $Set \to Set \to prop$).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • christophe c
    christophe c
    Sur ta remarque sur le choix des connecteurs tu as raison. Mais ce n'était pas mon sujet. En général je mets:

    C, B (ou D, B) étage linéaire
    K étage affine
    W duplication

    Mais comme on peut faire B avec W,C,K j'ai économisé voulant en mettre le minimum.

    Pour le reste je te répondrai d'un PC. Que la théorie originelle soit contradictoire n'implique pas que les preuves y soient inintéressante et c'est bien ce qu'il se passe. Les gens non set théorie taffent dans Z mais sinon personne ne s'interdit de grossir un ZF. Encore une fois ce qui compte ce son t les preuves. N'importe quel instance du schéma de compréhension originelle s'exécute avec l'identité de toute façon. Donc le problème (moderne) n'edt vraiment plus la cohérence d'un système fixe qui s'imposerait à tous. Idem pour ton typage : j'ai répondu sur ce point dans l'autre fil face à la demande de GG
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    @foys pardon je suis au lit et n'ai pas rallumé mon PC. J'en reviens aux types. Je précise un truc que j'oublie trop souvent de dire.

    Je ne les conteste pas (pour la bonne raison que j'ai même fait un programme qui type TOUT terme). J'essaie juste de dire que JUSTEMENT faire des maths consiste à faire des exos consistant à varier la typation. Autrement dit "un théorème == une invention de typation". Il est donc COMPLÈTEMENT RIDICULE SELON MOI de vouloir imposer UNE SEUL système vu que c'est comme faire un seul exo et dire "pour la nuit des temps refaites ce même exo". Et je peux essentiellement prouver ce que je viens de dire.

    On retrouve d'ailleurs ma critique de l'autre fil: de bonnes recherches scientifiques de gens qui finissent par Peter une durite et se revendiquer fondateurs.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Foys
    Foys
    Si tu as des règles de typage ne respectant pas l'un des 6 principes suivants (les ajouts additionnels étant à la discrétion des utilisateurs) je voudrais bien les voir...
    Il n'y a essentiellement qu'une seule façon raisonnable de faire pour une vaste classe d'objets.

    $P,Q,R$ étant des types quelconques:
    (i)Pour tous $f:P\to Q$ et tous $x:P$, on a $f(x):Q$
    (ii)$x \mapsto x = \mathbf I: P \to P$
    (iii)$x,y,z \mapsto x(y)(y) = \mathbf W: (P \to P \to Q) \to (P\to Q)$
    (iv)$x,y \mapsto x = \mathbf K: P \to Q \to P$
    (v)$x,y,z \mapsto x(y(z)) =\mathbf B:(Q \to R) \to (P \to Q) \to (P \to R)$
    (vi)$x,y,z \mapsto x(z)(y)= \mathbf C: (P \to Q \to R) \to Q \to P \to R$
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • christophe c
    christophe c
    Tout est dans "vaste" et dans ce que veut dire "type". La tu n'es pas en train de parler de typage mais, sans forcément en avoir conscience, de réalisabilite.

    Tout est aussi dans "les ajouts sont à la discrétion..."

    Par ailleurs parler de "type dépendant" comme le fait HoTT est quasiment un aveu d'échec des le départ.

    Mais de toute façon je répète mon point de vue. Censurer n'est jamais bon. Il n'y a que rarement des morphismes entre théories même universelles , on ne peut pas se priver de preuves. On a déjà du mal scolairement à faire converger vers des preuves les activités si en plus on ne taffe plus que dans Peano ou proche...
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    D'un PC: je peux être un peu plus précis. Foys, n'oublie pas qu'on parle de fondements.

    Tu as raison, mais tu ne donnes pas le "bon nom" à la chose que tu décris. Il s'agit de réalisabilité et non de typage.

    Tu ne le dis pas (enfin je peux dire tu ne le prouves pas, tu le dis juste), mais ce que tu écris se prouve. Et ça n'a pas de conflit avec tout ce que j'ai dit avant.

    Prends par exemple $WJ(WJ)$. Et bien il réalise $B$ dès lors qu'il existe $A$ vérifiant $A=(A\to B)$.

    Preuve:
    $W$ réalise $(A\to (A\to B)) \to (A\to B$, donc $(A\to A)\to (A\to B)$, or $J$ réalise $A\to A$, donc $WJ$ réalise $A\to B$.
    $WJ$ réalise $A\to B$, donc $A$, donc en l'appliquant à lui-même, tu réalises $B$.

    Preuve que $J$ réalise $A\to A$. Soit $x\in A$. Alors $Jx=x\in A$.
    Preuve que $W$ réalise $(A\to (A\to B)) \to (A\to B$. Soit $x\in (A\to (A\to B)); y\in A$. Alors $Wxy = (xy)y$. Or $xy\in (A\to B)$ donc $(xy)y\in B$.

    Bref, ça ne change rien au schmilblick de dire qu'on type, qu'on ne type pas tant qu'on n'a pas précisé ce qu'est un type. Par ailleurs, dans la mesure où la tradition est de les considérer comme des pointeurs, il n'y a absolument pas lieu de prétendre leur imposer une bonne fondation. Il serait aberrant de prétendre que "par une espèce de magie naturelle", les pointeurs t'arrivent bien fondés.

    De même pour les définitions. Il n'y a aucun lieu de les prétendre bien fondés (sans boucle, puisque l'informatique est finie).

    Il n'y aurait rien de pire comme programmeur que celui qui prétendrait que son logiciel (enfin sa DLL) ne marche que quand il est confronté à un environnement qui a la gentillesse de lui présenter des pointeurs non cycliques.

    On retombe encore et toujours sur les mêmes problèmes, robustes de fondement et d'applications de la science (et de sa sécurité ingénierique):

    Je te fais un tableau:
    consistance | non cyclicité des pointeurs | typage bien fondé

    Vieilles lunes: prétendre prouver que le système s'arrête.
    Erreur fatale: Godel, Post, Turing, Chruch, indécidabilité du problème de l'arrêt.

    Bref, je pense que tu sais ce qu'est un ensemble créatif: c'est un ensemble récursivement énumérable $A$ et une fonction récursive totale $f$ telle que tout programme $p$ prétendant calculer $\N\setminus A$ se fait immédiatement ridiculiser par $f(p)$ (ie $f(p)$ est dans $A$ ssi $p$ prétend que $f(p)$ n'y est pas).

    Ces mécanismes ne sont pas des particularités, ils sont universels. Ils impliquent presque prouvablement que :

    FONDER => TAFFER dans un système qui prouve tout et porter l'attention sur les preuves et non les théorèmes.

    Tu pourras tourner le truc de la manière que tu veux, on n'en sort pas. Evidemment, une façon de faire "peiner $f$" consiste à flouter et trainer, bref tricher dans la descrption de $p$ (autrement dit garder la main et ne jamais appuyer sur "envoyer" lors du INPUT. C'est ce que font ces gens (HoTT, les publicitaires pro-catégories quand ils s'égarent en fondement, etc).
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    A la rigueur ce genre de programme pourrait être moins de l'esbrouffe s'il était vrai qu'entre théorie universelle il y a des morphismes, mais ce n'est pas le cas, donc de toute façon l'attitude mathématique est OBLIGEE DE SE RESUMER à :

    "Msieurs-dames, j'ai prouvé $ZF\to A$; $ZFC\to B$; etc (par exemple $NF\to C$)"


    On ne peut pas imposer de cadres. Métaphore: vrai; faux vivent dans un connexe et ces entreprises vouées à l'échec tentent de construire un minuscule voisinage ouvert ET fermé autour de $vrai$. Chaque fois qu'elles ont construit un ouvert (qui donc n'est pas fermé), la tentation (et à l'instar des cordistes en physique) est grande pour cette communauté de tricher pour tenter de substituer à la non fermeture des discours publicitaires absconses et des diversions, les pensant aussi efficaces que s'ils avaient construit un fermé.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Je précise ce qu'est un morphisme entre théories:

    C'est une fonction $\phi$ telle que pour tous énoncés $X,Y$

    $X\to Y$ est un théorème de $T_1$ ssi $\phi(X)\to \phi(Y)$ est un théorème de $T_2$ et qui vérifie en plus:

    $\forall X,Y: \phi(X\to Y) = (\phi(X)\to \phi(Y))$
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • GG
    GG
    @cc, pour le moment ma seule contribution à ce fil stratosphérique est de te signaler, comme tu aimes bien l'utiliser, que le mot "esbroufe" ne prend qu'un "f". Oui je sais, ce n'est mathématiquement pas bien riche, tu vois mon niveau ! :-)
  • Martial
    Martial
    @GG : en principe je ne suis pas trop mauvais en haurretograf, mais là tu viens de m'apprendre quelque chose : j'ai toujours écrit "esbrouffe" avec 2 f, peut-être pour mieux "esbrouffer" les gens, lol.
    C'est comme quand un mec m'énerve, j'ai envie de le "giffler", relol.
  • GG
    GG
    @Martial, :-)
  • Foys
    Foys
    christophe c a écrit:
    On retombe encore et toujours sur les mêmes problèmes, robustes de fondement et d'applications de la science (et de sa sécurité ingénierique):

    Je te fais un tableau:

    consistance | non cyclicité des pointeurs | typage bien fondé



    Vieilles lunes: prétendre prouver que le système s'arrête.
    Erreur fatale: Godel, Post, Turing, Chruch, indécidabilité du problème de l'arrêt.

    Ce sont des épouvantails ça (personne ne prétend prouver la consistance des maths en général et dire "mais ils le pensent secrètement" consiste surtout à se dire télépathe), le typage d'un terme est décidable et la forte normalisation est un théorème soft (et pour des combinateurs le graphe de toutes les réductions d'un terme typé est carrément fini).
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • christophe c
    christophe c
    Foys a écrit:
    le typage d'un terme est décidable et la forte normalisation est un théorème soft

    C'est bien pour ça (COQ est fortement normalisable) qu'ils ne peuvent prétendre, même pas un peu, à quoi que ce soit de fondant.

    Le premier devoir d'un système fondant est de ne SURTOUT PAS NORMALISER. J'espère que tu connais assez de CCH pour comprendre que c'est isomorphe à dire que le premier devoir de l'OS de ton ordinateur de bureau est de ne pas s'éteindre subitement sans te demander ton avis.

    Le pointeurs et les GOTO de ton OS se doivent de boucler. J'ai l'impression que c'est peut-être un point de la CCH que tu n'as pas visité assez longtemps. Tu ne serais pas le seul t'inquiète.

    Je pense par contre que tu le sais, j'en ai parlé dans l'autre fil, il faut savoir que la réciproque est vraie aussi et que c'est peut-être ça le plus édifiant: normalisation forte => existence d'un typage trivial (précisément dans $\to; \cap$). De plus la question $x\mapsto [x$ est-il fortement normalisable$]$ est un ensemble récursivement énumérable universelle, bien entendu, mais de plus créatif. Autrement dit, il revient strictement au même de chercher à typer que de chercher si un programme s'arrête. C'est prouvablement la même activité.

    Donc un système de typage qui normalise fortement ce n'est rien d'autre qu'une fonction récursive totale. Et le vendeurs de cette fonction ne sont rien d'autre que des gens qui disent "notre $f$ résout tous les problèmes", c'est à dire diffusent de la publicité ... mensongère.

    Si je me suis permis de techniciser mes discours d'avant, je ne change pourtant pas de propos, c'est juste parce que toi, je crois savoir que tu as pas mal cherché à avancer dans ce domaine (au point même de fournir une table de traduction entre les combinateurs tels que je les nomme et tels que la convention les nomme :-D ) mais je continue de penser que c'est de l'excellente recherche MAIS QUE CA N'A AUCUNE VERTU FONDATRICE.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • christophe c
    christophe c
    Foys a écrit:
    le typage d'un terme est décidable

    Attention, dit comme ça, c'est profondément faux, donc tu as dû être imprécis. Peut-être pensais-tu juste au typage dans $L(\to)$? Mais là, c'est évident, mais HS.
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Foys
    Foys
    christophe c a écrit:
    Attention, dit comme ça, c'est profondément faux, donc tu as dû être imprécis. Peut-être pensais-tu juste au typage dans ? $L (\to)$ Mais là, c'est évident, mais HS.
    Je ne connais pas tous les innombrables systèmes de typage qui existent loin s'en faut et pensais en priorité au lambda calcul/LC avec types simples certes, mais en informatique, dans les langages usuels si le système ne peut pas typer il envoie bouler l'utilisateur (ocaml ...).
    Ce n'est pas une exigence déraisonnable.
    Une fonction est un ensemble $f$ de couples tel que pour tous $x,y,z$, si $(x,y)\in f$ et $(x,z)\in f$ alors $y = z$.
  • christophe c
    christophe c
    Attention caml a prévu une parade en te laissant créer les types que tu veux (j'en sais quelque chose vu que j'en ai abusé des centaines de fois :-D )
    Aide les autres comme toi-même car ils sont toi, ils sont vraiment toi
  • Chaurien
    Chaurien
    Que signifie GG, Gouvernement général ?
  • GG
    GG
    Grande Gueule ?!
    Bon, pour mettre les points sur les i, cc m'a fait l'honneur immérité d'ouvrir un fil à mon nom, auquel je n'ai pas les moyens intellectuels de participer :-)
Connectez-vous ou Inscrivez-vous pour répondre.

Bonjour!

Pour participer au forum, cliquer sur l'un des boutons :

Connexion S'inscrire

Catégories

In this Discussion

Qui est en ligne 33

DomGaBuZoMeuJLapinMatricule_63Paul-ACvpf +27 Invités