Relación 3
De Lógica matemática y fundamentos (2012-13)
Revisión del 14:22 14 mar 2013 de Raumonpaj (discusión | contribuciones)
header {* R3: Deducción natural proposicional *}
theory R3
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
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_1a:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show 3: "q" using 1 2 by (rule mp)
qed
-- "Isabel Duarte"
lemma ejercicio_1b:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms(1,2) by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_2a:
assumes 1:"p ⟶ q" and
2:"q ⟶ r" and
3:"p"
shows "r"
proof -
have 4: "q" using 1 3 by (rule mp)
show 5: "r" using 2 4 by (rule mp)
qed
-- "Isabel Duarte"
lemma ejercicio_2b:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
proof -
have "q" using assms(1,3) ..
with `q ⟶ r` show "r" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_3a:
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 6: "r" using 4 5 by (rule mp)
qed
-- "Isabel Duarte"
lemma ejercicio_3b:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
proof -
have "q ⟶ r" using assms(1,3) ..
have "q" using assms(2,3) ..
with `q ⟶ r` show "r" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_4a:
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
lemma ejercicio_4d:
assumes "p ⟶ q" and
"q ⟶ r"
shows "p ⟶ r"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "Isabel Duarte"
lemma ejercicio_5a:
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof -
{assume 3: "q"
{assume 4: "p"
have "q ⟶ r" using 1 4 ..
hence 5: "r" using 3 ..}
hence 6: "p ⟶ r" by (rule impI)}
thus "q ⟶ (p ⟶ r)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "José Mª Contreras"
lemma ejercicio_6a:
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof -
{assume 2: "p ⟶ q"
{assume 3: "p"
have 4: "q ⟶ r" using 1 3 ..
have 5: "q" using 2 3 ..
have "r" using 4 5 ..}
hence "p ⟶ r" by (rule impI)}
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
proof -
{assume 1: "q"}
show "q⟶ p" using assms(1) by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
proof -
{assume 1: "p"
hence 2: "q ⟶ p" by (rule impI)}
thus "p ⟶q⟶p" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- Carmen Martinez Navarro, Erlinda Menendez Perez
lemma ejercicio_9:
assumes 1: "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof-
{assume 2: "q ⟶ r"
{assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "r" using 2 4 by (rule mp)}
hence 6: "p ⟶ r" by (rule impI)}
thus "(q ⟶ r) ⟶ (p ⟶ r)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_10:
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 assms have "q⟶ r⟶ s" ..
hence "r⟶ s" using `q` ..
thus "s" using `r`..
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_11a:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
lemma ejercicio_11:
shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume 1: "p ⟶ (q ⟶ r)"
show 2: "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume 3: "p⟶ q"
show 4: "p⟶ r"
proof
assume 5: "p"
have 6: "q" using 3 5 by (rule mp)
have 7:"q⟶ r" using 1 5 by (rule mp)
show 8: "r" using 7 6 ..
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_12a:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof -
have 1: "(p⟶ q)⟶ r" using assms by this
{assume 2: "p"
{assume 3: "q"
{assume 4: "p"
have 5: "q" using 3 by this}
hence 6: "p⟶ q" ..
have 7: "r" using assms 6 ..}
hence 8: "q⟶ r" ..}
thus 9: "p⟶ (q⟶ r)" ..
qed
section {* Conjunciones *}
text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_13:
assumes 1:"p" and
2:"q"
shows "p ∧ q"
proof -
show "p ∧ q" using 1 2 by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
proof -
show "p" using assms by (rule conjunct1)
qed
text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
proof -
show "q" using assms by (rule conjunct2)
qed
text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q)∧ r"
proof -
have 1: "p" using assms by (rule conjunct1)
have 2: "(q ∧ r)" using assms 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 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_17:
assumes "(p∧ q) ∧ r"
shows "p ∧ (q∧ r)"
proof -
have 1: "r" using assms by (rule conjunct2)
have 2: "(p∧q)" using assms by (rule conjunct1)
have 3: "p" using 2 by (rule conjunct1)
have 4: "q" using 2 by (rule conjunct2)
have 5: "(q∧r)" using 4 1 by (rule conjI)
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
proof -
have 1: "q" using assms by (rule conjunct2)
show "p⟶ q" using 1 by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}
--Carmen Martinez Navarro , Erlinda Menendez Perez
lemma ejercicio_19:
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ (q ∧ r)"
proof (rule impI)
assume 2: "p"
have 3: "p ⟶ q" using assms by (rule conjunct1)
have 4: "q" using 3 2 by (rule mp)
have 5: "p ⟶ r" using assms by (rule conjunct2)
have 6: "r" using 5 2 by (rule mp)
show "q ∧ r" using 4 6 by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}
-- "Jesús Horno Cobo"
lemma ejercicio_20:
assumes 1:"p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof -
{ assume 3: "p"
have 4: "q ∧ r" using 1 3 by (rule mp)
have 5: "q" using 4 by (rule conjunct1) }
hence 6: "p ⟶ q" by (rule impI)
{ assume 7: "p"
have 8: "q ∧ r" using 1 7 by (rule mp)
have 9: "r" using 8 by (rule conjunct2) }
hence 10: "p ⟶ r" by (rule impI)
show "(p ⟶ q) ∧ (p ⟶ r)" using 6 10 by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_21a:
assumes 1:"p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof
assume 2:"p∧q"
show "r"
proof -
have 3: "p" using 2 by (rule conjunct1)
have 4: "q" using 2 ..
have 5: "(q⟶ r)" using 1 3 ..
show 6: "r" using 5 4 ..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_22a:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q⟶ r"
proof
assume "q"
have "p∧q" using `p` `q` ..
show "r" using assms `p∧q`..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_23a:
assumes 1:"(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof
assume 2:"p∧q"
hence 3:"p" ..
have 4:"q" using 2 ..
hence 5: "p⟶ q" ..
show"r" using 1 5 by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_24a:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
assume 0:"p⟶ q"
show "r"
proof -
have 1: "p" using assms ..
have 2: "q" using 0 1 ..
have 3: "q⟶ r" using assms ..
show 3: "r" using 3 2 ..
qed
qed
section {* Disyunciones *}
text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI1)
qed
text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI2)
qed
text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"
proof -
have "p ∨ q" using assms by this
moreover
{ assume 2: "p"
have "q ∨ p" using 2 by (rule disjI2) }
moreover
{ assume 3: "q"
have "q ∨ p" using 3 by (rule disjI1) }
ultimately show "q ∨ p" by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_28a:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof
assume 1: "p∨q"
moreover
{assume "p"
hence "p∨r" by (rule disjI1)}
moreover
{assume "q"
have "r" using assms `q`..
hence "p∨r" ..}
ultimately
show "p∨r" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_29a:
assumes "p ∨ p"
shows "p"
proof-
have "p∨p" using assms by this
moreover
{assume "p"
hence "p" by this}
moreover
{assume "p"
hence "p" by this}
ultimately
show "p" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_30a:
assumes "p"
shows "p ∨ p"
proof -
show "p∨p" using assms ..
text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_31a:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
proof -
have 1: "p ∨ (q ∨ r)" using assms by this
moreover
{assume "p"
hence "(p∨q)" ..
hence "(p∨q)∨r" ..}
moreover
{assume "(q∨r)"
moreover
{assume "q"
hence "(p∨q)"..
hence "(p∨q)∨r" ..}
moreover
{assume "r"
hence "(p∨q)∨r" ..}
ultimately
have "(p∨q)∨r"..}
ultimately
show "(p∨q)∨r" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}
-- "Pedro G. Ros"
lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using assms(1)
proof
assume "p∨q"
thus "p∨q∨r"
proof
assume "p"
thus "p∨q∨r" ..
next
assume "q"
hence "q∨r" ..
thus "p∨q∨r" ..
qed
next
assume "r"
hence "q∨r" ..
thus "p∨q∨r" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}
-- "Pedro"
lemma ejercicio_33a:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 1: "p" using assms ..
have 2: "q∨r" using assms ..
moreover
{assume 3: "q"
have "(p∧q)" using 1 3 ..
hence "(p ∧ q) ∨ (p ∧ r)" ..}
moreover
{assume 4: "r"
have "p∧r" using 1 4 ..
hence "(p ∧ q) ∨ (p ∧ r)" ..}
ultimately
show "(p ∧ q) ∨ (p ∧ r)" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_34a:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
proof -
have 1: "(p ∧ q) ∨ (p ∧ r)" using assms by this
moreover
{assume "(p ∧ q)"
hence "p" ..
have "q" using `p ∧ q` ..
hence "(q∨r)"..
have "p∧(q∨r)" using `p``(q∨r)`..}
moreover
{assume "(p∧r)"
hence "p" ..
have "r" using `p ∧ r` ..
hence "(q∨r)"..
have "p∧(q∨r)" using `p``(q∨r)`..}
ultimately
show "p ∧ (q ∨ r)" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_35a:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
proof -
have 1: "p ∨ (q ∧ r)" using assms by this
moreover
{assume "p"
hence 2: "(p∨q)" ..
have 3: "(p∨r)" using `p` ..
have 4: "(p ∨ q) ∧ (p ∨ r)" using 2 3 ..}
moreover
{assume 5:"(q∧r)"
hence 6: "q" ..
have 7: "r" using 5 ..
have 8: "p∨q" using 6 ..
have 9: "p∨r" using 7 ..
have "(p ∨ q) ∧ (p ∨ r)"using 8 9 ..}
ultimately
show "(p ∨ q) ∧ (p ∨ r)" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have "p∨q" using assms..
moreover
{assume "p"
hence "p∨(q∧r)"..}
moreover
{assume "q"
have "p∨r" using assms..
moreover
{assume "p"
hence "p∨(q∧r)"..}
moreover
{assume "r"
with `q` have "q∧r"..
hence "p∨(q∧r)"..}
ultimately have "p∨(q∧r)"..}
ultimately show "p∨(q∧r)"..
qed
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}
--Erlinda Menendez Perez , Carmen Martinez Navarro
lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof (rule impI)
assume 1: "p ∨ q"
thus "r"
proof (rule disjE)
assume 2:"p"
have 3: "p ⟶ r" using assms by (rule conjunct1)
show "r" using 3 2 by (rule mp)
next
assume 5:"q"
have 6: "q ⟶ r" using assms by (rule conjunct2)
show "r" using 6 5 by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof -
{assume 1: "p"
have 2:"p ∨ q" using 1 ..
have 3: "r" using assms 2 ..}
hence 4: "p⟶r" ..
{assume 5: "q"
have 6: "p ∨ q" using 5 ..
have 7: "r" using assms 6 ..}
hence 8: "q⟶r" ..
show "(p⟶r)∧(q⟶r)" using 4 8 ..
qed
section {* Negaciones *}
text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_39:
assumes "p"
shows "¬¬p"
proof -
show "¬¬p" using assms by (rule notnotI)
qed
text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
proof (rule impI)
{assume 1: "p"
show "q" using assms 1 by (rule notE)}
qed
text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof (rule impI)
{assume "¬q"
with assms show "¬p" by (rule mt) }
qed
text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
proof -
note `p∨q`
moreover
{assume "p"
hence "p" by this}
moreover
{assume "q"
with assms (2) have "p" ..}
ultimately show "p" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 43. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}
lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
oops
text {* ---------------------------------------------------------------
Ejercicio 44. 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
------------------------------------------------------------------ *}
-- "Raúl montes Pajuelo"
lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
assume "(p⟶q)⟶p"
show "p"
proof (rule ccontr)
note `(p⟶q)⟶p`
assume "¬p"
with `(p⟶q)⟶p` have "¬(p⟶q)" by (rule mt)
{assume "p"
with `¬p` have "q" by (rule notE)}
hence "p⟶q" by (rule impI)
with `¬(p⟶q)` show False by (rule notE)
qed
qed
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
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof(rule conjI)
show "p"
proof(rule ccontr)
{assume "¬p"
hence "¬p∨¬q"..
with assms show False..}
qed
show "q"
proof(rule ccontr)
{assume "¬q"
hence "¬p∨¬q"..
with assms show False..}
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have "¬p∨p"..
moreover
{assume "¬p"
hence "¬p∨¬q"..}
moreover
{assume "p"
have "¬q∨q"..
moreover
{assume "¬q"
hence "¬p∨¬q"..}
moreover
{assume "q"
with `p`have "p∧q"..
with `¬(p∧q)` have "¬p∨¬q"..}
ultimately have "¬p∨¬q"..}
ultimately show "¬p∨¬q"..
qed
text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" ..
moreover
{assume "¬p"
{assume "p"
with `¬p` have "q" ..}
hence "p⟶q" ..
hence "(p⟶q)∨(q⟶p)" ..}
moreover
{assume "p"
{assume "q"
note `p`}
hence "q⟶p"..
hence "(p⟶q)∨(q⟶p)"..}
ultimately show "(p⟶q)∨(q⟶p)" ..
qed
end