Buenas,
Probando el comando tauto, en particular:
Theorem test: (~PA /\ PF) -> PH.
Proof.
tauto.
Qed.
Lo anterior es demostrado por tauto. Sin embargo, si considero el conjunto de hipotesis R={~PA, PF, PR, ~PH}.
A partir de R puedo demostrar las tres reglas del ejercicio 12. También se cumple (~PA /\ PF) pero no se cumple PH, por lo tanto no se debería cumplir (~PA /\ PF) -> PH. ¿Cómo es posible que tauto de el teorema por valido?
Hola Bruno.
Hay algún problema en tu planteo, ya que con las hipótesis correspondientes a las tres reglas no es posible demostrar con tauto: ~PA /\ PF -> PH. Quizás estás asumiendo alguna hipótesis extra, que no deberías. Por ejemplo, por qué planteás ~PH como hipótesis en el conjunto R?
Por qué te planteás demostrar las tres reglas del ejercicio 12? Son hipótesis del problema...
En concreto, con las tres reglas solamente no deberías poder demostrar: ~PA /\ PF -> PH. Si querés hacete un archivo aparte con este ejercicio para ver que no estás asumiendo nada previo que influya en la prueba.
Saludos, Carlos