10.2: Esquema de la Prueba
- Page ID
- 103595
La prueba del teorema de integridad es un poco compleja, y al leerlo por primera vez, es fácil perderse. Así que vamos a delinear la prueba. El primer paso es un cambio de perspectiva, que nos permite ver una ruta a una prueba. Cuando se piensa que la integridad es “siempre que\(\Gamma \Entails A\) entonces”\(\Gamma \Proves A\), puede ser difícil incluso llegar a una idea: para demostrar que\(\Gamma \Proves A\) tenemos que encontrar una derivación, y no se parece a la hipótesis que nos\(\Gamma \Entails A\) ayuda para esto de ninguna manera . Para algunos sistemas de prueba es posible construir directamente una derivación, pero tomaremos un enfoque ligeramente diferente. El cambio de perspectiva que se requiere es éste: la integridad también puede formularse como: “si\(\Gamma\) es consistente, es satisfecha”. Quizás podamos usar la información\(\Gamma\) junto con la hipótesis de que es consistente construir una estructura que satisfaga cada oración en\(\Gamma\). Después de todo, sabemos qué tipo de estructura estamos buscando: ¡una que sea como la\(\Gamma\) describe!
Si solo\(\Gamma\) contiene oraciones atómicas, es fácil construir un modelo para ello. Supongamos que las oraciones atómicas son\(\Atom{P}{a_1,\dots,a_n}\) where the \(a_i\) are constant symbols. todas de la forma Todo lo que tenemos que hacer es idear un dominio\(\Domain{M}\) y una asignación para\(P\) eso\(\Sat{M}{\Atom{P}{a_1,\ldots,a_n}}\). Pero eso no es muy difícil: poner\(\Domain{M} = \Nat\)\(\Assign{\Obj c_i}{M} = i\), y para cada\(\Atom{P}{a_1,\ldots,a_n} \in \Gamma\), poner la tupla\(\tuple{k_1, \dots, k_n}\) en\(\Assign{P}{M}\), donde\(k_i\) está el índice del símbolo constante\(a_i\) (es decir, \(a_i \ident \Obj c_{k_i}\)).
Ahora supongamos que\(\Gamma\) contiene alguna fórmula\(\lnot B\), con\(B\) atómica. Nos puede preocupar que la construcción de\({\Struct{M}}\) interfiera con la posibilidad de hacer\(\lnot B\) realidad. Pero aquí es donde\(\Gamma\) entra la consistencia de: si\(\lnot B \in \Gamma\), entonces\(B \notin \Gamma\), o de lo contrario\(\Gamma\) sería inconsistente. Y si\(B \notin \Gamma\), entonces según nuestra construcción de\({\Struct{M}}\),\(\SatN{M}{B}\), entonces\(\Sat{M}{\lnot B}\). Hasta el momento tan bueno.
¿Y si\(\Gamma\) contiene fórmulas complejas y no atómicas? Decir que contiene\(A \land B\). Para que eso sea cierto, debemos proceder como si ambos\(A\) y\(B\) estuvieran adentro\(\Gamma\). Y si\(A \lor B \in \Gamma\), entonces tendremos que hacer que al menos uno de ellos sea cierto, es decir, proceder como si uno de ellos estuviera adentro\(\Gamma\).
Esto sugiere la siguiente idea: agregamos fórmulas adicionales para\(\Gamma\) (a) mantener el conjunto resultante consistente y (b) asegurarnos de que para cada oración atómica posible\(A\), o bien\(A\) esté en el conjunto resultante, o\(\lnot A\) is, y (c) tal que, siempre que\(A \land B\) esté en el set, así son ambos\(A\) y\(B\), si\(A \lor B\) está en el set, al menos uno de\(A\) o también lo\(B\) es, etc. seguimos haciendo esto (potencialmente para siempre). Llame al conjunto de todas las fórmulas así agregadas\(\Gamma^*\). Entonces nuestra construcción anterior nos proporcionaría una estructura\(\Struct{M}\) para la cual podríamos probar, por inducción, que satisface todas las oraciones en\(\Gamma^*\), y de ahí también todas las oraciones en\(\Gamma\) since\(\Gamma \subseteq \Gamma^*\). Resulta que con garantizar (a) y (b) es suficiente. Un conjunto de oraciones para las cuales (b) sostiene se denomina completo. Por lo que nuestra tarea será extender el conjunto consistente\(\Gamma\) a un conjunto consistente y completo\(\Gamma^*\).
Hay una arruga en este plan: si\(\lexists{x}{A(x)} \in \Gamma\) esperaríamos poder escoger algún símbolo constante\(c\) y sumar\(A(c)\) en este proceso. Pero, ¿cómo sabemos que siempre podemos hacer eso? Quizás solo tenemos unos pocos símbolos constantes en nuestro idioma, y para cada uno de ellos tenemos\(\lnot A(c) \in \Gamma\). Tampoco podemos agregar\(A(c)\), ya que esto haría que el conjunto fuera inconsistente, y no sabríamos si\(\Struct{M}\) tiene que hacer\(A(c)\) o\(\lnot A(c)\) verdad. Además, podría suceder que solo\(\Gamma\) contenga oraciones en un lenguaje que no tenga símbolos constantes en absoluto (por ejemplo, el lenguaje de la teoría de conjuntos).
La solución a este problema es simplemente agregar infinitamente muchas constantes al principio, más oraciones que las conecten con los cuantificadores de la manera correcta. (Por supuesto, tenemos que verificar que esto no puede introducir una inconsistencia).
Nuestra construcción original funciona bien si solo tenemos símbolos constantes en las oraciones atómicas. Pero el lenguaje también podría contener símbolos de función. En ese caso, podría ser complicado encontrar las funciones adecuadas\(\Nat\) para asignar a estos símbolos de función para que todo funcione. Entonces aquí hay otro truco: en lugar de usar\(i\) para interpretar\(\Obj c_i\), solo toma el conjunto de símbolos constantes en sí mismo como el dominio. Entonces\(\Struct M\) puede asignarse cada símbolo constante a sí mismo:\(\Assign{\Obj c_i}{M} = \Obj c_i\). Pero, ¿por qué no ir hasta el final? ¡Que\(\Domain{M}\) sean todos los términos del idioma! Si hacemos esto, hay una asignación obvia de funciones (que toman términos como argumentos y tienen términos como valores) a símbolos de función: asignamos al símbolo de función\(\Obj f^n_i\) la función que, dados\(n\) términos\(t_1\),...,\(t_n\) como input, produce el término\(\Obj f^n_i(t_1, \dots, t_n)\) como valor.
La última pieza del rompecabezas es con qué hacer\(\eq[][]\). El símbolo predicado\(\eq[][]\) tiene una interpretación fija:\(\Sat{M}{\eq[t][t']}\) iff\(\Value{t}{M} = \Value{t'}{M}\). Ahora bien, si configuramos las cosas para que el valor de un término\(t\) sea\(t\) en sí mismo, entonces esta estructura no hará que ninguna oración de la forma sea\(\eq[t][t']\) verdadera a menos que\(t\) y\(t'\) sean uno y el mismo término. Y por supuesto esto es un problema, ya que básicamente toda teoría interesante en un lenguaje con símbolos de función tendrá como teoremas oraciones\(\eq[t][t']\) donde\(t\) y no\(t'\) son el mismo término (e.g., en teorías de la aritmética:\(\eq[(\Obj 0+ \Obj 0)][\Obj 0]\)). Para resolver este problema, cambiamos el dominio de\(\Struct M\): en lugar de usar términos como objetos en\(\Domain{M}\), usamos conjuntos de términos, y cada conjunto es para que contenga todos aquellos términos que las oraciones en\(\Gamma\) requieren que sean iguales. Entonces, por ejemplo, si\(\Gamma\) es una teoría de la aritmética, uno de estos conjuntos contendrá:\(\Obj 0\)\((\Obj 0 + \Obj 0)\)\((\Obj 0 \times \Obj 0)\),,, etc. Este será el conjunto al que asignemos\(\Obj 0\), y resultará que este conjunto es también el valor de todos los términos en ella, e.g., también de\((\Obj 0 + \Obj 0)\). Por lo tanto, la frase\(\eq[(\Obj 0+ \Obj 0)][\Obj 0]\) será cierta en esta estructura revisada.
Entonces esto es lo que haremos. Primero investigamos las propiedades de conjuntos consistentes completos, en particular probamos que un conjunto consistente completo contiene\(A \land B\) iff contiene ambos\(A\) y\(B\),\(A \lor B\) iff contiene al menos uno de ellos, etc. ( Proposición 10.3.1). Después definimos e investigamos conjuntos de oraciones “saturadas”. Un conjunto saturado es aquel que contiene condicionales que vinculan cada oración cuantificada con instancias de la misma (Definición 10.4.2). Mostramos que cualquier conjunto consistente Luego\(\Gamma\) can always be extended to a saturated set \(\Gamma'\) (Lemma 10.4.1). If a set is consistent, saturated, and complete it also has the property that it contains \(\lexists{x}{A(x)}\) iff it contains \(A(t)\) for some closed term \(t\) and \(\lforall{x}{A(x)}\) iff it contains \(A(t)\) for all closed terms \(t\) (Proposition 10.4.2). tomaremos el conjunto consistente saturado\({\Gamma'}\) y mostraremos que se puede extender a un conjunto saturado, consistente y completo\(\Gamma^*\) (Lema 10.5.1). Este conjunto\(\Gamma^*\) es lo que usaremos para definir nuestro modelo de términos\(\Struct M(\Gamma^*)\). El término modelo tiene como dominio el conjunto de términos cerrados, y la interpretación de sus símbolos predicados viene dada por las oraciones atómicas en\(\Gamma^*\) (Definición 10.6.1). Usaremos las propiedades de conjuntos consistentes completos saturados para mostrar que efectivamente\(\Sat{M(\Gamma^*)}{A}\) iff\(A \in \Gamma^*\) (Lemma 10.6.1), y por lo tanto en particular,\(\Sat{M(\Gamma^*)}{\Gamma}\). Finalmente, consideraremos cómo definir un modelo de término si\(\Gamma\) contains \(\eq[][]\) as well (Definition 10.7.3) and show that it satisfies \(\Gamma^*\) (Lemma 10.7.1).