5.12: Asignaciones Variables

Última actualización
Guardar como PDF

Page ID: 103677

$ \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}}$

Template:MathJaxZach

Una asignación de variables$s$ proporciona un valor para cada variable, y hay infinitamente muchas de ellas. Esto, por supuesto, no es necesario. Requerimos asignaciones de variables para asignar valores a todas las variables simplemente porque facilita mucho las cosas. El valor de un término$t$, y si una fórmula$A$ se satisface o no en una estructura con respecto a$s$, sólo depende de las asignaciones$s$ que haga a las variables en$t$ y las variables libres de $A$. Este es el contenido de las dos proposiciones siguientes. Para hacer precisa la idea de “depende de”, mostramos que cualesquiera dos asignaciones de variables que coincidan en todas las variables en$t$ dan el mismo valor, y que$A$ se satisface en relación con una iff se satisface en relación con la otra si dos asignaciones de variables coinciden en todas variables libres de$A$.

Proposición$\PageIndex{1}$

Si las variables en un término$t$ están entre$x_1$,...$x_n$,, y$s_1(x_i) = s_2(x_i)$ para$i = 1$,...$n$, entonces$\Value[s_1]{t}{M} = \Value[s_2]{t}{M}$.

Comprobante. Por inducción sobre la complejidad de$t$. Para el caso base,$t$ puede ser un símbolo constante o una de las variables$x_1$,...,$x_n$. Si$t = c$, entonces$\Value[s_1]{t}{M} = \Assign{c}{M} = \Value[s_2]{t}{M}$. Si$t = x_i$,$s_1(x_i) = s_2(x_i)$ por la hipótesis de la proposición, y así$\Value[s_1]{t}{M} = s_1(x_i) = s_2(x_i) = \Value[s_2]{t}{M}$.

Para el paso inductivo, asumir que$t = \Atom{f}{t_1, \dots, t_k}$ y que el reclamo se sostiene para$t_1$,...,$t_k$. Entonces

\ [\ begin {aligned}
\ Valor [s_1] {t} {M}
& =\ Valor [s_1] {\ Atom {f} {t_1,\ dots, t_k}} {M} =\
& =\ Asignar {f} {M} (\ Valor [s_1] {t_1} {M},\ puntos,\ Valor [s_1] {t_k} {M})
\ end {alineado}\]

Para$j = 1, \dots, k$, las variables de$t_j$ se encuentran entre$x_1, \dots,x_n$. Entonces por hipótesis de inducción,$\Value[s_1]{t_j}{M} = \Value[s_2]{t_j}{M}$. Entonces,

\ [\ begin {aligned}
\ Valor [s_1] {t} {M} & =\ Valor [s_2] {\ Atom {f} {t_1,\ dots, t_k}} {M} =\ & =\ Asignar {f} {M} (\ Valor [s_1] {t_1} {M},\ puntos,\ Valor [s_1] {t_k} {M}) =\\ & =\ Asignar {f} {M} (\ Valor [s_2] {t_1} {M},\ puntos,\ Valor [s_2] {t_k} {M}) =\\ & =\ Valor [s_2] {\ Atom {f} {t_1,\ puntos, t_k}} {M} =\ Valor [ s_2] {t} {M}. \ end {alineado}\] ◻

Proposición$\PageIndex{2}$

Si las variables libres en$A$ están entre$x_1$,...,$x_n$, y$s_1(x_i) = s_2(x_i)$ para$i = 1$,...,$n$, entonces$\Sat[,s_1]{M}{A}$ iff$\Sat[,s_2]{M}{A}$.

Comprobante. Utilizamos la inducción en la complejidad de$A$. Para el caso base, donde$A$ es atómico,$A$ puede ser:$\lfalse$,$\Atom{R}{t_1, \dots, t_k}$ para un predicado$R$ y términos$k$ -place$t_1$,...$t_k$, o$\eq[t_1][t_2]$ para términos$t_1$ y$t_2$.

$\indcase{A}{\lfalse}$ambos$\SatN[,s_1]{M}{A}$ y$\SatN[,s_2]{M}{A}$.
$\indcase{A}{\Atom{R}{t_1, \ldots, t_k}}$dejar$\Sat[,s_1]{M}{\indfrm}$. Entonces\[\langle \Value[s_1]{t_1}{M}, \ldots, \Value[s_1]{t_k}{M} \rangle \in \Assign{R}{M}.\nonumber\] Por$i = 1$,...,$k$,$\Value[s_1]{t_i}{M} = \Value[s_2]{t_i}{M}$ por Proposición$\PageIndex{1}$. Entonces también tenemos$\langle \Value[s_2]{t_i}{M}, \ldots, \Value[s_2]{t_k}{M} \rangle \in \Assign{R}{M}$.
$\indcase{A}{\eq[t_1][t_2]}$supongamos$\Sat[,s_1]{M}{\indfrm}$. Entonces$\Value[s_1]{t_1}{M} = \Value[s_1]{t_2}{M}$. Entonces,\[\begin{aligned} \Value[s_2]{t_1}{M} & = \Value[s_1]{t_1}{M} & \text{(by Proposition $\PageIndex{1}$)} \\ & = \Value[s_1]{t_2}{M} & \text{(since $\Sat[,s_1]{M}{\eq[t_1][t_2]}$)}\\ &= \Value[s_2]{t_2}{M} & \text{(by Proposition $\PageIndex{1}$),} \end{aligned}\] entonces$\Sat[,s_2]{M}{\eq[t_1][t_2]}$.

Ahora asuma$\Sat[,s_1]{M}{B}$ iff$\Sat[,s_2]{M}{B}$ para todas las fórmulas$B$ menos complejas que$A$. El paso de inducción procede por casos determinados por el operador principal de$A$. En cada caso, solo demostramos la dirección hacia delante del bicondicional; la prueba de la dirección inversa es simétrica. En todos los casos excepto los de los cuantificadores, aplicamos la hipótesis de inducción a las subfórmulas$B$ de$A$. Las variables libres de$B$ se encuentran entre las de$A$. Así, si$s_1$ y$s_2$ acuerdan las variables libres de$A$, también coinciden en las de$B$, y la hipótesis de inducción se aplica a$B$.

$\indcase{A}{\lnot B}$si$\Sat[,s_1]{M}{\indfrm}$, entonces$\SatN[,s_1]{M}{B}$, así por la hipótesis de inducción,$\SatN[,s_2]{M}{B}$, de ahí$\Sat[,s_2]{M}{\indfrm}$.
$\indcase{A}{B \land C}$ejercicio.
$\indcase{A}{B \lor C}$si$\Sat[,s_1]{M}{\indfrm}$, entonces$\Sat[,s_1]{M}{B}$ o$\Sat[,s_1]{M}{C}$. Por hipótesis de inducción,$\Sat[,s_2]{M}{B}$ o$\Sat[,s_2]{M}{C}$, así$\Sat[,s_2]{M}{\indfrm}$.
$\indcase{A}{B \lif C}$ejercicio.
$\indcase{A}{\lexists{x}{B}}$si$\Sat[,s_1]{M}{\indfrm}$, hay una$x$ -variante$s_1'$ de$s_1$ para que$\Sat[,s_1']{M}{B}$. $s_2'$Sea la$x$ -variante de$s_2$ que le asigne lo mismo a$x$ lo que hace$s_1'$. Las variables libres de$B$ se encuentran entre$x_1$,...$x_n$, y$x$. $s_1'(x_i) = s_2'(x_i)$, ya que$s_1'$ y$s_2'$ son$x$ -variantes de$s_1$ y$s_2$, respectivamente, y por hipótesis$s_1(x_i) = s_2(x_i)$. $s_1'(x) = s_2'(x)$por la forma en que hemos definido$s_2'$. Entonces la hipótesis de inducción se aplica a$B$ y$s_1'$,$s_2'$, entonces$\Sat[,s_2']{M}{B}$. De ahí que haya una$x$ -variante de$s_2$ que satisfaga$B$, y así$\Sat[,s_2]{M}{\indfrm}$.
$\indcase{A}{\lforall{x}{B}}$ejercicio.

Por inducción, obtenemos ese$\Sat[,s_1]{M}{A}$ iff$\Sat[,s_2]{M}{A}$ siempre que las variables libres en$A$ se encuentren entre$x_1$,...,$x_n$ y$s_1(x_i)=s_2(x_i)$ para$i = 1$,...,$n$. ◻

Problema$\PageIndex{1}$

Completar el comprobante de Proposición$\PageIndex{2}$.

Las oraciones no tienen variables libres, por lo que dos asignaciones de variables cualesquiera asignan las mismas cosas a todas las variables libres (cero) de cualquier oración. La proposición recién probada entonces significa que el que se satisfaga o no una oración en una estructura relativa a una asignación variable es completamente independiente de la asignación. Vamos a grabar este hecho. Justifica la definición de satisfacción de una oración en una estructura (sin mencionar una asignación variable) que sigue.

Corolario$\PageIndex{1}$

Si$A$ es una oración y$s$ una asignación variable, entonces$\Sat[,s]{M}{A}$ iff$\Sat[,s']{M}{A}$ para cada asignación de variable$s'$.

Comprobante. Dejar$s'$ ser cualquier asignación de variables. Ya que$A$ es una oración, no tiene variables libres, y así cada asignación de variables asigna$s'$ trivialmente las mismas cosas a todas las variables libres de$A$ como lo hace$s$. Entonces se cumple la condición de Proposición$\PageIndex{2}$, y tenemos$\Sat[,s]{M}{A}$ iff$\Sat[,s']{M}{A}$. ◻

Definición$\PageIndex{1}$

Si$A$ es una oración, decimos que una estructura$\Struct M$ satisface$A$,$\Sat{M}{A}$, iff$\Sat[,s]{M}{A}$ para todas las asignaciones de variables$s$.

Si$\Sat{M}{A}$, también simplemente decimos que$A$ es cierto en$\Struct{M}$.

Proposición$\PageIndex{3}$

Dejar$\Struct{M}$ ser una estructura,$A$ ser una oración, y$s$ una asignación variable. $\Sat{M}{A}$iff$\Sat[,s]{M}{A}$.

Comprobante. Ejercicio. ◻

Problema$\PageIndex{2}$

Probar Proposición$\PageIndex{3}$.

Proposición$\PageIndex{4}$

Supongamos que$A(x)$ solo contiene$x$ libre, y$\Struct M$ es una estructura. Entonces:

$\Sat{M}{\lexists{x}{A(x)}}$iff$\Sat[,s]{M}{A(x)}$ para al menos una asignación de variables$s$.
$\Sat{M}{\lforall{x}{A(x)}}$iff$\Sat[,s]{M}{A(x)}$ para todas las asignaciones de variables$s$.

Comprobante. Ejercicio. ◻

Problema$\PageIndex{3}$

Demostrar Proposición$\PageIndex{4}$.

Problema$\PageIndex{4}$

Supongamos que$\Lang L$ es un lenguaje sin símbolos de función. Dada una estructura$\Struct M$,$c$ un símbolo constante y$a \in \Domain M$,$\Struct M[a/c]$ definir como la estructura que es igual$\Struct M$, excepto eso$\Assign{c}{M[a/c]} = a$. Definir$\Struct M \mathrel{||}\joinrel\Relbar A$ para oraciones$A$ por:

$\indcase{A}{\lfalse}$no$\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$.
$\indcase{A}{\Atom{R}{d_1, \dots, d_n}}$$\Struct M \mathrel{||}\joinrel\Relbar\indfrm$iff$\langle \Assign{d_1}{M}, \dots, \Assign{d_n}{M} \rangle \in \Assign{R}{M}$.
$\indcase{A}{\eq[d_1][d_2]}$$\Struct M \mathrel{||}\joinrel\Relbar\indfrm$iff$\Assign{d_1}{M} = \Assign{d_2}{M}$.
$\indcase{A}{\lnot B}$$\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$iff no$\Struct{M} \mathrel{||}\joinrel\Relbar{B}$.
$\indcase{A}{(B \land C)}$$\Struct{M} \mathrel{||}\joinrel\Relbar \indfrm$iff$\Struct{M} \mathrel{||}\joinrel\Relbar B$ y$\Struct{M} \mathrel{||}\joinrel\Relbar C$.
$\indcase{A}{(B \lor C)}$$\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$iff$\Struct{M} \mathrel{||}\joinrel\Relbar B$ o$\Struct{M} \mathrel{||}\joinrel\Relbar C$ (o ambos).
$\indcase{A}{(B \lif C)}$$\Struct{M} \mathrel{||}\joinrel\Relbar\indfrm$iff no$\Struct {M} \mathrel{||}\joinrel\Relbar B$ o$\Struct M \mathrel{||}\joinrel\Relbar C$ (o ambos).
$\indcase{A}{\lforall{x}{B}}$$\Struct{M} \mathrel{||}\joinrel\Relbar{\indfrm}$iff para todos$a \in \Domain{M}$,$\Struct{M[a/c]} \mathrel{||}\joinrel\Relbar\Subst{B}{c}{x}$, si$c$ no ocurre en$B$.
$\indcase{A}{\lexists{x}{B}}$$\Struct{M} \mathrel{||}\joinrel\Relbar {\indfrm}$si hay$a \in \Domain M$ tal que$\Struct{M[a/c]} \mathrel{||}\joinrel\Relbar\Subst{B}{c}{x}$, si$c$ no ocurre en$B$.

Que$x_1$,...,$x_n$ sean todas las variables libres en$A$$c_1$,,..., símbolos$c_n$ constantes no en$A$$a_1$,,...$a_n \in \Domain M$, y$s(x_i) = a_i$.

Demuestre que$\Sat[,s]{M}{A}$ iff$\Struct M[a_1/c_1,\dots,a_n/c_n] \mathrel{||}\joinrel\Relbar\Subst{\Subst{A}{c_1}{x_1}\dots}{c_n}{x_n}$.

(Este problema muestra que es posible dar una semántica para lógica de primer orden que haga prescindir de asignaciones de variables).

Problema$\PageIndex{5}$

Supongamos que$f$ es un símbolo de función no en$A(x,y)$. Demostrar que hay una estructura$\Struct{M}$$\Sat{M}{\lforall{x}{\lexists{y}{A(x,y)}}}$ tal que si hay una$\Struct M'$ tal que$\Sat{M'}{\lforall{x}{A(x,f(x))}}$.

(Este problema es un caso especial de lo que se conoce como Teorema de Skolem;$\lforall{x}{A(x,f(x))}$ se llama una forma normal de Skolem)$\lforall{x}{\lexists{y}{A(x,y)}}$.