Saltar al contenido principal

# 10.6: Construcción de un Modelo

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

$$\newcommand{\vectorA}[1]{\vec{#1}} % arrow$$

$$\newcommand{\vectorAt}[1]{\vec{\text{#1}}} % arrow$$

$$\newcommand{\vectorB}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} }$$

$$\newcommand{\vectorC}[1]{\textbf{#1}}$$

$$\newcommand{\vectorD}[1]{\overrightarrow{#1}}$$

$$\newcommand{\vectorDt}[1]{\overrightarrow{\text{#1}}}$$

$$\newcommand{\vectE}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash{\mathbf {#1}}}}$$

$$\newcommand{\vecs}[1]{\overset { \scriptstyle \rightharpoonup} {\mathbf{#1}} }$$

$$\newcommand{\vecd}[1]{\overset{-\!-\!\rightharpoonup}{\vphantom{a}\smash {#1}}}$$

$$\newcommand{\avec}{\mathbf a}$$ $$\newcommand{\bvec}{\mathbf b}$$ $$\newcommand{\cvec}{\mathbf c}$$ $$\newcommand{\dvec}{\mathbf d}$$ $$\newcommand{\dtil}{\widetilde{\mathbf d}}$$ $$\newcommand{\evec}{\mathbf e}$$ $$\newcommand{\fvec}{\mathbf f}$$ $$\newcommand{\nvec}{\mathbf n}$$ $$\newcommand{\pvec}{\mathbf p}$$ $$\newcommand{\qvec}{\mathbf q}$$ $$\newcommand{\svec}{\mathbf s}$$ $$\newcommand{\tvec}{\mathbf t}$$ $$\newcommand{\uvec}{\mathbf u}$$ $$\newcommand{\vvec}{\mathbf v}$$ $$\newcommand{\wvec}{\mathbf w}$$ $$\newcommand{\xvec}{\mathbf x}$$ $$\newcommand{\yvec}{\mathbf y}$$ $$\newcommand{\zvec}{\mathbf z}$$ $$\newcommand{\rvec}{\mathbf r}$$ $$\newcommand{\mvec}{\mathbf m}$$ $$\newcommand{\zerovec}{\mathbf 0}$$ $$\newcommand{\onevec}{\mathbf 1}$$ $$\newcommand{\real}{\mathbb R}$$ $$\newcommand{\twovec}[2]{\left[\begin{array}{r}#1 \\ #2 \end{array}\right]}$$ $$\newcommand{\ctwovec}[2]{\left[\begin{array}{c}#1 \\ #2 \end{array}\right]}$$ $$\newcommand{\threevec}[3]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \end{array}\right]}$$ $$\newcommand{\cthreevec}[3]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \end{array}\right]}$$ $$\newcommand{\fourvec}[4]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$$ $$\newcommand{\cfourvec}[4]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \end{array}\right]}$$ $$\newcommand{\fivevec}[5]{\left[\begin{array}{r}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$$ $$\newcommand{\cfivevec}[5]{\left[\begin{array}{c}#1 \\ #2 \\ #3 \\ #4 \\ #5 \\ \end{array}\right]}$$ $$\newcommand{\mattwo}[4]{\left[\begin{array}{rr}#1 \amp #2 \\ #3 \amp #4 \\ \end{array}\right]}$$ $$\newcommand{\laspan}[1]{\text{Span}\{#1\}}$$ $$\newcommand{\bcal}{\cal B}$$ $$\newcommand{\ccal}{\cal C}$$ $$\newcommand{\scal}{\cal S}$$ $$\newcommand{\wcal}{\cal W}$$ $$\newcommand{\ecal}{\cal E}$$ $$\newcommand{\coords}[2]{\left\{#1\right\}_{#2}}$$ $$\newcommand{\gray}[1]{\color{gray}{#1}}$$ $$\newcommand{\lgray}[1]{\color{lightgray}{#1}}$$ $$\newcommand{\rank}{\operatorname{rank}}$$ $$\newcommand{\row}{\text{Row}}$$ $$\newcommand{\col}{\text{Col}}$$ $$\renewcommand{\row}{\text{Row}}$$ $$\newcommand{\nul}{\text{Nul}}$$ $$\newcommand{\var}{\text{Var}}$$ $$\newcommand{\corr}{\text{corr}}$$ $$\newcommand{\len}[1]{\left|#1\right|}$$ $$\newcommand{\bbar}{\overline{\bvec}}$$ $$\newcommand{\bhat}{\widehat{\bvec}}$$ $$\newcommand{\bperp}{\bvec^\perp}$$ $$\newcommand{\xhat}{\widehat{\xvec}}$$ $$\newcommand{\vhat}{\widehat{\vvec}}$$ $$\newcommand{\uhat}{\widehat{\uvec}}$$ $$\newcommand{\what}{\widehat{\wvec}}$$ $$\newcommand{\Sighat}{\widehat{\Sigma}}$$ $$\newcommand{\lt}{<}$$ $$\newcommand{\gt}{>}$$ $$\newcommand{\amp}{&}$$ $$\definecolor{fillinmathshade}{gray}{0.9}$$

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