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