More around Gödel and whatnot.

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}