https://www.glc.us.es/~jalonso/LMF2018/api.php?action=feedcontributions&feedformat=atom&user=Agucrurom Lógica matemática y fundamentos (2017-18) - Contribuciones del usuario [es] 2026-07-25T04:19:02Z Contribuciones del usuario MediaWiki 1.31.14 https://www.glc.us.es/~jalonso/LMF2018/index.php?title=Relaci%C3%B3n_3&diff=121 Relación 3 2018-03-15T18:16:47Z <p>Agucrurom: /* Relación 3: Deducción natural en lógica proposicional */</p> <hr /> <div><br /> === Relación 3: Deducción natural en lógica proposicional ===<br /> <br /> ----<br /> &#039;&#039;&#039;Ejercicio 1.&#039;&#039;&#039; Demostrar mediante deducción natural:<br /> : ( p ∨ q ) ∧ ( p ∨ r ) ⊧ p ∨ ( q ∧ r )<br /> ----<br /> <br /> &#039;&#039;&#039;Solución:&#039;&#039;&#039; marmedmar3<br /> [https://i.gyazo.com/684b64b4146fa9d7e3e766350a6e3e81.png]<br /> <br /> <br /> ----<br /> &#039;&#039;&#039;Ejercicio 2.&#039;&#039;&#039; Demostrar mediante deducción natural:<br /> : p ∨ q ⊧ ¬(¬ p ∧ ¬ q )<br /> ----<br /> <br /> &#039;&#039;&#039;Solución:&#039;&#039;&#039;<br /> marmedmar3 [https://i.gyazo.com/11c29761ca9713a9c5e73da5cceb2325.png]<br /> <br /> ----<br /> &#039;&#039;&#039;Ejercicio 3.&#039;&#039;&#039; Demostrar mediante deducción natural:<br /> : ¬ p ∨ ¬ q ⊧ ¬( p ∧ q )<br /> ----<br /> <br /> &#039;&#039;&#039;Solución:&#039;&#039;&#039;<br /> marmedmar3 [https://i.gyazo.com/e98547a9c91132882d5401cc34744d4c.png]<br /> ----<br /> &#039;&#039;&#039;Ejercicio 4.&#039;&#039;&#039; Demostrar mediante deducción natural:<br /> : {p → r, r → ¬ q} ⊧ ¬(p ∧ q)<br /> ----<br /> <br /> &#039;&#039;&#039;Solución:&#039;&#039;&#039;<br /> marmedmar3 [https://i.gyazo.com/d9718d155692f74046b33426645db94f.png]<br /> <br /> ----<br /> &#039;&#039;&#039;Ejercicio 5.&#039;&#039;&#039; Demostrar mediante deducción natural:<br /> : (p → r) ∨ (q → s) ⊧ (p ∧ q) → (r ∨ s)<br /> ----<br /> <br /> &#039;&#039;&#039;Solución:&#039;&#039;&#039;<br /> marmedmar3 [https://i.gyazo.com/491d65b063dd124899cb4ce409d6e10a.png]<br /> <br /> ----<br /> &#039;&#039;&#039;Ejercicio 6.&#039;&#039;&#039; Demostrar mediante deducción natural:<br /> : p → (q ∧ r) ⊧ (p → q) ∨ (p → r)<br /> ----<br /> <br /> &#039;&#039;&#039;Solución:&#039;&#039;&#039;<br /> marmedmar3 [https://i.gyazo.com/91d8560cc5d5a221916c5dfd29e35348.png]</div> Agucrurom https://www.glc.us.es/~jalonso/LMF2018/index.php?title=Relaci%C3%B3n_4&diff=120 Relación 4 2018-03-15T18:14:49Z <p>Agucrurom: </p> <hr /> <div>&lt;source lang = &quot;isar&quot;&gt;<br /> <br /> chapter {* R4: Deducción natural proposicional *}<br /> <br /> theory R4<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: &quot;P ⟹ ¬¬ P&quot;<br /> by auto<br /> <br /> lemma mt: &quot;⟦F ⟶ G; ¬G⟧ ⟹ ¬F&quot;<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: josrodjim2 carmarria inmbenber<br /> assumes 1: &quot;p ⟶ q&quot; and<br /> 2: &quot;p&quot;<br /> shows &quot;q&quot;<br /> <br /> proof -<br /> show 1: &quot;q&quot; using 1 2 by (rule mp)<br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 2. Demostrar<br /> p ⟶ q, q ⟶ r, p ⊢ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_2: josrodjim2 carmarria inmbenber<br /> assumes 1: &quot;p ⟶ q&quot; and<br /> 2: &quot;q ⟶ r&quot; and<br /> 3: &quot;p&quot; <br /> shows &quot;r&quot;<br /> <br /> <br /> proof-<br /> have 4: &quot;q&quot; using 1 3 by (rule mp)<br /> show &quot;r&quot; using 2 4 by (rule mp)<br /> qed<br /> <br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 3. Demostrar<br /> p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_3: josrodjim2 carmarria inmbenber<br /> assumes 1: &quot;p ⟶ (q ⟶ r)&quot; and<br /> 2: &quot;p ⟶ q&quot; and<br /> 3: &quot;p&quot;<br /> shows &quot;r&quot;<br /> <br /> proof-<br /> have 4: &quot;q&quot; using 2 3 by (rule mp)<br /> have 5: &quot;(q ⟶ r)&quot; using 1 3 by (rule mp)<br /> show &quot;r&quot; using 5 4 by (rule mp)<br /> <br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 4. Demostrar<br /> p ⟶ q, q ⟶ r ⊢ p ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_4: josrodjim2<br /> assumes 1: &quot;p ⟶ q&quot; and<br /> 2: &quot;q ⟶ r&quot; <br /> shows &quot;p ⟶ r&quot;<br /> <br /> proof-<br /> { assume 3: &quot;p&quot;<br /> have 4: &quot;q&quot; using 1 3 by (rule mp)<br /> have 5: &quot;r&quot; using 2 4 by (rule mp)}<br /> hence 6: &quot;p ⟶ r&quot; using 3 5 by (rule impI)<br /> show &quot;p⟶r&quot; using 6 by this<br /> <br /> oops<br /> <br /> lemma ejercicio_4: carmarria<br /> assumes 1: &quot;p ⟶ q&quot; and<br /> 2: &quot;q ⟶ r&quot; <br /> shows &quot;p ⟶ r&quot;<br /> proof -<br /> { assume 3: p <br /> have 4: &quot;q&quot; using 1 3 by (rule mp)<br /> have 5: &quot;r&quot; using 2 4 by (rule mp)<br /> }<br /> thus &quot;p ⟶ r&quot; by (rule impI) <br /> qed<br /> lemma ejercicio_4: inmbenber<br /> assumes 1: &quot;p ⟶ q&quot; and<br /> 2: &quot;q ⟶ r&quot; <br /> shows &quot;p ⟶ r&quot;<br /> proof -<br /> { assume 3: &quot;p&quot; <br /> have 4: &quot;q&quot; using 1 3 by (rule mp)<br /> have 5: &quot;r&quot; using 2 4 by (rule mp) }<br /> thus &quot;p ⟶ r&quot; by (rule impI) <br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 5. Demostrar<br /> p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_5: josrodjim2 (NO DA ERROR, PERO SI ALERTA)<br /> assumes &quot;p ⟶ (q ⟶ r)&quot; <br /> shows &quot;q ⟶ (p ⟶ r)&quot;<br /> <br /> proof -<br /> <br /> { assume 2: &quot;q&quot;<br /> {assume 3: &quot;p&quot;<br /> have 4: &quot;q ⟶r&quot; using 1 3 by (rule mp)<br /> have 5: &quot;r&quot; using 4 2 by (rule mp)}<br /> hence 6: &quot;p⟶r&quot; using 3 5 by (rule impI)}<br /> hence 7: &quot;q ⟶ (p ⟶ r)&quot; using 2 6 by (rule impI)<br /> show &quot;q ⟶ (p ⟶ r)&quot; using 7 by this<br /> <br /> oops<br /> <br /> lemma ejercicio_5: carmarria <br /> assumes 1: &quot;p ⟶ (q ⟶ r)&quot; <br /> shows &quot;q ⟶ (p ⟶ r)&quot;<br /> <br /> proof - <br /> {assume 2: q<br /> {assume 3: p <br /> have 4: &quot;q ⟶ r&quot; using 1 3 by (rule mp)<br /> have 5: &quot;r&quot; using 4 2 by (rule mp)<br /> }<br /> hence &quot; p ⟶ r&quot; by (rule impI)<br /> }<br /> thus &quot;q ⟶ (p ⟶ r)&quot; by (rule impI)<br /> qed<br /> <br /> lemma ejercicio_5: inmbenber<br /> assumes 1: &quot;p ⟶ (q ⟶ r)&quot; <br /> shows &quot;q ⟶ (p ⟶ r)&quot;<br /> <br /> proof - <br /> {assume 2: &quot;q&quot;<br /> {assume 3: &quot;p&quot; <br /> have 4: &quot;q ⟶ r&quot; using 1 3 by (rule mp)<br /> have 5: &quot;r&quot; using 4 2 by (rule mp) }<br /> hence &quot; p ⟶ r&quot; by (rule impI) }<br /> thus &quot;q ⟶ (p ⟶ r)&quot; by (rule impI)<br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 6. Demostrar<br /> p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_6:josrodjim2<br /> assumes 1: &quot;p ⟶ (q ⟶ r)&quot; <br /> shows &quot;(p ⟶ q) ⟶ (p ⟶ r)&quot;<br /> <br /> proof- <br /> <br /> {assume 2: &quot;p⟶q&quot; <br /> {assume 3: &quot;p&quot;<br /> have 4: &quot;q⟶r&quot; using 1 3 by (rule mp)<br /> have 5: &quot;q&quot; using 2 3 by (rule mp)<br /> have 6: &quot;r&quot; using 4 5 by (rule mp)}<br /> hence 7: &quot;p⟶r&quot; using 3 6 by (rule impI)}<br /> hence 8: &quot;(p ⟶ q) ⟶ (p ⟶ r)&quot; using 2 7 by (rule impI)<br /> show &quot;(p ⟶ q) ⟶ (p ⟶ r)&quot; using 8 by this<br /> oops<br /> <br /> lemma ejercicio_6: carmarria, inmbenber<br /> assumes 1: &quot;p ⟶ (q ⟶ r)&quot; <br /> shows &quot;(p ⟶ q) ⟶ (p ⟶ r)&quot;<br /> proof -<br /> {assume 2: &quot;p ⟶ q&quot;<br /> {assume 3: &quot;p&quot;<br /> have 4: &quot;q&quot; using 2 3 by (rule mp)<br /> have 5: &quot;q ⟶ r&quot; using 1 3 by (rule mp)<br /> have 6: &quot;r&quot; using 5 4 by (rule mp)<br /> }<br /> hence 7: &quot;p ⟶ r&quot; by (rule impI)<br /> }<br /> thus &quot;(p ⟶ q) ⟶ (p ⟶ r)&quot; by (rule impI)<br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 7. Demostrar<br /> p ⊢ q ⟶ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_7: (NO SE QUE ESTA MAL)<br /> assumes &quot;p&quot; <br /> shows &quot;q ⟶ p&quot;<br /> <br /> proof -<br /> <br /> { assume 2: &quot;q&quot;<br /> have 3: &quot;p&quot; using 1<br /> }<br /> hence 4: &quot;q⟶p&quot; using 2 3 by (rule impI)<br /> <br /> show &quot;q⟶p&quot; using 4 by this<br /> <br /> oops<br /> <br /> lemma ejercicio_7: carmarria, inmbenber<br /> assumes 1: &quot;p&quot; <br /> shows &quot;q ⟶ p&quot;<br /> proof -<br /> {assume 2: &quot;q&quot;<br /> have 3: &quot;p&quot; using 1 by this}<br /> thus &quot;q ⟶ p&quot; by (rule impI)<br /> qed<br /> <br /> <br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 8. Demostrar<br /> ⊢ p ⟶ (q ⟶ p)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_8: carmarria<br /> &quot;p ⟶ (q ⟶ p)&quot;<br /> <br /> proof -<br /> {assume 1: p<br /> {assume 2: q<br /> have 3: p using 1 by this<br /> }<br /> hence 4: &quot;q ⟶ p&quot; by (rule impI)<br /> }<br /> thus &quot;p ⟶ (q ⟶ p)&quot; by (rule impI)<br /> qed<br /> text {* --------------------------------------------------------------- <br /> Ejercicio 9. Demostrar<br /> p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_9: carmarria<br /> assumes 1: &quot;p ⟶ q&quot; <br /> shows &quot;(q ⟶ r) ⟶ (p ⟶ r)&quot;<br /> proof -<br /> {assume 2: &quot;q ⟶ r&quot;<br /> {assume 3: &quot;p&quot;<br /> have 4: &quot;q&quot; using 1 3 by (rule mp)<br /> have 5: &quot;r&quot; using 2 4 by (rule mp)<br /> }<br /> hence 6: &quot;p ⟶ r&quot; by (rule impI)<br /> }<br /> thus 7: &quot;(q ⟶ r) ⟶ (p ⟶ r)&quot; by (rule impI)<br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 10. Demostrar<br /> p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_10: carmarria<br /> assumes 1: &quot;p ⟶ (q ⟶ (r ⟶ s))&quot; <br /> shows &quot;r ⟶ (q ⟶ (p ⟶ s))&quot;<br /> <br /> proof-<br /> {assume 2: r<br /> {assume 3: q<br /> {assume 4: p<br /> have 5: &quot;q ⟶ (r ⟶ s)&quot; using 1 4 by (rule mp)<br /> have 6: &quot;r ⟶ s&quot; using 5 3 by (rule mp)<br /> have 7: s using 6 2 by (rule mp)<br /> }<br /> hence 8: &quot;p ⟶ s&quot; by (rule impI)<br /> }<br /> hence 9: &quot;q ⟶ (p ⟶ s)&quot; by (rule impI)<br /> }<br /> thus &quot;r ⟶ (q ⟶ (p ⟶ s))&quot; by (rule impI)<br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 11. Demostrar<br /> ⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_11: carmarria<br /> &quot;(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))&quot;<br /> proof - <br /> {assume 1: &quot;p ⟶ (q ⟶ r)&quot;<br /> {assume 2: &quot;p ⟶ q&quot;<br /> {assume 3: p<br /> have 4: q using 2 3 by (rule mp)<br /> have 5: &quot;q ⟶ r&quot; using 1 3 by (rule mp)<br /> have 6: r using 5 4 by (rule mp)<br /> }<br /> hence 7: &quot;p ⟶ r&quot; by (rule impI)<br /> }<br /> hence 8: &quot;(p ⟶ q) ⟶ (p ⟶ r)&quot; by (rule impI)<br /> }<br /> thus &quot;(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))&quot; by (rule impI)<br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 12. Demostrar<br /> (p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_12: carmarria<br /> assumes 1: &quot;(p ⟶ q) ⟶ r&quot; <br /> shows &quot;p ⟶ (q ⟶ r)&quot;<br /> proof -<br /> {assume 2: p<br /> {assume 3: q<br /> {assume 4: p<br /> have 5: q using 3 by this<br /> }<br /> hence 6: &quot;p ⟶ q&quot; by (rule impI)<br /> have 7: r using 1 6 by (rule mp)<br /> }<br /> hence 8: &quot;q ⟶ r&quot; by (rule impI)<br /> }<br /> thus &quot;p ⟶ (q ⟶ r)&quot; by (rule impI)<br /> qed<br /> <br /> section {* Conjunciones *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 13. Demostrar<br /> p, q ⊢ p ∧ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_13:<br /> assumes &quot;p&quot;<br /> &quot;q&quot; <br /> shows &quot;p ∧ q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 14. Demostrar<br /> p ∧ q ⊢ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_14:<br /> assumes &quot;p ∧ q&quot; <br /> shows &quot;p&quot;<br /> proof -<br /> show &quot;p&quot; using assms by (rule conjunct1)<br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 15. Demostrar<br /> p ∧ q ⊢ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_15:<br /> assumes &quot;p ∧ q&quot; <br /> shows &quot;q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 16. Demostrar<br /> p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_16:<br /> assumes &quot;p ∧ (q ∧ r)&quot;<br /> shows &quot;(p ∧ q) ∧ r&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 17. Demostrar<br /> (p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_17:<br /> assumes &quot;(p ∧ q) ∧ r&quot; <br /> shows &quot;p ∧ (q ∧ r)&quot;<br /> proof (rule conjI)<br /> have &quot;p ∧ q&quot; using assms ..<br /> thus &quot;p&quot; ..<br /> next<br /> show &quot;q ∧ r&quot;<br /> proof (rule conjI)<br /> have &quot;p ∧ q&quot; using assms ..<br /> thus &quot;q&quot; ..<br /> next<br /> show &quot;r&quot; using assms ..<br /> qed<br /> qed<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 18. Demostrar<br /> p ∧ q ⊢ p ⟶ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_18:<br /> assumes &quot;p ∧ q&quot; <br /> shows &quot;p ⟶ q&quot;<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 &quot;(p ⟶ q) ∧ (p ⟶ r)&quot; <br /> shows &quot;p ⟶ q ∧ r&quot;<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 &quot;p ⟶ q ∧ r&quot; <br /> shows &quot;(p ⟶ q) ∧ (p ⟶ r)&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 21. Demostrar<br /> p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_21:<br /> assumes &quot;p ⟶ (q ⟶ r)&quot; <br /> shows &quot;p ∧ q ⟶ r&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 22. Demostrar<br /> p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_22:<br /> assumes &quot;p ∧ q ⟶ r&quot; <br /> shows &quot;p ⟶ (q ⟶ r)&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 23. Demostrar<br /> (p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_23:<br /> assumes &quot;(p ⟶ q) ⟶ r&quot; <br /> shows &quot;p ∧ q ⟶ r&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 24. Demostrar<br /> p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_24:<br /> assumes &quot;p ∧ (q ⟶ r)&quot; <br /> shows &quot;(p ⟶ q) ⟶ r&quot;<br /> oops<br /> <br /> section {* Disyunciones *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 25. Demostrar<br /> p ⊢ p ∨ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_25:<br /> assumes &quot;p&quot;<br /> shows &quot;p ∨ q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 26. Demostrar<br /> q ⊢ p ∨ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_26:<br /> assumes &quot;q&quot;<br /> shows &quot;p ∨ q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 27. Demostrar<br /> p ∨ q ⊢ q ∨ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_27:<br /> assumes &quot;p ∨ q&quot;<br /> shows &quot;q ∨ p&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 28. Demostrar<br /> q ⟶ r ⊢ p ∨ q ⟶ p ∨ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_28:<br /> assumes &quot;q ⟶ r&quot; <br /> shows &quot;p ∨ q ⟶ p ∨ r&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 29. Demostrar<br /> p ∨ p ⊢ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_29:<br /> assumes &quot;p ∨ p&quot;<br /> shows &quot;p&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 30. Demostrar<br /> p ⊢ p ∨ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_30:<br /> assumes &quot;p&quot; <br /> shows &quot;p ∨ p&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 31. Demostrar<br /> p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_31:<br /> assumes &quot;p ∨ (q ∨ r)&quot; <br /> shows &quot;(p ∨ q) ∨ r&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 32. Demostrar<br /> (p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_32:<br /> assumes &quot;(p ∨ q) ∨ r&quot; <br /> shows &quot;p ∨ (q ∨ r)&quot;<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 &quot;p ∧ (q ∨ r)&quot; <br /> shows &quot;(p ∧ q) ∨ (p ∧ r)&quot;<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 &quot;(p ∧ q) ∨ (p ∧ r)&quot; <br /> shows &quot;p ∧ (q ∨ r)&quot;<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 &quot;p ∨ (q ∧ r)&quot; <br /> shows &quot;(p ∨ q) ∧ (p ∨ r)&quot;<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 &quot;(p ∨ q) ∧ (p ∨ r)&quot;<br /> shows &quot;p ∨ (q ∧ r)&quot;<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 &quot;(p ⟶ r) ∧ (q ⟶ r)&quot; <br /> shows &quot;p ∨ q ⟶ r&quot;<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 &quot;p ∨ q ⟶ r&quot; <br /> shows &quot;(p ⟶ r) ∧ (q ⟶ r)&quot;<br /> oops<br /> <br /> section {* Negaciones *}<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 39. Demostrar<br /> p ⊢ ¬¬p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_39:<br /> assumes &quot;p&quot;<br /> shows &quot;¬¬p&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 40. Demostrar<br /> ¬p ⊢ p ⟶ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_40:<br /> assumes &quot;¬p&quot; <br /> shows &quot;p ⟶ q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 41. Demostrar<br /> p ⟶ q ⊢ ¬q ⟶ ¬p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_41:<br /> assumes &quot;p ⟶ q&quot;<br /> shows &quot;¬q ⟶ ¬p&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 42. Demostrar<br /> p∨q, ¬q ⊢ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_42:<br /> assumes &quot;p∨q&quot;<br /> &quot;¬q&quot; <br /> shows &quot;p&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 42. Demostrar<br /> p ∨ q, ¬p ⊢ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_43:<br /> assumes &quot;p ∨ q&quot;<br /> &quot;¬p&quot; <br /> shows &quot;q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 40. Demostrar<br /> p ∨ q ⊢ ¬(¬p ∧ ¬q)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_44:<br /> assumes &quot;p ∨ q&quot; <br /> shows &quot;¬(¬p ∧ ¬q)&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 45. Demostrar<br /> p ∧ q ⊢ ¬(¬p ∨ ¬q)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_45:<br /> assumes &quot;p ∧ q&quot; <br /> shows &quot;¬(¬p ∨ ¬q)&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 46. Demostrar<br /> ¬(p ∨ q) ⊢ ¬p ∧ ¬q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_46:<br /> assumes &quot;¬(p ∨ q)&quot; <br /> shows &quot;¬p ∧ ¬q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 47. Demostrar<br /> ¬p ∧ ¬q ⊢ ¬(p ∨ q)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_47:<br /> assumes &quot;¬p ∧ ¬q&quot; <br /> shows &quot;¬(p ∨ q)&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 48. Demostrar<br /> ¬p ∨ ¬q ⊢ ¬(p ∧ q)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_48:<br /> assumes &quot;¬p ∨ ¬q&quot;<br /> shows &quot;¬(p ∧ q)&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 49. Demostrar<br /> ⊢ ¬(p ∧ ¬p)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_49:<br /> &quot;¬(p ∧ ¬p)&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 50. Demostrar<br /> p ∧ ¬p ⊢ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_50:<br /> assumes &quot;p ∧ ¬p&quot; <br /> shows &quot;q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 51. Demostrar<br /> ¬¬p ⊢ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_51:<br /> assumes &quot;¬¬p&quot;<br /> shows &quot;p&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 52. Demostrar<br /> ⊢ p ∨ ¬p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_52:<br /> &quot;p ∨ ¬p&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 53. Demostrar<br /> ⊢ ((p ⟶ q) ⟶ p) ⟶ p<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_53:<br /> &quot;((p ⟶ q) ⟶ p) ⟶ p&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 54. Demostrar<br /> ¬q ⟶ ¬p ⊢ p ⟶ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_54:<br /> assumes &quot;¬q ⟶ ¬p&quot;<br /> shows &quot;p ⟶ q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 55. Demostrar<br /> ¬(¬p ∧ ¬q) ⊢ p ∨ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_55:<br /> assumes &quot;¬(¬p ∧ ¬q)&quot;<br /> shows &quot;p ∨ q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 56. Demostrar<br /> ¬(¬p ∨ ¬q) ⊢ p ∧ q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_56:<br /> assumes &quot;¬(¬p ∨ ¬q)&quot; <br /> shows &quot;p ∧ q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 57. Demostrar<br /> ¬(p ∧ q) ⊢ ¬p ∨ ¬q<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_57:<br /> assumes &quot;¬(p ∧ q)&quot;<br /> shows &quot;¬p ∨ ¬q&quot;<br /> oops<br /> <br /> text {* --------------------------------------------------------------- <br /> Ejercicio 58. Demostrar<br /> ⊢ (p ⟶ q) ∨ (q ⟶ p)<br /> ------------------------------------------------------------------ *}<br /> <br /> lemma ejercicio_58:<br /> &quot;(p ⟶ q) ∨ (q ⟶ p)&quot;<br /> oops<br /> <br /> end<br /> <br /> &lt;/source&gt;</div> Agucrurom