summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorDavid A. Madore <david+git@madore.org>2023-12-15 18:22:55 +0100
committerDavid A. Madore <david+git@madore.org>2023-12-15 18:22:55 +0100
commit98caa0b4b6ec6161334699bbd91488eff78dc535 (patch)
treec969b2a0e472578b78e4e49bf245ca57082611d8
parent88c2c12c57568de9edac5ff2775aab7bb0ebf287 (diff)
downloadinf110-lfi-98caa0b4b6ec6161334699bbd91488eff78dc535.tar.gz
inf110-lfi-98caa0b4b6ec6161334699bbd91488eff78dc535.tar.bz2
inf110-lfi-98caa0b4b6ec6161334699bbd91488eff78dc535.zip
Note the disjunction property for realizability semantics.
-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