Gödel's theorem.

1 files 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
 
@@ -1443,4 +1443,169 @@ 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}