From 7642c21489594995bc78be6afe22cbae30239368 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sat, 2 Dec 2023 22:54:25 +0100
Subject: Various informal explanations of constructive math / intuitionism.

---
 transp-inf110-02-typage.tex | 142 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 142 insertions(+)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 9b95039..06473c2 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -1709,6 +1709,148 @@ A=\top&\bot&\top\\
 $
 \end{tabular}
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Un peu d'histoire des maths : Brouwer et l'intuitionnisme}
+
+\itempoint L'\textbf{intuitionnisme} est à l'origine une philosophie
+des mathématiques développée (à partir de 1912) par L. E. J. Brouwer
+(1881–1966) en réaction/opposition au \textbf{formalisme} promu par
+D. Hilbert (1862–1943).
+
+\medskip
+
+Quelques principes de l'intuitionnisme \emph{à l'origine} :
+
+\begin{itemize}
+\item rejet de la loi du tiers exclu (« principe d'omniscience ») pour
+  demander des preuves \alert{constructives} (pour Brouwer, montrer
+  que $x$ ne peut pas ne pas exister n'est pas la même chose que
+  montrer que $x$ existe),
+\item refus de la logique formelle (pour Brouwer, les maths sont
+  « créatives »),
+\item principes de continuité (notamment : toute fonction $\mathbb{R}
+  \to \mathbb{R}$ est continue).
+\end{itemize}
+
+\medskip
+
+\itempoint Idées rejetées par Hilbert (et la plupart des
+mathématiciens).
+
+$\rightarrow$ « controverse Hilbert-Brouwer » {\footnotesize
+  (rapidement devenue querelle personnelle)}
+
+\medskip
+
+Hilbert : « Retirer au mathématicien le principe du tiers exclu
+serait comme empêcher à un boxeur d'utiliser ses poings. »
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Les maths constructives après Brouwer}
+
+\itempoint L'intuitionnisme a été ensuite reformulé et modifié par les
+élèves de Brouwer et leurs propres élèves (notamment A. Heyting,
+A. Troelstra) et d'autres écoles (analyse constructive d'E. Bishop,
+constructivisme russe de A. Markov fils) :
+
+\begin{itemize}
+\item dans le cadre de la logique formelle (ou compatible avec elle),
+\item sans impliquer de principe \emph{contredisant} les maths
+  classiques,
+\item mais toujours \alert{sans la loi du tiers exclu}.
+\end{itemize}
+
+\bigskip
+
+\itempoint Les termes de « \textbf{mathématiques constructives} » et
+« intuitionnisme » sont devenus plus ou moins interchangeables pour
+« maths sans le tiers exclu ».
+
+\bigskip
+
+\itempoint Dans \emph{certains} tels systèmes, prouver $P\lor Q$
+resp. $\exists x.P(x)$ passe forcément par la preuve de $P$ ou de $Q$,
+resp. par la construction d'un $x$ vérifiant $P(x)$.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Pourquoi vouloir « boxer sans ses poings » ?}
+
+{\footnotesize Évidence : l'\alert{écrasante majorité des maths}
+  se fait en logique classique (loi du tiers exclu admise) !\par}
+
+\medskip
+
+Une preuve « constructive » (sans tiers exclu) est plus restrictive
+qu'une preuve classique, donc \alert{apporte plus} :
+
+\begin{itemize}
+\item principe de parcimonie ; \quad \itempoint curiosité purement théorique ;
+\item intérêt philosophique (pas de « principe d'omniscience ») ;
+\item validité dans un cadre mathématique plus large
+  ($\rightarrow$ « topos ») ;
+\item lien avec les systèmes de typage (via Curry-Howard) ;
+\item extraction d'algorithme (p.ex., d'une preuve de $\forall
+  m. \exists n. P(m,n)$ dans certains systèmes on peut extraire un
+  algo qui \alert{calcule} $n$ à partir de $m$) ;
+\item compatibilité avec des axiomes qui contredisent les maths
+  classiques (p.ex. « toute fonction $\mathbb{R}\to\mathbb{R}$ est
+  continue », « toute fonction $\mathbb{N}\to\mathbb{N}$ est
+  calculable » [$\leftarrow$ « calculabilité synthétique »]) qu'on
+  peut vouloir étudier.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Preuves classiques pas toujours satisfaisantes}
+
+Que penser de la preuve suivante ?
+
+\medskip
+
+\textbf{Affirmation :} Il existe un algo qui donné $k \in
+\mathbb{N}$ \alert{termine en temps fini} et renvoie
+\begin{itemize}
+\item soit le rang de la première occurrence de $k$ chiffres $7$ dans
+  l'écriture décimale de $\pi$,
+\item soit « $\infty$ » si une telle occurrence n'existe pas.
+\end{itemize}
+
+\medskip
+
+{\footnotesize
+
+\underline{Preuve} (classique !) : soit $f\colon \mathbb{N} \to
+\mathbb{N} \cup \{\infty\}$ la fonction qui à $k$ associe le rang
+recherché.
+
+\alert{De deux choses l'une :}
+\begin{itemize}
+\item soit il existe $k_0$ tel que $f(k) = \infty$ pour $k\geq k_0$ :
+  alors $f$ est calculable car $f$ est déterminée par $k_0$ et un
+  nombre \emph{fini} de valeurs $(f(0),\ldots,f(k_0-1))$ ;
+\item soit $f(k)$ est fini pour tout $k \in \mathbb{N}$ : alors $f$
+  est calculable par l'algorithme qui, donné $k$, calcule indéfiniment
+  des décimales de $\pi$ jusqu'à en trouver $k$ consécutives
+  valant $7$, et renvoie le rang (cet algorithme termine toujours par
+  hypothèse).
+\end{itemize}
+
+Dans tous les cas $f$ est calculable.\qed
+\par}
+
+\medskip
+
+\textcolor{blue}{Objection :} cette preuve (correcte en maths
+classiques) ne nous donne pas du tout d'algorithme !  Elle montre
+juste qu'il « existe » classiquement.
+
 \end{frame}
 %
 % TODO:
-- 
cgit v1.2.3