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

    \( \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

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