Saltar al contenido principal

# 10.6: Construcción de un Modelo


Template:MathJaxZach

En este momento no nos preocupa$$\eq[][]$$, i.e., we only want to show that a consistent set $$\Gamma$$ of sentences not containing $$\eq[][]$$ is satisfiable. We first extend $$\Gamma$$ to a consistent, complete, and saturated set $$\Gamma^*$$. In this case, the definition of a model $$\Struct{M(\Gamma^*)}$$ is simple: We take the set of closed terms of $$\Lang{L'}$$ as the domain. We assign every constant symbol to itself, and make sure that more generally, for every closed term $$t$$, $$\Value{t}{M(\Gamma^*)} = t$$. The predicate symbols are assigned extensions in such a way that an atomic sentence is true in $$\Struct{M(\Gamma^*)}$$ iff it is in $$\Gamma^*$$. This will obviously make all the atomic sentences in $$\Gamma^*$$ true in $$\Struct{M(\Gamma^*)}$$. The rest are true provided the $$\Gamma^*$$ we start with is consistent, complete, and saturated.

Definición$$\PageIndex{1}$$: Term model

$$\Gamma^*$$Sea un conjunto completo y consistente, saturado de oraciones en un idioma$$\Lang L$$. El término modelo$$\Struct M(\Gamma^*)$$ de$$\Gamma^*$$ es la estructura definida de la siguiente manera:

1. El dominio$$\Domain{M(\Gamma^*)}$$ es el conjunto de todos los términos cerrados de$$\Lang L$$.

2. La interpretación de un símbolo constante$$c$$ es$$c$$ en sí misma:$$\Assign{c}{M(\Gamma^*)} = c$$.

3. Al símbolo de función$$f$$ se le asigna la función que, dado como argumentos los términos cerrados$$t_1$$,...$$t_n$$, tiene como valor el término cerrado$$f(t_1, \dots, t_n)$$:$\Assign{f}{M(\Gamma^*)}(t_1, \dots, t_n) = f(t_1,\dots, t_n)\nonumber$

4. Si$$R$$ es un símbolo de predicado$$n$$ -place, entonces$\tuple{t_1, \dots, t_n} \in \Assign{R}{M(\Gamma^*)} \text{ iff } \Atom{R}{t_1, \dots, t_n} \in \Gamma^*.\nonumber$

Una estructura$$\Struct{M}$$ may make an existentially quantified sentence $$\lexists{x}{A(x)}$$ true without there being an instance $$A(t)$$ that it makes true. Una estructura$$\Struct{M}$$ may make all instances $$A(t)$$ of a universally quantified sentence $$\lforall{x}{A(x)}$$ true, without making $$\lforall{x}{A(x)}$$ true. Esto se debe a que en general no todos los elementos de$$\Domain{M}$$ es el valor de un término cerrado ($$\Struct{M}$$puede no estar cubierto). Esta es la razón por la que la relación de satisfacción se define a través de asignaciones variables. Sin embargo, para nuestro modelo de términos$$\Struct{M(\Gamma^*)}$$ esto no sería necesario, porque está cubierto. Este es el contenido del siguiente resultado.

Proposición$$\PageIndex{1}$$

$$\Struct M(\Gamma^*)$$Sea el término modelo de Definición$$\PageIndex{1}$$.

1. $$\Sat{M(\Gamma^*)}{\lexists{x}{A(x)}}$$iff$$\Sat{M}{A(t)}$$ por al menos un término$$t$$.

2. $$\Sat{M(\Gamma^*)}{\lforall{x}{A(x)}}$$iff$$\Sat{M}{A(t)}$$ para todos los términos$$t$$.

Comprobante.

1. Por Proposición 5.12.4,$$\Sat{M(\Gamma^*)}{\lexists{x}{A(x)}}$$ iff para al menos una asignación variable$$s$$,$$\Sat[,s]{M(\Gamma^*)}{A(x)}$$. Como$$\Domain{M(\Gamma^*)}$$ consiste en los términos cerrados de$$\Lang{L}$$, este es el caso si hay al menos un término cerrado$$t$$ tal que$$s(x) = t$$ y$$\Sat[,s]{M(\Gamma^*)}{A(x)}$$. Por Proposición 5.13.3,$$\Sat[,s]{M(\Gamma^*)}{A(x)}$$ iff$$\Sat[,s]{M(\Gamma^*)}{A(t)}$$, donde$$s(x) = t$$. Por la Proposición 5.12.3,$$\Sat[,s]{M(\Gamma^*)}{A(t)}$$ iff$$\Sat{M(\Gamma^*)}{A(t)}$$, ya que$$A(t)$$ es una oración.

2. Ejercicio.

Problema$$\PageIndex{1}$$

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

Lema$$\PageIndex{1}$$: Truth Lemma

Supongamos$$A$$ does not contain $$\eq[][]$$. Then$$\Sat{M(\Gamma^*)}{A}$$ iff$$A \in \Gamma^*$$.

Comprobante. Demostramos ambas direcciones simultáneamente, y por inducción en$$A$$.

1. $$\indcase{A}{\lfalse}$$ $${\SatN{M(\Gamma^*)}{\lfalse}}$$ by definition of satisfaction. On the other hand, $$\lfalse \notin \Gamma^*$$ since $$\Gamma^*$$ is consistent.

2. $$\indcase{A}{R(t_1, \dots, t_n)}$$ $$\Sat{M(\Gamma^*)}{\Atom{R}{t_1, \dots, t_n}}$$ iff $$\tuple{t_1, \dots, t_n} \in \Assign{R}{M(\Gamma^*)}$$ (by the definition of satisfaction) iff $$R(t_1, \dots, t_n) \in \Gamma^*$$ (by the construction of $$\Struct M(\Gamma^*)$$).

3. $$\indcase{A}{\lnot B}$$ $$\Sat{M(\Gamma^*)}{\indfrm}$$ iff $${\SatN{M(\Gamma^*)}{B}}$$ (by definition of satisfaction). By induction hypothesis, $${\SatN{M(\Gamma^*)}{B}}$$ iff $$B \notin \Gamma^*$$. Since $$\Gamma^*$$ is consistent and complete, $$B \notin \Gamma^*$$ iff $$\lnot B \in \Gamma^*$$.

4. $$\indcase{A}{B \land C}$$ exercise.

5. $$\indcase{A}{B \lor C}$$ $$\Sat{M(\Gamma^*)}{\indfrm}$$ iff $$\Sat{M(\Gamma^*)}{B}$$ or $$\Sat{M(\Gamma^*)}{C}$$ (by definition of satisfaction) iff $$B \in \Gamma^*$$ or $$C \in \Gamma^*$$ (by induction hypothesis). This is the case iff $$(B \lor C) \in \Gamma^*$$ (by Proposition 10.3.1(3)).

6. $$\indcase{A}{B \lif C}$$ exercise.

7. $$\indcase{A}{\lforall{x}{B(x)}}$$ exercise.

8. $$\indcase{A}{\lexists{x}{B(x)}}$$ $$\Sat{M(\Gamma^*)}{\indfrm}$$ iff $$\Sat{M(\Gamma^*)}{B(t)}$$ for at least one term $$t$$ (Proposition $$\PageIndex{1}$$). By induction hypothesis, this is the case iff $$B(t) \in \Gamma^*$$ for at least one term $$t$$. By Proposition 10.4.2, this in turn is the case iff $$\lexists{x}{B(x)} \in \Gamma^*$$.

Problema$$\PageIndex{2}$$

Completar el comprobante de Lemma$$\PageIndex{1}$$.

This page titled 10.6: Construcción de un Modelo is shared under a CC BY license and was authored, remixed, and/or curated by Richard Zach et al. (Open Logic Project) .