From 9e00a04747f4096b53e1a1c67609150266b6acda Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Fri, 5 Dec 2025 19:47:27 +0100
Subject: Various updates (mostly typos/thinkos, but also phase out
 "tautology").

---
 transp-inf110-02-typage.tex | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 71547c7..0694479 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -870,7 +870,7 @@ $\sigma_1,\ldots,\sigma_k$ :
 \itempoint Un \textbf{préterme} du $\lambda$CST est (inductivement) :
 \begin{itemize}
 \item une \textbf{variable de terme} ($a$, $b$, $c$... en nombre illimité),
-\item une \textbf{application} $(PQ)$ où $P$ et $Q$ sont deux termes,
+\item une \textbf{application} $(PQ)$ où $P$ et $Q$ sont deux prétermes,
 \item une \textbf{abstraction} $\lambda(v:\sigma).E$ avec $v$
   variable, $\sigma$ type et $E$ préterme.
 \end{itemize}
@@ -1396,7 +1396,7 @@ En français, et un peu informellement :
 \item pour introduire $\land$ : on démontre $Q_1$ et $Q_2$, ce qui
   donne $Q_1\land Q_2$ ; pour l'éliminer : si on a $Q_1 \land Q_2$ on
   en tire $Q_1$ resp. $Q_2$ ;
-\item pour introduire $\lor$ : on démontre $Q_1$ et $Q_2$, ce qui
+\item pour introduire $\lor$ : on démontre $Q_1$ ou $Q_2$, ce qui
   donne $Q_1\lor Q_2$ ;
 \item pour éliminer $\lor$ : si on a $P_1 \lor P_2$, on démontre $Q$
   successivement sous les hypothèses $P_1$ et $P_2$, ce qui donne $Q$
@@ -1593,17 +1593,17 @@ Présentation « drapeau », plus proche de l'écriture naturelle, commode
 \end{frame}
 %
 \begin{frame}
-\frametitle{Quelques tautologies du calcul propositionnel intuitionniste}
+\frametitle{Quelques théorèmes du calcul propositionnel intuitionniste}
 
 \itempoint Lorsque $\vdash P$ (sans hypothèse), on dit que $P$ est
 \textbf{valable} dans le calcul propositionnel intuitionniste, ou est
-une \textbf{tautologie} de celui-ci.
+un \textbf{théorème} / une \textbf{tautologie}.
 
 \medskip
 
 {\footnotesize
 
-Quelques tautologies importantes (« $P\Leftrightarrow Q$ » abrège
+Quelques théorèmes importants (« $P\Leftrightarrow Q$ » abrège
 « $P \Rightarrow Q$ et $Q \Rightarrow P$ ») :
 
 \begin{tabular}{|c|c|}
@@ -1655,14 +1655,14 @@ $\neg(A\land\neg A)$&$\neg\neg(A\lor\neg A)$\\
 \end{frame}
 %
 \begin{frame}
-\frametitle{Quelques non-tautologies}
+\frametitle{Quelques non-théorèmes}
 
 {\footnotesize Rappelons qu'\textcolor{blue}{on ne permet pas de
     raisonnement par l'absurde} dans notre logique.\par}
 
 \bigskip
 
-Les énoncés suivants \alert{ne sont pas} des tautologies du calcul
+Les énoncés suivants \alert{ne sont pas} des théorèmes du calcul
 propositionnel intuitionniste (même s'ils \emph{sont} valables en
 calcul propositionnel \emph{classique}) :
 \begin{itemize}
@@ -1686,7 +1686,7 @@ calcul propositionnel \emph{classique}) :
 \bigskip
 
 {\footnotesize\textcolor{brown}{Mais comment sait-on que quelque chose
-    \emph{n'est pas} une tautologie, au juste ?}\par}
+    \emph{n'est pas} un théorème, au juste ?}\par}
 
 \end{frame}
 %
@@ -1758,14 +1758,14 @@ La logique \textbf{classique} ou \textbf{booléenne} modifie la règle
 
 \bigskip
 
-Elle est donc \alert{plus forte} (= a plus de tautologies) que la
+Elle est donc \alert{plus forte} (= a plus de théorèmes) que la
 logique intuitionniste.
 
 \bigskip
 
 \itempoint\textbf{Théorème} {\footnotesize (« complétude de la
   sémantique booléenne du calcul propositionnel classique »)} : $P$
-est une tautologie de la logique classique \alert{ssi} pour toute
+est un théorème de la logique classique \alert{ssi} pour toute
 substitution de $\bot$ ou $\top$ à chacune des variables
 propositionnelles de $P$ a la valeur de vérité $\top$.  (Voir
 transp. \ref{truth-table-semantics} plus loin pour précisions.)
@@ -1917,8 +1917,8 @@ Que penser de la preuve suivante ?
 \textbf{Affirmation :} Il existe un algo qui donné $k \in
 \mathbb{N}$ \alert{termine en temps fini} et renvoie
 \begin{itemize}
-\item soit le rang de la première occurrence de $k$ chiffres $7$ dans
-  l'écriture décimale de $\pi$,
+\item soit le rang de la première occurrence de $k$ chiffres $7$
+  consécutifs dans l'écriture décimale de $\pi$,
 \item soit « $\infty$ » si une telle occurrence n'existe pas.
 \end{itemize}
 
@@ -2527,13 +2527,13 @@ après substitution).
 \medskip
 
 \itempoint Conséquence côté logique : substituer des propositions
-quelconques aux \alert{variables propositionnelles} d'une tautologie
-donne encore une tautologie.
+quelconques aux \alert{variables propositionnelles} d'un théorème
+donne encore un théorème.
 
 \medskip
 
 P.ex. : $(A\land B\Rightarrow C) \Rightarrow (A\Rightarrow
-B\Rightarrow C)$ est une tautologie, donc
+B\Rightarrow C)$ est un théorème, donc
 \[
 ((D\Rightarrow E)\land (E\Rightarrow D) \Rightarrow D) \Rightarrow ((D\Rightarrow E)\Rightarrow (E\Rightarrow D)\Rightarrow D)
 \]
@@ -2690,7 +2690,7 @@ dans une formule et on obtient ainsi une formule équivalente.
 
 \itempoint Le \textbf{calcul des séquents} est une autre présentation
 de la (même) logique propositionnelle intuitionniste (mêmes
-tautologies, mêmes séquents).
+théorèmes, mêmes séquents).
 
 \medskip
 
-- 
cgit v1.2.3