diff options
| -rw-r--r-- | exercices-inf110.tex | 153 |
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} + % % |