summaryrefslogtreecommitdiffstats
path: root/transp-inf110-02-typage.tex
diff options
context:
space:
mode:
Diffstat (limited to 'transp-inf110-02-typage.tex')
-rw-r--r--transp-inf110-02-typage.tex9
1 files changed, 8 insertions, 1 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 19bc7ae..8479808 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -4398,7 +4398,7 @@ $\mathcal{P}(\mathbb{N})$ des parties de $\mathbb{N}$ :
\item $P \dottedland Q = \{\langle m,n\rangle : m\in P, n\in Q\}$
(codage de Gödel du produit $P\times Q$)
\item $P \dottedlor Q = \{\langle 0,m\rangle : m\in P\} \cup \{\langle
- 1,n\rangle : m\in Q\}$ (sorte de réunion disjointe)
+ 1,n\rangle : n\in Q\}$ (sorte de réunion disjointe)
\item $(P \dottedlimp Q) = \{e \in \mathbb{N} : \Phi_e(P){\downarrow}
\subseteq Q\}$, ce qui signifie $\forall m\in P.\,
\Phi_e(m){\downarrow}\in Q$ (programmes définis sur tout $P$ et
@@ -4510,6 +4510,13 @@ s'agirait de trouver un \alert{même} entier qui \alert{quel que soit
la forme $\langle 1,n\rangle$ si $P=\varnothing$. Visiblement c'est
impossible (sans information sur $P$) !
+\smallskip
+
+{\footnotesize\textbf{Remarque :} en fait, si $\varphi\lor\psi$ est
+ réalisable, l'une de $\varphi$ ou $\psi$ l'est (selon que l'entier
+ réalisant $\varphi\lor\psi$ est de la forme $\langle 0,m\rangle$ ou
+ $\langle 1,m\rangle$).\par}
+
\medskip
\itempoint La formule $\neg\neg A \Rightarrow A$ n'est pas