CFPTT: Consulta ejercicios 1.12, 2.9.2 y 3.7

Buenas noches,

Quisiera consultar por los siguientes ejercicios. En ambos me ocurrió que intenté avanzar aplicando diferentes estrategias, pero no pude obtener resultados.

- Ej 1.12. (Diagnóstico)

Hypothesis Regla1: PF \/ PA -> PH \/ PR.
Hypothesis Regla2: ~PR \/ PF.
Hypothesis Regla3: PH /\ ~PR -> PA.

Theorem ej12: (~PA /\ PF) -> PR /\ ~PH.

- Ej 2.9.2: (Classical)

Lemma not_forall_ex_not: (~forall x :U, A x) -> (exists x:U, ~A x).

También aprovecho para consultar si la resolución de la función `And` del ejercicio 3.7 es la esperada:

Definition Bool := forall (X : Set), X -> X -> X.

Definition And (a : Bool) (b : Bool) : Bool := fun (X : Set) (the : X) (els : X) => a X (b X the els) els.

¡Gracias!

Saludos,

Cristian

Re: Consulta ejercicios 1.12, 2.9.2 y 3.7

de Carlos Luna - miércoles, 14 de octubre de 2020, 08:57

Hola Cristian.

En el ej 1.12 podés probar PR pero no podés asegurar nada sobre PH. Luego, el teorema debería ser (con las 3 hipótesis dadas): ~PA /\ PF -> PR. La prueba sale por lógica clásica (haciendo por ejemplo: classic PR).

En el ej 2.9.2 podés hacer "classic (exists x:U, ~A x)" así usás lo demostrado en 2.9.1.

En el 3.7 está bien la definición del And.

Saludos, Carlos