Ejercicio 5 (a) - Historial de revisiones

WikiSysop: Texto reemplazado: «isar» por «isabelle»

2018-07-16T12:27:08Z

Texto reemplazado: «isar» por «isabelle»

Jalonso en 17:52 3 jun 2015

2015-06-03T17:52:22Z

Jalonso: Página creada con ' 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...'

2015-06-03T17:49:58Z

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...'

Página nueva

<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:
*}

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: \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q
· conjunct1: P \<and> Q \<Longrightarrow> P
· conjunct2: P \<and> Q \<Longrightarrow> Q
· notnotD: \<not>\<not> P \<Longrightarrow> P
· mp: \<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q
· impI: (P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q
· disjI1: P \<Longrightarrow> P \<or> Q
· disjI2: Q \<Longrightarrow> P \<or> Q
· disjE: \<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
· FalseE: False \<Longrightarrow> P
· notE: \<lbrakk>\<not>P; P\<rbrakk> \<Longrightarrow> R
· notI: (P \<Longrightarrow> False) \<Longrightarrow> \<not>P
· iffI: \<lbrakk>P \<Longrightarrow> Q; Q \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P = Q
· iffD1: \<lbrakk>Q = P; Q\<rbrakk> \<Longrightarrow> P
· iffD2: \<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P
· ccontr: (\<not>P \<Longrightarrow> False) \<Longrightarrow> P
. excluded_middle:(\<not>P \<or> P)

· allE: \<lbrakk>\<forall>x. P x; P x \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
· allI: (\<And>x. P x) \<Longrightarrow> \<forall>x. P x
· exI: P x \<Longrightarrow> \<exists>x. P x
· exE: \<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q

· refl: t = t
· subst: \<lbrakk>s = t; P s\<rbrakk> \<Longrightarrow> P t
· trans: \<lbrakk>r = s; s = t\<rbrakk> \<Longrightarrow> r = t
· sym: s = t \<Longrightarrow> t = s
· not_sym: t \<noteq> s \<Longrightarrow> s \<noteq> t
· ssubst: \<lbrakk>t = s; P s\<rbrakk> \<Longrightarrow> P t
· box_equals: \<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> a: = d
· arg_cong: x = y \<Longrightarrow> f x = f y
· fun_cong: f = g \<Longrightarrow> f x = g x
· cong: \<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> f x = g y
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación.
*}

lemma notnotI: "P \<Longrightarrow> \<not>\<not> P"
by auto

lemma mt: "\<lbrakk>F \<longrightarrow> G; \<not>G\<rbrakk> \<Longrightarrow> \<not>F"
by auto

lemma Ejercicio5:
shows "(\<exists>x. \<forall>y. \<not>(P(y) \<longrightarrow> R(x,y))) \<longrightarrow> \<not>(\<forall>x. P(x) \<longrightarrow> R(x,x))"
proof (rule impI)
assume "\<exists>x. \<forall>y. \<not>(P(y) \<longrightarrow> R(x,y))"
then obtain a where "\<forall>y. \<not>(P(y) \<longrightarrow> R(a,y))" by (rule exE)
show "\<not>(\<forall>x. P(x) \<longrightarrow> R(x,x))"
proof (rule notI)
assume "\<forall>x. P(x) \<longrightarrow> R(x,x)"
then have "P(a) \<longrightarrow> 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)
then show False using `P(a) \<longrightarrow> R(a,a)` by (rule notE)
qed
qed

end
</source>

← Revisión anterior		Revisión del 12:27 16 jul 2018
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
    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
-   · 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
-lemma mt: "\<lbrakk>F \<longrightarrow> G; \<not>G\<rbrakk> \<Longrightarrow> \<not>F"
+lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
 by auto
 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)
-   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)
-      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

Ejercicio 5 (a) - Historial de revisiones

WikiSysop: Texto reemplazado: «isar» por «isabelle»

Jalonso en 17:52 3 jun 2015

Jalonso: Página creada con ' 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...'

Jalonso: Página creada con ' 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...'