T1 sol

text ‹Ejercicio 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(b) ⟶  A(b,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