From c33e09b6f137c315e3c95a880e4a67c64180dec0 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Mon, 8 Jan 2024 21:11:01 +0100 Subject: Gödel's theorem. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- transp-inf110-03-quantif.tex | 171 ++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 168 insertions(+), 3 deletions(-) diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index e2490e0..1485cf7 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -1238,9 +1238,9 @@ Elle est basée sur les \textbf{axiomes de Peano} (transp. suivant). \medskip -\itempoint On parle d'\textbf{arithmétique de Heyting} en logique -intuitionniste, et \textbf{de Peano} en logique classique -(\alert{mêmes axiomes}, seule la logique change). +\itempoint On parle d'\textbf{arithmétique de Heyting} ($\mathsf{HA}$) +en logique intuitionniste, et \textbf{de Peano} ($\mathsf{PA}$) en +logique classique (\alert{mêmes axiomes}, seule la logique change). \medskip @@ -1441,6 +1441,171 @@ $\varphi_e$ générale récursive telle que $\forall m. P(m,\varphi_e(m))$ (\textbf{extraction} de programme à partir de la preuve). +\end{frame} +% +\begin{frame} +\frametitle{Une différence entre Heyting et Peano} + +\itempoint On peut formaliser les fonctions générales récursives (ou +machines de Turing) en arithmétique de Heyting. Par exemple, +$\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$ ». + +\bigskip + +\itempoint La formule +\[ +\forall e. \forall i. (\varphi_e(i){\downarrow} \lor \neg \varphi_e(i){\downarrow}) +\] + +{\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. + +\end{frame} +% +\begin{frame} +\frametitle{Formalisation de la démontrabilité} + +\textcolor{blue}{Idée-clé :} tester \alert{si une preuve est valable} +est algorithmiquement \alert{décidable} (même primitif récursif). + +\smallskip + +En revanche, tester si un \alert{énoncé est un théorème} est seulement +\alert{semi-décidable} (en parcourant toutes les preuves possibles). + +\medskip + +Plus précisément : + +\smallskip + +\itempoint On peut construire un codage de Gödel pour les formules +arithmétiques et les preuves dans l'arithmétique de Heyting (ou de +Peano), et notamment écrire un prédicat \alert{primitif récursif} +\[ +\mathsf{Pf}_{\mathsf{HA}}(n,k) +\quad\text{~resp.~}\quad +\mathsf{Pf}_{\mathsf{PA}}(n,k) +\] +qui signifie « $n$ est le code de Gödel d'une preuve dans +l'arithmétique de Heyting (resp. Peano) de la formule codée par $k$ ». + +\medskip + +\itempoint Notamment, $\exists n.\, \mathsf{Pf}(n,k)$ peut se lire +comme « $k$ code un théorème », et l'ensemble de ces $k$ est (au +moins) semi-décidable. + +\end{frame} +% +\begin{frame} +\frametitle{Démontrabilité de l'arrêt} + +\textcolor{blue}{Idée-clé :} si une machine de Turing s'arrête, on +peut démontrer (dans l'arithmétique de Heyting) qu'elle s'arrête en +donnant une trace d'exécution pas à pas. + +\medskip + +Plus précisément : + +\smallskip + +\itempoint Si $T(n,e,i)$, i.e., si $n$ est un arbre de calcul de +$\varphi_e$ sur l'entrée $i$, alors on peut de façon algorithmique +(même p.r.) tirer de $n$ une preuve de $T(n,e,i)$ dans l'arithmétique +de Heyting (i.e., un $n'$ tel que $\mathsf{Pf}_{\mathsf{HA}}(n',k)$ où +$k$ est le code de Gödel de l'énoncé $\varphi_e(i){\downarrow}$, +i.e. $\exists n. T(n,e, i)$). + +\medskip + +\begin{center} +\alert{Si une machine de Turing s'arrête, alors le fait qu'elle + s'arrête est prouvable} (dans l'arithmétique de Heyting, \textit{a + fortiori} de Peano). +\end{center} + +\medskip + +{\footnotesize\itempoint On notera aussi que si programme fait une + boucle infinie \emph{explicite évidente}, alors le fait qu'il ne + termine pas est également prouvable.\par} + +\end{frame} +% +\begin{frame} +\frametitle{Gödel, Rosser et Turing jouent ensemble} + +{\footnotesize (Preuve du théorème de Gödel revue et corrigée par + Turing et par Rosser.)\par} + +\medskip + +Soit $g$ le programme suivant : +\begin{itemize} +\item $g$ cherche en parallèle une preuve (dans l'arithmétique de + Peano, disons) de l'énoncé « le programme $g$ termine » + (i.e. $\varphi_g(0){\downarrow}$) et de l'énoncé « le programme $g$ + ne termine pas », +\item c'est-à-dire qu'il énumère les entiers et, pour chacun, teste + s'il est le code de Gödel d'une preuve de $\varphi_g(0){\downarrow}$ + ou de $\neg\varphi_g(0){\downarrow}$, +\item s'il trouve (en premier) une preuve que $g$ termine, alors il + fait une boucle infinie explicite, +\item s'il trouve (en premier) une preuve que $g$ ne termine pas, + alors il termine immédiatement. +\end{itemize} + +\smallskip + +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. + +\end{frame} +% +\begin{frame} +\frametitle{Le théorème de Gödel} + +Admettons provisoirement ce qu'on notera +« $\mathsf{Consis}(\mathsf{PA})$ » : +\[ +\text{l'arithmétique de Peano ne prouve pas $\bot$} +\] + +\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 +preuve de $\bot$ dans l'arithmétique de Peano, contredisant le point +ci-dessus. + +\medskip + +\itempoint Si $g$ trouve une preuve qu'il termine, il fait une boucle +infinie. Mais ce point donne une preuve que $g$ ne termine pas +(boucle infinie explicite). Donc on a une preuve de $\bot$ dans +l'arithmétique de Peano, contredisant le point ci-dessus. + +\medskip + +Conclusion : $g$ ne trouve ni de preuve qu'il termine ni de preuve +qu'il ne termine pas. Donc : +\begin{itemize} +\item $g$ ne termine pas, +\item ce fait-là n'est pas prouvable dans l'arithmétique de Peano, +\item mais on l'a prouvé à l'aide de $\mathsf{Consis}(\mathsf{PA})$, + donc $\mathsf{Consis}(\mathsf{PA})$ lui-même n'est pas prouvable + dans Peano (toujours en supposant $\mathsf{Consis}(\mathsf{PA})$). +\end{itemize} + \end{frame} % \end{document} -- cgit v1.2.3