summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--transp-inf110-03-quantif.tex6
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}