From 618450ebbd0c2c49d7f53f12e3d66021c7b1dae1 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Sun, 3 Dec 2023 23:39:26 +0100
Subject: Non-uniqueness of proofs.
---
transp-inf110-02-typage.tex | 58 ++++++++++++++++++++++++++++++++++++++++++++-
1 file changed, 57 insertions(+), 1 deletion(-)
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 50a442d..5083da9 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -2253,11 +2253,67 @@ fun u -> (match (pi1 u) with Inj1 v -> Inj1 v\\
{\color{purple}- : ('a, 'b) sum * ('a, 'c) sum -> ('a, 'b * 'c) sum = <fun>}
}
+\end{frame}
+%
+\begin{frame}
+\frametitle{Les preuves ne sont pas uniques}
+
+{\footnotesize La question de l'égalité est compliquée, on ne
+ l'abordera guère.\par}
+
+\itempoint Une même proposition peut avoir des preuves
+(fonctionnellement) \alert{différentes}.
+
+\medskip
+
+Par exemple, les entiers de Church typés :
+\begin{itemize}
+\item $\overline{0}_{\alpha} :=
+ \lambda(f:\alpha\to\alpha).\lambda(x:\alpha).x$
+\item $\overline{1}_{\alpha} :=
+ \lambda(f:\alpha\to\alpha).\lambda(x:\alpha).fx$
+\item $\overline{2}_{\alpha} :=
+ \lambda(f:\alpha\to\alpha).\lambda(x:\alpha).f(fx)$ etc.
+\end{itemize}
+tous de type $(\alpha\to\alpha)\to(\alpha\to\alpha)$ prouvent tous
+$(A\Rightarrow A)\Rightarrow(A\Rightarrow A)$.
+
+\medskip
+
+{\footnotesize
+
+($\overline{0}$) : « [\textbf{(1)} Supposons $A\Rightarrow A$.
+ [\textbf{(2)} Supposons $A$.] \textbf{(3)} On a $A\Rightarrow A$
+ par $\Rightarrow$Int de (2) dans (2).] \textbf{(4)} On a
+ $(A\Rightarrow A)\Rightarrow(A\Rightarrow A)$ par $\Rightarrow$Int
+ de (1) dans (3). »
+
+\medskip
+
+($\overline{1}$) : « [\textbf{(1)} Supposons $A\Rightarrow A$.
+ [\textbf{(2)} Supposons $A$. \textbf{(3)} On a $A$ par
+ $\Rightarrow$Élim sur (1) et (2).] \textbf{(4)} On a
+ $A\Rightarrow A$ par $\Rightarrow$Int de (2) dans (3).]
+\textbf{(5)} On a $(A\Rightarrow A)\Rightarrow(A\Rightarrow A)$ par
+$\Rightarrow$Int de (1) dans (4). »
+
+\medskip
+
+($\overline{2}$) : « [\textbf{(1)} Supposons $A\Rightarrow A$.
+ [\textbf{(2)} Supposons $A$. \textbf{(3)} On a $A$ par
+ $\Rightarrow$Élim sur (1) et (2). \textbf{(4)} On a $A$ par
+ $\Rightarrow$Élim sur (1) et (3).] \textbf{(5)} On a
+ $A\Rightarrow A$ par $\Rightarrow$Int de (2) dans (4).]
+\textbf{(6)} On a $(A\Rightarrow A)\Rightarrow(A\Rightarrow A)$ par
+$\Rightarrow$Int de (1) dans (5). »
+
+\par}
+
\end{frame}
%
% TODO:
% - substitution des variables propositionnelles par des formules
% - substitution d'équivalences
-% - Kriple
+% - Kripke
%
\end{document}
--
cgit v1.2.3