Négation de formule insatisfiable

[invite3443c7ee]

Bonjour à tous,

Voici mon problème :
Je me situe en logique FOL des prédicats (logique du 1er ordre sans fonction).
Selon ce que j'ai lu : la négation d'une formule F insatisfiable de FOL est valide (est une tautologie).

Or j'ai trouvé une formule F insatisfiable dont la négation est invalide, c'est à dire que j'arrive à trouver une interprétation qui fausse la négation de F.
Je ne trouve pas ça normal... il doit y avoir une erreur.

Voici F = exists x forall y -r(y,y) <-> r(x,y)
F est clairement insatisfiable (n'est ce pas ?). La négation est exprimée par le signe moins "-".

Voici -F = forall x exists y r(y,y) <-> r(x,y).
On voit bien que l'interprétation suivante invalide -F :
Le domaine D={a,b,c} et les relations valides entre les éléments de D sont r(a,a) et r(b,c).
Si x:=a -F est vérifiée, puisqu'il existe y:=a tel que r(y,y) soit equivalent à r(x,y).
Si x:=b -F est fausse, puisqu'il n'existe pas de y tel que r(y,y) soit equivalent à r(b,y). En effet, si on choisit y=c on a r(c,c) <-> r(b,c) et c'est faux. Les autres choix pareil...

Alors que se passe-t-il lol, je n'y comprends plus rien ...
Si quelqu'un peut m'aider
Merci beaucoup de m'avoir lu
-----

[Médiat]

Voici -F = forall x exists y r(y,y) <-> r(x,y).
On voit bien que l'interprétation suivante invalide -F :

Il me semble que si tu choisis y = x la formule -F est vérifiée (dans tous les modèles)

[inviteeac53e14]

Il me semble que si tu choisis y = x la formule -F est vérifiée (dans tous les modèles)

Comme le dit Médiat, ta formule -F est clairement un tautologie (quel que soit x, il suffit de prendre y égal à x)