diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 71 |
1 files changed, 71 insertions, 0 deletions
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 @@ -1227,4 +1228,74 @@ y.\forall z. ((x=y) \Rightarrow (y=z) \Rightarrow (x=z))$ par \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} |