From 6d4aa42dd6d3f036dac1a8a7f429fde7e62edee6 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Tue, 9 Jan 2024 01:17:39 +0100
Subject: The set of theorems is not computable.

---
 transp-inf110-03-quantif.tex | 42 +++++++++++++++++++++++++++++++++++++-----
 1 file changed, 37 insertions(+), 5 deletions(-)

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 5272f83..5c69859 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -1229,7 +1229,7 @@ y.\forall z. ((x=y) \Rightarrow (y=z) \Rightarrow (x=z))$ par
 
 \end{frame}
 %
-\section{Arithmétique du premier ordre}
+\section{Arithmétique du premier ordre et théorème de Gödel}
 \begin{frame}
 \frametitle{L'arithmétique de Heyting et de Peano}
 
@@ -1703,7 +1703,9 @@ $\mathsf{Consis}(\mathsf{PA})$ par la traduction CPS (et cette
 \smallskip
 
 Notamment, Peano ne prouve pas non plus
-$\mathsf{Consis}(\mathsf{HA})$.
+$\mathsf{Consis}(\mathsf{HA})$.  Par propriété de la disjonction,
+$\mathsf{HA}$ ne prouve même pas $\mathsf{Consis}(\mathsf{HA}) \lor
+\neg\mathsf{Consis}(\mathsf{HA})$.
 
 \par}
 
@@ -1727,7 +1729,7 @@ pour l'arithmétique).
 \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 :
+intuitioniste, pas limitée au premier ordre) $T$ telle que :
 \begin{itemize}
 \item les énoncés et démonstrations sont codables par des entiers
   naturels,
@@ -1749,8 +1751,38 @@ dans le second.
 \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.
+$\mathsf{Consis}(T)$ (toujours si $\mathsf{Consis}(T)$).
+{\footnotesize Ceci s'applique notamment à Coq, à $\mathsf{ZFC}$,
+  etc.}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{L'ensemble des théorèmes est semi-décidable non décidable}
+
+Avec $T$ comme au transparent précédent (et sous l'hypothèse
+$\mathsf{Consis}(T)$), par exemple $\mathsf{PA}$ supposons par
+l'absurde qu'on puisse décider algorithmiquement si une formule $P$
+est un théorème de $T$.
+
+\medskip
+
+Soit $g''$ le programme qui :
+\begin{itemize}
+\item teste si $\varphi_{g''}(0){\downarrow}=0$ est un théorème de $T$
+  (grâce à l'hypothèse effectuée),
+\item si oui, termine et renvoie $1$,
+\item si non, termine et renvoie $0$.
+\end{itemize}
+
+\medskip
+
+\itempoint Par construction, $g''$ termine forcément et renvoie soit
+$0$ soit $1$.  Si $g''$ termine et renvoie $0$, alors $T$ le prouve,
+donc $g''$ termine et renvoie $1$, contradiction ; si $g''$ termine et
+renvoie $1$, alors $T$ le prouve, donc (par $\mathsf{Consis}(T)$) il
+ne proue pas que $g''$ termine et renvoie $0$, donc $g''$ termine et
+renvoie $0$, contradiction.
 
 \end{frame}
 %
-- 
cgit v1.2.3