Saltar al contenido principal
Library homepage
 
LibreTexts Español

10.6: Construcción de un Modelo

  • Page ID
    103600
  • \( \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}}\)

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