From d2c6749c7a37fc1f240613d3d618908ecabcd558 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Fri, 12 Jan 2024 18:26:59 +0100 Subject: =?UTF-8?q?Two=20exercises=20on=20L=C3=B6b's=20theorem.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- exercices-inf110.tex | 146 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 146 insertions(+) diff --git a/exercices-inf110.tex b/exercices-inf110.tex index 57abfbd..f3f8ae0 100644 --- a/exercices-inf110.tex +++ b/exercices-inf110.tex @@ -3262,6 +3262,152 @@ quantificateur universel.) \end{corrige} +% +% +% + +\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). + + % % % -- cgit v1.2.3