From 76f109e88de483f99b59b6f959c4bcb1e576b1bc Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Mon, 8 Jan 2024 19:32:42 +0100 Subject: More about first-order arithmetic. --- transp-inf110-03-quantif.tex | 115 +++++++++++++++++++++++++++++++++++++++++-- 1 file 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 @@ -1334,6 +1335,112 @@ chose comme ceci : $\mathsf{recurr}^{(\lambda k.(k=0 \lor \neg $P(0) \Rightarrow \penalty100 (\forall n.(P(n)\Rightarrow P(Sn))) \Rightarrow \penalty100 (\forall n.P(n))$.\par} +\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 = } +\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} -- cgit v1.2.3