Mjoseh en 09:51 14 may 2020

2020-05-14T09:51:03Z

Mjoseh en 09:55 10 may 2020

2020-05-10T09:55:42Z

Mjoseh: Protegió «T1 sol» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

2020-05-04T09:54:58Z

Protegió «T1 sol» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « text ‹Tarea 1 de Lógica Matemática y Fundamentos (24-abril-2020)› theory Tarea_1_sol imports Main begin lemma notnotI: "P ⟹ ¬¬ P"…»

2020-05-04T09:54:31Z

Página creada con «<source lang = "isabelle"> text ‹Tarea 1 de Lógica Matemática y Fundamentos (24-abril-2020)› theory Tarea_1_sol imports Main begin lemma notnotI: "P ⟹ ¬¬ P"…»

Página nueva

<source lang = "isabelle">
text ‹Tarea 1 de Lógica Matemática y Fundamentos (24-abril-2020)›

theory Tarea_1_sol
imports Main
begin

lemma notnotI: "P ⟹ ¬¬ P"
by auto

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text ‹Ejercicio: Formalizar la siguiente argumentación

Hay un profesor que agrada a todos los estudiantes a los que
agrada al menos un profesor. A todo estudiante le agrada uno u otro
profesor.
(a) Demostrar que hay un profesor que agrada a todos los estudiantes.
(b) ¿Hay un profesor que no agrade a ningún estudiante?

Simbología: P(x): x es un profesor, E(x): x es estudiante, A(x,y):
a x le agrada y.

Notas:
(1) No usar ninguno de los métodos automáticos: simp, simp_all,
auto, blast, force, fast, arith o metis.
(2) Se pueden establecer lemas auxiliares si se consideran útilies,
siempre que su demostración se realice de forma detallada, sin
usarlos métodos automáticos.›

― ‹(1) Demostración automática›
lemma
assumes "∃x. P(x) ∧ (∀y. E(y) ∧ (∃z. P(z) ∧ A(y,z)) ⟶ A(y,x))"
"∀y. E(y) ⟶ (∃x. P(x) ∧ A(y,x))"
shows "∃x. P(x) ∧ (∀y. E(y) ⟶ A(y,x))"
using assms by auto

― ‹(1) Demostración natural:
Tenemos
h1: ∃x. P(x) ∧ (∀y. E(y) ∧ (∃z. P(z) ∧ A(y,z)) ⟶ A(y,x))
h2: ∀y. E(y) ⟶ (∃x. P(x) ∧ A(y,x))

+ De h1, usando la regla exE, se obtiene a tal que
1: P(a) ∧ (∀y. E(y) ∧ (∃z. P(z) ∧ A(y,z)) ⟶ A(y,a))

De 1, usando las reglas de eliminación de la conjunción (conjunct1
y conjunct2) se obtiene
2: P(a)
3: ∀y. E(y) ∧ (∃z. P(z) ∧ A(y,z)) ⟶ A(y,a)

Veamos que a es el elemento que verifica las condiciones de la tesis.
Por 2, se verifica P(a). Por tanto, es suficiente probar
∀y. E(y) ⟶ A(y,a)
+ Para ello, por la regla allI, dado b cualquiera, hay que probar
E(y) ⟶ A(y,a)
+ Para ello, por la regla impI,
supuesto 4: E(b)
hay que probar A(b,a). En efecto:
+ De 3, usando la regla allE, se tiene
4: E(b) ∧ (∃z. P(z) ∧ A(b,z)) ⟶ A(b,a)
+ De 4, usando las reglas de eliminación de la conjunción
(conjunct1 y conjunct2) se obtiene
5: E(b)
6: (∃z. P(z) ∧ A(b,z)) ⟶ A(b,a)
+ De h2, usando la regla allE, se tiene
7: E(b) ⟶ (∃x. P(x) ∧ A(b,x))
+ De 7 y 5, usando la regla mp se tiene
8: ∃x. P(x) ∧ A(b,x)
+ De 6 y 8, usando la regla mp, se tiene
9: A(b,a), con lo que termina la demostración›

― ‹(1) Demostración detallada›
lemma
assumes "∃x. P(x) ∧ (∀y. E(y) ∧ (∃z. P(z) ∧ A(y,z)) ⟶ A(y,x))"
"∀y. E(y) ⟶ (∃x. P(x) ∧ A(y,x))"
shows "∃x. P(x) ∧ (∀y. E(y) ⟶ A(y,x))"
proof-
from assms(1) obtain a
where 1: " P(a) ∧ (∀y. E(y) ∧ (∃z. P(z) ∧ A(y,z)) ⟶ A(y,a))"
by (rule exE)
then have 2: "∀y. E(y) ∧ (∃z. P(z) ∧ A(y,z)) ⟶ A(y,a)"
by (rule conjunct2)
have "P(a)"
using 1 by (rule conjunct1)
have "∀y. E(y) ⟶ A(y,a)"
proof (rule allI)
fix b
show "E(b) ⟶ A(b,a)"
proof (rule impI)
assume "E(b)"
have "E(b) ⟶ (∃x. P(x) ∧ A(b,x))"
using assms(2) by (rule allE)
then have "∃x. P(x) ∧ A(b,x)"
using `E(b)` by (rule mp)
with `E(b)` have 3: "E(b) ∧ (∃x. P(x) ∧ A(b,x))"
by (rule conjI)
have "E(b) ∧ (∃z. P(z) ∧ A(b,z)) ⟶ A(b,a)"
using 2 by (rule allE)
then show "A(b,a)"
using 3 by (rule mp)
qed
qed
with `P(a)` have "P(a) ∧ (∀y. E(y) ⟶ A(y,a))"
by (rule conjI)
then show ?thesis
by (rule exI)
qed

― ‹(1) Demostración detallada aplicativa:›
lemma
"⟦∃x. P(x) ∧ (∀y. E(y) ∧ (∃z. P(z) ∧ A(y,z)) ⟶ A(y,x));
∀y. E(y) ⟶ (∃x. P(x) ∧ A(y,x))⟧
⟹ ∃x. P(x) ∧ (∀y. E(y) ⟶ A(y,x))"
apply(erule exE)
apply(rule_tac x = x in exI)
apply(erule conjE)
apply(rule conjI, assumption)
apply(rule allI)
apply(rule impI)
apply(erule_tac x = y in allE)
apply (drule mp, assumption)
apply(erule_tac x=y in allE)
apply(erule impE)
apply(rule conjI, assumption)
apply(assumption)+
done

― ‹(2) Contraejemplo:›
lemma
assumes "∃x. P(x) ∧ (∀y. E(y) ∧ (∃z. P(z) ∧ A(y,z)) ⟶ A(y,x))"
"∀y. E(y) ⟶ (∃x. P(x) ∧ A(y,x))"
shows "∃x. P(x) ∧ (∀y. E(y) ⟶ ¬A(y,x))"
quickcheck
oops

(* Quickcheck found a counterexample:
P = {a⇩1}
x = a⇩1
E = {a⇩1}
A = {(a⇩1, a⇩1)}
*)

― ‹(2) Comprobación del contramodelo:

Considerando la interpretación proporcionada por Isabelle:

+ La hipótesis h1 se verifica pues:
+ Se verifica P(a1)
+ Se verifica ∀y. E(y) ∧ (∃z. P(z) ∧ A(y,z)) ⟶ A(y,a1)) pues
el elemento para el que se verifica E(y) ∧ (∃z. P(z) ∧ A(y,z)) es
a1 y, en ese caso, también se verifica A(a1, a1).
+ La hipótesis h2 se verifica pues, para todos los elementos para los
que se verifique E, sólo a1, también se verifica ∃x. P(x) ∧ A(a1,x),
pues se cumple P(a1) ∧ A(a1,a1).
+ No se verifica la conclusión, pues el único elemento que verifica P
es a1. Y, para a1, no se verifica ∀y. E(y) ⟶ ¬A(y,a1) pues para a1
se cumple E(a1) y no se cumple ¬A(a1,a1).›

end

</source>

@@ Línea 1: / Línea 1: @@
 <source lang = "isabelle">
-text ‹Tarea 1 de Lógica Matemática y Fundamentos (24-abril-2020)›
+text ‹Ejercicio de Lógica Matemática y Fundamentos (24-abril-2020)›
 theory Tarea_1_sol

@@ Línea 54: / Línea 54: @@
       ∀y. E(y) ⟶  A(y,a)
    + Para ello, por la regla allI, dado b cualquiera, hay que probar
-         E(y) ⟶  A(y,a)
+         E(b) ⟶  A(b,a)
      + Para ello, por la regla impI,
           supuesto 4: E(b)

← Revisión anterior	Revisión del 09:54 4 may 2020
(Sin diferencias)

T1 sol - Historial de revisiones

Mjoseh en 09:51 14 may 2020

Mjoseh en 09:55 10 may 2020

Mjoseh: Protegió «T1 sol» ([Editar=Solo administradores] (indefinido) [Trasladar=Solo administradores] (indefinido))

Mjoseh: Página creada con « text ‹Tarea 1 de Lógica Matemática y Fundamentos (24-abril-2020)› theory Tarea_1_sol imports Main begin lemma notnotI: "P ⟹ ¬¬ P"…»