8.12: Solidez

Template:MathJaxZach

Un sistema de derivación, como el cálculo secuente, es sólido si no puede derivar cosas que realmente no se sostienen. Por lo tanto, la solidez es una especie de propiedad de seguridad garantizada para los sistemas de derivación. Dependiendo de qué prueba de propiedad teórica esté en cuestión, nos gustaría saber por ejemplo, que

1. todos los derivables\(A\) son válidos;

2. si una oración es derivable de algunas otras, también es consecuencia de ellas;

3. si un conjunto de oraciones es inconsistente, es insatisfactoria.

Estas son propiedades importantes de un sistema de derivación. Si alguno de ellos no se sostiene, el sistema de derivación es deficiente—derivaría demasiado. En consecuencia, es de suma importancia establecer la solidez de un sistema de derivación.

Debido a que todas estas propiedades teóricas de prueba se definen a través de la derivabilidad en el cálculo secuente de ciertos secuentes, probar (1) — (3) anterior requiere probar algo sobre las propiedades semánticas de los secuentes derivables. Primero definiremos lo que significa que un secuente sea válido, y luego mostraremos que cada secuente derivable es válido. (1) — (3) luego seguir como corolarios de este resultado.

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

Una estructura\(\Struct M\) satisface un\(\Gamma \Sequent \Delta\) iff secuente ya sea\(\SatN{M}{A}\) para algunos\(A \in \Gamma\) o\(\Sat{M}{A}\) para algunos\(A \in \Delta\).

Un secuente es válido si cada estructura lo\(\Struct M\) satisface.

Teorema\(\PageIndex{1}\): Soundness

Si\(\Log{LK}\) deriva\(\Theta \Sequent \Xi\), entonces\(\Theta \Sequent \Xi\) es válido.

Prueba. Dejar\(\pi\) ser una derivación de\(\Theta \Sequent \Xi\). Se procede por inducción sobre el número de inferencias\(n\) en\(\pi\).

Si el número de inferencias es\(0\), entonces\(\pi\) consiste únicamente en un secuente inicial. Cada secuente inicial\(A \Sequent A\) es obviamente válido, ya que para cada\(\Struct M\), cualquiera\(\SatN{M}{A}\) o\(\Sat{M}{A}\).

Si el número de inferencias es mayor que 0, distinguimos los casos según el tipo de inferencia más baja. Por hipótesis de inducción, podemos suponer que las premisas de esa inferencia son válidas, ya que el número de inferencias en la prueba de cualquier premisa es menor que\(n\).

Primero, consideramos las posibles inferencias con una sola premisa.

1. La última inferencia es un debilitamiento. Entonces\(\Theta \Sequent \Xi\) es\(A, \Gamma \Sequent \Delta\) (si la última inferencia es\(\LeftR{\Weakening}\)) o\(\Gamma \Sequent \Delta, A\) (si es\(\RightR{\Weakening}\)), y la derivación termina en uno de

   

   Por hipótesis de inducción,\(\Gamma \Sequent \Delta\) es válido, es decir, para cada estructura\(\Struct{M}\), o hay alguna\(C \in \Gamma\) tal que\(\SatN{M}{C}\) o hay alguna\(C \in \Delta\) tal que\(\Sat{M}{C}\).

   Si\(\SatN{M}{C}\) para algunos\(C \in \Gamma\), entonces\(C \in \Theta\) también desde entonces\(\Theta = A, \Gamma\), y así\(\SatN{M}{C}\) para algunos\(C \in \Theta\). De igual manera, si\(\Sat{M}{C}\) para algunos\(C \in \Delta\), como\(C \in \Xi\),\(\Sat{M}{C}\) para algunos\(C \in \Xi\). En consecuencia,\(\Theta \Sequent \Xi\) es válido.

2. La última inferencia es\(\LeftR{\lnot}\): Entonces la premisa de la última inferencia es\(\Gamma \Sequent \Delta, A\) y la conclusión es\(\lnot A, \Gamma \Sequent \Delta\), es decir, la derivación termina en

   

   y\(\Theta = \lnot A, \Gamma\) mientras\(\Xi = \Delta\).

   La hipótesis de inducción nos dice que\(\Gamma \Sequent \Delta, A\) es válido, es decir\(\Struct{M}\), para cada, ya sea (a) para algunos\(C \in \Gamma\)\(\SatN{M}{C}\), o (b) para algunos\(C \in \Delta\)\(\Sat{M}{C}\), o (c)\(\Sat{M}{A}\). Queremos demostrar que también\(\Theta \Sequent \Xi\) es válido. Dejar\(\Struct{M}\) ser una estructura. Si (a) sostiene, entonces hay\(C \in \Gamma\) así que\(\SatN{M}{C}\), pero\(C \in \Theta\) también. Si (b) sostiene, hay\(C \in \Delta\) tal que\(\Sat{M}{C}\), pero\(C \in \Xi\) también. Por último, si\(\Sat{M}{A}\), entonces\(\SatN{M}{\lnot A}\). Ya que\(\lnot A \in \Theta\), hay\(C \in \Theta\) tal que\(\SatN{M}{C}\). En consecuencia,\(\Theta \Sequent \Xi\) es válido.

3. La última inferencia es\(\RightR{\lnot}\): Ejercicio.

4. La última inferencia es\(\LeftR{\land}\): Hay dos variantes: se\(A \land B\) pueden inferir a la izquierda desde\(A\) o desde el\(B\) lado izquierdo de la premisa. En el primer caso, el\(\pi\) termina en

   

   y\(\Theta = A \land B, \Gamma\) mientras\(\Xi = \Delta\). Considera una estructura\(\Struct M\). Ya que por hipótesis de inducción,\(A, \Gamma \Sequent \Delta\) es válido, (a)\(\SatN{M}{A}\), (b)\(\SatN{M}{C}\) para algunos\(C \in \Gamma\), o (c)\(\Sat{M}{C}\) para algunos\(C \in \Delta\). En el caso (a)\(\SatN{M}{A \land B}\),, entonces hay\(C \in \Theta\) (es decir,\(A \land B\)) tal que\(\SatN{M}{C}\). En el caso b), hay\(C \in \Gamma\) tal que\(\SatN{M}{C}\), y\(C \in \Theta\) también. En el caso c), hay\(C \in \Delta\) tal que\(\Sat{M}{C}\), y\(C \in \Xi\) así desde entonces\(\Xi = \Delta\). Entonces en cada caso,\(\Struct M\) satisface\(A \land B, \Gamma \Sequent \Delta\). Ya que\(\Struct{M}\) fue arbitrario,\(\Gamma \Sequent \Delta\) es válido. El caso en el\(A \land B\) que se infiere\(B\) se maneja igual, cambiando\(A\) a\(B\).

5. La última inferencia es\(\RightR{\lor}\): Hay dos variantes: se\(A \lor B\) pueden inferir a la derecha desde\(A\) o desde el\(B\) lado derecho de la premisa. En el primer caso,\(\pi\) termina en

   

   Ahora\(\Theta = \Gamma\) y\(\Xi = \Delta, A \lor B\). Considera una estructura\(\Struct{M}\). Ya que\(\Gamma \Sequent \Delta, A\) es válido, (a)\(\Sat{M}{A}\), (b)\(\SatN{M}{C}\) para algunos\(C \in \Gamma\), o (c)\(\Sat{M}{C}\) para algunos\(C \in \Delta\). En el caso (a),\(\Sat{M}{A \lor B}\). En el caso b), hay\(C \in \Gamma\) tal que\(\SatN{M}{C}\). En el caso c), hay\(C \in \Delta\) tal que\(\Sat{M}{C}\). Entonces en cada caso,\(\Struct{M}\) satisface\(\Gamma \Sequent \Delta, A \lor B\), es decir,\(\Theta \Sequent \Xi\). Ya que\(\Struct{M}\) fue arbitrario,\(\Theta \Sequent \Xi\) es válido. El caso en el\(A \lor B\) que se infiere\(B\) se maneja igual, cambiando\(A\) a\(B\).

6. La última inferencia es\(\RightR{\lif}\): Luego\(\pi\) termina en

   

   Nuevamente, la hipótesis de inducción dice que la premisa es válida; queremos demostrar que la conclusión también es válida. Que\(\Struct{M}\) sea arbitrario. Ya que\(A, \Gamma \Sequent \Delta, B\) es válido, al menos uno de los siguientes casos obtiene: (a)\(\SatN{M}{A}\), (b)\(\Sat{M}{B}\), (c)\(\SatN{M}{C}\) para algunos\(~C \in \Gamma\), o (d)\(\Sat{M}{C}\) para algunos\(C \in \Delta\). En los casos a) y b),\(\Sat{M}{A \lif B}\) y así hay\(C \in \Delta, A \lif B\) tal que\(\Sat{M}{C}\). En el caso c), para algunos\(C \in \Gamma\),\(\SatN{M}{C}\). En el caso d), para algunos\(C \in \Delta\),\(\Sat{M}{C}\). En cada caso,\(\Struct{M}\) satisface\(\Gamma \Sequent \Delta, A \lif B\). Ya que\(\Struct{M}\) fue arbitrario,\(\Gamma \Sequent \Delta, A \lif B\) es válido.

7. La última inferencia es\(\LeftR{\lforall{}{}}\): Luego hay una fórmula\(A(x)\) y un término cerrado\(t\) tal que\(\pi\) termina en

   

   Queremos demostrar que la conclusión\(\lforall{x}{A(x)}, \Gamma \Sequent \Delta\) es válida. Considera una estructura\(\Struct M\). Ya que la premisa\(A(t), \Gamma \Sequent \Delta\) es válida, (a)\(\SatN{M}{A(t)}\), (b)\(\SatN{M}{C}\) para algunos\(C \in \Gamma\), o (c)\(\Sat{M}{C}\) para algunos\(C \in \Delta\). En el caso a), por la Proposición 5.14.4, si\(\Sat{M}{\lforall{x}{A(x)}}\), entonces\(\Sat{M}{A(t)}\). Ya que\(\SatN{M}{A(t)}\),\(\SatN{M}{\lforall{x}{A(x)}}\). En el caso b) y c),\(\Struct{M}\) también satisface\(\lforall{x}{A(x)}, \Gamma \Sequent \Delta\). Ya que\(\Struct M\) fue arbitrario,\(\lforall{x}{A(x)}, \Gamma \Sequent \Delta\) es válido.

8. La última inferencia es\(\RightR{\lexists{}{}}\): Ejercicio.

9. La última inferencia es\(\RightR{\lforall{}{}}\): Luego hay una fórmula\(A(x)\) y un símbolo constante\(a\) tal que\(\pi\) termina en

   

   donde se cumpla la condición de variable propia, es decir,\(a\) no ocurre en\(A(x)\),\(\Gamma\), o\(\Delta\). Por hipótesis de inducción, la premisa de la última inferencia es válida. Tenemos que demostrar que la conclusión también es válida, es decir, que para cualquier estructura\(\Struct M\), (a)\(\Sat{M}{\lforall{x}{A(x)}}\), (b)\(\SatN{M}{C}\) para algunos\(C \in \Gamma\), o (c)\(\Sat{M}{C}\) para algunos\(C \in \Delta\).

   Supongamos que\(\Struct{M}\) es una estructura arbitraria. Si (b) o (c) sostiene, estamos hechos, así que supongamos que ninguno sostiene: para todos\(C \in \Gamma\),\(\Sat{M}{C}\), y para todos\(C \in \Delta\),\(\SatN{M}{C}\). Tenemos que demostrar que (a) sostiene, es decir,\(\Sat{M}{\lforall{x}{A(x)}}\). Por la Proposición 5.12.4, si es suficiente para mostrar eso\(\Sat[,s]{M}{A(x)}\) para todas las asignaciones de variables\(s\). Así que vamos\(s\) a ser una asignación de variable arbitraria. Considera la estructura\(\Struct{M'}\) que es igual a\(\Struct{M}\) excepción\(\Assign{a}{M'} = s(x)\). Por Corolario 5.13.1, para cualquier\(C \in \Gamma\),\(\Sat{M'}{C}\) ya que\(a\) no ocurre en\(\Gamma\), y para ninguna\(C \in \Delta\),\(\SatN{M'}{C}\). Pero la premisa es válida, entonces\(\Sat{M'}{A(a)}\). Por la Proposición 5.12.3,\(\Sat[,s]{M'}{A(a)}\), ya que\(A(a)\) es una sentencia. Ahora\(\varAssign{s}{s}{x}\) con\(s(x) = \Value[s]{a}{M'}\), ya que hemos definido\(\Struct{M'}\) de esta manera. Entonces aplica la Proposición 5.13.3, y obtenemos\(\Sat[,s]{M'}{A(x)}\). Ya que\(a\) no ocurre en\(A(x)\), por la Proposición 5.13.1,\(\Sat[,s]{M}{A(x)}\). Ya que\(s\) fue arbitrario, hemos completado la prueba de que\(\Sat[,s]{M}{A(x)}\) para todas las asignaciones variables.

10. La última inferencia es\(\LeftR{\lexists{}{}}\): Ejercicio.

Ahora consideremos las posibles inferencias con dos premisas.

1. La última inferencia es un corte: luego\(\pi\) termina en

   

   Dejar\(\Struct{M}\) ser una estructura. Por hipótesis de inducción, las premisas son válidas, por lo que\(\Struct{M}\) satisface ambas premisas. Distinguimos dos casos: (a)\(\SatN{M}{A}\) y (b)\(\Sat{M}{A}\). En el caso (a),\(\Struct{M}\) para que satisfaga la premisa dejada, ésta deberá satisfacer\(\Gamma \Sequent \Delta\). Pero entonces también satisface la conclusión. En el caso b),\(\Struct{M}\) para que se satisfaga la premisa correcta, ésta deberá satisfacer\(\Pi \setminus \Lambda\). Nuevamente,\(\Struct{M}\) satisface la conclusión.

2. La última inferencia es\(\RightR{\land}\). Luego\(\pi\) termina en

   

   Considera una estructura\(\Struct M\). Si\(\Struct{M}\) satisface\(\Gamma \Sequent \Delta\), ya terminamos. Entonces supongamos que no lo hace. ya que\(\Gamma \fCenter \Delta, A\) es válido por hipótesis de inducción,\(\Sat{M}{A}\). De igual manera, ya que\(\Gamma \Sequent \Delta, B\) es válido,\(\Sat{M}{B}\). Pero entonces\(\Sat{M}{A \land B}\).

3. La última inferencia es\(\LeftR{\lor}\): Ejercicio.

4. La última inferencia es\(\LeftR{\lif}\). Luego\(\pi\) termina en

   

   De nuevo, consideremos una estructura\(\Struct{M}\) y supongamos que\(\Struct{M}\) no satisface\(\Gamma, \Pi \Sequent \Delta, \Lambda\). Tenemos que demostrarlo\(\SatN{M}{A \lif B}\). Si\(\Struct{M}\) no satisface\(\Gamma, \Pi \Sequent \Delta, \Lambda\), no satisface ni\(\Gamma \Sequent \Delta\) tampoco\(\Pi \Sequent \Lambda\). Ya que,\(\Gamma \Sequent \Delta, A\) es válido, tenemos\(\Sat{M}{A}\). Ya que\(B, \Pi \Sequent \Lambda\) es válido, tenemos\(\SatN{M}{B}\). Pero entonces\(\SatN{M}{A \lif B}\), que es lo que queríamos mostrar.

◻

Problema\(\PageIndex{1}\)

Completar la prueba del Teorema\(\PageIndex{1}\).

Corolario\(\PageIndex{1}\)

Si\(\Proves A\) entonces\(A\) es válido.

Corolario\(\PageIndex{2}\)

Si\(\Gamma \Proves A\) entonces\(\Gamma \Entails A\).

Prueba. Si\(\Gamma \Proves A\) entonces para algún subconjunto finito\(\Gamma_0 \subseteq \Gamma\), hay una derivación de\(\Gamma_0 \Sequent A\). Por teorema\(\PageIndex{1}\), toda estructura\(\Struct{M}\) o bien hace algunas\(B \in \Gamma_0\) falsas o hace\(A\) verdad. De ahí, si\(\Sat{M}{\Gamma}\) entonces también\(\Sat{M}{A}\). ◻

Corolario\(\PageIndex{3}\)

Si\(\Gamma\) es satisfecha, entonces es consistente.

Prueba. Demostramos lo contrapositivo. Supongamos que eso no\(\Gamma\) es consistente. Después hay un finito\(\Gamma_0 \subseteq \Gamma\) y una derivación de\(\Gamma_0 \Sequent \quad\). Por Teorema\(\PageIndex{1}\),\(\Gamma_0 \Sequent \quad\) es válido. Es decir, para cada estructura\(\Struct{M}\), hay\(C \in \Gamma_0\) así que eso\(\SatN{M}{C}\), y desde entonces\(\Gamma_0 \subseteq \Gamma\), eso también\(C\) está en\(\Gamma\). Así, no\(\Struct{M}\) satisface\(\Gamma\), y no\(\Gamma\) es satisfecha. ◻