24 lines
1.5 KiB
Markdown
24 lines
1.5 KiB
Markdown
#s/maths/logique
|
|
|
|
----
|
|
Un _skolem_ est une forme particulière de formules de la [[logique des predicats du premier ordre]].
|
|
Elle consiste en une formule sous [[forme normale conjonctive]] et [[forme prénèxe|prénèxe]], mais sur laquelle on à supprimé tous les [[quantificateurs]] existentiels ($\exists$) en utilisant des fonctions, pour ne garder que des quantificateurs $\forall$.
|
|
|
|
**Note :** On ne cherche pas à ce que la forme de skolem soit [[equivalence|équivalente]] à la formule originale. On veut simplement que **si l'une est [[satisfaisable]], l'autre le soit aussi**. On veut qu'elles soient [[equisatisfaisables]]
|
|
|
|
# Exemple
|
|
Soit la formule suivant : $\forall x \exists y \text{ Sup}(x, y)$
|
|
Avec $\text{Sup}(x, y) \equiv x < y$, et avec pour [[domaine d'interprétation]] $\N$
|
|
On sait que cette formule est vraie : on peut toujours trouver un entier plus grand que n'importe quel autre.
|
|
**Démonstration :**
|
|
Soit une [[interprétation]] $I_v(x)$ de $x$,
|
|
Il est possible de construire une [[interprétation]] $I_v(y) = I_v(x) + 1$
|
|
Comme $\N$ n'à pas de borne supérieure, cette interprétation existe toujours
|
|
Et dans ce cas, on à bien $\text{Sup}(I_v(x), I_v(y))$
|
|
**Lien avec la skolemisation :**
|
|
On a utilisé la fonction $f: x \mapsto x + 1$ pour faire cette démonstration.
|
|
On a posé que $y = f(x)$.
|
|
La skolemisation consiste à remplacer $y$ par $f(x)$ dans la formule :
|
|
$\forall x \exists y \text{Sup}(x, y)$ (forme normale)
|
|
$\forall x \text{Sup}{x, f(x)}$ (forme de _skolem_)
|