Relación 3

2016-03-15T16:18:41Z

Manmailop:

<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,2) by (rule mp)
qed

lemma ejercicio_1_b:
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,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" using assms(2,3) by (rule mp)
have 2: "q⟶r" using assms(1,3) by (rule mp)
show "r" using 2 1 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 ..
have 3: "r" using assms(2) 2 ..}
thus "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)"

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

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

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 2 by (rule mp)
have 4: "q" using 1 2 by (rule mp)
have "r" using 3 4 by (rule mp)}
hence "p⟶r" by (rule impI)}
thus "(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"
have "p" using assms .}
thus "q⟶p" by (rule impI)
qed

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

lemma ejercicio_8:
"p ⟶ (q ⟶ p)"

proof-
{assume 1:"p"
{assume 2:"q"
have 3: "p" using 1 .}
hence "q⟶p" ..}
thus "p⟶(q⟶p)" ..
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 2 ..
have "r" using 1 3 ..}
hence "p⟶r" ..}
thus "(q⟶r)⟶(p⟶r) " ..
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 3 ..
have 5: "r⟶s" using 4 2 ..
have 6: "s" using 5 1 ..}
hence "p⟶s" ..}
hence "q⟶(p⟶s)" ..}
thus "r⟶(q⟶(p⟶s))" ..
qed

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

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

proof (rule impI)
assume 3: "p⟶(q⟶r)"
show "(p⟶q)⟶(p⟶r)"
proof(rule impI)
assume 2:"p⟶q"
show "p⟶r"
proof (rule impI)
assume 1: "p"
have 4:"q" using 2 1 ..
have 5:"q⟶r" using 3 1 ..
show "r" using 5 4 ..
qed
qed
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 3:"q"
have 4:"p" using 1 .
have 5:"q" using 3 .
then have 6:"p⟶q" ..
have "r" using assms 6 ..}
hence "q⟶r" ..}
thus "p⟶(q⟶r)" ..
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 by (rule conjunct1)
qed

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

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
------------------------------------------------------------------ *}

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)
then have 3:"q" by (rule conjunct1)
have 4:"r" using 2 by (rule conjunct2)
have "p∧q" using 1 3 by (rule conjI)
then show "(p∧q)∧r" using 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 by (rule conjunct1)
have 2:"r" using assms 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-
have 1:"p" using assms ..
have 2:"q" using assms ..
then show "p⟶q" ..
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-
have 1:"p⟶q" using assms ..
have 2:"p⟶r" using assms ..
{assume 3:"p"
have 4:"q" using 1 3 ..
have 5:"r" using 2 3 ..
have 6:"q∧r" using 4 5 ..}
thus "p ⟶ q ∧ r" ..
qed

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

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

proof-
{assume 1: p
have 2:"q∧r" using assms 1 ..
have "r" using 2 ..}
hence 1:"p⟶r" ..
{assume 1: p
have 2:"q∧r" using assms 1 ..
have "q" using 2 ..}
hence 2:"p⟶q" ..
then show "(p ⟶ q) ∧ (p ⟶ r)" using 1 ..
qed

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

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

proof-
{assume 1:"p∧q"
have 2:"p" using 1 ..
have 3:"q⟶r" using assms 2 ..
have 4: "q" using 1 ..
have "r" using 3 4 ..}
thus "p∧q ⟶r" ..
qed

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

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 ..
have "r" using assms 3 ..}
hence "q⟶r" ..}
thus "p⟶(q⟶r)" ..
qed

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

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

proof-
{assume 1:"p∧q"
have 2:"p" using 1 ..
{assume "p"
have 3: "q" using 1 ..}
hence 4:"p⟶q" ..
have "r" using assms 4 ..}
thus "p∧q ⟶r" ..
qed

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

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

proof-
{assume 1: "p⟶q"
have 2:"p" using assms ..
have 3:"q⟶r" using assms..
have 4:"q" using 1 2 ..
have "r" using 3 4 ..}
thus "(p⟶q)⟶r" ..
qed

section {* Disyunciones *}

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

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
------------------------------------------------------------------ *}

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
------------------------------------------------------------------ *}

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
------------------------------------------------------------------ *}

lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof-
{assume "p ∨ q"
moreover
{ assume 1:"p"
have "p ∨ r" using 1 by (rule disjI1)}
moreover
{ assume 2:"q"
have 3:"r" using assms 2 by (rule mp)
have "p ∨ r" using 3 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
------------------------------------------------------------------ *}

lemma ejercicio_29:
assumes "p ∨ p"
shows "p"

proof-
have 1: "p ∨ p" using assms by this
moreover
{assume 1:"p"
have "p" using 1 by this}
moreover
{assume 2:"p"
have "p" using 2 by this}
ultimately show "p" by (rule disjE)

qed
text{* Otra forma:
using assms
proof
assume "p"
thus "p" .
qed}

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

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

text{* Otra forma:
using assms
proof
qed}

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

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{* Otra forma:
using assms
proof
assume "p"
then have "p∨q" ..
thus "(p∨q)∨r" ..
next
assume 1:"q∨r"
thus "(p ∨ q) ∨ r"
proof
assume "q"
then have "p∨q" ..
thus 1: "(p ∨ q) ∨ r" ..
next
assume "r"
then have 2:"(p∨q)∨r" ..
then have "q∨r⟶(p ∨ q) ∨ r" ..
thus "(p ∨ q) ∨ r" using 1 ..
qed}

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

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)
------------------------------------------------------------------ *}

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)
------------------------------------------------------------------ *}

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)
------------------------------------------------------------------ *}

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)
------------------------------------------------------------------ *}

lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof-
have "(p ∨ q)" using assms by (rule conjunct1)
moreover
{assume 1:"p"
have "p ∨ (q ∧ r)" using 1 by (rule disjI1) }
moreover
{assume 1:"q"
have "(p ∨ r)" using assms by (rule conjunct2)
moreover
{assume 2:"p"
have "p ∨ (q ∧ r)" using 2 by (rule disjI1)}
moreover
{assume 2:"r"
have 3:"(q ∧ r)" using 1 2 by (rule conjI)
have "p ∨ (q ∧ r)" using 3 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
------------------------------------------------------------------ *}

lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof-
{assume "p ∨ q"
moreover
{assume 1:"p"
have 2:"(p ⟶ r)" using assms by (rule conjunct1)
have "r" using 2 1 by (rule mp)}
moreover
{assume 1:"q"
have 2:"(q ⟶ r)" using assms by (rule conjunct2)
have "r" using 2 1 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)
------------------------------------------------------------------ *}

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
oops

section {* Negaciones *}

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

lemma ejercicio_39:
assumes "p"
shows "¬¬p"
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-
{assume 1: "p"
have "q" using assms 1 ..}
thus "p⟶q" ..
qed

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

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

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

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"

using assms(1)
proof
assume "p"
thus "p" .
next
assume 1:"q"
show "p" using assms(2) 1 ..
qed

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

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"

using assms(1)
proof
assume "q"
thus "q" .
next
assume 1:"p"
show "q" using assms(2) 1 ..
qed

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

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

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

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

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

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

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

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

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

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

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

lemma ejercicio_49:
"¬(p ∧ ¬p)"
oops

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

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
oops

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

lemma ejercicio_51:
assumes "¬¬p"
shows "p"
oops

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

lemma ejercicio_52:
"p ∨ ¬p"
oops

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

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
oops

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

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
oops

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

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

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

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

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

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

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

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
oops

end
</source>

Lógica Matemática y fundamentos (2015-16) - Contribuciones del usuario [es]

Relación 3