Verificação de Modelos

Os Amigos de Gandalf

Como verificar se uma interpretação é modelo de uma fórmula com quantificadores universais?

Sejam

• Constantes: $\cat{C}=\cbr{\lit{Gandalf}}$,
• Relações: $\cat{R}=\cbr{\lit{Amigo}_2}$,

Dada a seguinte interpretação daqueles símbolos em $\cat{U}=\cbr{\lit{A}, \lit{B}, \lit{C}}$: $$ \begin{aligned} \lit{Gandalf}^v &= \lit{A}, \cr \lit{Amigo}^v &= \cbr{\del{\lit{A}, \lit{A}}, \del{\lit{B}, \lit{A}}, \del{\lit{C}, \lit{A}}}. \end{aligned} $$

Será que $v$ satisfaz “Nenhum dos amigos dos amigos de Gandalf é amigo dele”?

$$p: \forall x \forall y~\underbrace{\fat{Amigo}{x, \lit{Gandalf}}\land\fat{Amigo}{y, x} \to \neg \fat{Amigo}{y, \lit{Gandalf}}}_{q\at{x,y}} $$

Para verificar se $v \models p$ listam-se os todos possíveis valores de $x,y$:

$$ \begin{array}{cc|ccc|c} x^v & y^v & \fat{Am}{x, \lit{Ga}}^v & \fat{Am}{x,y}^v & \neg \fat{A.}{y, \lit{Ga}}^v & q\at{x,y}^v\cr \hline \boxed{\lit{A}} & \boxed{\lit{A}} & \ndV & \ndV & \ndF & \boxed{\ndF} \cr \lit{A} & \lit{B} & \ndV & \ndF & \ndF & \ndV \cr \vdots & \vdots & \vdots & \vdots & \vdots & \vdots \end{array} $$

O que a primeira linha mostra é que, fazendo $x^v = A$ e $y^v = A$ então a fórmula $q\at{x,y}^v$ é falsa: $$ v \alert{\fix{x}{\lit{A}} \fix{y}{\lit{A}} \not \models} \fat{Amigo}{x, \lit{Gandalf}}\land\fat{Amigo}{y, x} \to \neg \fat{Amigo}{y, \lit{Gandalf}}. $$

Como uma das explicitações de $x,y$ não é verdade em $v$ então $$ v \not\models \forall x \forall y~\fat{Amigo}{x, \lit{Gandalf}}\land\fat{Amigo}{y, x} \to \neg \fat{Amigo}{y, \lit{Gandalf}}. $$