diff options
| -rw-r--r-- | transp-inf110-03-quantif.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex index 08001c0..d5765a5 100644 --- a/transp-inf110-03-quantif.tex +++ b/transp-inf110-03-quantif.tex @@ -925,7 +925,7 @@ Présentation avec les seules conclusions : \assume{mainhyp}{\exists x.\forall y.B(x,y)}{} \assume{vary}{y'}{} \assume{exhyp}{x,\;\forall y.B(x,y)}{} -\step{bare}{B(x,y')}{$\forall$Élim sur \ref{exhyp} et $y$} +\step{bare}{B(x,y')}{$\forall$Élim sur \ref{exhyp} et $y'$} \step{exbare}{\exists x'.B(x',y')}{$\exists$Int sur $x$ et \ref{bare}} \conclude{extrude}{\exists x'.B(x',y')}{$\exists$Elim sur \ref{mainhyp} de \ref{exhyp} dans \ref{exbare}} \conclude{mainconc}{\forall y'.\exists x'.B(x',y')}{$\forall$Int de \ref{vary} dans \ref{extrude}} @@ -1389,7 +1389,7 @@ 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 +$f(n,\emdash)\colon 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 @@ -1720,7 +1720,7 @@ $\varphi_e(i){\downarrow}$ est vrai.) » \smallskip -Donc $\mathsf{ZFC}$ est strictement plus fort que $\mathsf{HA}$ (même +Donc $\mathsf{ZFC}$ est strictement plus fort que $\mathsf{PA}$ (même pour l'arithmétique). \end{frame} |