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

(* benber *)
(* No es cierto si el universo consiste en más que un objeto. En ese caso, asignar la igualdad (=) a P
  es un contraejemplo. *)

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

(* benber *)
lemma
  assumes "A ∨ P ⟶ R ∧ F"
    and "F ∨ N ⟶ Or"
  shows "A ⟶ Or"
proof
  assume "A"
  hence "A ∨ P" by (rule disjI1)
  with `A ∨ P ⟶ R ∧ F` have "R ∧ F" by (rule mp)
  hence "F" by (rule conjunct2)
  hence "F ∨ N" by (rule disjI1)
  with `F ∨ N ⟶ Or` show "Or" by (rule mp)
qed

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

(* benber *)
lemma
  assumes "A ⟶ (M ⟷ ¬B)"
    and "A ∨ B"
  shows "¬B ⟶ M"
proof
  assume "¬B"
  note `A ∨ B`
  moreover {
    assume "A"
    with `A ⟶ (M ⟷ ¬B)` have "M ⟷ ¬B" by (rule mp)
    hence "¬B ⟹ M" by (rule iffD2)
    hence "M" using `¬B` .
  }
  moreover {
    note `¬B`
    moreover assume "B"
    ultimately have "M" by (rule notE)
  }
  ultimately show "M" by (rule disjE)
qed

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

(* benber *)
lemma
  assumes "∀x. ¬ R x ⟶ R (p x)"
  shows "∃x. R x ∧ R (p (p x))"
proof -
  have 0: "p ∨ ¬ p" for p
  proof (rule ccontr)
    assume "¬ (p ∨ ¬ p)"
    moreover {
      have "p"
      proof (rule ccontr)
        assume "¬ p"
        hence "p ∨ ¬ p" by (rule disjI2)
        with `¬ (p ∨ ¬ p)` show "False" by (rule notE)
      qed
      hence "p ∨ ¬ p" by (rule disjI1)
    }
    ultimately show "False" by (rule notE)
  qed

  have "¬ R x ⟶ R (p x)" for x using assms(1) by (rule allE)
  hence 1: "¬ R x ⟹ R (p x)" for x by (rule mp)

  have 2: "⟦R y; ¬ R (p y)⟧ ⟹ ?thesis" for y
  proof
    assume "R y"
    assume "¬ R (p y)"
    hence "R (p (p y))" by (rule 1)
    with `R y` show "R y ∧ R (p (p y))" by (rule conjI)
  qed

  have 3: "R y ⟹ ?thesis" for y
  proof -
    assume "R y"

    have "R (p y) ∨ ¬ R (p y)" by (rule 0)
    moreover {
      assume "R (p y)"
      have "R (p (p y)) ∨ ¬ R (p (p y))" by (rule 0)
      moreover {
        assume "R (p (p y))"
        with `R y` have "R y ∧ R (p (p y))" by (rule conjI)
        hence ?thesis by (rule exI)
      }
      moreover {
        assume "¬ R (p (p y))"
        with `R (p y)` have ?thesis by (rule 2)
      }
      ultimately have ?thesis by (rule disjE)
    }
    moreover {
      assume "¬ R (p y)"
      with `R y` have ?thesis by (rule 2)
    }
    ultimately show ?thesis by (rule disjE)
  qed

  fix y
  have "R y ∨ ¬ R y" by (rule 0)
  moreover {
    assume "R y"
    hence ?thesis by (rule 3)
  }
  moreover {
    assume "¬ R y"
    hence "R (p y)" by (rule 1)
    hence ?thesis by (rule 3)
  }
  ultimately show ?thesis by (rule disjE)
qed

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

(* benber *)
lemma
  assumes "∀x. Af x ⟶ (∀y. E y ⟶ Ap x y)"
    and "∀x. E x ⟶ ¬ Ap j x"
  shows "(∃x. E x ∧ N x) ⟶ ¬ Af j"
proof
  assume "∃x. E x ∧ N x"

  show "¬ Af j"
  proof (rule ccontr)
    assume "¬ ¬ Af j"
    hence "Af j" by (rule notnotD)

    note `∀x. Af x ⟶ (∀y. E y ⟶ Ap x y)`
    hence "Af j ⟶ (∀x. E x ⟶ Ap j x)" by (rule allE)
    moreover note `Af j`
    ultimately have "∀x. E x ⟶ Ap j x" by (rule mp)

    note `∃x. E x ∧ N x`
    moreover have "E x ∧ N x ⟹ False" for x
    proof -
      assume "E x ∧ N x"
      hence "E x" by (rule conjunct1)

      note `∀x. E x ⟶ Ap j x`
      hence "E x ⟶ Ap j x" by (rule allE)
      hence "Ap j x" using `E x`  by (rule mp)

      note `∀x. E x ⟶ ¬ Ap j x`
      hence "E x ⟶ ¬ Ap j x" by (rule allE)
      hence "¬ Ap j x" using `E x` by (rule mp)
      thus "False" using `Ap j x` by (rule notE)
    qed
    ultimately show "False" by (rule exE)
  qed
qed

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

(* benber *)
lemma
  assumes A1: "∀x. P x ⟶ R x"
    and A2: "∀x. P x ⟶ (¬(Q x) ⟶ R x)"
    and "¬(R a)"
  shows "P a ⟶ Q a"
proof
  have "P a ⟶ (¬(Q a) ⟶ R a)" using A2 by (rule allE)
  moreover assume "P a"
  ultimately have "¬(Q a) ⟶ R a" by (rule mp)

  show "Q a"
  proof (rule ccontr)
    assume "¬(Q a)"
    with `¬(Q a) ⟶ R a` have "R a" by (rule mp)
    with `¬(R a)` show "False" by (rule notE)
  qed
qed

end