EX 1

• Entrée : une formule $𝜑$ sur $\mathcal{F}\mathcal{,}\mathcal{P}$, avec $\mathcal{F}$ réc. én.

Sans perte de généralité, on suppose $𝜑$ close

• car si $𝜑$ non close :

  $$M\models 𝜑⟺\forall 𝜎,M,𝜎\models 𝜑$$

$𝜑$ valide

⟺ $\forall M,M\models 𝜑$

⟺ $\forall M,M⊭\neg 𝜑$

⟺ $\nexists M,M\models \neg 𝜑$

⟺ $\neg 𝜑$ n’est pas satisfaisable

1. $\neg 𝜑$ est logiquement équivalente à $𝜓$ où $𝜓$ est NNF (Non Negative Normal Form) (avec les règles de de Morgan).

2. ${𝜓}^{\prime }=Sk(𝜓)$. Par le théorème de Skolem, ${𝜓}^{\prime }$ est équisatisfaisable (mais PAS logiquement équivalente) à $𝜓$

   NB : Equivalence logique : tout modèle de l’une est modèle de l’autre VS Equisatisfaisabilité : pour tout modèle de l’une, il existe un modèle à l’autre

3. On met ${𝜓}^{\prime }$ sous forme prénexe : ${𝜓}^{\prime }=\forall x_1\cdots x_n{𝜑}_0$, où ${𝜑}_0$ est sans quantificateurs

Théorème de Herbrand :

pour toute formule close $𝜑$ universellement quantifiée, $𝜑$ est satisfiable ssi elle a un modèle de Herbrand.

Application à ${𝜓}^{\prime }$ : $𝜑$ valide ⟺ ${𝜓}^{\prime }$ n’admet aucun modèle de Herbrand.

Modèle de Herbrand :

une $F,P$-structure $H$ sur la $F$-algèbre $T(F)$ (termes clos).

NB : le seul degré de liberté qu’on a dans un modèle de Herbrand est l’interprétation des prédicats. Donc à chaque valeur de prédicat (ex: $P(0,0)$), on associe une variable propositionnelle (on passe de $H^{\prime }$ à $S_{H^{\prime }}$), et on se ramène à la satisfiabilité dans la logique des propositions.

Pour un $H^{\prime }$ fini, $H^{\prime }$ satisfaisable ssi $S_{H^{\prime }}$ est satisfaisable (calcul propositionnel).

Algo_valide(𝜑):

  Sk(¬𝜑) = ∀x_1, ⋯, x_n. 𝜓
  n = 0
  S = ∅
  n +=1 (L)
  S = S + {𝜓 𝜎 | 𝜎 n-ième substitution close}
  Si 𝜓 est insatisfiable: // en logique propositionnelle, où les termes clos sont les variables
    retourner Vrai
  Sinon:
    aller à (L)

OU

Algo_valide2(𝜑):

  S une partie non vide de H(𝜑_0)
  Pour chaque H':
    si S est insatisfiable :
      retourner "Valide"
    sinon:
        S = S + H'

NB : Pour “$S_{H^{\prime }}$ est insatisfiable”, on peut procéder de deux manière :

• il y a un nombre fini de variables, donc on peut tester toutes les valuations

• OU : avec la complétude réfutationnelle de $Res+Fact$, cela revient à montrer $S_{H^{\prime }}⊢\mathrm{\perp }$.

  Il suffit dont d’appliquer toutes les règles possibles depuis $S_{H^{\prime }}$ : ça termine, et on trouve nécessairement $\mathrm{\perp }$ si il y a insatisfaisabilité.

EX 2

$⟹$

Si $𝜎$ est un unificateur de $P$, montrons que $𝜎=𝜇𝜎$.

Il existe $𝜃$ unificateur tq

(car le mgu $𝜇$ est idempotent)

$⟸$

Si $𝜎=𝜇𝜎$ :

Comme $𝜇$ est un unificateur :

(par hypothèse)

EX 3

Supposons qu’il existe une telle $𝛹$, dont les modèles $M$ sont ceux tels que $D_M$ est infini.

On pose :

i.e :

$S\stackrel{\scriptscriptstyle\mathrm{def}}{=}\{\neg 𝛹\}\cup \{{𝜓}_n{\}}_{n\ge 0}$ est satisfaisable ssi elle est finiment satisfaisable.

Or, $S$ est insatisfiable (car si $M\models S$, $M\models \neg 𝛹$, donc $D_M$ est fini, ce qui contredit $M\models {𝜑}_{|D_M|+1}$)

Donc il existe une partie finie $S^{\prime }\subseteq S$ insatisfiable.

Or

• $S^{\prime }\stackrel{\scriptscriptstyle\mathrm{def}}{=}\{\neg 𝛹\}\cup \{{𝜓}_n{\}}_{n\le k}$

• OU $S^{\prime }\stackrel{\scriptscriptstyle\mathrm{def}}{=}\{{𝜓}_n{\}}_{n\le k}$

dans les deux cas : en choisissant un modèle $M$ à $k+1$ élément, ce modèle satisfait $S^{\prime }$ : absurde.

(exemple d’un tel modèle : un modèle de Herbrand à $k+1$ constantes où tous les prédicats sont interprétés par le vide et l’égalité par l’égalité numérique)

EX 5

$\forall P\in 𝒫,P\subseteq \mathcal{X}$.

Cas $F=\varnothing$ :

$𝜑$ satisfiable.

$𝒫$ fini.

Soit $M$ une $F,𝒫$-strucutre tq

$\forall x,y\in D_M$,

Soit $\sim$ définie par

$M^{\prime }=(D_M/\sim )$

Soit $P\in 𝒫$.

Alors :

Mq

$$M^{\prime }\models 𝜑$$

Hypothèse d’induction :

Pour toute sous-formule $𝜓$ de $𝜑$, pour toute $𝜎$ instantiation de $M$,

avec ${𝜎}^{\prime }=𝜎/\sim$