¿Cómo se prueba '(B→C)→¬A' a partir de '(A→B)∨C' y '(A→¬C)' en Fitch?

Estoy tratando de abrirme camino a través de esta prueba de Fitch, y no estoy seguro de lo que estoy haciendo mal, pero sigo atascado sin importar lo que intente.

Primer intento:

Segundo intento:

Respuestas (2)

Hacer esto como una prueba de estilo Fitch es muy tedioso, pero obtengo:

ingrese la descripción de la imagen aquí

De hecho, sería más rápido probar usando el método de cortocircuito o una tabla de verdad.

Utilizando el método de cortocircuito,

  1. la conclusión es falsa cuando el lado izquierdo de (B -> C) -> ~A es VERDADERO pero el lado derecho es FALSO
  2. Entonces eso significa que A tendría que ser verdadero VERDADERO para que la conclusión sea falsa.
  3. Si A es verdadera, entonces la primera premisa solo puede ser verdadera cuando C es FALSA.
  4. Si C es falso, entonces B debe ser FALSO para que el lado izquierdo de la conclusión sea VERDADERO.
  5. Si B es FALSO, entonces la premisa dos se convierte en: (VERDADERO -> FALSO) v FALSO -> FALSO o FALSO, por lo que no podemos hacer que ambas premisas sean verdaderas y la conclusión falsa.

Referencias

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

El 'método de cortocircuito' que proporciona es muy útil para comprender por qué tengo que comenzar asumiendo A en la línea 4, antes de asumir B, etc., para llegar a mi conclusión. Gracias

Tu primer intento es el mejor.

Estabas en lo correcto al usar una prueba condicional, y comenzando con la suposición B->C. Sin embargo, debe notarse que para derivar el consecuente debes introducir una negación. De hecho, puedo ver que te diste cuenta de eso, pero ¿por qué no viste que lo siguiente que se suponía era A con la intención de derivar una contradicción?

|  (A -> B) v C         premise I
|_ A -> ~C              premise II
|  |_ B -> C            assumed (for conditional proof)
|  |  |_ A              assumed (for negational proof)
:  :  :  :
|  |  |  #              negation eliminated (hopefully)
|  |  ~A                negation introduced 
|  (B -> C) -> ~A       conditional introduced

Ahora, una de sus premisas es A->~C, por lo que podemos derivar inmediatamente ~C en el contexto, y tendremos nuestra contradicción si la otra premisa implica C bajo ambas suposiciones.

Bueno, esa otra premisa es una disyunción, que se elimina usando una prueba por casos. Si lo hace, de hecho derivará C en cada caso (de hecho, es trivial en un caso).

Por lo tanto, debe incrustar una prueba por casos dentro de una prueba de negación dentro de una prueba condicional. Y habrás terminado.

|  (A -> B) v C         premise I
|_ A -> ~C              premise II
|  |_ B -> C            assumed (for conditional proof)
|  |  |_ A              assumed (for negational proof)
|  |  |  ~C             conditional eliminated
|  |  |  |_ A -> B      left case assumed
:  :  :  :  :           ... (It should be clear, what you need to do here.)
|  |  |  |  C           derived (hopefully)
|  |  |  (A -> B) -> C  conditional introduced
|  |  |  |_ C           right case assumed
|  |  |  C -> C         conditional introduced
|  |  |  C              disjunction eliminated
|  |  |  #              negation eliminated
|  |  ~A                negation introduced
|  (B -> C) -> ~A       conditional introduced

TL; DR Cada vez que prevea que necesitará eliminar una disyunción, retrase hacerlo para tantas suposiciones planteadas como pueda. Intenta construir una montaña con dos cumbres en lugar de dos montañas enteras.