Ver el código de «Sol 8» - Lógica matemática y fundamentos (2018-19)

<source lang = "isabelle">
chapter {* R8: Argumentación en lógica de primer orden *}

theory R8_sol
imports Main 
begin

text {*
  --------------------------------------------------------------------- 
  El objetivo de esta relación es formalizar en lógica de primer orden
  argumentos expresados en lenguaje natural.
 
  Antes de escribir la soluciones, comprobar con APLI2 la corrección de 
  la formalización. 
  ------------------------------------------------------------------ *}


text {* --------------------------------------------------------------- 
  Ejercicio 1. Formalizar el siguiente argumento 
     Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
     tanto, hay estudiantes inteligentes y trabajadores.
  Usar I(x) para x es inteligente
       T(x) para x es trabajador
  ------------------------------------------------------------------ *}

-- "La refutación automática es"
lemma ejercicio_1:
  assumes "(∃x. I(x)) ∧ (∃x. T(x))" 
  shows   "∃x. I(x) ∧ T(x)"
quickcheck
oops


text {*
  El argumento es incorrecto como muestra el siguiente contraejemplo:
     I = {a1}
     T = {a2}
*}

text {* --------------------------------------------------------------- 
  Ejercicio 2. Formalizar el siguiente argumento 
     Todos los participantes son vencedores. Hay como máximo un
     vencedor. Hay como máximo un participante. Por lo tanto, hay
     exactamente un participante. 
  Usar P(x) para x es un participante
       V(x) para x es un vencedor
  ------------------------------------------------------------------ *}

-- "La refutación automática es"
lemma ejercicio_2: 
  assumes "∀x. P(x) ⟶ V(x)"
          "∀x y. V(x) ∧ V(y) ⟶ x=y" 
          "∀x y. P(x) ∧ P(y) ⟶ x=y"
  shows   "∃x. P(x) ∧ (∀y. P(y) ⟶ x=y)"
quickcheck  
oops

text {*
  El argumento es incorrecto como muestra el siguiente contraejemplo:
     V = {}
     P = {}
*}

text {* --------------------------------------------------------------- 
  Ejercicio 3. Formalizar el siguiente argumento 
     Ningún aristócrata debe ser condenado a galeras a menos que sus
     crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
     hay aristócratas que han cometido crímenes vergonzosos aunque su
     forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
     que no está condenado a galeras. 
  Usar A(x)  para x es aristócrata
       G(x)  para x está condenado a galeras
       L(x)  para x lleva una vida licenciosa
       V(x)  para x ha cometido crímenes vergonzoso
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_3_a:
  assumes "∀x. A(x) ∧ G(x) ⟶ L(x) ∧ V(x)"
          "∃x. A(x) ∧ V(x) ∧ ¬L(x)"
  shows   "∃x. A(x) ∧ ¬G(x)"
using assms
by metis

lemma ejercicio_3_d:
  assumes "∀x. A(x) ∧ G(x) ⟶ L(x) ∧ V(x)"
          "∃x. A(x) ∧ V(x) ∧ ¬L(x)"
  shows   "∃x. A(x) ∧ ¬G(x)"
proof-
  from assms(2) obtain a where 1:"A(a) ∧ V(a) ∧ ¬L(a)" ..
  hence "A(a)" ..
  have "¬G(a)"
    proof
      assume "G(a)"
      with `A(a)` have 2: "A(a) ∧ G(a)" ..
      have "A(a) ∧ G(a) ⟶ L(a) ∧ V(a)" using assms(1) ..
      hence "L(a) ∧ V(a)" using 2 ..
      hence "L(a)" ..
      have "V(a) ∧ ¬L(a)" using 1 ..
      hence "¬L(a)" ..
      thus False using `L(a)`..
    qed
  with `A(a)` have "A(a) ∧ ¬G(a)" ..
  thus  "∃x. A(x) ∧ ¬G(x)" ..
qed

lemma ejercicio_3_e:
  "⟦∀x. A(x) ∧ G(x) ⟶ L(x) ∧ V(x);
          ∃x. A(x) ∧ V(x) ∧ ¬L(x)⟧ ⟹ ∃x. A(x) ∧ ¬G(x)"  
  apply (erule exE)
  apply (erule_tac x = x in allE)
  apply (rule_tac x = x in exI)
  apply (rule conjI)
   apply (erule conjunct1)
  apply (rule notI)
  apply (drule mp)
   apply (rule conjI)
    apply (erule conjunct1, assumption)
  apply (drule conjunct2)
  apply (drule conjunct1)
  apply (drule conjunct2)
  apply (erule notE, assumption)
    done
  
text {* --------------------------------------------------------------- 
  Ejercicio 4. Formalizar el siguiente argumento 
     Todos los robots obedecen a los amigos del programador jefe.
     Alvaro es amigo del programador jefe, pero Benito no le
     obedece. Por tanto, Benito no es un robot.
  Usar R(x)    para x es un robot
       Ob(x,y) para x obedece a y
       A(x)    para x es amigo del programador jefe
       b       para Benito
       a       para Alvaro
  ------------------------------------------------------------------ *}

lemma ejercicio_4_a:
  assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
          "A(a)"
          "¬Ob(b,a)"
  shows   "¬R(b)"
using assms
by metis

lemma ejercicio_4_b:
  assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
          "A(a)"
          "¬Ob(b,a)"
  shows   "¬R(b)"
proof
  assume "R(b)" 
  have "∀y. R(b) ∧ A(y) ⟶ Ob(b,y)" using assms(1) ..
  hence 1: "R(b) ∧ A(a) ⟶ Ob(b,a)" ..
  have "R(b) ∧ A(a)" using `R(b)` assms(2) ..
  with 1 have "Ob(b,a)" ..
  with assms(3) show False ..
qed

lemma ejercicio_4_c:
  "⟦∀x y. R(x) ∧ A(y) ⟶ Ob(x,y);
          A(a);¬Ob(b,a)⟧⟹ ¬R(b)"
  apply (rule notI)
  apply (erule_tac x = b in allE)
  apply (erule notE)
  apply (erule allE)
  apply (erule mp)
  apply (rule conjI, assumption+)
    done
  
text {* --------------------------------------------------------------- 
  Ejercicio 5. Formalizar el 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
   ------------------------------------------------------------------ *}

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

lemma ejercicio_5_b:
  assumes "¬(∃x. P(x) ∧ R(x))"
          "∀x. P(x) ∧ ¬Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
proof
  assume "P(a)" 
  show "Q(a)" 
   proof (rule ccontr)
     assume "¬Q(a)"
     with `P(a)` have 1: "P(a) ∧ ¬Q(a)" ..
     have "P(a) ∧ ¬Q(a) ⟶ R(a)" using assms(2) ..
     hence "R(a)" using 1 ..
     with `P(a)` have "P(a) ∧ R(a)" ..
     hence "∃x. P(x) ∧ R(x)" ..
     with assms(1) show False ..
   qed
 qed
   
lemma ejercicio_5_c:
   "⟦¬(∃x. P(x) ∧ R(x));
          ∀x. P(x) ∧ ¬Q(x) ⟶ R(x)⟧ ⟹ P(a) ⟶ Q(a)"   
  apply (rule impI)
  apply (erule_tac x = a in allE)
  apply (rule ccontr)
  apply (erule notE)
  apply (rule_tac x = a in exI)
  apply (rule conjI, assumption)
  apply (erule mp)
  apply (rule conjI, assumption+)
  done

text {* --------------------------------------------------------------- 
  Ejercicio 6. Formalizar el 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
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_6_a:
  assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
          "∀x. E(x) ⟶ ¬Ap(j,x)"
  shows   "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
using assms
by metis

lemma ejercicio_6_d:
  assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
          "∀x. E(x) ⟶ ¬Ap(j,x)"
  shows   "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
proof
  assume "∃x. E(x) ∧ N(x)" 
  then obtain a where "E(a) ∧ N(a)" ..
  hence "E(a)" ..
  have "E(a) ⟶ ¬Ap(j,a)" using assms(2) ..
  hence "¬Ap(j,a)" using `E(a)` ..
  show "¬Af(j)"
     proof
       assume "Af(j)"
       have "Af(j) ⟶ (∀y. E(y) ⟶ Ap(j,y))" using assms(1) ..
       hence "∀y. E(y) ⟶ Ap(j,y)" using `Af(j)` ..
       hence "E(a) ⟶ Ap(j,a)" ..
       hence "Ap(j,a)" using `E(a)` ..
       with `¬Ap(j,a)` show False ..
     qed
qed

lemma ejercicio_6_c:
  "⟦∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y));
          ∀x. E(x) ⟶ ¬Ap(j,x)⟧ ⟹
         (∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
  apply (rule impI)
  apply (erule exE)
  apply (erule_tac x = x in allE)
  apply (erule_tac x = j in allE)
  apply (rule notI)
  apply (drule mp)
   apply (erule conjunct1)
  apply (drule mp, assumption)
  apply (erule notE)
  apply (drule conjunct1)
  apply (erule_tac x = x in allE)
  apply (erule mp, assumption)
  done
    
text {* --------------------------------------------------------------- 
  Ejercicio 7. Formalizar el siguiente argumento 
     Todo aquel que entre en el país y no sea un VIP será cacheado por
     un aduanero. Hay un contrabandista que entra en el país y que solo
     podrá ser cacheado por contrabandistas. Ningún contrabandista es un
     VIP. Por tanto, algún aduanero es contrabandista.
  Usar A(x)    para x es aduanero
       Ca(x,y) para x cachea a y
       Co(x)   para x es contrabandista
       E(x)    para x entra en el pais
       V(x)    para x es un VIP
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_7_a:
  assumes "∀x. E(x) ∧ ¬V(x) ⟶ (∃y. A(y) ∧ Ca(y,x))"
           "∃x. Co(x) ∧ E(x) ∧ (∀y. Ca(y,x) ⟶ Co(y))"
           "¬(∃x. Co(x) ∧ V(x))"
  shows    "∃x. A(x) ∧ Co(x)"
using assms
by metis

lemma ejercicio_7_d:
  assumes "∀x. E(x) ∧ ¬V(x) ⟶ (∃y. A(y) ∧ Ca(y,x))"
           "∃x. Co(x) ∧ E(x) ∧ (∀y. Ca(y,x) ⟶ Co(y))"
           "¬(∃x. Co(x) ∧ V(x))"
  shows    "∃x. A(x) ∧ Co(x)"
proof-
  from assms(2) obtain a where 1: "Co(a) ∧ E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" ..
  hence "Co(a)" ..
  have 2:" E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" using 1 ..
  hence "E(a)" ..
  have 3: "∀y. Ca(y,a) ⟶ Co(y)" using 2 ..
  have "¬V(a) ∨ V(a)" ..
  thus "∃x. A(x) ∧ Co(x)"
     proof
       assume "¬V(a)"
         with `E(a)` have 4: "E(a) ∧ ¬V(a)" ..
         have "E(a) ∧ ¬V(a) ⟶ (∃y. A(y) ∧ Ca(y,a))" using assms(1) ..
         hence "∃y. A(y) ∧ Ca(y,a)" using 4 ..
         then obtain b where "A(b) ∧ Ca(b,a)" ..
         hence "A(b)" ..
         have "Ca(b,a)" using `A(b) ∧ Ca(b,a)` ..
         have "Ca(b,a) ⟶ Co(b)" using 3 ..
         hence "Co(b)" using `Ca(b,a)`..
         with `A(b)` have "A(b) ∧ Co(b)" ..
         thus "∃x. A(x) ∧ Co(x)" ..
       next 
       assume "V(a)"
       with `Co(a) ` have "Co(a) ∧ V(a)" ..
       hence "∃x. Co(x) ∧ V(x)" ..
       with assms(3) show "∃x. A(x) ∧ Co(x)" ..
     qed
qed

lemma ejercicio_7_c:
  "⟦∀x. E(x) ∧ ¬V(x) ⟶ (∃y. A(y) ∧ Ca(y,x));
      ∃x. Co(x) ∧ E(x) ∧ (∀y. Ca(y,x) ⟶ Co(y));
           ¬(∃x. Co(x) ∧ V(x)) ⟧ ⟹ ∃x. A(x) ∧ Co(x)"  
  apply (erule exE)
  apply (erule_tac x = x in allE)
  apply (drule mp)
   apply (rule conjI)
    apply (drule conjunct2)
    apply (drule conjunct1, assumption)
   apply (rule notI)
   apply (erule notE)
   apply (drule conjunct1)
   apply (rule_tac x = x in exI)
   apply (rule conjI, assumption+)
  apply (erule exE)
  apply (rule_tac x = y in exI)
  apply (rule conjI)
    apply (erule conjunct1)+
  apply (drule conjunct2)+
  apply (erule_tac x = y in allE)
  apply (drule mp, assumption+)
    done
    
  
section {* Ejercicios con igualdad *}

text {* --------------------------------------------------------------- 
  Ejercicio 8. Formalizar el siguiente argumento 
     Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
     Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
     primera. Hay como máximo una persona que ama a Rosa. Por tanto,
     Paco es Curro. 
  Usar A(x,y) para x ama a y 
       S(x,y) para x simpatiza con y 
       a      para Ana
       c      para Curro
       p      para Paco 
       r      para Rosa
  ------------------------------------------------------------------ *}

lemma ejercicio_8_a:
  assumes "A(r,c)" 
          "¬S(p,a)"
          "∀x. ¬S(x,a) ⟶ A(x,r)"
          "∀x y. A(x,y) ⟶ A(y,x)"
          "∀x y. A(x,r) ∧ A(y,r) ⟶ x=y"
  shows   "p = c"
using assms
by auto

lemma ejercicio_8_b:
  assumes "A(r,c)" 
          "¬S(p,a)"
          "∀x. ¬S(x,a) ⟶ A(x,r)"
          "∀x y. A(x,y) ⟶ A(y,x)"
          "∀x y. A(x,r) ∧ A(y,r) ⟶ x=y"
  shows   "p = c"
proof-
  have "∀y. A(r,y) ⟶ A(y,r)" using assms(4) ..
  hence "A(r,c) ⟶ A(c,r)" ..
  hence "A(c,r)" using assms(1) ..
  have "¬S(p,a) ⟶ A(p,r)" using assms(3) ..
  hence "A(p,r)" using assms(2) ..
  hence 1: "A(p,r) ∧ A(c,r)" using `A(c,r)`..
  have "∀y. A(p,r) ∧ A(y,r) ⟶ p=y" using assms(5) ..
  hence "A(p,r) ∧ A(c,r) ⟶ p=c" ..
  thus "p=c" using 1 ..
qed

lemma ejercicio_8_c:
  "⟦A(r,c);
    ¬S(p,a);
     ∀x. ¬S(x,a) ⟶ A(x,r);
     ∀x y. A(x,y) ⟶ A(y,x);
     ∀x y. A(x,r) ∧ A(y,r) ⟶ x=y ⟧ ⟹ p = c"  
  apply (drule_tac x = p in spec)
  apply (drule mp, assumption) 
  apply (drule_tac x = r in spec)
  apply (drule_tac x = p in spec)
  apply (frule_tac x = c in spec)
  apply (drule mp, assumption)
  apply (drule_tac x = c in spec)+
  apply (rule mp, assumption)
    apply (rule conjI, assumption+)
    done
  
text {* --------------------------------------------------------------- 
  Ejercicio 9. Formalizar el siguiente argumento 
     Todos los filósofos se han preguntado qué es la filosofía. Los que
     se preguntan qué es la filosofía se vuelven locos. Nietzsche es
     filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
     Nietzsche y su maestro son diferentes personas. 
  Usar F(x) para x es filósofo
       L(x) para x se vuelve loco
       P(x) para x se ha preguntado qué es la filosofía.
       m    para el maestro de Nietzsche
       n    para Nietzsche
  ------------------------------------------------------------------ *}

lemma ejercicio_9_a:
  assumes "∀x. F(x) ⟶ P(x)"
          "∀x. P(x) ⟶ L(x)"
          "F(n)"
          "¬L(m)"
  shows   "n ≠ m"
using assms
by auto

lemma ejercicio_9_b:
  assumes "∀x. F(x) ⟶ P(x)"
          "∀x. P(x) ⟶ L(x)"
          "F(n)"
          "¬L(m)"
  shows   "n ≠ m"
proof
  assume "n = m" 
  hence "F(m)" using assms(3) by (rule subst)
  have "F(m) ⟶ P(m)" using assms(1) ..
  hence "P(m)" using `F(m)` ..
  have "P(m) ⟶ L(m)" using assms(2) ..
  hence "L(m)" using `P(m)` ..
  with assms(4) show False ..
qed

lemma ejercicio_9_c:
  "⟦∀x. F(x) ⟶ P(x);
    ∀x. P(x) ⟶ L(x);
    F(n);
    ¬L(m) ⟧ ⟹ n ≠ m"  
  apply (rule notI)
  apply (erule_tac x = n in allE)
  apply (drule mp, assumption)
  apply (erule_tac x = m in allE)
    apply (erule notE)
  apply (erule mp)
  apply (erule subst, assumption)
    done
  
text {* --------------------------------------------------------------- 
  Ejercicio 10. Formalizar el siguiente argumento 
     Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
     de la defensa. O Eduardo estaba en clase o Antonio dio falso
     testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
     primer testigo de la defensa dio falso testimonio. 
  Usar C(x) para x estaba en clase
       F(x) para x dio falso testimonio
       V(x) para x pudo haber visto al asesino
       a    para Antonio
       e    para Eduardo
       p    para el primer testigo de la defensa
  ------------------------------------------------------------------ *}

lemma ejercicio_10_a:
  assumes "V(e)"
          "a = p"
          "C(e) ∨ F(a)"
          "∀x. C(x) ⟶ ¬V(x)"
   shows  "F(p)"
using assms
by auto

lemma ejercicio_10_b:
  assumes "V(e)"
          "a = p"
          "C(e) ∨ F(a)"
          "∀x. C(x) ⟶ ¬V(x)"
   shows  "F(p)"
using assms(3)
proof 
  assume "C(e)"
    have "C(e) ⟶ ¬V(e)" using assms(4) ..
    hence "¬V(e)" using `C(e)` ..
    thus  "F(p)" using assms(1) ..
  next
  assume "F(a)"
   with assms(2) show "F(p)" by (rule subst)
qed

lemma ejercicio_10_c:
  "⟦ V(e);
     a = p;
     C(e) ∨ F(a);
     ∀x. C(x) ⟶ ¬V(x) ⟧ ⟹ F(p)"  
  apply (erule disjE)
   apply (erule_tac x = e in allE)
   apply (drule mp, assumption)
   apply (erule notE, assumption)
  apply (erule subst, assumption)
    done
  
end

</source>