Relación 5

header {* R5: Argumentación en lógica de primer orden *}

theory R5
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.

  Una vez formalizadas, probar que el razonamiento es correcto, o refutarlo
  mediante un contraejemplo. 
  ------------------------------------------------------------------ *}

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

lemma ejercicio1
assumes "(∃x. I(x)) ∧ (∃x. T(x))" 
  shows   "∃x. I(x) ∧ T(x)"
oops

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
  ------------------------------------------------------------------ *}
lemma ejercicio2:
assumes 1: "∀x. (P(x)⟶V(x))" and
        2: "(¬(∃x. V(x))) ∨ (∃x. (V(x) ∧ (∀y. (V(y) ⟶ x=y))))" and
        3: "(¬(∃x. P(x))) ∨ (∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y))))" 
shows "∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y)))"
quickcheck
oops
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
  ------------------------------------------------------------------ *}
lemma ejercicio_3:
 assumes "∀x. (A x ∧ G x ⟶ V x ∧ L x)"
         "∃x. (A x ∧ V x ∧ ¬L x)"
 shows "∃x. (A x ∧ ¬G x)"
proof-
obtain b where 1 : "A b ∧ V b ∧ ¬L b" using assms(2) by (rule exE)
have 2 : "A b ∧ G b ⟶ V b ∧ L b" using assms(1) by (rule allE)
{assume 3 : "G b"
have 4 : "A b" using 1 by (rule conjunct1)
have 5 : "A b ∧ G b" using 4 3 by (rule conjI)
have 6 : "V b ∧ L b" using 2 5 by (rule mp)
have 7 : "L b" using 6 by (rule conjunct2)
have 8 : "V b ∧ ¬L b" using 1 by (rule conjunct2)
have 9 : "¬L b" using 8 by (rule conjunct2)
have "False" using 9 7 by (rule notE)}
hence 10 : "¬G b" by (rule notI)
have 11 : "A b" using 1 by (rule conjunct1)
have 12 : "A b ∧ ¬G b" using 11 10 by (rule conjI)
show "∃x. (A x ∧ ¬G x)" using 12 by (rule exI)
qed

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:
 assumes "∀x y. (R x ∧ A y ⟶ Ob x y)"
         "A a"
         "¬Ob b a"
 shows "¬R b"
proof-
{assume 1 : "R b"
have 2 : "∀y. R b ∧ A y ⟶ Ob b y" using assms(1) by (rule allE)
have 3 : "R b ∧ A a ⟶ Ob b a" using 2 by (rule allE)
have 4 : "R b ∧ A a" using 1 assms(2) by (rule conjI)
have 5 : "Ob b a" using 3  4 by (rule mp)
have "False" using assms(3) 5 by (rule notE)}
thus "¬R b" by (rule notI)
qed


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:
 assumes "¬(∃x. P x ∧ R x)"
         "∀x. (P x ∧ ¬Q x ⟶ R x)"
 shows "P a ⟶ Q a"
proof-
{assume 1 : "P a"
 {assume 2 : "¬Q a"
  have 3 : "P a ∧ ¬Q a ⟶ R a" using assms(2) by (rule allE)
  have 4 : "P a ∧ ¬Q a" using 1 2 by (rule conjI)
  have 5 : "R a" using 3 4 by (rule mp)
  have 6 : "P a ∧ R a" using 1 5 by (rule conjI)
  have 7 : "∃x. P x ∧ R x" using 6 by (rule exI)
  have "False" using assms(1) 7 by (rule notE)}
hence "Q a" by (rule ccontr)}
thus "P a ⟶ Q a" by (rule impI)
qed

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
  ------------------------------------------------------------------ *}
lemma ejercicio6
assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
          "∀x. E(x) ⟶ ¬Ap(j,x)"
  shows   "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
oops

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
  ------------------------------------------------------------------ *}
lemma ejercicio7:
assumes 1: "∀x. ((E(x) ∧ ¬V(x)) ⟶ (∃y. (A(y) ∧ Ca(y,x))))" and
        2: "∃x. ((Co(x) ∧ E(x)) ∧ (∀y. (Ca(y,x) ⟶ Co(y))))" and
        3: "∀x. (Co(x)⟶ ¬V(x))"
shows "∃x. (A(x) ∧ Co(x))" 
proof -
obtain a where 4: "(Co(a) ∧ E(a)) ∧ (∀y. (Ca(y,a)⟶Co(y)))" using 2 by (rule exE)
have 5: "Co(a) ∧ E(a)" using 4 by (rule conjunct1)
have 6: "Co(a)" using 5 by (rule conjunct1)
have 7: "E(a)" using 5 by (rule conjunct2)
have 8: "∀y. (Ca(y,a)⟶Co(y))" using 4 by (rule conjunct2)
have 9: "Co(a) ⟶ ¬V(a)" using 3 by (rule allE)
have 10: "¬V(a)" using 9 6 by (rule mp)
have 11: "(E(a)∧ ¬V(a)) ⟶ (∃y. (A(y) ∧ Ca(y,a)))" using 1 by (rule allE)
have 12: "E(a) ∧ ¬V(a)" using 7 10 by (rule conjI)
have 13: "∃y. (A(y) ∧ Ca(y,a))" using 11 12 by (rule mp)
obtain b where 14: "A(b) ∧ Ca(b,a)" using 13 by (rule exE)
have 15: "A(b)" using 14 by (rule conjunct1)
have 16: "Ca(b,a)⟶Co(b)" using 8 by (rule allE)
have 17: "Ca(b,a)" using 14 by (rule conjunct2)
have 18: "Co(b)" using 16 17 by (rule mp)
have 19: "A(b) ∧ Co(b)" using 15 18 by (rule conjI)
show 20: "∃x. (A(x) ∧ Co(x))" using 19 by (rule exI)
qed

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

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


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


end