Sol 7
De Lógica matemática y fundamentos (2018-19)
Revisión del 14:03 20 abr 2019 de Jalonso (discusión | contribuciones)
theory R7_sol
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta relación es escribir demostraciones usando sólo
las reglas básicas de deducción natural de la lógica proposicional y
los métodos rule, erule, frule, drule y assumption.
Las reglas básicas de la deducción natural son las siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· conjE: ⟦P ∧ Q; ⟦P; Q⟧ ⟹ R⟧ ⟹ R
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· impE: ⟦P ⟶ Q; P; Q ⟹ R⟧ ⟹ R
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· iffE: ⟦P = Q; ⟦P ⟶ Q; Q ⟶ P⟧ ⟹ R⟧ ⟹ R
· notnotD: ¬¬ P ⟹ P
· not_not: P = ¬¬P
· ccontr: (¬P ⟹ False) ⟹ P
· excluded_midle: ¬P ∨ P
· classical: (¬ P ⟹ P) ⟹ P
· contrapos_nn ⟦¬Q; P ⟹ Q⟧ ⟹ ¬P
---------------------------------------------------------------------
*}
text {*
Se usarán las reglas notnotI y mt que demostramos a continuación.
*}
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
section {* Implicaciones *}
text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ q, p ⊢ q
------------------------------------------------------------------ *}
lemma ej1a: "⟦p ⟶ q; p⟧ ⟹ q"
apply (erule mp) (* p ⟹ p *)
apply assumption (* *)
done
lemma ej1b: "⟦p ⟶ q; p⟧ ⟹ q"
apply (erule mp, assumption)
done
lemma ej1c: "⟦p ⟶ q; p⟧ ⟹ q"
by (erule mp, assumption)
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}
lemma ej2a: "⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r"
apply (erule mp) (* ⟦p ⟶ q; p⟧ ⟹ q *)
apply (erule mp) (* p ⟹ p *)
apply assumption (* *)
done
lemma ej2b: "⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r"
apply (erule mp)+ (* p ⟹ p *)
apply assumption (* *)
done
lemma ej2c: "⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r"
apply ((erule mp)+, assumption)
done
lemma ej2d: "⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r"
by ((erule mp)+, assumption)
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}
lemma ej3a: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
apply (drule mp) (* ⟦p ⟶ q; p⟧ ⟹ p
⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *)
apply assumption (* ⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *)
apply (drule mp) (* ⟦p; q ⟶ r⟧ ⟹ p
⟦p; q ⟶ r; q⟧ ⟹ r *)
apply assumption (* ⟦p; q ⟶ r; q⟧ ⟹ r *)
apply (drule mp) (* ⟦p; q⟧ ⟹ q
⟦p; q; r⟧ ⟹ r *)
apply assumption (* ⟦p; q; r⟧ ⟹ r *)
apply assumption (* *)
done
lemma ej3b: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
apply (drule mp, assumption) (* ⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *)
apply (drule mp, assumption) (* ⟦p; q ⟶ r; q⟧ ⟹ r *)
apply (drule mp, assumption) (* ⟦p; q; r⟧ ⟹ r *)
apply assumption (* *)
done
lemma ej3c: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
apply (drule mp, assumption)+ (* ⟦p; q; r⟧ ⟹ r *)
apply assumption (* *)
done
lemma ej3d: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
apply (drule mp, assumption+)+
done
lemma ej3e: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r"
by (drule mp, assumption+)+
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}
lemma ej4a: "⟦p ⟶ q; q ⟶ r⟧ ⟹ p ⟶ r"
apply (rule impI) (* ⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r *)
apply (erule mp) (* ⟦p ⟶ q; p⟧ ⟹ q *)
apply (erule mp) (* p ⟹ p *)
apply assumption (* *)
done
lemma ej4b: "⟦p ⟶ q; q ⟶ r⟧ ⟹ p ⟶ r"
apply (rule impI) (* ⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r *)
apply (erule mp)+ (* p ⟹ p *)
apply assumption (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
lemma ej5a: "p ⟶ (q ⟶ r) ⟹ q ⟶ (p ⟶ r)"
apply (rule impI) (* ⟦p ⟶ q ⟶ r; q⟧ ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ⟶ r; q; p⟧ ⟹ r *)
apply (erule impE) (* ⟦q; p⟧ ⟹ p
⟦q; p; q ⟶ r⟧ ⟹ r *)
apply assumption (* ⟦q; p; q ⟶ r⟧ ⟹ r *)
apply (erule impE) (* ⟦q; p⟧ ⟹ q
⟦q; p; r⟧ ⟹ r *)
apply assumption (* ⟦q; p; r⟧ ⟹ r *)
apply assumption (* *)
done
lemma ej5b: "p ⟶ (q ⟶ r) ⟹ q ⟶ (p ⟶ r)"
apply (rule impI) (* ⟦p ⟶ q ⟶ r; q⟧ ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ⟶ r; q; p⟧ ⟹ r *)
apply (erule impE, assumption) (* ⟦q; p; q ⟶ r⟧ ⟹ r *)
apply (erule impE, assumption+) (* *)
done
lemma ej5c: "p ⟶ (q ⟶ r) ⟹ q ⟶ (p ⟶ r)"
apply (rule impI)+ (* ⟦p ⟶ q ⟶ r; q; p⟧ ⟹ r *)
apply (erule impE, assumption) (* ⟦q; p; q ⟶ r⟧ ⟹ r *)
apply (erule impE, assumption+) (* *)
done
lemma ej5d: "p ⟶ (q ⟶ r) ⟹ q ⟶ (p ⟶ r)"
apply (rule impI)+ (* ⟦p ⟶ q ⟶ r; q; p⟧ ⟹ r *)
apply (erule impE, assumption+)+ (* ⟦q; p; q ⟶ r⟧ ⟹ r *)
done
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
lemma ej6a: "p ⟶ (q ⟶ r) ⟹ (p ⟶ q) ⟶ (p ⟶ r)"
apply (rule impI) (* ⟦p ⟶ q ⟶ r; p ⟶ q⟧ ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ⟶ r; p ⟶ q; p⟧ ⟹ r *)
apply (erule impE) (* ⟦p ⟶ q; p⟧ ⟹ p
⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *)
apply assumption (* ⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *)
apply (erule impE) (* ⟦p; q ⟶ r⟧ ⟹ p
⟦p; q ⟶ r; q⟧ ⟹ r *)
apply assumption (* ⟦p; q ⟶ r; q⟧ ⟹ r *)
apply (erule impE) (* ⟦p; q⟧ ⟹ q
⟦p; q; r⟧ ⟹ r *)
apply assumption (* ⟦p; q; r⟧ ⟹ r *)
apply assumption (* *)
done
lemma ej6b: "p ⟶ (q ⟶ r) ⟹ (p ⟶ q) ⟶ (p ⟶ r)"
apply (rule impI) (* ⟦p ⟶ q ⟶ r; p ⟶ q⟧ ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ⟶ r; p ⟶ q; p⟧ ⟹ r *)
apply (erule impE, assumption) (* ⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *)
apply (erule impE, assumption) (* ⟦p; q ⟶ r; q⟧ ⟹ r *)
apply (erule impE, assumption+) (* *)
done
lemma ej6c: "p ⟶ (q ⟶ r) ⟹ (p ⟶ q) ⟶ (p ⟶ r)"
apply (rule impI)+ (* ⟦p ⟶ q ⟶ r; p ⟶ q; p⟧ ⟹ r *)
apply (erule impE, assumption+)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}
lemma ej7a: "p ⟹ q ⟶ p"
apply (rule impI) (* ⟦p; q⟧ ⟹ p *)
apply assumption (* *)
done
lemma ej7b: "p ⟹ q ⟶ p"
apply (rule impI, assumption) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}
lemma ej8a: "p ⟶ (q ⟶ p)"
apply (rule impI) (* p ⟹ q ⟶ p *)
apply (rule impI) (* ⟦p; q⟧ ⟹ p *)
apply assumption (* *)
done
lemma ej8b: "p ⟶ (q ⟶ p)"
apply (rule impI)+ (* ⟦p; q⟧ ⟹ p *)
apply assumption (* *)
done
lemma ej8c: "p ⟶ (q ⟶ p)"
by (rule impI)+
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
lemma ej9a: "p ⟶ q ⟹ (q ⟶ r) ⟶ (p ⟶ r)"
apply (rule impI) (* ⟦p ⟶ q; q ⟶ r⟧ ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r *)
apply (erule mp) (* ⟦p ⟶ q; p⟧ ⟹ q *)
apply (erule mp) (* p ⟹ p *)
apply assumption (* *)
done
lemma ej9b: "p ⟶ q ⟹ (q ⟶ r) ⟶ (p ⟶ r)"
apply (rule impI)+ (* ⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r *)
apply (erule mp)+ (* p ⟹ p *)
apply assumption (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}
lemma ej10a: "p ⟶ (q ⟶ (r ⟶ s)) ⟹ r ⟶ (q ⟶ (p ⟶ s))"
apply (rule impI) (* ⟦p ⟶ q ⟶ r ⟶ s; r⟧ ⟹ q ⟶ p ⟶ s *)
apply (rule impI) (* ⟦p ⟶ q ⟶ r ⟶ s; r; q⟧ ⟹ p ⟶ s *)
apply (rule impI) (* ⟦p ⟶ q ⟶ r ⟶ s; r; q; p⟧ ⟹ s *)
apply (drule mp) (* ⟦r; q; p⟧ ⟹ p
⟦r; q; p; q ⟶ r ⟶ s⟧ ⟹ s *)
apply assumption (* ⟦r; q; p; q ⟶ r ⟶ s⟧ ⟹ s *)
apply (drule mp) (* ⟦r; q; p⟧ ⟹ q
⟦r; q; p; r ⟶ s⟧ ⟹ s *)
apply assumption (* ⟦r; q; p; r ⟶ s⟧ ⟹ s *)
apply (erule mp) (* ⟦r; q; p⟧ ⟹ r *)
apply assumption (* *)
done
lemma ej10b: "p ⟶ (q ⟶ (r ⟶ s)) ⟹ r ⟶ (q ⟶ (p ⟶ s))"
apply (rule impI) (* ⟦p ⟶ q ⟶ r ⟶ s; r⟧ ⟹ q ⟶ p ⟶ s *)
apply (rule impI) (* ⟦p ⟶ q ⟶ r ⟶ s; r; q⟧ ⟹ p ⟶ s *)
apply (rule impI) (* ⟦p ⟶ q ⟶ r ⟶ s; r; q; p⟧ ⟹ s *)
apply (drule mp, assumption) (* ⟦r; q; p; q ⟶ r ⟶ s⟧ ⟹ s *)
apply (drule mp, assumption) (* ⟦r; q; p; r ⟶ s⟧ ⟹ s *)
apply (erule mp, assumption) (* *)
done
lemma ej10c: "p ⟶ (q ⟶ (r ⟶ s)) ⟹ r ⟶ (q ⟶ (p ⟶ s))"
apply (rule impI)+ (* ⟦p ⟶ q ⟶ r ⟶ s; r; q; p⟧ ⟹ s *)
apply (drule mp, assumption+)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}
lemma ej11a: "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
apply (rule impI) (* p ⟶ q ⟶ r ⟹ (p ⟶ q) ⟶ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ⟶ r; p ⟶ q⟧ ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ⟶ r; p ⟶ q; p⟧ ⟹ r *)
apply (drule mp) (* ⟦p ⟶ q; p⟧ ⟹ p
⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *)
apply assumption (* ⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *)
apply (drule mp) (* ⟦p; q ⟶ r⟧ ⟹ p
⟦p; q ⟶ r; q⟧ ⟹ r *)
apply assumption (* ⟦p; q ⟶ r; q⟧ ⟹ r *)
apply (erule mp) (* ⟦p; q⟧ ⟹ q *)
apply assumption (* *)
done
lemma ej11b: "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
apply (rule impI)+ (* ⟦p ⟶ q ⟶ r; p ⟶ q; p⟧ ⟹ r *)
apply (drule mp, assumption+)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
lemma ej12a: "(p ⟶ q) ⟶ r ⟹ p ⟶ (q ⟶ r)"
apply (rule impI) (* ⟦(p ⟶ q) ⟶ r; p⟧ ⟹ q ⟶ r *)
apply (rule impI) (* ⟦(p ⟶ q) ⟶ r; p; q⟧ ⟹ r *)
apply (drule mp) (* ⟦p; q⟧ ⟹ p ⟶ q
⟦p; q; r⟧ ⟹ r *)
apply (rule impI) (* ⟦p; q; p⟧ ⟹ q
⟦p; q; r⟧ ⟹ r *)
apply assumption (* ⟦p; q; r⟧ ⟹ r *)
apply assumption (* *)
done
lemma ej12b: "(p ⟶ q) ⟶ r ⟹ p ⟶ (q ⟶ r)"
apply (rule impI)+ (* ⟦(p ⟶ q) ⟶ r; p; q⟧ ⟹ r *)
apply (drule mp) (* ⟦p; q⟧ ⟹ p ⟶ q
⟦p; q; r⟧ ⟹ r *)
apply (rule impI) (* ⟦p; q; p⟧ ⟹ q
⟦p; q; r⟧ ⟹ r *)
apply assumption+ (* *)
done
lemma ej12c: "(p ⟶ q) ⟶ r ⟹ p ⟶ (q ⟶ r)"
apply (rule impI)+ (* ⟦(p ⟶ q) ⟶ r; p; q⟧ ⟹ r *)
apply (drule mp) (* ⟦p; q⟧ ⟹ p ⟶ q
⟦p; q; r⟧ ⟹ r *)
apply (rule impI,
assumption+) (* *)
done
lemma ej12e: "(p ⟶ q) ⟶ r ⟹ p ⟶ (q ⟶ r)"
apply (rule impI)+ (* ⟦(p ⟶ q) ⟶ r; p; q⟧ ⟹ r *)
apply (rule_tac P="p ⟶ q" in mp)
(* ⟦(p ⟶ q) ⟶ r; p; q⟧ ⟹ (p ⟶ q) ⟶ r
⟦(p ⟶ q) ⟶ r; p; q⟧ ⟹ p ⟶ q *)
apply assumption (* ⟦(p ⟶ q) ⟶ r; p; q⟧ ⟹ p ⟶ q *)
apply (rule impI) (* ⟦(p ⟶ q) ⟶ r; p; q; p⟧ ⟹ q *)
apply assumption (* *)
done
section {* Conjunciones *}
text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}
lemma ej13: "⟦p; q⟧ ⟹ p ∧ q"
apply (rule conjI) (* ⟦p; q⟧ ⟹ p
⟦p; q⟧ ⟹ q *)
apply assumption (* ⟦p; q⟧ ⟹ q *)
apply assumption (* *)
done
lemma ej13b: "⟦p; q⟧ ⟹ p ∧ q"
apply (rule conjI) (* ⟦p; q⟧ ⟹ p
⟦p; q⟧ ⟹ q *)
apply assumption+ (* *)
done
lemma ej13c: "⟦p; q⟧ ⟹ p ∧ q"
apply (rule conjI, assumption+)
done
lemma ej13d: "⟦p; q⟧ ⟹ p ∧ q"
by (rule conjI, assumption+)
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}
lemma ej14a: "p ∧ q ⟹ p"
apply (erule conjunct1)
done
lemma ej14b: "p ∧ q ⟹ p"
by (erule conjunct1)
text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}
lemma ej15a: "p ∧ q ⟹ q"
apply (erule conjunct2)
done
lemma ej15b: "p ∧ q ⟹ q"
by (erule conjunct2)
text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}
lemma ej16a: "p ∧ (q ∧ r) ⟹ (p ∧ q) ∧ r"
apply (rule conjI) (* p ∧ (q ∧ r) ⟹ p ∧ q
p ∧ (q ∧ r) ⟹ r *)
apply (rule conjI) (* p ∧ (q ∧ r) ⟹ p
p ∧ (q ∧ r) ⟹ q
p ∧ (q ∧ r) ⟹ r *)
apply (erule conjunct1) (* p ∧ (q ∧ r) ⟹ q
p ∧ (q ∧ r) ⟹ r *)
apply (drule conjunct2) (* q ∧ r ⟹ q
p ∧ (q ∧ r) ⟹ r *)
apply (erule conjunct1) (* p ∧ (q ∧ r) ⟹ r *)
apply (drule conjunct2) (* q ∧ r ⟹ r *)
apply (erule conjunct2) (* *)
done
lemma ej16b: "p ∧ (q ∧ r) ⟹ (p ∧ q) ∧ r"
apply (rule conjI)+ (* p ∧ (q ∧ r) ⟹ p
p ∧ (q ∧ r) ⟹ q
p ∧ (q ∧ r) ⟹ r *)
apply (erule conjE) (* ⟦p; q ∧ r⟧ ⟹ p
p ∧ (q ∧ r) ⟹ q
p ∧ (q ∧ r) ⟹ r *)
apply assumption (* p ∧ (q ∧ r) ⟹ q
p ∧ (q ∧ r) ⟹ r *)
apply (erule conjE)+ (* ⟦p; q; r⟧ ⟹ q
p ∧ (q ∧ r) ⟹ r *)
apply assumption (* p ∧ (q ∧ r) ⟹ r *)
apply (erule conjE)+ (* ⟦p; q; r⟧ ⟹ r *)
apply assumption (* *)
done
lemma ej16c: "p ∧ (q ∧ r) ⟹ (p ∧ q) ∧ r"
apply (rule conjI)+ (* p ∧ (q ∧ r) ⟹ p
p ∧ (q ∧ r) ⟹ q
p ∧ (q ∧ r) ⟹ r *)
apply (erule conjE,
assumption) (* p ∧ (q ∧ r) ⟹ q
p ∧ (q ∧ r) ⟹ r *)
apply ((erule conjE)+,
assumption) (* p ∧ (q ∧ r) ⟹ r *)
apply ((erule conjE)+,
assumption) (* *)
done
lemma ej16d: "p ∧ (q ∧ r) ⟹ (p ∧ q) ∧ r"
apply (rule conjI)+ (* p ∧ (q ∧ r) ⟹ p
p ∧ (q ∧ r) ⟹ q
p ∧ (q ∧ r) ⟹ r *)
apply ((erule conjE)+,
assumption)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
lemma ej17a: "(p ∧ q) ∧ r ⟹ p ∧ (q ∧ r)"
apply (rule conjI) (* (p ∧ q) ∧ r ⟹ p
(p ∧ q) ∧ r ⟹ q ∧ r *)
apply (drule conjunct1) (* p ∧ q ⟹ p
(p ∧ q) ∧ r ⟹ q ∧ r *)
apply (erule conjunct1) (* (p ∧ q) ∧ r ⟹ q ∧ r *)
apply (rule conjI) (* (p ∧ q) ∧ r ⟹ q
(p ∧ q) ∧ r ⟹ r *)
apply (drule conjunct1) (* p ∧ q ⟹ q
(p ∧ q) ∧ r ⟹ r *)
apply (erule conjunct2) (* (p ∧ q) ∧ r ⟹ r *)
apply (erule conjunct2) (* *)
done
lemma ej17b: "(p ∧ q) ∧ r ⟹ p ∧ (q ∧ r)"
apply (erule conjE) (* ⟦p ∧ q; r⟧ ⟹ p ∧ (q ∧ r) *)
apply (erule conjE) (* ⟦r; p; q⟧ ⟹ p ∧ (q ∧ r) *)
apply (erule conjI) (* ⟦r; q⟧ ⟹ q ∧ r *)
apply (erule conjI) (* r ⟹ r *)
apply assumption (* *)
done
lemma ej17c: "(p ∧ q) ∧ r ⟹ p ∧ (q ∧ r)"
apply (erule conjE)+ (* ⟦r; p; q⟧ ⟹ p ∧ (q ∧ r) *)
apply (erule conjI)+ (* r ⟹ r *)
apply assumption (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ej18: "p ∧ q ⟹ p ⟶ q"
apply (rule impI) (* ⟦p ∧ q; p⟧ ⟹ q *)
apply (erule conjunct2) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}
lemma ej19a: "(p ⟶ q) ∧ (p ⟶ r) ⟹ p ⟶ q ∧ r"
apply (rule impI) (* ⟦(p ⟶ q) ∧ (p ⟶ r); p⟧ ⟹ q ∧ r *)
apply (rule conjI) (* ⟦(p ⟶ q) ∧ (p ⟶ r); p⟧ ⟹ q
⟦(p ⟶ q) ∧ (p ⟶ r); p⟧ ⟹ r *)
apply (drule conjunct1) (* ⟦p; p ⟶ q⟧ ⟹ q *)
apply (erule mp) (* p ⟹ p
⟦(p ⟶ q) ∧ (p ⟶ r); p⟧ ⟹ r *)
apply assumption (* ⟦(p ⟶ q) ∧ (p ⟶ r); p⟧ ⟹ r *)
apply (drule conjunct2) (* ⟦p; p ⟶ r⟧ ⟹ r *)
apply (erule mp) (* p ⟹ p *)
apply assumption (* *)
done
lemma ej19b: "(p ⟶ q) ∧ (p ⟶ r) ⟹ p ⟶ q ∧ r"
apply (erule conjE) (* ⟦p ⟶ q; p ⟶ r⟧ ⟹ p ⟶ q ∧ r *)
apply (rule impI) (* ⟦p ⟶ q; p ⟶ r; p⟧ ⟹ q ∧ r *)
apply (rule conjI) (* ⟦p ⟶ q; p ⟶ r; p⟧ ⟹ q
⟦p ⟶ q; p ⟶ r; p⟧ ⟹ r *)
apply (erule mp) (* ⟦p ⟶ r; p⟧ ⟹ p
⟦p ⟶ q; p ⟶ r; p⟧ ⟹ r *)
apply assumption (* ⟦p ⟶ q; p ⟶ r; p⟧ ⟹ r *)
apply (erule mp) (* ⟦p ⟶ q; p⟧ ⟹ p *)
apply assumption (* *)
done
lemma ej19c: "(p ⟶ q) ∧ (p ⟶ r) ⟹ p ⟶ q ∧ r"
apply (erule conjE) (* ⟦p ⟶ q; p ⟶ r⟧ ⟹ p ⟶ q ∧ r *)
apply (rule impI) (* ⟦p ⟶ q; p ⟶ r; p⟧ ⟹ q ∧ r *)
apply (rule conjI) (* ⟦p ⟶ q; p ⟶ r; p⟧ ⟹ q
⟦p ⟶ q; p ⟶ r; p⟧ ⟹ r *)
apply (erule mp,
assumption) (* ⟦p ⟶ q; p ⟶ r; p⟧ ⟹ r *)
apply (erule mp,
assumption) (* *)
done
lemma ej19d: "(p ⟶ q) ∧ (p ⟶ r) ⟹ p ⟶ q ∧ r"
apply (erule conjE) (* ⟦p ⟶ q; p ⟶ r⟧ ⟹ p ⟶ q ∧ r *)
apply (rule impI) (* ⟦p ⟶ q; p ⟶ r; p⟧ ⟹ q ∧ r *)
apply (rule conjI) (* ⟦p ⟶ q; p ⟶ r; p⟧ ⟹ q
⟦p ⟶ q; p ⟶ r; p⟧ ⟹ r *)
apply (erule mp,
assumption)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}
lemma ej20a: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)"
apply (rule conjI) (* p ⟶ q ∧ r ⟹ p ⟶ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ∧ r; p⟧ ⟹ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (drule mp) (* p ⟹ p
⟦p; q ∧ r⟧ ⟹ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply assumption (* ⟦p; q ∧ r⟧ ⟹ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (erule conjunct1) (* p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ∧ r; p⟧ ⟹ r *)
apply (drule mp) (* p ⟹ p
⟦p; q ∧ r⟧ ⟹ r *)
apply assumption (* ⟦p; q ∧ r⟧ ⟹ r *)
apply (erule conjunct2) (* *)
done
lemma ej20b: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)"
apply (rule conjI) (* p ⟶ q ∧ r ⟹ p ⟶ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ∧ r; p⟧ ⟹ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (drule mp,
assumption) (* ⟦p; q ∧ r⟧ ⟹ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (erule conjunct1) (* p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ∧ r; p⟧ ⟹ r *)
apply (drule mp,
assumption) (* ⟦p; q ∧ r⟧ ⟹ r *)
apply (erule conjunct2) (* *)
done
lemma ej20c: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)"
apply (rule conjI) (* p ⟶ q ∧ r ⟹ p ⟶ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ∧ r; p⟧ ⟹ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (drule mp,
assumption,
erule conjunct1) (* p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI) (* ⟦p ⟶ q ∧ r; p⟧ ⟹ r *)
apply (drule mp,
assumption,
erule conjunct2) (* *)
done
lemma ej20d: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)"
apply (rule conjI) (* p ⟶ q ∧ r ⟹ p ⟶ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI,
drule mp,
assumption,
erule conjunct1) (* p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI,
drule mp,
assumption,
erule conjunct2) (* *)
done
lemma ej20e: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)"
apply (rule conjI) (* p ⟶ q ∧ r ⟹ p ⟶ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI,
drule mp,
assumption,
erule conjE) (* ⟦p; q; r⟧ ⟹ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply assumption (* p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI,
drule mp,
assumption,
erule conjE) (* ⟦p; q; r⟧ ⟹ r *)
apply assumption (* *)
done
lemma ej20f: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)"
apply (rule conjI) (* p ⟶ q ∧ r ⟹ p ⟶ q
p ⟶ q ∧ r ⟹ p ⟶ r *)
apply (rule impI,
drule mp,
assumption,
erule conjE,
assumption)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
lemma ej21a: "p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r"
apply (rule impI) (* ⟦p ⟶ (q ⟶ r); p ∧ q⟧ ⟹ r *)
apply (frule conjunct1) (* ⟦p ⟶ (q ⟶ r); p ∧ q; p⟧ ⟹ r *)
apply (drule mp) (* ⟦p ∧ q; p⟧ ⟹ p
⟦p ∧ q; p; q ⟶ r⟧ ⟹ r *)
apply assumption (* ⟦p ∧ q; p; q ⟶ r⟧ ⟹ r *)
apply (drule conjunct2) (* ⟦p; q ⟶ r; q⟧ ⟹ r *)
apply (erule mp) (* ⟦p; q⟧ ⟹ q *)
apply assumption (* *)
done
lemma ej21b: "p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r"
apply (rule impI) (* ⟦p ⟶ (q ⟶ r); p ∧ q⟧ ⟹ r *)
apply (erule conjE) (* ⟦p ⟶ (q ⟶ r); p; q⟧ ⟹ r *)
apply (drule mp) (* ⟦p; q⟧ ⟹ p
⟦p; q; q ⟶ r⟧ ⟹ r *)
apply assumption (* ⟦p; q; q ⟶ r⟧ ⟹ r *)
apply (erule mp) (* ⟦p; q⟧ ⟹ q *)
apply assumption (* *)
done
lemma ej21c: "p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r"
apply (rule impI) (* ⟦p ⟶ (q ⟶ r); p ∧ q⟧ ⟹ r *)
apply (erule conjE) (* ⟦p ⟶ (q ⟶ r); p; q⟧ ⟹ r *)
apply (drule mp,
assumption) (* ⟦p; q; q ⟶ r⟧ ⟹ r *)
apply (erule mp,
assumption) (* *)
done
lemma ej21d: "p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r"
apply (rule impI) (* ⟦p ⟶ (q ⟶ r); p ∧ q⟧ ⟹ r *)
apply (erule conjE) (* ⟦p ⟶ (q ⟶ r); p; q⟧ ⟹ r *)
apply (drule mp,
assumption+)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
lemma ej22a: "p ∧ q ⟶ r ⟹ p ⟶ (q ⟶ r)"
apply (rule impI) (* ⟦p ∧ q ⟶ r; p⟧ ⟹ q ⟶ r *)
apply (rule impI) (* ⟦p ∧ q ⟶ r; p; q⟧ ⟹ r *)
apply (erule mp) (* ⟦p; q⟧ ⟹ p ∧ q *)
apply (rule conjI) (* ⟦p; q⟧ ⟹ p
⟦p; q⟧ ⟹ q *)
apply assumption (* ⟦p; q⟧ ⟹ q *)
apply assumption (* *)
done
lemma ej22b: "p ∧ q ⟶ r ⟹ p ⟶ (q ⟶ r)"
apply (rule impI)+ (* ⟦p ∧ q ⟶ r; p; q⟧ ⟹ r *)
apply (erule mp) (* ⟦p; q⟧ ⟹ p ∧ q *)
apply (erule conjI) (* q ⟹ q *)
apply assumption (* *)
done
lemma ej22c: "p ∧ q ⟶ r ⟹ p ⟶ (q ⟶ r)"
apply (rule impI)+ (* ⟦p ∧ q ⟶ r; p; q⟧ ⟹ r *)
apply (erule mp) (* ⟦p; q⟧ ⟹ p ∧ q *)
apply (erule conjI,
assumption) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
lemma ej23a: "(p ⟶ q) ⟶ r ⟹ p ∧ q ⟶ r"
apply (rule impI) (* ⟦(p ⟶ q) ⟶ r; p ∧ q⟧ ⟹ r *)
apply (erule mp) (* p ∧ q ⟹ p ⟶ q *)
apply (rule impI) (* ⟦p ∧ q; p⟧ ⟹ q *)
apply (erule conjunct2) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
lemma ej24a: "p ∧ (q ⟶ r) ⟹ (p ⟶ q) ⟶ r"
apply (rule impI) (* ⟦p ∧ (q ⟶ r); p ⟶ q⟧ ⟹ r *)
apply (frule conjunct1) (* ⟦p ∧ (q ⟶ r); p ⟶ q; p⟧ ⟹ r *)
apply (drule mp) (* ⟦p ∧ (q ⟶ r); p⟧ ⟹ p
⟦p ∧ (q ⟶ r); p; q⟧ ⟹ r *)
apply assumption (* ⟦p ∧ (q ⟶ r); p; q⟧ ⟹ r *)
apply (drule conjunct2) (* p; q; q ⟶ r⟧ ⟹ r *)
apply (erule mp) (* ⟦p; q⟧ ⟹ q *)
apply assumption (* *)
done
lemma ej24b: "p ∧ (q ⟶ r) ⟹ (p ⟶ q) ⟶ r"
apply (rule impI) (* ⟦p ∧ (q ⟶ r); p ⟶ q⟧ ⟹ r *)
apply (erule conjE) (* ⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *)
apply (drule mp) (* ⟦p; q ⟶ r⟧ ⟹ p
⟦p; q ⟶ r; q⟧ ⟹ r *)
apply assumption (* ⟦p; q ⟶ r; q⟧ ⟹ r *)
apply (erule mp) (* ⟦p; q⟧ ⟹ q *)
apply assumption (* *)
done
lemma ej24c: "p ∧ (q ⟶ r) ⟹ (p ⟶ q) ⟶ r"
apply (rule impI) (* ⟦p ∧ (q ⟶ r); p ⟶ q⟧ ⟹ r *)
apply (erule conjE) (* ⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *)
apply (drule mp,
assumption+)+ (* *)
done
section {* Disyunciones *}
text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}
lemma ej25: "p ⟹ p ∨ q"
apply (erule disjI1) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}
lemma ej26: "q ⟹ p ∨ q"
apply (erule disjI2) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}
lemma ej27: "p ∨ q ⟹ q ∨ p"
apply (erule disjE) (* p ⟹ q ∨ p
q ⟹ q ∨ p *)
apply (erule disjI2) (* q ⟹ q ∨ p *)
apply (erule disjI1) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}
lemma ej28: "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r"
apply (rule impI) (* ⟦q ⟶ r; p ∨ q⟧ ⟹ p ∨ r *)
apply (erule disjE) (* ⟦q ⟶ r; p⟧ ⟹ p ∨ r
⟦q ⟶ r; q⟧ ⟹ p ∨ r *)
apply (erule disjI1) (* ⟦q ⟶ r; q⟧ ⟹ p ∨ r *)
apply (drule mp) (* q ⟹ q
⟦q; r⟧ ⟹ p ∨ r *)
apply assumption (* ⟦q; r⟧ ⟹ p ∨ r *)
apply (erule disjI2) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}
lemma ej29: "p ∨ p ⟹ p"
apply (erule disjE) (* p ⟹ p
p ⟹ p *)
apply assumption+
done
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
lemma ej30: "p ⟹ p ∨ p"
apply (erule disjI1) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}
lemma ej31a: "p ∨ (q ∨ r) ⟹ (p ∨ q) ∨ r"
apply (erule disjE) (* p ⟹ (p ∨ q) ∨ r
q ∨ r ⟹ (p ∨ q) ∨ r *)
apply (rule disjI1) (* p ⟹ p ∨ q
q ∨ r ⟹ (p ∨ q) ∨ r *)
apply (erule disjI1) (* q ∨ r ⟹ (p ∨ q) ∨ r *)
apply (erule disjE) (* q ⟹ (p ∨ q) ∨ r
r ⟹ (p ∨ q) ∨ r *)
apply (rule disjI1) (* q ⟹ p ∨ q
r ⟹ (p ∨ q) ∨ r *)
apply (erule disjI2) (* r ⟹ (p ∨ q) ∨ r *)
apply (erule disjI2) (* *)
done
lemma ej31b: "p ∨ (q ∨ r) ⟹ (p ∨ q) ∨ r"
apply (erule disjE) (* p ⟹ (p ∨ q) ∨ r
q ∨ r ⟹ (p ∨ q) ∨ r *)
apply (rule disjI1) (* p ⟹ p ∨ q
q ∨ r ⟹ (p ∨ q) ∨ r *)
apply (erule disjI1) (* q ∨ r ⟹ (p ∨ q) ∨ r *)
apply (erule disjE) (* q ⟹ (p ∨ q) ∨ r
r ⟹ (p ∨ q) ∨ r *)
apply (rule disjI1,
erule disjI2) (* r ⟹ (p ∨ q) ∨ r *)
apply (erule disjI2) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}
lemma ej32a: "(p ∨ q) ∨ r ⟹ p ∨ (q ∨ r)"
apply (erule disjE) (* p ∨ q ⟹ p ∨ (q ∨ r)
r ⟹ p ∨ (q ∨ r) *)
apply (erule disjE) (* p ⟹ p ∨ (q ∨ r)
q ⟹ p ∨ (q ∨ r)
r ⟹ p ∨ (q ∨ r) *)
apply (erule disjI1) (* q ⟹ p ∨ (q ∨ r)
r ⟹ p ∨ (q ∨ r) *)
apply (rule disjI2) (* q ⟹ q ∨ r
r ⟹ p ∨ (q ∨ r) *)
apply (erule disjI1) (* r ⟹ p ∨ (q ∨ r) *)
apply (rule disjI2) (* r ⟹ q ∨ r *)
apply (erule disjI2) (* *)
done
lemma ej32b: "(p ∨ q) ∨ r ⟹ p ∨ (q ∨ r)"
apply (erule disjE) (* p ∨ q ⟹ p ∨ (q ∨ r)
r ⟹ p ∨ (q ∨ r) *)
apply (erule disjE) (* p ⟹ p ∨ (q ∨ r)
q ⟹ p ∨ (q ∨ r)
r ⟹ p ∨ (q ∨ r) *)
apply (erule disjI1) (* q ⟹ p ∨ (q ∨ r)
r ⟹ p ∨ (q ∨ r) *)
apply (rule disjI2,
erule disjI1) (* r ⟹ p ∨ (q ∨ r) *)
apply (rule disjI2,
erule disjI2) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}
lemma ej33a: "p ∧ (q ∨ r) ⟹ (p ∧ q) ∨ (p ∧ r)"
apply (erule conjE) (* ⟦p; q ∨ r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *)
apply (erule disjE) (* ⟦p; q⟧ ⟹ (p ∧ q) ∨ (p ∧ r)
⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *)
apply (rule disjI1) (* ⟦p; q⟧ ⟹ p ∧ q
⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *)
apply (rule conjI) (* ⟦p; q⟧ ⟹ p
⟦p; q⟧ ⟹ q
⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *)
apply assumption (* ⟦p; q⟧ ⟹ q
⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *)
apply assumption (* ⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *)
apply (rule disjI2) (* ⟦p; r⟧ ⟹ p ∧ r *)
apply (rule conjI) (* ⟦p; r⟧ ⟹ p
⟦p; r⟧ ⟹ r *)
apply assumption (* ⟦p; r⟧ ⟹ r *)
apply assumption (* *)
done
lemma ej33b: "p ∧ (q ∨ r) ⟹ (p ∧ q) ∨ (p ∧ r)"
apply (erule conjE) (* ⟦p; q ∨ r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *)
apply (erule disjE) (* ⟦p; q⟧ ⟹ (p ∧ q) ∨ (p ∧ r)
⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *)
apply (rule disjI1) (* ⟦p; q⟧ ⟹ p ∧ q
⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *)
apply (erule conjI,
assumption) (* ⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *)
apply (rule disjI2) (* ⟦p; r⟧ ⟹ p ∧ r *)
apply (erule conjI,
assumption) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}
lemma ej34a: "(p ∧ q) ∨ (p ∧ r) ⟹ p ∧ (q ∨ r)"
apply (erule disjE) (* p ∧ q ⟹ p ∧ (q ∨ r)
p ∧ r ⟹ p ∧ (q ∨ r) *)
apply (erule conjE) (* ⟦p; q⟧ ⟹ p ∧ (q ∨ r)
p ∧ r ⟹ p ∧ (q ∨ r) *)
apply (rule conjI) (* ⟦p; q⟧ ⟹ p
⟦p; q⟧ ⟹ q ∨ r
p ∧ r ⟹ p ∧ (q ∨ r) *)
apply assumption (* ⟦p; q⟧ ⟹ q ∨ r
p ∧ r ⟹ p ∧ (q ∨ r) *)
apply (rule disjI1) (* ⟦p; q⟧ ⟹ q
p ∧ r ⟹ p ∧ (q ∨ r) *)
apply assumption (* p ∧ r ⟹ p ∧ (q ∨ r) *)
apply (erule conjE) (* ⟦p; r⟧ ⟹ p ∧ (q ∨ r) *)
apply (rule conjI) (* ⟦p; r⟧ ⟹ p
⟦p; r⟧ ⟹ q ∨ r *)
apply assumption (* ⟦p; r⟧ ⟹ q ∨ r *)
apply (erule disjI2) (* *)
done
lemma ej34b: "(p ∧ q) ∨ (p ∧ r) ⟹ p ∧ (q ∨ r)"
apply (erule disjE) (* p ∧ q ⟹ p ∧ (q ∨ r)
p ∧ r ⟹ p ∧ (q ∨ r) *)
apply (erule conjE) (* ⟦p; q⟧ ⟹ p ∧ (q ∨ r)
p ∧ r ⟹ p ∧ (q ∨ r) *)
apply (rule conjI,
assumption) (* ⟦p; q⟧ ⟹ q ∨ r
p ∧ r ⟹ p ∧ (q ∨ r) *)
apply (rule disjI1,
assumption) (* p ∧ r ⟹ p ∧ (q ∨ r) *)
apply (erule conjE) (* ⟦p; r⟧ ⟹ p ∧ (q ∨ r) *)
apply (rule conjI,
assumption) (* ⟦p; r⟧ ⟹ q ∨ r *)
apply (erule disjI2) (* *)
done
lemma ej34c: "(p ∧ q) ∨ (p ∧ r) ⟹ p ∧ (q ∨ r)"
apply (rule conjI) (* (p ∧ q) ∨ (p ∧ r) ⟹ p
(p ∧ q) ∨ (p ∧ r) ⟹ q ∨ r *)
apply (erule disjE) (* p ∧ q ⟹ p
p ∧ r ⟹ p
(p ∧ q) ∨ (p ∧ r) ⟹ q ∨ r *)
apply (erule conjunct1) (* p ∧ r ⟹ p
(p ∧ q) ∨ (p ∧ r) ⟹ q ∨ r *)
apply (erule conjunct1) (* (p ∧ q) ∨ (p ∧ r) ⟹ q ∨ r *)
apply (erule disjE) (* p ∧ q ⟹ q ∨ r
p ∧ r ⟹ q ∨ r *)
apply (drule conjunct2) (* q ⟹ q ∨ r
p ∧ r ⟹ q ∨ r *)
apply (rule disjI1) (* q ⟹ q
p ∧ r ⟹ q ∨ r *)
apply assumption (* p ∧ r ⟹ q ∨ r *)
apply (drule conjunct2) (* r ⟹ q ∨ r *)
apply (erule disjI2) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}
lemma ej35a: "p ∨ (q ∧ r) ⟹ (p ∨ q) ∧ (p ∨ r)"
apply (erule disjE) (* p ⟹ (p ∨ q) ∧ (p ∨ r)
q ∧ r ⟹ (p ∨ q) ∧ (p ∨ r) *)
apply (rule conjI) (* p ⟹ p ∨ q
p ⟹ p ∨ r
q ∧ r ⟹ (p ∨ q) ∧ (p ∨ r) *)
apply (erule disjI1) (* p ⟹ p ∨ r
q ∧ r ⟹ (p ∨ q) ∧ (p ∨ r) *)
apply (erule disjI1) (* q ∧ r ⟹ (p ∨ q) ∧ (p ∨ r) *)
apply (erule conjE) (* ⟦q; r⟧ ⟹ (p ∨ q) ∧ (p ∨ r) *)
apply (rule conjI) (* ⟦q; r⟧ ⟹ p ∨ q
⟦q; r⟧ ⟹ p ∨ r *)
apply (erule disjI2) (* ⟦q; r⟧ ⟹ p ∨ r *)
apply (erule disjI2) (* *)
done
lemma ej35b: "p ∨ (q ∧ r) ⟹ (p ∨ q) ∧ (p ∨ r)"
apply (rule conjI) (* p ∨ (q ∧ r) ⟹ p ∨ q
p ∨ (q ∧ r) ⟹ p ∨ r *)
apply (erule disjE) (* p ⟹ p ∨ q
q ∧ r ⟹ p ∨ q
p ∨ (q ∧ r) ⟹ p ∨ r *)
apply (erule disjI1) (* q ∧ r ⟹ p ∨ q
p ∨ (q ∧ r) ⟹ p ∨ r *)
apply (drule conjunct1) (* q ⟹ p ∨ q
p ∨ (q ∧ r) ⟹ p ∨ r *)
apply (erule disjI2) (* p ∨ (q ∧ r) ⟹ p ∨ r *)
apply (erule disjE) (* p ⟹ p ∨ r
q ∧ r ⟹ p ∨ r *)
apply (erule disjI1) (* q ∧ r ⟹ p ∨ r *)
apply (drule conjunct2) (* r ⟹ p ∨ r *)
apply (erule disjI2) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}
lemma ej36a: "(p ∨ q) ∧ (p ∨ r) ⟹ p ∨ (q ∧ r)"
apply (erule conjE) (* ⟦p ∨ q; p ∨ r⟧ ⟹ p ∨ (q ∧ r) *)
apply (erule disjE) (* ⟦p ∨ r; p⟧ ⟹ p ∨ (q ∧ r)
⟦p ∨ r; q⟧ ⟹ p ∨ (q ∧ r) *)
apply (erule disjI1) (* ⟦p ∨ r; q⟧ ⟹ p ∨ (q ∧ r) *)
apply (erule disjE) (* ⟦q; p⟧ ⟹ p ∨ (q ∧ r)
⟦q; r⟧ ⟹ p ∨ (q ∧ r) *)
apply (erule disjI1) (* ⟦q; r⟧ ⟹ p ∨ (q ∧ r) *)
apply (rule disjI2) (* ⟦q; r⟧ ⟹ q ∧ r *)
apply (rule conjI) (* ⟦q; r⟧ ⟹ q
⟦q; r⟧ ⟹ r *)
apply assumption (* ⟦q; r⟧ ⟹ r *)
apply assumption (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}
lemma ej37a: "(p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟶ r"
apply (rule impI) (* ⟦(p ⟶ r) ∧ (q ⟶ r); p ∨ q⟧ ⟹ r *)
apply (erule conjE) (* ⟦p ∨ q; p ⟶ r; q ⟶ r⟧ ⟹ r *)
apply (erule disjE) (* ⟦p ⟶ r; q ⟶ r; p⟧ ⟹ r
⟦p ⟶ r; q ⟶ r; q⟧ ⟹ r *)
apply (erule mp) (* ⟦q ⟶ r; p⟧ ⟹ p
⟦p ⟶ r; q ⟶ r; q⟧ ⟹ r *)
apply assumption (* ⟦p ⟶ r; q ⟶ r; q⟧ ⟹ r *)
apply (erule_tac P=q in mp) (* ⟦p ⟶ r; q⟧ ⟹ q *)
apply assumption (* *)
done
lemma ej37b: "(p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟶ r"
apply (rule impI) (* (p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟹ r *)
apply (erule conjE) (* ⟦p ∨ q; p ⟶ r; q ⟶ r⟧ ⟹ r *)
apply (erule disjE) (* ⟦p ⟶ r; q ⟶ r; p⟧ ⟹ r
⟦p ⟶ r; q ⟶ r; q⟧ ⟹ r *)
apply (erule mp,
assumption+)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}
lemma ej38a: "p ∨ q ⟶ r ⟹ (p ⟶ r) ∧ (q ⟶ r)"
apply (rule conjI) (* p ∨ q ⟶ r ⟹ p ⟶ r
p ∨ q ⟶ r ⟹ q ⟶ r *)
apply (rule impI) (* ⟦p ∨ q ⟶ r; p⟧ ⟹ r
p ∨ q ⟶ r ⟹ q ⟶ r *)
apply (erule mp) (* p ⟹ p ∨ q
p ∨ q ⟶ r ⟹ q ⟶ r *)
apply (erule disjI1) (* p ∨ q ⟶ r ⟹ q ⟶ r *)
apply (rule impI) (* ⟦p ∨ q ⟶ r; q⟧ ⟹ r *)
apply (erule mp) (* q ⟹ p ∨ q *)
apply (erule disjI2) (* *)
done
section {* Negación *}
text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}
lemma ej39: "p ⟹ ¬¬p"
apply (rule notI) (* ⟦p; ¬ p⟧ ⟹ False *)
apply (erule notE) (* p ⟹ p *)
apply assumption (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ej40: "¬p ⟹ p ⟶ q"
apply (rule impI) (* ⟦¬ p; p⟧ ⟹ q *)
apply (erule notE) (* p ⟹ p *)
apply assumption (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}
lemma ej41: "p ⟶ q ⟹ ¬q ⟶ ¬p"
apply (rule impI) (* ⟦p ⟶ q; ¬ q⟧ ⟹ ¬ p *)
apply (rule notI) (* ⟦p ⟶ q; ¬ q; p⟧ ⟹ False *)
apply (drule mp) (* ⟦¬ q; p⟧ ⟹ p
⟦¬ q; p; q⟧ ⟹ False *)
apply assumption (* ⟦¬ q; p; q⟧ ⟹ False *)
apply (erule notE) (* ⟦p; q⟧ ⟹ q *)
apply assumption (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬q ⊢ p
------------------------------------------------------------------ *}
lemma ej42: "⟦p ∨ q; ¬q⟧ ⟹ p"
apply (erule disjE) (* ⟦¬ q; p⟧ ⟹ p
⟦¬ q; q⟧ ⟹ p *)
apply assumption (* ⟦¬ q; q⟧ ⟹ p *)
apply (erule notE) (* q ⟹ q *)
apply assumption (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 43. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}
lemma ej43: "⟦p ∨ q; ¬p⟧ ⟹ q"
apply (erule disjE) (* ⟦¬ p; p⟧ ⟹ q
⟦¬ p; q⟧ ⟹ q *)
apply (erule notE) (* p ⟹ p
⟦¬ p; q⟧ ⟹ q *)
apply assumption (* ⟦¬ p; q⟧ ⟹ q *)
apply assumption (* ⟦¬ p; q⟧ ⟹ q *)
done
text {* ---------------------------------------------------------------
Ejercicio 44. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}
lemma ej44a: "p ∨ q ⟹ ¬(¬p ∧ ¬q)"
apply (rule notI) (* ⟦p ∨ q; ¬ p ∧ ¬ q⟧ ⟹ False *)
apply (erule conjE) (* ⟦p ∨ q; ¬ p; ¬ q⟧ ⟹ False *)
apply (erule disjE) (* ⟦¬ p; ¬ q; p⟧ ⟹ False
⟦¬ p; ¬ q; q⟧ ⟹ False *)
apply (erule notE) (* ⟦¬ q; p⟧ ⟹ p
⟦¬ p; ¬ q; q⟧ ⟹ False *)
apply assumption (* ⟦¬ p; ¬ q; q⟧ ⟹ False *)
apply (erule_tac P=q in notE) (* ⟦¬ p; q⟧ ⟹ q *)
apply assumption (* *)
done
lemma ej44: "p ∨ q ⟹ ¬(¬p ∧ ¬q)"
apply (rule notI) (* ⟦p ∨ q; ¬ p ∧ ¬ q⟧ ⟹ False *)
apply (erule conjE) (* ⟦p ∨ q; ¬ p; ¬ q⟧ ⟹ False *)
apply (erule disjE) (* ⟦¬ p; ¬ q; p⟧ ⟹ False
⟦¬ p; ¬ q; q⟧ ⟹ False *)
apply (erule notE, assumption)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}
lemma ej45a: "p ∧ q ⟹ ¬(¬p ∨ ¬q)"
apply (rule notI) (* ⟦p ∧ q; ¬ p ∨ ¬ q⟧ ⟹ False *)
apply (erule conjE) (* ⟦¬ p ∨ ¬ q; p; q⟧ ⟹ False *)
apply (erule disjE) (* ⟦p; q; ¬ p⟧ ⟹ False
⟦p; q; ¬ q⟧ ⟹ False *)
apply (erule notE) (* ⟦p; q⟧ ⟹ p
⟦p; q; ¬ q⟧ ⟹ False *)
apply assumption (* ⟦p; q; ¬ q⟧ ⟹ False *)
apply (erule notE) (* ⟦p; q⟧ ⟹ q *)
apply assumption (* *)
done
lemma ej45b: "p ∧ q ⟹ ¬(¬p ∨ ¬q)"
apply (rule notI) (* ⟦p ∧ q; ¬ p ∨ ¬ q⟧ ⟹ False *)
apply (erule conjE) (* ⟦¬ p ∨ ¬ q; p; q⟧ ⟹ False *)
apply (erule disjE) (* ⟦p; q; ¬ p⟧ ⟹ False
⟦p; q; ¬ q⟧ ⟹ False *)
apply (erule notE,
assumption) (* ⟦p; q; ¬ q⟧ ⟹ False *)
apply (erule notE,
assumption) (* *)
done
lemma ej45c: "p ∧ q ⟹ ¬(¬p ∨ ¬q)"
apply (rule notI) (* ⟦p ∧ q; ¬ p ∨ ¬ q⟧ ⟹ False *)
apply (erule conjE) (* ⟦¬ p ∨ ¬ q; p; q⟧ ⟹ False *)
apply (erule disjE) (* ⟦p; q; ¬ p⟧ ⟹ False
⟦p; q; ¬ q⟧ ⟹ False *)
apply (erule notE,
assumption)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}
lemma ej46b: "¬(p ∨ q) ⟹ ¬p ∧ ¬q"
apply (rule conjI) (* ¬ (p ∨ q) ⟹ ¬ p
¬ (p ∨ q) ⟹ ¬ q *)
apply (rule notI) (* ⟦¬ (p ∨ q); p⟧ ⟹ False
¬ (p ∨ q) ⟹ ¬ q *)
apply (erule notE) (* p ⟹ p ∨ q
¬ (p ∨ q) ⟹ ¬ q *)
apply (erule disjI1) (* ¬ (p ∨ q) ⟹ ¬ q *)
apply (rule notI) (* ⟦¬ (p ∨ q); q⟧ ⟹ False *)
apply (erule notE) (* q ⟹ p ∨ q *)
apply (erule disjI2) (* *)
done
lemma ej46b: "¬(p ∨ q) ⟹ ¬p ∧ ¬q"
apply (rule conjI) (* ¬ (p ∨ q) ⟹ ¬ p
¬ (p ∨ q) ⟹ ¬ q *)
apply (rule notI,
erule notE,
(erule disjI1 |
erule disjI2))+ (* *)
done
lemma ej46c: "¬(p ∨ q) ⟹ ¬p ∧ ¬q"
by (rule conjI,
(rule notI,
erule notE,
(erule disjI1 |
erule disjI2))+)
text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}
lemma ej47a: "¬p ∧ ¬q ⟹ ¬(p ∨ q)"
apply (rule notI) (* ⟦¬ p ∧ ¬ q; p ∨ q⟧ ⟹ False *)
apply (erule disjE) (* ⟦¬ p ∧ ¬ q; p⟧ ⟹ False
⟦¬ p ∧ ¬ q; q⟧ ⟹ False *)
apply (drule conjunct1) (* ⟦p; ¬ p⟧ ⟹ False
⟦¬ p ∧ ¬ q; q⟧ ⟹ False *)
apply (erule notE) (* p ⟹ p
⟦¬ p ∧ ¬ q; q⟧ ⟹ False *)
apply assumption (* ⟦¬ p ∧ ¬ q; q⟧ ⟹ False*)
apply (drule conjunct2) (* ⟦q; ¬ q⟧ ⟹ False *)
apply (erule notE) (* q ⟹ q *)
apply assumption (* *)
lemma ej47b: "¬p ∧ ¬q ⟹ ¬(p ∨ q)"
apply (rule notI) (* ⟦¬ p ∧ ¬ q; p ∨ q⟧ ⟹ False *)
apply (erule disjE) (* ⟦¬ p ∧ ¬ q; p⟧ ⟹ False
⟦¬ p ∧ ¬ q; q⟧ ⟹ False *)
apply ((drule conjunct1 |
drule conjunct2),
erule notE,
assumption)+ (* *)
lemma ej47: "¬p ∧ ¬q ⟹ ¬(p ∨ q)"
apply (rule notI) (* ⟦¬ p ∧ ¬ q; p ∨ q⟧ ⟹ False *)
apply (erule conjE) (* ⟦p ∨ q; ¬ p; ¬ q⟧ ⟹ False *)
apply (erule disjE)
apply (erule notE,
assumption)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}
lemma ej48a: "¬p ∨ ¬q ⟹ ¬(p ∧ q)"
apply (rule notI) (* ⟦¬ p ∨ ¬ q; p ∧ q⟧ ⟹ False *)
apply (erule disjE) (* ⟦p ∧ q; ¬ p⟧ ⟹ False
⟦p ∧ q; ¬ q⟧ ⟹ False *)
apply (drule conjunct1) (* ⟦¬ p; p⟧ ⟹ False
⟦p ∧ q; ¬ q⟧ ⟹ False *)
apply (erule notE) (* p ⟹ p
⟦p ∧ q; ¬ q⟧ ⟹ False *)
apply assumption (* ⟦p ∧ q; ¬ q⟧ ⟹ False *)
apply (drule conjunct2) (* ⟦¬ q; q⟧ ⟹ False *)
apply (erule notE) (* q ⟹ q *)
apply assumption (* *)
done
lemma ej48b: "¬p ∨ ¬q ⟹ ¬(p ∧ q)"
apply (rule notI) (* ⟦¬ p ∨ ¬ q; p ∧ q⟧ ⟹ False *)
apply (erule conjE) (* ⟦¬ p ∨ ¬ q; p; q⟧ ⟹ False *)
apply (erule disjE) (* ⟦p; q; ¬ p⟧ ⟹ False
⟦p; q; ¬ q⟧ ⟹ False *)
apply (erule notE,
assumption)+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}
lemma ej49: "¬(p ∧ ¬p)"
apply (rule notI) (* p ∧ ¬ p ⟹ False *)
apply (erule conjE) (* ⟦p; ¬ p⟧ ⟹ False *)
apply (erule notE) (* ⟦p; ¬ p⟧ ⟹ False *)
apply assumption (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}
lemma ej50: "p ∧ ¬p ⟹ q"
apply (erule conjE) (* ⟦p; ¬ p⟧ ⟹ q *)
apply (erule notE) (* p ⟹ p *)
apply assumption (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}
lemma ej51: "¬¬p ⟹ p"
apply (erule notnotD) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}
lemma ej52: "p ∨ ¬p"
apply (cut_tac P="¬p" in excluded_middle) (* ¬¬p ∨ ¬p ⟹ p ∨ ¬p*)
apply (erule disjE) (* ¬ ¬ p ⟹ p ∨ ¬ p
¬ p ⟹ p ∨ ¬ p *)
apply (rule disjI1) (* ¬ ¬ p ⟹ p
¬ p ⟹ p ∨ ¬ p *)
apply (erule notnotD) (* ¬ p ⟹ p ∨ ¬ p *)
apply (erule disjI2) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}
lemma ej53: "((p ⟶ q) ⟶ p) ⟶ p"
apply (cut_tac P="p ⟶ q" in excluded_middle)
(* ¬ (p ⟶ q) ∨ (p ⟶ q) ⟹
((p ⟶ q) ⟶ p) ⟶ p *)
apply (erule disjE) (* ¬ (p ⟶ q) ⟹ ((p ⟶ q) ⟶ p) ⟶ p
p ⟶ q ⟹ ((p ⟶ q) ⟶ p) ⟶ p *)
apply (rule impI) (* ⟦¬ (p ⟶ q); (p ⟶ q) ⟶ p⟧ ⟹ p
p ⟶ q ⟹ ((p ⟶ q) ⟶ p) ⟶ p *)
apply (rule ccontr) (* ⟦¬ (p ⟶ q); (p ⟶ q) ⟶ p; ¬ p⟧ ⟹ False
p ⟶ q ⟹ ((p ⟶ q) ⟶ p) ⟶ p *)
apply (erule_tac P="p ⟶ q" in notE)
(* ⟦(p ⟶ q) ⟶ p; ¬ p⟧ ⟹ p ⟶ q
p ⟶ q ⟹ ((p ⟶ q) ⟶ p) ⟶ p *)
apply (rule impI) (* ⟦(p ⟶ q) ⟶ p; ¬ p; p⟧ ⟹ q
p ⟶ q ⟹ ((p ⟶ q) ⟶ p) ⟶ p *)
apply (erule notE) (* ⟦(p ⟶ q) ⟶ p; p⟧ ⟹ p
p ⟶ q ⟹ ((p ⟶ q) ⟶ p) ⟶ p *)
apply assumption (* p ⟶ q ⟹ ((p ⟶ q) ⟶ p) ⟶ p *)
apply (rule impI) (* ⟦p ⟶ q; (p ⟶ q) ⟶ p⟧ ⟹ p *)
apply (erule_tac P="p ⟶q" in mp)
(* p ⟶ q ⟹ p ⟶ q *)
apply assumption (* *)
text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ej54: "¬q ⟶ ¬p ⟹ p ⟶ q"
apply (rule impI) (* ⟦¬ q ⟶ ¬ p; p⟧ ⟹ q *)
apply (rule notnotD) (* ⟦¬ q ⟶ ¬ p; p⟧ ⟹ ¬ ¬ q *)
apply (erule mt) (* p ⟹ ¬ ¬ p *)
apply (erule notnotI) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}
lemma ej55: "¬(¬p ∧ ¬q) ⟹ p ∨ q"
apply (cut_tac P=p in excluded_middle)
(* ⟦¬ (¬ p ∧ ¬ q); ¬ p ∨ p⟧ ⟹ p ∨ q *)
apply (erule disjE) (* ⟦¬ (¬ p ∧ ¬ q); ¬ p⟧ ⟹ p ∨ q
⟦¬ (¬ p ∧ ¬ q); p⟧ ⟹ p ∨ q *)
apply (cut_tac P=q in excluded_middle)
(* ⟦¬ (¬ p ∧ ¬ q); ¬ p; ¬ q ∨ q⟧ ⟹ p ∨ q
⟦¬ (¬ p ∧ ¬ q); p⟧ ⟹ p ∨ q *)
apply (erule disjE) (* ⟦¬ (¬ p ∧ ¬ q); ¬ p; ¬ q⟧ ⟹ p ∨ q
⟦¬ (¬ p ∧ ¬ q); ¬ p; q⟧ ⟹ p ∨ q
⟦¬ (¬ p ∧ ¬ q); p⟧ ⟹ p ∨ q *)
apply (erule notE) (* ⟦¬ p; ¬ q⟧ ⟹ ¬ p ∧ ¬ q
⟦¬ (¬ p ∧ ¬ q); ¬ p; q⟧ ⟹ p ∨ q
⟦¬ (¬ p ∧ ¬ q); p⟧ ⟹ p ∨ q *)
apply (rule conjI) (* ⟦¬ p; ¬ q⟧ ⟹ ¬ p
⟦¬ p; ¬ q⟧ ⟹ ¬ q
⟦¬ (¬ p ∧ ¬ q); ¬ p; q⟧ ⟹ p ∨ q
⟦¬ (¬ p ∧ ¬ q); p⟧ ⟹ p ∨ q *)
apply assumption+ (* ⟦¬ (¬ p ∧ ¬ q); ¬ p; q⟧ ⟹ p ∨ q
⟦¬ (¬ p ∧ ¬ q); p⟧ ⟹ p ∨ q *)
apply (erule disjI2) (* ⟦¬ (¬ p ∧ ¬ q); p⟧ ⟹ p ∨ q *)
apply (erule disjI1) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
lemma ej56a: "¬(¬p ∨ ¬q) ⟹ p ∧ q"
apply (rule conjI) (* ¬ (¬ p ∨ ¬ q) ⟹ p
¬ (¬ p ∨ ¬ q) ⟹ q *)
apply (rule ccontr) (* ⟦¬ (¬ p ∨ ¬ q); ¬ p⟧ ⟹ False
¬ (¬ p ∨ ¬ q) ⟹ q *)
apply (erule notE) (* ¬ p ⟹ ¬ p ∨ ¬ q
¬ (¬ p ∨ ¬ q) ⟹ q *)
apply (erule disjI1) (* ¬ (¬ p ∨ ¬ q) ⟹ q *)
apply (rule ccontr) (* ⟦¬ (¬ p ∨ ¬ q); ¬ q⟧ ⟹ False *)
apply (erule notE) (* ¬ q ⟹ ¬ p ∨ ¬ q *)
apply (erule disjI2) (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}
lemma ej57: "¬(p ∧ q) ⟹ ¬p ∨ ¬q"
apply (cut_tac P=p in excluded_middle)
(* ⟦¬ (p ∧ q); ¬ p ∨ p⟧ ⟹ ¬ p ∨ ¬ q *)
apply (erule disjE) (* ⟦¬ (p ∧ q); ¬ p⟧ ⟹ ¬ p ∨ ¬ q
⟦¬ (p ∧ q); p⟧ ⟹ ¬ p ∨ ¬ q *)
apply (erule disjI1) (* ⟦¬ (p ∧ q); p⟧ ⟹ ¬ p ∨ ¬ q *)
apply (cut_tac P=q in excluded_middle)
(* ⟦¬ (p ∧ q); p; ¬ q ∨ q⟧ ⟹ ¬ p ∨ ¬ q *)
apply (erule disjE) (* ⟦¬ (p ∧ q); p; ¬ q⟧ ⟹ ¬ p ∨ ¬ q
⟦¬ (p ∧ q); p; q⟧ ⟹ ¬ p ∨ ¬ q *)
apply (erule disjI2) (* ⟦¬ (p ∧ q); p; q⟧ ⟹ ¬ p ∨ ¬ q *)
apply (erule notE) (* ⟦p; q⟧ ⟹ p ∧ q *)
apply (rule conjI) (* ⟦p; q⟧ ⟹ p
⟦p; q⟧ ⟹ q *)
apply assumption+ (* *)
done
text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
lemma ej58a: "(p ⟶ q) ∨ (q ⟶ p)"
apply (cut_tac P=p in excluded_middle)
(* ¬ p ∨ p ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (erule disjE) (* ¬ p ⟹ (p ⟶ q) ∨ (q ⟶ p)
p ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (rule disjI1) (* ¬ p ⟹ p ⟶ q
p ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (rule impI) (* ⟦¬ p; p⟧ ⟹ q
p ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (erule notE) (* p ⟹ p
p ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply assumption (* p ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (rule disjI2) (* p ⟹ q ⟶ p *)
apply (rule impI) (* ⟦p; q⟧ ⟹ p *)
apply assumption (* *)
done
lemma ej58b: "(p ⟶ q) ∨ (q ⟶ p)"
apply (cut_tac P="p ⟶ q" in excluded_middle)
(* ¬ (p ⟶ q) ∨ (p ⟶ q) ⟹
(p ⟶ q) ∨ (q ⟶ p) *)
apply (erule disjE) (* ¬ (p ⟶ q) ⟹ (p ⟶ q) ∨ (q ⟶ p)
p ⟶ q ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (rule disjI2) (* ¬ (p ⟶ q) ⟹ q ⟶ p
p ⟶ q ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (rule impI) (* ⟦¬ (p ⟶ q); q⟧ ⟹ p
p ⟶ q ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (erule notE) (* q ⟹ p ⟶ q
p ⟶ q ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (rule impI) (* ⟦q; p⟧ ⟹ q
p ⟶ q ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply assumption (* p ⟶ q ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (erule disjI1) (* *)
done
lemma ej58c: "(p ⟶ q) ∨ (q ⟶ p)"
apply (cut_tac P="¬(p ⟶ q)" in excluded_middle)
(* ¬ ¬ (p ⟶ q) ∨ ¬ (p ⟶ q) ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (erule disjE) (* ¬ ¬ (p ⟶ q) ⟹ (p ⟶ q) ∨ (q ⟶ p)
¬ (p ⟶ q) ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (drule notnotD) (* p ⟶ q ⟹ (p ⟶ q) ∨ (q ⟶ p)
¬ (p ⟶ q) ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (erule disjI1) (* ¬ (p ⟶ q) ⟹ (p ⟶ q) ∨ (q ⟶ p) *)
apply (rule disjI2) (* ¬ (p ⟶ q) ⟹ q ⟶ p *)
apply (rule impI) (* ⟦¬ (p ⟶ q); q⟧ ⟹ p *)
apply (erule notE) (* q ⟹ p ⟶ q *)
apply (rule impI) (* ⟦q; p⟧ ⟹ q *)
apply assumption (* *)
done
end