Relación 3

2015-03-15T13:07:10Z

Migpengal:

<source lang = "isar">
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
------------------------------------------------------------------ *}

lemma ejercicio_1:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms(1) assms(2) by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_2:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
proof - have 1: "q" using assms(1) assms(3) by (rule mp)
show "r" using assms(2) 1 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_3:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
proof -
have 1:"q⟶r" using assms(1) assms(3) by (rule mp)
have 2:"q" using assms(2) assms(3) by (rule mp)
show "r" using 1 2 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_4:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"

proof -
{assume 1: "p"
have 2: "q" using assms(1) 1 by (rule mp)
have 3: "r" using assms(2) 2 by (rule mp)}
then show "p⟶r" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_5:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"

proof-
{assume 1: "q"
{assume 2: "p"
have 3:"q⟶r" using assms(1) 2 by (rule mp)
have "r" using 3 1 by (rule mp)}
hence "p⟶r" by (rule impI)}
then show "q⟶(p⟶r)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_6:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"

proof-
{assume 1: "p⟶q"
{assume 2: "p"
have 3: "q⟶r" using assms(1) 2 by (rule mp)
have 4: "q" using 1 2 by (rule mp)
have 5: "r" using 3 4 by (rule mp)}
hence "p⟶r" by (rule impI)}
then show "(p⟶q)⟶(p⟶r)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
proof-
{assume 1: "q"
note `p`}
thus "q⟶p" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
proof-
{assume "p"
{assume "q"
note `p`}
hence "q⟶p" by (rule impI)}
thus "p⟶q⟶p" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_9:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"

proof-
{assume 1: "q⟶r"
{assume 2:"p"
have 3: "q" using assms(1) 2 by (rule mp)
have 4: "r" using 1 3 by (rule mp)}
hence "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))
------------------------------------------------------------------ *}

lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof -
{assume 1: "r"
{assume 2: "q"
{assume 3: "p"
have 4: "q ⟶ (r ⟶ s)" using assms(1) 3 by (rule mp)
have 5: "r⟶s" using 4 2 by (rule mp)
have 6: "s" using 5 1 by (rule mp)}
hence "p⟶s" by (rule impI)}
hence "q⟶(p⟶s)" by (rule impI)}
thus "r⟶(q⟶(p⟶s))" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}

lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"

proof-
{assume 1: "p⟶(q⟶r)"
{ assume 2: "p⟶q"
{assume 3: "p"
have 4: "q⟶r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
have 6: "r" using 4 5 by (rule mp)}
hence "p⟶r" by (rule impI)}
hence "(p⟶q)⟶(p⟶r)" by (rule impI)}
thus "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_12:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"

proof-
{assume 1: "p"
{assume 2: "q"
{assume 3:"p"
note `q`}
hence 4:"p⟶q" by (rule impI)
have 5: "r" using assms(1) 4 by (rule mp)}
hence "q⟶r" by (rule impI)}
thus "p⟶(q⟶r)" by (rule impI)
qed

section {* Conjunciones *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"
proof-
show "p∧q" using assms(1) assms(2) by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
proof-
show "p" using assms(1) by (rule conjunct1)
qed

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
proof-
show "q" using assms(1) by (rule conjunct2)
qed

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}

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

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_17:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"

proof-
have 1: "p ∧ q" using assms(1) by (rule conjunct1)
have 2: "r" using assms(1) by (rule conjunct2)
have 3: "p" using 1 by (rule conjunct1)
have 4: "q" using 1 by (rule conjunct2)
have 5: "q ∧ r" using 4 2 by (rule conjI)
show "p ∧(q ∧ r)" using 3 5 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"

proof-
{assume "p"
have "q" using assms(1) by (rule conjunct2)}
thus "p⟶q" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_19:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"

proof-
{assume 1: "p"
have 2: "p⟶q" using assms(1) by (rule conjunct1)
have 3: "p⟶r" using assms(1) by (rule conjunct2)
have 4: "q" using 2 1 by (rule mp)
have 5: "r" using 3 1 by (rule mp)
have 6: "q ∧ r" using 4 5 by (rule conjI)}
thus "p⟶(q ∧ r)" by(rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}
-- Francisco Javier Carmona

lemma ejercicio_20:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
{ assume 1: "p"
have 2: "q ∧ r" using assms(1) 1 by (rule mp)
have 3: "q" using 2 by (rule conjunct1)}
thus "p ⟶ q" by (rule impI)
next
{ assume 1: "p"
have 2: "q ∧ r" using assms(1) 1 by (rule mp)
have 3: "r" using 2 by (rule conjunct2)}
thus "p ⟶ r" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_21:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof -
{ assume 1: "p ∧ q"
have 2: "p" using 1 by (rule conjunct1)
have 3: "q ⟶ r" using assms(1) 2 by (rule mp)
have 4: "q" using 1 by (rule conjunct2)
have 5: "r" using 3 4 by (rule mp)}
thus "(p ∧ q) ⟶ r" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_22:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof -
{ assume 1: "p"
{assume 2: "q"
have 3: "p ∧ q" using 1 2 by (rule conjI)
have 4: "r" using assms(1) 3 by (rule mp)}
then have 5: "q ⟶ r" by (rule impI)}
thus "p ⟶ (q ⟶ r)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_23:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof -
{ assume 1: "p ∧q"
{assume 2: "p"
have 3: "q" using 1 by (rule conjunct2)}
hence 4: "p ⟶ q" by (rule impI)
have 5: "r" using assms(1) 4 by (rule mp)}
thus "p ∧ q ⟶ r" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_24:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof -
{ assume 1: "p ⟶ q"
have 2: "p" using assms(1) by (rule conjunct1)
have 3: "q" using 1 2 by (rule mp)
have 4: "q ⟶ r" using assms(1) by (rule conjunct2)
have 5: "r" using 4 3 by (rule mp)}
thus "(p ⟶ q) ⟶ r" by (rule impI)
qed

section {* Disyunciones *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
proof -
show "p ∨ q" using assms(1) by (rule disjI1)
qed

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
proof -
show "p ∨ q" using assms(1) by (rule disjI2)
qed

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"
proof -
have "p ∨ q" using assms(1) by this
moreover
{ assume 1: "p"
have 2: "q ∨ p" using 1 by (rule disjI2)}
moreover
{ assume 1: "q"
have 2: "q ∨ p" using 1 by (rule disjI1)}
ultimately show "q ∨ p" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof -
{ assume 1: "p ∨ q"
moreover
{ assume 2: "p"
have 3: "p ∨ r" using 2 by (rule disjI1)}
moreover
{ assume 4: "q"
have 5: "r" using assms(1) 4 by (rule mp)
have 6: "p ∨ r" using 5 by (rule disjI2)}
ultimately have "p ∨r" by (rule disjE)}
thus "p ∨ q ⟶ p ∨ r" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_29:
assumes "p ∨ p"
shows "p"
proof -
have "p ∨ p" using assms(1) by this
moreover
{ assume 1: "p"
have 2: "p" using 1 by this}
moreover
{ assume 3: "p"
have 4: "p" using 3 by this}
ultimately show "p" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
proof -
show "p ∨ p" using assms(1) by (rule disjI1)
qed

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_31:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
proof -
have "p ∨ (q ∨ r)" using assms(1) by this
moreover
{ assume 1: "p"
have 2: "p ∨ q" using 1 by (rule disjI1)
have 3: "(p ∨ q) ∨ r" using 2 by (rule disjI1)}
moreover
{ assume 4: "q ∨ r"
moreover
{ assume 5: "q"
have 6: "p ∨ q" using 5 by (rule disjI2)
have 7: "(p ∨ q) ∨ r" using 6 by (rule disjI1)}
moreover
{ assume 8: "r"
have 9: "(p ∨ q) ∨ r" using 8 by (rule disjI2)}
ultimately have "(p ∨ q) ∨ r" by (rule disjE)}
ultimately show "(p ∨ q) ∨ r" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
proof -
have "(p ∨ q) ∨ r" using assms(1) by this
moreover
{ assume 1: "p ∨ q"
moreover
{ assume 2: "p"
have 3: "p ∨ (q ∨ r)" using 2 by (rule disjI1)}
moreover
{ assume 4: "q"
have 5: "q ∨ r" using 4 by (rule disjI1)
have 6: "p ∨ (q ∨ r)" using 5 by (rule disjI2)}
ultimately have "p ∨ (q ∨ r)" by (rule disjE)}
moreover
{ assume 7: "r"
have 8: "q ∨ r" using 7 by (rule disjI2)
have 9: "p ∨ (q ∨ r)" using 8 by (rule disjI2)}
ultimately show "p ∨ (q ∨ r)" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_33:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "q ∨ r" using assms(1) by (rule conjunct2)
moreover
{ assume 3: "q"
have 4: "p ∧ q" using 1 3 by (rule conjI)
have 5: "(p ∧ q) ∨ (p ∧ r)" using 4 by (rule disjI1)}
moreover
{ assume 6: "r"
have 7: "p ∧ r" using 1 6 by (rule conjI)
have 8: "(p ∧ q) ∨ (p ∧ r)" using 7 by (rule disjI2)}
ultimately show "(p ∧ q) ∨ (p ∧ r)" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_34:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
proof -
have "(p ∧ q) ∨ (p ∧ r)" using assms(1) by this
moreover
{ assume 1: "p ∧ q"
have 2: "q" using 1 by (rule conjunct2)
have 3: "q ∨ r" using 2 by (rule disjI1)
have 4: "p" using 1 by (rule conjunct1)
have 5: "p ∧ (q ∨ r)" using 4 3 by (rule conjI)}
moreover
{ assume 6: "p ∧ r"
have 7: "r" using 6 by (rule conjunct2)
have 8: "q ∨ r" using 7 by (rule disjI2)
have 9: "p" using 6 by (rule conjunct1)
have 10: "p ∧ (q ∨ r)" using 9 8 by (rule conjI)}
ultimately show "p ∧ (q ∨ r)" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
proof -
have "p ∨ (q ∧ r)" using assms(1) by this
moreover
{ assume 1: "p"
have 2: "p ∨ q" using 1 by (rule disjI1)
have 3: "p ∨ r" using 1 by (rule disjI1)
have 4: "(p ∨ q) ∧ (p ∨ r)" using 2 3 by (rule conjI)}
moreover
{ assume 5: "q ∧ r"
have 6: "q" using 5 by (rule conjunct1)
have 7: "p ∨ q" using 6 by (rule disjI2)
have 8: "r" using 5 by (rule conjunct2)
have 9: "p ∨ r" using 8 by (rule disjI2)
have 10: "(p ∨ q) ∧ (p ∨ r)" using 7 9 by (rule conjI)}
ultimately show "(p ∨ q) ∧ (p ∨ r)" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have "(p ∨ q)" using assms(1) by (rule conjunct1)
moreover
{ assume 1: "p"
have 2: "p ∨ (q ∧ r)" using 1 by (rule disjI1)}
moreover
{ assume 3: "q"
have 4: "p ∨ r" using assms(1) by (rule conjunct2)
moreover
{ assume 5: "p"
have 6: "p ∨ (q ∧ r)" using 5 by (rule disjI1)}
moreover
{ assume 7: "r"
have 8: "q ∧ r" using 3 7 by (rule conjI)
have 9: "p ∨ (q ∧ r)" using 8 by (rule disjI2)}
ultimately have "p ∨ (q ∧ r)" by (rule disjE)}
ultimately show "p ∨ (q ∧ r)" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof -
{ assume 1: "p ∨ q"
moreover
{ assume 2: "p"
have 3: "p ⟶ r" using assms(1) by (rule conjunct1)
have 4: "r" using 3 2 by (rule mp)}
moreover
{ assume 5: "q"
have 6: "q ⟶ r" using assms(1) by (rule conjunct2)
have 7: "r" using 6 5 by (rule mp)}
ultimately have "r" by (rule disjE)}
thus "(p ∨ q) ⟶ r" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof (rule conjI)
{ assume 1: "p"
have 2: "p ∨ q" using 1 by (rule disjI1)
have 3: "r" using assms(1) 2 by (rule mp)}
thus "p ⟶ r" by (rule impI)
next
{ assume 4: "q"
have 5: "p ∨ q" using 4 by (rule disjI2)
have 6: "r" using assms(1) 5 by (rule mp)}
thus "q ⟶ r" by (rule impI)
qed

section {* Negaciones *}

text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_39:
assumes "p"
shows "¬¬p"
proof -
show "¬¬p" using assms(1) by (rule notnotI)
qed

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
proof -
{ assume 1: "p"
have 2: "False" using assms(1) 1 by (rule notE)
have 3: "q" using 2 by (rule FalseE)}
thus "p ⟶ q" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof -
{assume 1: "¬q"
have 2: "¬p" using assms(1) 1 by (rule mt)}
thus "¬q ⟶ ¬p" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
proof -
have "p ∨ q" using assms(1) by this
moreover
{ assume 1: "p"
have 2: "p" using 1 by this}
moreover
{ assume 3: "q"
have 4: "False" using assms(2) 3 by (rule notE)
have 5: "p" using 4 by (rule FalseE)}
ultimately show "p" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
proof -
have "p ∨ q" using assms(1) by this
moreover
{ assume 1: "p"
have 2: "False" using assms(2) 1 by (rule notE)
have 3: "q" using 2 by (rule FalseE)}
moreover
{ assume 4: "q"
have 5: "q" using 4 by this}
ultimately show "q" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof (rule ccontr)
assume 1: "¬¬(¬p ∧ ¬q)"
have 2: "¬p ∧ ¬q" using 1 by (rule notnotD)
have 3: "p ∨ q" using assms(1) by this
moreover
{ assume 4: "p"
have 5: "¬p" using 2 by (rule conjunct1)
have 6: "False" using 5 4 by (rule notE)}
moreover
{ assume 7: "q"
have 8: "¬q" using 2 by (rule conjunct2)
have 9: "False" using 8 7 by (rule notE)}
ultimately show "False" by (rule disjE)
qed

-- Miguel Peña Gallardo

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof-
{assume 1:"¬¬(¬p ∧ ¬q)"
have 2: "(¬p ∧ ¬q)" using 1 by (rule notnotD)
have 3: "¬p" using 2 by (rule conjunct1)
have 4: "¬q" using 2 by (rule conjunct2)
have "p∨q" using assms(1) by this
moreover
{assume 5: "p"
have 6: "False" using 3 5 by (rule notE)}
moreover
{assume 7: "q"
have 8: "False" using 4 7 by (rule notE)}
ultimately have "False" by (rule disjE)}
then show "¬(¬p ∧¬q)" by (rule ccontr)

qed

text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof (rule ccontr)
assume 1: "¬¬(¬p ∨ ¬q)"
have 2: "¬p ∨ ¬q" using 1 by (rule notnotD)
moreover
{assume 3: "¬p"
have 4: "p" using assms(1) by (rule conjunct1)
have 5: "False" using 3 4 by (rule notE)}
moreover
{ assume 6: "¬q"
have 7: "q" using assms(1) by (rule conjunct2)
have 8: "False" using 6 7 by (rule notE)}
ultimately show "False" by (rule disjE)
qed

--Miguel Peña Gallardo

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"

proof-
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "q" using assms(1) by (rule conjunct2)
{assume 3: "¬¬(¬p∨¬q)"
have 4: "¬p ∨¬q" using 3 by (rule notnotD)
have "¬p ∨¬q" using 4 by this
moreover
{assume 5: "¬p"
have 6: "False" using 5 1 by (rule notE)}
moreover
{assume 7: "¬q"
have 8: "False" using 7 2 by (rule notE)}
ultimately have "False" by (rule disjE)}
then show "¬(¬p∨¬q)" by (rule ccontr)

qed

text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
{assume 1: "¬¬p"
have 2: "p" using 1 by (rule notnotD)
have 3: "p ∨ q" using 2 by (rule disjI1)
have 4: "False" using assms(1) 3 by (rule notE)}
thus 5: "¬p" by (rule ccontr)
next
{ assume 6: "¬¬q"
have 7: "q" using 6 by (rule notnotD)
have 8: "p ∨ q" using 7 by (rule disjI2)
have 9: "False" using assms(1) 8 by (rule notE)}
thus 10: "¬q" by (rule ccontr)
qed

text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule ccontr)
assume 1: "¬¬(p ∨ q)"
have 2: "p ∨ q" using 1 by (rule notnotD)
moreover
{ assume 3: "p"
have 4: "¬p" using assms(1) by (rule conjunct1)
have 5: "False" using 4 3 by (rule notE)}
moreover
{ assume 6: "q"
have 7: "¬q" using assms(1) by (rule conjunct2)
have 8: "False" using 7 6 by (rule notE)}
ultimately show "False" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule ccontr)
assume 1: "¬¬(p ∧ q)"
have 2: "(p ∧ q)" using 1 by (rule notnotD)
have 3: "¬p ∨ ¬q" using assms(1) by this
moreover
{ assume 4: "¬p"
have 5: "p" using 2 by (rule conjunct1)
have 6: "False" using 4 5 by (rule notE)}
moreover
{ assume 7: "¬q"
have 8: "q" using 2 by (rule conjunct2)
have 9: "False" using 7 8 by (rule notE)}
ultimately show "False" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_49:
"¬(p ∧ ¬p)"
proof -
{assume 1: "¬¬(p ∧ ¬p)"
have 2: "p ∧ ¬p" using 1 by (rule notnotD)
have 3: "p" using 2 by (rule conjunct1)
have 4: "¬p" using 2 by (rule conjunct2)
have 5: "False" using 4 3 by (rule notE)}
thus "¬(p ∧ ¬p)" by (rule ccontr)
qed

text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
proof -
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "¬p" using assms(1) by (rule conjunct2)
have 3: "False" using 2 1 by (rule notE)
show 4: "q" using 3 by (rule FalseE)
qed

text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_51:
assumes "¬¬p"
shows "p"
proof -
show "p" using assms(1) by (rule notnotD)
qed

text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_52:
"p ∨ ¬p"
proof -
have 1: "¬p ∨ p" by (rule excluded_middle)
moreover
{ assume 2: "¬p"
have 3: "p ∨ ¬p" using 2 by (rule disjI2)}
moreover
{ assume 4: "p"
have 5: "p ∨ ¬p" using 4 by (rule disjI1)}
ultimately show "p ∨ ¬p" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
proof -
{assume 1: "(p ⟶ q) ⟶ p"
{ assume 3: "¬p"
have 4: "¬(p ⟶ q)" using 1 3 by (rule mt)
{ assume 5: "p"
have 6: "False" using 3 5 by (rule notE)
have 7: "q" using 6 by (rule FalseE)}
hence 8: "p ⟶ q" by (rule impI)
have 9: "False" using 4 8 by (rule notE)}
hence 10: "p" by (rule ccontr)}
thus 11: "((p ⟶ q) ⟶ p) ⟶ p" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
assume 1: "p"
have 2: "¬q ∨ q" by (rule excluded_middle)
moreover
{ assume 3: "¬q"
have 4: "¬p" using assms(1) 3 by (rule mp)
have 5: "False" using 4 1 by (rule notE)
have 6: "q" using 5 by (rule FalseE)}
moreover
{ assume 7: "q"
have 8: "q" using 7 by this}
ultimately show "q" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
have 1: "¬p ∨ p" by (rule excluded_middle)
moreover
{ assume 2: "¬p"
have 3: "¬q ∨ q" by (rule excluded_middle)
moreover
{ assume 4: "¬q"
have 5: "¬p ∧ ¬ q" using 2 4 by (rule conjI)
have 6: "False" using assms(1) 5 by (rule notE)
have 7: "p ∨ q" using 6 by (rule FalseE)}
moreover
{ assume 8: "q"
have 9: "p ∨ q" using 8 by (rule disjI2)}
ultimately have "p ∨ q" by (rule disjE)}
moreover
{ assume 10: "p"
have 11: "p ∨ q" using 10 by (rule disjI1)}
ultimately show "p ∨ q" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule conjI)
{ assume 1: "¬p"
have 2: "¬p ∨ ¬q" using 1 by (rule disjI1)
have 3: "False" using assms(1) 2 by (rule notE)}
thus 4: "p" by (rule ccontr)
next
{ assume 5: "¬q"
have 6: "¬p ∨ ¬q" using 5 by (rule disjI2)
have 7: "False" using assms(1) 6 by (rule notE)}
thus 8: "q" by (rule ccontr)
qed

text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have 1: "¬p ∨ p" by (rule excluded_middle)
moreover
{ assume 2: "¬p"
have 3: "¬p ∨ ¬q" using 2 by (rule disjI1)}
moreover
{ assume 4: "p"
have 5: "¬q ∨ q" by (rule excluded_middle)
moreover
{ assume 6: "¬q"
have 7: "¬p ∨ ¬q" using 6 by (rule disjI2)}
moreover
{ assume 8: "q"
have 9: "p ∧ q" using 4 8 by (rule conjI)
have 10: "False" using assms(1) 9 by (rule notE)
have 11: "¬p ∨ ¬q" using 10 by (rule FalseE)}
ultimately have "¬p ∨ ¬q" by (rule disjE)}
ultimately show "¬p ∨ ¬q" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" by (rule excluded_middle)
moreover
{ assume "¬p"
{ assume "p"
with `¬p` have "False" by (rule notE)
hence "q" by (rule FalseE)}
hence "p ⟶ q" by (rule impI)
hence "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)}
moreover
{ assume 1: "p"
{ assume "q"
have "p" using 1 by this}
hence "q ⟶ p" by (rule impI)
hence "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)}
ultimately show "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjE)
qed

end

</source>

Lógica matemática y fundamentos (2014-15) - Contribuciones del usuario [es]

Relación 3