Cómo demostrar la siguiente fórmula mediante una prueba indirecta

Question

Tengo que demostrar que la premisa $A \to (B \vee C)$ lleva a la conclusión $(A \to B) \vee (A \to C)$ . Esto es lo que tengo hasta ahora.

A partir de aquí estoy atascado (y ni siquiera estoy seguro de que esto sea correcto). Mi idea es usar la introducción de la negación asumiendo lo contrario y llegando a una contradicción. He asumido $A$ lo que llevó a $B \vee C$ y, como puedes ver, estoy probando o elim pero la única manera que se me ocurre de hacerlo es usar intro condicional y luego o intro pero eso parece que sólo funciona para una sola subprueba. En otras palabras, no puedo usar la suposición de $B$ para decir $A \to B$ . Esto se llama una prueba indirecta.

Answer 1

Siempre es un muy malo señal cuando alguien ha iniciado un montón de subpruebas sin indicar lo que ocurre al final de la subprueba.

Una prueba debe tener siempre un plan o esbozar y las subpruebas proporcionan el esqueleto para hacerlo. Pero de nuevo, necesitas indicar lo que quieres hacer con la subprueba, y eso implica indicar lo que quieres como la última línea de tu subprueba. No has hecho eso para ninguna de las tres subpruebas que has empezado, que es exactamente por lo que te metes en problemas, y consigues ver el bosque por los árboles.

Ahora, está claro que con tu primera subprueba esperas hacer una prueba por contradicción. Así que, empieza por crear la configuración adecuada para ello:

$A \rightarrow (B \lor C)$

$\quad \neg ((A \rightarrow B) \lor (A \rightarrow C))$

$\quad \text{... skip a bunch of lines ...}$

$\quad \bot$

$\neg \neg ((A \rightarrow B) \lor (A \rightarrow C))$

$(A \rightarrow B) \lor (A \rightarrow C)$

Bien, ahora que hemos establecido esto correctamente, volvamos al interior de la subprueba, y veamos cómo podemos derivar la contradicción de la premisa y la suposición.

Ahora, es en este punto que usted asume $A$ . ¿Por qué?

En realidad, creo que sé por qué, porque lo he visto con demasiada frecuencia: probablemente estás pensando "ooh, sería bueno tener $A$ porque entonces puedo combinar eso con la premisa. OK, así que vamos a suponer $A$ "

Bien, el problema con este tipo de pensamiento es que terminas suponiendo que algo que quiere ... lo que siempre es una mala idea, ya que a menudo conduce a una prueba circular. En efecto, supongamos que se combone $A$ con la premisa, y obtener $B \lor C$ ... OK .... ¡¿Y ahora qué?! Bueno, una cosa que puedes hacer es cerrar la subprueba y concluir $A \rightarrow (B \lor C)$ .... pero ten en cuenta que ahora sólo consigues la misma premisa, es decir, que no llegas a ninguna parte.

Aquí tienes un consejo general sobre las subpruebas, que vuelve a mi punto inicial sobre tener un plan: antes de empezar cualquier subprueba, deberías saber ya cómo vas a usar esa subprueba y, en particular, cuál debe ser la última línea de tu subprueba y qué regla vas a aplicar después de que la subprueba esté hecha.

Bien, reagrupémonos. Realmente no hay una buena razón para asumir $A$ . Bien, pero ¿qué debe hacer en la línea 3? Bueno, de nuevo, si tenía $A$ Podrías combinar eso con la premisa, pero en lugar de suponiendo que $A$ , podrías tratar de hacer $A$ su nuevo objetivo. Y, para probar $A$ una cosa que podrías hacer es asumir $\neg A$ y demostrar que eso lleva a una contradicción.

Sin embargo, hay algo mucho más sencillo de hacer. La suposición $\neg ((A \rightarrow B) \lor (A \rightarrow C))$ es la negación de una disyunción, y probablemente sepas que según DeMorgan eso es equivalente a la conjunción de los disyuntos negados, es decir, a $\neg (A \rightarrow B) \land \neg (A \rightarrow C)$ . Ahora bien, sospecho que usted no tiene a DeMorgan como regla de inferencia en su sistema específico, pero piénselo de esta manera: aparentemente debería ser capaz de derivar ambos $\neg (A \rightarrow B)$ así como $\neg (A \rightarrow C)$ de la Asunción. Ahora bien, ambas afirmaciones son negaciones, y probablemente conozcas la mejor estrategia para demostrar negaciones: ¡Probación por Contradicción!

Bien, entonces tenemos otra pieza de nuestro plan:

$A \rightarrow (B \lor C)$

$\quad \neg ((A \rightarrow B ) \lor (A \rightarrow C))$

$\quad \quad A \rightarrow B$

$\quad \quad \text{skip a few lines...}$

$\quad \quad \bot$

$\quad \neg (A \rightarrow B)$

$\quad \quad (A \rightarrow C)$

$\quad \quad \text{skip a few lines ...}$

$\quad \quad \bot$

$\quad \neg (A\rightarrow C)$

$\quad \text{few lines ...}$

$\quad \bot$

$\neg \neg ((A \rightarrow B) \lor (A \rightarrow C))$

$(A \rightarrow B) \lor (A \rightarrow C)$

Bien, ¿ves cómo está todo bien organizado? ¿Cómo tienes ahora un esquema, al que puedes añadir detalles y proporcionar los pasos que faltan en algún momento? Que es lo que se supone que debes hacer. Así es como mantienes tus pruebas y tu propio pensamiento organizado. De hecho, el objetivo de hacer pruebas de lógica formal es enseñar esa misma habilidad de organización cuidadosa.

Ahora, voy a dejar esos detalles para usted, pero le dejo una pista más: ¿qué es $\neg (A \rightarrow B)$ ¿equivalente a? .... intentar derivar eso, hacer lo mismo para $\neg (A \rightarrow C)$ y ya está todo listo. Buena suerte.

Answer 2

Sugerencia: si asume $A \to (B \lor C)$ , $\lnot(A \to B)$ y $A$ Entonces se puede concluir que $B \lor C$ y $\lnot B$ . ¿Puedes seguir a partir de ahí?

Answer 3

Tengo que demostrar que la premisa $A \to (B \vee C)$ lleva a la conclusión $(A \to B) \vee (A \to C)$ . Esto es lo que tengo hasta ahora. ...

Una disyunción se suele demostrar por reducción al absurdo.   Se asume su negación y se deriva una contradicción.   Normalmente, esto implica asumir la negación de una disyunción para derivar la otra. $$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{A\to (B\vee C)}{\fitch{\lnot((A\to B)\lor(A\to C))}{\fitch{\lnot (A\to B)}{\fitch A{~\vdots\\C}\\A\to C\\(A\to B)\vee(A\to C)\\\bot}\\\lnot\lnot(A\to B)\\A\to B\\(A\to B)\vee(A\to C)\\\bot}\\\lnot\lnot((A\to B)\vee(A\to C))\\(A\to B)\lor (A\to C)}$$

Answer 4

Supongo que está utilizando el comprobador de pruebas asociado a la forallx texto. No hay ninguna regla en este comprobador de pruebas que permita reglas de inferencia para implicación material . Por lo tanto, puede que no sea fácil proceder a la negación del objetivo si éste contiene declaraciones condicionales.

El siguiente intento de completar la prueba muestra lo que podría ocurrir:

Para descargar el supuesto $A$ en la línea 3, es probable que tenga que utilizar la ley del medio excluido en $A \lor \lnot A$ lo que implicaría otra subprueba.

Una forma alternativa de proceder es negar algo equivalente a la premisa o al objetivo para eliminar los enunciados condicionales. Por ejemplo, observe que la premisa es equivalente a $\lnot A \lor (B \lor C)$ . Si lo niego puedo reescribirlo utilizando las siguientes equivalencias:

$$\begin{align} \lnot (\lnot A \lor (B \lor C)) &\equiv \lnot \lnot A \land \lnot (B\lor C)\\ &\equiv A \land \lnot (B\lor C)\\ \end{align}$$

En lugar de utilizar la negación de la conclusión, utilizaré esa afirmación como supuesto y derivaré una contradicción. Aquí está la prueba:

La contradicción se derivó en la línea 6. Ahora tengo que continuar desde este punto y derivar la meta en sí. Este desvío de negar un enunciado equivalente a la premisa (o meta) puede facilitar la derivación de la meta.

---

Editor y comprobador de pruebas de deducción natural al estilo de JavaScript/PHP de Kevin Klement http://proofs.openlogicproject.org/