Réalisabilité de l'axiome de Peirce

Georges Abitbol · December 2019

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 c · December 2019

De mon téléphone: avec des billets de train (en ces temps de grève :-D )

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

christophe c · December 2019

En programmation cela consiste à donner une fonction au programme qui garantit (A-->B)-->A en la lui présentant comme typée A-->B. S'il ne l'appelle jamais tout va bien. S'il l'appelle c'est forcément qu'il lui donne un argument w de type A et la fonction, au lieu de calculer f(w) , stoppé violemment le programme et envoie w à l'appeleur de ce programme, qui voulait un objet de type A donc qui est content.

C'est l'implémentation des try.. finally

christophe c · December 2019

Je donne une preuve que c'est vrai (que cette action réalise le RPA).

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.

christophe c · December 2019

Remarque: dans la vraie vie, ce n'est pas ce qu'il se passe quand les gens appliquent la science. Ils ne remontent pas le temps après avoir perdu un match de tennis, pour le rejouer, et ainsi de suite, jusqu'à gagner la partie.

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$.

christophe c · December 2019

C'est pour ça que ce paradigme universel marche bien en informatique où l'environnement est espéré et supposé (et rarement contredit depuis que les ordinateurs existent) être la simple configuration informatique abstraite du moment, qui peut se scanner par définition autant qu'on veut. En réalité, il s'agit juste de pointeurs que tu déplaces, mais il faut de la mémoire physique.

Foys · December 2019

Il y a des documents sur le site de J.-L. Krivine.

Georges Abitbol · January 2020

Désolé, je n'ai pas trop regardé pendant les fêtes. Je partais mal, je croyais que l'axiome de Pierce c'était $(\forall B,\quad (A\Rightarrow

\Rightarrow

) \Rightarrow A$ donc merci d'avoir rappelé son bon énoncé :-D
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.

christophe c · January 2020

C'edt une hypothèse il n'a le droit de te refuser ton billet que s'il prouve que c'est un fake. Pour ça, il doit mettre le billet dans le composteur et attendre que l'alerte sonne.

christophe c · January 2020

De la même façon qu'un programme n'a un problème avec un pointeur que quand il l'appelle (ie demande sa valeur)

Georges Abitbol · April 2020

Ok j'étais dans le bain et je pensais à tout ça et je crois avoir compris. Je précise que je n'ai pas encore relu le fil, je fais une tentative "avec mes propres mots" et je verrai après si ça colle.

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.

christophe c · April 2020

Si si tu sembles avoir compris. Le raisonnement par l'absurde (enfin Peirce) est bien réalisé par le paradigme "WANTED". La banque annonce qu'elle offre des chèques, en quantité illimitée, de la somme A=>B, ce qui lui permet d'attraper les gens qui se présentent au guichet avec la somme A (car ils espèrent les changer contre

.

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.

Georges Abitbol · April 2020

Ok mais quand tu dis

christophe a écrit:

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.

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 ?

christophe c · April 2020

Oui, c'est ça EN GROS.

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.

Foys · April 2020

https://www.irif.fr/~krivine/articles/Well_order.pdf

christophe c · April 2020

Pour avoir beaucoup parlé avec Jean-Louis de ça, je précise que le document que foys a mis en lien est "un gros document" à avaler.

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.

christophe c · April 2020

Et comme de toute façon l'horloge n'affiche jamais le même nombre par définition même de sa vocation informatique (je parle de l'horloge interne, qu'on appelle en assembleur avec .... oups j'ai oublié, je préciserai ultérieurement), la garantie est sûre et en fait rend ACNE inoffensif (axiome qui a à peu près la même puissance qu'une définition).

Réalisabilité de l'axiome de Peirce

Réponses

Bonjour!

Catégories

In this Discussion

Qui est en ligne 34