An exercise about proving the irrealizability of the Kreisel-Putnam formula.

1 files changed, 119 insertions, 1 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index e6c7867..f492d9d 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -1039,7 +1039,7 @@ récursive.)
 
 %
 
-\exercice\ (${\star}{\star}$)\par\nobreak
+\exercice\label{exercise-computably-inseparable-sets}\ (${\star}{\star}$)\par\nobreak
 
 On dira que deux parties $L,M$ de $\mathbb{N}$ disjointes
 (c'est-à-dire $L\cap M = \varnothing$) sont \textbf{calculablement
@@ -2529,6 +2529,124 @@ le serait, or elles ne sont même pas prouvables classiquement).
 \end{corrige}
 
 
+\exercice\ (${\star}{\star}{\star}{\star}$)\par\nobreak
+
+En prenant connaissance du résultat de
+l'exercice \ref{exercise-computably-inseparable-sets}, montrer que la
+formule suivante (« axiome de Kreisel-Putnam ») n'est pas réalisable :
+\[
+(\neg A \Rightarrow B\lor C) \Rightarrow
+(\neg A\Rightarrow B) \lor (\neg A\Rightarrow C)
+\]
+(On pourra supposer par l'absurde qu'il y a un programme $r$ qui
+réalise cette formule, et chercher à s'en servir pour séparer les
+ensembles $L$ et $M$ définis dans
+l'exercice \ref{exercise-computably-inseparable-sets}.
+\emph{Indication :} plus précisément, on pourra poser $B_z$ comme
+valant $\mathbb{N}$ si $z\in L$ et $\varnothing$ sinon ; $C_z$ comme
+valant $\mathbb{N}$ si $z\in M$ et $\varnothing$ sinon ; et $A_z$
+comme valant $\varnothing$ si $z\in L\cup M$ et $\mathbb{N}$ sinon ;
+et chercher à définir un élément de $(\dottedneg A_z \dottedlimp
+B_z\dottedlor C_z)$ auquel appliquer $r$.)
+
+\begin{corrige}
+Supposons par l'absurde qu'il existe (un \emph{même}) $r$ qui réalise
+$(\neg A \Rightarrow B\lor C) \Rightarrow (\neg A\Rightarrow B) \lor
+(\neg A\Rightarrow C)$, c'est-à-dire qui appartienne à $(\dottedneg A
+\dottedlimp B\dottedlor C) \dottedlimp (\dottedneg A\dottedlimp B)
+\dottedlor (\dottedneg A\dottedlimp C)$ quels que soient
+$A,B,C\subseteq \mathbb{N}$ (où $P \dottedlor Q = \{\langle 0,m\rangle
+: m\in P\} \cup \{\langle 1,n\rangle : n\in Q\}$ et $(P \dottedlimp Q)
+= \{e \in \mathbb{N} : \varphi_e(P){\downarrow} \subseteq Q\}$, et on
+se rappelle bien sûr que $\dottedneg P = (P\dottedlimp \varnothing)$
+vaut $\mathbb{N}$ si $P$ est vide et $\varnothing$ si $P$ n'est pas
+vide).
+
+On pose $L := \{\langle e,x\rangle : \varphi_e(x){\downarrow} = 1\}$
+et $M := \{\langle e,x\rangle : \varphi_e(x){\downarrow} = 2\}$.  On a
+vu dans l'exercice \ref{exercise-computably-inseparable-sets} qu'il
+n'existe aucun programme $s$ qui, prenant en entrée un
+$z\in\mathbb{N}$, termine toujours en temps fini, et renvoie « vrai »
+lorsque $z \in L$ et « faux » lorsque $z \in M$ (et une réponse
+quelconque, lorsque $z \not\in L\cup M$, mais le programme doit quand
+même terminer).  Or on va utiliser $r$ pour faire précisément une
+telle chose, ce qui constituera une contradiction.
+
+Définissons les ensembles $A_z,B_z,C_z$ pour $z = \langle e,x\rangle$
+comme suit :
+\[
+\begin{aligned}
+A_z &= \varnothing \text{~si~$\varphi_e(x){\downarrow} = 1$ ou
+  $\varphi_e(x){\downarrow} = 2$,}\\
+&= \mathbb{N} \text{~sinon}\\
+\text{(donc~}\dottedneg A_z &= \mathbb{N} \text{~si~$\varphi_e(x){\downarrow} = 1$ ou
+  $\varphi_e(x){\downarrow} = 2$,}\\
+&= \varnothing \text{~sinon)}\\
+B_z &= \mathbb{N} \text{~si~$\varphi_e(x){\downarrow} = 1$,}\\
+&= \varnothing \text{~sinon}\\
+C_z &= \mathbb{N} \text{~si~$\varphi_e(x){\downarrow} = 2$,}\\
+&= \varnothing \text{~sinon}\\
+\end{aligned}
+\]
+
+Donné $z\in \mathbb{N}$, considérons le programme $p_z$ défini comme
+suit.  Il prend un unique argument, qu'il ignore.  Il décode le couple
+$z = \langle e,x\rangle$, puis il exécute $\varphi_e(x)$ (au moyen
+d'un interpréteur universel).  Si $\varphi_e(x){\downarrow} = 1$, il
+renvoie $\langle 0,0\rangle$, et si $\varphi_e(x){\downarrow} = 2$, il
+renvoie $\langle 1,0\rangle$ ; dans tout autre cas, il fait une boucle
+infinie (y compris bien sûr si $\varphi_e(x){\uparrow}$, c'est-à-dire
+si l'exécution ne termine jamais : dans ce cas forcément $p_z$ ne
+termine pas non plus).
+
+On remarque que $p_z$ est construit algorithmiquement en fonction
+de $z$ (par le théorème s-m-n si on veut).
+
+Par construction, si on passe à $p_z$ un argument de $\dottedneg A_z$,
+ce qui implique que $\varphi_e(x){\downarrow} = 1$ ou
+$\varphi_e(x){\downarrow} = 2$ (l'argument est une \emph{promesse} de
+ce fait), alors il renvoie un élément de $B_z \dottedlor C_z$ (à
+savoir un couple $\langle 0,n\rangle$ avec $n\in B_z$ ou $\langle
+1,n\rangle$ avec $n\in C_z$).  On a donc $p_z \in (\dottedneg A_z
+\dottedlimp B_z\dottedlor C_z)$.
+
+Par hypothèse sur $r$, on doit donc avoir $\varphi_r(p_z)$ défini et
+appartenant à $(\dottedneg A_z\dottedlimp B_z) \dottedlor (\dottedneg
+A_z\dottedlimp C_z)$.  Notamment, $\varphi_r(p_z)$ est (le codage
+d')un couple dont la première coordonnée vaut $0$ ou $1$ et indique si
+la seconde est dans $\dottedneg A_z\dottedlimp B_z$ ou dans
+$\dottedneg A_z\dottedlimp C_z$.  On considère le programme $s$ qui
+prend un $z$ en entrée, calcule $\varphi_r(p_z)$ (noter que ce calcul
+est bien algorithmique puisque $p_z$ est construit algorithmiquement
+en fonction de $z$, et il termine toujours d'après ce qu'on vient de
+dire), et renvoie « vrai » si la première coordonnée du résultat
+vaut $0$ et « faux » si la seconde coordonnée du résultat vaut $1$.
+
+Si $z = \langle e,x\rangle$ avec $\varphi_e(x){\downarrow} = 1$, alors
+$C_z = \varnothing$ et $\dottedneg A_z = \mathbb{N}$, donc
+$(\dottedneg A_z\dottedlimp C_z) = \varnothing$, donc $\varphi_r(p_z)$
+doit forcément être de la forme $\langle 0,\cdots\rangle$, et $s$
+renvoie « vrai » sur l'entrée $z$.  Symétriquement, si $z = \langle
+e,x\rangle$ avec $\varphi_e(x){\downarrow} = 2$, alors $(\dottedneg
+A_z\dottedlimp B_z) = \varnothing$ donc $\varphi_r(p_z)$ doit
+forcément être de la forme $\langle 1,\cdots\rangle$, et $s$ renvoie
+« faux » sur l'entrée $z$.
+
+Donc $s$ termine toujours, et sépare $L$ et $M$ puisqu'il renvoie
+« vrai » sur le premier et « faux » sur le second.  Ceci contredit le
+fait que $L$ et $M$ sont récursivement inséparables.  On a abouti à
+une contradiction : c'est qu'en fait $r$ n'existait pas.
+
+(La formule de Kreisel-Putnam n'est donc pas réalisable.  En
+particulier, par \emph{correction} de la sémantique de la
+réalisabilité, elle n'est pas démontrable dans le calcul
+propositionnel intuitionniste, c'est-à-dire, par Curry-Howard, qu'il
+n'y a pas de terme du $\lambda$-calcul simplement typé ayant pour type
+$(\neg A \Rightarrow B\lor C) \Rightarrow (\neg A\Rightarrow B) \lor
+(\neg A\Rightarrow C)$.)
+\end{corrige}
+
+
 %
 %
 %