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
-- "Pedro G. Ros"
lemma ejercicio_1c:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
using assms ..
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))"
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
-- "Reme Sillero"
lemma ejercicio_11b:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume "p"
with `p ⟶ q` have "q" ..
have "q ⟶ r" using `p⟶ (q ⟶ r)` `p` ..
show "r" using `q ⟶ r` `q` ..
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
-- "Pedro G. Ros"
lemma ejercicio_13b:
assumes 1:"p" and
2:"q"
shows "p ∧ q"
using assms ..
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
-- "Pedro G. Ros Reina"
lemma ejercicio_14b:
assumes "p ∧ q"
shows "p"
using assms ..
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
-- "Pedro G. Ros Reina"
lemma ejercicio_15b:
assumes "p ∧ q"
shows "q"
using assms ..
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
-- "Reme Sillero"
lemma ejercicio_18a:
assumes "p ∧ q"
shows "p ⟶ q"
proof
assume "p"
show "q" using assms ..
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
-- "Antonio Jesús Molero"
lemma ejercicio_20a:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
show "p ⟶ q"
proof (rule impI)
assume "p"
with `p ⟶ q ∧ r` have "q ∧ r" ..
thus "q" ..
qed
show "p ⟶ r"
proof (rule impI)
assume "p"
with `p ⟶ q ∧ r` have "q ∧ r" ..
thus "r" ..
qed
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
-- "Pedro G. Ros Reina"
lemma ejercicio_25b:
assumes "p"
shows "p ∨ q"
using assms ..
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
-- "Pedro G. Ros Reina"
lemma ejercicio_26b:
assumes "q"
shows "p ∨ q"
using assms ..
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
-- "Pedro Ros"
lemma ejercicio_29b:
assumes "p ∨ p"
shows "p"
using assms ..
-- "Antonio Jesús Molero"
lemma ejercicio_29c:
assumes "p ∨ p"
shows "p"
using assms
proof (rule disjE)
assume "p"
thus "p" by this
next
assume "p"
thus "p" by this
qed
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
-- "Pedro Ros"
lemma ejercicio_30a:
assumes "p"
shows "p ∨ p"
proof -
show "p∨p" using assms ..
qed
-- "Pedro Ros"
lemma ejercicio_30b:
assumes "p"
shows "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
-- "Pedro G. Ros Reina"
lemma ejercicio_39b:
assumes "p"
shows "¬¬p"
using assms by (rule notnotI)
-- "Raúl Montes Pajuelo"
lemma ejercicio_39c:
assumes "p"
shows "¬¬p"
proof (rule notI)
assume "¬p"
show False using `¬p` assms..
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
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
proof -
note `p∨q`
moreover
{assume "p"
with assms (2) have False..
hence "q"..}
moreover
{assume "q"
hence "q" .}
ultimately show "q"..
qed
text {* ---------------------------------------------------------------
Ejercicio 44. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof -
{assume "¬p∧¬q"
note `p∨q`
moreover
{have "¬p" using `¬p∧¬q`by (rule conjunct1)
assume "p"
with `¬p`have False by (rule notE)}
moreover
{have "¬q" using `¬p∧¬q`by (rule conjunct2)
assume "q"
with `¬q`have False by (rule notE)}
ultimately have False by (rule disjE)}
thus "¬(¬p∧¬q)" by (rule notI)
qed
text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof (rule notI)
assume "¬p∨¬q"
show False
proof (rule disjE)
{show "¬p∨¬q" using `¬p∨¬q`.
next
show "¬p⟹False"
proof -
{assume "¬p"
have "p" using assms..
with `¬p`show False..}
qed
next
show "¬q⟹False"
proof -
{assume "¬q"
have "q" using assms..
with `¬q`show False..}
qed}
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
show "¬p"
proof (rule notI)
{assume "p"
hence "p∨q"..
with assms show False..}
qed
next
show "¬q"
proof (rule notI)
{assume "q"
hence "p∨q"..
with assms show False..}
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule notI)
assume "p∨q"
show False
proof (rule disjE)
{show "p∨q" using `p∨q` .
next
show "p⟹False"
proof -
{have "¬p" using assms..
assume "p"
with `¬p`show False..}
qed
next
show "q⟹False"
proof -
{have "¬q" using assms..
assume "q"
with `¬q`show False..}
qed}
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule disjE)
show "¬p∨¬q" using assms .
next
show "¬p⟹¬(p∧q)"
proof -
{assume "¬p"
show "¬(p∧q)"
proof (rule notI)
{assume "p∧q"
hence "p"..
with `¬p`show False..}
qed}
qed
next
show "¬q⟹¬(p∧q)"
proof -
{assume "¬q"
show "¬(p∧q)"
proof (rule notI)
{assume "p∧q"
hence "q"..
with `¬q`show False..}
qed}
qed
qed
-- "Pedro Ros"
lemma ejercicio_48b:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule disjE)
show "¬p ∨ ¬q" using assms .
next
assume 1: "¬p"
show "¬(p∧q)"
proof
assume "p∧q"
hence 2: "p" ..
show "False" using 1 2 ..
qed
next
assume 1: "¬q"
show "¬(p∧q)"
proof
assume "p∧q"
hence 2: "q" ..
show "False" using 1 2 ..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_49:
"¬(p ∧ ¬p)"
proof (rule notI)
assume "p∧¬p"
hence "¬p"..
have "p" using `p∧¬p`..
with `¬p`show False..
qed
text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
proof (rule notE)
show "p" using assms ..
show "¬p" using assms ..
qed
text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_51:
assumes "¬¬p"
shows "p"
proof (rule ccontr)
assume "¬p"
with `¬¬p` show False..
qed
-- "Pedro Ros"
lemma ejercicio_51b:
assumes "¬¬p"
shows "p"
using assms by (rule notnotD)
text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_52:
"p ∨ ¬p"
proof (rule ccontr)
{assume "¬(p∨¬p)"
have "p"
proof (rule ccontr)
{assume "¬p"
hence "p∨¬p"..
with `¬(p∨¬p)` show False..}
qed
hence "p∨¬p"..
with `¬(p∨¬p)` show False..}
qed
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
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
{assume "p"
hence "¬¬p" by (rule notnotI)
with `¬q⟶¬p` have "¬¬q" by (rule mt)
show "q"
proof (rule ccontr)
{assume "¬q"
with `¬¬q` show False..}
qed}
qed
-- "Pedro Ros"
lemma ejercicio_54b:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
hence "¬¬p" by (rule notnotI)
with assms have "¬¬q" by (rule mt)
thus q by (rule notnotD)
qed
text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule disjE)
show "¬p∨p"..
show "¬p⟹p∨q"
proof -
{assume "¬p"
have "q"
proof (rule ccontr)
{assume "¬q"
with `¬p` have "¬p∧¬q"..
with assms show False..}
qed
then show "p∨q"..}
qed
show "p⟹p∨q"
proof -
{assume "p"
then show "p∨q"..}
qed
qed
-- "Pedro Ros"
lemma ejercicio_55b:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
hence " ¬p ∧ ¬q" by (rule ejercicio_46)
with assms show "False" ..
qed
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
-- "Raúl Montes Pajuelo: Voy a añadir algunos ejercicios de examen más. Creo que es interesante tenerlos aquí resueltos"
text {* ---------------------------------------------------------------
Ejercicio 59: Examen de Septiembre del 2006. Demostrar
(p ⟶ r) ∨ (q ⟶ s) ⊢ (p ∧ q) ⟶ (r ∨ s)
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_59:
assumes "(p ⟶ r) ∨ (q ⟶ s)"
shows "(p ∧ q) ⟶ (r ∨ s)"
proof
assume "p ∧ q"
show "r ∨ s"
proof (rule disjE)
show "(p ⟶ r) ∨ (q ⟶ s)" using assms.
next
show "p ⟶ r ⟹ r ∨ s"
proof -
assume "p ⟶ r"
have "p" using `p ∧ q`..
with `p ⟶ r`have "r"..
thus "r ∨ s"..
qed
next
show "q ⟶ s ⟹ (r ∨ s)"
proof -
assume "q ⟶ s"
have "q" using `p ∧ q`..
with `q ⟶ s`have "s"..
thus "r ∨ s"..
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 60: Examen de Junio del 2005. Demostrar
p ∧ ¬(q ⟶ r) ⊢ (p ∧ q) ∧ ¬r
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_60:
assumes "p ∧ ¬(q ⟶ r)"
shows "(p ∧ q) ∧ ¬r"
proof (rule conjI)
have "p" using assms..
have "¬(q ⟶ r)" using assms..
have "q"
proof (rule ccontr)
assume "¬q"
have "q ⟶ r"
proof
assume "q"
with `¬q` have False..
thus "r"..
qed
with `¬(q ⟶ r)` show False..
qed
with `p` show "p ∧ q"..
show "¬r"
proof (rule notI)
assume "r"
have "q ⟶ r"
proof
assume "q"
show "r" using `r`.
qed
with `¬(q ⟶ r)`show False..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 61: Examen de Diciembre del 2005. Demostrar
⊢(p ⟶ ¬q) ∧ (p ⟶ ¬r)⟶(p ⟶ ¬(q ∨ r))
------------------------------------------------------------------ *}
-- "Raúl Montes Pajuelo"
lemma ejercicio_61:
"(p ⟶ ¬q) ∧ (p ⟶ ¬r)⟶(p ⟶ ¬(q ∨ r))"
proof (rule impI)
assume "(p ⟶ ¬q) ∧ (p ⟶ ¬r)"
show "(p ⟶ ¬(q ∨ r))"
proof (rule impI)
assume "p"
show "¬(q ∨ r)"
proof (rule notI)
assume "q ∨ r"
thus False
proof
assume "q"
hence "¬¬q" by (rule notnotI)
have "p ⟶ ¬q" using `(p ⟶ ¬q) ∧ (p ⟶ ¬r)`..
have "¬p" using `p ⟶ ¬q` `¬¬q` by (rule mt)
show False using `¬p` `p`..
next
assume "r"
hence "¬¬r" by (rule notnotI)
have "p ⟶ ¬r" using `(p ⟶ ¬q) ∧ (p ⟶ ¬r)`..
have "¬p" using `p ⟶ ¬r` `¬¬r` by (rule mt)
show False using `¬p` `p`..
qed
qed
qed
qed
end