Kreisel-Putnam formula was backwards: fix this.HEADmaster

1 files changed, 5 insertions, 5 deletions

diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 4cc3b11..63300ba 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -4401,8 +4401,8 @@ intuitionniste.
 \item $(\dottedneg U \dottedlimp V_1) \dottedlor (\dottedneg U
   \dottedlimp V_2) = \mathbb{R}^2 \setminus\{(0,0)\}$
 \end{itemize}
-Ceci montre que $(\neg A \Rightarrow B_1) \lor (\neg A \Rightarrow
-B_2) \Rightarrow (\neg A \Rightarrow (B_1\lor B_2))$ (« axiome de
+Ceci montre que $(\neg A \Rightarrow (B_1\lor B_2)) \Rightarrow (\neg
+A \Rightarrow B_1) \lor (\neg A \Rightarrow B_2)$ (« axiome de
 Kreisel-Putnam ») n'est pas prouvable en logique intuitionniste (et
 \textit{a fortiori} $(C \Rightarrow B_1) \lor (C \Rightarrow B_2)
 \Rightarrow (C \Rightarrow (B_1\lor B_2))$ ne l'est pas).
@@ -4735,9 +4735,9 @@ pour le calcul propositionnel intuitionniste.
 \medskip
 
 {\footnotesize Elle n'est pas complète : p.ex., $(\neg A \Rightarrow
-  B_1) \lor (\neg A \Rightarrow B_2) \Rightarrow (\neg A \Rightarrow
-  (B_1\lor B_2))$ (Kreisel-Putnam, déjà évoqué) ou bien $((\neg\neg A
-  \Rightarrow A) \Rightarrow (A\lor\neg A)) \Rightarrow (\neg
+  (B_1\lor B_2)) \Rightarrow (\neg A \Rightarrow B_1) \lor (\neg A
+  \Rightarrow B_2)$ (Kreisel-Putnam, déjà évoqué) ou bien $((\neg\neg
+  A \Rightarrow A) \Rightarrow (A\lor\neg A)) \Rightarrow (\neg
   A\lor\neg\neg A)$ (Scott) sont Medvedev-valides mais non
   démontrables.\par}