header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}
theory e5_1_sol
imports Main
begin
text {*
Apellidos:
Nombre:
*}
text {* Sustituye la palabra uvus por tu usuario de la Universidad de
Sevilla y graba el fichero con dicho usuario .thy
*}
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 Ejercicio5:
shows "(∃x. ∀y. ¬(P(y) ⟶ R(x,y))) ⟶ ¬(∀x. P(x) ⟶ R(x,x))"
proof (rule impI)
assume "∃x. ∀y. ¬(P(y) ⟶ R(x,y))"
then obtain a where "∀y. ¬(P(y) ⟶ R(a,y))" by (rule exE)
show "¬(∀x. P(x) ⟶ R(x,x))"
proof (rule notI)
assume "∀x. P(x) ⟶ R(x,x)"
then have "P(a) ⟶ R(a,a)" by (rule allE)
have "¬(P(a) ⟶ R(a,a))" using `∀y. ¬(P(y) ⟶ R(a,y))` by (rule allE)
then show False using `P(a) ⟶ R(a,a)` by (rule notE)
qed
qed
end