Relación 6
De Razonamiento automático (2018-19)
Revisión del 21:39 15 ene 2019 de Benber (discusión | contribuciones)
chapter {* R6: Deducción natural proposicional *}
theory R6_Deduccion_natural_proposicional
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta relación es demostrar cada uno de los ejercicios
usando sólo las reglas básicas de deducción natural de la lógica
proposicional (sin usar el método auto).
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
· notnotD: ¬¬ P ⟹ P
· notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ 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
------------------------------------------------------------------ *}
(* pabalagon josgomrom4 *)
lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show "q" using 1 2 by (rule mp)
qed
(* benber *)
lemma ejercicio_1_1:
assumes "p ⟶ q"
"p"
shows "q"
using assms by (rule mp)
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}
(* pabalagon josgomrom4 *)
lemma ejercicio_2:
assumes 1: "p ⟶ q" and
2: "q ⟶ r" and
3: "p"
shows "r"
proof -
have 4: "q" using 1 3 by (rule mp)
show "r" using 2 4 by (rule mp)
qed
(* benber *)
lemma ejercicio_2_1:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
proof -
have "q" using `p ⟶ q` `p` by (rule mp)
with `q ⟶ r` show "r" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}
(* pabalagon josgomrom4 *)
lemma ejercicio_3:
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p ⟶ q" and
3: "p"
shows "r"
proof -
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show "r" using 4 5 by (rule mp)
qed
(* benber *)
lemma ejercicio_3_1:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
proof -
have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` by (rule mp)
moreover have "q" using `p ⟶ q` `p` by (rule mp)
ultimately show "r" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}
(* pabalagon josgomrom4 *)
lemma ejercicio_4:
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"
proof -
{ assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "r" using 2 4 by (rule mp)}
thus "p ⟶ r" by (rule impI)
qed
(* benber *)
lemma ejercicio_4_1:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
proof
assume p
with `p ⟶ q` have "q" by (rule mp)
with `q ⟶ r` show "r" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon josgomrom4 *)
lemma ejercicio_5:
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
show "r" using 4 2 by (rule mp)
qed
qed
(* benber *)
lemma ejercicio_5_1:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof
assume "q"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
thus "r" using `q` by (rule mp)
qed
qed
(* pabalagon *)
lemma ejercicio_5_2:
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof -
{ assume 2: "q"
{ assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "r" using 4 2 by (rule mp)}
hence "p ⟶ r" by (rule impI)
}
thus "q ⟶ (p ⟶ r)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_6:
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show "r" using 4 5 by (rule mp)
qed
qed
(* benber *)
lemma ejercicio_6_1:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume "p ⟶ q"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
moreover from `p ⟶ q` `p` have "q" by (rule mp)
ultimately show "r" by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_7:
assumes 1: "p"
shows "q ⟶ p"
proof (rule impI)
assume 2: "q"
show "p" using 1 by this
qed
(* benber *)
lemma ejercicio_7_1:
assumes "p"
shows "q ⟶ p"
proof
show "p" using `p` .
qed
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
proof (rule impI)
assume 1: "p"
show "q ⟶ p"
proof (rule impI)
assume 2: "q"
show "p" using 1 by this
qed
qed
(* benber *)
lemma ejercicio_8_1:
"p ⟶ (q ⟶ p)"
using ejercicio_7_1 by (rule impI)
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_9:
assumes 1: "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "q ⟶ r"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
show "r" using 2 4 by (rule mp)
qed
qed
(* benber *)
lemma ejercicio_9_1:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof
assume "q ⟶ r"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ q` have "q" by (rule mp)
with `q ⟶ r` show "r" by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_10:
assumes 1: "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof (rule impI)
assume 2: "r"
show "q ⟶ (p ⟶ s)"
proof (rule impI)
assume 3: "q"
show "p ⟶ s"
proof (rule impI)
assume 4: "p"
have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
have 6: "r ⟶ s" using 5 3 by (rule mp)
show "s" using 6 2 by (rule mp)
qed
qed
qed
(* benber *)
lemma ejercicio_10_1:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof
assume "r"
show "q ⟶ (p ⟶ s)"
proof
assume "q"
show "p ⟶ s"
proof
assume "p"
with `p ⟶ (q ⟶ (r ⟶ s))`
have "q ⟶ (r ⟶ s)" by (rule mp)
hence "r ⟶ s" using `q` by (rule mp)
thus "s" using `r` by (rule mp)
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)" using 1 ejercicio_6 by simp
qed
(* pabalagon *)
lemma ejercicio_11_2:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show "r" using 4 5 by (rule mp)
qed
qed
qed
(* benber *)
lemma ejercicio_11_1:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume "p ⟶ q"
show "p ⟶ r"
proof
assume p
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
moreover have "q" using `p ⟶ q` `p` by (rule mp)
ultimately show r by (rule mp)
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_12:
assumes 1: "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume 2: "p"
show "q ⟶ r"
proof (rule impI)
assume 3: "q"
have 4: "p ⟶ q"
proof (rule impI)
assume 5: "p"
show "q" using 3 by this
qed
show "r" using 1 4 by (rule mp)
qed
qed
(* benber *)
lemma ejercicio_12_1:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q ⟶ r"
proof
assume "q"
hence "p ⟶ q" by (rule impI)
with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
qed
qed
section {* Conjunciones *}
text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"
using assms(1, 2) by (rule conjI)
(* benber *)
lemma ejercicio_13_1:
assumes "p"
"q"
shows "p ∧ q"
using assms by (rule conjI)
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
using assms(1) by (rule conjunct1)
(* benber *)
lemma ejercicio_14_1:
assumes "p ∧ q"
shows "p"
using assms by (rule conjunct1)
text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
using assms(1) by (rule conjunct2)
(* benber *)
lemma ejercicio_15_1:
assumes "p ∧ q"
shows "q"
using assms by (rule conjunct2)
text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof -
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "q ∧ r" using assms(1) by (rule conjunct2)
have 3: "q" using 2 by (rule conjunct1)
have 4: "r" using 2 by (rule conjunct2)
have 5: "p ∧ q" using 1 3 by (rule conjI)
show "(p ∧ q) ∧ r" using 5 4 by (rule conjI)
qed
(* benber *)
lemma ejercicio_16_1:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof - (* TODO? *)
have "q ∧ r" using assms by (rule conjunct2)
have "p" using assms by (rule conjunct1)
moreover have "q" using `q ∧ r` by (rule conjunct1)
ultimately have "p ∧ q" by (rule conjI)
moreover have "r" using `q ∧ r` by (rule conjunct2)
ultimately show "(p ∧ q) ∧ r" by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_17:
assumes 1: "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof -
have 2: "r" using 1 by (rule conjunct2)
have 3: "p ∧ q" using 1 by (rule conjunct1)
have 4: "p" using 3 by (rule conjunct1)
have 5: "q" using 3 by (rule conjunct2)
have 6: "q ∧ r" using 5 2 by (rule conjI)
show ?thesis using 4 6 by (rule conjI)
qed
(* benber *)
lemma ejercicio_17_1:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof -
have "p ∧ q" using assms by (rule conjunct1)
have "p" using `p ∧ q` by (rule conjunct1)
moreover have "q ∧ r"
proof (rule conjI)
show "q" using `p ∧ q` by (rule conjunct2)
next
show "r" using assms by (rule conjunct2)
qed
ultimately show ?thesis by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using assms(1) by (rule conjunct2)
qed
(* benber *)
lemma ejercicio_18_1:
assumes "p ∧ q"
shows "p ⟶ q"
proof
show "q" using assms by (rule conjunct2)
qed
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_19:
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof (rule impI)
assume 2: "p"
have 3: "p ⟶ q" using 1 by (rule conjunct1)
have 4: "p ⟶ r" using 1 by (rule conjunct2)
have 5: "q" using 3 2 by (rule mp)
have 6: "r" using 4 2 by (rule mp)
show "q ∧ r" using 5 6 by (rule conjI)
qed
(* benber *)
lemma ejercicio_19_1:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof
assume p
show "q ∧ r"
proof
have "p ⟶ q" using assms by (rule conjunct1)
thus "q" using `p` by (rule mp)
next
have "p ⟶ r" using assms by (rule conjunct2)
thus "r" using `p` by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_20:
assumes 1: "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
show "p ⟶ q"
proof (rule impI)
assume 2: "p"
have 3: "q ∧ r" using 1 2 by (rule mp)
show 4: "q" using 3 by (rule conjunct1)
qed
show "p ⟶ r"
proof (rule impI)
assume 2: "p"
have 3: "q ∧ r" using 1 2 by (rule mp)
show 4: "r" using 3 by (rule conjunct2)
qed
qed
(* benber *)
lemma ejercicio_20_1:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof
show "p ⟶ q"
proof
assume "p"
with assms have "q ∧ r" by (rule mp)
thus "q" by (rule conjunct1)
qed
next
show "p ⟶ r"
proof
assume "p"
with assms have "q ∧ r" by (rule mp)
thus "r" by (rule conjunct2)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_21:
assumes 1: "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume 2: "p ∧ q"
have 3: "p" using 2 by (rule conjunct1)
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 by (rule conjunct2)
show "r" using 4 5 by (rule mp)
qed
(* benber *)
lemma ejercicio_21_1:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
hence "p" by (rule conjunct1)
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
moreover from `p ∧ q` have "q" by (rule conjunct2)
ultimately show "r" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_22:
assumes 1: "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume 2: "p"
show "q ⟶ r"
proof (rule impI)
assume 3: "q"
have 4: "p ∧ q" using 2 3 by (rule conjI)
show "r" using 1 4 by (rule mp)
qed
qed
(* benber *)
lemma ejercicio_22_1:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q ⟶ r"
proof
assume "q"
with `p` have "p ∧ q" by (rule conjI)
with `p ∧ q ⟶ r` show "r" by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_23:
assumes 1: "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume 2: "p ∧ q"
have 3: "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using 2 by (rule conjunct2)
qed
show "r" using 1 3 by (rule mp)
qed
(* benber *)
lemma ejercicio_23_1:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
hence "q" by (rule conjunct2)
hence "p ⟶ q" by (rule impI)
with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_24:
assumes 1: "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof (rule impI)
assume 2: "p ⟶ q"
have 3: "p" using 1 by (rule conjunct1)
have 4: "q ⟶ r" using 1 by (rule conjunct2)
have 5: "q" using 2 3 by (rule mp)
show 6: "r" using 4 5 by (rule mp)
qed
(* benber *)
lemma ejercicio_24_1:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
have "q ⟶ r" using assms by (rule conjunct2)
assume "p ⟶ q"
moreover have "p" using assms by (rule conjunct1)
ultimately have "q" by (rule mp)
with `q ⟶ r` show r by (rule mp)
qed
section {* Disyunciones *}
text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}
lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}
lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}
lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}
lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}
lemma ejercicio_29:
assumes "p ∨ p"
shows "p"
oops
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}
lemma ejercicio_31:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}
lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}
lemma ejercicio_33:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}
lemma ejercicio_34:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}
lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}
lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
oops
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}
lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
oops
text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}
lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
oops
section {* Negaciones *}
text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}
lemma ejercicio_39:
assumes "p"
shows "¬¬p"
oops
text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}
lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
oops
text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}
lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
oops
text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}
lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
oops
text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}
lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
oops
text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}
lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
oops
text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}
lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
oops
text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}
lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
oops
text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}
lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
oops
text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}
lemma ejercicio_49:
"¬(p ∧ ¬p)"
oops
text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}
lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
oops
text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}
lemma ejercicio_51:
assumes "¬¬p"
shows "p"
oops
text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}
lemma ejercicio_52:
"p ∨ ¬p"
oops
text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}
lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
oops
text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}
lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
oops
text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}
lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
oops
text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
oops
end