https://www.glc.us.es/~jalonso/RA2019/index.php?action=history&feed=atom&title=R7
R7 - Historial de revisiones
2026-07-18T14:25:51Z
Historial de revisiones de esta página en el wiki
MediaWiki 1.36.1
https://www.glc.us.es/~jalonso/RA2019/index.php?title=R7&diff=626&oldid=prev
Jalonso: Protegió «R7» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))
2019-12-19T09:16:58Z
<p>Protegió «<a href="/~jalonso/RA2019/index.php/R7" title="R7">R7</a>» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))</p>
<table style="background-color: #fff; color: #202122;" data-mw="interface">
<tr class="diff-title" lang="es">
<td colspan="1" style="background-color: #fff; color: #202122; text-align: center;">← Revisión anterior</td>
<td colspan="1" style="background-color: #fff; color: #202122; text-align: center;">Revisión del 09:16 19 dic 2019</td>
</tr><tr><td colspan="2" class="diff-notice" lang="es"><div class="mw-diff-empty">(Sin diferencias)</div>
</td></tr></table>
Jalonso
https://www.glc.us.es/~jalonso/RA2019/index.php?title=R7&diff=625&oldid=prev
Jalonso: Página creada con «<source lang="isabelle"> chapter ‹R7: Deducción natural proposicional› theory R7_Deduccion_natural_proposicional_2 imports Main begin text ‹----------------------…»
2019-12-19T09:16:45Z
<p>Página creada con «<source lang="isabelle"> chapter ‹R7: Deducción natural proposicional› theory R7_Deduccion_natural_proposicional_2 imports Main begin text ‹----------------------…»</p>
<p><b>Página nueva</b></p><div><source lang="isabelle"><br />
chapter ‹R7: Deducción natural proposicional›<br />
<br />
theory R7_Deduccion_natural_proposicional_2<br />
imports Main <br />
begin<br />
<br />
text ‹------------------------------------------------------------------ <br />
El objetivo de esta relación es demostrar cada uno de los ejercicios<br />
usando sólo las reglas básicas de deducción natural de la lógica<br />
proposicional (sin usar los método simp ni auto).<br />
<br />
Para cada ejercicio dar una demostración estructurada y otra<br />
aplicativa.<br />
<br />
Las reglas básicas de la deducción natural son las siguientes:<br />
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q<br />
· conjunct1: P ∧ Q ⟹ P<br />
· conjunct2: P ∧ Q ⟹ Q <br />
· notnotD: ¬¬ P ⟹ P<br />
· notnotI: P ⟹ ¬¬ P<br />
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q <br />
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F <br />
· impI: (P ⟹ Q) ⟹ P ⟶ Q<br />
· disjI1: P ⟹ P ∨ Q<br />
· disjI2: Q ⟹ P ∨ Q<br />
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R <br />
· FalseE: False ⟹ P<br />
· notE: ⟦¬P; P⟧ ⟹ R<br />
· notI: (P ⟹ False) ⟹ ¬P<br />
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q<br />
· iffD1: ⟦Q = P; Q⟧ ⟹ P <br />
· iffD2: ⟦P = Q; Q⟧ ⟹ P<br />
· ccontr: (¬P ⟹ False) ⟹ P<br />
---------------------------------------------------------------------›<br />
<br />
text ‹Se usarán las reglas notnotI y mt que demostramos a continuación.›<br />
<br />
lemma notnotI: "P ⟹ ¬¬ P"<br />
by auto<br />
<br />
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"<br />
by auto<br />
<br />
section ‹Disyunciones›<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 25. Demostrar<br />
p ⊢ p ∨ q<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_25:<br />
assumes "p"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 26. Demostrar<br />
q ⊢ p ∨ q<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_26:<br />
assumes "q"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 27. Demostrar<br />
p ∨ q ⊢ q ∨ p<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_27:<br />
assumes "p ∨ q"<br />
shows "q ∨ p"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 28. Demostrar<br />
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_28:<br />
assumes "q ⟶ r" <br />
shows "p ∨ q ⟶ p ∨ r"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 29. Demostrar<br />
p ∨ p ⊢ p<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_29:<br />
assumes "p ∨ p"<br />
shows "p"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 30. Demostrar<br />
p ⊢ p ∨ p<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_30:<br />
assumes "p" <br />
shows "p ∨ p"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 31. Demostrar<br />
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_31:<br />
assumes "p ∨ (q ∨ r)" <br />
shows "(p ∨ q) ∨ r"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 32. Demostrar<br />
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_32:<br />
assumes "(p ∨ q) ∨ r" <br />
shows "p ∨ (q ∨ r)"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 33. Demostrar<br />
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_33:<br />
assumes "p ∧ (q ∨ r)" <br />
shows "(p ∧ q) ∨ (p ∧ r)"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 34. Demostrar<br />
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_34:<br />
assumes "(p ∧ q) ∨ (p ∧ r)" <br />
shows "p ∧ (q ∨ r)"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 35. Demostrar<br />
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_35:<br />
assumes "p ∨ (q ∧ r)" <br />
shows "(p ∨ q) ∧ (p ∨ r)"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 36. Demostrar<br />
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_36:<br />
assumes "(p ∨ q) ∧ (p ∨ r)"<br />
shows "p ∨ (q ∧ r)"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 37. Demostrar<br />
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_37:<br />
assumes "(p ⟶ r) ∧ (q ⟶ r)" <br />
shows "p ∨ q ⟶ r"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 38. Demostrar<br />
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_38:<br />
assumes "p ∨ q ⟶ r" <br />
shows "(p ⟶ r) ∧ (q ⟶ r)"<br />
oops<br />
<br />
section ‹Negaciones›<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 39. Demostrar<br />
p ⊢ ¬¬p<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_39:<br />
assumes "p"<br />
shows "¬¬p"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_40:<br />
assumes "¬p" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 41. Demostrar<br />
p ⟶ q ⊢ ¬q ⟶ ¬p<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_41:<br />
assumes "p ⟶ q"<br />
shows "¬q ⟶ ¬p"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p∨q, ¬q ⊢ p<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_42:<br />
assumes "p∨q"<br />
"¬q" <br />
shows "p"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 42. Demostrar<br />
p ∨ q, ¬p ⊢ q<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_43:<br />
assumes "p ∨ q"<br />
"¬p" <br />
shows "q"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 40. Demostrar<br />
p ∨ q ⊢ ¬(¬p ∧ ¬q)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_44:<br />
assumes "p ∨ q" <br />
shows "¬(¬p ∧ ¬q)"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 45. Demostrar<br />
p ∧ q ⊢ ¬(¬p ∨ ¬q)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_45:<br />
assumes "p ∧ q" <br />
shows "¬(¬p ∨ ¬q)"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 46. Demostrar<br />
¬(p ∨ q) ⊢ ¬p ∧ ¬q<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_46:<br />
assumes "¬(p ∨ q)" <br />
shows "¬p ∧ ¬q"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 47. Demostrar<br />
¬p ∧ ¬q ⊢ ¬(p ∨ q)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_47:<br />
assumes "¬p ∧ ¬q" <br />
shows "¬(p ∨ q)"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 48. Demostrar<br />
¬p ∨ ¬q ⊢ ¬(p ∧ q)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_48:<br />
assumes "¬p ∨ ¬q"<br />
shows "¬(p ∧ q)"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 49. Demostrar<br />
⊢ ¬(p ∧ ¬p)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_49:<br />
"¬(p ∧ ¬p)"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 50. Demostrar<br />
p ∧ ¬p ⊢ q<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_50:<br />
assumes "p ∧ ¬p" <br />
shows "q"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 51. Demostrar<br />
¬¬p ⊢ p<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_51:<br />
assumes "¬¬p"<br />
shows "p"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 52. Demostrar<br />
⊢ p ∨ ¬p<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_52:<br />
"p ∨ ¬p"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 53. Demostrar<br />
⊢ ((p ⟶ q) ⟶ p) ⟶ p<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_53:<br />
"((p ⟶ q) ⟶ p) ⟶ p"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 54. Demostrar<br />
¬q ⟶ ¬p ⊢ p ⟶ q<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_54:<br />
assumes "¬q ⟶ ¬p"<br />
shows "p ⟶ q"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 55. Demostrar<br />
¬(¬p ∧ ¬q) ⊢ p ∨ q<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_55:<br />
assumes "¬(¬p ∧ ¬q)"<br />
shows "p ∨ q"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 56. Demostrar<br />
¬(¬p ∨ ¬q) ⊢ p ∧ q<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_56:<br />
assumes "¬(¬p ∨ ¬q)" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 57. Demostrar<br />
¬(p ∧ q) ⊢ ¬p ∨ ¬q<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_57:<br />
assumes "¬(p ∧ q)"<br />
shows "¬p ∨ ¬q"<br />
oops<br />
<br />
text ‹--------------------------------------------------------------- <br />
Ejercicio 58. Demostrar<br />
⊢ (p ⟶ q) ∨ (q ⟶ p)<br />
------------------------------------------------------------------›<br />
<br />
lemma ejercicio_58:<br />
"(p ⟶ q) ∨ (q ⟶ p)"<br />
oops<br />
<br />
end<br />
</source></div>
Jalonso