chapter ‹ R3: Deducción natural proposicional(II) ›
theory R3_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 los método simp ni auto).
Para cada ejercicio dar una demostración estructurada y otra
aplicativa.
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 ‹ 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
lemma ej25: "p ⟹ p ∨ q"
apply (erule disjI1)
done
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
lemma ej26: "q ⟹ p ∨ q"
apply (erule disjI2)
done
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"
then have "q ∨ p" ..}
moreover
{ assume "q"
then have "q ∨ p" .. }
ultimately show "q ∨ p" ..
qed
lemma ejercicio_27c:
assumes "p ∨ q"
shows "q ∨ p"
using assms
proof (rule disjE)
assume "p"
then show "q ∨ p" ..
next
assume "q"
then show "q ∨ p" ..
qed
lemma ejercicio_27d:
assumes "p ∨ q"
shows "q ∨ p"
using assms by auto
lemma ej27: "p ∨ q ⟹ q ∨ p"
apply (erule disjE)
apply (erule disjI2)
apply (erule disjI1)
done
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"
then show "p ∨ r" ..
next
assume "q"
with assms(1) have "r" ..
then show "p ∨ r" ..
qed
qed
lemma ejercicio_28c:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
using assms by auto
lemma ej28: "q ⟶ r ⟹ p ∨ q ⟶ p ∨ r"
apply (rule impI)
apply (erule disjE)
apply (erule disjI1)
apply (drule mp)
apply assumption
apply (erule disjI2)
done
text ‹ ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ ›
lemma ejercicio_29b:
assumes "p ∨ p"
shows "p"
using assms
proof (rule disjE)
assume "p"
then show "p" .
next
assume "p"
then show "p" .
qed
lemma ejercicio_29c:
assumes "p ∨ p"
shows "p"
using assms by auto
lemma ej29: "p ∨ p ⟹ p"
apply (erule disjE)
apply assumption+
done
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
lemma ej30: "p ⟹ p ∨ p"
apply (erule disjI1)
done
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"
then have "p ∨ q" by (rule disjI1)
then show "(p ∨ q) ∨ r" by (rule disjI1)
next
assume "q ∨ r"
then show "(p ∨ q) ∨ r"
proof (rule disjE)
assume "q"
then have "p ∨ q" by (rule disjI2)
then show "(p ∨ q) ∨ r" by (rule disjI1)
next
assume "r"
then show "(p ∨ q) ∨ r" by (rule disjI2)
qed
qed
lemma ejercicio_31b:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
using assms by auto
lemma ej31: "p ∨ (q ∨ r) ⟹ (p ∨ q) ∨ r"
apply (erule disjE)
apply (rule disjI1)
apply (erule disjI1)
apply (erule disjE)
apply (rule disjI1)
apply (erule disjI2)
apply (erule disjI2)
done
text ‹ ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ ›
lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
oops
lemma ejercicio_32b:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using ‹(p ∨ q) ∨ r›
proof (rule disjE)
assume "p ∨ q"
then show "p ∨ (q ∨ r)"
proof (rule disjE)
assume "p"
then show "p ∨ (q ∨ r)" by (rule disjI1)
next
assume "q"
then have "q ∨ r" by (rule disjI1)
then show "p ∨ (q ∨ r)" by (rule disjI2)
qed
next
assume "r"
then have "q ∨ r" by (rule disjI2)
then show "p ∨ (q ∨ r)" by (rule disjI2)
qed
lemma ej32: "(p ∨ q) ∨ r ⟹ p ∨ (q ∨ r)"
apply (erule disjE)
apply (erule disjE)
apply (erule disjI1)
apply (rule disjI2)
apply (erule disjI1)
apply (rule disjI2)
apply (erule disjI2)
done
text ‹ ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ ›
lemma ejercicio_33:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
oops
lemma ejercicio_33b:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof-
have "p" using ‹p ∧ (q ∨ r)› by (rule conjunct1)
show "(p ∧ q) ∨ (p ∧ r)"
proof (rule disjE)
assume "q"
have "p ∧ q" using ‹p› ‹q› by (rule conjI)
then show "(p ∧ q) ∨ (p ∧ r)" by (rule disjI1)
next
assume "r"
have "p ∧ r" using ‹p› ‹r› by (rule conjI)
then show "(p ∧ q) ∨ (p ∧ r)" by (rule disjI2)
next
show "q ∨ r" using ‹p ∧ (q ∨ r)› by (rule conjunct2)
qed
qed
lemma ej33: "p ∧ (q ∨ r) ⟹ (p ∧ q) ∨ (p ∧ r)"
apply (erule conjE)
apply (erule disjE)
apply (rule disjI1)
apply (rule conjI)
apply assumption
apply assumption
apply (rule disjI2)
apply (rule conjI)
apply assumption
apply assumption
done
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` ..
then show "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` ..
then show "q∨r" by (rule disjI2)
qed
qed
lemma ejercicio_34b:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
using assms by auto
lemma ej34: "(p ∧ q) ∨ (p ∧ r) ⟹ p ∧ (q ∨ r)"
apply (rule conjI)
apply (erule disjE)
apply (erule conjunct1)
apply (erule conjunct1)
apply (erule disjE)
apply (erule conjE)
apply (rule disjI1)
apply assumption
apply (erule conjE)
apply (erule disjI2)
done
text ‹ ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ ›
lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
oops
lemma ejercicio_35b:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
using ‹p ∨ (q ∧ r)›
proof (rule disjE)
assume "p"
then have "p ∨ r" by (rule disjI1)
have "p ∨ q" using ‹p› by (rule disjI1)
then show "(p ∨ q) ∧ (p ∨ r)" using ‹p ∨ r› by (rule conjI)
next
assume "q ∧ r"
then have "r" by (rule conjunct2)
then have "p ∨ r" by (rule disjI2)
have "q" using ‹q ∧ r› by (rule conjunct1)
then have "p ∨ q" by (rule disjI2)
then show "(p ∨ q) ∧ (p ∨ r)" using ‹p ∨ r› by (rule conjI)
qed
lemma ej35: "p ∨ (q ∧ r) ⟹ (p ∨ q) ∧ (p ∨ r)"
apply (erule disjE)
apply (rule conjI)
apply (erule disjI1)
apply (erule disjI1)
apply (erule conjE)
apply (rule conjI)
apply (erule disjI2)
apply (erule disjI2)
done
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 ..
then show "p ∨ (q ∧ r)"
proof
assume "p"
then show "p ∨ (q ∧ r)" by (rule disjI1)
next
assume "q"
have "p ∨ r" using assms ..
then show "p ∨ (q ∧ r)"
proof
assume "p"
then show "p ∨ (q∧r)" by (rule disjI1)
next
assume "r"
with `q` have "q ∧ r" ..
then show "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
lemma ej36: "(p ∨ q) ∧ (p ∨ r) ⟹ p ∨ (q ∧ r)"
apply (erule conjE)
apply (erule disjE)
apply (erule disjI1)
apply (erule disjE)
apply (erule disjI1)
apply (rule disjI2)
apply (rule conjI)
apply assumption+
done
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"
then show "r"
proof
assume "p"
have "p ⟶ r" using assms by (rule conjunct1)
then show "r" using `p` ..
next
assume "q"
have "q ⟶ r" using assms by (rule conjunct2)
then show "r" using `q` ..
qed
qed
lemma ejercicio_37b:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
using assms by auto
lemma ej37: "(p ⟶ r) ∧ (q ⟶ r) ⟹ p ∨ q ⟶ r"
apply (rule impI)
apply (erule conjE)
apply (erule disjE)
apply (drule mp, assumption+)+
done
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"
then have "p ∨ q" ..
with assms show "r" by (rule mp)
qed
next
show "q ⟶ r"
proof (rule impI)
assume "q"
then have "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
lemma ej38: "p ∨ q ⟶ r ⟹ (p ⟶ r) ∧ (q ⟶ r)"
apply (rule conjI)
apply (rule impI)
apply (drule mp)
apply (erule disjI1)
apply assumption
apply (rule impI)
apply (drule mp)
apply (erule disjI2)
apply assumption
done
section ‹ Negaciones ›
text ‹ ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ ›
lemma ejercicio_39:
assumes "p"
shows "¬¬p"
proof -
show "¬¬p" using assms by (rule notnotI)
qed
lemma ej39: "p ⟹ ¬¬p"
apply (rule notI)
apply (erule notE)
apply assumption
done
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
lemma ej40: "¬p ⟹ p ⟶ q"
apply (rule impI)
apply (erule notE)
apply assumption
done
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
lemma ej41: "p ⟶ q ⟹ ¬q ⟶ ¬p"
apply (rule impI)
apply (rule notI)
apply (erule impE)
apply assumption
apply (erule notE)
apply assumption
done
text ‹ ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ ›
lemma ejercicio_42a:
assumes "p∨q"
"¬q"
shows "p"
using assms(1)
proof
assume "p" then show "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
lemma ej42: "⟦p ∨ q; ¬q⟧ ⟹ p"
apply (erule disjE)
apply assumption
apply (erule notE)
apply assumption
done
text ‹ ---------------------------------------------------------------
Ejercicio 43. 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" then show q .
qed
lemma ejercicio_43b:
assumes "p ∨ q"
"¬p"
shows "q"
using assms by auto
lemma ej43: "⟦p ∨ q; ¬p⟧ ⟹ q"
apply (erule disjE)
apply (erule notE)
apply assumption
apply assumption
done
text ‹ ---------------------------------------------------------------
Ejercicio 44. 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"
then have "¬p" by (rule conjunct1)
then show False using `p` by (rule notE)
qed
next
assume "q"
show "¬(¬p ∧ ¬q)"
proof (rule notI)
assume "¬p ∧ ¬q"
then have "¬q" by (rule conjunct2)
then show 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)
then show False using `p` by (rule notE)
next
assume "q"
have "¬q" using `¬p ∧ ¬q` by (rule conjunct2)
then show False using `q` by (rule notE)
qed
qed
lemma ejercicio_44c:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
using assms by auto
lemma ej44: "p ∨ q ⟹ ¬(¬p ∧ ¬q)"
apply (rule notI)
apply (erule conjE)
apply (erule disjE)
apply (erule notE, assumption)+
done
text ‹ ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ ›
lemma ejercicio_45a:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof
assume "¬p ∨ ¬q"
then show 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
lemma ej45: "p ∧ q ⟹ ¬(¬p ∨ ¬q)"
apply (rule notI)
apply (erule conjE)
apply (erule disjE)
apply (erule notE, assumption)+
done
text ‹ ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ ›
lemma ejercicio_46a:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
show "¬p"
proof
assume "p"
then have "p ∨ q" by (rule disjI1)
with assms show False by (rule notE)
qed
next
show "¬q"
proof
assume "q"
then have "p ∨ q" ..
with assms show False ..
qed
qed
lemma ejercicio_46c:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
using assms by auto
lemma ej46: "¬(p ∨ q) ⟹ ¬p ∧ ¬q"
apply (rule conjI)
apply (rule notI)
apply (erule notE)
apply (erule disjI1)
apply (rule notI)
apply (erule notE)
apply (erule disjI2)
done
text ‹ ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ ›
lemma ejercicio_47a:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume "p ∨ q"
then show False
proof
assume "p"
have "¬p" using assms by (rule conjunct1)
then show False using `p` by (rule notE)
next
assume "q"
have "¬q" using assms by (rule conjunct2)
then show False using `q` by (rule notE)
qed
qed
lemma ejercicio_47c:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
using assms by auto
lemma ej47: "¬p ∧ ¬q ⟹ ¬(p ∨ q)"
apply (rule notI)
apply (erule conjE)
apply (erule disjE)
apply (erule notE, assumption)+
done
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"
then have "p" by (rule conjunct1)
with `¬p` show False by (rule notE)
qed
next
assume "¬q"
show "¬(p ∧ q)"
proof
assume "p ∧ q"
then have "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
lemma ej48: "¬p ∨ ¬q ⟹ ¬(p ∧ q)"
apply (rule notI)
apply (erule conjE)
apply (erule disjE)
apply (erule notE, assumption)+
done
text ‹ ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ ›
lemma ejercicio_49a:
"¬(p ∧ ¬p)"
proof
assume "p ∧ ¬p"
then have "p" ..
have "¬ p" using `p ∧ ¬p` ..
then show False using `p` ..
qed
lemma ejercicio_49b:
"¬(p ∧ ¬p)"
by auto
lemma ej49: "¬(p ∧ ¬p)"
apply (rule notI)
apply (erule conjE)
apply (erule notE)
apply assumption
done
text ‹ ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ ›
lemma ejercicio_50:
assumes 1: "p ∧ ¬p"
shows "q"
proof-
have 2: "p" using 1 by (rule conjunct1)
have 3: "¬p" using 1 by (rule conjunct2)
have 4: "False" using 3 2 by (rule notE)
show "q" using 4 by (rule FalseE)
qed
lemma ejercicio_50b:
assumes "p ∧ ¬p"
shows "q"
proof (rule notE)
show "p" using ‹p ∧ ¬p› by (rule conjunct1)
show "¬p" using ‹p ∧ ¬p› by (rule conjunct2)
qed
lemma ej50: "p ∧ ¬p ⟹ q"
apply (erule conjE)
apply (erule notE)
apply assumption
done
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
lemma ej51: "¬¬p ⟹ p"
apply (erule notnotD)
done
text ‹ ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ ›
lemma ejercicio_52a:
"p ∨ ¬p"
proof -
have "¬¬p ∨ ¬p" ..
then show "p ∨ ¬p" by simp
qed
lemma ejercicio_52b:
"p ∨ ¬p"
proof -
have "¬p ∨ p" ..
then show "p ∨ ¬p" by (rule ejercicio_27a)
qed
lemma ejercicio_52c:
"p ∨ ¬p"
by auto
lemma ej52: "p ∨ ¬p"
apply (cut_tac P="¬p" in excluded_middle)
apply (erule disjE)
apply (rule disjI1)
apply (erule notnotD)
apply (erule disjI2)
done
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)
then show "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"
then show "p" .
qed
qed
lemma ejercicio_53c:
"((p ⟶ q) ⟶ p) ⟶ p"
by auto
lemma ej53: "((p ⟶ q) ⟶ p) ⟶ p"
apply (rule impI)
apply (rule ccontr)
(* apply (case_tac "p ⟶ q") *)
apply (cut_tac P="p ⟶ q" in excluded_middle)
apply (erule disjE)
apply (erule_tac P="p ⟶ q" in notE)
apply (rule impI)
apply (erule notE)
apply assumption
apply (erule impE)
apply assumption
apply (erule notE)
apply assumption
done
text ‹ ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ ›
lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
then have "¬¬p" by (rule notnotI)
with assms have "¬¬q" by (rule mt)
then show "q" by (rule notnotD)
qed
lemma ej54: "¬q ⟶ ¬p ⟹ p ⟶ q"
apply (rule impI)
apply (rule ccontr)
apply (erule impE)
apply assumption
apply (erule notE)+
apply assumption
done
text ‹ ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ ›
lemma ejercicio_55a:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
have "¬p ∨ p" ..
then show "p∨q"
proof
assume "¬p"
have "¬q ∨ q" ..
then show "p∨q"
proof
assume "¬q"
with `¬p` have "¬p ∧ ¬q" by (rule conjI)
with assms show "p∨q" by (rule notE)
next
assume "q"
then show "p ∨ q" ..
qed
next
assume "p"
then show "p ∨q" ..
qed
qed
lemma ejercicio_55c:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
using assms by auto
lemma ej55: "¬(¬p ∧ ¬q) ⟹ p ∨ q"
apply (cut_tac P=p in excluded_middle)
apply (erule disjE)
apply (cut_tac P=q in excluded_middle)
apply (erule disjE)
apply (erule notE)
apply (rule conjI)
apply assumption+
apply (erule disjI2)
apply (erule disjI1)
done
text ‹ ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ ›
lemma ejercicio_56a:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
show "p"
proof -
have "¬p ∨ p" ..
then show "p"
proof
assume "¬p"
then have "¬p ∨ ¬q" by (rule disjI1)
with `¬(¬p ∨ ¬q)` show "p" by (rule notE)
next
assume "p" then show "p" .
qed
qed
next
show "q"
proof -
have "¬q ∨ q" ..
then show "q"
proof
assume "¬q"
then have "¬p ∨ ¬q" by (rule disjI2)
with `¬(¬p ∨ ¬q)` show "q" by (rule notE)
next
assume "q" then show "q" .
qed
qed
qed
lemma ejercicio_56c:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
using assms by auto
lemma ej56: "¬(¬p ∨ ¬q) ⟹ p ∧ q"
apply (rule conjI)
apply (rule ccontr)
apply (erule notE)
apply (erule disjI1)
apply (rule ccontr)
apply (erule notE)
apply (erule disjI2)
done
text ‹ ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ ›
lemma ejercicio_57a:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have "¬p ∨p" ..
then show "¬p ∨ ¬q"
proof
assume "¬p"
then show "¬p ∨ ¬q" ..
next
assume "p"
have "¬q ∨ q" ..
then show "¬p ∨ ¬q"
proof
assume "¬q"
then show "¬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
lemma ej57: "¬(p ∧ q) ⟹ ¬p ∨ ¬q"
apply (cut_tac P=p in excluded_middle)
apply (erule disjE)
apply (erule disjI1)
apply (cut_tac P=q in excluded_middle)
apply (erule disjE)
apply (erule disjI2)
apply (erule notE)
apply (rule conjI)
apply assumption+
done
lemma ej57_b:
"⟦¬(p ∧ q)⟧ ⟹ ¬p ∨ ¬q"
apply (rule ccontr)
apply (erule notE)
apply (rule conjI)
apply (rule ccontr)
apply (erule notE)
apply (rule disjI1)
apply assumption
apply (rule ccontr)
apply (erule notE)
apply (rule disjI2)
apply assumption
done
text ‹ ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------
›
lemma ejercicio_58a:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" by (rule excluded_middle)
then show "(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) *)
then show "(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 ej58: "(p ⟶ q) ∨ (q ⟶ p)"
apply (cut_tac P=p in excluded_middle)
apply (erule disjE)
apply (rule disjI1)
apply (rule impI)
apply (erule notE)
apply assumption
apply (rule disjI2)
apply (rule impI)
apply assumption
done
end
![Lógica matemática y fundamentos [Curso 2019-20]](/~jalonso/imagenes/logoUS.jpg)