Hacer esto como una prueba de estilo Fitch es muy tedioso, pero obtengo:
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,
Editor y comprobador de pruebas de deducción natural JavaScript/PHP estilo Fitch de Kevin Klement http://proofs.openlogicproject.org/
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.
35308