Note the disjunction property for realizability semantics.

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