https://www.glc.us.es/~jalonso/LMF2020/index.php?action=history&feed=atom&title=R2
R2 - Historial de revisiones
2026-07-19T19:31:15Z
Historial de revisiones para esta página en el wiki
MediaWiki 1.31.14
https://www.glc.us.es/~jalonso/LMF2020/index.php?title=R2&diff=81&oldid=prev
Mjoseh: Protegió «R2» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))
2020-02-20T08:19:23Z
<p>Protegió «<a href="/~jalonso/LMF2020/index.php/R2" title="R2">R2</a>» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))</p>
<table class="diff diff-contentalign-left" data-mw="interface">
<tr class="diff-title" lang="es">
<td colspan="1" style="background-color: #fff; color: #222; text-align: center;">← Revisión anterior</td>
<td colspan="1" style="background-color: #fff; color: #222; text-align: center;">Revisión del 08:19 20 feb 2020</td>
</tr><tr><td colspan="2" class="diff-notice" lang="es"><div class="mw-diff-empty">(Sin diferencias)</div>
</td></tr></table>
Mjoseh
https://www.glc.us.es/~jalonso/LMF2020/index.php?title=R2&diff=80&oldid=prev
Mjoseh: Página creada con «<source lang = "isabelle"> chapter ‹ R2: Deducción natural proposicional(I) › theory R2 imports Main begin text ‹ ----------------------------------------------…»
2020-02-20T08:19:08Z
<p>Página creada con «<source lang = "isabelle"> chapter ‹ R2: Deducción natural proposicional(I) › theory R2 imports Main begin text ‹ ----------------------------------------------…»</p>
<p><b>Página nueva</b></p><div><source lang = "isabelle"><br />
chapter ‹ R2: Deducción natural proposicional(I) ›<br />
<br />
theory R2<br />
imports Main <br />
begin<br />
<br />
text ‹<br />
--------------------------------------------------------------------- <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 el método auto).<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 />
<br />
text‹<br />
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 ‹ Implicaciones ›<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 1. Demostrar<br />
p ⟶ q, p ⊢ q<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_1:<br />
assumes "p ⟶ q"<br />
"p"<br />
shows "q"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 2. Demostrar<br />
p ⟶ q, q ⟶ r, p ⊢ r<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_2:<br />
assumes "p ⟶ q"<br />
"q ⟶ r"<br />
"p" <br />
shows "r"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 3. Demostrar<br />
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_3:<br />
assumes "p ⟶ (q ⟶ r)"<br />
"p ⟶ q"<br />
"p"<br />
shows "r"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 4. Demostrar<br />
p ⟶ q, q ⟶ r ⊢ p ⟶ r<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_4:<br />
assumes "p ⟶ q"<br />
"q ⟶ r" <br />
shows "p ⟶ r"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 5. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_5:<br />
assumes "p ⟶ (q ⟶ r)" <br />
shows "q ⟶ (p ⟶ r)"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 6. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_6:<br />
assumes "p ⟶ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ (p ⟶ r)"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 7. Demostrar<br />
p ⊢ q ⟶ p<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_7:<br />
assumes "p" <br />
shows "q ⟶ p"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 8. Demostrar<br />
⊢ p ⟶ (q ⟶ p)<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_8:<br />
"p ⟶ (q ⟶ p)"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 9. Demostrar<br />
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_9:<br />
assumes "p ⟶ q" <br />
shows "(q ⟶ r) ⟶ (p ⟶ r)"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 10. Demostrar<br />
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_10:<br />
assumes "p ⟶ (q ⟶ (r ⟶ s))" <br />
shows "r ⟶ (q ⟶ (p ⟶ s))"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 11. Demostrar<br />
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_11:<br />
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 12. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_12:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
section ‹ Conjunciones ›<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 13. Demostrar<br />
p, q ⊢ p ∧ q<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_13:<br />
assumes "p"<br />
"q" <br />
shows "p ∧ q"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 14. Demostrar<br />
p ∧ q ⊢ p<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_14:<br />
assumes "p ∧ q" <br />
shows "p"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 15. Demostrar<br />
p ∧ q ⊢ q<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_15:<br />
assumes "p ∧ q" <br />
shows "q"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 16. Demostrar<br />
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_16:<br />
assumes "p ∧ (q ∧ r)"<br />
shows "(p ∧ q) ∧ r"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 17. Demostrar<br />
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_17:<br />
assumes "(p ∧ q) ∧ r" <br />
shows "p ∧ (q ∧ r)"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 18. Demostrar<br />
p ∧ q ⊢ p ⟶ q<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_18:<br />
assumes "p ∧ q" <br />
shows "p ⟶ q"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 19. Demostrar<br />
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r <br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_19:<br />
assumes "(p ⟶ q) ∧ (p ⟶ r)" <br />
shows "p ⟶ q ∧ r"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 20. Demostrar<br />
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_20:<br />
assumes "p ⟶ q ∧ r" <br />
shows "(p ⟶ q) ∧ (p ⟶ r)"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 21. Demostrar<br />
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_21:<br />
assumes "p ⟶ (q ⟶ r)" <br />
shows "p ∧ q ⟶ r"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 22. Demostrar<br />
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_22:<br />
assumes "p ∧ q ⟶ r" <br />
shows "p ⟶ (q ⟶ r)"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 23. Demostrar<br />
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_23:<br />
assumes "(p ⟶ q) ⟶ r" <br />
shows "p ∧ q ⟶ r"<br />
oops<br />
<br />
text ‹ --------------------------------------------------------------- <br />
Ejercicio 24. Demostrar<br />
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br />
------------------------------------------------------------------ ›<br />
<br />
lemma ejercicio_24:<br />
assumes "p ∧ (q ⟶ r)" <br />
shows "(p ⟶ q) ⟶ r"<br />
oops<br />
<br />
end<br />
<br />
<br />
</source></div>
Mjoseh