Two exercises on Löb's theorem.

1 files changed, 146 insertions, 0 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index 57abfbd..f3f8ae0 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -3266,6 +3266,152 @@ quantificateur universel.)
 %
 %
 
+\section{Arithmétique du premier ordre et théorème de Gödel}
+
+\exercice\label{exercise-loebs-theorem}\ (${\star}{\star}{\star}{\star}$)\par\nobreak
+
+Soit $T$ une théorie logique telle
+que\footnote{\label{footnote-goedelian-theory}Comme pour le théorème
+de Gödel, il s'agit essentiellement que $T$ soit codable par des
+entiers naturels, permette de formaliser l'arrêt des machines de
+Turing, et ait des démonstrations algorithmiquement testables.  On ne
+donnera pas de conditions exactes (ce serait trop fastidieux) mais les
+théories proposées en exemple les vérifient.}  l'arithmétique de
+Heyting $\mathsf{HA}$, l'arithmétique de Peano $\mathsf{PA}$, Coq ou
+$\mathsf{ZFC}$.  On se propose ici de démontrer le \textbf{théorème de
+  Löb} : si $A$ est un énoncé de $T$ et si $T$ prouve « si $T$
+prouve $A$, alors $A$ », alors $T$ prouve $A$.
+
+On construit pour cela le programme $g_A$ suivant : $g_A$ cherche une
+preuve dans $T$ de l'énoncé « si $g_A$ termine, alors $A$ », et s'il
+en trouve une, il termine immédiatement.
+
+\textbf{(1)} Expliquer pourquoi $g_A$ est bien défini.  A-t-on besoin
+d'arriver à tester la véracité ou la démontrabilité de $A$ pour le
+construire ?
+
+\textbf{(2)} Supposons que $g_A$ termine : montrer que $A$ est
+démontrable dans $T$.
+
+\textbf{(3)} Remarquer que le point précédent est lui-même démontrable
+dans $T$.
+
+\textbf{(4)} Déduire de (3) que si $T$ prouve « si $T$ prouve $A$,
+alors $A$ », alors $g_A$ termine.
+
+\textbf{(5)} Déduire de (2) et (4) que si $T$ prouve « si $T$
+prouve $A$, alors $A$ », alors $T$ provue $A$.
+
+\begin{corrige}
+\textbf{(1)} Le programme $g_A$ est, comme d'habitude, bien défini
+grâce à l'astuce de Quine : il s'agit de construire le programme
+$h(e)$ qui cherche une preuve dans $T$ de l'énoncé « si $e$ termine,
+alors $A$ » et, s'il en trouve une, termine immédiatement, et de lui
+appliquer le théorème de récursion de Kleene.  Or l'énoncé entre
+guillemets peut être formalisé de façon algorithmique, et la
+contruction qui suit, notamment la recherche de démonstrations
+dans $T$, est bien algorithmique, donc $e \mapsto h(e)$ est bien
+calculable, et le théorème de récursion de Kleene s'applique.  On n'a
+pas besoin de tester $A$, juste de savoir algorithmiquement
+reconnaître une démonstration de « si $e$ termine, alors $A$ ».
+
+\textbf{(2)} Si $g_A$ termine, c'est qu'il a trouvé une démonstration
+dans $T$ de « si $g_A$ termine, alors $A$ ».  Mais le fait que $g_A$
+termine implique qu'il y a une démonstration dans $T$ de
+« $g_A$ termine » (en recopiant pas à pas la trace d'exécution, ou
+l'arbre de calcul, de $g_A$).  Comme $T$ permet le \textit{modus
+  ponens}, on en déduit qu'il y a une démonstration dans $T$ de $A$.
+
+\textbf{(3)} Tout ce qui a été utilisé dans la démonstration de (2)
+est de l'arithmétique élémentaire, et par ailleurs valable en logique
+intuitionniste (aucun raisonnement par l'absurde n'a été tenu), donc
+l'arithmétique de Heyting comme tous les systèmes proposés dans
+l'énoncé prouve le point du (2).  Bref, $T$ prouve « si $g_A$ termine,
+alors $T$ prouve $A$ ».
+
+\textbf{(4)} On vient de voir au (3) que $T$ prouve « si $g_A$
+termine, alors $T$ prouve $A$ » ; par conséquent, s'il prouve « si $T$
+prouve $A$, alors $A$ », par \textit{modus ponens}, il prouve « si
+$g_A$ termine, alors $A$ ».  Mais c'est exactement la preuve que $g_A$
+cherche, donc $g_A$ termine.
+
+\textbf{(5)} On a vu au (2) que si $g_A$ termine alors $T$ prouve $A$,
+et au (4) que si $T$ prouve « si $T$ prouve $A$, alors $A$ » alors
+$g_A$ termine.  On en déduit si $T$ prouve « si $T$ prouve $A$,
+alors $A$ » alors $T$ prouve $A$.  C'est le théorème de Löb.
+\end{corrige}
+
+%
+
+\exercice\ (${\star}{\star}{\star}{\star}$)\par\nobreak
+
+Soit $T$ une théorie logique telle que\footnote{Voir la
+note \ref{footnote-goedelian-theory}.}  l'arithmétique de Heyting
+$\mathsf{HA}$, l'arithmétique de Peano $\mathsf{PA}$, Coq ou
+$\mathsf{ZFC}$.
+
+On considère le programme $h$ suivant : $h$ cherche une démonstration
+dans $T$ du fait que $h$ termine, et s'il en trouve une, il termine
+immédiatement.
+
+\textbf{(1)} Expliquer pourquoi $h$ est bien défini.
+
+(Remarquez que ce programme est « conciliant » : alors que dans la
+démonstration du théorème de Gödel on a considéré un programme
+« contrariant » qui fait le contraire de la démonstration qu'il a
+trouvée, ici, si le programme trouve une preuve de son arrêt, il obéit
+sagement.)
+
+On va prouver que $h$ termine effectivement.
+
+\textbf{(2)} Montrer que si $T$ prouve que $h$ termine, alors $h$
+termine.
+
+\textbf{(3)} Remarquer que le point précédent est lui-même démontrable
+dans $T$.
+
+\textbf{(4)} Considérer l'énoncé « le programme $h$ termine »,
+appliquer le théorème de Löb énoncé à
+l'exercice \ref{exercise-loebs-theorem}, et conclure.
+
+\begin{proof}
+\textbf{(1)} Comme dans le (1) de
+l'exercice \ref{exercise-loebs-theorem}, le programme est bien défini
+par l'astuce de Quine et par le fait que vérifier une preuve dans $T$
+est algorithmique.
+
+\textbf{(2)} Par construction de $h$, si $T$ prouve que $h$ termine
+alors $h$ finira par trouver cette preuve, et terminera.
+(\emph{Attention :} ici il ne faut pas dire « si $T$ prouve que $h$
+termine alors $h$ termine puisqu'on l'a prouvé » : on n'a pas fait
+l'hypothèse que $T$ dit la vérité sur les arrêts de machines de
+Turing.)
+
+\textbf{(3)} Tout ce qui a été utilisé dans la démonstration de (2)
+est de l'arithmétique élémentaire, et par ailleurs valable en logique
+intuitionniste (aucun raisonnement par l'absurde n'a été tenu), donc
+l'arithmétique de Heyting comme tous les systèmes proposés dans
+l'énoncé prouve le point du (2).  Bref, $T$ prouve « si $T$ prouve que
+$h$ termine, alors $h$ termine ».
+
+\textbf{(4)} On a montré question (3) que $T$ prouve « si $T$ prouve
+que $h$ termine, alors $h$ termine ».  Mais on a montré à
+l'exercice \ref{exercise-loebs-theorem} que si $T$ prouve « si $T$
+prouve que $h$ termine, alors $h$ termine », alors $T$ prouve que $h$
+termine (c'est le théorème de Löb avec pour $A$ l'énoncé
+« $h$ termine »).  Par conséquent, $T$ prouve que $h$ termine.  Donc,
+par la question (1), $h$ termine effectivement.
+\end{proof}
+
+\emph{Remarque :} on peut résumer la conclusion de cet exercice en
+disant que « ceci est un théorème » est un théorème (mais la preuve,
+comme on vient de le voir, n'est pas vraiment évidente).
+
+
+%
+%
+%
+
 \section{Divers}
 
 \exercice\label{exercise-dragon-riddle}\ (${\star}{\star}{\star}{\star}{\star}$)\par\nobreak