TD 9 : Révisions générales

EX 1.

Il existe des groupes non abéliens (ex : $(GL_n(𝕂), ×)$, $(ℤ/2ℤ)^2$, etc…) donc la première conséquence logique est fausse.

---

Il existe des groupes abéliens (ex : $(ℝ, +)$, $(ℤ/2ℤ)$, etc…) donc la deuxième conséquence logique est fausse.

EX 2.

1.

\[𝜑_1 ≝ (∃x, ∀y, P(x,y)) ⟶ (∀y, ∃x, P(x,y))\]

a).

Formule prénexe équivalente à $𝜑_1$ :

\[(∃x, ∀y, P(x,y)) ⟶ (∀y, ∃x, P(x,y)) \\ ≡ (∃x, ∀y, P(x,y)) ⟶ (∀y', ∃x', P(x', y')) \\ ≡ ∀x, ∃y, (P(x,y) ⟶ ∀y', ∃x', P(x', y')) \\ ≡ ∀x, ∃y, ∀y', ∃x' (P(x,y) ⟶ P(x', y'))\]

b).

Formule prénexe équivalente à $¬𝜑_1$ :

\[∃x, ∀y, ∃y', ∀x' (P(x,y) ∧ ¬ P(x', y'))\]

Forme Skolémisée :

\[∀y, ∃y', ∀x' (P(a,y) ∧ ¬ P(x', y')) \\ ≡ ∀y, ∀x' \underbrace{(P(a,y) ∧ ¬ P(x', f_{∀x' (P(a,y) ∧ ¬ P(x', y'))}(y)))}_{≝ 𝜓'_1} ≝ 𝜓_1\]

c).

$𝜓_1 = Sk(¬𝜑_1)$ et $¬𝜑_1$ sont équisatisfaisables (car $𝜑_1$ était en forme normale négative).

Et $𝜓_1$ est satisfaisable

• ssi elle a un modèle de Herbrand (car c’est une formule en forme prénexe universellement quantifiée)

• ssi $H(𝜓_1) ≝ \lbrace 𝜓’_1 𝜎 \mid 𝜎 \text{ substitution close } \rbrace$ est satisfaisable

(car pour toute $𝜎 : X ⟶ T({\cal F})$ (close) : $H, 𝜎 \vDash 𝜑 ⟺ H \vDash 𝜑𝜎$)

Or :

\[H(𝜓_1) ≝ \lbrace P(a, t_1) ∧ ¬ P(t_2, f(t_1)) \mid t_i \text{ termes clos} \rbrace\] \[𝒫 = \lbrace P \rbrace \\ {\cal F} = \lbrace f (1), a (0) \rbrace \\ T({\cal F}) = \lbrace f^n (a) \mid n ≥0 \rbrace\]

avec

• $t_1 = t_2 = a$
• $t’_1 = f(a), t’_2 = a$

alors $\lbrace P(a, a) ∧ ¬ P(a, f(a)), P(a, f(a)) ∧ P(a, f(f(a))\rbrace ⊆ H(𝜓_1)$ et

\[\lbrace P(a, a) ∧ ¬ P(a, f(a)), P(a, f(a)) ∧ P(a, f(f(a))\rbrace \text{ est insatisfiable}\]

donc $H(𝜓_1)$ aussi, et $𝜓_1$ aussi, d’où : $¬ 𝜑_1$ est insatisfiable, i.e

$𝜑_1$ est valide.