diff options
| -rw-r--r-- | exercices-inf110.tex | 53 |
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 |