From 3a30427b2c8696e8a2e19a34bb9dde4f8e2ea865 Mon Sep 17 00:00:00 2001
From: "David A. Madore" <david+git@madore.org>
Date: Mon, 18 Dec 2023 19:58:36 +0100
Subject: Slight clarification.

---
 transp-inf110-03-super.tex | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'transp-inf110-03-super.tex')

diff --git a/transp-inf110-03-super.tex b/transp-inf110-03-super.tex
index 45d1e7c..76edb90 100644
--- a/transp-inf110-03-super.tex
+++ b/transp-inf110-03-super.tex
@@ -550,8 +550,8 @@ Présentation avec les seules conclusions :
 \itempoint L'introduction d'une variable d'individu libre porte en
 elle l'hypothèse que \alert{l'univers des individus est habité}
 ($\exists x. \top$).  Ce fait \alert{n'est pas prouvable} sans cette
-hypothèse.  Autrement dit : $z \vdash \exists x.\top$ (pour $z$ une
-variable quelconque) mais \alert{on n'a pas} $\vdash \exists x.\top$.
+hypothèse.  On a $z \vdash \exists x.\top$ (ici $z$ variable qcque)
+mais \alert{on n'a pas} $\vdash \exists x.\top$.
 
 \medskip
 
@@ -579,7 +579,8 @@ terme $z$ pour $t$ dans $\exists$Int) :
 \medskip
 
 \textbf{N.B.} Ces problèmes n'ont rien à voir avec la logique
-intuitionniste, ils sont identiques en logique classique.
+intuitionniste, ils sont identiques en logique classique.  On
+\alert{n'a pas} non plus $\forall x.A(x) \Rightarrow \exists x.A(x)$.
 
 \end{frame}
 %
-- 
cgit v1.2.3

