Tenemos que aprovechar el hecho de que en el caso de un tableau (o : árbol de la verdad ) para el conjunto $S$ de fórmulas, un completo Abrir define una asignación de verdad que satisface el conjunto de iniciales $S$ .
Este hecho corresponde al hecho obvio de que un camino cerrado es insatisfactible, porque cerramos un camino encontrando un par de fórmulas contradictorias.
Lo que tenemos que demostrar es la solidez del procedimiento de prueba, es decir, que:
si $T \cup \{ \lnot A \}$ cierra sin Abrir caminos, entonces $T \vDash A$ .
La prueba es por inducción, partiendo de la solidez de las reglas.
Esto significa considerar cada regla y demostrar que si la suposición de la regla es verdadera, también lo es al menos uno de los siguientes caminos.
Considere, por ejemplo, la regla :
$\dfrac {A \to B}{\lnot A | B }$ ;
claramente, si $A \to B$ es verdadero, o bien $B$ es verdadero o $A$ es falso (es decir $\lnot A$ es verdadero).
Del mismo modo, para $\dfrac {\lnot (A \land B)}{\lnot A | \lnot B }$ .
Lo mismo ocurre con las reglas relativas a los cuantificadores, como por ejemplo $\dfrac {\lnot \forall x A}{\lnot A[x/a] } \text { with } a \text { new}$ Si no es cierto que $A$ tiene cada objeto, esto implica que hay un objeto, llámese $a$ de los cuales $A$ no se sostiene.
Una vez verificado el caso base, tenemos que considerar un árbol $\mathcal T$ y una asignación de verdad $v_0$ a las variables sentenciales que aparecen en el árbol.
Decimos que un camino de $\mathcal T$ es verdadero bajo $v_0$ si todas las fórmulas que aparecen en el camino son verdaderas bajo $v_0$ .
Por último, diremos que el árbol $\mathcal T$ es verdadero bajo $v_0$ si al menos un camino es verdadero bajo $v_0$ .
Considera ahora un árbol $\mathcal T_1$ y que $\mathcal T_2$ la ampliación inmediata de $\mathcal T_1$ obtenido con la aplicación de una de las reglas.
La solidez de las reglas demostradas anteriormente equivale a probar que cualquier extensión inmediata $\mathcal T_2$ de un árbol $\mathcal T_1$ que es verdadera bajo una asignación de verdad dada $v_0$ vuelve a ser cierto bajo $v_0$ .
De esto se deduce por inducción matemática que para cualquier árbol $\mathcal T$ si el origen es verdadero bajo $v_0$ entonces $\mathcal T$ debe ser verdadera bajo $v_0$ .
Último paso: un árbol cerrado $\mathcal T$ no puede ser cierto bajo ninguna interpretación, por lo que el origen de un árbol cerrado debe ser insatisfactible .
Conclusión Si el árbol para $T \cup \{ \lnot A \}$ se cierra (es decir, se completa sin Abrir caminos) entonces el conjunto de fórmulas $T \cup \{ \lnot A \}$ es insatisfactible y esto a su vez significa que :
$T \vDash A$ .
