Relación 7

chapter {* R7: Deducción natural de primer orden *}

theory R7_Deduccion_natural_de_primer_orden
imports Main 
begin

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

  · allI:       ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
  · allE:       (⋀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, mt y not_ex que demostramos a 
  continuación. *}

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

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

lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 1. Demostrar
       P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x 
  ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes "P a ⟶ (∃x. Q x)"
  shows "∃x. P a ⟶ Q x"
proof (rule ccontr)
  assume "∄x. P a ⟶ Q x"

  have "P a ⟶ (∃x. P a ⟶ Q x)"
  proof
    assume "P a"
    with assms have "∃x. Q x" by (rule mp)
    moreover have "⋀x. Q x ⟹ ∃x'. P a ⟶ Q x'"
    proof -
      fix x
      assume "Q x"
      hence "P a ⟶ Q x" by (rule impI)
      thus "∃x'. P a ⟶ Q x'" by (rule exI)
    qed
    ultimately show "∃x. P a ⟶ Q x" by (rule exE)
  qed
  moreover note `∄x. P a ⟶ Q x`
  ultimately have "¬(P a)" by (rule mt)

  have "¬(P a) ⟶ (∃x. P a ⟶ Q x)"
  proof 
    fix x
    assume "¬(P a)"
    have "P a ⟶ Q x"
    proof
      assume "P a"
      with `¬(P a)` have "False" by (rule notE)
      thus "Q x" by (rule FalseE)
    qed
    thus "∃x. P a ⟶ Q x" by (rule exI)
  qed
  moreover note `∄x. P a ⟶ Q x`
  ultimately have "¬¬(P a)" by (rule mt)
  moreover note `¬(P a)`
  ultimately show "False" by (rule notE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 2. Demostrar
       {∀x y z. R x y ∧ R y z ⟶ R x z, 
        ∀x. ¬(R x x)}
       ⊢ ∀x y. R x y ⟶ ¬(R y x)
  ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes A1: "∀x y z. R x y ∧ R y z ⟶ R x z"
    and A2: "∀x. ¬(R x x)"
  shows "∀x y. R x y ⟶ ¬(R y x)"
proof -
  {
    fix x y
    {
      assume "R x y"
      have "¬ (R y x)"
      proof (rule ccontr)
        assume "¬ ¬ (R y x)"
        hence "R y x" by (rule notnotD)

        note `∀x y z. R x y ∧ R y z ⟶ R x z`
        moreover have "∀ y z. R x y ∧ R y z ⟶ R x z ⟹ False"
        proof -
          assume "∀ y z. R x y ∧ R y z ⟶ R x z"
          moreover have "∀ z. R x y ∧ R y z ⟶ R x z ⟹ False"
          proof -
            assume "∀ z. R x y ∧ R y z ⟶ R x z"
            moreover have "R x y ∧ R y x ⟶ R x x ⟹ False"
            proof -
              assume "R x y ∧ R y x ⟶ R x x"
              moreover {
                note `R x y`
                moreover note `R y x`
                ultimately have "R x y ∧ R y x" by (rule conjI)
              }
              ultimately have "R x x" by (rule mp)

              note `∀x. ¬(R x x)`
              moreover {
                assume "¬(R x x)"
                moreover note `R x x`
                ultimately have "False" by (rule notE)
              }
              ultimately show "False" by (rule allE)
            qed
            ultimately show "False" by (rule allE)
          qed
          ultimately show "False" by (rule allE)
        qed
        ultimately show "False" by (rule allE)
      qed
    }
    hence "R x y ⟶ ¬ (R y x)" by (rule impI)
  }
  hence "⋀x. ∀y. R x y ⟶ ¬ (R y x)" by (rule allI)
  thus ?thesis by (rule allI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar o refutar
       (∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 4. Demostrar o refutar
       (∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)
  ------------------------------------------------------------------ *}

(* benber *)
lemma "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
proof
  assume "∃y. ∀x. P x y"
  moreover have "⋀y. ∀x. P x y ⟹ ∀x. ∃y'. P x y'"
  proof
    fix x y
    assume "∀x'. P x' y"
    hence "P x y" by (rule allE)
    thus "∃y'. P x y'" by (rule exI)
  qed
  ultimately show "∀x. ∃y. P x y" by (rule exE)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 5. Demostrar o refutar
     {∀x. P a x x, 
      ∀x y z. P x y z ⟶ P (f x) y (f z)⟧
     ⊢ ∃z. P (f a) z (f (f a))
  ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes A1: "∀ x. P a x x"
    and A2: "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
proof
  from A2
  have "∀y z. P a y z ⟶ P (f a) y (f z)" by (rule allE)
  hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
  hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
  moreover have "P a (f a) (f a)" using A1 by (rule allE)
  ultimately show "P (f a) (f a) (f (f a))" by (rule mp)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 6. Demostrar o refutar
     {∀y. Q a y, 
      ∀x y. Q x y ⟶ Q (s x) (s y)} 
     ⊢ ∃z. Qa z ∧ Q z (s (s a))
  ------------------------------------------------------------------ *}

(* benber *)
lemma
  assumes "∀y. Q a y"
      and "∀x y. Q x y ⟶ Q (s x) (s y)"
    shows "∃z. Q a z ∧ Q z (s (s a))"
proof
  have "Q a a" using `∀y. Q a y` by (rule allE)
  moreover have "Q a (s (s a))" using `∀y. Q a y` by (rule allE)
  ultimately show "Q a a ∧ Q a (s (s a))" by (rule conjI)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 7. (En APLI2 el ejercicio 13 de LP) Formalizar, y demostrar
  la corrección, del siguiente argumento 
     Si la válvula está abierta o la monitorización está preparada,
     entonces se envía una señal de reconocimiento y un mensaje de
     funcionamiento al controlador del ordenador. Si se envía un mensaje 
     de funcionamiento al controlador del ordenador o el sistema está en 
     estado normal, entonces se aceptan las órdenes del operador. Por lo
     tanto, si la válvula está abierta, entonces se aceptan las órdenes
     del operador. 
  Usar A : La válvula está abierta.
       P : La monitorización está preparada.
       R : Envía una señal de reconocimiento.
       F : Envía un mensaje de funcionamiento.
       N : El sistema está en estado normal.
       Or : Se aceptan órdenes del operador.
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 8. (En APLI2 el ejercicio 5 de LP) Formalizar, y demostrar
  la corrección, del siguiente argumento 
     En cierto experimento, cuando hemos empleado un fármaco A, el
     paciente ha mejorado considerablemente en el caso, y sólo en el
     caso, en que no se haya empleado también un fármaco B. Además, o se
     ha empleado el fármaco A o se ha empleado el fármaco B. En
     consecuencia, podemos afirmar que si no hemos empleado el fármaco
     B, el paciente ha mejorado considerablemente. 
  Usar A: Hemos empleado el fármaco A.
       B: Hemos empleado el fármaco B.
       M: El paciente ha mejorado notablemente.
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 9. (En APLI2 el ejercicio 13 de LPO) Formalizar, y decidir
  la corrección, del siguiente argumento 
     Toda persona pobre tiene un padre rico. Por tanto, existe una
     persona rica que tiene un abuelo rico.
  Usar R(x) para x es rico
       p(x) para el padre de x
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 10. (En APLI2 el ejercicio 10 de LPO) Formalizar, y decidir
  la corrección, del siguiente argumento 
     Los aficionados al fútbol aplauden a cualquier futbolista
     extranjero. Juanito no aplaude a futbolistas extranjeros. Por
     tanto, si hay algún futbolista extranjero nacionalizado español,
     Juanito no es aficionado al fútbol.
  Usar Af(x)   para x es aficicionado al fútbol
       Ap(x,y) para x aplaude a y
       E(x)    para x es un futbolista extranjero
       N(x)    para x es un futbolista nacionalizado español
       j       para Juanito
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 11. Formalizar, y decidir la corrección, del siguiente
  argumento
     Ningún socio del club está en deuda con el tesorero del club. Si
     un socio del club no paga su cuota está en deuda con el tesorero
     del club. Por tanto, si el tesorero del club es socio del club,
     entonces paga su cuota. 
  Usar P(x) para x es socio del club
       Q(x) para x paga su cuota
       R(x) para x está en deuda con el tesorero
       a    para el tesorero del club
   ------------------------------------------------------------------ *}

end