Physique et téléphones

Vu ton edit, je n'avais pas répondu au tout début de ton post. Oui, tu as vu que j'avais répondu pour l'essentielle fausseté.

Pour Elicut, oui, mais pas que. Il faut que tu aies conscience que "Elicut" est un titre et non un théorème dans le sens qu'il y a un théorème elicut improvisé par théorie (on peut unifier, si ça t'intéresse, je te dirai comment).

Sans cette précision, ça n'aurait pas grand intérêt: tu pourrais dire << Peano me prouve Q, donc il existe un axiome A de Peano tel que A=>Q est un théorème absolu, j'élimine alors les coupures de la preuve trouvée de (A=>Q)>>. Mais faire ça "n'élimine rien du tout" de spécifiquement péaniste.

Il faut donc préciser avant toute chose ce qu'on a envie d'appeler "éliminer les coupures des preuves péanistes".

En réalité, Peano est une curiosité de musée dans laquelle, "éliminer les coupures péanistes" est ad hoc. On décrète qu'on ne donne plus des variables (des lettres) à manger aux preuves, mais carrément des entiers bien concrets. L'élimination des coupures consiste alors, en plus des coupures habituelles à remplacer la récurrence par une preuve de la récurrence dans le cas particulier suivant:

$$ (R(0) + ( \forall x: [R(x) \to R(x+1)] ) )\to R(1+1+1...+1)$$

Hélas, hélas, ce qu'on obtient n'est qu'un résultat esthétique car toutes les formules "vraies dans IN" sont prouvables** (sans coupure et même sans retour-arrière) dans ce paradigme et donc on a l'air "un peu idiot" de ne s'intéresser alors qu'aux preuves dont on a éliminé les coupures comme s'il s'agissait d'un exploit (les retour-arrière*** sont autorisés dans les preuves sans coupures)

** je te le laisse en exercice

*** Dans le jeu de la vérité, $\forall $ affronte $\exists$ en défendant le faux, comme tu sais. Le jeu de la vérité est bien plus sévère pour le joueur vrai que le jeu de la preuve face à une même phrase, mais en contre-partie, on "sait à qui on a affaire", ie les phrases atomiques sont décidées (leur valeur de vérité est fixé un axiome).

Le jeu de la preuve sans coupure est "presque" le même jeu, sauf que (et ce n'est pas rien) tu as le droit de faire un retour-arrière, exemple dans une partie $\forall a\exists b\forall c: R(a,b,c)$:

faux joue $a:=x$
LABEL
vrai joue $b:=y$
faux joue $c:=z$
vrai retourne à LABEL
vrai joue $b:=z$
faux joue $c:=tt$
vrai retourne à LABEL
vrai joue $b:=t$
faux joue $c:=e$
etc

Les conditions gains pour vrai (qu'il vaudrait mieux appeler prouveur) sont améliorées puisque sont :

$$R(x,y,z) \vee R(x,z,t)\vee R(x,t,e)$$

à ce stade de la partie.

GA a écrit:

j'ai du mal à voir ce qui confère à certains axiomes le fait d'être plus facilement acceptés comme clonables que d'autres énoncés

Plus généralement, tes questions sur la logique linéaire.

Oui la vulgarisation de JYG est pas mal, mais elle ne sert à rien pour les détails "fondamentaux". Ce qu'il faut intégrer et mettre dans ses tripes, c'est que c'est LA SEULE logique réelle utilisée par l'humain REELLEMENT.

J'ai t'ai déjà dit sa règle principale: si avec le groupe $R_1$ de ressources, tu peux obtenir $A$ et avec le groupe $R_2$ de ressources tu peux obtenir $B$ alors avec le groupe de ressources $R_1 + R_2$, tu peux obtenir $A+B$.

Il est bien important de comprendre que c'est la seule règle y compris en logiques traditionnelles, mais qu'on oublie de "le signaler". La logique traditionnelle AJOUTE quelque chose qui mérite de s'appeler d'une seule manière: axiome.

Cet axiome est basé sur de profondes convictions philosophico-éthiques, que même les enfants qu'on été les matheux ont tellement ressassé cet axiome pour le mettre en doute ou l'accepter, qu'ils en ont laissé une trace indélébile dans la mémoire de qui ils deviendront 50ans plus tard. Qui (devenu grand scientifique) ne se souvient pas avoir dit à ses élèves ou autre <<ces vérités sont immuables>> à propos des vérités mathématiques.

Dès lors, les logiques traditionnelles sont décrites comme suit:

si avec le groupe $R$ de ressources, tu peux obtenir $A$ et avec le groupe $R$ de ressources tu peux obtenir $B$ alors avec le groupe de ressources $R$, tu peux obtenir $A+B$.

Plutôt que comme suit:

si avec le groupe $R$ de ressources, tu peux obtenir $A$ et avec le groupe $R$ de ressources tu peux obtenir $B$ alors avec le groupe de ressources $R+R$, tu peux obtenir $A+B$.

avec un alinéa qui dit que << et sachez que comme $R\to (R+R)$ ....>>

En résumé, il y a un profond mystère (en train de se résorber depuis 50ans) sur nos perceptions de la pérennité des axiomes et de la générosité de la Nature. D'où ma phrase: "c'est mieux de cloner des axiomes que de cloner leurs conséquences" quand on discute avec un sceptique sur des points physiques"

A propos des preuves sans coupure: ce qu'il faut bien comprendre, c'est qu'elle sont, même si un peu "sales", certes, des "non-preuves" en ce sens qu'elles sont encore plusss des preuves que des preuves habituelles. Le lecteur n'a "vraiment rien à faire", et croit juste lire les axiomes (autrement dit, les hypothèses que son adversaire prouveur lui demande de ne pas discuter). Peut-être pourrais-je t'inviter à en passer en revue quelques unes avant de continuer à "imaginer" ce que donnent les théorèmes sur la MQ une fois qu'on en a éliminé les coupures? Mais il faudrait que je te trouve un réservoir, et c'est pas évident (quasiment toutes les preuves publiées, même pédago, sont coupées (les pédagos, quand elles sont valables sont même souvent encore plus coupées que les autres!!)

GA a écrit:

que si on remplace n'importe quelle variable dans l'énoncé par un vrai entier, alors le texte donne une vraie démonstration

Non, mais justement, ça c'est un préjugé, que de croire qu'il y a "de vrais entiers". N'oublie pas que l'alternance $\forall / / \exists$ met un bordel faramineux.
Beaucoup de gens pensent juste à quelques exemples, je te donne donc un truc pour "ressentir profondément" l'envisagement que Peano soit contradictoire:

1/ Tu prends une fonction qui croit très très vite. Par exemple Ackermann. Mais tu la choisi démontrablement terminante dans Peano quand-même

2/ Tu la décris avec un prédicat plutôt qu'un symbole fonctionnel. Par exemple pour Ackermann:
2.1/ $\forall ... : U(x,0,x+1); [U(x,r,z)\wedge U(x+1,y,r)] \to U(x+1,y+1,z)$

3/ Tu ajoutes à Peano $\forall x: non(U(1000,1000,x)$

Ca te donne une théorie contradictoire. Bin, tu vas voir l'énoooooorme différence entre le ELicut où on garde les axiomes comme tels et le Elicut où on exécute aussi les axiomes (avec un cadre changé).

C'était en réponse à

tu voudrais éliminer des usages de l'axiome de récurrence dans les démonstrations peanistes. Etant donné que c'est un axiome, il n'y a rien à éliminer, non ?

Je précise que ce n'est pas moi qui veux, c'est juste comme je te l'ai dit, une éthique générale: elicut est un titre de chapitre, et pas un théorème (sinon on s'entiendrait au banal premier elicut démontré et ce serait tout).

Le cadre pour comprendre ça est celui qui permet de comprendre "quels sont les bons axiomes". Autrement dit, celui où on "démontre les axiomes". Une "bonne" théorie est une théorie dont les axiomes sont "démontrables" (la seule théorie connue à ce jour ayant cette propriété est ZF (ou plus généralement la TDE avec ALL compréhension), et c'est ce point que j'essaie souvent de faire comprendre de manière vulgarisée aux gens qui s'auto-improvisent à a petite semaine "refondateurs" alors qu'ils apportent des "axiomes ad hoc" sans légitimité objective (catégoriciens, théorie homotopique des types, etc).

Bien entendu, le problème de légitimer la légitimité de la légitimité de tels axiomes et pas d'autres est encore un problème, mais il y a "une route" disons. Peano n'est pas une bonne théorie, mais on peut la plonger dans une théorie dont les axiomes sont "prouvables", ie où l'exécution avec le combinateur identité (ie l'instruction qui ne fait rien) est possible pour tous ses axiomes (extensionalité mise à part évidemment), en l'occurence, c'est ZF - axiome de l'infini (il dit la même chose que Peano en termes d'apports scientifiques, mais à la différence de Peano, c'est une théorie "prouvable" (ou plus précisément "légitimable").

Autrement dit, pas besoin de "prendre une initiative humaine" pour avoir l'énoncé Elicut pour elle, il suffit de dire que les termes venant de ses preuves (où les axiomes ont été remplacé par J) sont normalisables (ie leur exécution termine). Mais je papote, mais sache qu'il faut "entrer un peu dedans", c'est une spécialité.

Mais "pour faire plaisir aux gens", on peut retourner ensuite dans Peano, traduire ça et ça te donne à peu près le résultats que je t'ai signalé (j'ai bien insisté sur sa seule qualité esthétique, puisque VéritéArithmétiques tout entier est prouvable sans coupure)

Cf plus haut : si les coupures ne sont que des appels à des lemmes, alors je ne comprends pas trop cette phrase.
Et, enfin, en quoi les retour-arrières sont avantageux ?

Dans le jeu de la vérité, pas de retour-arrière. Mais en contre partie toute les formules atomiques sont décidées par l'arbitre. Autrement dit, tu joues à ce jeu dans un "modèle" autrement dit dans une théorie complète.

Alors qu'au jeu de la preuve, quand on arrive finalement à $23\in Germaine^2$ et que la parole est à l'arbitre, et bien il dit "j'en sais rien, débrouillez-vous".

Une sans coupure n'est rien d'autre qu'une stratégie qui gagne au jeu de la vérité avec juste le petit relachement que le joueur peut revenir en arrière. De sorte qu'à la fin, on a une liste finie de phrases. Elles ne sont pas décidées, ce sont juste des phrases (on n'est pas dans un modèle, on traite tous les modèles en même temps), l'arbitre fume une clope et n'est pas disponible. Par contre, pour que le prouveur gagne, il lui suffit d'arguer qu'est présent un $A$ dans la liste et un peu plus loin un $non(A)$. Car même sans arbitre, ni modèle, il peut dire au prouveur (tu vois bien que j'aurais gagné la partie sans retour-arrière qui a abouti à la feuille A ou celle à la feuille nonA).

Et pour info "éliminer les lemmes", aboutit à une stratégie gagnante à ce jeu pourtant à vue de nez extrêmement défavorable au prouveur.

Je viens de lire ton post. Permets-moi de te répondre plus tard et de soigner mes réponses. Je le relirai plusieurs fois pour bien m'imbiber de ce qui est resté flou.

oula, non, j'ai l'impression que tu as compris très exactement à l'envers.

JUSTEMENT, le "phénomène général" de l'élimination des coupures ne se réduit pas aux théorèmes célèbres qui affirment et sont prouvés depuis longtemps qu'on peut éliminer les coupures d'une théorème pur (ie sans axiome). Sinon, je n'utiliserais pas le sigle "ELICUT" (qui reste assez vague) pour désigner le phénomène général, j'aurais donné un nom aux 2-3 théorèmes classiques et basta.

Ce qui se passe, et c'est plus récent, j'en conviens, c'est qu'il y a en maths des "bons axiomes" et des "mauvais axiomes". Par exemple, tous les "délires (histoire de faire crier dom, mais pas sûr qu'il lise ce fil)" auto-revendiqués "refondateur" sont très exactement "fautifs" de ce point de vue car ils utilisent des "axiomes ad hoc" inventés par le génie du moment ou le groupe de personnes qui fait du lobbying pour sa passion (l'exemple des catégories, ou encore celui récent du gros traité sur la théorie des (soit disant homotopiques) types, etc.

Très précisément (le choix des mots "bon/mauvais" est provocateur, j'aurais pu dire "vert/rouge"), un axiome est bon quand il est "garantissable" par la Nature. Sinon, on le considère comme une hypothèse que l'on attribuera poliment à son ou ses auteurs et c'est tout (on le laisse avec un tag "hypothèse pure" lors de l'exécution de la CCH). Digression: le fait que COQ ne marche pas*** par exemple est justement dû à une volonté "idéologique" de boycotter ça.

Le tag "ELICUT" c'est quand tu remplaces MEME certains axiomes, a priori complètement gratuits, par des instructions précises. Et d'ailleurs, il est important de préciser qu'il n'y a pas de théorèmes de terminaison, sauf pour les systèmes "triviaux"** n'ayant que peu d'intérêt (logique pure, arithmétique du second ordre), et même mieux que ça: il ne peut pas y en avoir car "terminer" est synonyme de "ne pas marcher" en réalité profonde (imagine ton pc qui s'éteint subitement parce qu'il a "terminé" :-D )

L'exemple archétypal de bon axiome est le schéma total (sans bridage) de compréhension, c'est à dire quand tu exécutes un axiome de la forme $[\forall aR(a)] \to [Q:=R(RemplacePar(a,UneRelationDefinissableQuelconque)]$ avec le combinateur $J$, autrement dit quand tu considères que $[\forall aR(a)] \subset Q$ est une VRAIE INCLUSION ENSEMBLISTE et non pas un "machin" baroque

Par exemple, la célèbre preuve qui a provoqué la crise des fondements est tout à fait exécutable et bloque l'ordinateur en le plongeant dans une boucle stérile. Mais il n'y a pour autant aucun problème, on le sait, on ne s'amusera à l'exécuter que pour des raisons précises (par exemple priver un pirate de l'accès à d'autres options, ou pour autodétruire la machine).

Bref, en résumé, comme de toute façon toutes les maths sont écrites dans ZF, tu peux retenir qu'éliminer les coupures d'un théorème de maths (enfin plutôt exécuter), quelqu'il soit, ça consiste à faire la chose suivante:

1) Transformer en terme ta preuve
2) Remplacer les instances de l'axiome d'extensionalité (qui n'est pas réalisable) par la lettre $E$
3) Remplacer les instances des autres axiomes de compréhension* par $J$ (le combinateur tel que $\forall x: Jx=x$)
4) Lancer la machine et contempler. (Eventuellement tu auras mis des tags de communication pendant l'exécution de manière à dialoguer avec la preuve du théorème).

(A noter que grace à l'intervenant alesha, il y a 2 ans, tu peux même t'assurer pour pas cher la TERMINAISON du processus en éliminant les dupliqueurs $W$ du terme et en les remplaçant par la preuve de $(A\to (A\to )\to (A\to $ à partir de l'extensionalité. Par contre, le problème est que le platonisme extrême de l'extensionalité entraine que les alertes de terminaison ce faisant sont assez frustrantes (elles donnent envie de réintroduire des $W$ à la main et relancer en appuyant sur entrée, mais elles permettent tout de même d'admirer la superpuissance de l'extensionalité que la plupart du temps les gens ignorent et méprisent (au poins qu'ils en oublient, par exemple dans le secondaire, même jusqu'à d'avoir conscience qu'ils l'utilisent (passage de $\forall x: f(x)=g(x)$ à $f=g$), provoquant l'abandon de leurs élèves très tôt dans la scolarité))

* Sous la forme très précise où je l'ai signalée ci-dessus. Pas en l'écrivant comme un sagoin avec des $\exists, etc$ :-D

*** est compliqué et peu utilisable par le peuple

** ils n'étaient bien sûr pas triviaux à l'époque où ils ont été découverts (années 70-80), car c'était nouveau.

Je réponds d'abod à quelques unes de tes questions pour lesquelles peu de lignes suffisent.

Ton point7: tu es gêné par ce que je qualifie de détail négligeable. Oui $ZF\subset TDE$, donc quand je t'ai dit que toutes les maths sont écrites dans $ZF$, ça ne contredit pas qu'elles sont écrites en TDE, mais c'est juste que factuellement, les gens, actuellement, n'utilisent pas d'axiomes de $TDE\setminus ZFC$. J'espère que cet aspect ne te gênera plus.

Ton point6: je te confirme que tu as raison, ne doute pas de ça, pas d'ambiguité la dessus.

Ton point5
L'axiome de compréhension non bridé dans sa forme traditionnelle est:

$$ \exists a\forall x: [x\in a\iff R(x)]$$

Mais cette forme fait intervenir un $\exists$ qui n'existe pas dans le langage (même si on peut le définir plus tard) et donne une illusion maladroite sur "l'altitude" de cet axiome (qui ainsi est présenté comme un banal axiome dogmatique).

La bonne forme est la suivante:

$$ [\forall aR(a)]\to Q $$

où $Q$ s'obtient, à partir d'une relation $S(y)$ en remplaçant toutes les apparitions d'une suite de signes de la forme $t\in a$ dans $R(a)$ par $S(t)$. La contrainte est qu'il ne figure jamais de $a\in quelquechose$ dans la phrase $R(a)$.

Cette forme est équivalente à l'autre, mais elle est plus "correcte" pour des raisons que je vais t'expliquer ultérieurement. Exemple d'utilisation sur le fameux paradoxe de la CDF, peu importe le symbole $\exists$, il pourrait être retiré (exercice) mais ça rallongerait:

$$(\forall a [\exists x: (x\in x\iff x\in a)])\to [\exists x: (x\in x\iff x\notin x)]$$

où j'ai particularisé avec: $S(t):=t\notin t$

En français, cette forme d'expression se dit comme suit, si un truc arrive à tous le monde, il arrive à la collection des $x$ tels que $x\notin x$.

Ton point2: là encore tu as compris, c'est bien ça.





Ton point9: alesha est un intervenant du forum qui m'a informé, et rempli mon esprit de lumière ce faisant, il y a 2ans environ je pense, que :

$$ [((a=b)\to ((a=b)\to X)] \to [(a=b)\to X]$$

est un théorème de logique linéaire. C'est certes trivial une fois qu'on te le dit, mais encore faut-il y penser quand on ne te le dit pas!!

Comme, sans clonage (et même sans forcément passer par le droit de poubelle, mais c'est plus fin), tout phrase est affinement équivalente à une égalité en théorie des ensembles, il suit que ZF TOTAL (ie le ZF usuel accompagné de ses habituels raisonnements en logique classique, sans restriction) est en fait un simple conséquence déductive du ZF + logique affine (que personne n'a jamais l'idée saugrenue d'utiliser), et même du ZF + logique linéaire. Ca permet, par exemple de formaliser pourquoi les topos "ne marchent pas"*** ( pour comprendre les choses en profondeur) et d'expliquer bien d'autres petits trucs divers et variés qui en fait constituaient jusqu'à présent des problèmes qui à un chouya près auraient pu être annoncés officiellement ouverts sur wikipedia par exemple.

*** ils ne prennent qu'une partie "bancale" (ou si tu préfères un mot neutre: assymétrique**) de l'univers (ils mélangent "vieilles fonctions" (au sens du ground model du forcing) et "nouveaux ensembles". C'est bien entendu passionnant et intéressant d'étudier ces structures, mais elles ne peuvent refléter honnêtement les mécanismes atomiques.

** exactement d'ailleurs comme le faitla logique intuitionniste, qui refuse de mettre "plusieurs formules à droite du séquent" (cette phrase sera précisée quand je te posterai des réponses complètes à 1+3+9


Les points 1;3 et 8 expriment en fait le même désarroi, pour lequel je vais te faire un autre post détaillé.

Et pardon, quelle galère, j'écris les arbres avec <<slash frac>> à cause de ma béotie en latex. Mais je pense que tu peux taper "calcul de séquents" et visiter quelques pages wiki qui te familiariseront avec ces arbres de preuves.

De même téléphone : je reviens dimanche mais sois rassuré : non seulement tu peux l'écrire mais en plus c'est AU SENS PROPRE la même chose :-D vue l'abréviation.

Je ne pourrai réagir que d'un PC. Merci de remonter cette thématique en tout cas. Depuis j'ai en fait découvert que MEME LA RR implique presque le slogan "multi". En fait c=infty. Mais quand on se déplace on est obligé de "descendre des pentes" dans des fils supplémentaires ce qui conduit à arriver systématiquement dans des mondes qui ont un peu d'avance. Il est d'ailleurs intéressant de passer en projectif pour mieux voir.

Un moyen simple d'ailleurs de le ressentir "en dur" est d'aller en décapotable en 1H sur la galaxie voisine. Le vent dans les cheveux ne trompera pas sur la vitesse moyenne à laquelle on aura fait le voyage alors que les calculs abstraits RR type ne disent rien à part signaler cmt les horloges vont nous signaler l'heure.

Bon hélas de mon téléphone pour ne pas te faire attendre trop. Il n'y a AUCUN aléatoire dont dépendraient les argument de ma thèse et ce pour une raison simple: je ne veux pas donner prise à l'objection "à condition d'admettre le paradigme probabiliste".

Dans le protocole casino on a seulement une règle du jeu croisée qui exige que le numéro que doit tenter de deviner Bob pour gagner EST COMMUNIQUÉ à Léa et que celui que Léa doit deviner est COMMUNIQUÉ à Bob.

C'est une manière pour le casino de se contraindre à l'honnêteté en offrant de quoi lui faire un procès PLUS TARD (quand Léa et Bob se retrouveront pour faire le bilan.

Un téléphone est casino inoffensif quand le fait que Bob et Léa en dispose et puisse l'utiliser avant de miser ne change CONCRETEMENT rien à leurs perspectives.

C'est SEULEMENT ENSUITE et c'est juste un exo de maths qu'Anatole à fait de tête avant même ma seconde respiration quand je l'ai informé de la definition qu'on s'aperçoit qu'une FACON EQUIVALENTE de le dire consiste à affirmer qu'il existe un jeu de probas LOCALES qu'on peut attacher SEPAREMENT à chaque combiné qui est compatible avec la garantie au sens que les situations qui violent la garantie ont une probabilité NULLE de survenir en faisant le calcul naïf le plus défavorable possible au défendeur pour éviter toute objection.


Un exemple très simple de téléphone (pas trop puissant et non TSD) QUI N'EST PAS CI est le suivant: Léa tape un nombre entier n et recoit sur son ecran i qui vaut 0 ou 1. Bob de son côté tape un j qui vaut 0 ou 1 et recoit sur son ecran un entier p. Le téléphone garantit i=j implique n=P

Autrement dit ce téléphone injecte IN dans 2.

J'aurais pu mettre 3 à la place de IN.

Je n'ai pas ma thèse sous les yeux de mon téléphone. Mais le post précédent que je t'ai écrit repond le plus précisément possible sur "ce qui se passe". J'ai lu tes trucs rouges. Si tu veux je demanderai à Anatole qui est à Paris de lire ton post. De toute façon dès que PC je te répondrai.

1) au moins un des 2 (en fait c'est individuel-like: Bob empoche ses mises et Lea aussi. Le fait que Léa connaisse le numéro qui ferait gagner Bob est une simple "garantie juridique" pour l'equipe).

Prends l'exemple que je t'ai mis. Le chiffre gagnant est un nombre entre 1 et 10. Léa le tape et sur l'écran de Bob il s'affichera à la seule condition que Bob devine le bit qui s'est affiché sur l'écran de Léa.

2) je relirai, mais comme il y avait un calcul... J'ai zappé pardon:-D

Ça nécessite vraiment que je te réponde d'un PC car si je comprends ta quedtion2 il y a de gros malentendus. Il n'y a aucune fonction ici c'est bien plus simple.

Pour la 1) je te le redis si Bob devine son nombre il empoche la mise epictout même si Les ne deviné pas le sien. Mais du col de Peyresourde sans pc ni bonne connexion je ne peux écrire les dissipations de mâle tendus.

Je reprends dans l'ordre.

Ton post d'hier 11h13. Quand les gens ne veulent pas être convaincus ils ne le sont pas de toute façon. L'important est que toi aies compris. Les physiciens en question auraient besoin de temps et de sérénité pour comprendre que si on peut falsifier toute f, c'est qu'il n'y a pas de f et non pas une f espiègle qu'on ne deviné jamais. Il faut que tu saches que pour la plupart des physiciens l'existence d'une stratégie gagnante aux échecs qui est un banal théorème de maths n'est pas un truc qui leur est familier. Ils ont t tendance à croire que la f évoquée est dans le présent et dépend des coups. Ils ne comprennent pas quand on leur parle de FONCTION et que ça s'applique AUSSI à leur x|

---

> f_x(x) où f_x est la fonction qu'il prétendent dépendre de x.

Pour la question 2 sur les casino inoffensifs j'ai téléphoné à Anatole pour prendre conseils mais comme il avait modifié une définition ça complique. Mais AVANT TOUT tu as des téléphones dont on étudie les puissances. En dehors de l'instance UNE SEULE FOIS UTILISEE (dans mon chap5 je crois) d'envisager une fonction incluse dans une garantie ce procédé N'EST jamais à utiliser "par essence" même du sujet d'étude. Remplacer R par f c'est CHANGER le téléphone.

Concernant la casino inoffensifs nous sommes tombes d'accord que la def la plus digérable est celle avec les probas locales. Dans un premier temps tu peux oublier l'autre def.

J'en reviens à ton post d'hier. Après de nombreuses expériences comme on a SYSTÉMATIQUEMENT falsifié la f proposée ou tirée au sort (mais il faut le voir en live) on est convaincu qu'il n'y a pas de f. Au même titre que quand un mec gagné SYSTÉMATIQUEMENT le gros lot du loto tout le monde se mettra à penser qu'il est informé.

Mais ces choses ne surviennent que quand le choc se produit. Tes physiciens ont peut être la même réaction qu'un ami DR il y a 20ans. Durant 1H nous avons discuté sans nous rendre compte que quand je disais forall ça voulait dire forall (il traduisait SYSTÉMATIQUEMENT en "for almost all" par habitude). En gros il 'e s'etonnait que "pour tout x dans IR , x différent de 5" :-D. 1H de perdue pour un malentendu bête et méchant .