T1

text ‹Tarea 1 de Lógica Matemática y Fundamentos (24-abril-2020)›

theory Tarea1
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 ‹Nota: En las demostraciones se pueden 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⟧ ⟹ c = 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

  También se pueden usar las reglas notnotI y mt que demostramos a
  continuación. 
›

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



end