From 3a30427b2c8696e8a2e19a34bb9dde4f8e2ea865 Mon Sep 17 00:00:00 2001 From: "David A. Madore" 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