header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}
theory e5_2_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. P(x) ⟶ R(x,x)) ⟶ (∀x. ∃y. R(x,y) ∨ ¬P(y))"
proof (rule impI)
assume "∀x. P(x) ⟶ R(x,x)"
show "∀x. ∃y. R(x,y) ∨ ¬P(y)"
proof (rule allI)
fix a
have "¬P(a) ∨ P(a)" ..
then show "∃y. R(a,y) ∨ ¬P(y)"
proof (rule disjE)
assume "¬P(a)"
then have "R(a,a) ∨ ¬P(a)" by (rule disjI2)
then show "∃y. R(a,y) ∨ ¬P(y)" by (rule exI)
next
assume "P(a)"
have "P(a) ⟶ R(a,a)" using `∀x. P(x) ⟶ R(x,x)` by (rule allE)
then have "R(a,a)" using `P(a)` by (rule mp)
then have "R(a,a) ∨ ¬P(a)" by (rule disjI1)
then show "∃y. R(a,y) ∨ ¬P(y)" by (rule exI)
qed
qed
qed
end
