temps "=" axiome du choix

Une "autorisation" bien connue en mathématique, qui appartient au groupe dont le nom officiel est {\it inférence} est celle qui consiste à faire l'enchainement suivant dans une preuve:

...A
...$A\to B$

{\bf donc B}

Cette inférence s'appelle un {\it modus ponens}

La construction correspondante, en terme de programmes ou en termes "d'idées opératoires" est la suivante:

Vous disposez par hypothèse d'une garantie $v$ de $A$, et d'une garantie $u$ de $A\to B$. But: fabriquer une garantie de $B$

Le "robot" $r$ qui va garantir $B$ se comportera de la manière suivante: il passera la main au robot $u$, mais il aura pris soin avant de placer $v$ en "bouclier".

En effet, ce faisant, soit $E$ un {\it environnement} hostile à $B$. Voyons si, dans cet environnement le robot $r$ s'en tire: il place en "bouclier" le robot $v$ (qui je le rappelle garantit $A$) puis passe la main à $u$.

Au moment où le robot $u$ est sollicité, il se trouve face à un environnement $F$ qui "agresse" $A\to B$. {\bf Et notre hypothèse} était que $u$ s'en tire face à n'importe quel environnement qui agresse $A\to B$...

La seule chose que j'ai vraiment supposé ici, et ce sera une définition: après avoir placé $v$ comme "bouclier" le robot $v$ a {\bf transformé} légèrement l'environnement dans lequel il se trouvait. Et précisément, il l'a fait passé de $E$ à $F$.

$E$ agressait $B$ alors que $F$ n'agresse plus que $A\to B$.

Un cosmonaute à poil dans le vide n'est pas du tout comme un cosmonaute à poil dans sa combinaison dans le vide. Ici c'était $v$ la combinaison et $u$ le cosmonaute.

Sans rien justifier pour l'instant, voici des définitions-hypothèses:

1) Un environnement qui agresse $A\to B$ fournit une "promesse" de $A$ et nous supposerons qu'en fait, il fournit {\bf une garantie de $A$} (ce qui illustre une certaine imbrication entre les robots et les environnements.

2) Un robot $r$ qui garantit $\forall w\in Clavier\ numerique$ blabla, a forcément une façon "robotique" (et même uniforme) de réagir à l'appui sur n'importe quelle touche $w$. Nous noterons le robot induit $r(w)$ (comportement du robot $r$ {\bf après} qu'on lui a envoyé le signal qu'on a tapé sur la touche $w$)




Voilà l'argument Krivinien:

je construis un robot $r$ "réaliste" et je vous raconte pourquoi il n'échoue dans aucun environnement qui agresse H.

Un environnement $E$ qui agresse H va, avant toute chose, d'abord taper sur une certaine touche $x_0$ puis sur une touche $y_0$, puis ensuite, il va agresser:

$(\forall p\in \N f(x_0,p)\notin x_0)\to y_0\notin x_0$.

Il va donc fournir une promesse (et j'ai dit juste au début de ce post que cette promesse est une garantie de..), donc une garantie $u$ de:

$\forall p\in \N f(x_0,p)\notin x_0$

Et ensuite, il agresse $y_0\notin x_0$. (Au moment où il démarre cette agression, il est devenu l'environnement disons $G$). Un agresseur de $y_0\in x_0\to tout$ fournit forcément une garantie (sous forme d'un robot $v$) de $y_0\in x_0$ avant, ensuite d'agresser "tout".

Le robot $r$ va {\bf se servir de l'horloge} pour fournir l'heure à $u$ (sous forme d'un entier dont il n'a jamais encore été question dans l'histoire de leur chamailleries (robots contre environnements). Autrement dit, il va passer la main à "$u(time)$" puis placer en bouclier le robot $v$. $time$ ne sera ici rien d'autre qu'un entier dont il n'a encore jamais été question (un tout nouvel entier).

Par hypothèse, $u(time)$ sort vainqueur dans toute agression de $f(x_0,time)\in x_0\to tout$.

Cela implique en particulier que $y_0\neq f(x_0,time)$, {\bf or, on voit mal comment, dans une "bagarre" entre un robot et un environnement, comment sans jamais préciser ce que veut dire $f$, bref, on voit mal comment le robot $u(time)$ pourrait garantir que $f(x_0;time)\notin x_0$, sans en fait avoir une méthode uniforme de comportement, qui finalement garantit AUSSI $y_0\notin x_0$}.

Mais si cette partie non justifiée de mon argumentation est vrai, c'est à dire si, selon toute vraisemblance, $u(time)$ garantit $y_0\in x_0\to tout$, alors, comme $v$ garantit $y_0\in x_0$... Je vous laisse terminer!