Fix small mistakes noted during lecture on 2024-01-17.

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}