chapter {* R4: Deducción natural proposicional *}
theory R4_sol
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
· excluded_middle: ¬P ∨ 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_1a:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show "q" using 1 2 by (rule mp)
qed
lemma ejercicio_1b:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms by (rule mp)
qed
lemma ejercicio_1c:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms ..
qed
lemma ejercicio_1d:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms by auto
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}
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
lemma ejercicio_2b:
assumes 1:"p ⟶ q" and
2:"q ⟶ r" and
3:"p"
shows "r"
proof -
have 4: "q" using 1 3 by (rule mp)
show "r" using 2 4 by (rule mp)
qed
lemma ejercicio_2c:
assumes "p ⟶ q" and
"q ⟶ r" and
"p"
shows "r"
proof -
have "q" using assms(1,3) ..
show "r" using assms(2) `q` ..
qed
lemma ejercicio_2d:
assumes "p ⟶ q" and
"q ⟶ r" and
"p"
shows "r"
proof -
show "r" using assms by auto
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}
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
lemma ejercicio_3b:
assumes "p ⟶ (q ⟶ r)" and
"p ⟶ q" and
"p"
shows "r"
proof -
have 4: "q ⟶ r" using assms(1,3) ..
have "q" using assms(2,3) ..
show "r" using 4 `q` ..
qed
lemma ejercicio_3c:
assumes "p ⟶ (q ⟶ r)" and
"p ⟶ q" and
"p"
shows "r"
proof -
have "q" using assms(2,3) ..
have "q ⟶ r" using assms(1,3) ..
thus "r" using `q` ..
qed
lemma ejercicio_3d:
assumes "p ⟶ (q ⟶ r)" and
"p ⟶ q" and
"p"
shows "r"
proof -
show "r" using assms by auto
qed
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}
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_4b:
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"
proof (rule impI)
assume 3:"p"
have "q" using 1 3 by (rule mp)
show "r" using 2 `q` by (rule mp)
qed
lemma ejercicio_4c:
assumes "p ⟶ q" and
"q ⟶ r"
shows "p ⟶ r"
proof (rule impI)
assume "p"
have "q" using assms(1) `p` ..
show "r" using assms(2) `q` ..
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)
------------------------------------------------------------------ *}
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
lemma ejercicio_5b:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof (rule impI)
assume "q"
show "p ⟶ r"
proof (rule impI)
assume "p"
have "q ⟶ r" using assms(1) `p` ..
thus "r" using `q` ..
qed
qed
lemma ejercicio_5c:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof (rule impI)
assume "q"
show "p ⟶ r"
proof
assume "p"
with assms(1) have "q ⟶ r" ..
thus "r" using `q` ..
qed
qed
lemma ejercicio_5d:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
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
lemma ejercicio_6b:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume "p"
with `p ⟶ q` have "q" ..
have "q ⟶ r" using assms(1) `p` ..
thus "r" using `q` ..
qed
qed
lemma ejercicio_6c:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}
lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
proof (rule impI)
assume "q"
show "p" using assms(1) by this
qed
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}
lemma ejercicio_8a:
"p ⟶ (q ⟶ p)"
proof (rule impI)
assume "p"
show "q ⟶ p"
proof (rule impI)
assume "q"
show "p" using `p` .
qed
qed
lemma ejercicio_8b:
"p ⟶ (q ⟶ p)"
by auto
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
lemma ejercicio_9a:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof (rule impI)
assume "q ⟶ r"
show "p ⟶ r"
proof (rule impI)
assume "p"
have "q" using assms(1) `p` ..
show "r" using `q ⟶ r` `q` ..
qed
qed
lemma ejercicio_9b:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}
lemma ejercicio_10a:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof (rule impI)
assume "r"
show "q ⟶ (p ⟶ s)"
proof (rule impI)
assume "q"
show "p ⟶ s"
proof (rule impI)
assume "p"
with assms(1) have "q ⟶ (r ⟶ s)" ..
hence "r ⟶ s" using `q` ..
thus "s" using `r` ..
qed
qed
qed
lemma ejercicio_10b:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}
lemma ejercicio_11a:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume "p"
have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p`..
have "q" using `p ⟶ q` `p` ..
show "r" using `q ⟶ r` `q` ..
qed
qed
qed
lemma ejercicio_11b:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume "p ⟶ (q ⟶ r)"
{assume "p ⟶ q"
{assume "p"
with `p ⟶ q` have "q" ..
have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` ..
hence "r" using `q` ..}
hence "p ⟶ r" ..}
thus "(p ⟶ q) ⟶ (p ⟶ r)" ..
qed
lemma ejercicio_11c:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
by auto
text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
lemma ejercicio_12a:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume "p"
show "q ⟶ r"
proof (rule impI)
assume "q"
show "r"
proof -
{assume "p"
have "q" using `q` .}
hence "p ⟶ q" ..
show "r" using assms(1) `p ⟶ q` ..
qed
qed
qed
lemma ejercicio_12b:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
{assume "q"
{assume "p"
have "q" using `q` .}
hence "p ⟶ q" ..
with assms(1) have "r" ..}
thus "q ⟶ r" ..
qed
lemma ejercicio_12c:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
using assms by auto
section {* Conjunciones *}
text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}
lemma ejercicio_13a:
assumes 1:"p" and
2:"q"
shows "p ∧ q"
proof -
show "p ∧ q" using 1 2 by (rule conjI)
qed
lemma ejercicio_13b:
assumes "p" and
"q"
shows "p ∧ q"
proof (rule conjI)
show "p" using assms(1) .
show "q" using assms(2) .
qed
lemma ejercicio_13c:
assumes "p" and
"q"
shows "p ∧ q"
using assms by auto
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_16a:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q)∧ r"
proof -
have 1: "p" using assms by (rule conjunct1)
have 2: "(q ∧ r)" using assms by (rule conjunct2)
have 3: "q" using 2 by (rule conjunct1)
have 4: "r" using 2 by (rule conjunct2)
have 5: "(p∧q)" using 1 3 by (rule conjI)
show "(p∧q) ∧ r" using 5 4 by (rule conjI)
qed
lemma ejercicio_16b:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q)∧ r"
proof (rule conjI)
show "p ∧ q"
proof (rule conjI)
show "p" using assms ..
next
have "q ∧ r" using assms ..
thus "q" ..
qed
next
have "q ∧ r" using assms ..
thus "r" ..
qed
lemma ejercicio_16c:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q)∧ r"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
lemma ejercicio_17a:
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 "p∧(q∧r)" using 3 5 by (rule conjI)
qed
lemma ejercicio_17b:
assumes "(p∧ q) ∧ r"
shows "p ∧ (q∧ r)"
proof (rule conjI)
have "p ∧ q" using assms ..
thus "p" ..
next
show "q ∧ r"
proof (rule conjI)
have "p ∧ q" using assms ..
thus "q" ..
next
show "r" using assms ..
qed
qed
lemma ejercicio_17c:
assumes "(p∧ q) ∧ r"
shows "p ∧ (q∧ r)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ejercicio_18a:
assumes "p ∧ q"
shows "p ⟶ q"
proof -
have 1: "q" using assms by (rule conjunct2)
show "p⟶ q" using 1 by (rule impI)
qed
lemma ejercicio_18b:
assumes "p ∧ q"
shows "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using assms ..
qed
lemma ejercicio_18c:
assumes "p ∧ q"
shows "p ⟶ q"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}
lemma ejercicio_19a:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof (rule impI)
assume "p"
show "q ∧ r"
proof (rule conjI)
have "p ⟶ q" using assms ..
thus "q" using `p` ..
have "p ⟶ r" using assms ..
thus "r" using `p` ..
qed
qed
lemma ejercicio_19c:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}
lemma ejercicio_20a:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
show "p ⟶ q"
proof (rule impI)
assume "p"
with `p ⟶ q ∧ r` have "q ∧ r" ..
thus "q" ..
qed
show "p ⟶ r"
proof (rule impI)
assume "p"
with `p ⟶ q ∧ r` have "q ∧ r" ..
thus "r" ..
qed
qed
lemma ejercicio_20c:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
lemma ejercicio_21a:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
using assms by auto
lemma ejercicio_21b:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume "p ∧ q"
hence "p" ..
with `p ⟶ (q ⟶ r)` have "q ⟶ r" ..
have "q" using `p ∧ q` ..
with `q ⟶ r` show "r" ..
qed
lemma ejercicio_21c:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume "p ∧ q"
hence "p" ..
have "q" using `p ∧ q`..
have "q ⟶ r" using assms(1) `p` ..
thus "r" using `q` ..
qed
text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
lemma ejercicio_22a:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume "p"
show "q ⟶ r"
proof (rule impI)
assume "q"
with `p` have "p ∧ q" ..
with assms(1) show "r" ..
qed
qed
lemma ejercicio_22c:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
lemma ejercicio_23a:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume "p ∧ q"
hence "q" ..
have "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using `q` .
qed
with assms(1) show "r" ..
qed
lemma ejercicio_23c:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
lemma ejercicio_24b:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof (rule impI)
assume "p ⟶ q"
have "p" using assms(1) ..
with `p ⟶ q` have "q" ..
have "q ⟶ r" using assms(1) ..
thus "r" using `q` ..
qed
lemma ejercicio_24c:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
using assms by auto
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_27a:
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
lemma ejercicio_27b:
assumes "p ∨ q"
shows "q ∨ p"
proof -
note `p ∨ q`
moreover
{ assume "p"
hence "q ∨ p" ..}
moreover
{ assume "q"
hence "q ∨ p" .. }
ultimately show "q ∨ p" ..
qed
lemma ejercicio_27c:
assumes "p ∨ q"
shows "q ∨ p"
using assms
proof (rule disjE)
assume "p"
thus "q ∨ p" ..
next
assume "q"
thus "q ∨ p" ..
qed
lemma ejercicio_27d:
assumes "p ∨ q"
shows "q ∨ p"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}
lemma ejercicio_28b:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
assume "p ∨ q"
show "p ∨ r"
using `p ∨ q`
proof (rule disjE)
assume "p"
thus "p ∨ r" ..
next
assume "q"
with assms(1) have "r" ..
thus "p ∨ r" ..
qed
qed
lemma ejercicio_28c:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}
lemma ejercicio_29b:
assumes "p ∨ p"
shows "p"
using assms
proof (rule disjE)
assume "p"
thus "p" .
next
assume "p"
thus "p" .
qed
lemma ejercicio_29c:
assumes "p ∨ p"
shows "p"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
lemma ejercicio_30a:
assumes "p"
shows "p ∨ p"
using assms
proof (rule disjI1)
qed
lemma ejercicio_30b:
assumes "p"
shows "p ∨ p"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}
lemma ejercicio_31a:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
using assms
proof (rule disjE)
assume "p"
hence "p ∨ q" by (rule disjI1)
thus "(p ∨ q) ∨ r" by (rule disjI1)
next
assume "q ∨ r"
thus "(p ∨ q) ∨ r"
proof (rule disjE)
assume "q"
hence "p ∨ q" by (rule disjI2)
thus "(p ∨ q) ∨ r" by (rule disjI1)
next
assume "r"
thus "(p ∨ q) ∨ r" by (rule disjI2)
qed
qed
lemma ejercicio_31b:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
using assms by auto
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_34a:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
using assms
proof
assume "p∧q"
show "p ∧ (q ∨ r)"
proof (rule conjI)
show "p" using `p∧q` ..
next
have "q" using `p∧q` ..
thus "q∨r" by (rule disjI1)
qed
next
assume "p∧r"
show "p ∧ (q ∨ r)"
proof (rule conjI)
show "p" using `p∧r` ..
next
have "r" using `p∧r` ..
thus "q∨r" by (rule disjI2)
qed
qed
lemma ejercicio_34b:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
using assms by auto
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_36a:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have "p ∨ q" using assms ..
thus "p ∨ (q ∧ r)"
proof
assume "p"
thus "p ∨ (q ∧ r)" by (rule disjI1)
next
assume "q"
have "p ∨ r" using assms ..
thus "p ∨ (q ∧ r)"
proof
assume "p"
thus "p ∨ (q∧r)" by (rule disjI1)
next
assume "r"
with `q` have "q ∧ r" ..
thus "p ∨ (q ∧ r)" by (rule disjI2)
qed
qed
qed
lemma ejercicio_36b:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}
lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof (rule impI)
assume "p ∨ q"
thus "r"
proof
assume "p"
have "p ⟶ r" using assms by (rule conjunct1)
thus "r" using `p` ..
next
assume "q"
have "q ⟶ r" using assms by (rule conjunct2)
thus "r" using `q` ..
qed
qed
lemma ejercicio_37b:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}
lemma ejercicio_38a:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof (rule conjI)
show "p ⟶ r"
proof (rule impI)
assume "p"
hence "p ∨ q" ..
with assms show "r" by (rule mp)
qed
next
show "q ⟶ r"
proof (rule impI)
assume "q"
hence "p ∨ q" ..
with assms show "r" by (rule mp)
qed
qed
lemma ejercicio_38b:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
using assms by auto
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_40a:
assumes "¬p"
shows "p ⟶ q"
proof
assume "p"
with assms show "q" by (rule notE)
qed
lemma ejercicio_40b:
assumes "¬p"
shows "p ⟶ q"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}
lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof
assume "¬q"
with assms show "¬p" by (rule mt)
qed
lemma ejercicio_41b:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}
lemma ejercicio_42a:
assumes "p∨q"
"¬q"
shows "p"
using assms(1)
proof
assume "p" thus "p" .
next
assume "q"
with assms(2) show "p" by (rule notE)
qed
lemma ejercicio_42b:
assumes "p∨q"
"¬q"
shows "p"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}
lemma ejercicio_43a:
assumes "p ∨ q"
"¬p"
shows "q"
using assms(1)
proof
assume "p"
with assms(2) show "q" by (rule notE)
next
assume "q" thus q .
qed
lemma ejercicio_43b:
assumes "p ∨ q"
"¬p"
shows "q"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}
lemma ejercicio_44a:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
using assms
proof
assume "p"
show "¬(¬p ∧ ¬q)"
proof (rule notI)
assume "¬p ∧ ¬q"
hence "¬p" by (rule conjunct1)
thus False using `p` by (rule notE)
qed
next
assume "q"
show "¬(¬p ∧ ¬q)"
proof (rule notI)
assume "¬p ∧ ¬q"
hence "¬q" by (rule conjunct2)
thus False using `q` by (rule notE)
qed
qed
lemma ejercicio_44b:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof (rule notI)
assume "¬p ∧ ¬q"
show False using assms
proof (rule disjE)
assume "p"
have "¬p" using `¬p ∧ ¬q` by (rule conjunct1)
thus False using `p` by (rule notE)
next
assume "q"
have "¬q" using `¬p ∧ ¬q` by (rule conjunct2)
thus False using `q` by (rule notE)
qed
qed
lemma ejercicio_44c:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}
lemma ejercicio_45a:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof
assume "¬p ∨ ¬q"
thus False
proof (rule disjE)
assume "¬p"
have "p" using assms ..
with `¬ p` show False ..
next
assume "¬q"
have "q" using assms by (rule conjunct2)
with `¬ q` show False by (rule notE)
qed
qed
lemma ejercicio_45c:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}
lemma ejercicio_46a:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
show "¬p"
proof
assume "p"
hence "p ∨ q" by (rule disjI1)
with assms show False by (rule notE)
qed
next
show "¬q"
proof
assume "q"
hence "p ∨ q" ..
with assms show False ..
qed
qed
lemma ejercicio_46c:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}
lemma ejercicio_47a:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume "p ∨ q"
thus False
proof
assume "p"
have "¬p" using assms by (rule conjunct1)
thus False using `p` by (rule notE)
next
assume "q"
have "¬q" using assms by (rule conjunct2)
thus False using `q` by (rule notE)
qed
qed
lemma ejercicio_47c:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}
lemma ejercicio_48a:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
using assms
proof
assume "¬p"
show "¬(p ∧ q)"
proof
assume "p ∧ q"
hence "p" by (rule conjunct1)
with `¬p` show False by (rule notE)
qed
next
assume "¬q"
show "¬(p ∧ q)"
proof
assume "p ∧ q"
hence "q" ..
with `¬q` show False ..
qed
qed
lemma ejercicio_48b:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof
assume "p ∧ q"
show False
using assms
proof
assume "¬p"
have "p" using `p ∧ q` ..
with `¬p` show False ..
next
assume "¬q"
have "q" using `p ∧ q` ..
with `¬q` show False ..
qed
qed
lemma ejercicio_48c:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}
lemma ejercicio_49a:
"¬(p ∧ ¬p)"
proof
assume "p ∧ ¬p"
hence "p" ..
have "¬ p" using `p ∧ ¬p` ..
thus False using `p` ..
qed
lemma ejercicio_49b:
"¬(p ∧ ¬p)"
by auto
text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}
lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
oops
text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}
lemma ejercicio_51a:
assumes "¬¬p"
shows "p"
using assms by (rule notnotD)
lemma ejercicio_51b:
assumes "¬¬p"
shows "p"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}
lemma ejercicio_52a:
"p ∨ ¬p"
proof -
have "¬¬p ∨ ¬p" ..
thus "p ∨ ¬p" by simp
qed
lemma ejercicio_52b:
"p ∨ ¬p"
proof -
have "¬p ∨ p" ..
thus "p ∨ ¬p" by (rule ejercicio_27a)
qed
lemma ejercicio_52c:
"p ∨ ¬p"
by auto
text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}
lemma ejercicio_53b:
"((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
assume "(p ⟶ q) ⟶ p"
show "p"
proof (rule ccontr)
assume "¬p"
have "¬ (p ⟶ q)" using `(p ⟶ q) ⟶ p` `¬p` by (rule mt)
have "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using `¬p` `p` by (rule notE)
qed
show False using `¬ (p ⟶ q)` `p ⟶ q` ..
qed
qed
lemma ejercicio_53a:
"((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
assume "(p ⟶ q) ⟶ p"
have "¬p ∨ p" by (rule excluded_middle)
thus "p"
proof (rule disjE)
{assume "¬p"
have "¬(p⟶ q)" using `(p ⟶ q) ⟶ p` `¬p` by (rule mt)
have "p⟶ q"
proof (rule impI)
assume "p"
show "q" using `¬p``p` by (rule notE)
qed
show "p" using `¬(p⟶ q)` `p⟶ q` by (rule notE)
}
next
{assume "p"
thus "p" .
}
qed
qed
lemma ejercicio_53c:
"((p ⟶ q) ⟶ p) ⟶ p"
by auto
text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
hence "¬¬p" by (rule notnotI)
with assms have "¬¬q" by (rule mt)
thus "q" by (rule notnotD)
qed
text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}
lemma ejercicio_55a:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
have "¬p ∨ p" ..
thus "p∨q"
proof
assume "¬p"
have "¬q ∨ q" ..
thus "p∨q"
proof
assume "¬q"
with `¬p` have "¬p ∧ ¬q" by (rule conjI)
with assms show "p∨q" by (rule notE)
next
assume "q"
thus "p ∨ q" ..
qed
next
assume "p"
thus "p ∨q" ..
qed
qed
lemma ejercicio_55c:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
lemma ejercicio_56a:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
show "p"
proof -
have "¬p ∨ p" ..
thus "p"
proof
assume "¬p"
hence "¬p ∨ ¬q" by (rule disjI1)
with `¬(¬p ∨ ¬q)` show "p" by (rule notE)
next
assume "p" thus "p" .
qed
qed
next
show "q"
proof -
have "¬q ∨ q" ..
thus "q"
proof
assume "¬q"
hence "¬p ∨ ¬q" by (rule disjI2)
with `¬(¬p ∨ ¬q)` show "q" by (rule notE)
next
assume "q" thus "q" .
qed
qed
qed
lemma ejercicio_56c:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}
lemma ejercicio_57a:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have "¬p ∨p" ..
thus "¬p ∨ ¬q"
proof
assume "¬p"
thus "¬p ∨ ¬q" ..
next
assume "p"
have "¬q ∨ q" ..
thus "¬p ∨ ¬q"
proof
assume "¬q"
thus "¬p ∨ ¬q" ..
next
assume "q"
with `p` have "p∧q" by (rule conjI)
with assms show "¬p ∨ ¬q" by (rule notE)
qed
qed
qed
lemma ejercicio_57c:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
using assms by auto
text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
lemma ejercicio_58a:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "(p ⟶ q) ∨ (q ⟶ p)"
proof
assume "¬p"
show "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjI1)
show "p ⟶ q"
proof
assume "p"
with `¬ p` show "q" by (rule notE)
qed
qed
next
assume "p"
show "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjI2)
show "q ⟶ p"
proof (rule impI)
assume "q"
show "p" using `p` .
qed
qed
qed
qed
lemma ejercicio_58b:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" .. (* by (rule excluded_middle) *)
thus "(p ⟶ q) ∨ (q ⟶ p)"
proof
assume "¬p"
show "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjI1)
show "p ⟶ q"
proof
assume "p"
with `¬ p` show "q" .. (* by (rule notE) *)
qed
qed
next
assume "p"
show "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjI2)
show "q ⟶ p"
proof (* (rule impI) *)
assume "q"
show "p" using `p` .
qed
qed
qed
qed
lemma ejercicio_58c:
"(p ⟶ q) ∨ (q ⟶ p)"
by auto
lemma ej_59: assumes "p ∧ ¬(q ⟶ r)"
shows "(p ∧ q) ∧ ¬r"
proof
show "p ∧ q"
proof
show "p" using assms by (rule conjunct1)
next
show "q"
proof (rule ccontr)
assume "¬q"
have "¬(q ⟶ r)" using assms ..
have "q ⟶ r"
proof
assume "q"
with `¬q` show "r" by (rule notE)
qed
with `¬(q ⟶ r)` show False ..
qed
qed
next
show "¬r"
proof
assume "r"
have "q ⟶ r"
proof
assume "q" show "r" using `r` .
qed
have "¬(q ⟶ r)" using assms ..
thus False using `q ⟶ r` ..
qed
qed
lemma ej_60: "¬(s ∨ (p ⟶ q)) ⟶ p ∧ ¬q ∧ ¬s"
proof
assume 1:"¬(s ∨ (p ⟶ q))"
show "p ∧ ¬q ∧ ¬s"
proof
show "p"
proof (rule ccontr)
assume "¬p"
have "p ⟶q"
proof
assume "p" with `¬p` show "q" by (rule notE)
qed
hence "s ∨ (p ⟶ q)" ..
with 1 show False ..
qed
next
show "¬q ∧ ¬s"
proof
show "¬q"
proof
assume "q"
have "p ⟶ q"
proof
assume "p" show "q" using `q` by this
qed
hence "s ∨ (p ⟶ q)" ..
with 1 show False ..
qed
next
show "¬s"
proof
assume "s"
hence "s ∨ (p ⟶ q)" ..
with 1 show False ..
qed
qed
qed
qed
lemma ejercicio_70:
assumes "p ∧ q ⟶ r ∨ s"
"q ⟶ ¬s"
shows "p ⟶ ¬q ∨ r"
proof
assume "p"
show "¬q ∨ r"
proof-
have "¬q ∨ q" ..
thus "¬q ∨ r"
proof (rule disjE)
assume "¬q"
thus "¬q ∨ r" ..
next
assume "q"
with `p` have "p ∧ q" ..
with assms(1) have "r ∨ s" ..
thus "¬q ∨ r"
proof (rule disjE)
assume "r" thus "¬q ∨ r" ..
next
assume "s"
hence "¬¬s" by (rule notnotI)
with assms(2) have "¬q" by (rule mt)
thus "¬q ∨ r" ..
qed
qed
qed
qed
lemma ejercicio_71:
assumes "∀x. (P(x) ⟶ Q(x))"
"∀x. (¬S(x) ⟶ ¬Q(x))"
"¬ (∀x. S(x))"
shows "∃x. ¬P(x)"
proof (rule ccontr)
assume 3: "¬ (∃x. ¬ P x)"
have "∀x. S(x)"
proof
fix a
show "S(a)"
proof (rule ccontr)
assume 1:"¬ S a"
have "¬S(a) ⟶ ¬Q(a)" using assms(2) by (rule allE)
hence 2:"¬Q(a)" using 1 ..
have "P(a) ⟶ Q(a)" using assms(1) ..
hence "¬P(a)" using 2 by (rule mt)
hence "∃x. ¬P(x)" ..
with 3 show False ..
qed
qed
with assms(3) show False ..
qed
end
