Diferencia entre revisiones de «Sol 7»
De Lógica matemática y fundamentos (2018-19)
| (No se muestra una edición intermedia de otro usuario) | |||
| Línea 1: | Línea 1: | ||
| − | <source lang = "isabelle"> | + | <source lang="isabelle"> |
theory R7_sol | theory R7_sol | ||
| + | |||
imports Main | imports Main | ||
begin | begin | ||
| Línea 37: | Línea 38: | ||
--------------------------------------------------------------------- | --------------------------------------------------------------------- | ||
*} | *} | ||
| + | |||
| + | 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 *} | section {* Implicaciones *} | ||
| Línea 45: | Línea 56: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej1a: "⟦p ⟶ q; p⟧ ⟹ q" |
| − | apply (erule mp) | + | apply (erule mp) (* p ⟹ p *) |
| − | apply assumption | + | apply assumption (* *) |
done | done | ||
| + | |||
| + | lemma ej1b: "⟦p ⟶ q; p⟧ ⟹ q" | ||
| + | apply (erule mp, assumption) | ||
| + | done | ||
| + | |||
| + | lemma ej1c: "⟦p ⟶ q; p⟧ ⟹ q" | ||
| + | by (erule mp, assumption) | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 55: | Línea 73: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej2a: "⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r" |
| − | apply (erule mp) | + | apply (erule mp) (* ⟦p ⟶ q; p⟧ ⟹ q *) |
| − | apply assumption | + | apply (erule mp) (* p ⟹ p *) |
| + | apply assumption (* *) | ||
done | 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 {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 66: | Línea 97: | ||
lemma ej3a: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r" | lemma ej3a: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r" | ||
| − | apply ( | + | apply (drule mp) (* ⟦p ⟶ q; p⟧ ⟹ p |
| − | apply assumption | + | ⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *) |
| − | apply ( | + | apply assumption (* ⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *) |
| − | apply assumption | + | apply (drule mp) (* ⟦p; q ⟶ r⟧ ⟹ p |
| − | apply ( | + | ⟦p; q ⟶ r; q⟧ ⟹ r *) |
| − | apply assumption | + | 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 | done | ||
lemma ej3b: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r" | lemma ej3b: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r" | ||
| − | apply ( | + | 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 | done | ||
| + | |||
| + | lemma ej3e: "⟦p ⟶ (q ⟶ r); p ⟶ q; p⟧ ⟹ r" | ||
| + | by (drule mp, assumption+)+ | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 83: | Línea 133: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | + | lemma ej4a: "⟦p ⟶ q; q ⟶ r⟧ ⟹ p ⟶ r" | |
| − | lemma | + | apply (rule impI) (* ⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r *) |
| − | apply (rule impI) | + | apply (erule mp) (* ⟦p ⟶ q; p⟧ ⟹ q *) |
| − | apply (erule mp) | + | apply (erule mp) (* p ⟹ p *) |
| − | apply (erule mp) | + | apply assumption (* *) |
| − | 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 | done | ||
| Línea 96: | Línea 151: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej5a: "p ⟶ (q ⟶ r) ⟹ q ⟶ (p ⟶ r)" |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ⟶ q ⟶ r; q⟧ ⟹ p ⟶ r *) |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ⟶ q ⟶ r; q; p⟧ ⟹ r *) |
| − | apply (erule impE, assumption) | + | apply (erule impE) (* ⟦q; p⟧ ⟹ p |
| − | apply (erule impE, assumption+) | + | ⟦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 | done | ||
| Línea 108: | Línea 186: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej6a: "p ⟶ (q ⟶ r) ⟹ (p ⟶ q) ⟶ (p ⟶ r)" |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ⟶ q ⟶ r; p ⟶ q⟧ ⟹ p ⟶ r *) |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ⟶ q ⟶ r; p ⟶ q; p⟧ ⟹ r *) |
| − | apply (erule impE, assumption) | + | apply (erule impE) (* ⟦p ⟶ q; p⟧ ⟹ p |
| − | apply (erule impE, assumption) | + | ⟦p ⟶ q; p; q ⟶ r⟧ ⟹ r *) |
| − | apply (erule impE, assumption+) | + | 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 | done | ||
| Línea 121: | Línea 219: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej7a: "p ⟹ q ⟶ p" |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p; q⟧ ⟹ p *) |
| − | apply assumption | + | apply assumption (* *) |
| + | done | ||
| + | |||
| + | lemma ej7b: "p ⟹ q ⟶ p" | ||
| + | apply (rule impI, assumption) (* *) | ||
done | done | ||
| Línea 131: | Línea 233: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej8a: "p ⟶ (q ⟶ p)" |
| − | apply (rule impI) | + | apply (rule impI) (* p ⟹ q ⟶ p *) |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p; q⟧ ⟹ p *) |
| − | apply assumption | + | apply assumption (* *) |
done | done | ||
| − | text {* --------------------------------------------------------------- | + | 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 | Ejercicio 9. Demostrar | ||
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r) | p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r) | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej9a: "p ⟶ q ⟹ (q ⟶ r) ⟶ (p ⟶ r)" |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ⟶ q; q ⟶ r⟧ ⟹ p ⟶ r *) |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ⟶ q; q ⟶ r; p⟧ ⟹ r *) |
| − | apply (erule | + | apply (erule mp) (* ⟦p ⟶ q; p⟧ ⟹ q *) |
| − | apply (erule | + | 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 | done | ||
| Línea 154: | Línea 271: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej10a: "p ⟶ (q ⟶ (r ⟶ s)) ⟹ r ⟶ (q ⟶ (p ⟶ s))" |
| − | apply (rule impI)+ | + | apply (rule impI) (* ⟦p ⟶ q ⟶ r ⟶ s; r⟧ ⟹ q ⟶ p ⟶ s *) |
| − | apply ( | + | 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 | done | ||
| Línea 164: | Línea 304: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej11a: "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" |
| − | apply (rule impI)+ | + | apply (rule impI) (* p ⟶ q ⟶ r ⟹ (p ⟶ q) ⟶ p ⟶ r *) |
| − | apply ( | + | 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 | done | ||
| Línea 174: | Línea 328: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej12a: "(p ⟶ q) ⟶ r ⟹ p ⟶ (q ⟶ r)" |
| − | apply (rule impI)+ | + | apply (rule impI) (* ⟦(p ⟶ q) ⟶ r; p⟧ ⟹ q ⟶ r *) |
| − | apply (rule_tac P="p ⟶ q" in mp) | + | apply (rule impI) (* ⟦(p ⟶ q) ⟶ r; p; q⟧ ⟹ r *) |
| − | apply assumption | + | apply (drule mp) (* ⟦p; q⟧ ⟹ p ⟶ q |
| − | apply (rule impI) | + | ⟦p; q; r⟧ ⟹ r *) |
| − | apply assumption | + | 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 | done | ||
| Línea 190: | Línea 374: | ||
lemma ej13: "⟦p; q⟧ ⟹ p ∧ q" | lemma ej13: "⟦p; q⟧ ⟹ p ∧ q" | ||
| − | apply (rule conjI) | + | apply (rule conjI) (* ⟦p; q⟧ ⟹ p |
| − | apply assumption | + | ⟦p; q⟧ ⟹ q *) |
| − | apply assumption | + | apply assumption (* ⟦p; q⟧ ⟹ q *) |
| + | apply assumption (* *) | ||
done | 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 {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 200: | Línea 398: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej14a: "p ∧ q ⟹ p" |
apply (erule conjunct1) | apply (erule conjunct1) | ||
done | done | ||
| + | |||
| + | lemma ej14b: "p ∧ q ⟹ p" | ||
| + | by (erule conjunct1) | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 209: | Línea 410: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej15a: "p ∧ q ⟹ q" |
apply (erule conjunct2) | apply (erule conjunct2) | ||
done | done | ||
| + | |||
| + | lemma ej15b: "p ∧ q ⟹ q" | ||
| + | by (erule conjunct2) | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 218: | Línea 422: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej16a: "p ∧ (q ∧ r) ⟹ (p ∧ q) ∧ r" |
| − | apply (rule conjI) | + | apply (rule conjI) (* p ∧ (q ∧ r) ⟹ p ∧ q |
| − | apply (rule conjI) | + | p ∧ (q ∧ r) ⟹ r *) |
| − | apply (erule conjunct1) | + | apply (rule conjI) (* p ∧ (q ∧ r) ⟹ p |
| − | apply (drule conjunct2) | + | p ∧ (q ∧ r) ⟹ q |
| − | apply (erule conjunct1) | + | p ∧ (q ∧ r) ⟹ r *) |
| − | apply (drule conjunct2) | + | apply (erule conjunct1) (* p ∧ (q ∧ r) ⟹ q |
| − | apply (erule conjunct2) | + | 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 | done | ||
| Línea 233: | Línea 479: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej17a: "(p ∧ q) ∧ r ⟹ p ∧ (q ∧ r)" |
| − | apply (rule conjI) | + | apply (rule conjI) (* (p ∧ q) ∧ r ⟹ p |
| − | apply (drule conjunct1) | + | (p ∧ q) ∧ r ⟹ q ∧ r *) |
| − | apply (erule conjunct1) | + | apply (drule conjunct1) (* p ∧ q ⟹ p |
| − | apply (rule conjI) | + | (p ∧ q) ∧ r ⟹ q ∧ r *) |
| − | apply (drule conjunct1) | + | apply (erule conjunct1) (* (p ∧ q) ∧ r ⟹ q ∧ r *) |
| − | apply (erule conjunct2) | + | apply (rule conjI) (* (p ∧ q) ∧ r ⟹ q |
| − | apply (erule conjunct2) | + | (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 | 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 {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 18. Demostrar | Ejercicio 18. Demostrar | ||
| Línea 249: | Línea 513: | ||
lemma ej18: "p ∧ q ⟹ p ⟶ q" | lemma ej18: "p ∧ q ⟹ p ⟶ q" | ||
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ∧ q; p⟧ ⟹ q *) |
| − | apply (erule conjunct2) | + | apply (erule conjunct2) (* *) |
done | done | ||
| Línea 258: | Línea 522: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej19a: "(p ⟶ q) ∧ (p ⟶ r) ⟹ p ⟶ q ∧ r" |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦(p ⟶ q) ∧ (p ⟶ r); p⟧ ⟹ q ∧ r *) |
| − | apply (rule conjI) | + | apply (rule conjI) (* ⟦(p ⟶ q) ∧ (p ⟶ r); p⟧ ⟹ q |
| − | apply (drule conjunct1) | + | ⟦(p ⟶ q) ∧ (p ⟶ r); p⟧ ⟹ r *) |
| − | apply (erule | + | apply (drule conjunct1) (* ⟦p; p ⟶ q⟧ ⟹ q *) |
| − | apply assumption | + | apply (erule mp) (* p ⟹ p |
| − | + | ⟦(p ⟶ q) ∧ (p ⟶ r); p⟧ ⟹ r *) | |
| − | apply (drule conjunct2) | + | apply assumption (* ⟦(p ⟶ q) ∧ (p ⟶ r); p⟧ ⟹ r *) |
| − | apply (erule | + | apply (drule conjunct2) (* ⟦p; p ⟶ r⟧ ⟹ r *) |
| − | apply assumption | + | apply (erule mp) (* p ⟹ p *) |
| − | + | apply assumption (* *) | |
done | 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 {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 20. Demostrar | Ejercicio 20. Demostrar | ||
| Línea 276: | Línea 572: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej20a: "p ⟶ q ∧ r ⟹ (p ⟶ q) ∧ (p ⟶ r)" |
| − | apply (rule conjI) | + | apply (rule conjI) (* p ⟶ q ∧ r ⟹ p ⟶ q |
| − | apply (rule impI) | + | p ⟶ q ∧ r ⟹ p ⟶ r *) |
| − | apply (erule | + | apply (rule impI) (* ⟦p ⟶ q ∧ r; p⟧ ⟹ q |
| − | apply assumption | + | p ⟶ q ∧ r ⟹ p ⟶ r *) |
| − | apply (erule conjunct1) | + | apply (drule mp) (* p ⟹ p |
| − | apply (rule impI) | + | ⟦p; q ∧ r⟧ ⟹ q |
| − | apply (erule | + | p ⟶ q ∧ r ⟹ p ⟶ r *) |
| − | apply assumption | + | apply assumption (* ⟦p; q ∧ r⟧ ⟹ q |
| − | apply (erule conjunct2) | + | 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 | done | ||
| Línea 293: | Línea 663: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej21a: "p ⟶ (q ⟶ r) ⟹ p ∧ q ⟶ r" |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ⟶ (q ⟶ r); p ∧ q⟧ ⟹ r *) |
| − | apply (erule conjE) | + | apply (frule conjunct1) (* ⟦p ⟶ (q ⟶ r); p ∧ q; p⟧ ⟹ r *) |
| − | apply (erule | + | apply (drule mp) (* ⟦p ∧ q; p⟧ ⟹ p |
| − | apply assumption | + | ⟦p ∧ q; p; q ⟶ r⟧ ⟹ r *) |
| − | apply (erule | + | apply assumption (* ⟦p ∧ q; p; q ⟶ r⟧ ⟹ r *) |
| − | + | apply (drule conjunct2) (* ⟦p; q ⟶ r; q⟧ ⟹ r *) | |
| − | apply assumption | + | 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 | done | ||
| Línea 308: | Línea 705: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej22a: "p ∧ q ⟶ r ⟹ p ⟶ (q ⟶ r)" |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ∧ q ⟶ r; p⟧ ⟹ q ⟶ r *) |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ∧ q ⟶ r; p; q⟧ ⟹ r *) |
| − | apply (erule | + | apply (erule mp) (* ⟦p; q⟧ ⟹ p ∧ q *) |
| − | apply (rule conjI) | + | apply (rule conjI) (* ⟦p; q⟧ ⟹ p |
| − | apply assumption | + | ⟦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 | done | ||
| Línea 321: | Línea 734: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej23a: "(p ⟶ q) ⟶ r ⟹ p ∧ q ⟶ r" |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦(p ⟶ q) ⟶ r; p ∧ q⟧ ⟹ r *) |
| − | apply (erule | + | apply (erule mp) (* p ∧ q ⟹ p ⟶ q *) |
| − | + | apply (rule impI) (* ⟦p ∧ q; p⟧ ⟹ q *) | |
| − | + | apply (erule conjunct2) (* *) | |
| − | |||
done | done | ||
| Línea 334: | Línea 746: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej24a: "p ∧ (q ⟶ r) ⟹ (p ⟶ q) ⟶ r" |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ∧ (q ⟶ r); p ⟶ q⟧ ⟹ r *) |
| − | apply (erule conjE) | + | apply (frule conjunct1) (* ⟦p ∧ (q ⟶ r); p ⟶ q; p⟧ ⟹ r *) |
| − | apply ( | + | apply (drule mp) (* ⟦p ∧ (q ⟶ r); p⟧ ⟹ p |
| − | apply assumption | + | ⟦p ∧ (q ⟶ r); p; q⟧ ⟹ r *) |
| − | apply (erule | + | 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 | done | ||
| Línea 351: | Línea 782: | ||
lemma ej25: "p ⟹ p ∨ q" | lemma ej25: "p ⟹ p ∨ q" | ||
| − | apply (erule disjI1) | + | apply (erule disjI1) (* *) |
done | done | ||
| Línea 360: | Línea 791: | ||
lemma ej26: "q ⟹ p ∨ q" | lemma ej26: "q ⟹ p ∨ q" | ||
| − | apply (erule disjI2) | + | apply (erule disjI2) (* *) |
done | done | ||
| Línea 369: | Línea 800: | ||
lemma ej27: "p ∨ q ⟹ q ∨ p" | lemma ej27: "p ∨ q ⟹ q ∨ p" | ||
| − | apply (erule disjE) | + | apply (erule disjE) (* p ⟹ q ∨ p |
| − | apply (erule disjI2) | + | q ⟹ q ∨ p *) |
| − | apply (erule disjI1) | + | apply (erule disjI2) (* q ⟹ q ∨ p *) |
| + | apply (erule disjI1) (* *) | ||
done | done | ||
| Línea 380: | Línea 812: | ||
lemma ej28: "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r" | lemma ej28: "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r" | ||
| − | apply (rule impI) | + | apply (rule impI) (* ⟦q ⟶ r; p ∨ q⟧ ⟹ p ∨ r *) |
| − | apply (erule disjE) | + | apply (erule disjE) (* ⟦q ⟶ r; p⟧ ⟹ p ∨ r |
| − | apply (erule disjI1) | + | ⟦q ⟶ r; q⟧ ⟹ p ∨ r *) |
| − | apply ( | + | apply (erule disjI1) (* ⟦q ⟶ r; q⟧ ⟹ p ∨ r *) |
| − | apply assumption | + | apply (drule mp) (* q ⟹ q |
| − | apply (erule disjI2) | + | ⟦q; r⟧ ⟹ p ∨ r *) |
| + | apply assumption (* ⟦q; r⟧ ⟹ p ∨ r *) | ||
| + | apply (erule disjI2) (* *) | ||
done | done | ||
| Línea 394: | Línea 828: | ||
lemma ej29: "p ∨ p ⟹ p" | lemma ej29: "p ∨ p ⟹ p" | ||
| − | apply (erule disjE) | + | apply (erule disjE) (* p ⟹ p |
| + | p ⟹ p *) | ||
apply assumption+ | apply assumption+ | ||
done | done | ||
| Línea 404: | Línea 839: | ||
lemma ej30: "p ⟹ p ∨ p" | lemma ej30: "p ⟹ p ∨ p" | ||
| − | apply (erule disjI1) | + | apply (erule disjI1) (* *) |
done | done | ||
| Línea 412: | Línea 847: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej31a: "p ∨ (q ∨ r) ⟹ (p ∨ q) ∨ r" |
| − | apply (erule disjE) | + | apply (erule disjE) (* p ⟹ (p ∨ q) ∨ r |
| − | apply (rule disjI1) | + | q ∨ r ⟹ (p ∨ q) ∨ r *) |
| − | apply (erule disjI1) | + | apply (rule disjI1) (* p ⟹ p ∨ q |
| − | apply (erule disjE) | + | q ∨ r ⟹ (p ∨ q) ∨ r *) |
| − | apply (rule disjI1) | + | apply (erule disjI1) (* q ∨ r ⟹ (p ∨ q) ∨ r *) |
| − | apply (erule disjI2) | + | apply (erule disjE) (* q ⟹ (p ∨ q) ∨ r |
| − | apply (erule disjI2) | + | 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 | done | ||
| Línea 427: | Línea 879: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej32a: "(p ∨ q) ∨ r ⟹ p ∨ (q ∨ r)" |
| − | apply (erule disjE) | + | apply (erule disjE) (* p ∨ q ⟹ p ∨ (q ∨ r) |
| − | apply (erule disjE) | + | r ⟹ p ∨ (q ∨ r) *) |
| − | apply (erule disjI1) | + | apply (erule disjE) (* p ⟹ p ∨ (q ∨ r) |
| − | apply (rule disjI2) | + | q ⟹ p ∨ (q ∨ r) |
| − | apply (erule disjI1) | + | r ⟹ p ∨ (q ∨ r) *) |
| − | apply (rule disjI2) | + | apply (erule disjI1) (* q ⟹ p ∨ (q ∨ r) |
| − | apply (erule disjI2) | + | 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 | done | ||
| Línea 442: | Línea 913: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej33a: "p ∧ (q ∨ r) ⟹ (p ∧ q) ∨ (p ∧ r)" |
| − | apply (erule conjE) | + | apply (erule conjE) (* ⟦p; q ∨ r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *) |
| − | apply (erule disjE) | + | apply (erule disjE) (* ⟦p; q⟧ ⟹ (p ∧ q) ∨ (p ∧ r) |
| − | apply (rule disjI1) | + | ⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *) |
| − | apply (rule conjI) | + | apply (rule disjI1) (* ⟦p; q⟧ ⟹ p ∧ q |
| − | apply assumption | + | ⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *) |
| − | apply assumption | + | apply (rule conjI) (* ⟦p; q⟧ ⟹ p |
| − | apply (rule disjI2) | + | ⟦p; q⟧ ⟹ q |
| − | apply (rule conjI) | + | ⟦p; r⟧ ⟹ (p ∧ q) ∨ (p ∧ r) *) |
| − | apply assumption | + | apply assumption (* ⟦p; q⟧ ⟹ q |
| − | apply assumption | + | ⟦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 | done | ||
| Línea 460: | Línea 950: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej34a: "(p ∧ q) ∨ (p ∧ r) ⟹ p ∧ (q ∨ r)" |
| − | apply (rule conjI) | + | apply (erule disjE) (* p ∧ q ⟹ p ∧ (q ∨ r) |
| − | apply (erule disjE) | + | p ∧ r ⟹ p ∧ (q ∨ r) *) |
| − | apply (erule conjunct1) | + | apply (erule conjE) (* ⟦p; q⟧ ⟹ p ∧ (q ∨ r) |
| − | apply (erule conjunct1) | + | p ∧ r ⟹ p ∧ (q ∨ r) *) |
| − | apply (erule disjE) | + | apply (rule conjI) (* ⟦p; q⟧ ⟹ p |
| − | apply ( | + | ⟦p; q⟧ ⟹ q ∨ r |
| − | apply (rule disjI1) | + | p ∧ r ⟹ p ∧ (q ∨ r) *) |
| − | apply assumption | + | apply assumption (* ⟦p; q⟧ ⟹ q ∨ r |
| − | apply ( | + | p ∧ r ⟹ p ∧ (q ∨ r) *) |
| − | apply (erule disjI2) | + | 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 | done | ||
| Línea 478: | Línea 1011: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej35a: "p ∨ (q ∧ r) ⟹ (p ∨ q) ∧ (p ∨ r)" |
| − | apply (erule disjE) | + | apply (erule disjE) (* p ⟹ (p ∨ q) ∧ (p ∨ r) |
| − | apply (rule conjI) | + | q ∧ r ⟹ (p ∨ q) ∧ (p ∨ r) *) |
| − | apply (erule disjI1) | + | apply (rule conjI) (* p ⟹ p ∨ q |
| − | apply (erule disjI1) | + | p ⟹ p ∨ r |
| − | apply (erule conjE) | + | q ∧ r ⟹ (p ∨ q) ∧ (p ∨ r) *) |
| − | apply (rule conjI) | + | apply (erule disjI1) (* p ⟹ p ∨ r |
| − | apply (erule disjI2) | + | q ∧ r ⟹ (p ∨ q) ∧ (p ∨ r) *) |
| − | apply (erule disjI2) | + | 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 | 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 {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 36. Demostrar | Ejercicio 36. Demostrar | ||
| Línea 494: | Línea 1050: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej36a: "(p ∨ q) ∧ (p ∨ r) ⟹ p ∨ (q ∧ r)" |
| − | apply (erule conjE) | + | apply (erule conjE) (* ⟦p ∨ q; p ∨ r⟧ ⟹ p ∨ (q ∧ r) *) |
| − | apply (erule disjE) | + | apply (erule disjE) (* ⟦p ∨ r; p⟧ ⟹ p ∨ (q ∧ r) |
| − | apply (erule disjI1) | + | ⟦p ∨ r; q⟧ ⟹ p ∨ (q ∧ r) *) |
| − | apply (erule disjE) | + | apply (erule disjI1) (* ⟦p ∨ r; q⟧ ⟹ p ∨ (q ∧ r) *) |
| − | apply (erule disjI1) | + | apply (erule disjE) (* ⟦q; p⟧ ⟹ p ∨ (q ∧ r) |
| − | apply (rule disjI2) | + | ⟦q; r⟧ ⟹ p ∨ (q ∧ r) *) |
| − | apply (rule conjI) | + | apply (erule disjI1) (* ⟦q; r⟧ ⟹ p ∨ (q ∧ r) *) |
| − | apply assumption | + | apply (rule disjI2) (* ⟦q; r⟧ ⟹ q ∧ r *) |
| + | apply (rule conjI) (* ⟦q; r⟧ ⟹ q | ||
| + | ⟦q; r⟧ ⟹ r *) | ||
| + | apply assumption (* ⟦q; r⟧ ⟹ r *) | ||
| + | apply assumption (* *) | ||
done | done | ||
| Línea 510: | Línea 1070: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej37a: "(p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟶ r" |
| − | apply (rule impI) | + | apply (rule impI) (* ⟦(p ⟶ r) ∧ (q ⟶ r); p ∨ q⟧ ⟹ r *) |
| − | apply (erule conjE) | + | apply (erule conjE) (* ⟦p ∨ q; p ⟶ r; q ⟶ r⟧ ⟹ r *) |
| − | apply (erule disjE) | + | apply (erule disjE) (* ⟦p ⟶ r; q ⟶ r; p⟧ ⟹ r |
| − | apply (erule | + | ⟦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 | done | ||
| Línea 522: | Línea 1096: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej38a: "p ∨ q ⟶ r ⟹ (p ⟶ r) ∧ (q ⟶ r)" |
| − | apply (rule conjI) | + | apply (rule conjI) (* p ∨ q ⟶ r ⟹ p ⟶ r |
| − | apply (rule impI) | + | p ∨ q ⟶ r ⟹ q ⟶ r *) |
| − | apply (erule | + | apply (rule impI) (* ⟦p ∨ q ⟶ r; p⟧ ⟹ r |
| − | apply (erule disjI1) | + | p ∨ q ⟶ r ⟹ q ⟶ r *) |
| − | + | apply (erule mp) (* p ⟹ p ∨ q | |
| − | apply (rule impI) | + | p ∨ q ⟶ r ⟹ q ⟶ r *) |
| − | apply (erule | + | apply (erule disjI1) (* p ∨ q ⟶ r ⟹ q ⟶ r *) |
| − | apply (erule disjI2) | + | apply (rule impI) (* ⟦p ∨ q ⟶ r; q⟧ ⟹ r *) |
| − | + | apply (erule mp) (* q ⟹ p ∨ q *) | |
| + | apply (erule disjI2) (* *) | ||
done | done | ||
| Línea 542: | Línea 1117: | ||
lemma ej39: "p ⟹ ¬¬p" | lemma ej39: "p ⟹ ¬¬p" | ||
| − | apply (rule notI) | + | apply (rule notI) (* ⟦p; ¬ p⟧ ⟹ False *) |
| − | apply (erule notE) | + | apply (erule notE) (* p ⟹ p *) |
| − | apply assumption | + | apply assumption (* *) |
done | done | ||
| Línea 553: | Línea 1128: | ||
lemma ej40: "¬p ⟹ p ⟶ q" | lemma ej40: "¬p ⟹ p ⟶ q" | ||
| − | apply (rule impI) | + | apply (rule impI) (* ⟦¬ p; p⟧ ⟹ q *) |
| − | apply (erule notE) | + | apply (erule notE) (* p ⟹ p *) |
| − | apply assumption | + | apply assumption (* *) |
done | done | ||
| Línea 564: | Línea 1139: | ||
lemma ej41: "p ⟶ q ⟹ ¬q ⟶ ¬p" | lemma ej41: "p ⟶ q ⟹ ¬q ⟶ ¬p" | ||
| − | apply (rule impI) | + | apply (rule impI) (* ⟦p ⟶ q; ¬ q⟧ ⟹ ¬ p *) |
| − | apply (rule notI) | + | apply (rule notI) (* ⟦p ⟶ q; ¬ q; p⟧ ⟹ False *) |
| − | apply ( | + | apply (drule mp) (* ⟦¬ q; p⟧ ⟹ p |
| − | apply assumption | + | ⟦¬ q; p; q⟧ ⟹ False *) |
| − | apply (erule notE) | + | apply assumption (* ⟦¬ q; p; q⟧ ⟹ False *) |
| − | apply assumption | + | apply (erule notE) (* ⟦p; q⟧ ⟹ q *) |
| + | apply assumption (* *) | ||
done | done | ||
| Línea 578: | Línea 1154: | ||
lemma ej42: "⟦p ∨ q; ¬q⟧ ⟹ p" | lemma ej42: "⟦p ∨ q; ¬q⟧ ⟹ p" | ||
| − | apply (erule disjE) | + | apply (erule disjE) (* ⟦¬ q; p⟧ ⟹ p |
| − | apply assumption | + | ⟦¬ q; q⟧ ⟹ p *) |
| − | apply (erule notE) | + | apply assumption (* ⟦¬ q; q⟧ ⟹ p *) |
| − | apply assumption | + | apply (erule notE) (* q ⟹ q *) |
| + | apply assumption (* *) | ||
done | done | ||
| Línea 590: | Línea 1167: | ||
lemma ej43: "⟦p ∨ q; ¬p⟧ ⟹ q" | lemma ej43: "⟦p ∨ q; ¬p⟧ ⟹ q" | ||
| − | apply (erule disjE) | + | apply (erule disjE) (* ⟦¬ p; p⟧ ⟹ q |
| − | apply (erule notE) | + | ⟦¬ p; q⟧ ⟹ q *) |
| − | apply assumption | + | apply (erule notE) (* p ⟹ p |
| − | apply assumption | + | ⟦¬ p; q⟧ ⟹ q *) |
| + | apply assumption (* ⟦¬ p; q⟧ ⟹ q *) | ||
| + | apply assumption (* ⟦¬ p; q⟧ ⟹ q *) | ||
done | done | ||
| Línea 601: | Línea 1180: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| + | 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)" | lemma ej44: "p ∨ q ⟹ ¬(¬p ∧ ¬q)" | ||
| − | apply (rule notI) | + | apply (rule notI) (* ⟦p ∨ q; ¬ p ∧ ¬ q⟧ ⟹ False *) |
| − | apply (erule conjE) | + | apply (erule conjE) (* ⟦p ∨ q; ¬ p; ¬ q⟧ ⟹ False *) |
| − | apply (erule disjE) | + | apply (erule disjE) (* ⟦¬ p; ¬ q; p⟧ ⟹ False |
| − | apply (erule notE, assumption)+ | + | ⟦¬ p; ¬ q; q⟧ ⟹ False *) |
| − | done | + | apply (erule notE, assumption)+ (* *) |
| + | done | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 613: | Línea 1205: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej45a: "p ∧ q ⟹ ¬(¬p ∨ ¬q)" |
| − | apply (rule notI) | + | apply (rule notI) (* ⟦p ∧ q; ¬ p ∨ ¬ q⟧ ⟹ False *) |
| − | apply (erule conjE) | + | apply (erule conjE) (* ⟦¬ p ∨ ¬ q; p; q⟧ ⟹ False *) |
| − | apply (erule disjE) | + | apply (erule disjE) (* ⟦p; q; ¬ p⟧ ⟹ False |
| − | apply (erule notE, assumption)+ | + | ⟦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 | done | ||
| Línea 625: | Línea 1242: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej46b: "¬(p ∨ q) ⟹ ¬p ∧ ¬q" |
| − | apply (rule conjI) | + | apply (rule conjI) (* ¬ (p ∨ q) ⟹ ¬ p |
| − | apply (rule notI) | + | ¬ (p ∨ q) ⟹ ¬ q *) |
| − | apply (erule notE) | + | apply (rule notI) (* ⟦¬ (p ∨ q); p⟧ ⟹ False |
| − | apply (erule disjI1) | + | ¬ (p ∨ q) ⟹ ¬ q *) |
| − | apply (rule notI) | + | apply (erule notE) (* p ⟹ p ∨ q |
| − | apply (erule notE) | + | ¬ (p ∨ q) ⟹ ¬ q *) |
| − | apply (erule disjI2) | + | 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 | done | ||
| + | |||
| + | lemma ej46c: "¬(p ∨ q) ⟹ ¬p ∧ ¬q" | ||
| + | by (rule conjI, | ||
| + | (rule notI, | ||
| + | erule notE, | ||
| + | (erule disjI1 | | ||
| + | erule disjI2))+) | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
| Línea 639: | Línea 1275: | ||
¬p ∧ ¬q ⊢ ¬(p ∨ q) | ¬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)" | lemma ej47: "¬p ∧ ¬q ⟹ ¬(p ∨ q)" | ||
| − | apply (rule notI) | + | apply (rule notI) (* ⟦¬ p ∧ ¬ q; p ∨ q⟧ ⟹ False *) |
| − | apply (erule conjE) | + | apply (erule conjE) (* ⟦p ∨ q; ¬ p; ¬ q⟧ ⟹ False *) |
apply (erule disjE) | apply (erule disjE) | ||
| − | apply (erule notE, assumption)+ | + | apply (erule notE, |
| + | assumption)+ (* *) | ||
done | done | ||
| Línea 652: | Línea 1311: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej48a: "¬p ∨ ¬q ⟹ ¬(p ∧ q)" |
| − | apply (rule notI) | + | apply (rule notI) (* ⟦¬ p ∨ ¬ q; p ∧ q⟧ ⟹ False *) |
| − | apply (erule conjE) | + | apply (erule disjE) (* ⟦p ∧ q; ¬ p⟧ ⟹ False |
| − | apply (erule disjE) | + | ⟦p ∧ q; ¬ q⟧ ⟹ False *) |
| − | apply (erule notE, assumption)+ | + | 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 | done | ||
| Línea 665: | Línea 1340: | ||
lemma ej49: "¬(p ∧ ¬p)" | lemma ej49: "¬(p ∧ ¬p)" | ||
| − | apply (rule notI) | + | apply (rule notI) (* p ∧ ¬ p ⟹ False *) |
| − | apply (erule conjE) | + | apply (erule conjE) (* ⟦p; ¬ p⟧ ⟹ False *) |
| − | apply (erule notE) | + | apply (erule notE) (* ⟦p; ¬ p⟧ ⟹ False *) |
| − | apply assumption | + | apply assumption (* *) |
done | done | ||
| Línea 677: | Línea 1352: | ||
lemma ej50: "p ∧ ¬p ⟹ q" | lemma ej50: "p ∧ ¬p ⟹ q" | ||
| − | apply (erule conjE) | + | apply (erule conjE) (* ⟦p; ¬ p⟧ ⟹ q *) |
| − | apply (erule notE) | + | apply (erule notE) (* p ⟹ p *) |
| − | apply assumption | + | apply assumption (* *) |
done | done | ||
| Línea 688: | Línea 1363: | ||
lemma ej51: "¬¬p ⟹ p" | lemma ej51: "¬¬p ⟹ p" | ||
| − | apply (erule notnotD) | + | apply (erule notnotD) (* *) |
done | done | ||
| Línea 697: | Línea 1372: | ||
lemma ej52: "p ∨ ¬p" | lemma ej52: "p ∨ ¬p" | ||
| − | apply (cut_tac P="¬p" in excluded_middle) | + | apply (cut_tac P="¬p" in excluded_middle) (* ¬¬p ∨ ¬p ⟹ p ∨ ¬p*) |
| − | apply (erule disjE) | + | apply (erule disjE) (* ¬ ¬ p ⟹ p ∨ ¬ p |
| − | apply (rule disjI1) | + | ¬ p ⟹ p ∨ ¬ p *) |
| − | apply (erule notnotD) | + | apply (rule disjI1) (* ¬ ¬ p ⟹ p |
| − | apply (erule disjI2) | + | ¬ p ⟹ p ∨ ¬ p *) |
| + | apply (erule notnotD) (* ¬ p ⟹ p ∨ ¬ p *) | ||
| + | apply (erule disjI2) (* *) | ||
done | done | ||
| Línea 710: | Línea 1387: | ||
lemma ej53: "((p ⟶ q) ⟶ p) ⟶ p" | lemma ej53: "((p ⟶ q) ⟶ p) ⟶ p" | ||
| − | |||
| − | |||
apply (cut_tac P="p ⟶ q" in excluded_middle) | apply (cut_tac P="p ⟶ q" in excluded_middle) | ||
| − | apply (erule disjE) | + | (* ¬ (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) | apply (erule_tac P="p ⟶ q" in notE) | ||
| − | apply (rule impI) | + | (* ⟦(p ⟶ q) ⟶ p; ¬ p⟧ ⟹ p ⟶ q |
| − | apply (erule notE) | + | p ⟶ q ⟹ ((p ⟶ q) ⟶ p) ⟶ p *) |
| − | apply assumption | + | apply (rule impI) (* ⟦(p ⟶ q) ⟶ p; ¬ p; p⟧ ⟹ q |
| − | apply ( | + | p ⟶ q ⟹ ((p ⟶ q) ⟶ p) ⟶ p *) |
| − | + | apply (erule notE) (* ⟦(p ⟶ q) ⟶ p; p⟧ ⟹ p | |
| − | apply ( | + | p ⟶ q ⟹ ((p ⟶ q) ⟶ p) ⟶ p *) |
| − | apply assumption | + | 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 {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 54. Demostrar | Ejercicio 54. Demostrar | ||
| Línea 730: | Línea 1415: | ||
lemma ej54: "¬q ⟶ ¬p ⟹ p ⟶ q" | lemma ej54: "¬q ⟶ ¬p ⟹ p ⟶ q" | ||
| − | apply (rule impI) | + | apply (rule impI) (* ⟦¬ q ⟶ ¬ p; p⟧ ⟹ q *) |
| − | apply (rule | + | apply (rule notnotD) (* ⟦¬ q ⟶ ¬ p; p⟧ ⟹ ¬ ¬ q *) |
| − | apply (erule | + | apply (erule mt) (* p ⟹ ¬ ¬ p *) |
| − | + | apply (erule notnotI) (* *) | |
| − | apply (erule | ||
| − | |||
done | done | ||
| − | + | ||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Ejercicio 55. Demostrar | Ejercicio 55. Demostrar | ||
| Línea 745: | Línea 1428: | ||
lemma ej55: "¬(¬p ∧ ¬q) ⟹ p ∨ q" | lemma ej55: "¬(¬p ∧ ¬q) ⟹ p ∨ q" | ||
apply (cut_tac P=p in excluded_middle) | apply (cut_tac P=p in excluded_middle) | ||
| − | apply (erule disjE) | + | (* ⟦¬ (¬ p ∧ ¬ q); ¬ p ∨ p⟧ ⟹ p ∨ q *) |
| − | + | apply (erule disjE) (* ⟦¬ (¬ p ∧ ¬ q); ¬ p⟧ ⟹ p ∨ q | |
| − | apply (erule disjE) | + | ⟦¬ (¬ p ∧ ¬ q); p⟧ ⟹ p ∨ q *) |
| − | apply (erule notE) | + | apply (cut_tac P=q in excluded_middle) |
| − | apply (rule conjI) | + | (* ⟦¬ (¬ p ∧ ¬ q); ¬ p; ¬ q ∨ q⟧ ⟹ p ∨ q |
| − | apply assumption+ | + | ⟦¬ (¬ p ∧ ¬ q); p⟧ ⟹ p ∨ q *) |
| − | apply (erule disjI2) | + | apply (erule disjE) (* ⟦¬ (¬ p ∧ ¬ q); ¬ p; ¬ q⟧ ⟹ p ∨ q |
| − | apply (erule disjI1) | + | ⟦¬ (¬ 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 | done | ||
| Línea 760: | Línea 1455: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej56a: "¬(¬p ∨ ¬q) ⟹ p ∧ q" |
| − | apply (rule conjI) | + | apply (rule conjI) (* ¬ (¬ p ∨ ¬ q) ⟹ p |
| − | apply (rule ccontr) | + | ¬ (¬ p ∨ ¬ q) ⟹ q *) |
| − | apply (erule notE) | + | apply (rule ccontr) (* ⟦¬ (¬ p ∨ ¬ q); ¬ p⟧ ⟹ False |
| − | apply (erule disjI1) | + | ¬ (¬ p ∨ ¬ q) ⟹ q *) |
| − | apply (rule ccontr) | + | apply (erule notE) (* ¬ p ⟹ ¬ p ∨ ¬ q |
| − | apply (erule notE) | + | ¬ (¬ p ∨ ¬ q) ⟹ q *) |
| − | apply (erule disjI2) | + | apply (erule disjI1) (* ¬ (¬ p ∨ ¬ q) ⟹ q *) |
| + | apply (rule ccontr) (* ⟦¬ (¬ p ∨ ¬ q); ¬ q⟧ ⟹ False *) | ||
| + | apply (erule notE) (* ¬ q ⟹ ¬ p ∨ ¬ q *) | ||
| + | apply (erule disjI2) (* *) | ||
done | done | ||
| Línea 777: | Línea 1475: | ||
lemma ej57: "¬(p ∧ q) ⟹ ¬p ∨ ¬q" | lemma ej57: "¬(p ∧ q) ⟹ ¬p ∨ ¬q" | ||
apply (cut_tac P=p in excluded_middle) | apply (cut_tac P=p in excluded_middle) | ||
| − | apply (erule disjE) | + | (* ⟦¬ (p ∧ q); ¬ p ∨ p⟧ ⟹ ¬ p ∨ ¬ q *) |
| − | apply (erule disjI1) | + | 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) | apply (cut_tac P=q in excluded_middle) | ||
| − | apply (erule disjE) | + | (* ⟦¬ (p ∧ q); p; ¬ q ∨ q⟧ ⟹ ¬ p ∨ ¬ q *) |
| − | apply (erule disjI2) | + | apply (erule disjE) (* ⟦¬ (p ∧ q); p; ¬ q⟧ ⟹ ¬ p ∨ ¬ q |
| − | apply (erule notE) | + | ⟦¬ (p ∧ q); p; q⟧ ⟹ ¬ p ∨ ¬ q *) |
| − | apply (rule conjI) | + | apply (erule disjI2) (* ⟦¬ (p ∧ q); p; q⟧ ⟹ ¬ p ∨ ¬ q *) |
| − | apply assumption+ | + | apply (erule notE) (* ⟦p; q⟧ ⟹ p ∧ q *) |
| + | apply (rule conjI) (* ⟦p; q⟧ ⟹ p | ||
| + | ⟦p; q⟧ ⟹ q *) | ||
| + | apply assumption+ (* *) | ||
done | done | ||
| Línea 792: | Línea 1495: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
| − | lemma | + | lemma ej58a: "(p ⟶ q) ∨ (q ⟶ p)" |
apply (cut_tac P=p in excluded_middle) | apply (cut_tac P=p in excluded_middle) | ||
| − | apply (erule disjE) | + | (* ¬ p ∨ p ⟹ (p ⟶ q) ∨ (q ⟶ p) *) |
| − | apply (rule disjI1) | + | apply (erule disjE) (* ¬ p ⟹ (p ⟶ q) ∨ (q ⟶ p) |
| − | apply (rule impI) | + | p ⟹ (p ⟶ q) ∨ (q ⟶ p) *) |
| − | apply (erule notE) | + | apply (rule disjI1) (* ¬ p ⟹ p ⟶ q |
| − | apply assumption | + | p ⟹ (p ⟶ q) ∨ (q ⟶ p) *) |
| − | apply (rule disjI2) | + | apply (rule impI) (* ⟦¬ p; p⟧ ⟹ q |
| − | apply (rule impI) | + | p ⟹ (p ⟶ q) ∨ (q ⟶ p) *) |
| − | apply assumption | + | 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 | done | ||
end | end | ||
| − | |||
</source> | </source> | ||
Revisión actual del 14:03 20 abr 2019
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