theory examen_1_31_may_DN imports Main begin text {* Demostrar o refutar los siguientes lemas usando sólo las reglas básicas de deducción natural de la lógica proposicional, de los cuantificadores y de la igualdad: · conjI: \P; Q\ \ P \ Q · conjunct1: P \ Q \ P · conjunct2: P \ Q \ Q · notnotD: \\ P \ P · mp: \P \ Q; P\ \ Q · 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 . excluded_middle:(\P \ P) · allE: \\x. P x; P x \ R\ \ R · allI: (\x. P x) \ \x. P x · exI: P x \ \x. P x · exE: \\x. P x; \x. P x \ Q\ \ Q · refl: t = t · subst: \s = t; P s\ \ P t · trans: \r = s; s = t\ \ r = t · sym: s = t \ t = s · not_sym: t \ s \ s \ t · ssubst: \t = s; P s\ \ P t · box_equals: \a = b; a = c; b = d\ \ a: = d · arg_cong: x = y \ f x = f y · fun_cong: f = g \ f x = g x · cong: \f = g; x = y\ \ f x = g y *} 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 lemma Ejercicio1: assumes "p \ q \ r \ s" "q \ \s" shows "p \ \q \ r" proof assume "p" show "\q \ r" proof- have "\q \ q" by (rule excluded_middle) thus "\q \ r" proof (rule disjE) assume "\q" thus "\q \ r" by (rule disjI1) next assume "q" with `p` have "p \ q" by (rule conjI) with assms(1) have "r \ s" by (rule mp) thus "\q \ r" proof (rule disjE) assume "r" thus "\q \ r" by (rule disjI2) next assume "s" hence "\\s" by (rule notnotI) with assms(2) have "\q" by (rule mt) thus "\q \ r" by (rule disjI1) qed qed qed qed lemma Ejercicio2: assumes "\x. (P(x) \ Q(x))" "\x. (\S(x) \ \Q(x))" "\ (\x. S(x))" shows "\x. \P(x)" proof (rule ccontr) assume 1: "\ (\x. \ P x)" have "\x. S(x)" proof fix a show "S(a)" proof (rule ccontr) assume "\ S a" have "\S(a) \ \Q(a)" using assms(2) by (rule allE) hence "\Q(a)" using `\ S a` by (rule mp) have "P(a) \ Q(a)" using assms(1) by (rule allE) hence "\P(a)" using `\Q(a)` by (rule mt) hence "\x. \P(x)" by (rule exI) with 1 show False by (rule notE) qed qed with assms(3) show False by (rule notE) qed end