From 7cade47b047775b70e0422a236431fc8ce824272 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 8 Jan 2024 18:46:37 +0100
Subject: An example proof in Heyting arithmetic.

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

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index f2eb9e3..fec933e 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -1190,8 +1190,8 @@ devient un programme de type
 binaire « $=$ » (notée de façon infixe) sujette aux \alert{axiomes}
 suivants :
 \begin{itemize}
-\item réflexivité : $\textsf{refl} : \forall x.(x=x)$
-\item substitution : $\textsf{subst}_{(\lambda s.P(s))} : \forall
+\item réflexivité : $\mathsf{refl} : \forall x.(x=x)$
+\item substitution : $\mathsf{subst}^{(\lambda s.P(s))} : \forall
   x.\forall y.((x=y) \Rightarrow P(x) \Rightarrow P(y))$ pour toute
   formule $P(s)$ ayant une variable d'individu libre $s$.
 \end{itemize}
@@ -1202,7 +1202,7 @@ suivants :
   limites : on n'a pas le droit de quantifier sur $P(s)$ ni même
   d'introduire $\lambda (s:I). P(s)$.  Il faut donc comprendre qu'on a
   un « schéma d'axiomes » de substitution, dont chaque
-  $\textsf{subst}_{(\lambda s.P(s))}$ est une instance (et $\lambda
+  $\mathsf{subst}^{(\lambda s.P(s))}$ est une instance (et $\lambda
   s.P(s)$ une notation \textit{ad hoc}).\par}
 
 \medskip
@@ -1212,7 +1212,7 @@ suivants :
 valant « $s=x$ », donc par le $\lambda$-terme
 \[
 \lambda (x:I). \,
-\lambda (y:I). \, \lambda (u:(x=y)). \, \textsf{subst}_{(\lambda
+\lambda (y:I). \, \lambda (u:(x=y)). \, \mathsf{subst}^{(\lambda
   s.s=x)} \, x \, y \, u \, (\mathsf{refl}\,x)
 \]
 
@@ -1222,7 +1222,7 @@ valant « $s=x$ », donc par le $\lambda$-terme
 y.\forall z. ((x=y) \Rightarrow (y=z) \Rightarrow (x=z))$ par
 \[
 \lambda (x:I). \, \lambda (y:I). \, \lambda (z:I). \, \lambda
-(u:(x=y)). \, \lambda (v:(y=z)). \, \textsf{subst}_{(\lambda s.x=s)}
+(u:(x=y)). \, \lambda (v:(y=z)). \, \mathsf{subst}^{(\lambda s.x=s)}
 \, y \, z \, v \, u
 \]
 
@@ -1296,6 +1296,44 @@ libre $s$ : la substitution de l'égalité et la récurrence sont des
 \alert{schémas d'axiomes} (un axiome pour chaque $P$ possible) car on
 ne peut pas quantifier sur $P$ au premier ordre.
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Exemple de preuve en arithmétique de Heyting}
+
+Montrons que $\forall n. (n=0 \lor \neg n=0)$ (classiquement c'est une
+évidence logique, mais c'est aussi démontrable intuitionistement) :
+
+\medskip
+
+\itempoint On procède par récurrence.  Notons par $P(k)$ la formule
+$k=0 \lor \neg k=0$ :
+\begin{itemize}
+\item $P(0)$ vaut car $0=0$ vaut (réflexivité de l'égalité).
+\item $P(Sn)$ vaut car $\neg(Sn=0)$ (premier axiome de Peano).  En
+  particulier, $P(n) \Rightarrow P(Sn)$.
+\item Donc, par récurrence, $\forall n. P(n)$, ce qu'on voulait
+  prouver.
+\end{itemize}
+
+\medskip
+
+\itempoint Le $\lambda$-terme de cette preuve ressemble à quelque
+chose comme ceci : $\mathsf{recurr}^{(\lambda k.(k=0 \lor \neg
+  k=0))}\penalty0\, (\iota_1^{(0=0, \neg 0=0)}(\mathsf{refl}\,0))
+\penalty0\, (\lambda (n:\mathsf{nat}).\penalty0\,
+\lambda(h:(n=0)\lor\neg(n=0)).\penalty0\, \iota_2^{(Sn=0, \neg
+  Sn=0)}(\mathsf{succnotz}\,n))$.
+
+\smallskip
+
+{\footnotesize Ici, « $\mathsf{nat}$ » a été mis pour le type des
+  individus (entiers naturels), « $\mathsf{succnotz}$ » pour l'axiome
+  de Peano qui affirme $\forall n.\neg(Sn=0)$, et
+  « $\mathsf{recurr}^{(\lambda k.P(k))}$ » pour celui qui affirme
+  $P(0) \Rightarrow \penalty100 (\forall n.(P(n)\Rightarrow P(Sn)))
+  \Rightarrow \penalty100 (\forall n.P(n))$.\par}
+
 \end{frame}
 %
 \end{document}
-- 
cgit v1.2.3