From df53831fb15d3f0c5f05465cc9cd9e8382602679 Mon Sep 17 00:00:00 2001 From: "David A. Madore" Date: Fri, 25 Apr 2025 14:43:57 +0200 Subject: Kreisel-Putnam formula was backwards: fix this. --- transp-inf110-02-typage.tex | 10 +++++----- 1 file 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} -- cgit v1.2.3