diff options
| -rw-r--r-- | exercices-inf110.tex | 80 |
1 files changed, 79 insertions, 1 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex index 10a5e8b..d3c885c 100644 --- a/exercices-inf110.tex +++ b/exercices-inf110.tex @@ -20,6 +20,7 @@ \usepackage{graphics} \usepackage[usenames,dvipsnames]{xcolor} \usepackage{tikz} +\usetikzlibrary{arrows} % \theoremstyle{definition} \newtheorem{comcnt}{Tout}[section] @@ -2079,7 +2080,7 @@ $(u \mapsto 0, v\mapsto 1, w\mapsto 1)$. Or si $(\neg\neg A \Rightarrow A) \Rightarrow (A \lor \neg A)$ était démontrable en calcul propositionnel intuitionniste, on trouverait constamment $1$ quelle que soit l'affectation $p$ utilisé pour $A$ (par -\emph{correction} de la sémantique des ouverts). Comme ce n'est pas +\emph{correction} de la sémantique de Kripke). Comme ce n'est pas le cas, c'est que la proposition en question n'est pas démontrable. Une autre preuve est fournie par la sémantique de la réalisabilité @@ -2217,4 +2218,81 @@ $\neg\neg(P \lor \neg P)$ (sans hypothèse). Si on postule $\neg\neg Q % % % + +\section{Sémantique(s) du calcul propositionnel intuitionniste} + + +\exercice\ (${\star}$)\par\nobreak + +On considère le cadre de Kripke dessiné ci-dessous, où une flèche $w +\to w'$ signifie que $w \leq w'$ (« le monde $w'$ est accessible +depuis le monde $w$ »), sachant que la relation $\leq$ doit bien sûr +être réflexive et transitive (c'est la clôture réflexive-transitive de +celle qui est représentée par les flèches : c'est-à-dire qu'on a bien +sûr $u_0\leq u_0$ et $u_2\leq u_0$ par exemple, malgré l'absence de +flèches explicites pour le rappeler). +\begin{center} +\begin{tikzpicture}[>=stealth'] +\node (u0) at (0bp,0bp) {$u_0$}; +\node (v0) at (35bp,-15bp) {$v_0$}; +\node (u1) at (0bp,-30bp) {$u_1$}; +\node (v1) at (35bp,-45bp) {$v_1$}; +\node (u2) at (0bp,-60bp) {$u_2$}; +\draw[->] (u1)--(u0); +\draw[->] (u2)--(u1); +\draw[->] (v1)--(v0); +\draw[->] (u2)--(v0); +\draw[->] (v1)--(u0); +\end{tikzpicture} +\end{center} +Soit $p$ l'affectation de vérité qui vaut $1$ en $u_0$ et $0$ en +chacun de $v_0,u_1,v_1,u_2$. Pour ce $p$, calculer l'affectation de +vérité de $((\neg\neg p \Rightarrow p)\Rightarrow(p\lor\neg p)) +\Rightarrow(\neg p\lor\neg\neg p)$. En déduire que la formule +$((\neg\neg A \Rightarrow A)\Rightarrow(A\lor\neg A)) \Rightarrow(\neg +A\lor\neg\neg A)$ n'est pas démontrable en calcul propositionnel +intuitionniste. + +\begin{corrige} +On calcule successivement l'affectation de vérité de chacune des +sous-formules de la formule proposée : on se rappelle que +$q\Rightarrow r$ vaut $1$ en un monde $w$ lorsque dans tout monde $w'$ +accessible depuis $w$ pour lequel $q(w') = 1$ on a aussi $r(w') = 1$, +et notamment, $\neg q$ vaut $q$ en un monde $w$ lorsque dans tout +monde $w'$ accessible depuis $w$ on a $q(w') = 0$. Par ailleurs, pour +éviter de se trompre, on vérifie à tout stade que les affectations de +vérité sont permanentes, c'est-à-dire que si $q(w) = 1$ on a $q(w') = +1$ pour tout monde $w'$ accessible depuis $w$. On obtient les +résultats tabulés ci-dessous : + +\begin{center} +\begin{tabular}{r|ccccc} +Formule&$u_2$&$v_1$&$u_1$&$v_0$&$u_0$\\\hline +$p$&$0$&$0$&$0$&$0$&$1$\\ +$\neg p$&$0$&$0$&$0$&$1$&$0$\\ +$p\lor \neg p$&$0$&$0$&$0$&$1$&$1$\\ +$\neg\neg p$&$0$&$0$&$1$&$0$&$1$\\ +$\neg p\lor \neg\neg p$&$0$&$0$&$1$&$1$&$1$\\ +$\neg\neg p \Rightarrow p$&$0$&$1$&$0$&$1$&$1$\\ +$(\neg\neg p \Rightarrow p)\Rightarrow (p\lor \neg p)$&$1$&$0$&$1$&$1$&$1$\\ +$((\neg\neg p \Rightarrow p)\Rightarrow (p\lor \neg p)) +\Rightarrow(\neg p\lor\neg\neg p)$&$0$&$1$&$1$&$1$&$1$\\ +\end{tabular} +\end{center} + +On constate que l'affecatation de vérité de $((\neg\neg p \Rightarrow +p)\Rightarrow (p\lor \neg p)) \Rightarrow(\neg p\lor\neg\neg p)$ n'est +pas identiquement $1$ sur le cadre. Or si $((\neg\neg A \Rightarrow +A)\Rightarrow(A\lor\neg A)) \Rightarrow(\neg A\lor\neg\neg A)$ était +démontrable en calcul propositionnel intuitionniste, on trouverait +constamment $1$ dans tout cadre et en remplaçant $p$ par n'importe +quelle affectation de vérité sur le cadre (par \emph{correction} de la +sémantique de la sémantique de Kripke) : c'est donc que cette formule +n'est pas démontrable. +\end{corrige} + + +% +% +% \end{document} |