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}\)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.
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.
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})\).
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.
Supongamos que\(\Gamma\) es completo, consistente y saturado.
-
\(\lexists{x}{A(x)} \in \Gamma\) iff \(A(t) \in \Gamma\) for at least one closed term \(t\).
-
\(\lforall{x}{A(x)} \in \Gamma\) iff \(A(t) \in \Gamma\) for all closed terms \(t\).
Comprobante.
-
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\).
-
Ejercicio.
◻