Réalisabilité de l'axiome de Peirce
Bonjour,
Christophe, tu as une histoire sur la réalisabilité de l'axiome de Peirce, où tu te fais emmener à l'endroit où tu veux aller en mentant au chauffeur de taxi. Est-ce que tu peux la raconter encore une fois et commenter un peu ?
Christophe, tu as une histoire sur la réalisabilité de l'axiome de Peirce, où tu te fais emmener à l'endroit où tu veux aller en mentant au chauffeur de taxi. Est-ce que tu peux la raconter encore une fois et commenter un peu ?
Connectez-vous ou Inscrivez-vous pour répondre.
Réponses
Convention : tu paies quand tu as eu le produit.
Tu demandes au Taxi de t'emmener à la gare A. Il accepte en t'annonçant que le prix est A=>B. Tu lui donnes un faux billet pour ce trajet.
Il t'emmène. Il s'aperçoit seulement que son billet est faux quand TOI tu es arrivé en A. Il ne peut le savoir avant puisque la fausseté ne peut être révélée qu'en le glissant dans le composteur de la gare A
Cela prouve ((A=>B)=>A)=>A.
Remarque: le fait que de l'obligation d'être dans A pour dénoncer la fausseté est important et profond. In the real life , il n'est pas possible de prétendre que le "passage" de A à B n'est pas fourni par un objet sans rien connaitre de A
C'est l'implémentation des try.. finally
Supposons que ton environnement $e$ agresse $((A\to \to A)\to A$. Cela veut dire qu'il t'offre un robot $u$ qui réalise $(A\to \to A$, puis ensuite agresse (ie devient un environnement $e_2$ qui ) $A$.
Tu donnes $f$ à ton robot $u$ en lui faisant croire qu'elle réalise $A\to B$. Il va donc la mettre en bouclier contre $e_2$ de sorte que le nouvel environnement (tu peux l'appeler comme tu veux) agresse $(A\to \to A$, et in fine, $u$ va gagner dans cet environnement par définition, puisqu'il réalise cette phrase.
Alors attention quand-même. Encore faut-il que tu n'aies pas menti en vendant $f$ comme une réalisatrice de $A\to B$. Ce dépend donc de ton paradigme. Jusqu'ici tout va bien, mais ensuite, le paradigme est important (tu t'en doutes puisque sinon, le RPA serait prouvable de manière intuitionniste (voir linéaire si on n'accepte pas la duplication de robots).
Voici le paradigmes qui fonctionne (parmi peut-être d'autre, mais le présent a gagné les faveurs de l'histoire de la science actuelle).
Je te prouve donc que $f$, si elle a un certain comportement, réalise $A\to B$ (en fait, elle réalise $A\to Tout$ mais peu importe, à aucun moment il ne sera question de $B$).
Soit $s$ un environnement qui agresse $A\to B$. Autrement dit, il fournit à $f$ un robot $a$ qui réalise $A$ et ensuite devient un environnement $s_2$ qui agresse $B$. Comment va réagir $f$? Réponse: elle va téléporter $a$, en "remontant le temps", devant l'environnement $e_2$ qui agressait $A$. Sauf que maintenant, $a$, qui réalise $A$ se trouve devant un environnement $s_2$ qui agresse $A$ et tout marche bien.
Mais comme tu vois, il a fallu à $f$ la capacité d'appuyer sur son siège éjectable pour revenir devant $e_2$. Pour ça, li fallait être dans des conditions où son agresseur $s_2$ l'y autorisait. C'est ce qui explique par exemple que le RPA ne peut pas toujours s'appliquer dans la science appliquée.
Ce qu'ils font et ce que fait le soldat armé de son robot $u$ est qu'il ANALYSE FINEMENT (faut avoir le temps) son environnement $e_2$, il en fait une photographie haute résolution, puis utilise "une imprimante 3D" en quelque sorte pour en fabriquer un factice $e'_2$ face auquel il confronte le robot $u(f)$ (cette notation désigne le fait de mettre un bouclier $f$ puis d'exécuter $u$).. Il attend alors pour voir ce qu'il va se passer et là, DANS TOUS LES CAS IL GAGNE, puisque si $f$ est sollicitée, il peut appuyer sur STOP la simulation de guerre et récupérer le $a$ fourni par l'environnement factice qui a hérité de $e'_2$.
Je ne me suis pas encore plongé dans les détails, mais là où j'ai une difficulté c'est de savoir pourquoi diable le chauffeur de taxi est assez bête pour me conduire en $A$. Je reviens quand j'ai compris ou alors quand j'arrive à mettre le doigt où je bloque.
L'histoire que je vais vous raconter concerne deux personnages que je vais appeler G (Griffin) et K (Krivine) ("Griffin", ça ressemble un peu à une version américanisée de "Krivine", vous ne trouvez pas ?) puisque ce sont deux héros de la vraie vie.
G : Hey K, j'ai une machine typée $((A\to \to A) \to A$ !
K : Pffff, si c'était vrai ça se saurait !
G : C'est pas un argument, ça ! Donne-moi voir une machine typée $(A\to \to A$ et on la met dans ma machine !
K : Ok ok, voilà $p$, on le met dans ta machine ?
G : Minute papillon ! Ton $p$, qu'est-ce qui me prouve qu'il est bien $(A \to \to A$ ?
K : T'es un peu tatillon... Ben donne voir une machine typée $A \to B$, on la mettra dans ma machine et on verra bien.
G : Oh, volontiers. Voilà $q$.
K : Il m'a l'air louche, ton $q$.
G : Tu me crois toujours pas ? Donne voir une machine typée $A$, et on la mettra dans mon $q$.
K : Pfffff ça sent l'arnaque ton truc. Tiens, voilà un $a$ typé $A$.
G prend $a$ et se barre en courant, en jetant $q$ par dessus son épaule. K ramasse $q$ et voit marqué dessus "je t'ai bien eu !".
C'est bien ça, l'histoire ? Du coup, tout ce petit protocole permet à G d'obtenir un truc $A$ à partir d'un truc $(A\to \to A$. Et en fait, si $q$ était bel et bien typé $A\to B$, alors il rentrerait dans $p$ et cracherait un truc $a$ que G pourrait avoir !
L'idée qu'il y a derrière cette histoire, c'est que douter d'un argument, c'est appeler un programme ?
EDIT : J'ai relu le fil. L'histoire des trains, je ne la comprends pas. J'ai l'impression de comprendre le post d'après avec les programmes. Ensuite, le coup des robots et des environnements, il faudra que je retrouve le fil où tu exposes précisément de quoi il en retourne. Mais j'ai l'impression qu'à un moment, tu dis (ou quelque chose d'équivalent) que le G, dans mon histoire, n'a pas le droit de tricher en donnant un faux $q$, et je me dis que je n'ai peut-être pas compris.
Il y a bien un bluff dans cette démarche, bluff qui permet de récupérer un argument, qui d'habitude est conçu comme enregistré sur un port d'entrée, inaccessible en écriture.
En programmation, ça s'écrit:
Bluf(a):=
begin
Declenche une exception et mets a sur le port 4
end
RPA(L) :=
begin
try L(Bluff) end;
exception déclenchée -> récupère x sur port 4
renvoyer x
end
La fonction Bluff a le type A=>B (tu peux prendre ce que tu veux pour
La fonction L donnée en argument a le type (A=>B)=>A
Il se peut qu'à l'exécution L n'appelle jamais son argument et ça ne déclenchera pas d'exception. Mais SI elle l'appelle, elle lui aura filé, par définition, un argument de type A que RPA va récupérer en breakant L, puis renvoyer comme résultat.
qu'est-ce que tu veux dire quand tu dis "ne pas mentir en vendant $f$ comme réalisant $A\to B$" ? D'après un autre fil, je sais (enfin, j'y crois par argument d'autorité, je n'ai pas vérifié ça moi-même) que si c'était vrai pour la logique combinatoire, alors ce serait démontrable en logique intuitionniste, ce qui est faux.
Dans les paradigmes où on peut tricher, c'est bon, mais dans les autres, non ?
Lorsque tu donnes à quelqu'un un billet (vrai ou faux) de train Paris-Marseille, en espérant que cette ruse va te permettre d'aller à Paris, tu as formellement 2 types de réactions possibles:
1/ "Zy Va, j'y crois pas, je pense que ton billet est un faux, je le déchire et le jette à la poubelle".
2/ "ah, merci, je m'empresse de l'utiliser, viens avec moi"
Dans le cas (1), ça ne t'avance pas pour aller à Paris.
Dans le cas (2), c'est en arrivant à Paris (et donc tu as gagné, tu peux même lui dire "c'était un faux, désolé") que ta victime (en cas d'arnaque) s'aperçoit (parce que le contrôleur l'empêche de passer pour monter dans le train) seulement de ton bluf, qui est alors démasqué.
Dans la CCH, "il se trouve" qu'on n'a pas de problème parce que les stratégies sont des "croyances religieuses abstraites" en quelque sorte qui servent de procès d'intention à des joueurs, qui sont eux, bien réels.
Ainsi, la $f:A\to B$ évoquée ne survient jamais autrement que lorsque Toto a joué un élément $x$ de $A$ et attend que John réponse dans la partie avec un élément de $B$ (le nom $f$ n'étant que le procès d'intention fait à John de d'appliquer la stratégie $f$, autrement dit, de systématiquement répondre $f(x)$ dans toute partie aussi bien réelle, qu'envisagée au conditionnelle).
Ne surtout pas confondre avec l'idée (hélas qui fait aussi des ravages en pédagogie) que $s$ serait donnée sous la forme d'une description que son utilisateur pourrait parser, découper, analyser, autopsier.
Les réalisateurs de $(A\to \to C$ garantissent répondre à N'IMPORTE QUELLE $f\in A\to B$ avec un élément de $C$. Pas seulement aux $f$ calculables, ou je ne sais quoi. Ce sont des maths, pas des "descriptions partielles". Il n'y a pas que les fonctions usuelles de l'année de première S qui vivent dans $\R ^\R$, pour le dire de manière plus provocatrice.
Il s'agit de réussir une réalisation EXTENSIONNELLE de l'ADN-substantifique moelle de l'axiome du choix, ledit étant parfaitement inoffensif si on ne lui demande pas de vérifier $f(a)=f(b)$ pour tout couple $(a,b)$ "de noms d'ensemble" tels que $a\subset b$ et $b\subset a$, en plus de $f(a)\in a$ pour chaque $a\neq \emptyset$.
Sauf erreur de ma part, il a cherché ça des années avant de trouver, dur labeur solitaire à son bureau de Jussieu, puis de Chevaleret, puis de Sophie Germain.
Sa première réalisation de ce qu'il a nommé ACNE (pour axiome du choix non extensionnel), exploitant l'horloge de la machine informatique où elle est implémentée a été, dixit lui, bien plus facile.
Je rappelle comment on réalise ACNE
Au lieu de garantir $\forall X,y: [y\in X \to \phi(X)\in X]$, on va garantir :
$$ \forall X\exists n\in \N: [y\in X\to \phi(X,n) \in X]$$
avec l'horloge. On AURA ALORS gagné avec
$$\forall X: [\sigma(X):=\phi(X,n(X))]$$
où $n:X\mapsto min(\{p\in \N: \phi(X,p)\in X\})$
La finitude de la prouvabilité (compacité) assure que dans les échanges prouveurs-sceptiques, ou les affrontements machines VS environnements, seuls un nombre fini de défis surviennent.
Lorsqu'est agressé $$[\forall n: \phi(X,n)\notin X]\to a\notin X$$
durant ce combat, il suffit de consulter l'horloge en récupérant l'entier $p$ affiché et d'ajouter l'hypothèse ad hoc:
$$ \phi(X,p) := a$$
qui permet de n'avoir plus qu'à défendre (moyennant ce cadeau) :
$$[a\notin X]\to [a\notin X]$$
et gagner.