Relación 11

header {* R11: Deducción natural de primer orden *}

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

-- "maresccas4 irealetei" (* Una! nos ha salido Una!!! *)
lemma ej_1_auto:
  assumes " P a ⟶ (∃x. Q x)"
  shows "∃x. P a ⟶ Q x"
using assms by auto

lemma ej_1:
  fixes P Q :: "'b ⇒ bool" 
  assumes 0:"P a ⟶ (∃x. Q x)"
  shows   "∃x. P a ⟶ Q x"
proof -
  have "¬(P a) ∨ P a" by (rule excluded_middle)
  then show "∃x. P a ⟶ Q x"
  proof (rule disjE)
      {assume 2:"(P a)"
        have 4: "∃x. Q x" using 0 2 ..
        obtain b where "Q b" using 4 by (rule exE)
        then have "P a ⟶ Q b" ..
        then show "∃x. P a ⟶ Q x" by (rule exI)}
      next 
       {assume 2:"¬(P a)"
        {assume "¬(∃x. P a ⟶ Q x)"
         then have 3: "∀x. ¬(P a ⟶ Q x)" by (rule no_ex)
         fix b
         have "¬(P a ⟶ Q b)" using 3 ..
         then have "P a ∧ ¬Q b" by (rule Meson.not_impD)
         then have 4:"P a" ..
         have "False" using 2 4 ..}
        then show " ∃x. P a ⟶ Q x" by (rule ccontr)}
       qed
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)
  ------------------------------------------------------------------ *}

-- "irealetei maresccas4" (* Dos *)

lemma ej_2:
  assumes "∀x. ∀y. ∀z. R x y ∧ R y z ⟶ R x z"
          "∀x. ¬(R x x)"
  shows "∀x. ∀y. R x y ⟶ ¬(R y x)"
proof -
  {fix a
  {fix b
  {assume 1:"R a b"
  have  "¬(R b a)"
  proof (rule ccontr)
    assume "¬¬(R b a)"
    then have "R b a" by (rule notnotD)
    with 1 have 3:"R a b ∧ R b a" ..
    have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) ..
    then have "∀z. R a b ∧ R b z ⟶ R a z" ..
    then have "R a b ∧ R b a ⟶ R a a" ..
    then have "R a a" using 3 ..
    have "¬(R a a)" using assms(2) ..
    then show False using `R a a`..
  qed}
  then have 4:"R a b ⟶ ¬(R b a)" ..}
  then have "∀y. R a y ⟶ ¬ R y a" ..}
  then show "∀x y. R x y ⟶ ¬ R y x" ..
qed

text {* --------------------------------------------------------------- 
  Ejercicio 3. Demostrar o refutar
       (∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
  ------------------------------------------------------------------ *}
-- "irealetei maresccas4"
lemma ej_3_auto:
  assumes "∀x. ∃y. P x y"
  shows "∃y. ∀x. P x y"
quickcheck
oops

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

-- "irealetei maresccas4"
lemma ej_4_auto:
  assumes "∃y. ∀x. P x y"
  shows "∀x. ∃y. P x y" 
using assms by auto

lemma ej_4:
  assumes 1:"∃y. ∀x. P x y"
  shows "∀x. ∃y. P x y" 
proof -
  {fix a
  obtain b where 2:"∀x. P x b" using 1 ..
  have "P a b" using 2 ..
  then have "∃y. P a y"  ..}
  then show "∀x. ∃y. P x y" ..
qed

lemma ej_4_bis:"(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)" 
proof 
  assume 1:"∃y. ∀x. P x y"
  {fix a
  obtain b where 2:"∀x. P x b" using 1 ..
  have "P a b" using 2 ..
  then have "∃y. P a y"  ..}
  then show "∀x. ∃y. P x y" ..
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))
  ------------------------------------------------------------------ *}

-- "maresccas4"
lemma ej_5:
  assumes "∀x. P a x x"
          "∀x y z. P x y z ⟶ P (f x) y (f z)"
  shows "∃z. P (f a) z (f (f a))"
proof -
  have "P a (f a) (f a)" using assms(1) ..
  have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) ..
  then have "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
  then have "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
  then have "P (f a) (f a) (f (f a))" using `P a (f a) (f a)` ..
  then show "∃z. P (f a) z (f (f a))" ..
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))
  ------------------------------------------------------------------ *}

-- "maresccas4"
lemma ej_6:
  assumes "∀y. Q a y"
          "∀x y. Q x y ⟶ Q (s x) (s y)"
  shows "∃z. Q a z ∧ Q z (s (s a))"
proof -
  have "Q a (s a)" using assms(1) ..
  have "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) ..
  then have "Q a (s a) ⟶ Q (s a) (s (s a))" ..
  then have "Q (s a) (s (s a))" using `Q a (s a)` ..
  with  `Q a (s a)` have "Q a (s a) ∧ Q (s a) (s (s a))"  by (rule conjI)
  then show "∃z. Q a z ∧ Q z (s (s a))" ..
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.
  ------------------------------------------------------------------ *}

-- "pabflomar maresccas4"

lemma ej7_pfm:
  assumes 1: "A ∨ P ⟶ R ∧ F" and
          2: "(F ∨ N) ⟶ Or"
 shows "A ⟶ Or"
proof -
  { assume 3: "A"
    have 4: "A ∨ P" using 3 by (rule disjI1)
    have 5: "R ∧ F" using 1 4 by (rule mp)
    have 6: "F" using 5 by (rule conjunct2)
    have 7: "F ∨ N" using 6 by (rule disjI1)
    have 8: "Or" using 2 7 by (rule mp)}
  then show "A ⟶ Or" ..
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.
  ------------------------------------------------------------------ *}
-- "pabflomar" 
{* Aquí dejo dos formalizaciones válidas del enunciado, por si alguien encuentra la inspiración que yo he perdido. In Diego we trust! *}

lemma ej8_pfm:
  assumes 1: "A ⟶ (M ⟷ ¬B)" and
          2: "A ∨ B"
 shows "¬B ⟶ M"
proof

oops

lemma ej8_pfm_2:
  assumes 1: "(A ∧ M) ⟶ ¬B ∧ A" and
          2: "A ∨ B"
 shows "¬B ⟶ M"
  

oops

-- "maresccas4"
lemma ej_8:
  assumes "(A ⟶ M) ⟷ ¬B"
          "A ∨ B"
  shows "¬B ⟶ M"
using assms(2)
proof
  { assume "A"
    { assume "¬B"
      have "¬B ⟶ (A ⟶ M)" using assms(1) ..
      then have "A ⟶ M" using `¬B` ..
      then have "M" using `A` .. }
    then show "¬B ⟶ M" ..
  }
next
  { assume "B"
    { assume "¬B"
      then have False using `B` ..
      then have "M" .. }
    then show "¬B ⟶ M" ..
  }
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
  ------------------------------------------------------------------ *}
-- "julrobrel"
lemma apli2_ej13_lpo:
    assumes "∀ x. ¬R(x) ⟶ R(p(x))"
      shows "∃ x. R(x) ∧ R(p(p(x)))"
using assms
by auto

lemma apli2_ej13_lpo_d:
    assumes 0:"∀ x. ¬R(x) ⟶ R(p(x))"
      shows "∃ x. R(x) ∧ R(p(p(x)))"
oops


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
  ------------------------------------------------------------------ *}
-- "julrobrel"
lemma apli2_ej10_lpo:
    assumes "∀ x. Af(x) ⟶ (∀ y. E(y) ⟶ Ap(x,y))"
            "∀ y. E(y) ⟶ ¬ Ap(j,y)"
      shows "∃ y. E(y) ∧ N(y) ⟶ ¬Af(j)"
using assms
by auto

lemma apli2_ej10_lpo_d:
    assumes 0:"∀ x. Af(x) ⟶ (∀ y. E(y) ⟶ Ap(x,y))"
        and 1:"∀ y. E(y) ⟶ ¬ Ap(j,y)"
      shows "∃ y. E(y) ∧ N(y) ⟶ ¬Af(j)"
oops



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

-- "julrobrel"
lemma apli2_ej24_lpo:
  assumes "¬ (∃ x. P(x) ∧ R(x))"
          "∀ x. P(x) ∧ ¬ Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
using assms
by auto

-- "julrobrel"
lemma apli2_ej24_lpo_d:
  assumes 0:"¬ (∃ x. P(x) ∧ R(x))"
      and 1:"∀ x. P(x) ∧ ¬ Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
oops

-- "julrobrel: cuatro sencillos lemas, aunque no faciles de demostrar, y al final el principal"

--"julrobrel: es el modus tolens(mt)"
lemma apli2_ej24_lpo_d_aux1:
  assumes 0:"p ∧ ¬q ⟶ r"
  shows   "¬r⟶¬p ∨ q"
using assms
by auto

-- "julrobrel"
lemma apli2_ej24_lpo_d_aux2:
  assumes 0:"¬(p ∧ r)"
  shows   "p ⟶ ¬r"
using assms
by auto

--"julrobrel: este lema debe de tener un nombre..."
lemma apli2_ej24_lpo_d_aux3:
  assumes "(p ⟶ q) ∧ (q ⟶ r)"
  shows   "p ⟶ r"
using assms
by auto

-- "julrobrel"
lemma apli2_ej24_lpo_d_aux4:
  assumes 0:"p⟶(¬p ∨ q)"
  shows   "p ⟶ q"
using assms
by auto

-- "julrobrel"
lemma apli2_ej24_lpo_d:
  assumes 0:"¬ (∃ x. P(x) ∧ R(x))"
      and 1:"∀ x. P(x) ∧ ¬ Q(x) ⟶ R(x)"
    shows   "P(a)⟶Q(a)"
proof -
  have 2:"∀ x. ¬(P(x) ∧ R(x))" using 0 by (rule no_ex)
  fix a
  have 3:"¬(P(a) ∧ R(a))" using 2 ..
  have 4:"P(a) ∧ ¬ Q(a) ⟶ R(a)" using 1 ..
  have 5:"¬R(a) ⟶ ¬ P(a) ∨ Q(a)" using 4 by (rule apli2_ej24_lpo_d_aux1)
  have 6:"P(a)⟶¬R(a)" using 3 by (rule apli2_ej24_lpo_d_aux2)
  have 7:"(P(a)⟶¬R(a)) ∧ (¬R(a) ⟶ ¬P(a) ∨ Q(a))" using 6 5 by (rule conjI)
  have 8:"P(a)⟶(¬P(a) ∨ Q(a))" using 7 by (rule apli2_ej24_lpo_d_aux3)
  have 9:"P(a)⟶Q(a)" using 8 by (rule apli2_ej24_lpo_d_aux4)
  show "P(a)⟶Q(a)" using 9 .
qed

end