TD 13 : Satisfiabilité, Résolution, complétude

Enoncé Page 1 Enoncé Page 2
Enoncé

EX 1

L’ensemble de formules suivant est-il satisfaisable ?

\[\lbrace ∀x. Q(x, a), \\ ∀x, y, z. ¬ P(y,y)∨ ¬ P(f(a,x),z), \\ ∀x, y, z. P(z , y) ∨ P(y, f(x, b)) ∨ ¬ Q(z, a) \rbrace\]

On note $(1), (2), (3)$ respectivement les formules précédentes.

Par factorisation de $(3)$, on dérive $P(f(c, b), f(c, b)) ∨ ¬Q(c’, a)$ pour toutes constantes $c, c’ ∈ \lbrace a, b \rbrace$

Puis, par factorisation avec $(1)$, on dérive $P(f(c, b), f(c, b))$ pour toute constante $c’ ∈ \lbrace a, b \rbrace$

Par ailleurs, par résolution de $(2)$, on dérive $¬P(f(a, c’), f(a, c’))$ pour toute constante $c’ ∈ \lbrace a, b \rbrace$.

Donc avec $c’= b, c=a$ dans les formules qui précèdent, on dérive par résolution $\bot$.

Donc par correction de $Res+Fact$, on en déduit que l’ensemble est insatisfaisable.

NB : Notons que comme l’ensemble est insatisfaisable, il est nécéssaire de pouvoir en dériver $\bot$, par complétude réfutationnelle de $Res+Fact$.

EX 2

1.

Faux, prendre la théorie des ordres denses (complète, cohérente, et même récursive), ou la théorie $Th(ℕ)$ (théorie d’un modèle : cohérente et complète).

2.

Faux : prendre $Th(ℕ)$ (théorie d’un modèle : complète, mais indécidable car contient $Q$).

3.

Vrai si la théorie est saturée (supposé dans le cours), puisqu’alors elle contient $\bot$, et, partant, toutes les autres formules.

4.

Vrai :

M1 :

si on avait un modèle $M$ fini de $Q$, le graphe de la fonction “successeur” serait de la forme

  digraph {
    rankdir=BT;
    0 -> 1;
    1 -> k[style=dashed];
    k -> n[style=dashed];
    n -> k;
  }

avec

  • $k≠0$ puisque $0$ n’est pas un successeur

mais alors on n’a plus l’injectivité du successeur, puisque $k = succ(n) = succ(k-1)$

M2 :

S’il existait un modèle fini $M$ de $Q$, par le principe des tiroirs : il existerait $p>n ∈ℕ$ tel que :

\[s^n(0) = s^p(0)\]

mais alors, par injectivité du successeur :

\[0 = s^{p-n}(0)\]

absurde, puisque $0$ n’est pas un successeur.

5.

Faux : on pose

\[T_1 ≝ \lbrace \text{formules closes} \rbrace\]

$T_1$ est

  • incohérente
  • complète
  • décidable

mais $Q ⊆ T_1$ (et $Q$ est engendrée par un ensemble fini d’axiomes), mais $Q$ n’est pas décidable.

6.

Vrai : on exécute les deux machines de Turing en parallèle.

7.

On aurait envie de dire : “Vrai : deuxième théorème d’incomplétude de Gödel.”

Mais c’est plutôt “on ne sait pas” : voir l’explication dans cette partie du cours de $𝜆$-calcul de Jean Goubault-Larrecq.

Problème

1.

a).

on utilise l’axiome $(1)$ pour montrer que $s(0)≥s(0)$, d’où (par $(5)$) $s(0)≥ 0$.

Et comme d’après $(7)$ : $0 ≥ s(0)$, il vient par $(2)$ que $0 = s(0)$

b).

Par $(9)$ : $s(p(0)) = 0 = s(0)$ (avec ce qui précède), donc $p(0) ≥ 0$ (par $(4)$), et d’après $(7)$ et $(2)$ : $p(0)=0$

c).

Montrons que :

\[∀x. s(x)≥x\]

En effet :

D’après $(5)$, comme $s(x)≥s(x)$ (par $(1)$), on conclut.

Montrons que \(∀x. p(s(x)) = x\)

On sait que $∀x. p(s(x)) ≥ x$ avec $(9)$ et $(5)$.

Par $(2)$, il suffit donc de montrer que $∀x. x ≥ p(s(x))$.

Or, c’est équivalent à montrer, par $(5)$, que $∀x. s(x)≥s(x)$, ce qui est vrai par $(1)$.

d).

Par $(4)$ et $∀x. p(s(x)) = x$, on en déduit que $∀x, y. (x ≥ s(y) \leftrightarrow p(x) ≥ y)$.

On conclut, avec $(5)$, que $∀x, y. x≥y \leftrightarrow (x=y ∨ p(x)≥y)$.

e).

Montrons que :

\[∀x. x ≥ p(x)\]

En effet :

On conclut avec $(4)$ et $∀x. s(x) ≥ x$.

Par $∀x. x ≥ p(x)$ et par $∀x, y. x≥y \leftrightarrow (x=y ∨ p(x)≥y)$, on en déduit que

\[∀x, y. x≥y \leftrightarrow p(x)≥p(y)\]

f).

Par $∀x, y. x≥y \leftrightarrow p(x)≥p(y)$ et $(1)$, il suffit de montrer que $p(y)≥p(x) ∧ p(x)\not ≥ p(y) \leftrightarrow y ≥ s(x) ∧ x ≠ 0$

Or, par $(4)$ et $(5)$, $p(y)≥p(x) \leftrightarrow y ≥ x \leftrightarrow y ≥ s(x) ∨ x = y$

Donc

\[p(y)≥p(x) ∧ p(x)\not ≥ p(y) \leftrightarrow y ≥ x ∧ x \not ≥ y \\ \leftrightarrow (y ≥ s(x) ∨ x = y) ∧ x \not ≥ y \\ \leftrightarrow (y ≥ s(x)) ∧ x \not ≥ y \\ ⟶ (y ≥ s(x)) ∧ x ≠ 0\]

Réciproquement, on utilise $(1)$ et a).

2.

$ℤ∪ \lbrace +∞ \rbrace$ où $0$ est interprété comme $+∞$ en est un modèle.

3.

Non, démonstration analogue à EX 2.4)

4.

On simplifie les formules avec 1. c)

5.

En enlevant l’axiome 7, $ℤ$ est un modèle.

Pour montrer que

\[T \not \vDash 𝜙\]

on exhibe un modèle de $T$ qui ne satisfait pas $𝜙$.

Donc pour montrer que $T$ est incomplète, on veut montrer que

  • $T \not \vDash 𝜙$
  • $T \not \vDash ¬ 𝜙$, i.e. $T \vDash 𝜙$

Donc on exhibe deux modèles de $T$ : l’un ne vérifiant pas $𝜙$, l’autre vérifiant $𝜙$.

  • Pour l’axiome 8 : on prend un modèle avec un seul élément

  • Pour l’axiome 9 : on prend $ℤ ∪ \lbrace +∞ \rbrace$, où $p=s=succ$

Leave a comment