A tedious exercise in using Peano's axioms.

1 files changed, 53 insertions, 0 deletions

diff --git a/exercices-inf110.tex b/exercices-inf110.tex
index f3f8ae0..8e8aec8 100644
--- a/exercices-inf110.tex
+++ b/exercices-inf110.tex
@@ -3268,6 +3268,59 @@ quantificateur universel.)
 
 \section{Arithmétique du premier ordre et théorème de Gödel}
 
+\exercice\label{exercise-zero-leftneutral}\ (${\star}$)\par\nobreak
+
+Démontrer dans l'arithmétique de Heyting que $\forall n.(0+n=n)$.
+
+\begin{corrige}
+Voici une preuve complète écrite dans le style « drapeau » :
+\bgroup\normalsize
+\begin{footnotesize}
+\begin{flagderiv}[exercise-zero-leftneutral-proof]
+\step{recurr}{(0+0=0) \Rightarrow\\\quad (\forall n.((0+n=n)\Rightarrow (0+Sn=Sn)))
+\Rightarrow\\\quad (\forall n.(0+n=n))}{Instance du schéma de récurrence}
+\step{zero-rightneutral}{\forall m.(m+0 = m)}{Un des axiomes de Peano}
+\step{recurr-start}{0+0 = 0}{$\forall$Élim sur \ref{zero-rightneutral} et $0$}
+\step{recurr-zero}{(\forall n.((0+n=n)\Rightarrow (0+Sn=Sn)))
+\Rightarrow\\\quad (\forall n.(0+n=n))}{$\Rightarrow$Élim sur \ref{recurr} et \ref{recurr-start}}
+\assume{varn}{n}{}
+\assume{rhyp}{0+n=n}{}
+\step{subst}{\forall m.\forall m'.((m=m') \Rightarrow\\\quad (0+Sn=Sm) \Rightarrow (0+Sn=Sm'))}{Instance du schéma de substitution de l'égalité}
+\step{subst-1}{\forall m'.((0+n=m') \Rightarrow\\\quad (0+Sn=S(0+n)) \Rightarrow (0+Sn=Sm'))}{$\forall$Élim sur \ref{subst} et $0+n$}
+\step{subst-2}{(0+n=n) \Rightarrow\\\quad (0+Sn=S(0+n)) \Rightarrow (0+Sn=Sn)}{$\forall$Élim sur \ref{subst-1} et $n$}
+\step{subst-3}{(0+Sn=S(0+n)) \Rightarrow (0+Sn=Sn)}{$\Rightarrow$Élim sur \ref{subst-2} et \ref{rhyp}}
+\step{plus-succ}{\forall m.\forall m'.(m+Sm' = S(m+m'))}{Un des axiomes de Peano}
+\step{plus-succ-zero}{\forall m'.(0+Sm' = S(0+m'))}{$\forall$Élim sur \ref{plus-succ} et $0$}
+\step{plus-succ-zero-n}{0+Sn = S(0+n)}{$\forall$Élim sur \ref{plus-succ-zero} et $n$}
+\step{subst-4}{0+Sn=Sn}{$\Rightarrow$Élim sur \ref{subst-3} et \ref{plus-succ-zero-n}}
+\conclude{recurr-induct}{(0+n=n)\Rightarrow (0+Sn=Sn)}{$\Rightarrow$Int de \ref{rhyp} dans \ref{subst-4}}
+\conclude{recurr-induct-univ}{\forall n.((0+n=n)\Rightarrow (0+Sn=Sn))}{$\forall$Int de \ref{varn} dans \ref{recurr-induct}}
+\step{mainconc}{\forall n.(0+n=n)}{$\Rightarrow$Élim sur \ref{recurr-zero} et \ref{recurr-induct-univ}}
+\end{flagderiv}
+\end{footnotesize}
+\egroup
+
+(On comprend pourquoi on écrit rarement de telles choses
+complètement.)  Le $\lambda$-terme correspondant est le suivant :
+$\mathsf{recurr}^{(\lambda k.(0+k=k))}\penalty500\,
+(\mathsf{defplusz}\,0)\penalty0\, (\lambda(n:\mathsf{nat}).\,
+\lambda(h:0+n=n).\penalty500\, \mathsf{subst}^{(\lambda
+  k.(0+Sn=Sk))}(0+n)\,n\,h\penalty500\,(\mathsf{defplusn}\,0\,n))$ où
+on a donné les noms aux axiomes $\mathsf{defplusz} \; : \; \forall
+m.(m+0 = m)$ et $\mathsf{defplusn} \; : \; \forall m.\forall m'.(m+Sm'
+= S(m+m'))$ et pour les instances de schémas
+$\mathsf{recurr}^{(\lambda k. P(k))}$ pour $P(0) \Rightarrow (\forall
+n.(P(n)\Rightarrow P(Sn))) \Rightarrow (\forall n.P(n))$ et
+$\mathsf{subst}^{(\lambda k. P(k))}$ pour $\forall m.\forall n.((m=n)
+\Rightarrow P(m) \Rightarrow P(n))$ (le $\lambda$ en exposant est ici
+complètement conventionnel), et enfin $\mathsf{nat}$ pour marquer le
+type des individus.  Si tant est que ce programme fasse quoi que ce
+soit, c'est une boucle prenant $n$ fois le successeur de $0$ jusqu'à
+obtenir un témoignage d'égalité de $0+n$ à $n$.
+\end{corrige}
+
+%
+
 \exercice\label{exercise-loebs-theorem}\ (${\star}{\star}{\star}{\star}$)\par\nobreak
 
 Soit $T$ une théorie logique telle