diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 172 |
1 files changed, 159 insertions, 13 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index 1485cf7..5272f83 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -31,6 +31,7 @@ \renewcommand{\thefootnote}{\textdagger} \newcommand{\dbllangle}{\mathopen{\langle\!\langle}} \newcommand{\dblrangle}{\mathclose{\rangle\!\rangle}} +\newcommand{\cps}{\mathrm{CPS}} %\newcommand{\dottedlimp}{\mathbin{\dot\Rightarrow}} %\newcommand{\dottedland}{\mathbin{\dot\land}} %\newcommand{\dottedlor}{\mathbin{\dot\lor}} @@ -1428,22 +1429,56 @@ On peut souvent s'en faire une idée d'après son type, p.ex. : $n$ à $0$ soit un programme qui donné un tel témoignage renvoie qqch d'impossible. Donc en pratique, ce programme prend $n$ et teste si $n=0$. -\item Une preuve de $\forall m.\exists n. P(m,n)$ va correspondre à un +\item Une preuve de $\forall m.\exists n. Q(m,n)$ va correspondre à un programme qui prend $m$ et renvoie $n$ ainsi qu'un témoignage de - $P(m,n)$. + $Q(m,n)$. \end{itemize} \medskip -Notamment, \alert{si} $\forall m.\exists n. P(m,n)$ est prouvable dans +Notamment, \alert{si} $\forall m.\exists n. Q(m,n)$ est prouvable dans l'arithmétique de \alert{Heyting}, \alert{alors} on peut en déduire -$\varphi_e$ générale récursive telle que $\forall -m. P(m,\varphi_e(m))$ (\textbf{extraction} de programme à partir de la +$\varphi_e$ générale récursive totale telle que $\forall +m. Q(m,\varphi_e(m))$ (\textbf{extraction} de programme à partir de la preuve). \end{frame} % \begin{frame} +\frametitle{Propriétés métamathématiques de l'arithmétique de Heyting} + +\itempoint L'arithmétique de Heyting a la \textbf{propriété de la + disjonction} : si elle prouve $Q_1\lor Q_2$, alors elle prouve $Q_1$ +ou $Q_2$. + +\smallskip + +\itempoint Et la \textbf{propriété de l'existence} : si elle prouve +$\exists n. Q(n)$, alors elle prouve $Q(n)$ pour un $n$ explicite. + +\smallskip + +{\tiny Petits caractères : ces faits, comme l'extraction de programme, + dépendent d'un résultat de normalisation sur l'arithmétique de + Heyting (donc de $\mathsf{Consis}(\mathsf{HA})$).\par} + +\medskip + +\centerline{*} + +\medskip + +\itempoint Soit $P^{\cps}$ la formule obtenue en ajoutant +« $\neg\neg$ » devant la formule tout entière, devant la conclusion de +chaque $\Rightarrow$, et après chaque $\forall k$. Alors Heyting +prouve $P^{\cps}$ ssi Peano prouve $P$ : +\[ +\mathsf{PA} \vdash P\text{~\alert{ssi}~}\mathsf{HA} \vdash P^{\cps} +\] + +\end{frame} +% +\begin{frame} \frametitle{Une différence entre Heyting et Peano} \itempoint On peut formaliser les fonctions générales récursives (ou @@ -1452,6 +1487,26 @@ $\varphi_e(i){\downarrow}$ signifie $\exists n. T(n,e, i)$ où $T$ est le prédicat (p.r.) de la forme normale de Kleene, « $n$ code un arbre de calcul valable de $\varphi_e$ sur l'entrée $i$ ». +\medskip + +%% \itempoint Si l'arithmétique de Heyting $\mathsf{HA}$ prouve $\forall +%% m. (Q_1(m) \lor Q_2(m))$, alors il existe $\varphi_e \colon \mathbb{N} +%% \to \{1,2\}$ générale récursive totale telle que $\mathsf{HA}$ prouve +%% $\forall m. (\varphi_e(m){\downarrow}=1 \land Q_1(m) \; \lor \penalty0\; +%% \varphi_e(m){\downarrow}=2 \land Q_2(m))$. + +%% \smallskip + +\itempoint Si $\mathsf{PA}$ prouve $\forall +m. \varphi_e(m){\downarrow}$, alors $\mathsf{HA}$ le prouve (la +réciproque est évidente). + +\medskip + +\itempoint Si $\mathsf{HA}$ prouve $\forall m.\exists n. Q(m,n)$, +alors il existe $e$ telle que $\mathsf{HA}$ prouve $\forall +m. \varphi_e(m){\downarrow}$ et $\forall m. Q(m,\varphi_e(m))$. + \bigskip \itempoint La formule @@ -1460,15 +1515,22 @@ de calcul valable de $\varphi_e$ sur l'entrée $i$ ». \] {\footnotesize (c'est-à-dire $\forall e. \forall i. ((\exists - n. T(n,e, i)) \lor \neg (\exists n. T(n,e, i)))$)} est démontrable -dans l'arithmétique de Peano (= en logique classique). Elle -\alert{n'est pas démontrable} en arithmétique de Heyting (= en logique -intuitioniste), car par Curry-Howard on pourrait extraire de la preuve -un algorithme résolvant le problème de l'arrêt. + n. T(n,e, i)) \lor \neg (\exists n. T(n,e, i)))$)} est évidemment +démontrable dans l'arithmétique de Peano (= en logique classique). +Elle \alert{n'est pas démontrable} en arithmétique de Heyting (= en +logique intuitioniste), car par Curry-Howard on pourrait extraire de +la preuve un algorithme résolvant le problème de l'arrêt. + +\smallskip + +{\tiny Petits caractères : ces faits, comme l'extraction de programme, + dépendent d'un résultat de normalisation sur l'arithmétique de + Heyting (donc de $\mathsf{Consis}(\mathsf{HA})$).\par} \end{frame} % \begin{frame} +\label{proof-checking-predicate} \frametitle{Formalisation de la démontrabilité} \textcolor{blue}{Idée-clé :} tester \alert{si une preuve est valable} @@ -1505,6 +1567,7 @@ moins) semi-décidable. \end{frame} % \begin{frame} +\label{halting-implies-halting-provability} \frametitle{Démontrabilité de l'arrêt} \textcolor{blue}{Idée-clé :} si une machine de Turing s'arrête, on @@ -1567,7 +1630,8 @@ Soit $g$ le programme suivant : Ce programme $g$ a bien un sens, comme d'habitude, par l'« astuce de Quine » (théorème de récursion de Kleene) + le fait que la -vérification des preuves est algorithmique. +vérification des preuves est algorithmique +(transp. \ref{proof-checking-predicate}). \end{frame} % @@ -1582,8 +1646,9 @@ Admettons provisoirement ce qu'on notera \bigskip -\itempoint Si $g$ trouve une preuve qu'il ne termine pas, alors il -termine. Mais ce point donne une preuve qu'il termine. Donc on a une +\itempoint Si le programme $g$ trouve une preuve qu'il ne termine pas, +alors il termine. Mais ce point donne une preuve qu'il termine +(transp. \ref{halting-implies-halting-provability}). Donc on a une preuve de $\bot$ dans l'arithmétique de Peano, contredisant le point ci-dessus. @@ -1608,4 +1673,85 @@ qu'il ne termine pas. Donc : \end{frame} % +\begin{frame} +\frametitle{Cohérence de Peano} + +\itempoint L'énoncé $\mathsf{Consis}(\mathsf{PA})$ peut se lire +ainsi : + +\smallskip + +« Le programme $g'$ qui parcourt les entiers et, pour chacun, teste +s'il est le code de Gödel d'une preuve de $\bot$ dans l'arithmétique +de Peano et dans ce cas termine, ne termine pas. » + +\smallskip + +Cet énoncé \alert{a un sens} dans l'arithmétique du premier ordre, +mais (on vient de le voir) \alert{n'est pas démontrable} s'il est +vrai. + +\medskip + +{\footnotesize + +\itempoint L'énoncé $\mathsf{Consis}(\mathsf{HA})$ analogue pour +l'arithmétique de Heyting \alert{est équivalent} à +$\mathsf{Consis}(\mathsf{PA})$ par la traduction CPS (et cette +équivalence est prouvable dans $\mathsf{HA}$). + +\smallskip + +Notamment, Peano ne prouve pas non plus +$\mathsf{Consis}(\mathsf{HA})$. + +\par} + +\bigskip + +\itempoint En revanche, $\mathsf{ZFC}$ (le cadre usuel pour faire des +mathématiques) démontre $\mathsf{Consis}(\mathsf{PA})$ : « Les axiomes +de Peano sont vrais dans $\mathbb{N}$ donc leurs conséquences le sont +aussi, et notamment $\bot$ ne peut pas en faire partie. (Et au +passage, si $\mathsf{PA}$ démontre $\varphi_e(i){\downarrow}$, alors +$\varphi_e(i){\downarrow}$ est vrai.) » + +\smallskip + +Donc $\mathsf{ZFC}$ est strictement plus fort que $\mathsf{HA}$ (même +pour l'arithmétique). + +\end{frame} +% +\begin{frame} +\frametitle{Le théorème de Gödel généralisé} + +Pour n'importe quelle sorte de « théorie logique » (classique ou +intuitioniste) $T$ telle que : +\begin{itemize} +\item les énoncés et démonstrations sont codables par des entiers + naturels, +\item on peut algorithmiquement tester si un entier naturel code une + démonstration valable dans $T$, et quelle est sa conclusion, +\item $T$ permet de formaliser « $\varphi_e(i){\downarrow}$ » + (calculablement en $e$ et $i$), +\item si $\varphi_e(i){\downarrow}$ alors on peut tirer d'une trace + d'exécution une preuve de ce fait dans $T$, et idem pour une boule + infinie explicite, +\end{itemize} +on peut construire le programme $g_T$ qui cherche en parallèle dans +$T$ une preuve de que $g_T$ termine ou ne termine pas, et fait une +boule infinie explicite dans le premier cas, termine immédiatement +dans le second. + +\medskip + +\itempoint Si $T$ ne prouve pas $\bot$ (hypothèse notée +« $\mathsf{Consis}(T)$ »), alors $g_T$ ne termine pas, mais $T$ ne +peut pas le prouver. Notamment, $T$ ne prouve pas +$\mathsf{Consis}(T)$ (toujours si $\mathsf{Consis}(T)$). Ceci +s'applique notamment à Coq, à $\mathsf{ZFC}$, etc. + +\end{frame} +% \end{document} |