DM : QBF et la logique intuitionniste

DM de Logique

Younesse Kaddar

I. De QBF à la logique intuitionniste

Le lemme suivant sera récurremment utilisé dans la suite :

Lemme Introductif : Si $𝜑$ est une formule QBF et $I⊆𝒫$ :

\[I \, ∩ (fv(𝜑)∪bv(𝜑)) \overset{\tiny QBF}{\vDash} 𝜑 ⟺ I \overset{\tiny QBF}{\vDash} 𝜑\]

Preuve : Par induction structurelle sur $𝜑$ :

  • Si $𝜑=\bot$ (resp. $𝜑=\top$) : cela revient à montrer l’équivalence de deux propositions fausses (resp. vraies), c’est immédiat.

  • Si $𝜑 = p ∈𝒫$ : Pour tout $I⊆𝒫$ :

    \[\begin{align*} &\quad I \, ∩ (\underbrace{fv(𝜑)∪bv(𝜑)}_{= \lbrace p \rbrace}) \overset{\tiny QBF}{\vDash} p \\ ⟺ &\quad p∈ I \, ∩ \lbrace p \rbrace \\ ⟺ &\quad p∈ I \\ ⟺ &\quad I \overset{\tiny QBF}{\vDash} p \end{align*}\]

  • Si $𝜑 = ¬𝜓$ : Pour tout $I⊆𝒫$ :

    \[\begin{align*} &\quad I \, ∩ (fv(𝜑)∪bv(𝜑)) \overset{\tiny QBF}{\vDash} 𝜑 \\ ⟺ &\quad I \, ∩ (fv(𝜑)∪bv(𝜑)) \overset{\tiny QBF}{\not\vDash} 𝜓 \\ ⟺ &\quad I \overset{\tiny QBF}{\not\vDash} 𝜓 &&\text{ (par hypothèse d'induction)} \\ ⟺ &\quad I \overset{\tiny QBF}{\vDash} ¬𝜓 = 𝜑 \end{align*}\]

  • Si $𝜑 ∈ \lbrace 𝜑_1 ∧ 𝜑_2, 𝜑_1 ∨ 𝜑_2, 𝜑_1 ⟶ 𝜑_2 \rbrace$ : Le résultat découle directement de l’application de l’hypothèse d’induction à $𝜑_1$ et $𝜑_2$

  • Si $𝜑 = ∀p. 𝜓$ (resp. $𝜑 = ∃p. 𝜓$) :

    \[\begin{align*} &&\quad I \, ∩ (fv(𝜑)∪ bv(𝜑)) \overset{\tiny QBF}{\vDash} 𝜑 \\ ⟺ &&\quad \underbrace{\Big(I \, ∩ (\underbrace{fv(𝜑)∪bv(𝜑)}_{= \lbrace p \rbrace ∪ fv(𝜓)∪bv(𝜓)}) \Big) \backslash \lbrace p \rbrace}_{= \Big(I\backslash \lbrace p \rbrace\Big) ∩ \big(fv(𝜓)∪ bv(𝜓)\big) } \overset{\tiny QBF}{\vDash} 𝜓 \\ &\text{ et (resp. ou) }& I \, ∩ (fv(𝜑)∪bv(𝜑)) ∪ \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \\ \\ ⟺ &&\quad I\backslash \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 &&\text{ (par hypothèse d'induction)}\\ &\text{ et (resp. ou) }& I \, ∩ \Big(\lbrace p \rbrace ∪ fv(𝜓)∪bv(𝜓)\Big) ∪ \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \\ \\ ⟺ &&\quad I\backslash \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \\ &\text{ et (resp. ou) }& \bigg(I \, ∩ \Big(\lbrace p \rbrace ∪ fv(𝜓)∪bv(𝜓)\Big) ∪ \lbrace p \rbrace \bigg) ∩ \big(fv(𝜓)∪ bv(𝜓)\big) \overset{\tiny QBF}{\vDash} 𝜓 &&\text{ (par hypothèse d'induction)}\\ \\ ⟺ &&\quad I\backslash \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \\ &\text{ et (resp. ou) }& \underbrace{\bigg(\Big( I \, ∩ \big(fv(𝜓)∪ bv(𝜓)\big)\Big) ∪ \overbrace{\Big(I \, ∩ \lbrace p \rbrace\Big) ∪ \lbrace p \rbrace}^{= \lbrace p \rbrace} \bigg) ∩ \big(fv(𝜓)∪ bv(𝜓)\big)}_{= \Big( I \, ∩ \big(fv(𝜓)∪ bv(𝜓)\big)\Big) ∪ \Big( \lbrace p \rbrace ∩ \big(fv(𝜓)∪ bv(𝜓)\big)\Big) = \big( I \, ∪ \, \lbrace p \rbrace \big)∩ \big(fv(𝜓)∪ bv(𝜓)\big) } \overset{\tiny QBF}{\vDash} 𝜓 \\ ⟺ &&\quad I\backslash \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \\ &\text{ et (resp. ou) }& I \, ∪ \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 &&\text{ (par hypothèse d'induction)}\\ ⟺ &&\quad I \overset{\tiny QBF}{\vDash} 𝜑 \end{align*}\]

Donc le résultat est acquis.

NB :

  • L’induction structurelle sur une formule QBF $𝜑$ est entendue comme étant :

    • l’induction structurelle sur $𝜑$ si $𝜑∈{\cal F}_0$ n’a pas de quantificateurs
    • l’induction sur le nombre de quantificateurs $𝜑$ en a

    En d’autres termes, la syntaxe d’une formule QBF peut-être définie par la grammaire suivante (sur laquelle l’induction structurelle est faite) :

    \[\begin{align*} S &⟶ p \mid ⊥ \mid ⊤ &&\text{(pour } p∈𝒫 \text{)}\\ F_0 &⟶ ¬ F_0 \mid F_0 ∨ F_0 \mid F_0 ∧ F_0 \mid F_0 → F_0 \mid S \\ QBF &⟶ ∀p.QBF \mid ∃p.QBF \mid ∀p.F_0 \mid ∃p.F_0 &&\text{(pour } p∈𝒫 \text{)} \end{align*}\]

  • Intuitivement, ce lemme signifie que si $𝜑$ ne contient pas la variable $p$, alors rajouter ou non $p$ à une interprétation donnée ne change rien au fait que cette interprétation statisfasse $𝜑$ ou non.

  • Un lemme analogue (plus simple à démontrer, puisqu’il n’y a pas à considérer les quantificateurs) peut être démontré pour la logique intuitionniste.

1.

Scolie : Pour toute formule QBF $𝜑$, pour toute $p ∈ bv(𝜑)$, et pour toute $q ∈ 𝒫 \backslash (bv(𝜑) ∪ fv(𝜑))$, $𝜑$ est équivalente à la $𝜑[p←q]$, où $𝜑$ est la formule QBF obtenue à partir de $𝜑$ en remplaçant $p$ par $q$.

Preuve : par induction structurelle sur $𝜑$.

  • Cas de base : si $𝜑∈{\cal F}_0(𝒫)$ :

    c’est immédiat puisque $bv(𝜑) = ∅$

  • Hérédité : si $𝜑 ≝ Qp.𝜓$ (avec les notations de l’énoncé) :

    alors

    • $𝜑[p←q] ≝ Qq.𝜓[p←q]$
    • on montre par une induction structurelle immédiate sur $𝜓$ que toute interprétation $I ⊆ 𝒫$ vérifie $I ∪ \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \, \Big( \text{ resp. } I \backslash \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \Big)$ dès que $I ∪ \lbrace q \rbrace \overset{\tiny QBF}{\vDash} 𝜓[p←q] \, \Big( \text{ resp. } I \backslash \lbrace q \rbrace \overset{\tiny QBF}{\vDash} 𝜓[p←q] \Big)$, et la réciproque se montre de manière analogue.

    Il découle donc ainsi que :

    • Si $Q = ∀$ : $\Big(I ∪ \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \, \text{ et } I \backslash \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓\Big) \text{ ssi } \Big(I ∪ \lbrace q \rbrace \overset{\tiny QBF}{\vDash} 𝜓[p←q] \, \text{ et } I \backslash \lbrace q \rbrace \overset{\tiny QBF}{\vDash} 𝜓[p←q]\Big)$
    • Si $Q = ∃$ : $\Big(I ∪ \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \, \text{ ou } I \backslash \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \Big) \text{ ssi } \Big(I ∪ \lbrace q \rbrace \overset{\tiny QBF}{\vDash} 𝜓[p←q] \, \text{ ou } I \backslash \lbrace q \rbrace \overset{\tiny QBF}{\vDash} 𝜓[p←q] \Big)$ Dans tous les cas : le résultat est acquis.

Soit $𝜑$ une formule QBF.

Montrons que $𝜑$ est équivalente à une formule QBF bien quantifiée, par induction sur le nombre de quantificateurs $n$ de $𝜑$.

  • Cas de base : si $n=0$

    alors $𝜑∈{\cal F}_0(𝒫)$, et $𝜑$ est clairement bien quantifiée, puisqu’elle n’a pas de sous-formule de la forme $Qp.𝜓$

  • Hérédité : si $𝜑 ≝ Qp.𝜓$ où $Q∈ \lbrace ∀, ∃ \rbrace$ a $n>0$ quantificateurs et est bien quantifiée :

    alors

    • $p ∉ bv(𝜓)$ ($𝜑$ est bien quantifiée)
    • $𝜓$ est une formule QBF bien quantifiée (puisque $𝜑$ l’est) à $n-1$ quantificateurs, donc par hypothèse d’induction : $𝜓$ est équivalente à une formule QBF $𝜓’$ bien quantifiée.

    • Comme $𝒫$ est infini, il existe $𝒫 \backslash (bv(𝜓’) ∪ fv(𝜓’)) \ni q ≠ p$.

      Quitte à considérer $𝜓’[p←q]$, qui reste bien quantifiée (car $q ∉ bv(𝜓’) ∪ fv(𝜓’)$) et est équivalente à $𝜓’$ si $p∈bv(𝜓’)$ (par la scolie), on peut supposer que $p∉bv(𝜓’)$ (l’équivalence des formules QBF est une relation d’équivalence (et est donc transitive)).

    Soit $I ⊆ 𝒫$. Montrons que

    \[I \overset{\tiny QBF}{\vDash} 𝜑 = Qp.𝜓 ⟺ I \overset{\tiny QBF}{\vDash} Qp.𝜓' ≝ 𝜑'\]

    • $⟹$ :

      Si $I ∪ \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \, \Big( \text{ resp. } I \backslash \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓 \Big)$, alors $I ∪ \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓’ \, \Big( \text{ resp. } I \backslash \lbrace p \rbrace \overset{\tiny QBF}{\vDash} 𝜓’ \Big)$ par équivalence de $𝜓$ et $𝜓’$.

      Donc que $Q$ vaille $∀$ ou $∃$, on vérifie bien que si $I \overset{\tiny QBF}{\vDash} Qp.𝜓$, alors $I \overset{\tiny QBF}{\vDash} Qp.𝜓’$.

    • $⟸$ : se montre de la même manière.

    Comme $𝜑’ = Qp.𝜓’$ est bien quantifiée (puisque $𝜓’$ l’est et $p∉bv(𝜓’)$), le résultat est donc acquis.

On a montré que :

Toute formule QBF est logiquement équivalente à une formule QBF bien quantifiée.

2.

Par induction sur le nombre de quantificateurs $n$ de $𝜑$, montrons que :

Pour tous $I ⊆ 𝒫$, $𝒦 ≝ (W, ≤_𝒦, α_𝒦)$, $𝜑$ bien quantifiée telle que $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$ :

si $I \overset{\tiny QBF}{\vDash} 𝜑$ et $𝒦$ force $I$ sur $𝒫 \backslash (bv(𝜑) ∪ 𝒬)$ alors pour tout $w ∈ W, 𝒦, w \overset{\tiny KPK}{\vDash} 𝜑^\ast$

NB : Comme $𝜑^\ast$ n’est pas définie dans le cas contraire, on fera l’hypothèse que $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$

Cas de base : si $n=0, 𝜑∈{\cal F}_0(𝒫)$ :

Soient $I ⊆ 𝒫$, $𝒦 ≝ (W, ≤_𝒦, α_𝒦)$ un modèle de Kripke, $𝜑$ une formule QBF de ${\cal F}_0(𝒫)$ telle que $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$.

Supposons que $I \overset{\tiny QBF}{\vDash} 𝜑$, i.e $I \overset{\tiny CL}{\vDash} 𝜑$, et que $𝒦$ force $I$ sur $𝒫 \backslash (\underbrace{bv(𝜑)}_{=∅} ∪ 𝒬) = 𝒫 \backslash 𝒬$.

Soit $w ∈ W$.

Pour toute $p ∈ 𝒫 \backslash 𝒬$,

  • $p∈I ⟹ 𝒦, w \overset{\tiny KPK}{\vDash} p$
  • $p∉I ⟹ ∀w’≥w, 𝒦, w’ \overset{\tiny KPK}{\not\vDash} p$

D’où en particulier :

\[∀p ∈ 𝒫 \backslash 𝒬, \, \, p∈I ⟺ 𝒦, w \overset{\tiny KPK}{\vDash} p ⟺ p ∈ α_𝒦(w)\]

Donc comme $I, α_𝒦(w) ⊆ 𝒫$ , il vient que :

\[I\backslash 𝒬 = α_𝒦(w)\backslash 𝒬\]

Montrons que : si

  • $I \overset{\tiny CL}{\vDash} 𝜑$
  • $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$

alors $w \overset{\tiny KPK}{\vDash} 𝜑^\ast = 𝜑$, par induction sur la taille $\vert 𝜑 \vert$ de $𝜑$ :

Cas de base : $\vert 𝜑 \vert=1$

  • $𝜑 = \top$ : c’est immédiat.
  • $𝜑 = \bot$ : ce cas est exclus puisque $I \overset{\tiny CL}{\vDash} 𝜑$

  • $𝜑∈𝒫$ :

    comme

    • $(\underbrace{fv(𝜑)}{=\lbrace 𝜑 \rbrace} ∪ \underbrace{bv(𝜑)}{=∅}) ∩ 𝒬 = ∅$, d’où $𝜑∉ 𝒬$
    • et $𝜑 ∈ I$ (car $I \overset{\tiny CL}{\vDash} 𝜑$)

    il vient que $𝜑 ∈ I\backslash 𝒬 = α_𝒦(w)\backslash 𝒬 ⊆ α_𝒦(w)$, soit $w \overset{\tiny KPK}{\vDash} 𝜑$

Hérédité : $\vert 𝜑 \vert>1$

  • $𝜑 = 𝜑_1 ∧ 𝜑_2$ ou $𝜑 = 𝜑_1 ∨ 𝜑_2$ : le résultat découle directement de $I \overset{\tiny CL}{\vDash} 𝜑$ et de l’application de l’hypothèse d’induction à $𝜑_1$ et $𝜑_2$

  • $𝜑 = 𝜑_1 ⟶ 𝜑_2$ :

    Soit $w’ ≥ w$ tel que $w’ \overset{\tiny KPK}{\vDash} 𝜑_1$. Montrons que $w’ \overset{\tiny KPK}{\vDash} 𝜑_2$.

    • Cas 1 : $I \overset{\tiny CL}{\vDash} 𝜑_1$ :

      Comme $I \overset{\tiny CL}{\vDash} 𝜑$, alors $I \overset{\tiny CL}{\vDash} 𝜑_2$, et d’après l’hypothèse d’induction : $w \overset{\tiny KPK}{\vDash} 𝜑_2$. Donc par monotonicité : $w’ \overset{\tiny KPK}{\vDash} 𝜑_2$

    • Cas 2 : $I \overset{\tiny CL}{\not\vDash} 𝜑_1$, i.e $I \overset{\tiny CL}{\vDash} ¬ 𝜑_1$ :

      Comme $\vert ¬ 𝜑_1 \vert < \vert 𝜑 \vert$, on peut appliquer l’hypothèse d’induction à $¬ 𝜑_1$ : il vient que $w \overset{\tiny KPK}{\vDash} ¬ 𝜑_1$. Donc par définition sémantique : $w’ \overset{\tiny KPK}{\not\vDash} 𝜑_1$, ce qui contredit notre hypothèse : ce cas est exclus.

  • $𝜑 = ¬ 𝜓$ :

    Soit $w’ ≥ w$. Montrons que $w’ \overset{\tiny KPK}{\not\vDash} 𝜓$. Sachant qu’on sait que $I \overset{\tiny CL}{\not\vDash} 𝜓$, le résultat sera acquis si on montre la contraposée :

    \[w' \overset{\tiny KPK}{\vDash} 𝜓 ⟹ I \overset{\tiny CL}{\vDash} 𝜓\]

    Supposons que $w’ \overset{\tiny KPK}{\vDash} 𝜓$. Alors $𝛼(w’) \overset{\tiny CL}{\vDash} 𝜓$ (on le vérifie aisément puisque les règles de la sémantique intuitioniste sont plus fortes que les règles sémantiques de la logique classique).

    Or, comme $(fv(𝜓) ∪ bv(𝜓)) ∩ 𝒬 = ∅$, il est clair que :

    \[𝛼(w')\backslash 𝒬 \overset{\tiny CL}{\vDash} 𝜓\]

    Par ailleurs : $𝛼(w’)\backslash 𝒬 \supset 𝛼(w)\backslash 𝒬 = I \backslash 𝒬$.

    Supposons, par l’absurde, que $\Big(𝛼(w’)\backslash 𝒬 \Big) \backslash \Big( I\backslash 𝒬 \Big) ≠ ∅$ : alors il existerait $p ∉I$ tel que $𝒦, w’ \overset{\tiny KPK}{\vDash} p$. Mais comme $w’≥w$, cela contredirait : $p∉I ⟹ ∀w’≥w, 𝒦, w’ \overset{\tiny KPK}{\not\vDash} p$.

    Donc $𝛼(w’)\backslash 𝒬 = I \backslash 𝒬$, et :

    \[I\backslash 𝒬 \overset{\tiny CL}{\vDash} 𝜓\]

    et comme $(fv(𝜓) ∪ bv(𝜓)) ∩ 𝒬 = ∅$ :

    \[I \overset{\tiny CL}{\vDash} 𝜓\]

    Le résultat est acquis.

Hérédité : si $𝜑 ≝ Qp.𝜓$ a $n>0$ quantificateurs :

(avec les notations de l’énoncé)

Soient $I ⊆ 𝒫$, $𝒦 ≝ (W, ≤_𝒦, α_𝒦)$ un modèle de Kripke, $𝜑 ≝ Qp.𝜓$ une formule QBF à $n>0$ quantificateurs bien quantifiée telle que $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$.

Supposons que $I \overset{\tiny QBF}{\vDash} 𝜑 = Qp.𝜓$, et que $𝒦$ force $I$ sur $𝒫 \backslash (\underbrace{bv(𝜑)}_{= \lbrace p \rbrace ∪ bv(𝜓)} ∪ 𝒬)$.

Soit $w ∈ W$.

Pour toute variable $q ∉ \lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬$,

  • $q∈I ⟹ 𝒦, w \overset{\tiny KPK}{\vDash} q$
  • $q∉I ⟹ ∀w’≥w, 𝒦, w’ \overset{\tiny KPK}{\not\vDash} q$

D’où en particulier, de même que précédemment :

$I\backslash \Big( \lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬 \Big) = α_𝒦(w)\backslash \Big( \lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬 \Big)$

On remarque par ailleurs que :

  • $p ∉ bv(𝜓)$ car $𝜑$ est bien quantifiée
  • $p∉ 𝒬$ car $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$

Montrons que $w \overset{\tiny KPK}{\vDash} 𝜑^\ast$.

Cas 1 : Si $Q=∀$

Soit $w’≥w$.

Supposons que $w’ \overset{\tiny KPK}{\vDash} p∨¬p$, i.e $w’ \overset{\tiny KPK}{\vDash} p$ ou $w’ \overset{\tiny KPK}{\vDash} ¬p$, et montrons que $w’ \overset{\tiny KPK}{\vDash} 𝜓^\ast$.

Considérons la structure de Kripke :

\[𝒦_{w'} ≝ (\lbrace w''∈W \mid w'' ≥ w' \rbrace, ≤_𝒦, 𝛼)\]

Le point clé est que, par monotonicité :

  • si $w’ \overset{\tiny KPK}{\vDash} p$ : tous les mondes de $𝒦_{w’}$ forcent $p$
  • si $w’ \overset{\tiny KPK}{\vDash} ¬p$ : tous les mondes de $𝒦_{w’}$ forcent $¬p$

On sait par ailleurs que $I ∪ \lbrace p \rbrace \overset{\tiny CL}{\vDash} 𝜓$ et $I \backslash \lbrace p \rbrace \overset{\tiny CL}{\vDash} 𝜓$

Donc :

  • si $w’ \overset{\tiny KPK}{\vDash} p$ : $𝒦_{w’}$ force $I ∪ \lbrace p \rbrace ⊆ 𝒫$ sur $𝒫\backslash \Big( bv(𝜓) ∪ 𝒬 \Big)$ puisque

    • $𝒦$ force $I$ sur $𝒫\backslash \Big( \lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬 \Big)$
    • $p ∈ I ∪ \lbrace p \rbrace$, et pour tout $w’‘≥w’$, $w’’ \overset{\tiny KPK}{\vDash} p$ par monotonicité

    et on applique l’hypothèse d’induction à $𝜓$ : par suite, pour tout $w’‘≥w’$, $w’’ \overset{\tiny KPK}{\vDash} 𝜓^\ast$.

    Le résultat est donc acquis.

  • si $w’ \overset{\tiny KPK}{\vDash} ¬ p$ : $𝒦_{w’}$ force $I \backslash \lbrace p \rbrace ⊆ 𝒫$ sur $𝒫\backslash \Big( bv(𝜓) ∪ 𝒬 \Big)$ puisque

    • $𝒦$ force $I$ sur $𝒫\backslash \Big( \lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬 \Big)$
    • $p ∉ I \backslash \lbrace p \rbrace$, et pour tout $w’‘≥w’$, $w’’ \overset{\tiny KPK}{\vDash} ¬p$ par monotonicité

    et on conclut de même en appliquant l’hypothèse d’induction à $𝜓$.

Cas 2 : Si $Q=∃$

Soit $w’≥w$.

Supposons que $w’ \overset{\tiny KPK}{\vDash} 𝜓^\ast ⟶ q_n$, et montrons que

  • $w’ \overset{\tiny KPK}{\vDash} \Big((p⟶q_n) ∨ (¬p⟶q_n)\Big)$
  • i.e $w’ \overset{\tiny KPK}{\vDash} p⟶q_n$ ou $w’ \overset{\tiny KPK}{\vDash} ¬p⟶q_n$
  • i.e $\Big($ pour tout $w’‘≥w’$ : si $w’’ \overset{\tiny KPK}{\vDash} p$ , alors $w’’ \overset{\tiny KPK}{\vDash} q_n \Big)$ OU $\Big($ pour tout $w’‘≥w’$ : si $w’’ \overset{\tiny KPK}{\vDash} ¬p$ , alors $w’’ \overset{\tiny KPK}{\vDash} q_n \Big)$

On sait par ailleurs que $I ∪ \lbrace p \rbrace \overset{\tiny CL}{\vDash} 𝜓$ ou $I \backslash \lbrace p \rbrace \overset{\tiny CL}{\vDash} 𝜓$

  • si $I ∪ \lbrace p \rbrace \overset{\tiny CL}{\vDash} 𝜓$ :

    On pose

    \[𝒦_{w'} ≝ (\underbrace{\lbrace w''∈W \mid w'' ≥ w' \text{ et } w'' \overset{\tiny KPK}{\vDash} p \rbrace}_{≝ \, W'}, ≤_𝒦, 𝛼)\]

    Il vient que $𝒦_{w’}$ force $I ∪ \lbrace p \rbrace ⊆ 𝒫$ sur $𝒫\backslash \Big( bv(𝜓) ∪ 𝒬 \Big)$ puisque

    • $𝒦$ force $I$ sur $𝒫\backslash \Big( \lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬 \Big)$
    • $p ∈ I ∪ \lbrace p \rbrace$, et pour tout $w’‘∈W’$, $w’’ \overset{\tiny KPK}{\vDash} p$

    On applique l’hypothèse d’induction à $𝜓$ : par suite, pour tout $w’‘≥w’$ tel que $w’’ \overset{\tiny KPK}{\vDash} p$, $w’’ \overset{\tiny KPK}{\vDash} 𝜓^\ast$.

    Il s’ensuit que $w’’ \overset{\tiny KPK}{\vDash} q_n$, puisque $w’ \overset{\tiny KPK}{\vDash} 𝜓^\ast ⟶ q_n$.

    On a donc montré que : pour tout $w’‘≥w’$ : si $w’’ \overset{\tiny KPK}{\vDash} p$ , alors $w’’ \overset{\tiny KPK}{\vDash} q_n$, et le résultat est acquis.

  • si $I \backslash \lbrace p \rbrace \overset{\tiny CL}{\vDash} 𝜓$ :

    On procède de la même manière, avec $𝒦_{w’} ≝ (\underbrace{\lbrace w’‘∈W \mid w’’ ≥ w’ \text{ et } w’’ \overset{\tiny KPK}{\vDash} ¬ p \rbrace}_{≝ \, W’}, ≤_𝒦, 𝛼)$, pour montrer que pour tout $w’‘≥w’$ : si $w’’ \overset{\tiny KPK}{\vDash} ¬ p$ , alors $w’’ \overset{\tiny KPK}{\vDash} q_n$.

3.

Par induction sur le nombre de quantificateurs $n$ de $𝜑$, montrons que :

Pour tous $𝜑$ bien quantifiée telle que $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$, $I ⊆ 𝒫$ :

si $I \overset{\tiny QBF}{\not\vDash} 𝜑$, alors il existe un modèle de Kripke $𝒦 ≝ (W, ≤_𝒦, α_𝒦)$ et un monde $w_0∈W$ tels que :

  • $𝒦$ force $I$ sur $𝒫 \backslash (bv(𝜑) ∪ 𝒬)$
  • $𝒦, w_0 \overset{\tiny KPK}{\not\vDash} 𝜑^\ast$

NB : Encore une fois, comme $𝜑^\ast$ n’est pas définie dans le cas contraire, on fera l’hypothèse que $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$

Cas de base : si $n=0, 𝜑∈{\cal F}_0(𝒫)$ :

Soient $I ⊆ 𝒫$, $𝜑$ une formule QBF de ${\cal F}_0(𝒫)$ telle que $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$.

Supposons que $I \overset{\tiny QBF}{\not\vDash} 𝜑$, i.e $I \overset{\tiny CL}{\not\vDash} 𝜑$.

Soit $w_0$ un monde tel que \(𝛼(w_0) ≝ I\)

On pose $𝒦 ≝ (\lbrace w_0 \rbrace, =, 𝛼)$.

$𝒦$ force $I$ sur $𝒫 \backslash (\underbrace{bv(𝜑)}_{=∅} ∪ 𝒬) = 𝒫 \backslash 𝒬$, puisque pour toute $p ∈ 𝒫 \backslash 𝒬$ :

  • $p∈I=𝛼(w_0) ⟹ 𝒦, w_0 \overset{\tiny KPK}{\vDash} p$
  • $p∉I=𝛼(w_0) ⟹ ∀w’≥w_0, 𝒦, w’ \overset{\tiny KPK}{\not\vDash} p$ (le seul monde supérieur à $w_0$ est $w_0$)

De plus :

\[𝒦, w_0 \overset{\tiny KPK}{\not\vDash} 𝜑^\ast = 𝜑\]

(on le vérifie aisément puisque $𝛼(w_0) = I\overset{\tiny CL}{\not\vDash} 𝜑$, les règles de la sémantique intuitioniste sont plus fortes que les règles sémantiques de la logique classique et $w_0$ est le seul monde de $𝒦$).

Hérédité : si $𝜑 ≝ Qp.𝜓$ a $n>0$ quantificateurs :

(avec les notations de l’énoncé)

Soient $I ⊆ 𝒫$, $𝜑 ≝ Qp.𝜓$ une formule QBF à $n>0$ quantificateurs bien quantifiée telle que $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$.

Supposons que $I \overset{\tiny QBF}{\not\vDash} 𝜑 = Qp.𝜓$.

Notons que :

  • $p ∉ bv(𝜓)$ car $𝜑$ est bien quantifiée
  • $p∉ 𝒬$ car $(fv(𝜑) ∪ bv(𝜑)) ∩ 𝒬 = ∅$

Construisons un modèle de Kripke

\[𝒦 ≝ (W, ≤_𝒦, α_𝒦)\]

qui force $I$ sur $𝒫 \backslash (\underbrace{bv(𝜑)}_{= \lbrace p \rbrace ∪ bv(𝜓)} ∪ 𝒬)$, et un monde $w_0 ∈ W$ tel que $w_0 \overset{\tiny KPK}{\not\vDash} 𝜑^\ast$

Cas 1 : Si $Q=∀$

Il vient que $I ∪ \lbrace p \rbrace \overset{\tiny CL}{\not\vDash} 𝜓$ ou $I \backslash \lbrace p \rbrace \overset{\tiny CL}{\not\vDash} 𝜓$

Si $I ∪ \lbrace p \rbrace \overset{\tiny CL}{\not\vDash} 𝜓$ :

On applique l’hypothèse d’induction à $𝜓$ et $I ∪ \lbrace p \rbrace ⊆ 𝒫$ : par suite, il existe un modèle de Kripke $𝒦 ≝ (W, ≤_𝒦, α_𝒦)$ et un monde $w_0∈W$ tels que

  • $𝒦$ force $I ∪ \lbrace p \rbrace ⊆ 𝒫$ sur $𝒫 \backslash (bv(𝜓) ∪ 𝒬)$, donc en particulier :

    • $𝒦$ force $I$ sur $𝒫 \backslash (\lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬) \quad ⊛$
    • comme $p∈I ∪ \lbrace p \rbrace$ : $∀w∈W, 𝒦, w \overset{\tiny KPK}{\vDash} p$

  • $𝒦, w_0 \overset{\tiny KPK}{\not\vDash} 𝜓^\ast$

Il vient donc que $𝒦, w_0 \overset{\tiny KPK}{\vDash} p$ et $\,𝒦, w_0 \overset{\tiny KPK}{\not\vDash} 𝜓^\ast$, d’où

\[\, 𝒦, w_0 \overset{\tiny KPK}{\not\vDash} p∨¬p ⟶ 𝜓^\ast = 𝜑^\ast\quad ⊛⊛\]

Avec $⊛$ et $⊛⊛$, le résultat est acquis.

Si $I \backslash \lbrace p \rbrace \overset{\tiny CL}{\not\vDash} 𝜓$ :

On procède de même $I \backslash \lbrace p \rbrace$ : en l’occurrence, on aura $\, 𝒦, w_0 \overset{\tiny KPK}{\vDash} ¬p$ et $\, 𝒦, w_0 \overset{\tiny KPK}{\not\vDash} 𝜓^\ast$ (ce qui implique aussi que $ 𝒦, w_0 \overset{\tiny KPK}{\not\vDash} p∨¬p ⟶ 𝜓^\ast$).

Cas 2 : Si $Q=∃$

Il vient que $I ∪ \lbrace p \rbrace \overset{\tiny CL}{\not\vDash} 𝜓$ et $I \backslash \lbrace p \rbrace \overset{\tiny CL}{\not\vDash} 𝜓$

On applique deux fois l’hypothèse d’induction : à $𝜓$ et $I \backslash \lbrace p \rbrace ⊆ 𝒫$, et à $𝜓$ et $I ∪ \lbrace p \rbrace ⊆ 𝒫$.

Par suite, il existe des modèle de Kripke

\[𝒦_{¬p} ≝ (W_{¬p}, ≤_{𝒦_{¬p}}, α_{𝒦_{¬p}}), \, 𝒦_{p} ≝ (W_p, ≤_{𝒦_{p}}, α_{𝒦_{p}})\]

et des mondes

\[w_{¬p}∈W_{¬p}, \, w_{p} ∈W_p\]

tels que

  • $𝒦_{¬p}$ force $I \backslash \lbrace p \rbrace ⊆ 𝒫$ sur $𝒫 \backslash (bv(𝜓) ∪ 𝒬)$, donc en particulier :

    • $𝒦_{¬p}$ force $I$ sur $𝒫 \backslash (\lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬)$
    • comme $p∉I \backslash \lbrace p \rbrace$ : $∀w∈W_{¬p}, 𝒦_{¬p}, w \overset{\tiny KPK}{\vDash} ¬p$

  • $𝒦_{p}$ force $I ∪ \lbrace p \rbrace ⊆ 𝒫$ sur $𝒫 \backslash (bv(𝜓) ∪ 𝒬)$, donc en particulier :

    • $𝒦_{p}$ force $I$ sur $𝒫 \backslash (\lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬)$
    • comme $p∈I ∪ \lbrace p \rbrace$ : $∀w∈W_p, 𝒦_{p}, w \overset{\tiny KPK}{\vDash} p$

  • $𝒦_p, w_{¬p} \overset{\tiny KPK}{\not\vDash} 𝜓^\ast$ et $𝒦_{¬p} \overset{\tiny KPK}{\not\vDash} 𝜓^\ast$

On pose

\[𝒦 ≝ (W_{p} ∪ W_{¬p} ∪ \lbrace w_0 \rbrace, ≤_{𝒦}, α_{𝒦})\]

où :

  • on prolonge $≤_{ 𝒦_{p} }$ et $≤_{ 𝒦_{¬p} }$ pour construire un monde $w_0$ tel que
    • \[∀w∈𝒦_{p},\quad w_0 ≤_{𝒦_{p}} w\]
    • \[∀w∈𝒦_{¬p},\quad w_0 ≤_{𝒦_{¬p}} w\]
  • \[≤_𝒦 \quad ≝ \quad ≤_{𝒦_{p}} \, ∨ \, ≤_{𝒦_{¬p}}\]
  • Quitte à le supprimer, on peut supposer que $q_n$ n’appartient à aucun des $𝛼_{𝒦_{p}}(w)$ (pour $w∈𝒦_{p}$) ni des $𝛼_{𝒦_{¬p}}(w)$ (pour $w∈𝒦_{¬p}$), puisque $q_n$ n’intervient pas dans $𝜓^\ast$ ($𝜓$ a strictement moins de $n$ quantificateurs).

    • on définit alors $𝛼_{𝒦}$ de la manière suivante :

      • $𝛼_𝒦(w_0) ≝ I \backslash \Big(bv(𝜑) ∪ \lbrace q_1, ⋯, q_{n-1}\rbrace\Big)$

      • $∀w ∈ W_p$,

        \[𝛼_𝒦(w) ≝ \begin{cases} 𝛼_{𝒦_p}(w) ∪ \lbrace q_n \rbrace \text{ si } 𝒦_p, w \overset{\tiny KPK}{\vDash} 𝜓^\ast \\ 𝛼_{𝒦_p}(w) \text{ sinon} \end{cases}\]

      • $∀w∈W_{¬p}$,

        \[𝛼_𝒦(w) ≝ \begin{cases} 𝛼_{𝒦_{¬p}}(w) ∪ \lbrace q_n \rbrace \text{ si } 𝒦_{¬p}, w \overset{\tiny KPK}{\vDash} 𝜓^\ast \\ 𝛼_{𝒦_{¬p}}(w) \text{ sinon} \end{cases}\]

NB :

  • Notons qu’ajouter $q_n$ ou non aux interprétations des mondes ne change le fait qu’ils forcent ou non $𝜓^\ast$, puisque $q_n$ n’intervient pas dans $𝜓^\ast$ ($𝜓$ a strictement moins de $n$ quantificateurs). Et par monotonicité, cet ajout laisse $𝛼_𝒦$ croissante.

  • $𝒦, w_0 \overset{\tiny KPK}{\not\vDash} 𝜓^\ast$ puisque $𝒦, w_p \text{ (resp. } w_{¬p}) \, \overset{\tiny KPK}{\not\vDash} 𝜓^\ast$, et $w_p \, \text{ (resp. } w_{¬p}) \, ≥ w_0$

  digraph {
    rankdir=BT;
    ⋯2[label="⋯"];
    ⋯3[label="⋯"];
    ⋯4[label="⋯"];
    subgraph cluster_0 {
      label = "𝒦";
      w_0; w_p; w_¬p;
    subgraph cluster_1 {
      label = "𝒦_p";
      w_p; ⋯; ⋯3;
    }
    subgraph cluster_2 {
      label = "𝒦_¬p";
      w_¬p; ⋯2; ⋯4;
    }
    }
    w_0 -> {⋯, ⋯2};
    ⋯ -> w_p -> ⋯3[style=dashed];
    ⋯2 -> w_¬p -> ⋯4[style=dashed];
  }

Dans $𝒦$, on a construit $w_0$ pour que $𝒦, w_0 \overset{\tiny KPK}{\vDash} 𝜓^\ast ⟶ q_n$ (puisque pour tous les mondes supérieurs à $w_0$, $q_n$ est satisfaite dès que $𝜓^\ast$ l’est).

En revanche,

\[𝒦, w_0 \overset{\tiny KPK}{\not\vDash} (p ⟶ q_n) ∨ (¬p ⟶ q_n)\]

puisque $w_p$ (resp. $w_{¬p}$) vérifie

  • $𝒦, w_p \overset{\tiny KPK}{\vDash} p$ (resp. $𝒦, w_{¬p} \overset{\tiny KPK}{\vDash} ¬p$)

  • $𝒦, w_p \text{ (resp. } w_{¬p}) \, \overset{\tiny KPK}{\not\vDash} 𝜓^\ast$, d’où $𝒦, w_p \text{ (resp. } w_{¬p}) \, \overset{\tiny KPK}{\not\vDash} q_n$

et contredit donc $𝒦, w_0 \overset{\tiny KPK}{\not\vDash} p ⟶ q_n$ (resp. $w_0 \overset{\tiny KPK}{\not\vDash} ¬p ⟶ q_n$).

Il apparaît donc que

\[𝒦, w_0 \overset{\tiny KPK}{\not\vDash} (𝜓^\ast ⟶ q_n) ⟶ \Big((p ⟶ q_n) ∨ (¬p ⟶ q_n)\Big) = 𝜑^\ast\]

Par ailleurs, $𝒦$ force $I$ sur $𝒫 \backslash (\lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬)$, puisque :

  • $𝒦_{¬p}$ force $I$ sur $𝒫 \backslash (\lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬)$

  • $𝒦_{p}$ force $I$ sur $𝒫 \backslash (\lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬)$

  • Pour toute variable $q ∉ \lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬$,

    • \[\begin{align*} q∈I & ⟹ q∈𝛼_𝒦(w_0) && \bigg( I \backslash \Big(\lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬\Big) ⊆ \underbrace{I \backslash \Big(bv(𝜑) ∪ \lbrace q_1, ⋯, q_{n-1}\rbrace\Big)}_{⊆ 𝛼_𝒦(w_0)} \bigg)\\ & ⟹ 𝒦, w_0 \overset{\tiny KPK}{\vDash} q\\ \end{align*}\]
    • \[\begin{align*} q∉I & ⟹ q∉𝛼_𝒦(w_0) && \bigg( 𝒫 \backslash \Big(I ∪ \lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬\Big) ⊆ 𝒫 \backslash \Big( \underbrace{ I ∪ bv(𝜑) ∪ \lbrace q_1, ⋯, q_n\rbrace}_{ \supseteq 𝛼_𝒦(w_0)} \Big) \bigg)\\ & ⟹ 𝒦, w_0 \overset{\tiny KPK}{\not\vDash} q\\ & ⟹ ∀w'≥w_0, 𝒦, w' \overset{\tiny KPK}{\not\vDash} q &&\bigg(\text{ car } 𝒦_{p} \text{ et } 𝒦_{¬p} \text{ forcent } I \text{ sur } 𝒫 \backslash (\lbrace p \rbrace ∪ bv(𝜓) ∪ 𝒬) \bigg) \end{align*}\]

Donc le résultat est acquis.

4.

Pour toute formule QBF $𝜑$, on note $\widetilde{𝜑}$ la formule bien quantifiée équivalente construite comme dans la question 1 par renommage éventuel des variables liées, vérifiant en plus $(fv(\widetilde{𝜑}) ∪ bv(\widetilde{𝜑})) ∩ 𝒬 = ∅$, ce qu’il est loisible de supposer si on n’effectue le renommage qu’avec des variables de $𝒫\backslash 𝒬$.

NB :

  • Il est alors nécessaire de supposer que $\vert 𝒫\backslash 𝒬 \vert > \vert fv(𝜑) ∪ bv(𝜑) \vert$, et ce, pour toute variable $𝜑$ : il faut donc que $𝒫\backslash 𝒬$ soit infini (hypothèse qui n’est pas faite dans l’énoncé, mais qu’il est raisonnable de faire vu le but du DM).
  • Notons que si $𝜑$ est close, $\widetilde{𝜑}$ le reste.

On pose, pour tout formule QBF $𝜑$ :

\[𝜑^\dagger ≝ (\widetilde{𝜑})^\ast\]

Montrons que

\[\overset{\tiny QBF}{\vDash} 𝜑 \quad ⟺ \quad \overset{\tiny KPK}{\vDash} 𝜑^\dagger\]

$⟸$ :

Montrons la contraposée : si il existe $I ⊆ 𝒫$ tel que $I \overset{\tiny QBF}{\not\vDash} 𝜑$, soit $I \overset{\tiny QBF}{\not\vDash} \widetilde{𝜑}$ (puisque $𝜑$ et $\widetilde{𝜑}$ sont équivalentes), alors en appliquant la question 3 à $\widetilde{𝜑}$, il existe un modèle de Kripke $𝒦 ≝ (W, ≤_𝒦, α_𝒦)$ et un monde $w_0∈W$ tels que

\[𝒦, w_0 \overset{\tiny KPK}{\not\vDash} (\widetilde{𝜑})^\ast = 𝜑^\dagger\]

Et il en résulte que $\quad \overset{\tiny KPK}{\not\vDash} 𝜑^\dagger$.

$⟹$ :

Supposons que pour tout $I ⊆ 𝒫$, $I \overset{\tiny QBF}{\vDash} 𝜑$, soit $I \overset{\tiny QBF}{\vDash} \widetilde{𝜑}$ (puisque $𝜑$ et $\widetilde{𝜑}$ sont équivalentes).

Soit $𝒦 ≝ (W, ≤_𝒦, α_𝒦)$ un modèle de Kripke.

Montrons que $∀w ∈ W, \quad 𝒦, w \overset{\tiny KPK}{\vDash} 𝜑^\ast = (\widetilde{𝜑})^\ast$.

  • S’il existe $I⊆𝒫$ tel que $𝒦$ force $I$ sur $𝒫 \backslash (bv(\widetilde{𝜑}) ∪ 𝒬)$ :

    alors comme $I \overset{\tiny QBF}{\vDash} \widetilde{𝜑}$, on applique le théorème de question 2 à $\widetilde{𝜑}$, et le résultat s’ensuit.

  • Sinon, si $𝒦$ ne force pas $I$ sur $𝒫 \backslash (bv(\widetilde{𝜑}) ∪ 𝒬)$ pour tout $I⊆𝒫$ :

    alors pour tout $I⊆𝒫$, il existe $w∈W$ et une variable $p∉ bv(\widetilde{𝜑})∪𝒬$ tels que :

    • $p∈I$ et $\underbrace{𝒦, w \overset{\tiny KPK}{\not\vDash} p}_{\text{ i.e }\; p∉𝛼_𝒦(w)}$ $\quad⊛$

    OU

    • $p∉I$ et $\underbrace{𝒦, w \overset{\tiny KPK}{\not\vDash} ¬p}_{\text{ i.e }\; ∃w’≥w;: \; p∈𝛼_𝒦(w’)}$ $\quad⊛⊛$

    Notons alors que : pour que $𝒦$ ne force pas $I$ sur $𝒫 \backslash (bv(\widetilde{𝜑}) ∪ 𝒬)$ pour tout $I⊆𝒫$, il faut et il suffit qu’il existe une variable $p∉ bv(\widetilde{𝜑})∪𝒬$ telle que :

    \[∃ w_0, w_1∈W; \; p∈𝛼_𝒦(w_0) ∧ p∉𝛼_𝒦(w_1)\]

    • La condition est nécessaire, car sinon : en posant $I_0 ≝ \lbrace p∈ 𝒫 \backslash (bv(𝜑) ∪ 𝒬) \mid ∀w∈W, \, 𝒦, w \overset{\tiny KPK}{\vDash} p \rbrace$, $𝒦$ forcerait $I$ sur $𝒫 \backslash (bv(\widetilde{𝜑}) ∪ 𝒬)$

      • en effet : toute variable $q∈𝒫 \backslash (bv(𝜑) ∪ 𝒬)$ n’appartenant pas à $I$ n’appartiendrait pas à l’interprétation d’un certain monde $w_1$, et donc n’appartiendrait à l’interprétation d’aucun autre, car sinon il existerait $w_0, w_1∈W$ tels que $q∈𝛼_𝒦(w_0) ∧ q∉𝛼_𝒦(w_1)$

    • Elle est suffisante puisqu’alors : pour tout $I⊆𝒫$, si $p∈I$, $p$ vérifie $⊛$ avec $w=w_1$, et si $p∉I$, $p$ vérifie $⊛⊛$ avec $w=w’=w_0$

    On pose alors

    \[𝒫_0 ≝ \lbrace p∈ 𝒫 \backslash (bv(\widetilde{𝜑}) ∪ 𝒬) \mid ∃ w_0, w_1∈W; \; p∈𝛼_𝒦(w_0) ∧ p∉𝛼_𝒦(w_1) \rbrace ≠ ∅\]

    Et on note $𝒦_0$ le modèle de Kripke obtenu à partir de $𝒦$ en supprimant toutes les variables appartenant à $𝒫_0$ des interprétations des mondes de $𝒦$.

    On remarque que tout monde de $𝒦$ force $(\widetilde{𝜑})^\ast$ si, et seulement si il force $(\widetilde{𝜑})^\ast$ dans $𝒦_0$, puisque toutes les variables de $(\widetilde{𝜑})^\ast$ appartiennent à $bv(\widetilde{𝜑}) ∪ 𝒬$ (et donc n’appartiennent pas à $𝒫_0$) comme $\widetilde{𝜑}$ est close.

Par l’absurde : S’il existait un monde $w$ de $𝒦$ tel que $𝒦, w \overset{\tiny KPK}{\not\vDash} (\widetilde{𝜑})^\ast$, il existerait donc aussi un monde $w_0$ de $𝒦_0$ tel que

\[𝒦_0, w_0 \overset{\tiny KPK}{\not\vDash} (\widetilde{𝜑})^\ast \quad ⊛⊛⊛\]

Or, $𝒦_0$ force $∅$ sur $𝒫 \backslash (bv(\widetilde{𝜑}) ∪ 𝒬)$, puisqu’aucune variable de $𝒫 \backslash (bv(\widetilde{𝜑}) ∪ 𝒬)$ n’appartient à une interprétation de $𝒦_0$, donc aucune variable de $𝒫 \backslash (bv(\widetilde{𝜑}) ∪ 𝒬)$ n’est satisfaite par un monde de $𝒦_0$.

$⊛⊛⊛$ contredit donc le théorème de la question 2 appliqué à $\widetilde{𝜑}$, $I=∅$, et $𝒦_0$.

Donc tous les mondes de $𝒦$ forcent $(\widetilde{𝜑})^\ast = 𝜑^\dagger$.

Dans tous les cas, le résultat est acquis.

Par ailleurs, on peut construire une fonction qui à toute formule QBF $𝜑$ associe $(\widetilde{𝜑})^\ast = 𝜑^\dagger$ dans $LOGSPACE$, de la manière suivante :

NB :

  • Dans un souci de simplification, on supposera qu’on peut écrire sur le ruban d’entrée : à la fin, ce ruban est recopié sur le ruban de sortie.
  • tous les compteurs utilisés seront dans une base $b≥2$, pour occuper un espace logarithmique, et chaque variable de $𝒬$ comme de $𝒫\backslash 𝒬$ sera identifiée par un bit introductif (pour indiquer si elle appartient à $𝒬$ ou à $𝒫\backslash 𝒬$) concaténé à son numéro dans l’ensemble auquel elle appartient.

Pour toute entrée $𝜑$ :

  • on compte le nombre $m$ de variables distinctes de $𝜑$, et on remplace toutes les variables appartenant à $𝒬$ par de nouvelles variables de $𝒫\backslash 𝒬$
  • Pour calculer $\widetilde{𝜑}$, il suffit de remplacer les variables liées comme décrit dans la question 1 (pour ce faire, on n’a besoin que d’écrire des numéros de $O(1)$ variables sur le ruban de travail, donc on n’occupe encore qu’un espace logarithmique)

  • Pour calculer $(\widetilde{𝜑})^\ast = 𝜑^\dagger$, on utilise la procédure décrite dans l’énoncé, en éliminant les quantificateurs de gauche à droite. Si le premier quantificateur sur le ruban d’entrée (en partant de la gauche) est :

    • $∀$, suivi d’une variable $p$, on écrit “$(p∨¬p)⟶$” devant la formule qui le suit (quitte à faire un décalage, en espace constant).
    • $∃$, suivi d’une variable $p$, on écrit “$($” avant la formule qui le suit, et “$⟶ q_n) ⟶ (p ⟶ q_n) ∨ (¬p ⟶ q_n)$” après, l’indice $n$ étant tenu à jour par un compteur.

L’espace occupé est donc logarithmique en la taille de la formule.

La fonction $𝜑 \mapsto 𝜑^\dagger$ précédemment décrite est dans $LOGSPACE$, et donc a fortiori dans $PTIME$.

II. De la logique intuitionniste à QBF

5.

\[\cfrac{\qquad }{ 𝛤 \, ∪ \lbrace 𝜑 \rbrace \vdash 𝜑} \quad (Ax)\] \[\cfrac{𝛤 \vdash 𝜑_1 \qquad 𝛤 \, ∪ \lbrace 𝜑_2 \rbrace \vdash 𝜓 \qquad 𝜑_1 ⟶ 𝜑_2 ∈ 𝛤 }{ 𝛤 \vdash 𝜓} \quad (⟶ L)\] \[\cfrac{𝛤 \, ∪ \lbrace 𝜑_1 \rbrace \vdash 𝜑_2}{ 𝛤 \vdash 𝜑_1 ⟶ 𝜑_2} \quad (⟶ R)\]

Soit $𝜑$ une formule à $m$ variables dont le seul connecteur logique est $⟶$.

Si on retire toutes les parenthèses, l’écriture syntaxique de $𝜑$ est de la forme :

\[p_1 ⟶ p_2 ⟶ ⋯ ⟶ p_m\]

où les $p_i$ sont des variables propositionnelles.

$𝜑$ est donc de taille

\[n ≝ 2m-1\]

Supposons que $\vdash_{LJ_O’} 𝜑$.

On veut borner la profondeur de l’arbre de preuve de plus petite taille (i.e ayant le moins de noeuds) de $\vdash_{LJ_O’} 𝜑$.

Dans la suite, on considérera la plus longue branche de cet arbre de plus petite taille en partant du bas (de la racine $\vdash_{LJ_O’} 𝜑$) vers le haut (vers la règle $(Ax)$) : elle est constituée d’un certain nombre d’applications de règle d’inférences de $LJ_0’$.

Observation 1 : La règle $(Ax)$ n’y est appliquée qu’une et une seule fois, et c’est la dernière règle appliquée.

Preuve : $(Ax)$ ne peut être appliquée qu’une fois au plus, et toute branche finie se termine nécessairement par cette règle.

Observation 2 : À chaque étape, l’ensemble des hypothèses est un sous-ensemble de l’ensemble des sous-formules de $𝜑$, et le but est une sous-formule de $𝜑$.

Preuve : c’est vrai au départ (l’ensemble des hypothèses est vide, le but vaut $𝜑$), et on vérifie aisément que l’invariant est conservé à chaque application d’une des règles d’inférence de $LJ_0’$.

Observation 3 : À chaque application de la règle $(⟶ R)$ ou de la règle $(⟶ L)$, l’ensemble des hypothèses croît (pour l’ordre d’inclusion ensembliste).

Preuve : c’est vrai au départ (l’ensemble des hypothèses de la racine est vide), et on vérifie aisément par induction que la propriété est vérifiée à chaque application d’une des deux règles d’inférence $(⟶ R)$ ou $(⟶ L)$ :

\[\cfrac{𝛤 \vdash 𝜑_1 \qquad 𝛤 \, ∪ \lbrace 𝜑_2 \rbrace \vdash 𝜓 \qquad 𝜑_1 ⟶ 𝜑_2 ∈ 𝛤 }{ 𝛤 \vdash 𝜓} \quad (⟶ L)\] \[\cfrac{𝛤 \, ∪ \lbrace 𝜑_1 \rbrace \vdash 𝜑_2}{ 𝛤 \vdash 𝜑_1 ⟶ 𝜑_2} \quad (⟶ R)\]

Observation 4 : À chaque application de la règle $(⟶ R)$ ou de la règle $(⟶ L)$ :

  • l’ensemble des hypothèses croît strictement

ou

  • l’ensemble des hypothèses $𝛤$ reste constant mais le but $𝜓$ (sous-formule de $𝜑$) change, et le séquent $𝛤 \vdash 𝜓$ n’apparaît plus dans la branche ultérieurement.

Preuve :

Dans le cas contraire : le même séquent apparaîtrait deux fois dans la branche : les règles intermédiaires entre ces deux occurrences seraient donc superflues, et on pourrait avoir un arbre de preuve de taille strictement plus petite en les supprimant, ce qui contredirait la minimalité de l’arbre qu’on considère.

Notons de plus qu’il y a au plus $n$ sous-formules de $𝜑$, puisque chaque sous-formule correspond à la donnée d’un sous-arbre de l’arbre syntaxique de $𝜑$, et chaque sous-arbre est déterminé de manière biunivoque par sa racine (qui est un sommet de l’arbre syntaxique de $𝜑$).

Par conséquent, d’après l’observation 2 et l’observation 4 : les règles $(⟶ L)$ et $(⟶ R)$ ne peuvent être appliquées qu’un nombre de fois inférieur à :

\[\underbrace{(n+1)}_{\substack{\text{hypothèses :} \\ \text{cardinal max. d'une suite str. croissante de } \\ \text{sous-ensembles de l'ensemble des sous-formules de } 𝜑}} × \underbrace{n}_{\substack{\text{buts :} \\ \text{nombre de } \\ \text{sous-formules de } 𝜑}}\]

La branche considérée est donc de longueur inférieure à

\[p(n) ≝ (n+1)n + \underbrace{1}_{\text{règle } (Ax) \text{ à la fin}}\]

On a montré que

Pour toute formule $𝜑$ de taille $n$ :

si $\vdash_{LJ_0’}𝜑$, alors $\; \vdash_{LJ_0’}^{p(n)} 𝜑$, avec $p(n) ≝ n^2 + n + 1$

La réciproque est évidente.

6.

J’énonce quelques idées, mais je n’ai pas le temps de les creuser :

  • Dans $entails_p^𝜑$ : une grande conjonction initiale assurera que chacun des $X_i$ (resp. $Y_i$) “représente” la sous formule $𝜓_i$ au moyen d’une équivalence (les $X_i$ représentant les hypothèses, les $Y_i$ les buts) :

    \[(X_i ⟶ 𝜓_i) ∧ (𝜓_i ⟶ X_i) ∧ (Y_i ⟶ 𝜓_i) ∧ (𝜓_i ⟶ Y_i)\]

  • Dans cette conjonction initiale, on veillera aussi à ce que les implications entre sous-formules de $𝜑$ soient conservées par cet encodage : pour tout $i$, si $𝜓_i$ s’écrit sous la forme $𝜓_{i_1} ⟶ 𝜓_{i_2}$, alors la conjonction contiendra :

    \[X_{i_1} ⟶ X_{i_2}\]

  • L’idée est d’encoder $p$ choix possibles de règles d’inférence de $(LJ_0’)$ dans $entails_p^𝜑$ (pour que la preuve résultante soit de longueur inférieure à $p$) en usant de quantificateurs :

    • une première difficulté peut être de “choisir” existentiellement une des variables $X_i$ (par exemple : la sous-formule (but) à laquelle s’appliquera la règle $(Ax)$ ou $(⟶ R)$).

      La difficulté venant du fait que les quantificateurs ne portent que sur des valeurs de vérité binaires (qu’on peut voir comme correspondant à l’activation d’un bit ou non).

      Une astuce pourrait être de se servir de $\lfloor \log n\rfloor+1$ variables muettes $p_1, ⋯, p_{\lfloor \log n\rfloor+1}$ qui serviraient à “deviner” existentiellement l’écriture binaire d’un indice $i∈⟦1,n⟧$ correspondant à $X_i$, en ajoutant les contraintes :

      \[p_i ⟶ ¬ X_j \text{ pour tout } j \text{ dont le } i\text{-ème bit dans l'écriture binaire vaut } 0\]

      Ainsi, si $n = 7$ et $p_1, p_3$ ont pour valuation “vrai”, $p_2$ a pour valuation “faux” dans l’interprétation courante : la seule variable $X_i$ qui pourra être évaluée à “vrai” en cas de satisfaction de $entails_p^𝜑$ sera $X_{1012} = X{5}$.

      \[∃p_1, ∃p_2, \ldots, ∃p_{\lfloor \log n\rfloor+1}, [⋯]\]

      forcera donc le choix d’une variable $X_i$

Leave a comment