diff options
-rw-r--r-- | transp-inf110-03-quantif.tex | 42 |
1 files 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} % |