Loading [MathJax]/jax/output/HTML-CSS/jax.js
Saltar al contenido principal
Library homepage
 

Text Color

Text Size

 

Margin Size

 

Font Type

Enable Dyslexic Font
LibreTexts Español

5.12: Asignaciones Variables

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

Template:MathJaxZach

Una asignación de variabless 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érminot, y si una fórmulaA se satisface o no en una estructura con respecto as, sólo depende de las asignacioness que haga a las variables ent 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 ent dan el mismo valor, y queA 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 deA.

Proposición5.12.1

Si las variables en un términot están entrex1,...xn,, ys1(xi)=s2(xi) parai=1,...n, entonces\Value[s1]tM=\Value[s2]tM.

Comprobante. Por inducción sobre la complejidad det. Para el caso base,t puede ser un símbolo constante o una de las variablesx1,...,xn. Sit=c, entonces\Value[s1]tM=\AssigncM=\Value[s2]tM. Sit=xi,s1(xi)=s2(xi) por la hipótesis de la proposición, y así\Value[s1]tM=s1(xi)=s2(xi)=\Value[s2]tM.

Para el paso inductivo, asumir quet=\Atomft1,,tk y que el reclamo se sostiene parat1,...,tk. 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}\]

Paraj=1,,k, las variables detj se encuentran entrex1,,xn. Entonces por hipótesis de inducción,\Value[s1]tjM=\Value[s2]tjM. 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ón5.12.2

Si las variables libres enA están entrex1,...,xn, ys1(xi)=s2(xi) parai=1,...,n, entonces\Sat[,s1]MA iff\Sat[,s2]MA.

Comprobante. Utilizamos la inducción en la complejidad deA. Para el caso base, dondeA es atómico,A puede ser:\lfalse,\AtomRt1,,tk para un predicadoR y términosk -placet1,...tk, o\eq[t1][t2] para términost1 yt2.

  1. \indcaseA\lfalseambos\SatN[,s1]MA y\SatN[,s2]MA.

  2. \indcaseA\AtomRt1,,tkdejar\Sat[,s1]M\indfrm. Entonces\Value[s1]t1M,,\Value[s1]tkM\AssignRM. Pori=1,...,k,\Value[s1]tiM=\Value[s2]tiM por Proposición5.12.1. Entonces también tenemos\Value[s2]tiM,,\Value[s2]tkM\AssignRM.

  3. \indcaseA\eq[t1][t2]supongamos\Sat[,s1]M\indfrm. Entonces\Value[s1]t1M=\Value[s1]t2M. Entonces,\Value[s2]t1M=\Value[s1]t1M(by Proposition 5.12.1)=\Value[s1]t2M(since \Sat[,s1]M\eq[t1][t2])=\Value[s2]t2M(by Proposition 5.12.1), entonces\Sat[,s2]M\eq[t1][t2].

Ahora asuma\Sat[,s1]MB iff\Sat[,s2]MB para todas las fórmulasB menos complejas queA. El paso de inducción procede por casos determinados por el operador principal deA. 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órmulasB deA. Las variables libres deB se encuentran entre las deA. Así, sis1 ys2 acuerdan las variables libres deA, también coinciden en las deB, y la hipótesis de inducción se aplica aB.

  1. \indcaseA¬Bsi\Sat[,s1]M\indfrm, entonces\SatN[,s1]MB, así por la hipótesis de inducción,\SatN[,s2]MB, de ahí\Sat[,s2]M\indfrm.

  2. \indcaseABCejercicio.

  3. \indcaseABCsi\Sat[,s1]M\indfrm, entonces\Sat[,s1]MB o\Sat[,s1]MC. Por hipótesis de inducción,\Sat[,s2]MB o\Sat[,s2]MC, así\Sat[,s2]M\indfrm.

  4. \indcaseAB\lifCejercicio.

  5. \indcaseA\lexistsxBsi\Sat[,s1]M\indfrm, hay unax -variantes1 des1 para que\Sat[,s1]MB. s2Sea lax -variante des2 que le asigne lo mismo ax lo que haces1. Las variables libres deB se encuentran entrex1,...xn, yx. s1(xi)=s2(xi), ya ques1 ys2 sonx -variantes des1 ys2, respectivamente, y por hipótesiss1(xi)=s2(xi). s1(x)=s2(x)por la forma en que hemos definidos2. Entonces la hipótesis de inducción se aplica aB ys1,s2, entonces\Sat[,s2]MB. De ahí que haya unax -variante des2 que satisfagaB, y así\Sat[,s2]M\indfrm.

  6. \indcaseA\lforallxBejercicio.

Por inducción, obtenemos ese\Sat[,s1]MA iff\Sat[,s2]MA siempre que las variables libres enA se encuentren entrex1,...,xn ys1(xi)=s2(xi) parai=1,...,n. ◻

Problema5.12.1

Completar el comprobante de Proposición5.12.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.

Corolario5.12.1

SiA es una oración ys una asignación variable, entonces\Sat[,s]MA iff\Sat[,s]MA para cada asignación de variables.

Comprobante. Dejars ser cualquier asignación de variables. Ya queA es una oración, no tiene variables libres, y así cada asignación de variables asignas trivialmente las mismas cosas a todas las variables libres deA como lo haces. Entonces se cumple la condición de Proposición5.12.2, y tenemos\Sat[,s]MA iff\Sat[,s]MA. ◻

Definición5.12.1

SiA es una oración, decimos que una estructura\StructM satisfaceA,\SatMA, iff\Sat[,s]MA para todas las asignaciones de variabless.

Si\SatMA, también simplemente decimos queA es cierto en\StructM.

Proposición5.12.3

Dejar\StructM ser una estructura,A ser una oración, ys una asignación variable. \SatMAiff\Sat[,s]MA.

Comprobante. Ejercicio. ◻

Problema5.12.2

Probar Proposición5.12.3.

Proposición5.12.4

Supongamos queA(x) solo contienex libre, y\StructM es una estructura. Entonces:

  1. \SatM\lexistsxA(x)iff\Sat[,s]MA(x) para al menos una asignación de variabless.

  2. \SatM\lforallxA(x)iff\Sat[,s]MA(x) para todas las asignaciones de variabless.

Comprobante. Ejercicio. ◻

Problema5.12.3

Demostrar Proposición5.12.4.

Problema5.12.4

Supongamos que\LangL es un lenguaje sin símbolos de función. Dada una estructura\StructM,c un símbolo constante ya\DomainM,\StructM[a/c] definir como la estructura que es igual\StructM, excepto eso\AssigncM[a/c]=a. Definir\StructM||\joinrel\RelbarA para oracionesA por:

  1. \indcaseA\lfalseno\StructM||\joinrel\Relbar\indfrm.

  2. \indcaseA\AtomRd1,,dn\StructM||\joinrel\Relbar\indfrmiff\Assignd1M,,\AssigndnM\AssignRM.

  3. \indcaseA\eq[d1][d2]\StructM||\joinrel\Relbar\indfrmiff\Assignd1M=\Assignd2M.

  4. \indcaseA¬B\StructM||\joinrel\Relbar\indfrmiff no\StructM||\joinrel\RelbarB.

  5. \indcaseA(BC)\StructM||\joinrel\Relbar\indfrmiff\StructM||\joinrel\RelbarB y\StructM||\joinrel\RelbarC.

  6. \indcaseA(BC)\StructM||\joinrel\Relbar\indfrmiff\StructM||\joinrel\RelbarB o\StructM||\joinrel\RelbarC (o ambos).

  7. \indcaseA(B\lifC)\StructM||\joinrel\Relbar\indfrmiff no\StructM||\joinrel\RelbarB o\StructM||\joinrel\RelbarC (o ambos).

  8. \indcaseA\lforallxB\StructM||\joinrel\Relbar\indfrmiff para todosa\DomainM,\StructM[a/c]||\joinrel\Relbar\SubstBcx, sic no ocurre enB.

  9. \indcaseA\lexistsxB\StructM||\joinrel\Relbar\indfrmsi haya\DomainM tal que\StructM[a/c]||\joinrel\Relbar\SubstBcx, sic no ocurre enB.

Quex1,...,xn sean todas las variables libres enAc1,,..., símboloscn constantes no enAa1,,...an\DomainM, ys(xi)=ai.

Demuestre que\Sat[,s]MA iff\StructM[a1/c1,,an/cn]||\joinrel\Relbar\Subst\SubstAc1x1cnxn.

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

Problema5.12.5

Supongamos quef es un símbolo de función no enA(x,y). Demostrar que hay una estructura\StructM\SatM\lforallx\lexistsyA(x,y) tal que si hay una\StructM tal que\SatM\lforallxA(x,f(x)).

(Este problema es un caso especial de lo que se conoce como Teorema de Skolem;\lforallxA(x,f(x)) se llama una forma normal de Skolem)\lforallx\lexistsyA(x,y).


This page titled 5.12: Asignaciones Variables is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .

Support Center

How can we help?

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