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

Ejercicio 3

2013-04-27T10:30:34Z

Erlmenper: /* Selección del ejercicio */

== Enunciado ==
El tercer ejercicio evaluable consiste en la realización de un ejercicio de argumentación en lógica de primer orden, haciendo la demostración por deducción natural con Isabelle/HOL y por tableros semánticos.
Para ello,
* Cada alumno elegirá uno de los ejercicios propuestos en [[E3|E3]].
* Una vez elegido, lo anotará en la lista que se muestra a continuación, no pudiendo un mismo ejercicio ser elegido por más de un alumno.
* Se enviará a mjoseh@us.es antes del viernes 10 de mayo de 2013, dos ficheros: uno usuario_3a.thy con la prueba por deducción natural y otro con la prueba por tableros.
* Los lemas que se usen en una demostración tendrán que ser probados de forma no automática.
* En la valoración del ejercicio se tendrá en cuenta tanto el nivel de dificultad como la calidad de la demostración.

== Selección del ejercicio ==

* Ejercicio 1:
* Ejercicio 2: Francisco Vilches Chacón
* Ejercicio 3:
* Ejercicio 4: M Inmaculada Arjona Arjona
* Ejercicio 5:
* Ejercicio 6:
* Ejercicio 7:
* Ejercicio 8:
* Ejercicio 9:
* Ejercicio 10: Gonzalo José Muñoz González-Meneses
* Ejercicio 11: José Antonio Jaime Sabín
* Ejercicio 12: Erlinda Menéndez Pérez
* Ejercicio 13: Concepción García Vidal
* Ejercicio 14: Carmen Martínez Navarro
* Ejercicio 15:
* Ejercicio 16:
* Ejercicio 17:
* Ejercicio 18:
* Ejercicio 19: Mª de los Remedios Sillero Denamiel
* Ejercicio 20: Antonio Jesús Molero del Río
* Ejercicio 21: Irene Araujo Guijo
* Ejercicio 22: FºJavier Sanz Gil
* Ejercicio 23:
* Ejercicio 24:
* Ejercicio 25:
* Ejercicio 26: José María Contreras Beltrán
* Ejercicio 27: Isabel Duarte Tosso
* Ejercicio 28:

Ejercicio 2

2013-04-12T14:07:40Z

Erlmenper: /* Selección del ejercicio */

== Enunciado ==
El segundo ejercicio evaluable consiste en la realización de una demostración por deducción natural en la Lógica de primer orden, con Isabelle/HOL.
Para ello,
* Cada alumno elegirá uno de los ejercicios propuestos en [[T2|T2]].
* Una vez elegido, lo anotará en la lista que se muestra a continuación, no pudiendo un mismo ejercicio ser elegido por más de un alumno.
* El ejercicio resuelto se enviará a mjoseh@us.es en un fichero usuario_2.thy antes del viernes 26 de abril de 2013.
* En la valoración del ejercicio se tendrá en cuenta tanto el nivel de dificultad como la calidad de la demostración.

== Selección del ejercicio ==

* Ejercicio 1: Francisco Vilches Chacón
* Ejercicio 2:
* Ejercicio 3:
* Ejercicio 4:
* Ejercicio 5:
* Ejercicio 6:
* Ejercicio 7:
* Ejercicio 8: Inmaculada Arjona Arjona
* Ejercicio 9:
* Ejercicio 10:
* Ejercicio 11:
* Ejercicio 12:
* Ejercicio 13:
* Ejercicio 14:
* Ejercicio 15:
* Ejercicio 16:
* Ejercicio 17:
* Ejercicio 18:
* Ejercicio 19:
* Ejercicio 20:
* Ejercicio 21:
* Ejercicio 22: Erlinda Menéndez Pérez
* Ejercicio 23: Irene Araujo Guijo
* Ejercicio 24:
* Ejercicio 25:
* Ejercicio 26: José Mª Contreras Beltrán
* Ejercicio 27: FºJavier Sanz Gil
* Ejercicio 28: Isabel Duarte Tosso
* Ejercicio 29:
* Ejercicio 30:
* Ejercicio 31:
* Ejercicio 32:
* Ejercicio 33:

Ejercicio 2

2013-04-12T13:51:12Z

Erlmenper: /* Selección del ejercicio */

== Enunciado ==
El segundo ejercicio evaluable consiste en la realización de una demostración por deducción natural en la Lógica de primer orden, con Isabelle/HOL.
Para ello,
* Cada alumno elegirá uno de los ejercicios propuestos en [[T2|T2]].
* Una vez elegido, lo anotará en la lista que se muestra a continuación, no pudiendo un mismo ejercicio ser elegido por más de un alumno.
* El ejercicio resuelto se enviará a mjoseh@us.es en un fichero usuario_2.thy antes del viernes 26 de abril de 2013.
* En la valoración del ejercicio se tendrá en cuenta tanto el nivel de dificultad como la calidad de la demostración.

== Selección del ejercicio ==

* Ejercicio 1: Francisco Vilches Chacón
* Ejercicio 2:
* Ejercicio 3:
* Ejercicio 4:
* Ejercicio 5:
* Ejercicio 6:
* Ejercicio 7:
* Ejercicio 8: Inmaculada Arjona Arjona
* Ejercicio 9:
* Ejercicio 10:
* Ejercicio 11:
* Ejercicio 12:
* Ejercicio 13:
* Ejercicio 14:
* Ejercicio 15:
* Ejercicio 16:
* Ejercicio 17:
* Ejercicio 18:
* Ejercicio 19:
* Ejercicio 20:
* Ejercicio 21:
* Ejercicio 22:
* Ejercicio 23: Irene Araujo Guijo
* Ejercicio 24:
* Ejercicio 25:
* Ejercicio 26: José Mª Contreras Beltrán
* Ejercicio 27: FºJavier Sanz Gil
* Ejercicio 28: Isabel Duarte Tosso
* Ejercicio 29:
* Ejercicio 30:
* Ejercicio 31:
* Ejercicio 32:
* Ejercicio 33:

Relación 3

2013-03-06T12:47:17Z

Erlmenper:

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

-- "Pedro G. Ros"
lemma ejercicio_1a:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show 3: "q" using 1 2 by (rule mp)
qed

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

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

-- "Pedro G. Ros"
lemma ejercicio_2a:
assumes 1:"p ⟶ q" and
2:"q ⟶ r" and
3:"p"
shows "r"
proof -
have 4: "q" using 1 3 by (rule mp)
show 5: "r" using 2 4 by (rule mp)
qed

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

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

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

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

lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
oops

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

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

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 G. Ros Reina"

lemma ejercicio_13:
assumes 1:"p" and
2:"q"
shows "p ∧ q"
proof -
show "p ∧ q" using 1 2 by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
proof -
show "p" using assms by (rule conjunct1)
qed

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
proof -
show "q" using assms by (rule conjunct2)
qed

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q)∧ r"
proof -
have 1: "p" using assms by (rule conjunct1)
have 2: "(q ∧ r)" using assms by (rule conjunct2)
have 3: "q" using 2 by (rule conjunct1)
have 4: "r" using 2 by (rule conjunct2)
have 5: "(p∧q)" using 1 3 by (rule conjI)
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_17:
assumes "(p∧ q) ∧ r"
shows "p ∧ (q∧ r)"
proof -
have 1: "r" using assms by (rule conjunct2)
have 2: "(p∧q)" using assms by (rule conjunct1)
have 3: "p" using 2 by (rule conjunct1)
have 4: "q" using 2 by (rule conjunct2)
have 5: "(q∧r)" using 4 1 by (rule conjI)
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
proof -
have 1: "q" using assms by (rule conjunct2)
show "p⟶ q" using 1 by (rule impI)
qed

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

--Carmen Martinez Navarro , Erlinda Menendez Perez

lemma ejercicio_19:
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ (q ∧ r)"
proof (rule impI)
assume 2: "p"
have 3: "p ⟶ q" using assms by (rule conjunct1)
have 4: "q" using 3 2 by (rule mp)
have 5: "p ⟶ r" using assms by (rule conjunct2)
have 6: "r" using 5 2 by (rule mp)
show "q ∧ r" using 4 6 by (rule conjI)
qed

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

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

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

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

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

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

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

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

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

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

section {* Disyunciones *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI1)
qed

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI2)
qed

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"
proof -
have "p ∨ q" using assms by this
moreover
{ assume 2: "p"
have "q ∨ p" using 2 by (rule disjI2) }
moreover
{ assume 3: "q"
have "q ∨ p" using 3 by (rule disjI1) }
ultimately show "q ∨ p" by (rule disjE)
qed

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

lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
oops

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

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

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

lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
oops

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

lemma ejercicio_31:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
oops

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

lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
oops

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

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

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

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

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

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

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

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

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

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

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
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_39:
assumes "p"
shows "¬¬p"
proof -
show "¬¬p" using assms by (rule notnotI)
qed

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

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

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

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

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

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

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

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

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>

Relación 3

2013-03-06T11:27:14Z

Erlmenper:

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

-- "Pedro G. Ros"
lemma ejercicio_1a:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show 3: "q" using 1 2 by (rule mp)
qed

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

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

-- "Pedro G. Ros"
lemma ejercicio_2a:
assumes 1:"p ⟶ q" and
2:"q ⟶ r" and
3:"p"
shows "r"
proof -
have 4: "q" using 1 3 by (rule mp)
show 5: "r" using 2 4 by (rule mp)
qed

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

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

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

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

lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
oops

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

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

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 G. Ros Reina"

lemma ejercicio_13:
assumes 1:"p" and
2:"q"
shows "p ∧ q"
proof -
show "p ∧ q" using 1 2 by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
proof -
show "p" using assms by (rule conjunct1)
qed

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
proof -
show "q" using assms by (rule conjunct2)
qed

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q)∧ r"
proof -
have 1: "p" using assms by (rule conjunct1)
have 2: "(q ∧ r)" using assms by (rule conjunct2)
have 3: "q" using 2 by (rule conjunct1)
have 4: "r" using 2 by (rule conjunct2)
have 5: "(p∧q)" using 1 3 by (rule conjI)
show 6: "(p∧q) ∧ r" using 5 4 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_17:
assumes "(p∧ q) ∧ r"
shows "p ∧ (q∧ r)"
proof -
have 1: "r" using assms by (rule conjunct2)
have 2: "(p∧q)" using assms by (rule conjunct1)
have 3: "p" using 2 by (rule conjunct1)
have 4: "q" using 2 by (rule conjunct2)
have 5: "(q∧r)" using 4 1 by (rule conjI)
show 6: "p∧(q∧r)" using 3 5 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
proof -
have 1: "q" using assms by (rule conjunct2)
show "p⟶ q" using 1 by (rule impI)
qed

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

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

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

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

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

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

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

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

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

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

section {* Disyunciones *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI1)
qed

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
proof -
show "p∨q" using assms by (rule disjI2)
qed

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"
proof -
have "p ∨ q" using assms by this
moreover
{ assume 2: "p"
have "q ∨ p" using 2 by (rule disjI2) }
moreover
{ assume 3: "q"
have "q ∨ p" using 3 by (rule disjI1) }
ultimately show "q ∨ p" by (rule disjE)
qed

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

lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
oops

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

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

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

lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
oops

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

lemma ejercicio_31:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
oops

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

lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
oops

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

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

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

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

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

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

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

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

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

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

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
------------------------------------------------------------------ *}
-- "Pedro G. Ros Reina"
lemma ejercicio_39:
assumes "p"
shows "¬¬p"
proof -
show "¬¬p" using assms by (rule notnotI)
qed

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

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

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

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

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

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

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

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

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>