diff options
Diffstat (limited to 'transp-inf110-02-typage.tex')
| -rw-r--r-- | transp-inf110-02-typage.tex | 9 |
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 |