diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 48 |
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} |