Saltar al contenido principal
LibreTexts Español

10.4: Expansión Henkin

  • Page ID
    103563
  • \( \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

    Parte del reto para probar el teorema de integridad es que el modelo que construimos a partir de un conjunto consistente completo\(\Gamma\) debe hacer que todas las fórmulas cuantificadas sean\(\Gamma\) verdaderas. Para garantizar esto, utilizamos un truco debido a Leon Henkin. En esencia, el truco consiste en expandir el lenguaje por infinitamente muchos símbolos constantes y agregar, para cada fórmula con una variable libre\(A(x)\) una fórmula de la forma\(\lexists{x}{A(x)} \lif A(c)\), donde\(c\) está uno de los nuevos símbolos constantes. Cuando construimos la estructura satisfactoria\(\Gamma\), esto garantizará que cada oración existencial verdadera tenga un testimonio entre las nuevas constantes.

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

    Si\(\Gamma\) es consistente en\(\Lang L\) y\(\Lang L'\) se obtiene de\(\Lang L\) agregando un conjunto infinitamente contable de nuevos símbolos constantes\(\Obj d_0\),\(\Obj d_1\),..., entonces\(\Gamma\) es consistente en \(\Lang L'\).

    Definición\(\PageIndex{1}\): Saturated set

    Un conjunto\(\Gamma\) de fórmulas de un idioma\(\Lang {L}\) está saturado iff para cada fórmula\(A(x) \in \Frm[L]\) con una variable libre\(x\) hay un símbolo constante\(c \in \Lang{L}\) tal que\(\lexists{x}{A(x)} \lif A(c) \in \Gamma\).

    Se utilizará la siguiente definición en la prueba del siguiente teorema.

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

    Seamos\(\Lang L'\) como en la Proposición\(\PageIndex{1}\). Fijar una enumeración\(A_0(x_0)\),\(A_1(x_1)\),... de todas las fórmulas\(A_i(x_i)\) de\(\Lang L'\) en las que una variable (\(x_i\)) se produce libre. Definimos las oraciones\(D_n\) por inducción sobre\(n\).

    \(c_0\)Sea el primer símbolo constante entre los que\(\Obj d_i\) añadimos al\(\Lang{L}\) que no se da en\(A_0(x_0)\). Suponiendo que\(D_0\),..., ya se\(D_{n-1}\) han definido, dejemos\(c_n\) ser los primeros entre los nuevos símbolos constantes\(\Obj d_i\) que no se dan ni en\(D_0\),...,\(D_{n-1}\) ni en\(A_n(x_n)\).

    Ahora\(D_{n}\) déjese ser la fórmula\(\lexists{x_{n}}{A_{n}(x_{n})} \lif A_{n}(c_{n})\).

    Lema\(\PageIndex{1}\)

    Cada conjunto consistente se\(\Gamma\) puede extender a un conjunto consistente saturado\(\Gamma'\).

    Comprobante. Dado un conjunto consistente de oraciones\(\Gamma\) en un idioma\(\Lang{L}\), expanda el lenguaje agregando un conjunto contablemente infinito de nuevos símbolos constantes para formar\(\Lang{L'}\). Por Proposición\(\PageIndex{1}\),\(\Gamma\) sigue siendo consistente en el lenguaje más rico. Además,\(D_i\) seamos como en Definición\(\PageIndex{2}\). Dejar\[\begin{aligned} \Gamma_0 & = \Gamma \\ \Gamma_{n+1} & = \Gamma_n \cup \{D_n \}\end{aligned}\] es decir,\(\Gamma_{n+1} = \Gamma \cup \{ D_0, \dots, D_n \}\), y dejar\(\Gamma' = \bigcup_{n} \Gamma_n\). \(\Gamma'\)está claramente saturado.

    Si\(\Gamma'\) fueran inconsistentes, entonces para algunos\(n\),\(\Gamma_n\) sería inconsistente (Ejercicio: explicar por qué). Entonces, para demostrar que\(\Gamma'\) es consistente basta con mostrar, por inducción en\(n\), que cada conjunto\(\Gamma_n\) es consistente.

    La base de inducción es simplemente la afirmación que\(\Gamma_0 = \Gamma\) es consistente, que es la hipótesis del teorema. Para el paso de inducción, supongamos que eso\(\Gamma_{n}\) es consistente pero\(\Gamma_{n+1} = \Gamma_n \cup \{D_n\}\) es inconsistente. Recordemos\(D_n\) es decir\(\lexists{x_{n}}{A_{n}(x_n)} \lif A_{n}(c_{n})\), donde\(A_n(x_n)\) es una fórmula de\(\Lang{L'}\) con solo la variable\(x_n\) libre. Por cierto hemos elegido el\(c_n\) (ver Definición\(\PageIndex{2}\)),\(c_n\) no ocurre en\(A_n(x_n)\) ni en\(\Gamma_n\).

    Si\(\Gamma_n \cup \{D_n\}\) es inconsistente, entonces\(\Gamma_n \Proves \lnot D_n\), y por lo tanto ambos de lo siguiente sostienen:\[\Gamma_n \Proves \lexists{x_n}{A_n(x_n)} \qquad \Gamma_n \Proves \lnot A_n(c_n)\nonumber\] Dado que\(c_n\) no ocurre en\(\Gamma_n\) o en\(A_n(x_n)\), Teoremas 8.11.1 y 9.10.1 aplica. De\(\Gamma_n \Proves \lnot A_n(c_n)\), obtenemos\(\Gamma_n \Proves \lforall{x_n}{\lnot A_n(x_n)}\). Así tenemos que ambos\(\Gamma_n \Proves \lexists{x_n}{A_n(x_n)}\) and \(\Gamma_n \Proves \lforall{x_n}{\lnot A_n(x_n)}\), así\(\Gamma_n\) mismo es inconsistente. (Obsérvese que\(\lforall{x_n}{\lnot A_n(x_n)} \Proves \lnot\lexists{x_n}{A_n(x_n)}\).) Contradicción: se\(\Gamma_n\) suponía que era consistente. De ahí\(\Gamma_n \cup \{ D_n\}\) que sea consistente. ◻

    Ahora mostraremos que los conjuntos completos y consistentes que están saturados tienen la propiedad de que contiene una oración universalmente cuantificada si contiene todas sus instancias y contiene una oración cuantificada existencialmente iff contiene al menos una instancia . Usaremos esto para mostrar que la estructura que generaremos a partir de un conjunto completo, consistente y saturado hace que todas sus oraciones cuantificadas sean verdaderas.

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

    Supongamos que\(\Gamma\) es completo, consistente y saturado.

    1. \(\lexists{x}{A(x)} \in \Gamma\) iff \(A(t) \in \Gamma\) for at least one closed term \(t\).

    2. \(\lforall{x}{A(x)} \in \Gamma\) iff \(A(t) \in \Gamma\) for all closed terms \(t\).

    Comprobante.

    1. Primero supongamos eso\(\lexists{x}{A(x)} \in \Gamma\). Porque\(\Gamma\) está saturado,\((\lexists{x}{A(x)} \lif A(c)) \in \Gamma\) para algún símbolo constante\(c\). Por Proposiciones 8.10.3 y 9.9.3, ítem (1), y Proposición 10.3.1 (1),\(A(c) \in \Gamma\).

      Para la otra dirección, la saturación no es necesaria: Supongamos\(A(t) \in \Gamma\). Después\(\Gamma \Proves \lexists{x}{A(x)}\) por las Proposiciones 8.11.1 y 9.10.1, ítem (1). Por Proposición 10.3.1 (1),\(\lexists{x}{A(x)} \in \Gamma\).

    2. Ejercicio.


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