5.11: Satisfacción de una Fórmula en una Estructura

Template:MathJaxZach

La noción básica que relaciona expresiones como términos y fórmulas, por un lado, y estructuras por otro, son las de valor de un término y satisfacción de una fórmula. Informalmente, el valor de un término es un elemento de una estructura; si el término es solo una constante, su valor es el objeto asignado a la constante por la estructura, y si se construye usando símbolos de función, el valor se calcula a partir de los valores de las constantes y las funciones asignadas a las funciones en el término. Una fórmula se satisface en una estructura si la interpretación dada a los predicados hace que la fórmula sea verdadera en el dominio de la estructura. Esta noción de satisfacción se especifica inductivamente: la especificación de la estructura establece directamente cuándo se satisfacen las fórmulas atómicas, y definimos cuándo se satisface una fórmula compleja dependiendo del conectivo o cuantificador principal y si se satisfacen o no las subfórmulas inmediatas. El caso de los cuantificadores aquí es un poco complicado, ya que la subfórmula inmediata de una fórmula cuantificada tiene una variable libre, y las estructuras no especifican los valores de las variables. Para hacer frente a esta dificultad, también introducimos asignaciones variables y definimos la satisfacción no con respecto a una estructura sola, sino con respecto a una estructura más una asignación variable.

Definición\(\PageIndex{1}\): Variable Assignment

Una asignación de variables\(s\) para una estructura\(\Struct{M}\) es una función que mapea cada variable a un elemento de\(\Domain M\), es decir,\(s\colon \Var \to \Domain M\).

Una estructura asigna un valor a cada símbolo constante y una asignación de variables a cada variable. Pero queremos usar términos construidos a partir de ellos para nombrar también elementos del dominio. Para ello definimos el valor de los términos inductivamente. Para símbolos y variables constantes el valor es tal como la estructura o la asignación de variables lo especifica; para términos más complejos se calcula recursivamente usando las funciones que la estructura asigna a los símbolos de función.

Definición\(\PageIndex{2}\): Value of Terms

Si\(t\) es un término del lenguaje\(\Lang L\),\(\Struct M\) es una estructura para\(\Lang L\), y\(s\) es una asignación variable para\(\Struct M\), el valor\(\Value[s]{t}{M}\) se define de la siguiente manera:

1. \(\indcase{t}{c}\)\(\Value[s]{t}{M} = \Assign{c}{M}\).

2. \(\indcase{t}{x}\)\(\Value[s]{t}{M} = s(x)\).

3. \(\indcase{t}{\Atom{f}{t_1, \ldots, t_n}}\)\[\Value[s]{t}{M} = \Assign{f}{M}(\Value[s]{t_1}{M}, \ldots, \Value[s]{t_n}{M}).\nonumber\]

Definición\(\PageIndex{3}\): \(x\)-Variant

Si\(s\) es una asignación de variables para una estructura\(\Struct M\), entonces cualquier asignación de variable\(s'\) para la\(\Struct M\) que difiera de como máximo\(s\) en lo que asigna\(x\) se llama \(x\)-variante de\(s\). Si\(s'\) es una\(x\) -variante de\(s\) escribimos\(\varAssign{s'}{s}{x}\).

Tenga en cuenta que una\(x\) variante -de una asignación\(s\) no tiene que asignar algo diferente a\(x\). De hecho, cada asignación cuenta como una\(x\) variante de sí misma.

Definición\(\PageIndex{4}\): Satisfaction

La satisfacción de una fórmula\(A\) en una estructura\(\Struct M\) relativa a una asignación variable\(s\), en símbolos:\(\Sat[,s]{M}{A}\), se define recursivamente de la siguiente manera. (Escribimos\(\SatN[,s]{M}{A}\) para significar “no”)\(\Sat[,s]{M}{A}\).

1. \(\indcase{A}{\lfalse}\)\(\SatN[,s]{M}{\indfrm}\).

2. \(\indcase{A}{\Atom{R}{t_1, \dots, t_n}}\)\(\Sat[,s]{M}{\indfrm}\)iff\(\langle \Value[s]{t_1}{M}, \dots, \Value[s]{t_n}{M} \rangle \in \Assign{R}{M}\).

3. \(\indcase{A}{\eq[t_1][t_2]}\)\(\Sat[,s]{M}{\indfrm}\)iff\(\Value[s]{t_1}{M} = \Value[s]{t_2}{M}\).

4. \(\indcase{A}{\lnot B}\)\(\Sat[,s]{M}{\indfrm}\)iff\(\SatN[,s]{M}{B}\).

5. \(\indcase{A}{(B \land C)}\)\(\Sat[,s]{M}{\indfrm}\)iff\(\Sat[,s]{M}{B}\) y\(\Sat[,s]{M}{C}\).

6. \(\indcase{A}{(B \lor C)}\)\(\Sat[,s]{M}{\indfrm}\)iff\(\Sat[,s]{M}{A}\) o\(\Sat[,s]{M}{B}\) (o ambos).

7. \(\indcase{A}{(B \lif C)}\)\(\Sat[,s]{M}{\indfrm}\)iff\(\SatN[,s]{M}{B}\) o\(\Sat[,s]{M}{C}\) (o ambos).

8. \(\indcase{A}{\lforall{x}{B}}\)\(\Sat[,s]{M}{\indfrm}\)iff para cada\(x\) -variante\(s'\) de\(s\),\(\Sat[,s']{M}{B}\).

9. \(\indcase{A}{\lexists{x}{B}}\)\(\Sat[,s]{M}{\indfrm}\)iff hay una\(x\) -variante\(s'\) de\(s\) así que\(\Sat[,s']{M}{B}\).

Las asignaciones de variables son importantes en las dos últimas cláusulas. No podemos definir la satisfacción de\(\lforall{x}{B(x)}\) por “para todos”\(a \in \Domain{M}\),\(\Sat{M}{B(a)}\). No podemos definir la satisfacción de\(\lexists{x}{B(x)}\) por “por lo menos uno”\(a \in \Domain{M}\),\(\Sat{M}{B(a)}\). El motivo es que no\(a\) es símbolo de la lengua, y así no\(B(a)\) es una fórmula (es decir, no\(\Subst{B}{a}{x}\) está definida). Tampoco podemos suponer que tenemos constantes símbolos o términos disponibles que nombran a cada elemento de\(\Struct{M}\), ya que no hay nada en la definición de estructuras que lo requiera. Incluso en el lenguaje estándar el conjunto de símbolos constantes es contablemente infinito, así que si no\(\Domain{M}\) es enumerable no hay ni siquiera suficientes símbolos constantes para nombrar a cada objeto.

Ejemplo\(\PageIndex{1}\)

Dejar\(\Lang{L} = \{a, b, f, R\}\) donde\(a\) y\(b\) son símbolos constantes,\(f\) es un símbolo de función de dos lugares, y\(R\) es un símbolo de predicado de dos lugares. Considere la estructura\(\Struct{M}\) definida por:

1. \(\Domain M = \{1, 2, 3, 4\}\)

2. \(\Assign{a}{M} = 1\)

3. \(\Assign{b}{M} = 2\)

4. \(\Assign{f}{M}(x, y) = x+y\)si\(x+y \le 3\) y de\(= 3\) otra manera.

5. \(\Assign{R}{M} = \{\tuple{1, 1}, \tuple{1, 2}, \tuple{2, 3}, \tuple{2, 4}\}\)

La función\(s(x) = 1\) que asigna\(1 \in \Domain{M}\) a cada variable es una asignación de variables para\(\Struct{M}\).

Entonces

\[\Value[s]{f(a,b)}{M} = \Assign{f}{M}(\Value[s]{a}{M}, \Value[s]{b}{M}).\nonumber\]

Ya que\(a\) y\(b\) son símbolos constantes,\(\Value[s]{a}{M} = \Assign{a}{M} = 1\) y\(\Value[s]{b}{M} = \Assign{b}{M} = 2\). Entonces

\[\Value[s]{f(a,b)}{M} = \Assign{f}{M}(1, 2) = 1+2 = 3.\nonumber\]

Para calcular el valor de\(f(f(a,b),a)\) tenemos que considerar

\[\Value[s]{f(f(a,b),a)}{M} = \Assign{f}{M}(\Value[s]{f(a, b)}{M}, \Value[s]{a}{M}) = \Assign{f}{M}(3, 1) = 3,\nonumber\]

ya que\(3+1 > 3\). Desde\(s(x) = 1\) y\(\Value[s]{x}{M} = s(x)\), también tenemos

\[\Value[s]{f(f(a,b),x)}{M} = \Assign{f}{M}(\Value[s]{f(a, b)}{M}, \Value[s]{x}{M}) = \Assign{f}{M}(3, 1) = 3.\nonumber\]

Una fórmula atómica\(R(t_1, t_2)\) se satisface si la tupla de valores de sus argumentos, es decir\(\tuple{\Value[s]{t_1}{M}, \Value[s]{t_2}{M}}\), es un elemento de\(\Assign{R}{M}\). Entonces, por ejemplo, tenemos\(\Sat[,s]{M}{R(b,f(a,b))}\) desde\(\tuple{\Value{b}{M}, \Value{f(a,b)}{M}} = \tuple{2, 3} \in \Assign{R}{M}\), pero\(\SatN[,s]{M}{R(x, f(a,b))}\) desde entonces\(\tuple{1, 3} \notin \Assign{R}{M}[s]\).

Para determinar si\(A\) se cumple una fórmula no atómica, se aplican las cláusulas en la definición inductiva que se aplica al conectivo principal. Por ejemplo, el principal conectivo en\(R(a, a) \lif (R(b, x) \lor R(x, b))\) es el\(\lif\), y

\ [\ comenzar {alineado}
&\ sáb [, s] {M} {R (a, a)\ lif (R (b, x)\ lor R (x, b))}\ texto {iff}\\
&\ qquad\ satN [, s] {M} {R (a, a)}\ texto {o}\ sáb [, s] {M} {R (b, x)\ or R (x, b)}
\ final {alineado}\]

Ya que\(\Sat[,s]{M}{R(a,a)}\) (porque\(\tuple{1,1} \in \Assign{R}{M}\)) aún no podemos determinar la respuesta y primero debemos averiguar si\(\Sat[,s]{M}{R(b, x) \lor R(x, b)}\):

\ [\ begin {alineado}
&\ sáb [, s] {M} {R (b, x)\ lor R (x, b)}\ texto {iff}\\
&\ qquad\ sáb [, s] {M} {R (b, x)}\ texto {o}\ sáb [, s] {M} {R (x, b)}
\ fin {alineado}\]

Y este es el caso, ya que\(\Sat[,s]{M}{R(x, b)}\) (porque\(\tuple{1,2} \in \Assign{R}{M}\)).

Recordemos que una\(x\) -variante de\(s\) es una asignación variable que difiere de\(s\) como mucho en lo que asigna a\(x\). Para cada elemento de\(\Domain{M}\), hay una\(x\) -variante de\(s\):\(s_1(x) = 1\),,\(s_2(x) = 2\),\(s_3(x) = 3\)\(s_4(x) = 4\), y con\(s_i(y) = s(y) = 1\) para todas las variables\(y\) aparte de\(x\). Estas son todas las\(x\) -variantes de\(s\) para la estructura\(\Struct{M}\), ya que\(\Domain{M} = \{1, 2, 3, 4\}\). Tenga en cuenta, en particular, que también\(s_1 = s\) es una\(x\) -variante de\(s\), es decir, siempre\(s\) es una\(x\) -variante de sí misma.

Para determinar si\(\lexists{x}{A(x)}\) se satisface una fórmula cuantificada existencialmente, tenemos que determinar si\(\Sat[,s']{M}{A(x)}\) para al menos una\(x\) -variante\(s'\) de\(s\). Entonces,\[\Sat[,s]{M}{\lexists{x}{(R(b,x) \lor R(x,b))}},\nonumber\] ya que\(\Sat[,s_1]{M}{R(b,x) \lor R(x, b)}\) (también se\(s_3\) ajustaría a la factura). Pero,\[\SatN[,s]{M}{\lexists{x}{(R(b,x) \land R(x,b))}}\nonumber\] ya que para ninguno de los\(s_i\),\(\Sat[,s_i]{M}{R(b,x) \land R(x,b)}\).

Para determinar si\(\lforall{x}{A(x)}\) se satisface una fórmula universalmente cuantificada, tenemos que determinar si\(\Sat[,s']{M}{A(x)}\) para todas las\(x\) variantes\(s'\) de\(s\). Entonces,\[\Sat[,s]{M}{\lforall{x}{(R(x,a) \lif R(a,x))}},\nonumber\] ya que\(\Sat[,s_i]{M}{R(x,a) \lif R(a,x)}\) para todos\(s_i\) (\(\Sat[,s_1]{M}{R(a,x)}\)y\(\SatN[,s_j]{M}{R(x,a)}\) para\(j = 2\),\(3\), y\(4\)). Pero,\[\SatN[,s]{M}{\lforall{x}{(R(a,x) \lif R(x,a))}}\nonumber\] desde\(\SatN[,s_2]{M}{R(a,x) \lif R(x,a)}\) (porque\(\Sat[,s_2]{M}{R(a, x)}\) y\(\SatN[,s_2]{M}{R(x, a)}\)).

Para un caso más complicado, considere\[\lforall{x}{(R(a,x) \lif \lexists{y}{R(x,y)})}.\nonumber\] Desde\(\SatN[,s_3]{M}{R(a,x)}\) y\(\SatN[,s_4]{M}{R(a,x)}\), los casos interesantes en los que tenemos que preocuparnos por lo consecuente del condicional son sólo\(s_1\) y\(s_2\). ¿Se\(\Sat[,s_1]{M}{\lexists{y}{R(x,y)}}\) sostiene? Lo hace si hay al menos una\(y\) -variante\(s_1'\) de\(s_1\) así que\(\Sat[,s_1']{M}{R(x,y)}\). De hecho,\(s_1\) es tal\(y\) -variante (\(s_1(x) = 1\),\(s_1(y) = 1\), y\(\tuple{1,1} \in \Assign{R}{M}\)), entonces la respuesta es sí. Para determinar si\(\Sat[,s_2]{M}{\lexists{y}{R(x,y)}}\) tenemos que mirar las\(y\) -variantes de\(s_2\). Aquí,\(s_2\) en sí mismo no satisface\(R(x,y)\) (\(s_2(x) = 2\),\(s_2(y) = 1\), y\(\tuple{2,1}\notin \Assign{R}{M}\)). Sin embargo, considere\(\varAssign{s_2'}{s_2}{y}\) con\(s_2'(y) = 3\). \(\Sat[,s_2']{M}{R(x,y)}\)desde\(\tuple{2,3} \in \Assign{R}{M}\), y así\(\Sat[,s_2]{M}{\lexists{y}{R(x,y)}}\). En suma, por cada\(x\) -variante\(s_i\) de\(s\), ya sea\(\SatN[,s_i]{M}{R(a,x)}\) (\(i = 3\),\(4\)) o\(\Sat[,s_i]{M}{\lexists{y}{R(x,y)}}\) (\(i = 1\),\(2\)), y así\[\Sat[,s]{M}{\lforall{x}{(R(a,x) \lif \lexists{y}{R(x,y)})}}.\nonumber\] Por otro lado,\[\SatN[,s]{M}{\lexists{x}{(R(a,x) \land \lforall{y}{R(x,y)})}}.\nonumber\] Las únicas\(x\) -variantes\(s_i\) de\(s\) con\(\Sat[,s_i]{M}{R(a,x)}\) son\(s_1\) y\(s_2\). Pero para cada uno, hay a su vez una\(y\) -variante\(\varAssign{s_i'}{s_i}{y}\) con\(s_i'(y) = 4\) así que eso\(\SatN[,s_i']{M}{R(x,y)}\) y así\(\SatN[,s_i]{M}{\lforall{y}{R(x,y)}}\) para\(i = 1\),\(2\). En suma, ninguna de las\(x\)\(\varAssign{s_i}{s}{x}\) -variantes es tal que\(\Sat[,s_i]{M}{R(a,x) \land \lforall{y}{R(x,y)}}\).

Problema\(\PageIndex{1}\)

Dejar\(\Lang L = \{c, f, A\}\) con un símbolo constante, un símbolo de función de un solo lugar y un símbolo de predicado de dos lugares, y dejar que la estructura\(\Struct{M}\) sea dada por

1. \(\Domain M = \{1, 2, 3\}\)

2. \(\Assign{c}{M} = 3\)

3. \(\Assign{f}{M}(1) = 2, \Assign{f}{M}(2) = 3, \Assign{f}{M}(3) = 2\)

4. \(\Assign{A}{M} = \{\tuple{1, 2}, \tuple{2, 3}, \tuple{3, 3}\}\)

(a) Dejar\(s(v) = 1\) para todas las variables\(v\). Averigua si\[\Sat[,s]{M}{\lexists{x}{(A(f(z), c) \lif \lforall{y}{(A(y, x) \lor A(f(y), x))})}}\nonumber\] Explica por qué o por qué no.

b) Dar una estructura diferente y asignación de variables en la que no se satisfaga la fórmula.