From 082cc97afe2b11c709677bba4bc6282dfd49eef4 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 8 Jan 2024 17:39:27 +0100
Subject: Curry-Howard and equality for first-order logic.

---
 transp-inf110-03-quantif.tex | 98 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 98 insertions(+)

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index d2d9bd0..d2ef3ef 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -947,6 +947,7 @@ Présentation avec les seules conclusions :
 \end{frame}
 %
 \begin{frame}
+\label{example-predicate-proof-as-lambda-term}
 \frametitle{Notation des preuves par des $\lambda$-termes}
 
 On reprend la preuve donnée aux transp. précédents :
@@ -1127,6 +1128,103 @@ ordre (pas de \emph{fonctions} d'individus, seulement des
 (on ne peut former un terme d'individu qu'en invoquant une variable du
 contexte).
 
+\end{frame}
+%
+\begin{frame}
+\frametitle{Curry-Howard pour la logique du premier ordre}
+
+\itempoint Il faut penser Curry-Howard dans le sens
+preuve $\mapsto$ programme.
+
+\smallskip
+
+{\footnotesize (Faute de description précise de règles de typage on ne
+  peut pas espérer mieux ici.)\par}
+
+\medskip
+
+\itempoint Curry-Howard va mélanger le monde logique avec le monde des
+individus.
+
+\medskip
+
+\itempoint On convertit les propositions en types :
+\begin{itemize}
+\item $\Rightarrow,\land,\lor,\top,\bot$ deviennent
+  $\rightarrow,\times,+,1,0$ comme en calcul propositionnel,
+\item $\forall,\exists$ deviennent produits et sommes $\prod,\sum$
+  paramétrés par $v:I$.
+\end{itemize}
+
+\smallskip
+
+\itempoint On convertit preuves en programmes selon l'interprétation
+fonctionnelle des notations données au
+transp. \ref{natural-deduction-rules-with-quantifiers-and-notations}.
+
+\medskip
+
+\itempoint P.ex., la preuve de $(\exists x.\forall
+y.B(x,y))\Rightarrow (\forall y'.\exists x'.B(x',y'))$ donnée
+transp. \ref{example-predicate-proof-as-lambda-term} :
+\[
+\lambda(u:\exists x.\forall y.B(x,y)).\;
+\lambda(y':I).\;
+(\texttt{match~}u\texttt{~with~}\langle x,v\rangle \mapsto
+\langle x,vy'\rangle)
+\]
+devient un programme de type
+\[
+(\sum_{x:I} \prod_{y:I} \, B(x,y)) \rightarrow
+(\prod_{y':I} \sum_{x':I} \, B(x',y'))
+\]
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{L'égalité au premier ordre}
+
+\itempoint En général on veut travailler en logique du premier ordre
+\alert{avec égalité}.  C'est-à-dire qu'on introduit une relation
+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
+  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}
+
+\medskip
+
+{\footnotesize \itempoint La logique du premier ordre montre ici ses
+  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
+  s.P(s)$ une notation \textit{ad hoc}).\par}
+
+\medskip
+
+\itempoint Exemple de preuve : la symétrie $\forall x.\forall y.((x=y)
+\Rightarrow (y=x))$ est prouvée en appliquant la substitution à $P(s)$
+valant « $s=x$ », donc par le $\lambda$-terme
+\[
+\lambda (x:I). \,
+\lambda (y:I). \, \lambda (u:(x=y)). \, \textsf{subst}_{(\lambda
+  s.s=x)} \, x \, y \, u \, (\mathsf{refl}\,x)
+\]
+
+\medskip
+
+\itempoint Autre exemple : la transitivité $\forall x.\forall
+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)}
+\, y \, z \, v \, u
+\]
+
 \end{frame}
 %
 \end{document}
-- 
cgit v1.2.3