From e3b1f08083786d3ae30e8a1f3864f1d02338c1d3 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 8 Jan 2024 18:12:05 +0100
Subject: Start writing about first-order arithmetic.

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

diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index d2ef3ef..f2eb9e3 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -1182,6 +1182,7 @@ devient un programme de type
 \end{frame}
 %
 \begin{frame}
+\label{first-order-equality}
 \frametitle{L'égalité au premier ordre}
 
 \itempoint En général on veut travailler en logique du premier ordre
@@ -1225,6 +1226,76 @@ y.\forall z. ((x=y) \Rightarrow (y=z) \Rightarrow (x=z))$ par
 \, y \, z \, v \, u
 \]
 
+\end{frame}
+%
+\section{Arithmétique du premier ordre}
+\begin{frame}
+\frametitle{L'arithmétique de Heyting et de Peano}
+
+\itempoint L'\textbf{arithmétique du premier ordre} est une (tentative
+d')axiomatisation des entiers naturels en logique du premier ordre.
+Elle est basée sur les \textbf{axiomes de Peano} (transp. suivant).
+
+\medskip
+
+\itempoint On parle d'\textbf{arithmétique de Heyting} en logique
+intuitionniste, et \textbf{de Peano} en logique classique
+(\alert{mêmes axiomes}, seule la logique change).
+
+\medskip
+
+\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) :
+\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.
+\end{itemize}
+
+\smallskip
+
+Ils sont censés représenter le successeur ($Sn$ désigne $n+1$), la
+somme, le produit et l'exponentiation.  On omet les parenthèses comme
+d'habitude.  On peut abréger $1 = S0$ et $2 = S(S0)$, etc.
+
+\end{frame}
+%
+\begin{frame}
+\frametitle{Les axiomes de Peano}
+
+On garde les axiomes de l'égalité :
+\begin{itemize}
+\item $\forall n.(n=n)$
+\item $\forall m.\forall n.((m=n) \Rightarrow P(m) \Rightarrow P(n))$
+(schéma de substitution)
+\end{itemize}
+
+\medskip
+
+Les \textbf{axiomes de Peano} du premier ordre s'y ajoutent :
+\begin{itemize}
+\item $\forall n.\neg(Sn=0)$
+\item $\forall m.\forall n.((Sm=Sn) \Rightarrow (m=n))$
+\item $P(0) \Rightarrow (\forall n.(P(n)\Rightarrow P(Sn)))
+\Rightarrow (\forall n.P(n))$ (schéma de \alert{récurrence})
+\item $\forall m.(m+0 = m)$
+\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)$
+\end{itemize}
+
+\medskip
+
+Ci-dessus, $P(s)$ désigne une formule ayant une variable d'individu
+libre $s$ : la substitution de l'égalité et la récurrence sont des
+\alert{schémas d'axiomes} (un axiome pour chaque $P$ possible) car on
+ne peut pas quantifier sur $P$ au premier ordre.
+
 \end{frame}
 %
 \end{document}
-- 
cgit v1.2.3