chapter ‹R5: Deducción natural de primer orden›
theory R5_sol
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
· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀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
text ‹---------------------------------------------------------------
Ejercicio 1. Demostrar
∀x. P x ⟶ Q x ⊢ (∀x. P x) ⟶ (∀x. Q x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_1a:
"∀x. P x ⟶ Q x ⟹ (∀x. P x) ⟶ (∀x. Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_1b:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof
assume "∀x. P x"
show "∀x. Q x"
proof
fix a
have "P a" using ‹∀x. P x› ..
have "P a ⟶ Q a" using assms(1) ..
thus "Q a" using ‹P a› ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_1c:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof (rule impI)
assume "∀x. P x"
show "∀x. Q x"
proof (rule allI)
fix a
have "P a" using ‹∀x. P x› by (rule allE)
have "P a ⟶ Q a" using assms(1) by (rule allE)
thus "Q a" using ‹P a› by (rule mp)
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_1d:
"⟦∀x. P x ⟶ Q x⟧ ⟹(∀x. P x) ⟶ (∀x. Q x)"
apply (rule impI)
apply (rule allI)
apply (erule_tac x = x in allE)
apply (erule_tac x = x in allE)
apply (drule mp)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 2. Demostrar
∃x. ¬(P x) ⊢ ¬(∀x. P x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_2a: "∃x. ¬(P x) ⟹ ¬(∀x. P x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_2b:
assumes "∃x. ¬(P x)"
shows "¬(∀x. P x)"
proof
assume "∀x. P x"
obtain a where "¬(P a)" using assms(1) ..
have "P a" using ‹∀x. P x› ..
with ‹¬(P a)› show False ..
qed
― ‹La demostración detallada es›
lemma ejercicio_2c:
assumes "∃x. ¬(P x)"
shows "¬(∀x. P x)"
proof (rule notI)
assume "∀x. P x"
obtain a where "¬(P a)" using assms(1) by (rule exE)
have "P a" using ‹∀x. P x› by (rule allE)
with ‹¬(P a)› show False by (rule notE)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_2d: "⟦∃x. ¬(P x)⟧ ⟹ ¬(∀x. P x)"
apply (rule notI)
apply (erule exE)
apply (erule allE)
apply (erule notE)
apply assumption
done
text ‹---------------------------------------------------------------
Ejercicio 3. Demostrar
∀x. P x ⊢ ∀y. P y
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_3a: "∀x. P x ⟹ ∀y. P y"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_3b:
assumes "∀x. P x"
shows "∀y. P y"
proof
fix a
show "P a" using assms ..
qed
― ‹La demostración estructurada es›
lemma ejercicio_3c:
assumes "∀x. P x"
shows "∀y. P y"
proof (rule allI)
fix a
show "P a" using assms by (rule allE)
qed
― ‹La demostración estructurada es›
lemma ejercicio_3d: "⟦∀x. P x⟧ ⟹ ∀y. P y"
apply (rule allI)
apply (erule allE)
apply assumption
done
text ‹---------------------------------------------------------------
Ejercicio 4. Demostrar
∀x. P x ⟶ Q x ⊢ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_4a:
"∀x. P x ⟶ Q x ⟹ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_4b:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof
assume "∀x. ¬(Q x)"
show "∀x. ¬(P x)"
proof
fix a
show "¬(P a)"
proof
assume "P a"
have "P a ⟶ Q a" using assms ..
hence "Q a" using ‹P a› ..
have "¬(Q a)" using ‹∀x. ¬(Q x)› ..
thus False using ‹Q a› ..
qed
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_4c:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof (rule impI)
assume "∀x. ¬(Q x)"
show "∀x. ¬(P x)"
proof (rule allI)
fix a
show "¬(P a)"
proof
assume "P a"
have "P a ⟶ Q a" using assms by (rule allE)
hence "Q a" using ‹P a› by (rule mp)
have "¬(Q a)" using ‹∀x. ¬(Q x)› by (rule allE)
thus False using ‹Q a› by (rule notE)
qed
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_4d:
"⟦∀x. P x ⟶ Q x⟧⟹(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
apply (rule impI)
apply (rule allI)
apply (erule_tac x = x in allE)
apply (erule_tac x = x in allE)
apply (drule mt)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 5. Demostrar
∀x. P x ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_5a:
"∀x. P x ⟶ ¬(Q x) ⟹ ¬(∃x. P x ∧ Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_5b:
assumes "∀x. P x ⟶ ¬(Q x)"
shows "¬(∃x. P x ∧ Q x)"
proof
assume "∃x. P x ∧ Q x"
then obtain a where "P a ∧ Q a" ..
hence "P a" ..
have "P a ⟶ ¬(Q a)" using assms ..
hence "¬(Q a)" using ‹P a› ..
have "Q a" using ‹P a ∧ Q a› ..
with ‹¬(Q a)› show False ..
qed
― ‹La demostración estructurada es›
lemma ejercicio_5c:
assumes "∀x. P x ⟶ ¬(Q x)"
shows "¬(∃x. P x ∧ Q x)"
proof (rule notI)
assume "∃x. P x ∧ Q x"
then obtain a where "P a ∧ Q a" by (rule exE)
hence "P a" by (rule conjunct1)
have "P a ⟶ ¬(Q a)" using assms by (rule allE)
hence "¬(Q a)" using ‹P a› by (rule mp)
have "Q a" using ‹P a ∧ Q a› by (rule conjunct2)
with ‹¬(Q a)› show False by (rule notE)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_5d:
"⟦∀x. P x ⟶ ¬(Q x)⟧ ⟹ ¬(∃x. P x ∧ Q x)"
apply (rule notI)
apply (erule exE)
apply (frule conjunct2)
apply (rule notE)
apply (erule allE)
apply (drule mp)
apply (rule conjunct1)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 6. Demostrar
∀x y. P x y ⊢ ∀u v. P u v
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_6a:
"∀x y. P x y ⟹ ∀u v. P u v"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_6b:
assumes "∀x y. P x y"
shows "∀u v. P u v"
proof
fix a
show "∀v. P a v"
proof
fix b
have "∀y. P a y" using assms ..
thus "P a b" ..
qed
qed
― ‹La demostración estructurada simplificada es›
lemma ejercicio_6b2:
assumes "∀x y. P x y"
shows "∀u v. P u v"
proof (rule allI)+
fix a b
have "∀y. P a y" using assms ..
thus "P a b" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_6c:
assumes "∀x y. P x y"
shows "∀u v. P u v"
proof (rule allI)+
fix a b
have "∀y. P a y" using assms by (rule allE)
thus "P a b" by (rule allE)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_6e: "⟦∀x y. P x y ⟧ ⟹ ∀u v. P u v"
apply (rule allI)
apply (rule allI)
apply (erule allE)+
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 7. Demostrar
∃x y. P x y ⟹ ∃u v. P u v
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_7a:
"∃x y. P x y ⟹ ∃u v. P u v"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_7b:
assumes "∃x y. P x y"
shows "∃u v. P u v"
proof -
obtain a where "∃y. P a y" using assms ..
then obtain b where "P a b" ..
hence "∃v. P a v" ..
thus "∃u v. P u v" ..
qed
― ‹La demostración aplicativa es›
lemma ejercicio_7d: "⟦∃x y. P x y ⟧ ⟹ ∃u v. P u v"
apply (erule exE)+
apply (rule exI)
apply (rule exI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 8. Demostrar
∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_8a:
"∃x. ∀y. P x y ⟹ ∀y. ∃x. P x y"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_8b:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
proof
fix b
obtain a where "∀y. P a y" using assms ..
hence "P a b" ..
thus "∃x. P x b" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_8c:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
proof (rule allI)
fix b
obtain a where "∀y. P a y" using assms by (rule exE)
hence "P a b" by (rule allE)
thus "∃x. P x b" by (rule exI)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_8d: "⟦∃x. ∀y. P x y ⟧ ⟹ ∀y. ∃x. P x y"
apply (rule allI)
apply (rule exE)
apply assumption+
apply (rule allE)
apply assumption+
apply (rule exI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 9. Demostrar
∃x. P a ⟶ Q x ⊢ P a ⟶ (∃x. Q x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_9a:
"∃x. P a ⟶ Q x ⟹ P a ⟶ (∃x. Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_9b:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
proof
assume "P a"
obtain b where "P a ⟶ Q b" using assms ..
hence "Q b" using ‹P a› ..
thus "∃x. Q x" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_9c:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
proof (rule impI)
assume "P a"
obtain b where "P a ⟶ Q b" using assms by (rule exE)
hence "Q b" using ‹P a› by (rule mp)
thus "∃x. Q x" by (rule exI)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_9d: "⟦∃x. P a ⟶ Q x ⟧ ⟹ P a ⟶ (∃x. Q x)"
apply (rule impI)
apply (rule exE)
apply assumption+
apply (drule mp)
apply assumption+
apply (rule exI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 10. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------›
lemma ejercicio_10a:
"P a ⟶ (∃x. Q x) ⟹ ∃x. P a ⟶ Q x"
by auto
lemma ejercicio_10b:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof -
have "¬(P a) ∨ P a" ..
thus "∃x. P a ⟶ Q x"
proof
assume "¬(P a)"
have "P a ⟶ Q a"
proof
assume "P a"
with ‹¬(P a)› show "Q a" ..
qed
thus "∃x. P a ⟶ Q x" ..
next
assume "P a"
with assms have "∃x. Q x" by (rule mp)
then obtain b where "Q b" ..
have "P a ⟶ Q b"
proof
assume "P a"
note ‹Q b›
thus "Q b" .
qed
thus "∃x. P a ⟶ Q x" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_10c:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof -
have "¬(P a) ∨ P a" by (rule excluded_middle)
thus "∃x. P a ⟶ Q x"
proof (rule disjE)
assume "¬(P a)"
have "P a ⟶ Q a"
proof (rule impI)
assume "P a"
with ‹¬(P a)› show "Q a" by (rule notE)
qed
thus "∃x. P a ⟶ Q x" by (rule exI)
next
assume "P a"
with assms have "∃x. Q x" by (rule mp)
then obtain b where "Q b" by (rule exE)
have "P a ⟶ Q b"
proof (rule impI)
assume "P a"
note ‹Q b›
thus "Q b" by this
qed
thus "∃x. P a ⟶ Q x" by (rule exI)
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_10d:
"P a ⟶ (∃x. Q x) ⟹ ∃x. P a ⟶ Q x"
apply (cut_tac P="P a" in excluded_middle)
apply (erule disjE)
apply (rule exI)
apply (rule impI)
apply (erule notE, assumption)
apply (drule mp, assumption)
apply (erule exE)
apply (rule_tac x = "x" in exI)
apply (rule impI, assumption)
done
text ‹---------------------------------------------------------------
Ejercicio 11. Demostrar
(∃x. P x) ⟶ Q a ⊢ ∀x. P x ⟶ Q a
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_11a:
"(∃x. P x) ⟶ Q a ⟹ ∀x. P x ⟶ Q a"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_11b:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
proof
fix b
show "P b ⟶ Q a"
proof
assume "P b"
hence "∃x. P x" ..
with assms show "Q a" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_11c:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
proof (rule allI)
fix b
show "P b ⟶ Q a"
proof (rule impI)
assume "P b"
hence "∃x. P x" by (rule exI)
with assms show "Q a" by (rule mp)
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_11d: "⟦(∃x. P x) ⟶ Q a ⟧ ⟹ ∀x. P x ⟶ Q a"
apply (rule allI)
apply (rule impI)
apply (erule mp)
apply (rule exI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 12. Demostrar
∀x. P x ⟶ Q a ⊢ ∃ x. P x ⟶ Q a
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_12a:
"∀x. P x ⟶ Q a ⟹ ∃x. P x ⟶ Q a"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_12b:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
proof -
have "P b ⟶ Q a" using assms ..
thus "∃x. P x ⟶ Q a" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_12c:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
proof -
have "P b ⟶ Q a" using assms by (rule allE)
thus "∃x. P x ⟶ Q a" by (rule exI)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_12d: "⟦∀x. P x ⟶ Q a ⟧ ⟹ ∃x. P x ⟶ Q a"
apply (erule allE)
apply (rule exI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 13. Demostrar
(∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_13a:
"(∀x. P x) ∨ (∀x. Q x) ⟹ ∀x. P x ∨ Q x"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_13b:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
proof
fix a
note assms
thus "P a ∨ Q a"
proof
assume "∀x. P x"
hence "P a" ..
thus "P a ∨ Q a" ..
next
assume "∀x. Q x"
hence "Q a" ..
thus "P a ∨ Q a" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_13c:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
proof (rule allI)
fix a
note assms
thus "P a ∨ Q a"
proof (rule disjE)
assume "∀x. P x"
hence "P a" by (rule allE)
thus "P a ∨ Q a" by (rule disjI1)
next
assume "∀x. Q x"
hence "Q a" by (rule allE)
thus "P a ∨ Q a" by (rule disjI2)
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_13d: "⟦(∀x. P x) ∨ (∀x. Q x) ⟧ ⟹ ∀x. P x ∨ Q x"
apply (rule allI)
apply (rule disjE)
apply assumption+
apply (rule disjI1)
apply (rule allE)
apply assumption+
apply (rule disjI2)
apply (rule allE)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 14. Demostrar
∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_14a:
"∃x. P x ∧ Q x ⟹ (∃x. P x) ∧ (∃x. Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_14b:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
proof
obtain a where "P a ∧ Q a" using assms ..
hence "P a" ..
thus "∃x. P x" ..
next
obtain a where "P a ∧ Q a" using assms ..
hence "Q a" ..
thus "∃x. Q x" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_14c:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
proof (rule conjI)
obtain a where "P a ∧ Q a" using assms by (rule exE)
hence "P a" by (rule conjunct1)
thus "∃x. P x" by (rule exI)
next
obtain a where "P a ∧ Q a" using assms by (rule exE)
hence "Q a" by (rule conjunct2)
thus "∃x. Q x" by (rule exI)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_14e:
"⟦∃x. P x ∧ Q x⟧ ⟹ (∃x. P x) ∧ (∃x. Q x)"
apply (rule conjI)
apply (erule exE)
apply (rule exI)
apply (rule conjunct1)
apply assumption+
apply (erule exE)
apply (rule exI)
apply (rule conjunct2)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 15. Demostrar
∀x y. P y ⟶ Q x ⊢ (∃y. P y) ⟶ (∀x. Q x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_15a:
"∀x y. P y ⟶ Q x ⟹ (∃y. P y) ⟶ (∀x. Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_15b:
assumes "∀x y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
proof
assume "∃y. P y"
then obtain b where "P b" ..
show "∀x. Q x"
proof
fix a
have "∀y. P y ⟶ Q a" using assms ..
hence "P b ⟶ Q a" ..
thus "Q a" using ‹P b› ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_15c:
assumes "∀x y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
proof (rule impI)
assume "∃y. P y"
then obtain b where "P b" by (rule exE)
show "∀x. Q x"
proof (rule allI)
fix a
have "∀y. P y ⟶ Q a" using assms by (rule allE)
hence "P b ⟶ Q a" by (rule allE)
thus "Q a" using ‹P b› by (rule mp)
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_15d:
"⟦∀x y. P y ⟶ Q x⟧⟹(∃y. P y) ⟶ (∀x. Q x)"
apply (rule impI)
apply (rule allI)
apply (rule exE)
apply assumption+
apply (erule allE)
apply (rule allE)
apply assumption+
apply (rule mp)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 16. Demostrar
¬(∀x. ¬(P x)) ⊢ ∃x. P x
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_16a:
"¬(∀x. ¬(P x)) ⟹ ∃x. P x"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_16b:
assumes "¬(∀x. ¬(P x))"
shows "∃x. P x"
proof (rule ccontr)
assume "¬(∃x. P x)"
have "∀x. ¬(P x)"
proof
fix a
show "¬(P a)"
proof
assume "P a"
hence "∃x. P x" ..
with ‹¬(∃x. P x)› show False ..
qed
qed
with assms show False ..
qed
― ‹La demostración detallada es›
lemma ejercicio_16c:
assumes "¬(∀x. ¬(P x))"
shows "∃x. P x"
proof (rule ccontr)
assume "¬(∃x. P x)"
have "∀x. ¬(P x)"
proof (rule allI)
fix a
show "¬(P a)"
proof
assume "P a"
hence "∃x. P x" by (rule exI)
with ‹¬(∃x. P x)› show False by (rule notE)
qed
qed
with assms show False by (rule notE)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_16d:
"⟦¬(∀x. ¬(P x))⟧ ⟹ ∃x. P x"
apply (rule notnotD)
apply (rule notI)
apply (erule notE)
apply (rule allI)
apply (rule notI)
apply (erule notE)
apply (rule exI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 17. Demostrar
∀x. ¬(P x) ⊢ ¬(∃x. P x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_17a:
"∀x. ¬(P x) ⟹ ¬(∃x. P x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_17b:
assumes "∀x. ¬(P x)"
shows "¬(∃x. P x)"
proof
assume "∃x. P x"
then obtain a where "P a" ..
have "¬(P a)" using assms ..
thus False using ‹P a› ..
qed
― ‹La demostración detallada es›
lemma ejercicio_17c:
assumes "∀x. ¬(P x)"
shows "¬(∃x. P x)"
proof (rule notI)
assume "∃x. P x"
then obtain a where "P a" by (rule exE)
have "¬(P a)" using assms by (rule allE)
thus False using ‹P a› by (rule notE)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_17d:
"⟦∀x. ¬(P x)⟧ ⟹ ¬(∃x. P x)"
apply (rule notI)
apply (erule exE)
apply (rule notE)
apply (rule allE)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 18. Demostrar
∃x. P x ⊢ ¬(∀x. ¬(P x))
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_18a:
"∃x. P x ⟹ ¬(∀x. ¬(P x))"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_18b:
assumes "∃x. P x"
shows "¬(∀x. ¬(P x))"
proof
assume "∀x. ¬(P x)"
obtain a where "P a" using assms ..
have "¬(P a)" using ‹∀x. ¬(P x)› ..
thus False using ‹P a› ..
qed
― ‹La demostración detallada es›
lemma ejercicio_18c:
assumes "∃x. P x"
shows "¬(∀x. ¬(P x))"
proof (rule notI)
assume "∀x. ¬(P x)"
obtain a where "P a" using assms by (rule exE)
have "¬(P a)" using ‹∀x. ¬(P x)› by (rule allE)
thus False using ‹P a› by (rule notE)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_18d:
"∃x. P x ⟹ ¬(∀x. ¬(P x))"
apply (rule notI)
apply (erule exE)+
apply (erule allE)+
apply (rule notE)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 19. Demostrar
P a ⟶ (∀x. Q x) ⊢ ∀x. P a ⟶ Q x
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_19a:
"P a ⟶ (∀x. Q x) ⟹ ∀x. P a ⟶ Q x"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_19b:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
proof
fix b
show "P a ⟶ Q b"
proof
assume "P a"
with assms have "∀x. Q x" ..
thus "Q b" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_19c:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
proof (rule allI)
fix b
show "P a ⟶ Q b"
proof (rule impI)
assume "P a"
with assms have "∀x. Q x" by (rule mp)
thus "Q b" by (rule allE)
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_19d:
"P a ⟶ (∀x. Q x) ⟹ ∀x. P a ⟶ Q x"
apply (rule allI)
apply (rule impI)
apply (rule allE)
apply (rule mp)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 20. Demostrar
{∀x y z. R x y ∧ R y z ⟶ R x z,
∀x. ¬(R x x)}
⊢ ∀x y. R x y ⟶ ¬(R y x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_20a:
"⟦∀x y z. R x y ∧ R y z ⟶ R x z; ∀x. ¬(R x x)⟧ ⟹ ∀x y. R x y ⟶ ¬(R y x)"
by metis
― ‹La demostración estructurada es›
lemma ejercicio_20b:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof (rule allI)+
fix a b
show "R a b ⟶ ¬(R b a)"
proof
assume "R a b"
show "¬(R b a)"
proof
assume "R b a"
show False
proof -
have "R a b ∧ R b a" using ‹R a b› ‹R b a› ..
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) ..
hence "∀z. R a b ∧ R b z ⟶ R a z" ..
hence "R a b ∧ R b a ⟶ R a a" ..
hence "R a a" using ‹R a b ∧ R b a› ..
have "¬(R a a)" using assms(2) ..
thus False using ‹R a a› ..
qed
qed
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_20c:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof (rule allI)+
fix a b
show "R a b ⟶ ¬(R b a)"
proof (rule impI)
assume "R a b"
show "¬(R b a)"
proof (rule notI)
assume "R b a"
show False
proof -
have "R a b ∧ R b a" using ‹R a b› ‹R b a› by (rule conjI)
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
hence "R a b ∧ R b a ⟶ R a a" by (rule allE)
hence "R a a" using ‹R a b ∧ R b a› by (rule mp)
have "¬(R a a)" using assms(2) by (rule allE)
thus False using ‹R a a› by (rule notE)
qed
qed
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_20d:
"⟦∀x y z. R x y ∧ R y z ⟶ R x z; ∀x. ¬(R x x)⟧ ⟹
∀x y. R x y ⟶ ¬(R y x)"
apply (rule allI)+
apply (rule impI)
apply (erule_tac x = "x" in allE)
apply (erule_tac x = "x" in allE)
apply (erule_tac x = "y" in allE)
apply (erule_tac x = "x" in allE)
apply (rule notI)
apply (drule mp)
apply (rule conjI, assumption+)
apply (erule notE, assumption)
done
text ‹---------------------------------------------------------------
Ejercicio 21. Demostrar
{∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_21a:
"⟦∀x. P x ∨ Q x; ∃x. ¬(Q x); ∀x. R x ⟶ ¬(P x)⟧ ⟹ ∃x. ¬(R x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_21b:
assumes "∀x. P x ∨ Q x"
"∃x. ¬(Q x)"
"∀x. R x ⟶ ¬(P x)"
shows "∃x. ¬(R x)"
proof -
obtain a where "¬(Q a)" using assms(2) ..
have "P a ∨ Q a" using assms(1) ..
hence "P a"
proof
assume "P a"
thus "P a" .
next
assume "Q a"
with ‹¬(Q a)› show "P a" ..
qed
hence "¬¬(P a)" by (rule notnotI)
have "R a ⟶ ¬(P a)" using assms(3) ..
hence "¬(R a)" using ‹¬¬(P a)› by (rule mt)
thus "∃x. ¬(R x)" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_21c:
assumes "∀x. P x ∨ Q x"
"∃x. ¬(Q x)"
"∀x. R x ⟶ ¬(P x)"
shows "∃x. ¬(R x)"
proof -
obtain a where "¬(Q a)" using assms(2) by (rule exE)
have "P a ∨ Q a" using assms(1) by (rule allE)
hence "P a"
proof (rule disjE)
assume "P a"
thus "P a" by this
next
assume "Q a"
with ‹¬(Q a)› show "P a" by (rule notE)
qed
hence "¬¬(P a)" by (rule notnotI)
have "R a ⟶ ¬(P a)" using assms(3) by (rule allE)
hence "¬(R a)" using ‹¬¬(P a)› by (rule mt)
thus "∃x. ¬(R x)" by (rule exI)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_21d:
"⟦∀x. P x ∨ Q x;∃x. ¬(Q x);∀x. R x ⟶ ¬(P x)⟧ ⟹
∃x. ¬(R x)"
apply (erule exE)
apply (rule_tac x = "x" in exI)
apply (rule notI)
apply (erule_tac x = "x" in allE)
apply (erule disjE)
apply (erule_tac x = "x" in allE)
apply (drule mp, assumption)
apply (erule_tac P = "P x" in notE, assumption)
apply (erule_tac P = "Q x" in notE, assumption)
done
text ‹---------------------------------------------------------------
Ejercicio 22. Demostrar
{∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_22a:
"⟦∀x. P x ⟶ Q x ∨ R x; ¬(∃x. P x ∧ R x)⟧ ⟹ ∀x. P x ⟶ Q x"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_22b:
assumes "∀x. P x ⟶ Q x ∨ R x"
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
proof
fix a
show "P a ⟶ Q a"
proof
assume "P a"
have "P a ⟶ Q a ∨ R a" using assms(1) ..
hence "Q a ∨ R a" using ‹P a› ..
thus "Q a"
proof
assume "Q a"
thus "Q a" .
next
assume "R a"
with ‹P a› have "P a ∧ R a" ..
hence "∃x. P x ∧ R x" ..
with assms(2) show "Q a" ..
qed
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_22c:
assumes "∀x. P x ⟶ Q x ∨ R x"
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
proof (rule allI)
fix a
show "P a ⟶ Q a"
proof (rule impI)
assume "P a"
have "P a ⟶ Q a ∨ R a" using assms(1) by (rule allE)
hence "Q a ∨ R a" using ‹P a› by (rule mp)
thus "Q a"
proof (rule disjE)
assume "Q a"
thus "Q a" by this
next
assume "R a"
with ‹P a› have "P a ∧ R a" by (rule conjI)
hence "∃x. P x ∧ R x" by (rule exI)
with assms(2) show "Q a" by (rule notE)
qed
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_22d:
"⟦∀x. P x ⟶ Q x ∨ R x;¬(∃x. P x ∧ R x)⟧ ⟹ ∀x. P x ⟶ Q x"
apply (rule allI)
apply (rule impI)
apply (rule disjE)
apply (erule allE)
apply (rule mp)
apply assumption+
apply (rule notE)
apply assumption+
apply (rule exI)
apply (erule conjI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 23. Demostrar
∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_23a:
"∃x y. R x y ∨ R y x ⟹ ∃x y. R x y"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_23b:
assumes "∃x y. R x y ∨ R y x"
shows "∃x y. R x y"
proof -
obtain a where "∃y. R a y ∨ R y a" using assms ..
then obtain b where "R a b ∨ R b a" ..
thus "∃x y. R x y"
proof
assume "R a b"
hence "∃y. R a y" ..
thus "∃ x y. R x y" ..
next
assume "R b a"
hence "∃y. R b y" ..
thus "∃ x y. R x y" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_23c:
assumes "∃x y. R x y ∨ R y x"
shows "∃x y. R x y"
proof -
obtain a where "∃y. R a y ∨ R y a" using assms by (rule exE)
then obtain b where "R a b ∨ R b a" by (rule exE)
thus "∃x y. R x y"
proof (rule disjE)
assume "R a b"
hence "∃y. R a y" by (rule exI)
thus "∃ x y. R x y" by (rule exI)
next
assume "R b a"
hence "∃y. R b y" by (rule exI)
thus "∃ x y. R x y" by (rule exI)
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_23d:
"⟦∃x y. R x y ∨ R y x⟧ ⟹ ∃x y. R x y"
apply (erule exE)+
apply (erule disjE)
apply (rule exI)
apply (rule exI)
apply assumption+
apply (rule exI)
apply (rule exI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 24. Demostrar
(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_24a: "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_24b: "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof
assume "∃x. ∀y. P x y"
then obtain a where "∀y. P a y" ..
show "∀y. ∃x. P x y"
proof
fix b
have "P a b" using ‹∀y. P a y› ..
thus "∃x. P x b" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_24c: "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof (rule impI)
assume "∃x. ∀y. P x y"
then obtain a where "∀y. P a y" by (rule exE)
show "∀y. ∃x. P x y"
proof (rule allI)
fix b
have "P a b" using ‹∀y. P a y› by (rule allE)
thus "∃x. P x b" by (rule exI)
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_24d:
"(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
apply (rule impI)
apply (rule allI)
apply (erule exE)
apply (erule allE)
apply (rule exI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 25. Demostrar
(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_25a: "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_25b: "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
proof
assume "∀x. P x ⟶ Q"
show "(∃x. P x) ⟶ Q"
proof
assume "∃x. P x"
then obtain a where "P a" ..
have "P a ⟶ Q" using ‹∀x. P x ⟶ Q› ..
thus "Q" using ‹P a› ..
qed
next
assume "(∃x. P x) ⟶ Q"
show "∀x. P x ⟶ Q"
proof
fix b
show "P b ⟶ Q"
proof
assume "P b"
hence "∃x. P x" ..
with ‹(∃x. P x) ⟶ Q› show "Q" ..
qed
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_25c: "(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
proof (rule iffI)
assume "∀x. P x ⟶ Q"
show "(∃x. P x) ⟶ Q"
proof (rule impI)
assume "∃x. P x"
then obtain a where "P a" by (rule exE)
have "P a ⟶ Q" using ‹∀x. P x ⟶ Q› by (rule allE)
thus "Q" using ‹P a› by (rule mp)
qed
next
assume "(∃x. P x) ⟶ Q"
show "∀x. P x ⟶ Q"
proof (rule allI)
fix b
show "P b ⟶ Q"
proof (rule impI)
assume "P b"
hence "∃x. P x" by (rule exI)
with ‹(∃x. P x) ⟶ Q› show "Q" by (rule mp)
qed
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_25d:
"(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
apply (rule iffI)
prefer 2
apply (rule allI)
apply (rule impI)
apply (rule mp)
apply assumption+
apply (rule exI)
apply assumption+
apply (rule impI)
apply (erule exE)
apply (erule allE)
apply (rule mp)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 26. Demostrar
((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_26a: "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_26b: "((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
proof
assume "(∀x. P x) ∧ (∀x. Q x)"
show "∀x. P x ∧ Q x"
proof
fix a
have "∀x. P x" using ‹(∀x. P x) ∧ (∀x. Q x)› ..
have "∀x. Q x" using ‹(∀x. P x) ∧ (∀x. Q x)› ..
hence "Q a" ..
have "P a" using ‹∀x. P x› ..
thus "P a ∧ Q a" using ‹Q a› ..
qed
next
assume "∀x. P x ∧ Q x"
have "∀x. P x"
proof
fix a
have "P a ∧ Q a" using ‹∀x. P x ∧ Q x› ..
thus "P a" ..
qed
moreover have "∀x. Q x"
proof
fix a
have "P a ∧ Q a" using ‹∀x. P x ∧ Q x› ..
thus "Q a" ..
qed
ultimately show "(∀x. P x) ∧ (∀x. Q x)" ..
qed
― ‹La demostración detallada es›
lemma ejercicio_26c: "((∀x. P x) ∧ (∀x. Q x)) = (∀x. P x ∧ Q x)"
proof (rule iffI)
assume "(∀x. P x) ∧ (∀x. Q x)"
show "∀x. P x ∧ Q x"
proof (rule allI)
fix a
have "∀x. P x" using ‹(∀x. P x) ∧ (∀x. Q x)› by (rule conjunct1)
have "∀x. Q x" using ‹(∀x. P x) ∧ (∀x. Q x)› by (rule conjunct2)
hence "Q a" by (rule allE)
have "P a" using ‹∀x. P x› by (rule allE)
thus "P a ∧ Q a" using ‹Q a› by (rule conjI)
qed
next
assume "∀x. P x ∧ Q x"
have "∀x. P x"
proof (rule allI)
fix a
have "P a ∧ Q a" using ‹∀x. P x ∧ Q x› by (rule allE)
thus "P a" by (rule conjunct1)
qed
moreover have "∀x. Q x"
proof (rule allI)
fix a
have "P a ∧ Q a" using ‹∀x. P x ∧ Q x› by (rule allE)
thus "Q a" by (rule conjunct2)
qed
ultimately show "(∀x. P x) ∧ (∀x. Q x)" by (rule conjI)
qed
― ‹La demostración aplicativa es›
lemma ejercicio_26d:
"((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
apply (rule iffI)
prefer 2
apply (rule conjI)
apply (rule allI)
apply (erule allE)
apply (erule conjunct1)
apply (rule allI)
apply (erule allE)
apply (erule conjunct2)
apply (rule allI)
apply (frule conjunct1)
apply (frule conjunct2)
apply (erule allE)+
apply (rule conjI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 27. Demostrar o refutar
((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)
------------------------------------------------------------------›
lemma ejercicio_27: "((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
oops
(*
Auto Quickcheck found a counterexample:
P = {a⇩1}
Q = {a⇩2}
*)
text ‹---------------------------------------------------------------
Ejercicio 28. Demostrar o refutar
((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_28a:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_28b:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
proof
assume "(∃x. P x) ∨ (∃x. Q x)"
thus "∃x. P x ∨ Q x"
proof
assume "∃x. P x"
then obtain a where "P a" ..
hence "P a ∨ Q a" ..
thus "∃x. P x ∨ Q x" ..
next
assume "∃x. Q x"
then obtain a where "Q a" ..
hence "P a ∨ Q a" ..
thus "∃x. P x ∨ Q x" ..
qed
next
assume "∃x. P x ∨ Q x"
then obtain a where "P a ∨ Q a" ..
thus "(∃x. P x) ∨ (∃x. Q x)"
proof
assume "P a"
hence "∃x. P x" ..
thus "(∃x. P x) ∨ (∃x. Q x)" ..
next
assume "Q a"
hence "∃x. Q x" ..
thus "(∃x. P x) ∨ (∃x. Q x)" ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_28c:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
proof (rule iffI)
assume "(∃x. P x) ∨ (∃x. Q x)"
thus "∃x. P x ∨ Q x"
proof (rule disjE)
assume "∃x. P x"
then obtain a where "P a" by (rule exE)
hence "P a ∨ Q a" by (rule disjI1)
thus "∃x. P x ∨ Q x" by (rule exI)
next
assume "∃x. Q x"
then obtain a where "Q a" by (rule exE)
hence "P a ∨ Q a" by (rule disjI2)
thus "∃x. P x ∨ Q x" by (rule exI)
qed
next
assume "∃x. P x ∨ Q x"
then obtain a where "P a ∨ Q a" by (rule exE)
thus "(∃x. P x) ∨ (∃x. Q x)"
proof (rule disjE)
assume "P a"
hence "∃x. P x" by (rule exI)
thus "(∃x. P x) ∨ (∃x. Q x)" by (rule disjI1)
next
assume "Q a"
hence "∃x. Q x" by (rule exI)
thus "(∃x. P x) ∨ (∃x. Q x)" by (rule disjI2)
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_28d:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
apply (rule iffI)
apply (erule disjE)
apply (erule exE)
apply (drule disjI1)
apply (rule exI)
apply assumption+
apply (erule exE)
apply (drule disjI2)
apply (rule exI)
apply assumption+
apply (erule exE)
apply (erule disjE)
apply (rule disjI1)
apply (rule exI)
apply assumption+
apply (rule disjI2)
apply (rule exI)
apply assumption+
done
text ‹---------------------------------------------------------------
Ejercicio 29. Demostrar o refutar
(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
------------------------------------------------------------------›
lemma ejercicio_29:
"(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
quickcheck
(*
Quickcheck found a counterexample:
P = (λx. undefined)((a⇩1 := {a⇩2}, a⇩2 := {a⇩1})
*)
oops
text ‹---------------------------------------------------------------
Ejercicio 30. Demostrar o refutar
(¬(∀x. P x)) ⟷ (∃x. ¬P x)
------------------------------------------------------------------›
― ‹La demostración automática es›
lemma ejercicio_30a:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
by auto
― ‹La demostración estructurada es›
lemma ejercicio_30b:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof
assume "¬(∀x. P x)"
show "∃x. ¬P x"
proof (rule ccontr)
assume "¬(∃x. ¬P x)"
have "∀x. P x"
proof
fix a
show "P a"
proof (rule ccontr)
assume "¬P a"
hence "∃x. ¬P x" ..
with ‹¬(∃x. ¬P x)› show False ..
qed
qed
with ‹¬(∀x. P x)› show False ..
qed
next
assume "∃x. ¬P x"
then obtain a where "¬P a" ..
show "¬(∀x. P x)"
proof
assume "∀x. P x"
hence "P a" ..
with ‹¬P a› show False ..
qed
qed
― ‹La demostración detallada es›
lemma ejercicio_30c:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof (rule iffI)
assume "¬(∀x. P x)"
show "∃x. ¬P x"
proof (rule ccontr)
assume "¬(∃x. ¬P x)"
have "∀x. P x"
proof (rule allI)
fix a
show "P a"
proof (rule ccontr)
assume "¬P a"
hence "∃x. ¬P x" by (rule exI)
with ‹¬(∃x. ¬P x)› show False by (rule notE)
qed
qed
with ‹¬(∀x. P x)› show False by (rule notE)
qed
next
assume "∃x. ¬P x"
then obtain a where "¬P a" by (rule exE)
show "¬(∀x. P x)"
proof (rule notI)
assume "∀x. P x"
hence "P a" by (rule allE)
show False using ‹¬P a› ‹P a› by (rule notE)
qed
qed
― ‹La demostración aplicativa es›
lemma ejercicio_30d:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
apply (rule iffI)
apply (rule notnotD)
apply (rule notI)
apply (erule notE)
apply (rule allI)
apply (rule notnotD)
apply (rule notI)
apply (erule notE)
apply (rule exI)
apply assumption+
apply (erule exE)
apply (rule notI)
apply (erule allE)
apply (erule notE)
apply assumption+
done
end
![Lógica matemática y fundamentos [Curso 2019-20]](/~jalonso/imagenes/logoUS.jpg)