Énoncé

EX 1.

1.

Dans $N{K}_0$ :

Donc :

L’idée, c’est qu’on peut appliquer la loi de De Morgan au niveau de la sémantique :

On veut prouver par l’absurde (avec $𝒞$) que $\neg \neg (A\vee \neg A)$, i.e

Or, si on se donne $\neg (A\vee \neg A)$, on se donne (De Morgan) $\neg \neg A$ et $\neg A$. Pour prouver $\mathrm{\perp }$, on n’a qu’à donner $\neg A$ en argument (prémisse) de $\neg \neg A=\neg A⟶\mathrm{\perp }$.

2.

EX 2

1.

Par induction structurelle sur $F$, on montre que $F\models F^{\neg \neg }$ et $F^{\neg \neg }\models F$, puis on conclut par complétude.

2.

a).

Si $u:F$,

b).

Si $u:F⟹G,v:\neg G$,

c).

Si $u:\neg \neg \neg F$,

d).

Si $u:\neg \neg (F⟹G),v:\neg \neg F$,

3.

• Si $F=A$ ou $F=\mathrm{\perp }$ est atomique :

  $$\begin{array}{c}{u}_A\stackrel{\scriptscriptstyle\mathrm{def}}{=}𝜆x_A.x^{-}:A⟹\neg \neg A\\ v_A\stackrel{\scriptscriptstyle\mathrm{def}}{=}𝜆x_{\neg \neg A}.𝒞(x):\neg \neg A⟹A\end{array}$$

• Puis : récurrence simultanée sur ${\bullet }^{\circ }$ et ${\bullet }^{\neg \neg }$