More about first-order arithmetic.

1 files changed, 111 insertions, 4 deletions

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index fec933e..e2490e0 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -1247,12 +1247,12 @@ intuitionniste, et \textbf{de Peano} en logique classique
 \itempoint Le cadre de base est la logique du premier ordre
 \alert{avec égalité} (cf. transp. \ref{first-order-equality}) et avec
 des opérations de formation de termes d'individus $0$ (nullaire), $S$
-(unaire) et $+$, $\times$, $\textasciicircum$ (binaires) :
+(unaire) et $+$, $\times$, $\vartriangle$ (binaires) :
 \begin{itemize}
 \item $0$ est un terme,
 \quad\itempoint si $m$ est un terme, $(Sm)$ en est un,
 \item si $m$, $n$ sont deux termes, $(m+n)$, $(m\times n)$,
-  $(m\textasciicircum n)$ en sont.
+  $(m\vartriangle n)$ en sont.
 \end{itemize}
 
 \smallskip
@@ -1285,8 +1285,8 @@ Les \textbf{axiomes de Peano} du premier ordre s'y ajoutent :
 \quad\itempoint $\forall m.\forall n.(m+(Sn) = S(m+n))$
 \item $\forall m.(m\times 0 = 0)$
 \quad\itempoint $\forall m.\forall n.(m\times (Sn) = m\times n + m)$
-\item $\forall m.(m\textasciicircum 0 = S0)$
-\quad\itempoint $\forall m.\forall n.(m\textasciicircum (Sn) = m\textasciicircum n \times m)$
+\item $\forall m.(m\vartriangle 0 = S0)$
+\quad\itempoint $\forall m.\forall n.(m\vartriangle (Sn) = m\vartriangle n \times m)$
 \end{itemize}
 
 \medskip
@@ -1299,6 +1299,7 @@ ne peut pas quantifier sur $P$ au premier ordre.
 \end{frame}
 %
 \begin{frame}
+\label{example-proof-in-heyting-arithmetic}
 \frametitle{Exemple de preuve en arithmétique de Heyting}
 
 Montrons que $\forall n. (n=0 \lor \neg n=0)$ (classiquement c'est une
@@ -1336,4 +1337,110 @@ chose comme ceci : $\mathsf{recurr}^{(\lambda k.(k=0 \lor \neg
 
 \end{frame}
 %
+\begin{frame}
+\frametitle{Quelques théorèmes de l'arithmétique du premier ordre}
+
+On peut prouver en arithmétique de Heyting (et notamment, de Peano)
+que :
+\begin{itemize}
+\item l'addition est commutative, associative, a $0$ pour élément
+  neutre...,
+\item la multiplication est commutative, associative, a $1 = S0$ pour
+  élément neutre...,
+\item les identités habituelles sur l'addition, la multiplication,
+  l'exponentiation,
+\item les propriétés basiques de $m\leq n$ défini par $\exists
+  k.(n=m+k)$,
+\item les propriétés basiques du codage de Gödel $\langle m,n\rangle$
+  défini par $m + \frac{1}{2}(m+n)(m+n+1)$,
+\item les propriétés basiques des suites finies codées par $\dbllangle
+  a_0,\ldots,a_{k-1}\dblrangle := \langle a_0, \langle a_1,
+  \langle\cdots,\langle a_{k-1},0\rangle+1\cdots\rangle+1\rangle+1$,
+\item l'existence et l'unicité de la division euclidienne,
+\item des propriétés arithmétique de base : existence d'une infinité
+  de nombres premiers, existence et unicité de la DFP, irrationalité
+  de $\sqrt{2}$ ($\forall p. \forall q. ((p\times p = 2\times q \times
+  q) \Rightarrow q = 0)$), etc.
+\end{itemize}
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Curry-Howard pour l'arithmétique de Heyting}
+
+\itempoint La formule $m=n$ est une relation binaire sur les entiers
+naturels : elle doit devenir un \alert{type} (paramétré par $m$, $n$,
+et habité seulement lorsqu'ils sont égaux) sous l'effet de
+Curry-Howard.
+
+\smallskip
+
+\itempoint Il faut y penser comme le type des \textbf{témoignages
+  d'égalité} de $m$ et $n$.  En pratique, ce sera un type ayant
+seul habitant $\{m\}$ lorsque $m=n$ et aucun sinon.
+
+\medskip
+
+\itempoint Chaque axiome de Peano doit devenir un
+programme {\footnotesize (à penser comme l'API d'une bibliothèque
+  « entiers naturels »)}.  Le seul non trivial est le schéma de
+récurrence $P(0) \Rightarrow (\forall n.(P(n)\Rightarrow P(Sn)))
+\Rightarrow (\forall n.P(n))$ : il faut y penser comme la
+
+\alert{primitive récursion} d'une fonction, qui à $c \in A_0$ et
+$f\colon \mathbb{N} \times A_n \to A_{n+1}$ associe la suite $u_n \in
+\prod_{n\in\mathbb{N}} A_n$ définie par $u_0 = c$ et $u_{n+1} =
+f(n,u_n)$, ou en OCaml
+
+\smallskip
+
+{\footnotesize\tt
+let recurr = fun c -> fun f -> let rec u = fun n -> if n==0 then c
+else f (n-1) (u (n-1)) in u ;;\\
+{\color{purple}val recurr : 'a -> (int -> 'a -> 'a) -> int -> 'a = <fun>}
+\par}
+
+\smallskip
+
+…mais avec un type qui permet à chaque $u_n$ d'être dans un $A_n$
+différent : $A_0 \rightarrow (\prod_n\,(A_n\rightarrow A_{n+1}))
+\rightarrow (\prod_n\,A_n)$.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Curry-Howard pour l'arithmétique de Heyting (2)}
+
+\textcolor{brown}{À quoi ressemble le programme associé à une preuve
+  dans l'arithmétique de Heyting ?}
+
+\medskip
+
+On peut souvent s'en faire une idée d'après son type, p.ex. :
+\begin{itemize}
+\item La commutativité de la multiplication $\forall m.\forall
+  m.(m\times n = n\times m)$ prend $m$ et $n$ et un renvoie un
+  témoignage d'égalité de $m\times n$ et $n\times m$ (c'est-à-dire en
+  fait $m\times n$ calculé de deux manières différentes).
+\item La preuve de $\forall n. (n=0 \lor \neg n=0)$ donnée
+  transp. \ref{example-proof-in-heyting-arithmetic} prend en entrée
+  $n$ et renvoie un type somme avec soit un témoignage d'égalité de
+  $n$ à $0$ soit un programme qui donné un tel témoignage renvoie qqch
+  d'impossible.  Donc en pratique, ce programme prend $n$ et teste si
+  $n=0$.
+\item Une preuve de $\forall m.\exists n. P(m,n)$ va correspondre à un
+  programme qui prend $m$ et renvoie $n$ ainsi qu'un témoignage de
+  $P(m,n)$.
+\end{itemize}
+
+\medskip
+
+Notamment, \alert{si} $\forall m.\exists n. P(m,n)$ est prouvable dans
+l'arithmétique de \alert{Heyting}, \alert{alors} on peut en déduire
+$\varphi_e$ générale récursive telle que $\forall
+m. P(m,\varphi_e(m))$ (\textbf{extraction} de programme à partir de la
+preuve).
+
+\end{frame}
+%
 \end{document}