Diferencia entre revisiones de «Relación 6»
De Razonamiento automático (2018-19)
Línea 2: | Línea 2: | ||
chapter {* R6: Deducción natural proposicional *} | chapter {* R6: Deducción natural proposicional *} | ||
− | theory | + | theory R6_Deduccion_natural_proposicional_alu |
imports Main | imports Main | ||
begin | begin | ||
Línea 50: | Línea 50: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 cammonagu raffergon2 chrgencar gleherlop giafus1 | + | (* pabalagon manperjim josgomrom4 cammonagu raffergon2 chrgencar |
− | marfruman1 enrparalv pabbergue antramhur alikan juacanrod hugrubsan *) | + | gleherlop giafus1 marfruman1 enrparalv pabbergue antramhur alikan |
+ | juacanrod hugrubsan *) | ||
lemma ejercicio_1: | lemma ejercicio_1: | ||
assumes 1: "p ⟶ q" and | assumes 1: "p ⟶ q" and | ||
Línea 73: | Línea 74: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2 chrgencar giafus1 | + | (* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2 |
− | marfruman1 alfmarcua enrparalv pabbergue antramhur alikan juacanrod hugrubsan *) | + | chrgencar giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur |
+ | alikan juacanrod hugrubsan *) | ||
lemma ejercicio_2: | lemma ejercicio_2: | ||
assumes 1: "p ⟶ q" and | assumes 1: "p ⟶ q" and | ||
Línea 101: | Línea 103: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2 chrgencar giafus1 | + | (* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2 |
− | marfruman1 alfmarcua enrparalv pabbergue antramhur alikan juacanrod hugrubsan *) | + | chrgencar giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur |
+ | alikan juacanrod hugrubsan *) | ||
lemma ejercicio_3: | lemma ejercicio_3: | ||
assumes 1: "p ⟶ (q ⟶ r)" and | assumes 1: "p ⟶ (q ⟶ r)" and | ||
Línea 131: | Línea 134: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 cammonagu chrgencar raffergon2 gleherlop giafus1 | + | (* pabalagon manperjim josgomrom4 cammonagu chrgencar raffergon2 |
− | marfruman1 alfmarcua enrparalv pabbergue antramhur alikan juacanrod hugrubsan *) | + | gleherlop giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur |
+ | alikan juacanrod hugrubsan *) | ||
lemma ejercicio_4: | lemma ejercicio_4: | ||
assumes 1: "p ⟶ q" and | assumes 1: "p ⟶ q" and | ||
Línea 160: | Línea 164: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim raffergon2 giafus1 gleherlop | + | (* pabalagon manperjim raffergon2 giafus1 gleherlop marfruman1 alfmarcua |
− | marfruman1 alfmarcua enrparalv chrgencar pabbergue antramhur alikan hugrubsan *) | + | enrparalv chrgencar pabbergue antramhur alikan hugrubsan *) |
lemma ejercicio_5: | lemma ejercicio_5: | ||
assumes 1: "p ⟶ (q ⟶ r)" | assumes 1: "p ⟶ (q ⟶ r)" | ||
Línea 202: | Línea 206: | ||
thus "q ⟶ (p ⟶ r)" by (rule impI) | thus "q ⟶ (p ⟶ r)" by (rule impI) | ||
qed | qed | ||
− | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 210: | Línea 213: | ||
(* pabalagon manperjim cammonagu chrgencar raffergon2 gleherlop giafus1 | (* pabalagon manperjim cammonagu chrgencar raffergon2 gleherlop giafus1 | ||
− | marfruman1 alfmarcua enrparalv pabbergue antramhur alikan juacanrod hugrubsan *) | + | marfruman1 alfmarcua enrparalv pabbergue antramhur alikan juacanrod |
+ | hugrubsan *) | ||
lemma ejercicio_6: | lemma ejercicio_6: | ||
assumes 1: "p ⟶ (q ⟶ r)" | assumes 1: "p ⟶ (q ⟶ r)" | ||
Línea 245: | Línea 249: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 giafus1 gleherlop marfruman1 enrparalv pabbergue antramhur alikan hugrubsan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 giafus1 gleherlop |
+ | marfruman1 enrparalv pabbergue antramhur alikan hugrubsan *) | ||
lemma ejercicio_7: | lemma ejercicio_7: | ||
assumes 1: "p" | assumes 1: "p" | ||
Línea 273: | Línea 278: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 giafus1 marfruman1 enrparalv pabbergue antramhur alikan hugrubsan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 giafus1 marfruman1 |
+ | enrparalv pabbergue antramhur alikan hugrubsan *) | ||
lemma ejercicio_8: | lemma ejercicio_8: | ||
"p ⟶ (q ⟶ p)" | "p ⟶ (q ⟶ p)" | ||
Línea 289: | Línea 295: | ||
"p ⟶ (q ⟶ p)" | "p ⟶ (q ⟶ p)" | ||
using ejercicio_7_1 by (rule impI) | using ejercicio_7_1 by (rule impI) | ||
− | |||
text {* --------------------------------------------------------------- | text {* --------------------------------------------------------------- | ||
Línea 296: | Línea 301: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim raffergon2 giafus1 marfruman1 alfmarcua enrparalv gleherlop antramhur alikan hugrubsan *) | + | (* pabalagon manperjim raffergon2 giafus1 marfruman1 alfmarcua enrparalv |
+ | gleherlop antramhur alikan hugrubsan *) | ||
lemma ejercicio_9: | lemma ejercicio_9: | ||
assumes 1: "p ⟶ q" | assumes 1: "p ⟶ q" | ||
Línea 329: | Línea 335: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim raffergon2 marfruman1 gleherlop alfmarcua enrparalv pabbergue antramhur alikan juacanrod hugrubsan *) | + | (* pabalagon manperjim raffergon2 marfruman1 gleherlop alfmarcua |
+ | enrparalv pabbergue antramhur alikan juacanrod hugrubsan *) | ||
lemma ejercicio_10: | lemma ejercicio_10: | ||
assumes 1: "p ⟶ (q ⟶ (r ⟶ s))" | assumes 1: "p ⟶ (q ⟶ (r ⟶ s))" | ||
Línea 373: | Línea 380: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 gleherlop cammonagu giafus1 alfmarcua chrgencar pabbergue alikan juacanrod hugrubsan *) | + | (* pabalagon manperjim josgomrom4 gleherlop cammonagu giafus1 alfmarcua |
+ | chrgencar pabbergue alikan juacanrod hugrubsan *) | ||
lemma ejercicio_11: | lemma ejercicio_11: | ||
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" | "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" | ||
Línea 422: | Línea 430: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim raffergon2 marfruman1 gleherlop enrparalv pabbergue antramhur alikan juacanrod hugrubsan *) | + | (* pabalagon manperjim raffergon2 marfruman1 gleherlop enrparalv |
+ | pabbergue antramhur alikan juacanrod hugrubsan *) | ||
lemma ejercicio_12: | lemma ejercicio_12: | ||
assumes 1: "(p ⟶ q) ⟶ r" | assumes 1: "(p ⟶ q) ⟶ r" | ||
Línea 461: | Línea 470: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon | + | (* pabalagon *) |
lemma ejercicio_13: | lemma ejercicio_13: | ||
assumes "p" | assumes "p" | ||
Línea 468: | Línea 477: | ||
using assms(1, 2) by (rule conjI) | using assms(1, 2) by (rule conjI) | ||
− | (* benber manperjim josgomrom4 cammonagu raffergon2 marfruman1 alfmarcua enrparalv chrgencar gleherlop pabbergue antramhur juacanrod hugrubsan | + | (* benber manperjim josgomrom4 cammonagu raffergon2 marfruman1 alfmarcua |
+ | enrparalv chrgencar gleherlop pabbergue antramhur juacanrod hugrubsan | ||
alikan *) | alikan *) | ||
lemma ejercicio_13_1: | lemma ejercicio_13_1: | ||
Línea 487: | Línea 497: | ||
using assms(1) by (rule conjunct1) | using assms(1) by (rule conjunct1) | ||
− | (* benber manperjim cammonagu raffergon2 marfruman1 alfmarcua enrparalv chrgencar pabbergue gleherlop antramhur hugrubsan juacanrod alikan *) | + | (* benber manperjim cammonagu raffergon2 marfruman1 alfmarcua enrparalv |
+ | chrgencar pabbergue gleherlop antramhur hugrubsan juacanrod alikan *) | ||
lemma ejercicio_14_1: | lemma ejercicio_14_1: | ||
assumes "p ∧ q" | assumes "p ∧ q" | ||
Línea 504: | Línea 515: | ||
using assms(1) by (rule conjunct2) | using assms(1) by (rule conjunct2) | ||
− | (* benber cammonagu raffergon2 marfruman1 alfmarcua enrparalv chrgencar pabbergue antramhur gleherlop hugrubsan alikan *) | + | (* benber cammonagu raffergon2 marfruman1 alfmarcua enrparalv chrgencar |
+ | pabbergue antramhur gleherlop hugrubsan alikan *) | ||
lemma ejercicio_15_1: | lemma ejercicio_15_1: | ||
assumes "p ∧ q" | assumes "p ∧ q" | ||
Línea 515: | Línea 527: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua cammmonagu enrparalv chrgencar gleherlop pabbergue antramhur hugrubsan alikan juacanrod cammonagu*) | + | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua |
+ | cammmonagu enrparalv chrgencar gleherlop pabbergue antramhur | ||
+ | hugrubsan alikan juacanrod cammonagu *) | ||
lemma ejercicio_16: | lemma ejercicio_16: | ||
assumes "p ∧ (q ∧ r)" | assumes "p ∧ (q ∧ r)" | ||
Línea 534: | Línea 548: | ||
proof - (* TODO? *) | proof - (* TODO? *) | ||
have "q ∧ r" using assms by (rule conjunct2) | have "q ∧ r" using assms by (rule conjunct2) | ||
− | |||
have "p" using assms by (rule conjunct1) | have "p" using assms by (rule conjunct1) | ||
moreover have "q" using `q ∧ r` by (rule conjunct1) | moreover have "q" using `q ∧ r` by (rule conjunct1) | ||
Línea 547: | Línea 560: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua cammonagu chrgencar gleherlop pabbergue antramhur enrparalv hugrubsan juacanrod alikan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua |
+ | cammonagu chrgencar gleherlop pabbergue antramhur enrparalv hugrubsan | ||
+ | juacanrod alikan *) | ||
lemma ejercicio_17: | lemma ejercicio_17: | ||
assumes 1: "(p ∧ q) ∧ r" | assumes 1: "(p ∧ q) ∧ r" | ||
Línea 566: | Línea 581: | ||
proof - | proof - | ||
have "p ∧ q" using assms by (rule conjunct1) | have "p ∧ q" using assms by (rule conjunct1) | ||
− | |||
have "p" using `p ∧ q` by (rule conjunct1) | have "p" using `p ∧ q` by (rule conjunct1) | ||
moreover have "q ∧ r" | moreover have "q ∧ r" | ||
Línea 591: | Línea 605: | ||
qed | qed | ||
− | (* benber manperjim josgomrom4 cammonagu alfmarcua chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan *) | + | (* benber manperjim josgomrom4 cammonagu alfmarcua chrgencar pabbergue |
+ | gleherlop antramhur enrparalv hugrubsan *) | ||
lemma ejercicio_18_1: | lemma ejercicio_18_1: | ||
assumes "p ∧ q" | assumes "p ∧ q" | ||
Línea 604: | Línea 619: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua cammonagu chrgencar gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua |
+ | cammonagu chrgencar gleherlop pabbergue antramhur enrparalv juacanrod | ||
+ | hugrubsan alikan *) | ||
lemma ejercicio_19: | lemma ejercicio_19: | ||
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" | assumes 1: "(p ⟶ q) ∧ (p ⟶ r)" | ||
Línea 638: | Línea 655: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua cammonagu chrgencar gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua |
+ | cammonagu chrgencar gleherlop pabbergue antramhur enrparalv juacanrod | ||
+ | hugrubsan alikan *) | ||
lemma ejercicio_20: | lemma ejercicio_20: | ||
assumes 1: "p ⟶ q ∧ r" | assumes 1: "p ⟶ q ∧ r" | ||
Línea 682: | Línea 701: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua cammonagu chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua |
+ | cammonagu chrgencar pabbergue gleherlop antramhur enrparalv juacanrod | ||
+ | hugrubsan alikan *) | ||
lemma ejercicio_21: | lemma ejercicio_21: | ||
assumes 1: "p ⟶ (q ⟶ r)" | assumes 1: "p ⟶ (q ⟶ r)" | ||
Línea 711: | Línea 732: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua |
+ | chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan | ||
+ | alikan *) | ||
lemma ejercicio_22: | lemma ejercicio_22: | ||
assumes 1: "p ∧ q ⟶ r" | assumes 1: "p ∧ q ⟶ r" | ||
Línea 744: | Línea 767: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua |
+ | chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan | ||
+ | alikan *) | ||
lemma ejercicio_23: | lemma ejercicio_23: | ||
assumes 1: "(p ⟶ q) ⟶ r" | assumes 1: "(p ⟶ q) ⟶ r" | ||
Línea 774: | Línea 799: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan juacanrod cammonagu alikan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua |
+ | chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan juacanrod | ||
+ | cammonagu alikan *) | ||
lemma ejercicio_24: | lemma ejercicio_24: | ||
assumes 1: "p ∧ (q ⟶ r)" | assumes 1: "p ∧ (q ⟶ r)" | ||
Línea 792: | Línea 819: | ||
proof | proof | ||
have "q ⟶ r" using assms by (rule conjunct2) | have "q ⟶ r" using assms by (rule conjunct2) | ||
− | |||
assume "p ⟶ q" | assume "p ⟶ q" | ||
moreover have "p" using assms by (rule conjunct1) | moreover have "p" using assms by (rule conjunct1) | ||
Línea 806: | Línea 832: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 benber cammonagu raffergon2 marfruman1 alfmarcua chrgencar gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim josgomrom4 benber cammonagu raffergon2 marfruman1 |
+ | alfmarcua chrgencar gleherlop pabbergue antramhur enrparalv juacanrod | ||
+ | hugrubsan alikan *) | ||
lemma ejercicio_25: | lemma ejercicio_25: | ||
assumes "p" | assumes "p" | ||
Línea 817: | Línea 845: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 benber cammonagu marfruman1 alfmarcua chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim josgomrom4 benber cammonagu marfruman1 alfmarcua |
+ | chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan | ||
+ | alikan *) | ||
lemma ejercicio_26: | lemma ejercicio_26: | ||
assumes "q" | assumes "q" | ||
Línea 828: | Línea 858: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar pabbergue antramhur enrparalv juacanrod hugrubsan cammonagu alikan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar |
+ | pabbergue antramhur enrparalv juacanrod hugrubsan cammonagu alikan *) | ||
lemma ejercicio_27: | lemma ejercicio_27: | ||
assumes 1: "p ∨ q" | assumes 1: "p ∨ q" | ||
Línea 854: | Línea 885: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar gleherlop alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan cammonagu alikan *) | + | (* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar |
+ | gleherlop alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan | ||
+ | cammonagu alikan *) | ||
lemma ejercicio_28: | lemma ejercicio_28: | ||
assumes 1: "q ⟶ r" | assumes 1: "q ⟶ r" | ||
Línea 898: | Línea 931: | ||
qed | qed | ||
− | (* benber manperjim cammonagu josgomrom4 raffergon2 chrgencar alfmarcua gleherlop pabbergue antramhur enrparalv hugrubsan alikan *) | + | (* benber manperjim cammonagu josgomrom4 raffergon2 chrgencar alfmarcua |
+ | gleherlop pabbergue antramhur enrparalv hugrubsan alikan *) | ||
lemma ejercicio_29_1: | lemma ejercicio_29_1: | ||
assumes "p ∨ p" | assumes "p ∨ p" | ||
Línea 909: | Línea 943: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim benber josgomrom4 raffergon2 marfruman1 chrgencar alfmarcua pabbergue gleherlop antramhur enrparalv hugrubsan juacanrod cammonagu alikan *) | + | (* pabalagon manperjim benber josgomrom4 raffergon2 marfruman1 |
+ | chrgencar alfmarcua pabbergue gleherlop antramhur enrparalv hugrubsan | ||
+ | juacanrod cammonagu alikan *) | ||
lemma ejercicio_30: | lemma ejercicio_30: | ||
assumes "p" | assumes "p" | ||
Línea 920: | Línea 956: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue |
+ | gleherlop antramhur enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_31: | lemma ejercicio_31: | ||
assumes 1: "p ∨ (q ∨ r)" | assumes 1: "p ∨ (q ∨ r)" | ||
Línea 970: | Línea 1007: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop |
+ | pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_32: | lemma ejercicio_32: | ||
assumes 1: "(p ∨ q) ∨ r" | assumes 1: "(p ∨ q) ∨ r" | ||
Línea 1019: | Línea 1057: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 chrgencar gleherlop alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 chrgencar gleherlop |
+ | alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_33: | lemma ejercicio_33: | ||
assumes 1: "p ∧ (q ∨ r)" | assumes 1: "p ∧ (q ∨ r)" | ||
Línea 1062: | Línea 1101: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua |
+ | gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_34: | lemma ejercicio_34: | ||
assumes "(p ∧ q) ∨ (p ∧ r)" | assumes "(p ∧ q) ∨ (p ∧ r)" | ||
Línea 1110: | Línea 1150: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua |
+ | gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_35: | lemma ejercicio_35: | ||
assumes "p ∨ (q ∧ r)" | assumes "p ∨ (q ∧ r)" | ||
Línea 1158: | Línea 1199: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua |
+ | gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_36: | lemma ejercicio_36: | ||
assumes 1: "(p ∨ q) ∧ (p ∨ r)" | assumes 1: "(p ∨ q) ∧ (p ∨ r)" | ||
Línea 1211: | Línea 1253: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop |
+ | pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_37: | lemma ejercicio_37: | ||
assumes 1: "(p ⟶ r) ∧ (q ⟶ r)" | assumes 1: "(p ⟶ r) ∧ (q ⟶ r)" | ||
Línea 1250: | Línea 1293: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop |
+ | pabbergue antramhur enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_38: | lemma ejercicio_38: | ||
assumes "p ∨ q ⟶ r" | assumes "p ∨ q ⟶ r" | ||
Línea 1295: | Línea 1339: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim benber josgomrom4 raffergon2 gleherlop marfruman1 chrgencar alfmarcua pabbergue enrparalv juacanrod hugrubsan cammonagu alikan *) | + | (* pabalagon manperjim benber josgomrom4 raffergon2 gleherlop |
+ | marfruman1 chrgencar alfmarcua pabbergue enrparalv juacanrod | ||
+ | hugrubsan cammonagu alikan *) | ||
lemma ejercicio_39: | lemma ejercicio_39: | ||
assumes "p" | assumes "p" | ||
Línea 1306: | Línea 1352: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue gleherlop juacanrod enrparalv hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue |
+ | gleherlop juacanrod enrparalv hugrubsan alikan *) | ||
lemma ejercicio_40: | lemma ejercicio_40: | ||
assumes 1: "¬p" | assumes 1: "¬p" | ||
Línea 1328: | Línea 1375: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua |
+ | pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_41: | lemma ejercicio_41: | ||
assumes 1: "p ⟶ q" | assumes 1: "p ⟶ q" | ||
Línea 1350: | Línea 1398: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua |
+ | pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_42: | lemma ejercicio_42: | ||
assumes "p∨q" | assumes "p∨q" | ||
Línea 1381: | Línea 1430: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua |
+ | pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *) | ||
lemma ejercicio_43: | lemma ejercicio_43: | ||
assumes "p ∨ q" | assumes "p ∨ q" | ||
Línea 1412: | Línea 1462: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim gleherlop josgomrom4 marfruman1 pabbergue juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim gleherlop josgomrom4 marfruman1 pabbergue |
+ | juacanrod hugrubsan alikan *) | ||
lemma ejercicio_44: | lemma ejercicio_44: | ||
assumes "p ∨ q" | assumes "p ∨ q" | ||
Línea 1433: | Línea 1484: | ||
proof | proof | ||
assume "¬p ∧ ¬q" | assume "¬p ∧ ¬q" | ||
− | |||
note `p ∨ q` | note `p ∨ q` | ||
moreover { | moreover { | ||
Línea 1453: | Línea 1503: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue |
+ | juacanrod hugrubsan alikan *) | ||
lemma ejercicio_45: | lemma ejercicio_45: | ||
assumes 1: "p ∧ q" | assumes 1: "p ∧ q" | ||
Línea 1492: | Línea 1543: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue |
+ | juacanrod hugrubsan alikan *) | ||
lemma ejercicio_46: | lemma ejercicio_46: | ||
assumes 1: "¬(p ∨ q)" | assumes 1: "¬(p ∨ q)" | ||
Línea 1550: | Línea 1602: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 pabbregue juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 pabbregue juacanrod |
+ | hugrubsan alikan *) | ||
lemma ejercicio_47: | lemma ejercicio_47: | ||
assumes 1: "¬p ∧ ¬q" | assumes 1: "¬p ∧ ¬q" | ||
Línea 1593: | Línea 1646: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 pabbergue juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 pabbergue juacanrod |
+ | hugrubsan alikan *) | ||
lemma ejercicio_48: | lemma ejercicio_48: | ||
assumes 1: "¬p ∨ ¬q" | assumes 1: "¬p ∨ ¬q" | ||
Línea 1623: | Línea 1677: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcu gleherlop hugrubsan juacanrod cammonagu alikan *) | + | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcu gleherlop |
+ | hugrubsan juacanrod cammonagu alikan *) | ||
lemma ejercicio_49: | lemma ejercicio_49: | ||
"¬(p ∧ ¬p)" | "¬(p ∧ ¬p)" | ||
Línea 1647: | Línea 1702: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 gleherlop alfmarcua enrparalv pabbergue juacanrod hugrubsan alikan *) | + | (* pabalagon manperjim raffergon2 josgomrom4 marfruman1 gleherlop |
+ | alfmarcua enrparalv pabbergue juacanrod hugrubsan alikan *) | ||
lemma ejercicio_50: | lemma ejercicio_50: | ||
assumes 1: "p ∧ ¬p" | assumes 1: "p ∧ ¬p" | ||
Línea 1671: | Línea 1727: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim benber raffergon2 josgomrom4 marfruman1 gleherlop alfmarcua enrparalv pabbergue juacanrod hugrubsan cammmonagu alikan *) | + | (* pabalagon manperjim benber raffergon2 josgomrom4 marfruman1 gleherlop |
+ | alfmarcua enrparalv pabbergue juacanrod hugrubsan cammmonagu alikan *) | ||
lemma ejercicio_51: | lemma ejercicio_51: | ||
assumes "¬¬p" | assumes "¬¬p" | ||
Línea 1723: | Línea 1780: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop juacanrod pabbergue *) | + | (* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop |
+ | juacanrod pabbergue *) | ||
lemma ejercicio_53: | lemma ejercicio_53: | ||
"((p ⟶ q) ⟶ p) ⟶ p" | "((p ⟶ q) ⟶ p) ⟶ p" | ||
Línea 1758: | Línea 1816: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod pabbergue *) | + | (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod |
+ | pabbergue *) | ||
lemma ejercicio_54: | lemma ejercicio_54: | ||
assumes 1: "¬q ⟶ ¬p" | assumes 1: "¬q ⟶ ¬p" | ||
Línea 1820: | Línea 1879: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod pabbergue *) | + | (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod |
+ | pabbergue *) | ||
lemma ejercicio_56: | lemma ejercicio_56: | ||
assumes 1: "¬(¬p ∨ ¬q)" | assumes 1: "¬(¬p ∨ ¬q)" | ||
Línea 1857: | Línea 1917: | ||
------------------------------------------------------------------ *} | ------------------------------------------------------------------ *} | ||
− | (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod pabbergue *) | + | (* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod |
+ | pabbergue *) | ||
lemma ejercicio_57: | lemma ejercicio_57: | ||
assumes 1: "¬(p ∧ q)" | assumes 1: "¬(p ∧ q)" |
Revisión del 13:57 28 feb 2019
chapter {* R6: Deducción natural proposicional *}
theory R6_Deduccion_natural_proposicional_alu
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
---------------------------------------------------------------------
*}
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
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 cammonagu raffergon2 chrgencar
gleherlop giafus1 marfruman1 enrparalv pabbergue antramhur alikan
juacanrod hugrubsan *)
lemma ejercicio_1:
assumes 1: "p ⟶ q" and
2: "p"
shows "q"
proof -
show "q" using 1 2 by (rule mp)
qed
(* benber alfmarcua *)
lemma ejercicio_1_1:
assumes "p ⟶ q"
"p"
shows "q"
using assms by (rule mp)
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2
chrgencar giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
alikan juacanrod hugrubsan *)
lemma ejercicio_2:
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
(* benber *)
lemma ejercicio_2_1:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
proof -
have "q" using `p ⟶ q` `p` by (rule mp)
with `q ⟶ r` show "r" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 cammonagu gleherlop raffergon2
chrgencar giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
alikan juacanrod hugrubsan *)
lemma ejercicio_3:
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 "r" using 4 5 by (rule mp)
qed
(* benber *)
lemma ejercicio_3_1:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
proof -
have "q ⟶ r" using `p ⟶ (q ⟶ r)` `p` by (rule mp)
moreover have "q" using `p ⟶ q` `p` by (rule mp)
ultimately show "r" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 cammonagu chrgencar raffergon2
gleherlop giafus1 marfruman1 alfmarcua enrparalv pabbergue antramhur
alikan juacanrod hugrubsan *)
lemma ejercicio_4:
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
(* benber *)
lemma ejercicio_4_1:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
proof
assume p
with `p ⟶ q` have "q" by (rule mp)
with `q ⟶ r` show "r" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim raffergon2 giafus1 gleherlop marfruman1 alfmarcua
enrparalv chrgencar pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_5:
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
show "r" using 4 2 by (rule mp)
qed
qed
(* benber josgomrom4 juacanrod cammonagu *)
lemma ejercicio_5_1:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof
assume "q"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
thus "r" using `q` by (rule mp)
qed
qed
(* pabalagon *)
lemma ejercicio_5_2:
assumes 1: "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof -
{ assume 2: "q"
{ assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "r" using 4 2 by (rule mp)}
hence "p ⟶ r" by (rule impI)
}
thus "q ⟶ (p ⟶ r)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim cammonagu chrgencar raffergon2 gleherlop giafus1
marfruman1 alfmarcua enrparalv pabbergue antramhur alikan juacanrod
hugrubsan *)
lemma ejercicio_6:
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show "r" using 4 5 by (rule mp)
qed
qed
(* benber josgomrom4 *)
lemma ejercicio_6_1:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume "p ⟶ q"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
moreover from `p ⟶ q` `p` have "q" by (rule mp)
ultimately show "r" by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 giafus1 gleherlop
marfruman1 enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_7:
assumes 1: "p"
shows "q ⟶ p"
proof (rule impI)
assume 2: "q"
show "p" using 1 by this
qed
(* benber cammonagu juacanrod chrgencar *)
lemma ejercicio_7_1:
assumes "p"
shows "q ⟶ p"
proof
show "p" using `p` .
qed
(* alfmarcua *)
lemma ejercicio_7_2:
assumes "p"
shows "q ⟶ p"
using assms by (rule impI)
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 giafus1 marfruman1
enrparalv pabbergue antramhur alikan hugrubsan *)
lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
proof (rule impI)
assume 1: "p"
show "q ⟶ p"
proof (rule impI)
assume 2: "q"
show "p" using 1 by this
qed
qed
(* benber cammonagu gleherlop chrgencar juacanrod alfmarcua *)
lemma ejercicio_8_1:
"p ⟶ (q ⟶ p)"
using ejercicio_7_1 by (rule impI)
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim raffergon2 giafus1 marfruman1 alfmarcua enrparalv
gleherlop antramhur alikan hugrubsan *)
lemma ejercicio_9:
assumes 1: "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "q ⟶ r"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
show "r" using 2 4 by (rule mp)
qed
qed
(* benber josgomrom4 cammonagu chrgencar juacanrod pabbergue *)
lemma ejercicio_9_1:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof
assume "q ⟶ r"
show "p ⟶ r"
proof
assume "p"
with `p ⟶ q` have "q" by (rule mp)
with `q ⟶ r` show "r" by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}
(* pabalagon manperjim raffergon2 marfruman1 gleherlop alfmarcua
enrparalv pabbergue antramhur alikan juacanrod hugrubsan *)
lemma ejercicio_10:
assumes 1: "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof (rule impI)
assume 2: "r"
show "q ⟶ (p ⟶ s)"
proof (rule impI)
assume 3: "q"
show "p ⟶ s"
proof (rule impI)
assume 4: "p"
have 5: "q ⟶ (r ⟶ s)" using 1 4 by (rule mp)
have 6: "r ⟶ s" using 5 3 by (rule mp)
show "s" using 6 2 by (rule mp)
qed
qed
qed
(* benber josgomrom4 cammonagu chrgencar giafus1 *)
lemma ejercicio_10_1:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof
assume "r"
show "q ⟶ (p ⟶ s)"
proof
assume "q"
show "p ⟶ s"
proof
assume "p"
with `p ⟶ (q ⟶ (r ⟶ s))`
have "q ⟶ (r ⟶ s)" by (rule mp)
hence "r ⟶ s" using `q` by (rule mp)
thus "s" using `r` by (rule mp)
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 gleherlop cammonagu giafus1 alfmarcua
chrgencar pabbergue alikan juacanrod hugrubsan *)
lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)" using 1 ejercicio_6 by simp
qed
(* pabalagon raffergon2 marfruman1 enrparalv antramhur *)
lemma ejercicio_11_2:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "p ⟶ q"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show "r" using 4 5 by (rule mp)
qed
qed
qed
(* benber *)
lemma ejercicio_11_1:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume "p ⟶ (q ⟶ r)"
show "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume "p ⟶ q"
show "p ⟶ r"
proof
assume p
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
moreover have "q" using `p ⟶ q` `p` by (rule mp)
ultimately show r by (rule mp)
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim raffergon2 marfruman1 gleherlop enrparalv
pabbergue antramhur alikan juacanrod hugrubsan *)
lemma ejercicio_12:
assumes 1: "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume 2: "p"
show "q ⟶ r"
proof (rule impI)
assume 3: "q"
have 4: "p ⟶ q"
proof (rule impI)
assume 5: "p"
show "q" using 3 by this
qed
show "r" using 1 4 by (rule mp)
qed
qed
(* benber josgomrom4 cammonagu giafus1 alfmarcua chrgencar *)
lemma ejercicio_12_1:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q ⟶ r"
proof
assume "q"
hence "p ⟶ q" by (rule impI)
with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
qed
qed
section {* Conjunciones *}
text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}
(* pabalagon *)
lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"
using assms(1, 2) by (rule conjI)
(* benber manperjim josgomrom4 cammonagu raffergon2 marfruman1 alfmarcua
enrparalv chrgencar gleherlop pabbergue antramhur juacanrod hugrubsan
alikan *)
lemma ejercicio_13_1:
assumes "p"
"q"
shows "p ∧ q"
using assms by (rule conjI)
text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}
(* pabalagon josgomrom4 *)
lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
using assms(1) by (rule conjunct1)
(* benber manperjim cammonagu raffergon2 marfruman1 alfmarcua enrparalv
chrgencar pabbergue gleherlop antramhur hugrubsan juacanrod alikan *)
lemma ejercicio_14_1:
assumes "p ∧ q"
shows "p"
using assms by (rule conjunct1)
text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}
(* pabalagon manperjim juacanrod josgomrom4 *)
lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
using assms(1) by (rule conjunct2)
(* benber cammonagu raffergon2 marfruman1 alfmarcua enrparalv chrgencar
pabbergue antramhur gleherlop hugrubsan alikan *)
lemma ejercicio_15_1:
assumes "p ∧ q"
shows "q"
using assms by (rule conjunct2)
text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
cammmonagu enrparalv chrgencar gleherlop pabbergue antramhur
hugrubsan alikan juacanrod cammonagu *)
lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof -
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "q ∧ r" using assms(1) 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
(* benber *)
lemma ejercicio_16_1:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof - (* TODO? *)
have "q ∧ r" using assms by (rule conjunct2)
have "p" using assms by (rule conjunct1)
moreover have "q" using `q ∧ r` by (rule conjunct1)
ultimately have "p ∧ q" by (rule conjI)
moreover have "r" using `q ∧ r` by (rule conjunct2)
ultimately show "(p ∧ q) ∧ r" by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
cammonagu chrgencar gleherlop pabbergue antramhur enrparalv hugrubsan
juacanrod alikan *)
lemma ejercicio_17:
assumes 1: "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof -
have 2: "r" using 1 by (rule conjunct2)
have 3: "p ∧ q" using 1 by (rule conjunct1)
have 4: "p" using 3 by (rule conjunct1)
have 5: "q" using 3 by (rule conjunct2)
have 6: "q ∧ r" using 5 2 by (rule conjI)
show ?thesis using 4 6 by (rule conjI)
qed
(* benber *)
lemma ejercicio_17_1:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof -
have "p ∧ q" using assms by (rule conjunct1)
have "p" using `p ∧ q` by (rule conjunct1)
moreover have "q ∧ r"
proof (rule conjI)
show "q" using `p ∧ q` by (rule conjunct2)
next
show "r" using assms by (rule conjunct2)
qed
ultimately show ?thesis by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}
(* pabalagon raffergon2 marfruman1 juacanrod alikan*)
lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using assms(1) by (rule conjunct2)
qed
(* benber manperjim josgomrom4 cammonagu alfmarcua chrgencar pabbergue
gleherlop antramhur enrparalv hugrubsan *)
lemma ejercicio_18_1:
assumes "p ∧ q"
shows "p ⟶ q"
proof
show "q" using assms by (rule conjunct2)
qed
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
cammonagu chrgencar gleherlop pabbergue antramhur enrparalv juacanrod
hugrubsan alikan *)
lemma ejercicio_19:
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof (rule impI)
assume 2: "p"
have 3: "p ⟶ q" using 1 by (rule conjunct1)
have 4: "p ⟶ r" using 1 by (rule conjunct2)
have 5: "q" using 3 2 by (rule mp)
have 6: "r" using 4 2 by (rule mp)
show "q ∧ r" using 5 6 by (rule conjI)
qed
(* benber cammonagu *)
lemma ejercicio_19_1:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof
assume p
show "q ∧ r"
proof
have "p ⟶ q" using assms by (rule conjunct1)
thus "q" using `p` by (rule mp)
next
have "p ⟶ r" using assms by (rule conjunct2)
thus "r" using `p` by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
cammonagu chrgencar gleherlop pabbergue antramhur enrparalv juacanrod
hugrubsan alikan *)
lemma ejercicio_20:
assumes 1: "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
show "p ⟶ q"
proof (rule impI)
assume 2: "p"
have 3: "q ∧ r" using 1 2 by (rule mp)
show 4: "q" using 3 by (rule conjunct1)
qed
show "p ⟶ r"
proof (rule impI)
assume 2: "p"
have 3: "q ∧ r" using 1 2 by (rule mp)
show 4: "r" using 3 by (rule conjunct2)
qed
qed
(* benber *)
lemma ejercicio_20_1:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof
show "p ⟶ q"
proof
assume "p"
with assms have "q ∧ r" by (rule mp)
thus "q" by (rule conjunct1)
qed
next
show "p ⟶ r"
proof
assume "p"
with assms have "q ∧ r" by (rule mp)
thus "r" by (rule conjunct2)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
cammonagu chrgencar pabbergue gleherlop antramhur enrparalv juacanrod
hugrubsan alikan *)
lemma ejercicio_21:
assumes 1: "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume 2: "p ∧ q"
have 3: "p" using 2 by (rule conjunct1)
have 4: "q ⟶ r" using 1 3 by (rule mp)
have 5: "q" using 2 by (rule conjunct2)
show "r" using 4 5 by (rule mp)
qed
(* benber *)
lemma ejercicio_21_1:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
hence "p" by (rule conjunct1)
with `p ⟶ (q ⟶ r)` have "q ⟶ r" by (rule mp)
moreover from `p ∧ q` have "q" by (rule conjunct2)
ultimately show "r" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan
alikan *)
lemma ejercicio_22:
assumes 1: "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume 2: "p"
show "q ⟶ r"
proof (rule impI)
assume 3: "q"
have 4: "p ∧ q" using 2 3 by (rule conjI)
show "r" using 1 4 by (rule mp)
qed
qed
(* benber cammonagu *)
lemma ejercicio_22_1:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "q ⟶ r"
proof
assume "q"
with `p` have "p ∧ q" by (rule conjI)
with `p ∧ q ⟶ r` show "r" by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan
alikan *)
lemma ejercicio_23:
assumes 1: "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume 2: "p ∧ q"
have 3: "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using 2 by (rule conjunct2)
qed
show "r" using 1 3 by (rule mp)
qed
(* benber cammonagu *)
lemma ejercicio_23_1:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
hence "q" by (rule conjunct2)
hence "p ⟶ q" by (rule impI)
with `(p ⟶ q) ⟶ r` show "r" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 alfmarcua
chrgencar pabbergue gleherlop antramhur enrparalv hugrubsan juacanrod
cammonagu alikan *)
lemma ejercicio_24:
assumes 1: "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof (rule impI)
assume 2: "p ⟶ q"
have 3: "p" using 1 by (rule conjunct1)
have 4: "q ⟶ r" using 1 by (rule conjunct2)
have 5: "q" using 2 3 by (rule mp)
show 6: "r" using 4 5 by (rule mp)
qed
(* benber *)
lemma ejercicio_24_1:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
have "q ⟶ r" using assms by (rule conjunct2)
assume "p ⟶ q"
moreover have "p" using assms by (rule conjunct1)
ultimately have "q" by (rule mp)
with `q ⟶ r` show r by (rule mp)
qed
section {* Disyunciones *}
text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 benber cammonagu raffergon2 marfruman1
alfmarcua chrgencar gleherlop pabbergue antramhur enrparalv juacanrod
hugrubsan alikan *)
lemma ejercicio_25:
assumes "p"
shows "p ∨ q"
using assms(1) by (rule disjI1)
text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 benber cammonagu marfruman1 alfmarcua
chrgencar pabbergue gleherlop antramhur enrparalv juacanrod hugrubsan
alikan *)
lemma ejercicio_26:
assumes "q"
shows "p ∨ q"
using assms(1) by (rule disjI2)
text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar
pabbergue antramhur enrparalv juacanrod hugrubsan cammonagu alikan *)
lemma ejercicio_27:
assumes 1: "p ∨ q"
shows "q ∨ p"
using 1 proof (rule disjE)
assume 2: "p" thus "q ∨ p" by (rule disjI2)
next
assume 3: "q" thus "q ∨ p" by (rule disjI1)
qed
(* benber alfmarcua gleherlop *)
lemma ejercicio_27_1:
assumes "p ∨ q"
shows "q ∨ p"
proof -
have "p ∨ q" using assms .
moreover have "p ⟹ q ∨ p" by (rule disjI2)
moreover have "q ⟹ q ∨ p" by (rule disjI1)
ultimately show "q ∨ p" by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 raffergon2 marfruman1 chrgencar
gleherlop alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan
cammonagu alikan *)
lemma ejercicio_28:
assumes 1: "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
assume 2: "p ∨ q" show "p ∨ r" using 2
proof (rule disjE)
assume 3: p thus "p ∨ r" by (rule disjI1)
next
assume 4: q have r using 1 4 by (rule mp)
thus "p ∨ r" by (rule disjI2)
qed
qed
(* benber *)
lemma ejercicio_28_1:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof
assume "p ∨ q"
moreover have "p ⟹ p ∨ r" by (rule disjI1)
moreover have "q ⟹ p ∨ r"
proof (rule disjI2)
assume "q"
with `q ⟶ r` show "r" by (rule mp)
qed
ultimately show "p ∨ r" by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}
(* pabalagon juacanrod marfruman1 *)
lemma ejercicio_29:
assumes 1: "p ∨ p"
shows "p"
using 1 proof (rule disjE)
assume "p" thus "p" .
next
assume "p" thus "p" .
qed
(* benber manperjim cammonagu josgomrom4 raffergon2 chrgencar alfmarcua
gleherlop pabbergue antramhur enrparalv hugrubsan alikan *)
lemma ejercicio_29_1:
assumes "p ∨ p"
shows "p"
using assms by (rule disjE)
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}
(* pabalagon manperjim benber josgomrom4 raffergon2 marfruman1
chrgencar alfmarcua pabbergue gleherlop antramhur enrparalv hugrubsan
juacanrod cammonagu alikan *)
lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
using assms(1) by (rule disjI1)
text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue
gleherlop antramhur enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_31:
assumes 1: "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r" (is "?R")
using 1 proof (rule disjE)
assume "p" hence "p ∨ q" by (rule disjI1)
thus ?R by (rule disjI1)
next
assume "q ∨ r" thus ?R
proof (rule disjE)
assume "q" hence "p ∨ q" by (rule disjI2)
thus "(p ∨ q) ∨ r" by (rule disjI1)
next
assume "r" thus ?thesis by (rule disjI2)
qed
qed
(* benber cammonagu *)
lemma ejercicio_31_1:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
proof -
have "p ∨ (q ∨ r)" using assms .
moreover {
assume "p"
hence "p ∨ q" by (rule disjI1)
hence "(p ∨ q) ∨ r" by (rule disjI1)
}
moreover {
assume "q ∨ r"
moreover {
assume "q"
hence "p ∨ q" by (rule disjI2)
hence "(p ∨ q) ∨ r" by (rule disjI1)
}
moreover {
assume "r"
hence "(p ∨ q) ∨ r" by (rule disjI2)
}
ultimately have "(p ∨ q) ∨ r" by (rule disjE)
}
ultimately show "(p ∨ q) ∨ r" by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_32:
assumes 1: "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using 1 proof (rule disjE)
assume "p ∨ q" thus ?thesis
proof (rule disjE)
assume p thus ?thesis by (rule disjI1)
next
assume q hence "q ∨ r" by (rule disjI1)
thus ?thesis by (rule disjI2)
qed
next
assume r hence "q ∨ r" by (rule disjI2)
thus ?thesis by (rule disjI2)
qed
(* benber cammonagu *)
lemma ejercicio_32_1:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
proof -
have "(p ∨ q) ∨ r" using assms .
moreover {
assume "p ∨ q"
moreover {
assume "p"
hence ?thesis by (rule disjI1)
}
moreover {
assume "q"
hence "q ∨ r" by (rule disjI1)
hence ?thesis by (rule disjI2)
}
ultimately have ?thesis by (rule disjE)
}
moreover {
assume "r"
hence "q ∨ r" by (rule disjI2)
hence ?thesis by (rule disjI2)
}
ultimately show ?thesis by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 chrgencar gleherlop
alfmarcua pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_33:
assumes 1: "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 2: p using 1 by (rule conjunct1)
show ?thesis
proof (rule disjE)
assume 3: q have "p ∧ q" using 2 3 by (rule conjI)
thus ?thesis by (rule disjI1)
next
assume 4: r have "p ∧ r" using 2 4 by (rule conjI)
thus ?thesis by (rule disjI2)
next
show "q ∨ r" using 1 by (rule conjunct2)
qed
qed
(* benber cammonagu *)
lemma ejercicio_33_1:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have "p" using assms by (rule conjunct1)
have "q ∨ r" using assms by (rule conjunct2)
moreover {
assume "q"
with `p` have "p ∧ q" by (rule conjI)
hence ?thesis by (rule disjI1)
}
moreover {
assume "r"
with `p` have "p ∧ r" by (rule conjI)
hence ?thesis by (rule disjI2)
}
ultimately show ?thesis by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua
gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_34:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
using assms(1) proof (rule disjE)
assume 2: "p ∧ q" hence q by (rule conjunct2)
hence 3: "q ∨ r" by (rule disjI1)
have p using 2 by (rule conjunct1)
thus ?thesis using 3 by (rule conjI)
next
assume 4: "p ∧ r" hence r by (rule conjunct2)
hence 5: "q ∨ r" by (rule disjI2)
have p using 4 by (rule conjunct1)
thus ?thesis using 5 by (rule conjI)
qed
(* benber cammonagu *)
lemma ejercicio_34_1:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
proof -
have "(p ∧ q) ∨ (p ∧ r)" using assms .
moreover {
assume "p ∧ q"
hence "p" by (rule conjunct1)
moreover {
have "q" using `p ∧ q` by (rule conjunct2)
hence "q ∨ r" by (rule disjI1)
}
ultimately have ?thesis by (rule conjI)
}
moreover {
assume "p ∧ r"
hence "p" by (rule conjunct1)
moreover {
have "r" using `p ∧ r` by (rule conjunct2)
hence "q ∨ r" by (rule disjI2)
}
ultimately have ?thesis by (rule conjI)
}
ultimately show ?thesis by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua
gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
using assms(1) proof (rule disjE)
assume 1: p hence 2: "p ∨ r" by (rule disjI1)
have "p ∨ q" using 1 by (rule disjI1)
thus ?thesis using 2 by (rule conjI)
next
assume 3: "q ∧ r" hence r by (rule conjunct2)
hence 4: "p ∨ r" by (rule disjI2)
have q using 3 by (rule conjunct1)
hence "p ∨ q" by (rule disjI2)
thus ?thesis using 4 by (rule conjI)
qed
(* benber cammonagu *)
lemma ejercicio_35_1:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
proof -
have "p ∨ (q ∧ r)" using assms .
moreover {
assume "p"
hence "p ∨ q" by (rule disjI1)
moreover have "p ∨ r" using `p` by (rule disjI1)
ultimately have ?thesis by (rule conjI)
}
moreover {
assume "q ∧ r"
{
have "q" using `q ∧ r` by (rule conjunct1)
hence "p ∨ q" by (rule disjI2)
}
moreover {
have "r" using `q ∧ r` by (rule conjunct2)
hence "p ∨ r" by (rule disjI2)
}
ultimately have ?thesis by (rule conjI)
}
ultimately show ?thesis by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 chrgencar alfmarcua
gleherlop pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_36:
assumes 1: "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have 2: "p ∨ q" using 1 by (rule conjunct1)
have 3: "p ∨ r" using 1 by (rule conjunct2)
show ?thesis using 2
proof (rule disjE)
assume p thus ?thesis by (rule disjI1)
next
assume 4: q show ?thesis using 3
proof (rule disjE)
assume p thus ?thesis by (rule disjI1)
next
assume 5: r have "q ∧ r" using 4 5 by (rule conjI)
thus ?thesis by (rule disjI2)
qed
qed
qed
(* benber cammonagu *)
lemma ejercicio_36_1:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof -
have "p ∨ q" using assms by (rule conjunct1)
moreover {
assume "p"
hence ?thesis by (rule disjI1)
}
moreover {
assume "q"
have "p ∨ r" using assms by (rule conjunct2)
moreover {
assume "p"
hence ?thesis by (rule disjI1)
}
moreover {
assume "r"
with `q` have "q ∧ r" by (rule conjI)
hence ?thesis by (rule disjI2)
}
ultimately have ?thesis by (rule disjE)
}
ultimately show ?thesis by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_37:
assumes 1: "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof (rule impI)
have 2: "p ⟶ r" using 1 by (rule conjunct1)
have 3: "q ⟶ r" using 1 by (rule conjunct2)
assume 4: "p ∨ q" show "r" using 4
proof (rule disjE)
assume 5: "p" show "r" using 2 5 by (rule mp)
next
assume 6: "q" show "r" using 3 6 by (rule mp)
qed
qed
(* benber cammonagu *)
lemma ejercicio_37_1:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof
assume "p ∨ q"
moreover {
have "p ⟶ r" using assms by (rule conjunct1)
moreover assume "p"
ultimately have "r" by (rule mp)
}
moreover {
have "q ⟶ r" using assms by (rule conjunct2)
moreover assume "q"
ultimately have "r" by (rule mp)
}
ultimately show "r" by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
pabbergue antramhur enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof (rule conjI)
show "p ⟶ r"
proof (rule impI)
assume "p" hence 1: "p ∨ q" by (rule disjI1)
show "r" using assms(1) 1 by (rule mp)
qed
next
show "q ⟶ r"
proof (rule impI)
assume q hence 2: "p ∨ q" by (rule disjI2)
show r using assms(1) 2 by (rule mp)
qed
qed
(* benber cammonagu*)
lemma ejercicio_38_1:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof
show "p ⟶ r"
proof
assume "p"
hence "p ∨ q" by (rule disjI1)
with assms show "r" by (rule mp)
qed
next
show "q ⟶ r"
proof
assume "q"
hence "p ∨ q" by (rule disjI2)
with assms show "r" by (rule mp)
qed
qed
section {* Negaciones *}
text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}
(* pabalagon manperjim benber josgomrom4 raffergon2 gleherlop
marfruman1 chrgencar alfmarcua pabbergue enrparalv juacanrod
hugrubsan cammonagu alikan *)
lemma ejercicio_39:
assumes "p"
shows "¬¬p"
using assms(1) by (rule notnotI)
text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua pabbergue
gleherlop juacanrod enrparalv hugrubsan alikan *)
lemma ejercicio_40:
assumes 1: "¬p"
shows "p ⟶ q"
proof (rule impI)
assume 2: p show q using 1 2 by (rule notE)
qed
(* benber cammonagu *)
lemma ejercicio_40_1:
assumes "¬p"
shows "p ⟶ q"
proof
assume "p"
with `¬p` show "q" by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}
(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_41:
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof (rule impI)
assume 2: "¬q" show "¬p" using 1 2 by (rule mt)
qed
(* benber cammonagu *)
lemma ejercicio_41_1:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof
assume "¬q"
with `p ⟶ q` show "¬p" by (rule mt)
qed
text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}
(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
using assms(1) proof (rule disjE)
assume "p" thus "p" .
next
assume 2: "q" show "p" using assms(2) 2 by (rule notE)
qed
(* benber cammonagu *)
lemma ejercicio_42_1:
assumes "p∨q"
"¬q"
shows "p"
proof -
note `p ∨ q`
moreover have "p ⟹ p" .
moreover {
assume "q"
with `¬q` have "p" by (rule notE)
}
ultimately show "p" by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 43. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}
(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 alfmarcua
pabbergue gleherlop enrparalv juacanrod hugrubsan alikan *)
lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
using assms(1) proof (rule disjE)
assume 1: "p" show "q" using assms(2) 1 by (rule notE)
next
assume "q" thus "q" .
qed
(* benber cammonagu*)
lemma ejercicio_43_1:
assumes "p ∨ q"
"¬p"
shows "q"
proof -
note `p ∨ q`
moreover {
assume "p"
with `¬p` have "q" by (rule notE)
}
moreover have "q ⟹ q" .
ultimately show "q" by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 44. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}
(* pabalagon manperjim gleherlop josgomrom4 marfruman1 pabbergue
juacanrod hugrubsan alikan *)
lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof (rule notI)
assume 1: "¬p ∧ ¬q" hence 2: "¬p" by (rule conjunct1)
have 3: "¬q" using 1 by (rule conjunct2)
show "False"
using assms(1) proof (rule disjE)
assume 4: "p" show ?thesis using 2 4 by (rule notE)
next
assume 5: "q" show ?thesis using 3 5 by (rule notE)
qed
qed
(* benber alfmarcua cammonagu *)
lemma ejercicio_44_1:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof
assume "¬p ∧ ¬q"
note `p ∨ q`
moreover {
from `¬p ∧ ¬q` have "¬p" by (rule conjunct1)
moreover assume "p"
ultimately have "False" by (rule notE)
}
moreover {
from `¬p ∧ ¬q` have "¬q" by (rule conjunct2)
moreover assume "q"
ultimately have "False" by (rule notE)
}
ultimately show "False" by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue
juacanrod hugrubsan alikan *)
lemma ejercicio_45:
assumes 1: "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof (rule notI)
assume 2: "¬p ∨ ¬q" have 3: "p" using 1 by (rule conjunct1)
have 4: "q" using 1 by (rule conjunct2)
show "False" using 2
proof (rule disjE)
assume "¬p" thus ?thesis using 3 by (rule notE)
next
assume "¬q" thus ?thesis using 4 by (rule notE)
qed
qed
(* benber alfmarcua cammonagu *)
lemma ejercicio_45_1:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof
assume "¬p ∨ ¬q"
moreover {
assume "¬p"
moreover have "p" using `p ∧ q` by (rule conjunct1)
ultimately have "False" by (rule notE)
}
moreover {
assume "¬q"
moreover have "q" using `p ∧ q` by (rule conjunct2)
ultimately have "False" by (rule notE)
}
ultimately show False by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 gleherlop pabbergue
juacanrod hugrubsan alikan *)
lemma ejercicio_46:
assumes 1: "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
show "¬p"
proof (rule notI)
assume p hence 2: "p ∨ q" by (rule disjI1)
show False using 1 2 by (rule notE)
qed
show "¬q"
proof (rule notI)
assume q hence 3: "p ∨ q" by (rule disjI2)
show False using 1 3 by (rule notE)
qed
qed
(* benber cammmonagu *)
lemma ejercicio_46_1:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
show "¬p"
proof (rule ccontr)
assume "¬¬p"
hence "p" by (rule notnotD)
hence "p ∨ q" by (rule disjI1)
with assms show "False" by (rule notE)
qed
next
show "¬q"
proof (rule ccontr)
assume "¬¬q"
hence "q" by (rule notnotD)
hence "p ∨ q" by (rule disjI2)
with assms show "False" by (rule notE)
qed
qed
(* alfmarcua *)
lemma ejercicio_46_2:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
have "p ⟹ p ∨ q" by (rule disjI1)
then have "p ⟶ p ∨ q" by (rule impI)
then show "¬ p" using assms by (rule mt)
next
have "q ⟹ p ∨ q" by (rule disjI2)
then have "q ⟶ p ∨ q" by (rule impI)
then show "¬ q" using assms by (rule mt)
qed
text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 pabbregue juacanrod
hugrubsan alikan *)
lemma ejercicio_47:
assumes 1: "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule notI)
have 2: "¬p" using 1 by (rule conjunct1)
have 3: "¬q" using 1 by (rule conjunct2)
assume 4: "p ∨ q"
show False
using 4 proof (rule disjE)
assume 5: p show ?thesis using 2 5 by (rule notE)
next
assume 6: q show ?thesis using 3 6 by (rule notE)
qed
qed
(* benber gleherlop cammonagu*)
lemma ejercicio_47_1:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume "p ∨ q"
hence "¬(¬p ∧ ¬q)" by (rule ejercicio_44_1)
thus "False" using assms by (rule notE)
qed
(* alfmarcua *)
lemma ejercicio_47_2:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule notI)
have "¬ p" using assms by (rule conjunct1)
have "¬ q" using assms by (rule conjunct2)
assume "p ∨ q"
then have "q" using `¬ p` by (rule ejercicio_43)
show False using `¬ q` `q` by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 pabbergue juacanrod
hugrubsan alikan *)
lemma ejercicio_48:
assumes 1: "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule notI)
assume 2: "p ∧ q" hence 3: p by (rule conjunct1)
have 4: q using 2 by (rule conjunct2)
show False
using 1 proof (rule disjE)
assume "¬p" thus ?thesis using 3 by (rule notE)
next
assume "¬q" thus ?thesis using 4 by (rule notE)
qed
qed
(* benber alfmarcua gleherlop cammonagu *)
lemma ejercicio_48_1:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof
assume "p ∧ q"
hence "¬(¬p ∨ ¬q)" by (rule ejercicio_45_1)
thus "False" using assms by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 alfmarcu gleherlop
hugrubsan juacanrod cammonagu alikan *)
lemma ejercicio_49:
"¬(p ∧ ¬p)"
proof (rule notI)
assume 1: "p ∧ ¬p" hence 2: p by (rule conjunct1)
have "¬p" using 1 by (rule conjunct2)
thus "False" using 2 by (rule notE)
qed
(* benber *)
lemma ejercicio_49_1:
"¬(p ∧ ¬p)"
proof
assume "p ∧ ¬p"
hence "¬p" by (rule conjunct2)
moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
ultimately show "False" by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}
(* pabalagon manperjim raffergon2 josgomrom4 marfruman1 gleherlop
alfmarcua enrparalv pabbergue juacanrod hugrubsan alikan *)
lemma ejercicio_50:
assumes 1: "p ∧ ¬p"
shows "q"
proof (rule notE)
show p using 1 by (rule conjunct1)
show "¬p" using 1 by (rule conjunct2)
qed
(* benber cammonagu*)
lemma ejercicio_50_1:
assumes "p ∧ ¬p"
shows "q"
proof -
have "¬p" using `p ∧ ¬p` by (rule conjunct2)
moreover have "p" using `p ∧ ¬p` by (rule conjunct1)
ultimately show "q" by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}
(* pabalagon manperjim benber raffergon2 josgomrom4 marfruman1 gleherlop
alfmarcua enrparalv pabbergue juacanrod hugrubsan cammmonagu alikan *)
lemma ejercicio_51:
assumes "¬¬p"
shows "p"
using assms(1) by (rule notnotD)
text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 juacanrod pabbergue alikan *)
lemma ejercicio_52:
"p ∨ ¬p"
proof (rule ccontr)
assume 1: "¬(p ∨ ¬p)"
have 2: "¬p" proof (rule notI)
assume p hence 3: "p ∨ ¬p" by (rule disjI1)
show "False" using 1 3 by (rule notE)
qed
have 4: "p ∨ ¬p" using 2 by (rule disjI2)
show "False" using 1 4 by (rule notE)
qed
(* benber cammonagu *)
lemma ejercicio_52_1:
"p ∨ ¬p"
proof (rule ccontr)
assume "¬ (p ∨ ¬ p)"
hence "¬p ∧ ¬¬p" by (rule ejercicio_46_1)
hence "¬p" by (rule conjunct1)
moreover {
have "¬¬p" using `¬p ∧ ¬¬p` by (rule conjunct2)
hence "p" by (rule notnotD)
}
ultimately show "False" by (rule notE)
qed
(* alfmarcua *)
lemma ejercicio_52_2:
"p ∨ ¬p"
proof (rule ccontr)
assume "¬ (p ∨ ¬ p)"
then have "¬ p ∧ ¬¬ p" by (rule ejercicio_46)
then show False by (rule ejercicio_50)
qed
text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 alfmarcua gleherlop
juacanrod pabbergue *)
lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
assume 1: "(p ⟶ q) ⟶ p"
show p proof (rule ccontr)
assume 2: "¬p"
have 3: "¬(p ⟶ q)" using 1 2 by (rule mt)
have 4: "p ⟶ q" proof (rule impI)
assume 5: p show q using 2 5 by (rule notE)
qed
show False using 3 4 by (rule notE)
qed
qed
(* benber cammonagu *)
lemma ejercicio_53_1:
"((p ⟶ q) ⟶ p) ⟶ p"
proof
assume "(p ⟶ q) ⟶ p"
have "p ∨ ¬p" by (rule ejercicio_52_1)
moreover have "p ⟹ p" .
moreover {
assume "¬ p"
hence "p ⟶ q" by (rule ejercicio_40_1)
with `(p ⟶ q) ⟶ p` have "p" by (rule mp)
}
ultimately show "p" by (rule disjE)
qed
text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
pabbergue *)
lemma ejercicio_54:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
assume 2: "p" hence 3: "¬¬p" by (rule notnotI)
have "¬¬q" using 1 3 by (rule mt)
thus "q" by (rule notnotD)
qed
(* benber alfmarcua cammonagu *)
lemma ejercicio_54_1:
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
------------------------------------------------------------------ *}
(* pabalagon marfruman1*)
lemma ejercicio_55:
assumes 1: "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume 2: "¬(p ∨ q)"
have 3: "p"
proof (rule ccontr)
assume 4: "¬p"
have 5: "q"
proof (rule ccontr)
assume 6: "¬q" have 7: "¬p ∧ ¬q" using 4 6 by (rule conjI)
show False using 1 7 by (rule notE)
qed
have 8: "p ∨ q" using 5 by (rule disjI2)
show False using 2 8 by (rule notE)
qed
have 9: "p ∨ q" using 3 by (rule disjI1)
show False using 2 9 by (rule notE)
qed
(* benber alfmarcua josgomrom4 manperjim pabbergue juacanrod cammonagu *)
lemma ejercicio_55_1:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
hence "¬p ∧ ¬q" by (rule ejercicio_46_1)
with assms show False by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
pabbergue *)
lemma ejercicio_56:
assumes 1: "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule conjI)
show 3: p
proof (rule ccontr)
assume "¬p" hence 4: "¬p ∨ ¬q" by (rule disjI1)
show False using 1 4 by (rule notE)
qed
show 5: q
proof (rule ccontr)
assume "¬q" hence 6: "¬p ∨ ¬q" by (rule disjI2)
show False using 1 6 by (rule notE)
qed
qed
(* benber alfmarcua cammonagu *)
lemma ejercicio_56_1:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof -
have "¬¬p ∧ ¬¬q" using assms by (rule ejercicio_46_1)
hence "¬¬p" by (rule conjunct1)
hence "p" by (rule notnotD)
moreover {
have "¬¬q" using `¬¬p ∧ ¬¬q` by (rule conjunct2)
hence "q" by (rule notnotD)
}
ultimately show "p ∧ q" by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}
(* pabalagon manperjim marfruman1 josgomrom4 gleherlop juacanrod
pabbergue *)
lemma ejercicio_57:
assumes 1: "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume 2: "¬(¬p ∨ ¬q)"
show False using 1
proof (rule notE)
show 3: "p ∧ q"
proof (rule conjI)
show p
proof (rule ccontr)
assume "¬p" hence 4: "¬p ∨ ¬q" by (rule disjI1)
show False using 2 4 by (rule notE)
qed
next
show q
proof (rule ccontr)
assume "¬q" hence 5: "¬p ∨ ¬q" by (rule disjI2)
show False using 2 5 by (rule notE)
qed
qed
qed
qed
(* benber alfmarcua cammonagu *)
lemma ejercicio_57_1:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume "¬(¬p ∨ ¬q)"
hence "p ∧ q" by (rule ejercicio_56_1)
with assms show "False" by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
(* pabalagon manperjim josgomrom4 marfruman1 juacanrod pabbergue *)
lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "(p ⟶ q) ∨ ¬(p ⟶ q)" proof (rule ccontr)
assume 1: "¬((p ⟶ q) ∨ ¬(p ⟶ q))"
have 2: "¬(p ⟶ q)" proof (rule notI)
assume "p ⟶ q"
hence 3: "(p ⟶ q) ∨ ¬(p ⟶ q)" by (rule disjI1)
show False using 1 3 by (rule notE)
qed
hence 4: "(p ⟶ q) ∨ ¬(p ⟶ q)" by (rule disjI2)
show "False" using 1 4 by (rule notE)
qed
thus ?thesis proof (rule disjE)
assume "p ⟶ q" thus ?thesis by (rule disjI1)
next
assume 1: "¬(p ⟶ q)"
have "q ⟶ p" proof (rule impI)
assume 2: q
have 3: "p ⟶ q" proof (rule impI)
assume p show q using 2 .
qed
show p using 1 3 by (rule notE)
qed
thus ?thesis by (rule disjI2)
qed
qed
(* pabalagon gleherlop *)
lemma ejercicio_58_2:
"(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
assume 1: "¬((p ⟶ q) ∨ (q ⟶ p))"
hence 1: "(p ∧ ¬q) ∧ (q ∧ ¬p)" by simp
hence "p ∧ ¬q" ..
hence 2: p ..
have "q ∧ ¬p" using 1 ..
hence 3: "¬p" ..
show False using 3 2 by (rule notE)
qed
(* benber cammonagu *)
lemma ejercicio_58_1:
"(p ⟶ q) ∨ (q ⟶ p)"
proof (rule ccontr)
assume "¬ ((p ⟶ q) ∨ (q ⟶ p))"
hence 1: "¬(p ⟶ q) ∧ ¬(q ⟶ p)" by (rule ejercicio_46_1)
have "p ∨ ¬p" by (rule ejercicio_52_1)
moreover {
assume "p"
hence "q ⟶ p" by (rule ejercicio_7_1)
have "¬(q ⟶ p)" using 1 by (rule conjunct2)
hence "False" using `q ⟶ p` by (rule notE)
}
moreover {
assume "¬p"
hence "p ⟶ q" by (rule ejercicio_40_1)
have "¬(p ⟶ q)" using 1 by (rule conjunct1)
hence "False" using `p ⟶ q` by (rule notE)
}
ultimately show "False" by (rule disjE)
moreover {
assume "p"
hence "q ⟶ p" by (rule ejercicio_7_1)
have "¬(q ⟶ p)" using 1 by (rule conjunct2)
hence "False" using `q ⟶ p` by (rule notE)
}
qed
(* alfmarcua *)
lemma ejercicio_58_3:
"(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjE)
show "p ∨ ¬ p" by (rule ejercicio_52)
next
assume "¬p"
then have "p ⟶ q" by (rule ejercicio_40)
then show ?thesis by (rule disjI1)
next
assume "p"
then have "q ⟶ p" by (rule ejercicio_7)
then show ?thesis by (rule disjI2)
qed
end