La integridad es una propiedad de los sistemas de prueba. A grandes rasgos, podemos decir que es una prueba de sistema iff verdad implica derivability. Sin embargo, las pruebas de FOL que encontramos habitualmente en los textos de lógica, es decir, "Henkin-pruebas", no parecen hacer referencia a ningún sistema deductivo.
Considere la siguiente prueba de dibujo:
Lema 1 (Modelo De Existencia). $\Gamma$ es consistente $\Rightarrow \Gamma$ es válido
Prueba. Deje $\mathcal{L}$ ser nuestra referencia de lenguaje. Una prueba usual va más o menos a lo largo de las líneas de
- Deje $\Gamma$ ser coherente.
- Extender $\Gamma$ a un máximo conjunto consistente $\Delta$
- Mostrar que $\Delta$ preserva la consistencia y que $\Gamma \subseteq \Delta$
- Definir una valoración $v$ $\Delta$ tal que $v(\psi)=1$ fib $\psi \in \Delta$ para todos los atómica $\psi \in \mathcal{L}$
- Definir $v$'s única extensión de $\bar v$ como de costumbre.
- A continuación, $\bar v \vDash \Delta$ y, desde $\Gamma \subseteq \Delta$,
- $\bar v \vDash \Gamma$. $\qquad \qquad \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \Box$
Teorema (Integridad) $\Gamma \vDash \varphi \Rightarrow \Gamma \vdash \varphi$
Prueba. Por contraposición. Deje $\Gamma \nvdash \varphi$. A continuación, $\Gamma \cup \{\neg \varphi\}$ es consistente y, por el Modelo de Existencia Lema, tiene un modelo. Por lo tanto, $\Gamma \nvDash \varphi$. $\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad \Box$
Tenga en cuenta que no me hacen ninguna mención explícita a cualquier intención de sistema deductivo. De hecho, me parece la única noción sintáctica que necesito es:
Definición (Consistencia) Un conjunto de oraciones $\Gamma$ es consistente si no es $\varphi$ tal que $\Gamma \nvdash \varphi$.
Pero sin embargo, puedo definir esta noción en general, de cualquier sistema deductivo.
Ahora me parecía haber demostrado integridad. Pero la integridad de los cuales deductivo sistema? No sé. Para la citada prueba de integridad, que no lo hacen explícito de cualquier axioma o regla de inferencia. Esto no parece extraño?
Si esto es así, a mí me parece que yo pueda aplicar el mismo argumento , mutatis mutandis, para cualquier otro sistema deductivo (incluso aquellos para los que no están completas?).
Pregunta. ¿Cuál es la función de la prueba del sistema en un Henkin a prueba de Integridad?
Soy probablemente falta algo. Así puede alguien explicar este tema en los detalles?