Probar las premisas trabajando en una prueba de la conclusión

Question

me gusta mucho este sitio.

Consideremos las siguientes reglas de un sistema de deducción (debido a Sch\"{u}tte). Las escribiré todas, pero algunas pueden no ser útiles.

---

REGLAS DÉBILES

Regla 1: \begin {Ecuación} \frac {C \vee A \vee B \vee D}{C \vee B \vee A \vee D} \end {Ecuación}

Regla 2: \begin {Ecuación} \frac {A \vee A \vee D}{A \vee D} \end {Ecuación}

REGLAS FUERTES

regla A: \begin {Ecuación} \frac {D}{A \vee D} \quad\text {(donde $A$ es un wff cerrado)} \end {Ecuación}

La regla de De Morgan: \begin {Ecuación} \frac { \neg A \vee D \quad \neg B \vee D}{ \neg (A \vee B) \vee D} \end {Ecuación}

Negación: \begin {Ecuación} \frac {A \vee D }{ \neg\neg A \vee D} \end {Ecuación}

Cuantificación: \begin {Ecuación} \frac { \neg A(t) \vee D}{( \neg (x)A(x)) \vee D} \end {Ecuación}

Inducción infinita: \begin {Ecuación} \frac {A( \bar {n}) \vee D \quad \text {para todos los números naturales n}}{(x)A(x)) \vee D} \quad \text {( $\bar{n}$ es un número)} \end {Ecuación}

REGLA DE CORTE

\begin {Ecuación} \frac {C \vee A \quad \neg A \vee D}{C \vee D} \end {Ecuación}

Las fórmulas C y D se llaman fórmulas auxiliares. Podemos eliminarlas (excepto en la regla A) obteniendo otras instancias de las reglas.

---

Necesito demostrar que a partir de una demostración de una fórmula que es consecuencia de unas premisas utilizando una de esas reglas (por ejemplo la regla de De Morgan), es posible obtener una demostración de las premisas. La prueba en cuestión se obtiene trabajando sobre la original. Hay una descripción de cómo se hace, pero no la entiendo. Intentaré explicarlo.

Supongamos que una fórmula $A$ se obtiene por la regla de DeMorgan y entonces es de la forma $\neg(B \vee E) \vee D$ . Tomando una prueba de $A$ podemos considerar todas las subfórmulas $\neg(B \vee E)$ del árbol de pruebas obtenido a partir de $\neg(B \vee E)$ en $A$ y volviendo a trepar por el árbol de las pruebas. (Aquí no me queda claro cuál es el verdadero significado). Este proceso (¿qué proceso?) continúa a través de las reglas débiles utilizadas y a través de las reglas fuertes utilizadas en las que $\neg(B \vee E)$ es una subfórmula de un wff auxiliar. Este proceso sólo puede terminar con una regla A o con una regla De Morgan. El conjunto de todas las ocurrencias de $\neg(B \vee E)$ se llama \emph {historia} de $\neg(B \vee E)$ . Ahora sustituye todas las ocurrencias de $\neg(B \vee E)$ en su historia con $\neg B$ . Entonces obtenemos otro árbol de pruebas (después de eliminar todas aquellas fórmulas que no son necesarias) cuya fórmula terminal es simplemente $\neg B \vee D$ (es decir, una de las premisas de la regla de De Morgan). Sustitución con $\neg E$ se obtiene una prueba de $\neg E \vee D$ (la otra premisa).

¿Qué método utilizamos precisamente para construir ese nuevo árbol de pruebas? ¿Puedes mostrarme un ejemplo de cómo demostrar las premisas de la regla de Morgan utilizando el método descrito anteriormente?

Muchas gracias.

Answer 1

Asumo que el último párrafo largo de la pregunta es, salvo por tus inserciones entre paréntesis, algo que citaste y que estás tratando de entender. (Si es así, te sugiero que lo hagas explícito para que la pregunta sea más fácil de entender).

Por tus comentarios, parece que los axiomas son sólo fórmulas atómicas y fórmulas atómicas negadas, es decir, no contienen ninguna conectiva lógica. En ese caso, el párrafo citado tiene sentido, aunque se salta algunos detalles no triviales. La idea es que en un árbol de pruebas de una fórmula de la forma $\neg(B \vee E) \vee D$ la subfórmula $\neg(B \vee E)$ debe haberse originado por una aplicación de la regla A o de la regla De Morgan.

No puede haberse originado en uno de los axiomas, ya que los axiomas no contienen conectivos lógicos. Así que repasemos las reglas y comprobemos cuáles pueden producir la subfórmula $\neg(B \vee E)$ si no estaba ya en uno de los locales. Estas son precisamente las reglas fuertes; las reglas débiles y la regla de corte sólo eliminan las subfórmulas.

Ahora, repasando las reglas de nuevo, encontramos que no hay ninguna regla que reduzca el número de cuantificadores o negaciones delante de una subfórmula. Esto significa que la subfórmula $\neg(B \vee E)$ no puede haberse derivado de una fórmula en la que haya sido precedida por un cuantificador o por negaciones adicionales. Pero eso significa que no puede haber sido producida por las reglas de negación, cuantificación o inducción infinita, ya que cada una de ellas sólo puede producir algo donde $\neg(B \vee E)$ iría precedido de al menos un cuantificador o una negación adicional.

Eso deja sólo la regla A y la regla De Morgan por la cual $\neg(B \vee E)$ podría haberse introducido en el árbol de pruebas. Pero en ambos casos, podemos sustituir $\neg(B \vee E)$ por $\neg B$ o por $\neg E$ en el caso de la regla A porque podemos introducir cualquier $A$ nos gusta, y en el caso de la regla De Morgan porque eso convierte la conclusión en una de las dos premisas.

Resumiendo, si modificamos el árbol de pruebas sustituyendo todas las ocurrencias de $\neg(B \vee E)$ por $\neg B$ seguirá siendo un árbol de pruebas válido, pero ahora será un árbol de pruebas para $\neg B \lor D$ (y lo mismo para $\neg E$ y $\neg B \lor E$ ). Por lo tanto, cualquier prueba de $\neg(B \vee E) \vee D$ puede utilizarse para producir pruebas tanto de $\neg B \vee D$ y $\neg E \vee D$ .