summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--transp-inf110-03-quantif.tex172
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}