diff options
| -rw-r--r-- | exercices-inf110.tex | 110 |
1 files changed, 106 insertions, 4 deletions
diff --git a/exercices-inf110.tex b/exercices-inf110.tex index 44f9c50..e6c7867 100644 --- a/exercices-inf110.tex +++ b/exercices-inf110.tex @@ -2383,10 +2383,14 @@ flèches explicites pour le rappeler). 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. +\Rightarrow(\neg p\lor\neg\neg p)$ (c'est-à-dire plus exactement +$((\dottedneg\dottedneg p \dottedlimp +p)\dottedlimp(p\dottedlor\dottedneg p)) \dottedlimp(\dottedneg +p\dottedlor\dottedneg\dottedneg p)$, où les points rappellent qu'on +parle de l'interprétation des connecteurs données par la sémantique de +Kripke). 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 @@ -2427,6 +2431,104 @@ n'est pas démontrable. \end{corrige} +\exercice\ (${\star}{\star}$)\par\nobreak + +Pour $n\in\mathbb{N}$, on considère le cadre de Kripke +$\{w_0,\ldots,w_{n-1}\}$ formé de $n$ mondes totalement ordonnés par +$w_i \leq w_j$ lorsque $i\geq j$ (le fait d'inverser l'ordre s'avérera +plus commode pour l'écriture de la suite) : +\begin{center} +\begin{tikzpicture}[>=stealth'] +\node (wmax) at (-180bp,0bp) {$w_{n-1}$}; +\node (dots) at (-140bp,0bp) {$\cdots$}; +\node (w2) at (-100bp,0bp) {$w_2$}; +\node (w1) at (-50bp,0bp) {$w_1$}; +\node (w0) at (0bp,0bp) {$w_0$}; +\draw (wmax)--(dots); +\draw[->] (dots)--(w2); +\draw[->] (w2)--(w1); +\draw[->] (w1)--(w0); +\end{tikzpicture} +\end{center} + +On définit aussi $n+1$ affectations de vérité $p_0,\ldots,p_n$ par +$p_k(w_i) = 1$ lorsque $i<k$ et $p_k(w_i) = 0$ lorsque $i\geq k$ +(notamment, $p_0$ est l'affectation $\dottedbot$ et $p_n$ est +l'affectation $\dottedtop$). Pourquoi sont-ce les seules affectations +de vérité sur ce cadre ? Calculer les tableaux de $\dottedland, +\dottedlor, \dottedlimp, \dottedneg$ sur $p_0,\ldots,p_n$. + +Donner un exemple de formule propositionnelle classiquement +démontrable et qui n'est pas validée par ce cadre (si $n\geq 2$), et +un exemple de formule propositionnelle validée par ce cadre et qui pas +démontrable intuitionnistement. + +\begin{corrige} +La contrainte sur une affectation de vérité sur un cadre de Kripke $W$ +est d'être permanente, i.e., si $p(w)=1$ alors $p(w')=1$ pour tout +monde $w'$ accessible depuis $w$ (c'est-à-dire $w\leq w'$), autrement +dit d'etre une fonction croissante $W \to \{0,1\}$. Comme ici $W$ est +simplement $\{0,\ldots,n-1\}$ avec l'ordre inversé, les seules +fonctions décroissantes $\{0,\ldots,n-1\} \to \{0,1\}$ étant celles +qui valent $1$ jusqu'à un certain point et $0$ ensuite, on obtient les +$p_k$ qu'on a décrits. + +Le calcul de $\dottedland$ et $\dottedlor$ est facile puisqu'il se +fait monde par monde : on a $(p_k \dottedland p_\ell)(w_i) = 1$ +lorsque $p_k(w_i) = 1$ et $p_\ell(w_i) = 1$, c'est-à-dire $i<k$ et +$i<\ell$, ce qui équivaut à $i<\min(k,\ell)$, ce qui montre $p_k +\dottedland p_\ell = p_{\min(k,\ell)}$ ; de même, on a $(p_k +\dottedlor p_\ell)(w_i) = 1$ lorsque $p_k(w_i) = 1$ ou $p_\ell(w_i) = +1$, c'est-à-dire $i<k$ ou $i<\ell$, ce qui équivaut à +$i<\max(k,\ell)$, ce qui montre $p_k \dottedlor p_\ell = +p_{\max(k,\ell)}$. + +Reste à traiter le cas de $\dottedlimp$. Si $k\leq\ell$, alors +$p_k(w_j) = 1$ implique $p_\ell(w_j) = 1$ (car $j<k$ implique +$j<\ell$), et ce, pour tout $j$, ce qui montre $(p_k\dottedlimp +p_\ell) = \dottedtop = p_n$ dans ce cas. En revanche, si $k>\ell$, il +faut distinguer deux cas : lorsque $j<\ell$, on a $p_k(w_j) = 1$ et +$p_\ell(w_j) = 1$, ce qui montre que $(p_k\dottedlimp p_\ell)(w_i) = +1$ pour $i<\ell$ ; mais comme $p_k(w_\ell) = 1$ et cependant +$p_\ell(w_\ell) = 0$, on a $(p_k\dottedlimp p_\ell)(w_i) = 0$ pour +$i\geq \ell$ ; c'est-à-dire que $(p_k\dottedlimp p_\ell) = p_\ell$ +dans ce cas. Enfin, $\dottedneg q$ est simplement $q\dottedlimp +\dottedbot$, c'est-à-dire $q\dottedlimp p_0$. + +Pour résumer : +\[ +\begin{aligned} +p_k \dottedland p_\ell &= p_{\min(k,\ell)} \\ +p_k \dottedlor p_\ell &= p_{\max(k,\ell)} \\ +(p_k \dottedlimp p_\ell) &= +\left\{ +\begin{array}{ll} +p_n&\text{~si $k\leq\ell$}\\ +p_\ell&\text{~si $k>\ell$}\\ +\end{array} +\right. +\\ +\dottedneg p_k &= +\left\{ +\begin{array}{ll} +p_n&\text{~si $k=0$}\\ +p_0&\text{~si $k>0$}\\ +\end{array} +\right. +\end{aligned} +\] + +La formule $A\lor\neg A$, classiquement démontrable, n'est pas validée +par ce cadre lorsque $n\geq 2$ (prendre $p_1$ pour $A$ : on trouve +$p_1 \dottedlor \dottedneg p_1 = p_1$). La formule $\neg +A\lor\neg\neg A$, en revanche, est validée par ce cadre (car +$\dottedneg\dottedneg p_k = p_n$ si $k>0$ et $p_0$ si $k=0$) mais +n'est pas prouvable intuitionnistement (par la propriété de la +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} + + % % % |