Acciones

Diferencia entre revisiones de «Ejercicio 5 (a)»

De Lógica matemática y fundamentos (2014-15)

(Página creada con '<source lang="isar"> header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *} theory e5_1_sol imports Main begin text {* Apellidos: Nombre: *} tex...')
 
m (Texto reemplazado: «isar» por «isabelle»)
 
(No se muestra una edición intermedia de otro usuario)
Línea 1: Línea 1:
−
<source lang="isar">
+
<source lang="isabelle">
 
header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}
 
header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}
  
Línea 19: Línea 19:
 
   básicas de deducción natural de la lógica proposicional, de los
 
   básicas de deducción natural de la lógica proposicional, de los
 
   cuantificadores y de la igualdad:  
 
   cuantificadores y de la igualdad:  
−
   · conjI:      \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q
+
   · conjI:      ⟦P; Q⟧ ⟹ P ∧ Q
−
   · conjunct1:  P \<and> Q \<Longrightarrow> P
+
   · conjunct1:  P ∧ Q ⟹ P
−
   · conjunct2:  P \<and> Q \<Longrightarrow> Q   
+
   · conjunct2:  P ∧ Q ⟹ Q   
−
   · notnotD:    \<not>\<not> P \<Longrightarrow> P
+
   · notnotD:    ¬¬ P ⟹ P
−
   · mp:        \<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q  
+
   · mp:        ⟦P ⟶ Q; P⟧ ⟹ Q  
−
   · impI:      (P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q
+
   · impI:      (P ⟹ Q) ⟹ P ⟶ Q
−
   · disjI1:    P \<Longrightarrow> P \<or> Q
+
   · disjI1:    P ⟹ P ∨ Q
−
   · disjI2:    Q \<Longrightarrow> P \<or> Q
+
   · disjI2:    Q ⟹ P ∨ Q
−
   · disjE:      \<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R  
+
   · disjE:      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R  
−
   · FalseE:    False \<Longrightarrow> P
+
   · FalseE:    False ⟹ P
−
   · notE:      \<lbrakk>\<not>P; P\<rbrakk> \<Longrightarrow> R
+
   · notE:      ⟦¬P; P⟧ ⟹ R
−
   · notI:      (P \<Longrightarrow> False) \<Longrightarrow> \<not>P
+
   · notI:      (P ⟹ False) ⟹ ¬P
−
   · iffI:      \<lbrakk>P \<Longrightarrow> Q; Q \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P = Q
+
   · iffI:      ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
−
   · iffD1:      \<lbrakk>Q = P; Q\<rbrakk> \<Longrightarrow> P  
+
   · iffD1:      ⟦Q = P; Q⟧ ⟹ P  
−
   · iffD2:      \<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P
+
   · iffD2:      ⟦P = Q; Q⟧ ⟹ P
−
   · ccontr:    (\<not>P \<Longrightarrow> False) \<Longrightarrow> P
+
   · ccontr:    (¬P ⟹ False) ⟹ P
−
   . excluded_middle:(\<not>P \<or> P)  
+
   . excluded_middle:(¬P ∨ P)  
  
−
   · allE:      \<lbrakk>\<forall>x. P x; P x \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
+
   · allE:      ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
−
   · allI:      (\<And>x. P x) \<Longrightarrow> \<forall>x. P x
+
   · allI:      (⋀x. P x) ⟹ ∀x. P x
−
   · exI:        P x \<Longrightarrow> \<exists>x. P x
+
   · exI:        P x ⟹ ∃x. P x
−
   · exE:        \<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q
+
   · exE:        ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
  
 
   · refl:      t = t
 
   · refl:      t = t
−
   · subst:      \<lbrakk>s = t; P s\<rbrakk> \<Longrightarrow> P t
+
   · subst:      ⟦s = t; P s⟧ ⟹ P t
−
   · trans:      \<lbrakk>r = s; s = t\<rbrakk> \<Longrightarrow> r = t
+
   · trans:      ⟦r = s; s = t⟧ ⟹ r = t
−
   · sym:        s = t \<Longrightarrow> t = s
+
   · sym:        s = t ⟹ t = s
−
   · not_sym:    t \<noteq> s \<Longrightarrow> s \<noteq> t
+
   · not_sym:    t ≠ s ⟹ s ≠ t
−
   · ssubst:    \<lbrakk>t = s; P s\<rbrakk> \<Longrightarrow> P t
+
   · ssubst:    ⟦t = s; P s⟧ ⟹ P t
−
   · box_equals: \<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> a: = d
+
   · box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
−
   · arg_cong:  x = y \<Longrightarrow> f x = f y
+
   · arg_cong:  x = y ⟹ f x = f y
−
   · fun_cong:  f = g \<Longrightarrow> f x = g x
+
   · fun_cong:  f = g ⟹ f x = g x
−
   · cong:      \<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> f x = g y
+
   · cong:      ⟦f = g; x = y⟧ ⟹ f x = g y
 
*}
 
*}
  
Línea 58: Línea 58:
 
   *}
 
   *}
  
−
lemma notnotI: "P \<Longrightarrow> \<not>\<not> P"
+
lemma notnotI: "P ⟹ ¬¬ P"
 
by auto
 
by auto
  
−
lemma mt: "\<lbrakk>F \<longrightarrow> G; \<not>G\<rbrakk> \<Longrightarrow> \<not>F"
+
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
 
by auto
 
by auto
  
 
lemma Ejercicio5:
 
lemma Ejercicio5:
−
   shows "(\<exists>x. \<forall>y. \<not>(P(y) \<longrightarrow> R(x,y)))  \<longrightarrow> \<not>(\<forall>x. P(x) \<longrightarrow> R(x,x))"
+
   shows "(∃x. ∀y. ¬(P(y) ⟶ R(x,y)))  ⟶ ¬(∀x. P(x) ⟶ R(x,x))"
 
proof (rule impI)
 
proof (rule impI)
−
   assume "\<exists>x. \<forall>y. \<not>(P(y) \<longrightarrow> R(x,y))"
+
   assume "∃x. ∀y. ¬(P(y) ⟶ R(x,y))"
−
   then obtain a where "\<forall>y. \<not>(P(y) \<longrightarrow> R(a,y))" by (rule exE)
+
   then obtain a where "∀y. ¬(P(y) ⟶ R(a,y))" by (rule exE)
−
   show "\<not>(\<forall>x. P(x) \<longrightarrow> R(x,x))"
+
   show "¬(∀x. P(x) ⟶ R(x,x))"
 
   proof (rule notI)
 
   proof (rule notI)
−
     assume "\<forall>x. P(x) \<longrightarrow> R(x,x)"
+
     assume "∀x. P(x) ⟶ R(x,x)"
−
     then have "P(a) \<longrightarrow> R(a,a)" by (rule allE)
+
     then have "P(a) ⟶ R(a,a)" by (rule allE)
−
     have "\<not>(P(a) \<longrightarrow> R(a,a))" using `\<forall>y. \<not>(P(y) \<longrightarrow> R(a,y))` 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) \<longrightarrow> R(a,a)` by (rule notE)
+
     then show False using `P(a) ⟶ R(a,a)` by (rule notE)
 
   qed
 
   qed
 
qed
 
qed

Revisión actual del 14:27 16 jul 2018

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
Obtenido de «https://www.glc.us.es/~jalonso/LMF2015/index.php?title=Ejercicio_5_(a)&oldid=343»