From 87bddb893aed3cc69e4df4e9b38061da4348eedc Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 22 Jan 2024 13:57:50 +0100
Subject: An exercise on Gödel's theorem.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 controle-20240126.tex | 79 +++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 79 insertions(+)

diff --git a/controle-20240126.tex b/controle-20240126.tex
index 7911a5c..42af5da 100644
--- a/controle-20240126.tex
+++ b/controle-20240126.tex
@@ -385,6 +385,85 @@ formule n'est pas démontrable.
 \end{corrige}
 
 
+
+%
+%
+%
+
+\exercice
+
+(On ne demande pas ici de réponses compliquées.)
+
+\textbf{(1)} Expliquer rapidement pourquoi, si $\mathscr{T}$ est un
+ensemble de formules logiques (par exemple de logique de premier
+ordre, mais peu importent les détails), on peut démontrer
+$P\rightarrow Q$ à partir de $\mathscr{T}$ si et seulement si on peut
+démontrer $Q$ à partir de $\mathscr{T} \cup \{P\}$.
+
+\textbf{(2)} Déduire de (1) et du théorème de Gödel que la théorie
+$\mathsf{PA}^*$ formée en ajoutant l'axiome
+$\neg\mathsf{Consis}(\mathsf{PA})$ à l'arithmétique de
+Peano ($\mathsf{PA}$), ne prouve pas $\bot$ (c'est-à-dire qu'elle
+n'est pas contradictoire).  On rappelle que
+$\mathsf{Consis}(\mathsf{PA})$ est l'énoncé qui affirme que
+$\mathsf{PA}$ n'est pas contradictoire, et que cet énoncé est
+démontrable dans les mathématiques usuelles $\mathsf{ZFC}$ où on
+travaille.
+
+\textbf{(3)} Expliquer pourquoi $\mathsf{Consis}(\mathsf{PA}^*)$
+implique $\mathsf{Consis}(\mathsf{PA})$ et en déduire que
+$\mathsf{PA}^*$ démontre $\neg\mathsf{Consis}(\mathsf{PA}^*)$.
+
+\textbf{(4)} On a vu en (2) que $\mathsf{PA}^*$ n'est pas
+contradictoire, et en (3) que $\mathsf{PA}^*$ démontre que
+$\mathsf{PA}^*$ est contradictoire.  Ceci peut sembler paradoxal.
+Qu'en pensez-vous ?
+
+\begin{corrige}
+\textbf{(1)} Les règles d'introduction et d'élimination
+de $\Rightarrow$ qui affirment que $\Gamma, P \vdash Q$ si et
+seulement si $\Gamma \vdash P\Rightarrow Q$ : autrement dit, on peut
+démontrer $P\Rightarrow Q$ si et seulement si on peut démontrer $Q$ en
+ajoutant $P$ aux hypothèses.
+
+\textbf{(2)} Le théorème de Gödel affirme que (sous l'hypothèse
+$\mathsf{Consis}(\mathsf{PA})$, qui est bien affirmable dans le cadre
+où on travaille), $\mathsf{Consis}(\mathsf{PA})$ n'est pas démontrable
+dans $\mathsf{PA}$ ; comme on est en logique classique (arithmétique
+de Peano !), c'est pareil que de dire que
+$\neg\neg\mathsf{Consis}(\mathsf{PA})$, ou, si on préfère,
+$(\neg\mathsf{Consis}(\mathsf{PA}))\Rightarrow\bot$ n'est pas
+démontrable dans $\mathsf{PA}$.  D'après la question précédente, cela
+signifie exactement que $\bot$ n'est pas démontrable dans $\mathsf{PA}
+\cup \{\neg\mathsf{Consis}(\mathsf{PA})\} =: \mathsf{PA}^*$.
+Autrement dit, on a $\mathsf{Consis}(\mathsf{PA}^*)$ : la théorie
+$\mathsf{PA}^*$ n'a pas de contradiction.
+
+\textbf{(3)} L'affirmation $\mathsf{Consis}(\mathsf{PA}^*)$ dit qu'on
+ne peut pas arriver à une contradiction à partir des axiomes de Peano
+auxquels on a ajouté l'axiome $\neg\mathsf{Consis}(\mathsf{PA})$ ; en
+particulier, on ne peut pas arriver à une contradiction à partir des
+axiomes de Peano seuls, c'est-à-dire $\mathsf{Consis}(\mathsf{PA})$.
+On a donc $\mathsf{Consis}(\mathsf{PA}^*) \Rightarrow
+\mathsf{Consis}(\mathsf{PA})$ (ce fait étant démontré à partir
+d'arithmétique élémentaire, donc dans $\mathsf{PA}$).
+
+Comme $\mathsf{PA}^*$ a $\neg\mathsf{Consis}(\mathsf{PA})$ dans ses
+axiomes, si $\mathsf{Consis}(\mathsf{PA}^*) \Rightarrow
+\mathsf{Consis}(\mathsf{PA})$, on en déduit que
+$\neg\mathsf{Consis}(\mathsf{PA}^*)$ dans $\mathsf{PA}^*$.
+
+\textbf{(4)} La théorie $\mathsf{PA}^*$ \emph{« pense »} (ou plus
+exactement, postule) que l'arithmétique de Peano est contradictoire,
+et en particulier (question (3)) qu'elle-même est contradictoire.
+Mais elle se trompe : ni $\mathsf{PA}$ ni $\mathsf{PA}^*$ elle-même ne
+sont contradictoires.  Ce n'est pas absurde : c'est juste que
+$\mathsf{PA}^*$ a un axiome faux, mais le phénomène d'incomplétude
+énoncé par le théorème de Gödel empêche de voir que cet axiome est
+faux, donc d'aboutir effectivement à une contradiction.
+\end{corrige}
+
+
 %
 %
 %
-- 
cgit v1.2.3