5.14: Nociones semánticas

Template:MathJaxZach

Dar la definición de estructuras para lenguajes de primer orden, podemos definir algunas propiedades semánticas básicas de y relaciones entre oraciones. El más simple de estos es la noción de validez de una oración. Una oración es válida si se satisface en cada estructura. Las oraciones válidas son aquellas que se satisfacen independientemente de cómo se interpreten los símbolos no lógicos en ella. Por lo tanto, las oraciones válidas también se denominan verdades lógicas —son verdaderas, es decir, satisfechas, en cualquier estructura y por lo tanto su verdad depende únicamente de los símbolos lógicos que ocurren en ellas y de su estructura sintáctica, pero no de los símbolos no lógicos ni de su interpretación.

Definición\(\PageIndex{1}\): Validity

Una sentencia\(A\) es válida,\(\Entails A\), iff\(\Sat{M}{A}\) para cada estructura\(\Struct M\).

Definición\(\PageIndex{2}\): Entailment

Un conjunto de oraciones\(\Gamma\) conlleva una oración\(A\),\(\Gamma \Entails A\), iff para cada estructura\(\Struct M\) con\(\Sat{M}{\Gamma}\),\(\Sat{M}{A}\).

Definición\(\PageIndex{3}\): Satisfiability

Un conjunto de oraciones\(\Gamma\) es satisfacible si\(\Sat{M}{\Gamma}\) por alguna estructura\(\Struct M\). Si no\(\Gamma\) es satisfecha se le llama insatisfactorio.

Proposición\(\PageIndex{1}\)

Una oración\(A\) es válida iff\(\Gamma \Entails A\) por cada conjunto de oraciones\(\Gamma\).

Prueba. Para la dirección hacia adelante, que\(A\) sea válido, y que\(\Gamma\) sea un conjunto de oraciones. Que\(\Struct M\) sea una estructura para que\(\Sat{M}{\Gamma}\). Ya que\(A\) es válido,\(\Sat{M}{A}\), de ahí\(\Gamma \Entails A\).

Para el contrapositivo de la dirección inversa, deje\(A\) ser inválido, por lo que hay una estructura\(\Struct M\) con\(\SatN{M}{A}\). Cuando\(\Gamma = \{ \ltrue \}\), ya que\(\ltrue\) es válido,\(\Sat{M}{\Gamma}\). De ahí que exista una estructura\(\Struct M\) para que\(\Sat{M}{\Gamma}\) pero\(\SatN{M}{A}\), de ahí que\(\Gamma\) no implique\(A\). ◻

Proposición\(\PageIndex{2}\)

\(\Gamma \Entails A\)iff\(\Gamma \cup \{\lnot A\}\) es insatisfactorio.

Prueba. Para la dirección hacia adelante, supongamos\(\Gamma \Entails A\) y supongamos al contrario que hay una estructura\(\Struct M\) así que eso\(\Sat{M}{\Gamma \cup \{ \lnot A \}}\). Desde\(\Sat{M}{\Gamma}\) y\(\Gamma \Entails A\),\(\Sat{M}{A}\). También, ya que\(\Sat{M}{\Gamma\cup \{ \lnot A \}}\)\(\Sat{M}{\lnot A}\), así tenemos ambos\(\Sat{M}{A}\) y\(\SatN{M}{A}\), una contradicción. De ahí que no pueda haber tal estructura\(\Struct M\), por lo que\(\Gamma \cup \{ A \}\) es insatisfactorio.

Para la dirección inversa, supongamos que\(\Gamma \cup \{ \lnot A \}\) es insatisfactorio. Entonces para cada estructura\(\Struct M\), ya sea\(\SatN{M}{\Gamma}\) o\(\Sat{M}{A}\). De ahí, para cada estructura\(\Struct M\) con\(\Sat{M}{\Gamma}\),\(\Sat{M}{A}\), entonces\(\Gamma \Entails A\). ◻

Problema\(\PageIndex{1}\)

1. Demuestre que el\(\Gamma \Entails \bot\) iff\(\Gamma\) es insatisfactorio.

2. Demuestre que\(\Gamma \cup \{A\} \Entails \bot\) iff\(\Gamma \Entails \lnot A\).

3. Supongamos que\(c\) no ocurre en\(A\) o\(\Gamma\). Demuestre que\(\Gamma \Entails \lforall{x}{A}\) iff\(\Gamma \Entails \Subst{A}{c}{x}\).

Proposición\(\PageIndex{3}\)

Si\(\Gamma \subseteq \Gamma'\) y\(\Gamma \Entails A\), entonces\(\Gamma' \Entails A\).

Prueba. Supongamos que\(\Gamma \subseteq \Gamma'\) y\(\Gamma \Entails A\). \(\Struct M\)Sea tal que\(\Sat{M}{\Gamma'}\); entonces\(\Sat{M}{\Gamma}\), y desde entonces\(\Gamma \Entails A\), eso lo conseguimos\(\Sat{M}{A}\). De ahí, siempre que\(\Sat{M}{\Gamma'}\)\(\Sat{M}{A}\), así\(\Gamma' \Entails A\). ◻

Teorema\(\PageIndex{1}\): Semantic Deduction Theorem

\(\Gamma \cup \{A\} \Entails B\)iff\(\Gamma \Entails A \lif B\).

Prueba. Para la dirección hacia adelante, deja\(\Gamma \cup \{ A \} \Entails B\) y deja\(\Struct M\) ser una estructura para que\(\Sat{M}{\Gamma}\). Si\(\Sat{M}{A}\), entonces\(\Sat{M}{\Gamma \cup \{ A \} }\), así ya que\(\Gamma \cup \{ A \}\) implica\(B\), obtenemos\(\Sat{M}{B}\). Por lo tanto\(\Sat{M}{A \lif B}\),, entonces\(\Gamma \Entails A \lif B\).

Para la dirección inversa, dejar\(\Gamma \Entails A \lif B\) y\(\Struct M\) ser una estructura para que\(\Sat{M}{\Gamma \cup \{ A \}}\). Entonces\(\Sat{M}{\Gamma}\), entonces\(\Sat{M}{A \lif B}\), y desde\(\Sat{M}{A}\),\(\Sat{M}{B}\). De ahí, siempre que\(\Sat{M}{\Gamma \cup \{ A \} }\)\(\Sat{M}{B}\), así\(\Gamma \cup \{ A \} \Entails B\). ◻

Proposición\(\PageIndex{4}\)

Dejar\(\Struct{M}\) ser una estructura, y\(A(x)\) una fórmula con una variable libre\(x\), y\(t\) un término cerrado. Entonces:

1. \(A(t) \Entails \lexists{x}{A(x)}\)

2. \(\lforall{x}{A(x)} \Entails A(t)\)

Prueba.

1. Supongamos\(\Sat{M}{A(t)}\). Let \(s\) be a variable assignment with \(s(x) = \Value{t}{M}\). Then \(\Sat[,s]{M}{A(t)}\) since \(A(t)\) is a sentence. By Proposition 5.13.3, \(\Sat[,s]{M}{A(x)}\). By Proposition 5.12.4, \(\Sat{M}{\lexists{x}{A(x)}}\).

2. Ejercicio.

◻

Problema\(\PageIndex{2}\)

Completar el comprobante de Proposición\(\PageIndex{4}\).