An exercise on refuting Tseitin's formula using open sets in the plane.

1 files changed, 153 insertions, 0 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 388fec4..aa1b1b5 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -2557,6 +2557,7 @@ sémantique de la sémantique de Kripke) : c'est donc que cette formule
 n'est pas démontrable.
 \end{corrige}
 
+%
 
 \exercice\ (${\star}{\star}$)\par\nobreak
 
@@ -2655,6 +2656,7 @@ disjonction : si elle était prouvable, soit $\neg A$ soit $\neg\neg A$
 le serait, or elles ne sont même pas prouvables classiquement).
 \end{corrige}
 
+%
 
 \exercice\ (${\star}{\star}{\star}{\star}$)\par\nobreak
 
@@ -2773,6 +2775,7 @@ $(\neg A \Rightarrow B\lor C) \Rightarrow (\neg A\Rightarrow B) \lor
 (\neg A\Rightarrow C)$.)
 \end{corrige}
 
+%
 
 \exercice\ (${\star}{\star}{\star}$)\par\nobreak
 
@@ -2848,6 +2851,156 @@ A\Rightarrow B) \lor (\neg A\Rightarrow C)$ est valide dans la
 sémantique des problèmes finis de Medvedev.
 \end{corrige}
 
+%
+
+\exercice\ (${\star}$)\par\nobreak
+
+En considérant les parties suivantes de $\mathbb{R}^2$ :
+\[
+\begin{array}{c@{\hskip 3em}c}
+U_1 = \{(x,y)\in\mathbb{R}^2 : x < 0\}
+& U_2 = \{(x,y)\in\mathbb{R}^2 : x > 0\}
+\\
+V_1 = \{(x,y)\in\mathbb{R}^2 : y > -x^2\}
+& V_2 = \{(x,y)\in\mathbb{R}^2 : y < x^2\}
+\end{array}
+\]
+(faire un dessin !) montrer que la formule de Tseitin
+\[
+\begin{aligned}
+&(\neg (A_1 \land A_2) \land (\neg A_1 \Rightarrow (B_1 \lor B_2))
+  \land (\neg A_2 \Rightarrow (B_1 \lor B_2)))\\
+\Rightarrow\,& ((\neg A_1 \Rightarrow B_1)\lor(\neg A_2 \Rightarrow B_1)\lor(\neg
+  A_1 \Rightarrow B_2)\lor(\neg A_2 \Rightarrow B_2))
+\end{aligned}
+\]
+n'est pas démontrable en calcul propositionnel intuitionniste.
+
+\begin{corrige}
+On va interpréter la formule de Tseitin dans la sémantique des ouverts
+de $\mathbb{R}^2$ en prenant $U_1,U_2,V_1,V_2$ pour $A_1,A_2,B_1,B_2$
+respectivement, c'est-à-dire qu'on va calculer :
+\[
+\begin{aligned}
+&(\dottedneg (U_1 \dottedland U_2) \dottedland (\dottedneg U_1 \dottedlimp (V_1 \dottedlor V_2))
+  \dottedland (\dottedneg U_2 \dottedlimp (V_1 \dottedlor V_2)))\\
+\dottedlimp\,& ((\dottedneg U_1 \dottedlimp V_1)\dottedlor(\dottedneg U_2 \dottedlimp V_1)\dottedlor(\dottedneg
+  U_1 \dottedlimp V_2)\dottedlor(\dottedneg U_2 \dottedlimp V_2))
+\end{aligned}
+\]
+On a représenté ci-dessous en grisé les parties \emph{ouvertes}
+décrites par différentes sous-expressions de cette formule :
+\begin{center}
+\lineskip=1explus5ex
+\begin{tabular}{c}
+\begin{tikzpicture}
+\fill[gray] (-1.5,-1.5) -- (0,-1.5) -- (0,1.5) -- (-1.5,1.5) -- cycle;
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $U_1 \;=\; \dottedneg U_2$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\fill[gray] (1.5,-1.5) -- (0,-1.5) -- (0,1.5) -- (1.5,1.5) -- cycle;
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $U_2 \;=\; \dottedneg U_1$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (-1.5,-2.25) .. controls (-1,-0.75) and (-0.5,0) .. (0,0) .. controls (0.5,0) and (1,-0.75) .. (1.5,-2.25) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $V_1$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (-1.5,2.25) .. controls (-1,0.75) and (-0.5,0) .. (0,0) .. controls (0.5,0) and (1,0.75) .. (1.5,2.25) -- (1.5,-1.5) -- (-1.5,-1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $V_2$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (-1.5,-1.5) -- (0,-1.5) -- (0,0) .. controls (0.5,0) and (1,-0.75) .. (1.5,-2.25) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $\dottedneg U_1 \dottedlimp V_1$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (-1.5,-2.25) .. controls (-1,-0.75) and (-0.5,0) .. (0,0) -- (0,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $\dottedneg U_2 \dottedlimp V_1$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (-1.5,1.5) -- (0.1,5) -- (0,0) .. controls (0.5,0) and (1,0.75) .. (1.5,2.25) -- (1.5,-1.5) -- (-1.5,-1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $\dottedneg U_1 \dottedlimp V_2$
+\end{tabular}
+\penalty0
+\begin{tabular}{c}
+\begin{tikzpicture}
+\begin{scope}
+\clip (-1.5,-1.5) -- (1.5,-1.5) -- (1.5,1.5) -- (-1.5,1.5) -- cycle;
+\fill[gray] (-1.5,2.25) .. controls (-1,0.75) and (-0.5,0) .. (0,0) -- (0,1.5) -- (1.5,1.5) -- (1.5,-1.5) -- (-1.5,-1.5) -- cycle;
+\end{scope}
+\draw[->] (-1.55,0)--(1.55,0) node[right]{$x$};
+\draw[->] (0,-1.55)--(0,1.55) node[above]{$y$};
+\end{tikzpicture}
+\\ $\dottedneg U_2 \dottedlimp V_2$
+\end{tabular}
+\end{center}
+Le membre de droite $((\dottedneg U_1 \dottedlimp
+V_1)\dottedlor(\dottedneg U_2 \dottedlimp V_1)\dottedlor(\dottedneg
+U_1 \dottedlimp V_2)\dottedlor(\dottedneg U_2 \dottedlimp V_2))$ du
+$\dottedlimp$ externe de la formule est la réunion des quatre
+dernières parties dessinées ci-dessus, c'est-à-dire le complémentaire
+de l'origine (noter qu'on n'attrape jamais l'origine puisqu'elle est
+au bord de chacune des parties dessinées, donc jamais dedans).  En
+revanche, chacun des facteurs, $\dottedneg (U_1 \dottedland U_2)$,
+$\dottedneg U_1 \dottedlimp (V_1 \dottedlor V_2)$ et $\dottedneg U_2
+\dottedlimp (V_1 \dottedlor V_2)$ du membre de gauche est
+$\mathbb{R}^2$ tout entier, puisque $U_1 \dottedland U_2$ est vide, et
+que $V_1 \dottedlor V_2$ est le complémentaire de l'origine donc
+contient $\dottedneg U_1$ comme $\dottedneg U_2$.  Finalement, pour
+l'expression tout entière, on trouve le complémentaire de l'origine,
+qui n'est pas $\mathbb{R}^2$, donc la formule de Tseitin n'est pas
+validée par ce choix d'ouverts, et (par \emph{correction} de la
+sémantique des ouverts) elle ne peut pas être démontrable.
+\end{corrige}
+
 
 %
 %