diff options
| author | David A. Madore <david+git@madore.org> | 2023-12-18 19:58:36 +0100 |
|---|---|---|
| committer | David A. Madore <david+git@madore.org> | 2023-12-18 19:58:36 +0100 |
| commit | 3a30427b2c8696e8a2e19a34bb9dde4f8e2ea865 (patch) | |
| tree | a11926744232533bf0f58843fb06d973d9d67e67 | |
| parent | 854d1d8643763442a8be0bcde8aba4a0e7a0fb07 (diff) | |
| download | inf110-lfi-3a30427b2c8696e8a2e19a34bb9dde4f8e2ea865.tar.gz inf110-lfi-3a30427b2c8696e8a2e19a34bb9dde4f8e2ea865.tar.bz2 inf110-lfi-3a30427b2c8696e8a2e19a34bb9dde4f8e2ea865.zip | |
Slight clarification.
| -rw-r--r-- | transp-inf110-03-super.tex | 7 |
1 files changed, 4 insertions, 3 deletions
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} % |