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"
lemma ejercicio_1a:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show 3: "q" using 1 2 by (rule mp)
qed
-- "Pedro"
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"
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
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}
-- "Pedro"
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
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}
-- "Pedro"
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
-- "Pedro"
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)
------------------------------------------------------------------ *}
-- "Pedro"
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)
------------------------------------------------------------------ *}
-- "Pedro"
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"
lemma ejercicio_7a:
assumes "p"
shows "q ⟶ p"
proof -
{assume 1: "q"}
show "q ⟶ p" using assms(1) by (rule impI)
qed
-- "Dani"
lemma ejercicio_7b:
assumes "p"
shows "q ⟶ p"
proof
assume "q"
show "p" using assms(1) .
qed
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}
-- "Dani"
lemma ejercicio_8a:
"p ⟶ (q ⟶ p)"
proof
assume "p"
show "q ⟶ p"
proof
assume "q"
show "p" using `p` .
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
-- "Pedro"
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)
------------------------------------------------------------------ *}
lemma ejercicio_12:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
oops
section {* Conjunciones *}
text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}
-- "Pedro"
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"
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"
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"
lemma ejercicio_16a:
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
-- Dani (No estoy seguro de si el ejercicio hecho por Pedro funciona)
lemma ejercicio_16b:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof
have "p" using assms(1) by (rule conjunct1)
have "q ∧ r" using assms(1) by (rule conjunct2)
hence "q" by (rule conjunct1)
show "p ∧ q" using `p` `q` by (rule conjI)
next
have "q ∧ r" using assms(1) by (rule conjunct2)
thus "r" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
-- "Pedro"
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"
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
------------------------------------------------------------------ *}
-- "Pedro"
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)
------------------------------------------------------------------ *}
lemma ejercicio_20:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
oops
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
-- Dani
lemma ejercicio_23b:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
hence p ..
have q using `p ∧ q` ..
hence "p ⟶ q" ..
with assms(1) show "r" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
-- Dani
lemma ejercicio_24a:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
assume "p ⟶ q"
have "p" using assms(1) ..
with `p ⟶ q` have "q" ..
have "q ⟶ r" using assms(1) ..
thus "r" using `q` ..
qed
section {* Disyunciones *}
text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "Pedro"
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"
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"
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"
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)
------------------------------------------------------------------ *}
text {* Pedro. Vienen demostradas en la teoría y necesito usarlas *}
lemma or2: "⟦P∨Q; ¬P⟧⟹ Q"
by auto
lemma LEM: "P ∨ ¬P"
by auto
lemma ejercicio_36a:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
using LEM
proof
have 1:"(p∨q)" using assms ..
have 2: "(p∨r)" using assms ..
assume "p"
thus "p∨(q∧r)" ..
next
have 1:"(p∨q)" using assms ..
have 2: "(p∨r)" using assms ..
assume "¬p"
have "q" using 1 `¬p` by (rule or2)
have "r" using 2 `¬p` by (rule or2)
have "q∧r" using `q` `r` ..
thus "p∨(q∧r)" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}
lemma ejercicio_37a:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof (rule impI)
assume 0:"p∨q"
show "r"
proof (rule disjE)
show "p∨q" using 0 .
next
assume p
have 1: "p⟶r" using assms ..
thus r using `p` ..
next
assume q
have 2: "q⟶r" using assms ..
thus r using `q`..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}
-- Dani
lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof
show "p ⟶ r"
proof
assume p
hence "p ∨ q" ..
with assms show r ..
qed
next
show "q ⟶ r"
proof
assume q
hence "p ∨ q" ..
with assms show r ..
qed
qed
section {* Negaciones *}
text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}
-- "Pedro"
lemma ejercicio_39:
assumes "p"
shows "¬¬p"
proof -
show "¬¬p" using assms by (rule notnotI)
qed
text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
proof (rule impI)
assume p
with assms show q ..
qed
text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}
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
------------------------------------------------------------------ *}
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 42. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}
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 40. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}
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)
------------------------------------------------------------------ *}
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
------------------------------------------------------------------ *}
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)
------------------------------------------------------------------ *}
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)
------------------------------------------------------------------ *}
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)
------------------------------------------------------------------ *}
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
------------------------------------------------------------------ *}
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
------------------------------------------------------------------ *}
lemma ejercicio_51b:
assumes "¬¬p"
shows "p"
using assms by (rule notnotD)
text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}
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
------------------------------------------------------------------ *}
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_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
------------------------------------------------------------------ *}
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
------------------------------------------------------------------ *}
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
------------------------------------------------------------------ *}
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)
------------------------------------------------------------------ *}
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