An exercise about proving the Medvedev-validity of the Kreisel-Putnam formula.

1 files changed, 75 insertions, 0 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index f492d9d..f483a19 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -2647,6 +2647,81 @@ $(\neg A \Rightarrow B\lor C) \Rightarrow (\neg A\Rightarrow B) \lor
 \end{corrige}
 
 
+\exercice\ (${\star}{\star}{\star}$)\par\nobreak
+
+\textbf{(1)} Donné un problème fini $(X,S)$, décrire soigneusement le
+problème $\dottedneg(X,S)$ (combien de candidats il a, et combien de
+solutions : on distinguera $S = \varnothing$ ou $S \neq\varnothing$).
+
+\textbf{(2)} Expliquer pourquoi la formule suivante (« axiome de
+Kreisel-Putnam ») est valable dans la sémantique de Medvedev des
+problèmes finis :
+\[
+(\neg A \Rightarrow B\lor C) \Rightarrow
+(\neg A\Rightarrow B) \lor (\neg A\Rightarrow C)
+\]
+(On décrira explicitement le problème fini décrit par la partie gauche
+et par la partie droite de l'implication centrale de cette formule, et
+leurs solutions.)
+
+\begin{corrige}
+\textbf{(1)} Soit $(X,S)$ un problème fini.  On rappelle que
+$\dottedbot = (\{\bullet\},\varnothing)$.  Le problème
+$\dottedneg(X,S)$, c'est-à-dire $(X,S) \dottedlimp
+(\{\bullet\},\varnothing)$ a une seul candidat, à savoir l'unique
+fonction $X \to \{\bullet\}$, qu'on notera abusivement aussi
+$\bullet$ ; les solutions de $\dottedneg(X,S)$ sont les fonctions $X
+\to \{\bullet\}$ qui envoient chaque élément de $S$ dans
+$\varnothing$ : or si $S = \varnothing$ c'est le cas de l'unique
+fonction $\bullet$, tandis que si $S \neq \varnothing$, elle n'envoie
+pas $S$ dans $\varnothing$.  Pour résumer, $\dottedneg(X,S)$ a
+toujours exactement un candidat $\bullet$, et ce candidat est solution
+exactement lorsque le problème $(X,S)$ de départ a n'a pas de
+solution.
+
+\textbf{(2)} Considérons d'abord $\dottedneg A \dottedlimp B\dottedlor
+C$ en remplaçant $A,B,C$ par trois problèmes finis $(X,S)$, $(Y,T)$ et
+$(Z,U)$ respectivement.  On a vu que $\dottedneg A$ a toujours
+exactement un candidat $\bullet$, et qu'il est solution précisément
+lorsque $S = \varnothing$, et sinon aucune.  Les candidats de
+$\dottedneg A \dottedlimp B\dottedlor C$ sont donc des fonctions de
+$\{\bullet\}$ vers l'ensemble des candidats $Y \uplus Z$ de
+$B\dottedlor C$, qu'on peut donc identifier à $Y \uplus Z$ (en
+identifiant une fonction $\{\bullet\} \to V$, pour $V$ un ensemble
+quelconque, avec l'image de $\bullet$ par cette fonction).  Parmi ces
+candidats, si $S \neq\varnothing$, ils sont tous solutions (car
+$\dottedneg A$ n'a pas de solution donc il n'y a pas de contrainte),
+tandis que si $S = \varnothing$, ceux qui sont solution sont ceux
+solution de $B$ et de $C$, i.e., c'est $T\uplus U$.
+
+Or la même description vaut pour $(\dottedneg A\dottedlimp B)
+\dottedlor (\dottedneg A\dottedlimp C)$ : le problème $(\dottedneg
+A\dottedlimp B)$ a un ensemble de candidats qui s'identifie à celui
+$Y$ de $B$, et si $S \neq\varnothing$ ils sont tous solutions tandis
+que si $S = \varnothing$ ceux qui sont solutions sont les solutions
+de $B$, c'est-à-dire $T$ ; et le problème $(\dottedneg A\dottedlimp
+C)$ a un ensemble de candidats qui s'identifie à celui $Z$ de $C$, et
+si $S \neq\varnothing$ ils sont tous solutions tandis que si $S =
+\varnothing$ ceux qui sont solutions sont les solutions de $C$,
+c'est-à-dire $V$.  Bref, $(\dottedneg A\dottedlimp B) \dottedlor
+(\dottedneg A\dottedlimp C)$ a pour ensemble de candidats $Y \uplus Z$
+et pour ensemble de solutions $Y\uplus Z$ lorsque $S \neq\varnothing$
+et $T\uplus U$ lorsque $S = \varnothing$.  C'est exactement pareil que
+$\dottedneg A \dottedlimp B\dottedlor C$.
+
+On a donc un candidat évident dans $(\dottedneg A \dottedlimp
+B\dottedlor C) \dottedlimp (\dottedneg A\dottedlimp B) \dottedlor
+(\dottedneg A\dottedlimp C)$, c'est l'identité (une fois faites nos
+identifications des candidats de $\dottedneg A \dottedlimp B\dottedlor
+C$ comme $(\dottedneg A\dottedlimp B) \dottedlor (\dottedneg
+A\dottedlimp C)$ avec $Y\uplus Z$), et par la description faite des
+solutions, ce candidat est toujours solution.  C'est précisément ce
+qui montre que $(\neg A \Rightarrow B\lor C) \Rightarrow (\neg
+A\Rightarrow B) \lor (\neg A\Rightarrow C)$ est valide dans la
+sémantique des problèmes finis de Medvedev.
+\end{corrige}
+
+
 %
 %
 %