Saltar al contenido principal

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

$$\newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} }$$

$$\newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}}$$

$$\newcommand{\id}{\mathrm{id}}$$ $$\newcommand{\Span}{\mathrm{span}}$$

( \newcommand{\kernel}{\mathrm{null}\,}\) $$\newcommand{\range}{\mathrm{range}\,}$$

$$\newcommand{\RealPart}{\mathrm{Re}}$$ $$\newcommand{\ImaginaryPart}{\mathrm{Im}}$$

$$\newcommand{\Argument}{\mathrm{Arg}}$$ $$\newcommand{\norm}[1]{\| #1 \|}$$

$$\newcommand{\inner}[2]{\langle #1, #2 \rangle}$$

$$\newcommand{\Span}{\mathrm{span}}$$

$$\newcommand{\id}{\mathrm{id}}$$

$$\newcommand{\Span}{\mathrm{span}}$$

$$\newcommand{\kernel}{\mathrm{null}\,}$$

$$\newcommand{\range}{\mathrm{range}\,}$$

$$\newcommand{\RealPart}{\mathrm{Re}}$$

$$\newcommand{\ImaginaryPart}{\mathrm{Im}}$$

$$\newcommand{\Argument}{\mathrm{Arg}}$$

$$\newcommand{\norm}[1]{\| #1 \|}$$

$$\newcommand{\inner}[2]{\langle #1, #2 \rangle}$$

$$\newcommand{\Span}{\mathrm{span}}$$ $$\newcommand{\AA}{\unicode[.8,0]{x212B}}$$

$$\newcommand{\vectorA}[1]{\vec{#1}} % arrow$$

$$\newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow$$

$$\newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} }$$

$$\newcommand{\vectorC}[1]{\textbf{#1}}$$

$$\newcommand{\vectorD}[1]{\overrightarrow{#1}}$$

$$\newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}}$$

$$\newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}}$$

$$\newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} }$$

$$\newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}}$$

$$\newcommand{\avec}{\mathbf a}$$ $$\newcommand{\bvec}{\mathbf b}$$ $$\newcommand{\cvec}{\mathbf c}$$ $$\newcommand{\dvec}{\mathbf d}$$ $$\newcommand{\dtil}{\widetilde{\mathbf d}}$$ $$\newcommand{\evec}{\mathbf e}$$ $$\newcommand{\fvec}{\mathbf f}$$ $$\newcommand{\nvec}{\mathbf n}$$ $$\newcommand{\pvec}{\mathbf p}$$ $$\newcommand{\qvec}{\mathbf q}$$ $$\newcommand{\svec}{\mathbf s}$$ $$\newcommand{\tvec}{\mathbf t}$$ $$\newcommand{\uvec}{\mathbf u}$$ $$\newcommand{\vvec}{\mathbf v}$$ $$\newcommand{\wvec}{\mathbf w}$$ $$\newcommand{\xvec}{\mathbf x}$$ $$\newcommand{\yvec}{\mathbf y}$$ $$\newcommand{\zvec}{\mathbf z}$$ $$\newcommand{\rvec}{\mathbf r}$$ $$\newcommand{\mvec}{\mathbf m}$$ $$\newcommand{\zerovec}{\mathbf 0}$$ $$\newcommand{\onevec}{\mathbf 1}$$ $$\newcommand{\real}{\mathbb R}$$ $$\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}$$ $$\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}$$ $$\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}$$ $$\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}$$ $$\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$$ $$\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$$ $$\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$$ $$\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$$ $$\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}$$ $$\newcommand{\laspan}[1]{\text{Span}\{#1\}}$$ $$\newcommand{\bcal}{\cal B}$$ $$\newcommand{\ccal}{\cal C}$$ $$\newcommand{\scal}{\cal S}$$ $$\newcommand{\wcal}{\cal W}$$ $$\newcommand{\ecal}{\cal E}$$ $$\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}$$ $$\newcommand{\gray}[1]{\color{gray}{#1}}$$ $$\newcommand{\lgray}[1]{\color{lightgray}{#1}}$$ $$\newcommand{\rank}{\operatorname{rank}}$$ $$\newcommand{\row}{\text{Row}}$$ $$\newcommand{\col}{\text{Col}}$$ $$\renewcommand{\row}{\text{Row}}$$ $$\newcommand{\nul}{\text{Nul}}$$ $$\newcommand{\var}{\text{Var}}$$ $$\newcommand{\corr}{\text{corr}}$$ $$\newcommand{\len}[1]{\left|#1\right|}$$ $$\newcommand{\bbar}{\overline{\bvec}}$$ $$\newcommand{\bhat}{\widehat{\bvec}}$$ $$\newcommand{\bperp}{\bvec^\perp}$$ $$\newcommand{\xhat}{\widehat{\xvec}}$$ $$\newcommand{\vhat}{\widehat{\vvec}}$$ $$\newcommand{\uhat}{\widehat{\uvec}}$$ $$\newcommand{\what}{\widehat{\wvec}}$$ $$\newcommand{\Sighat}{\widehat{\Sigma}}$$ $$\newcommand{\lt}{<}$$ $$\newcommand{\gt}{>}$$ $$\newcommand{\amp}{&}$$ $$\definecolor{fillinmathshade}{gray}{0.9}$$

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

&\ 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)}

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)}$$:

&\ 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)}

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.

This page titled 5.11: Satisfacción de una Fórmula en una Estructura is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .