diff options
| -rw-r--r-- | transp-inf110-02-typage.tex | 56 |
1 files changed, 54 insertions, 2 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex index 25c5720..3dc9c75 100644 --- a/transp-inf110-02-typage.tex +++ b/transp-inf110-02-typage.tex @@ -4321,10 +4321,62 @@ complète pour le calcul propositionnel intuitionniste : \item\underline{complétude :} réciproquement, si $\dot\varphi(U_1,\ldots,U_r) = \dottedtop$ pour tous ouverts $U_1,\ldots,U_r$ de tout espace topologique $X$, \alert{ou même - simplement de $\mathbb{R}^n$}, alors $\varphi$ est démontrable en - calcul propositionnel intuitionniste. + simplement de $\mathbb{R}^n$} pour un $n \geq 1$ donné, alors + $\varphi$ est démontrable en calcul propositionnel intuitionniste. \end{itemize} +\medskip + +\itempoint La sémantique des ouverts modélise plus ou moins +l'intuition que la vérité est une « notion locale » (si quelque chose +est vrai en un point, c'est vrai autour de ce point). + +\end{frame} +% +\begin{frame} +\frametitle{Sémantique des ouverts : exemples} + +\itempoint Soit $U = \mathopen{]}0,1\mathclose{[}$ dans $X = + \mathbb{R}$. Alors +\begin{itemize} +\item $\dottedneg U = \mathopen{]}-\infty,0\mathclose{[} \cup + \mathopen{]}1,+\infty\mathclose{[}$ +\quad\itempoint $\dottedneg\dottedneg U = \mathopen{]}0,1\mathclose{[} = U$ +\quad\itempoint $(\dottedneg\dottedneg U \dottedlimp U) = \mathbb{R}$ +\item $U \dottedlor \dottedneg U = \mathbb{R}\setminus\{0,1\}$ +\quad\itempoint $((\dottedneg\dottedneg U \dottedlimp U) \dottedlimp +(U \dottedlor \dottedneg U)) = \mathbb{R}\setminus\{0,1\}$ +\end{itemize} +Par correction, ceci montre que $((\neg\neg A \Rightarrow A) +\Rightarrow (A \lor \neg A))$ n'est pas prouvable en logique +intuitionniste. + +\bigskip + +{\footnotesize + +\itempoint Dans $X = \mathbb{R}^2$, soit $U = \{(x_1,x_2) : x_1<0 +\text{~et~} x_2<0\}$ et $V_1 = \{x_1>0\}$ et $V_2 = \{x_2>0$\}. +\begin{itemize} +\item $\dottedneg U = \{(x_1,x_2) : x_1>0 \text{~ou~} x_2>0\} = + V_1\dottedlor V_2$ +\quad\itempoint Donc $(\dottedneg U \dottedlimp (V_1\dottedlor V_2)) = +\mathbb{R}^2$ +\item $(\dottedneg U \dottedlimp V_1) = \{(x_1,x_2) : x_1<0 + \text{~ou~} x_2>0\}$ +\item $(\dottedneg U \dottedlimp V_2) = \{(x_1,x_2) : x_1>0 + \text{~ou~} x_2<0\}$ +\item $(\dottedneg U \dottedlimp V_1) \dottedlor (\dottedneg U + \dottedlimp V_2) = \mathbb{R}^2 \setminus\{(0,0)\}$ +\end{itemize} +Ceci montre que $(\neg A \Rightarrow B_1) \lor (\neg A \Rightarrow +B_2) \Rightarrow (\neg A \Rightarrow (B_1\lor B_2))$ (« axiome de +Kreisel-Putnam ») n'est pas prouvable en logique intuitionniste (et +\textit{a fortiori} $(C \Rightarrow B_1) \lor (C \Rightarrow B_2) +\Rightarrow (C \Rightarrow (B_1\lor B_2))$ ne l'est pas). + +\par} + \end{frame} % % TODO: |