summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--transp-inf110-03-quantif.tex48
1 files 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
\]
@@ -1298,4 +1298,42 @@ 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}