Ver el código de «Rel 5» - Lógica matemática y fundamentos (2014-15)

<source lang = "isar">
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. 
  ------------------------------------------------------------------ *}

text {* --------------------------------------------------------------- 
  Ejercicio 1. Formalizar el siguiente argumento 
     Sócrates es un hombre. 
     Los hombres son mortales. 
     Luego, Sócrates es mortal.
  Usar s    para Sócrates
       H(x) para x es un hombre          
       M(x) para x es mortal
  ------------------------------------------------------------------ *}

lemma ejercicio_1:
  assumes "H(s)" 
          "∀x. H(x) ⟶ M(x)"
  shows   "M(s)"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 2. 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_2:
  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}\<^isub>
     T = {a2}
*}

text {* --------------------------------------------------------------- 
  Ejercicio 3. 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_3: 
  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 4. 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_4:
  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

text {* --------------------------------------------------------------- 
  Ejercicio 5. Formalizar el siguiente argumento 
     Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
     María y a Pedro.
  Usar j      para Juan  
       m      para María
       p      para Pedro
       T(x,y) para x teme a y
  ------------------------------------------------------------------ *}

lemma ejercicio_5:
  assumes "T(j,m)" 
          "T(j,p)"
  shows   "∃x. T(x,m) ∧ T(x,p)"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 6. Formalizar el siguiente argumento 
     Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
     es padre de Luis. Por tanto, Carlos es padre de Juan.
  Usar H(x,y) para x es hermano de y
       P(x,y) para x es padre de y
       j      para Juan
       l      para Luis
       c      para Carlos
  ------------------------------------------------------------------ *}

lemma ejercicio_6:
  assumes "∀x y. H(x,y) ⟶ H(y,x)"
          "∀x y z. H(x,y) ∧ P(z,x) ⟶ P(z,y)"
          "H(j,l)"
          "P(c,l)"
  shows   "P(c,j)"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 7. Formalizar el siguiente argumento 
     La existencia de algún canal de TV pública, supone un acicate para
     cualquier canal de TV privada; el que un canal de TV tenga un
     acicate, supone una gran satisfacción para cualquiera de sus
     directivos; en Madrid hay varios canales públicos de TV; TV5 es un
     canal de TV privada; por tanto, todos los directivos de TV5 están
     satisfechos. 
  Usar Pu(x)  para x es un canal de TV pública
       Pr(x)  para x es un canal de TV privada
       A(x)   para x posee un acicate
       D(x,y) para x es un directivo del canal y
       S(x)   para x está satisfecho 
       t      para TV5
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_7:
  assumes "(∃x. Pu(x)) ⟶ (∀x. Pr(x) ⟶ A(x))"
          "∀x. A(x) ⟶ (∀y. D(y,x) ⟶ S(y))"
          "∃x. Pu(x)"
          "Pr(t)"
  shows   "∀x. D(x,t) ⟶ S(x)"
using assms
by auto


text {* --------------------------------------------------------------- 
  Ejercicio 8. Formalizar el siguiente argumento 
     Quien intente entrar en un país y no tenga pasaporte, encontrará
     algún aduanero que le impida el paso. A algunas personas
     motorizadas que intentan entrar en un país le impiden el paso
     únicamente personas motorizadas. Ninguna persona motorizada tiene
     pasaporte. Por tanto, ciertos aduaneros están motorizados.
  Usar E(x)   para x entra en un país
       P(x)   para x tiene pasaporte
       A(x)   para x es aduanero
       I(x,y) para x impide el paso a y
       M(x)   para x está motorizada
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_8:
  assumes "∀x. E(x) ∧ ¬P(x) ⟶ (∃y. A(y) ∧ I(y,x))"
          "∃x. M(x) ∧ E(x) ∧ (∀y. I(y,x) ⟶ M(y))"
          "∀x. M(x) ⟶ ¬P(x)"
  shows "∃x. A(x) ∧ M(x)"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 9. 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_9:
  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

text {* --------------------------------------------------------------- 
  Ejercicio 10. 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_10:
  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

text {* --------------------------------------------------------------- 
  Ejercicio 11. Formalizar el siguiente argumento 
     Todo individuo que esté conforme con el contenido de cualquier
     acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
     políticos. Cualquiera que se inhiba de los asuntos políticos, no
     participará en el próximo referéndum. Todo español, está conforme
     con el acuerdo internacional de Maastricht, al que sin embargo no
     apoya. Por tanto, cualquier individuo o no es español, o en otro
     caso, está conforme con el contenido del acuerdo internacional de
     Maastricht y no participará en el próximo referéndum. 
  Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
       A(x,y) para la persona x apoya el acuerdo y
       I(x)   para la persona x se inibe de asuntos políticos
       R(x)   para la persona x participará en el próximo referéndum
       E(x)   para la persona x es española
       m      para el acuerdo de Maastricht
  ------------------------------------------------------------------ *}

lemma ejercicio_11:
  assumes "∀x y. C(x,y) ⟶ A(x,y) ∨ I(x)"
          "∀x. I(x) ⟶ ¬R(x)"
          "∀x. E(x) ⟶ C(x,m) ∧ ¬A(x,m)"
  shows   "∀x. ¬E(x) ∨ (C(x,m) ∧ ¬R(x))"
using assms
by metis

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

lemma ejercicio_12:
  assumes "∀x. ¬R(x) ⟶ R(p(x))"
  shows   "∃x. R(x) ∧ R(p(p(x)))"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 13. Formalizar el siguiente argumento 
     Todo deprimido que estima a un submarinista es listo. Cualquiera
     que se estime a sí mismo es listo. Ningún deprimido se estima a sí
     mismo. Por tanto, ningún deprimido estima a un submarinista.
  Usar D(x)   para x está deprimido
       E(x,y) para x estima a y
       L(x)   para x es listo
       S(x)   para x es submarinista
  ------------------------------------------------------------------ *}

lemma ejercicio_13:
  assumes "∀x. D(x) ∧ (∃y. S(y) ∧ E(x,y)) ⟶ L(x)"
          "∀x. E(x,x) ⟶ L(x)"
          "¬(∃x. D(x) ∧ E(x,x))"
  shows   "¬(∃x. D(x) ∧ (∃y. S(y) ∧ E(x,y)))"
quickcheck
oops

text {*
  El argumento es incorrecto como muestra el siguiente contraejemplo:
     Quickcheck found a counterexample:
     D = {a2}
     S = {a1}
     E = {(a2,a1)}
     L = {a2}
*}

text {* --------------------------------------------------------------- 
  Ejercicio 14. 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_14:
  assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
          "A(a)"
          "¬Ob(b,a)"
  shows   "¬R(b)"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 15. Formalizar el siguiente argumento 
     En una pecera nadan una serie de peces. Se observa que:
     * Hay algún pez x que para cualquier pez y, si el pez x no se come
       al pez y entonces existe un pez z tal que z es un tiburón o bien
       z protege al pez y. 
     * No hay ningún pez que se coma a todos los demás.
     * Ningún pez protege a ningún otro.
     Por tanto, existe algún tiburón en la pecera.
  Usar C(x,y) para x se come a y 
       P(x,y) para x protege a y
       T(x)   para x es un tiburón
   ------------------------------------------------------------------ *}

lemma ejercicio_15:
  assumes "∃x. ∀y. ¬C(x,y) ⟶ (∃z. T(z) ∨ P(z,y))"
          "∀x. ∃y. ¬C(x,y)"
          "∀x y. ¬P(x,y)"
  shows   "∃x. T(x)"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 16. Formalizar el siguiente argumento 
     Supongamos conocidos los siguientes hechos acerca del número de
     aprobados de dos asignaturas A y B: 
     * Si todos los alumnos aprueban la asignatura A, entonces todos
       aprueban la asignatura B.
     * Si algún delegado de la clase aprueba A y B, entonces todos los 
       alumnos aprueban A.
     * Si nadie aprueba B, entonces ningún delegado aprueba A.
     * Si Manuel no aprueba B, entonces nadie aprueba B.
     Por tanto, si Manuel es un delegado y aprueba la asignatura A,
     entonces todos los alumnos aprueban las asignaturas A y B.
  Usar A(x,y) para x aprueba la asignatura y
       D(x)   para x es delegado
       m      para Manuel
       a      para la asignatura A
       b      para la asignatura B
   ------------------------------------------------------------------ *}

lemma ejercicio_16:
  assumes "(∀x. A(x,a)) ⟶ (∀x. A(x,b))"
          "(∃x. D(x) ∧ A(x,a) ∧ A(x,b)) ⟶ (∀x. A(x,a))"
          "(∀x. ¬A(x,b)) ⟶ (∀x. D(x) ⟶ ¬A(x,a))"
          "¬A(m,b) ⟶ (∀x. ¬A(x,b))"
   shows  "D(m) ∧ A(m,a) ⟶ (∀x. A(x,a) ∧ A(x,b))"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 17. Formalizar el siguiente argumento 
     En cierto país oriental se ha celebrado la fase final del
     campeonato mundial de fútbol. Cierto diario deportivo ha publicado
     las siguientes estadísticas de tan magno acontecimiento: 
     * A todos los porteros que no vistieron camiseta negra les marcó un
       gol algún delantero europeo.  
     * Algún portero jugó con botas blancas y sólo le marcaron goles
       jugadores con botas blancas.  
     * Ningún portero se marcó un gol a sí mismo. 
     * Ningún jugador con botas blancas vistió camiseta negra. 
     Por tanto, algún delantero europeo jugó con botas blancas.
  Usar P(x)   para x es portero
       D(x)   para x es delantero europeo 
       N(x)   para x viste camiseta negra
       B(x)   para x juega con botas blancas 
       M(x,y) para x marcó un gol a y
   ------------------------------------------------------------------ *}

lemma ejercicio_17:
  assumes "∀x. P(x) ∧ ¬N(x) ⟶ (∃y. D(y) ∧ M(y,x))"
          "∃x. P(x) ∧ B(x) ∧ (∀y. M(y,x) ⟶ B(y))"
          "¬(∃x. P(x) ∧ M(x,x))"
          "¬(∃x. B(x) ∧ N(x))"
  shows   "∃x. D(x) ∧ B(x)"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 18. Formalizar el siguiente argumento 
     Las relaciones de parentesco verifican la siguientes propiedades
     generales:  
     * Si x es hermano de y, entonces y es hermano de x. 
     * Todo el mundo es hijo de alguien. 
     * Nadie es hijo del hermano de su padre. 
     * Cualquier padre de una persona es también padre de todos los
       hermanos de esa persona. 
     * Nadie es hijo ni hermano de sí mismo. 
     Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
     Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
     son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
     de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
  Usar A       para Don Antonio
       He(x,y) para x es hermano de y 
       Hi(x,y) para x es hijo de y  
       L       para Don Luis
       a       para Antoñito
       m       para Manolito
   ------------------------------------------------------------------ *}

lemma ejercicio_18:
  assumes "∀x y. He(x,y) ⟶ He(y,x)"
          "∀x. ∃y. Hi(x,y)"
          "∀x y z. Hi(x,y) ∧ He(z,y) ⟶ ¬Hi(x,z)"
          "∀x y. Hi(x,y) ⟶ (∀z. He(z,x) ⟶ Hi(z,y))"
          "∀x. ¬Hi(x,x) ∧ ¬He(x,x)"
          "He(A,L)"
          "He(a,m)"
          "Hi(a,A)"
  shows   "¬Hi(m,L)"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 19. [Problema del apisonador de Schubert (en inglés, 
  "Schubert’s steamroller")] Formalizar el siguiente argumento 
     Si uno de los miembros del club afeita a algún otro (incluido a
     sí mismo), entonces todos los miembros del club lo han afeitado
     a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
     Petruccio y Cesare pertenecen al club de barberos. Guido ha
     afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
  Usar g      para Guido
       l      para Lorenzo
       p      para Petruccio
       c      para Cesare
       B(x)   para x es un miembro del club de barberos
       A(x,y) para x ha afeitado a y
   ------------------------------------------------------------------ *}

lemma ejercicio_19:
  assumes "∀x. B(x) ∧ (∃y. B(y) ∧ A(x,y)) ⟶ (∀z. B(z) ⟶ A(z,x))"
          "B(g)" 
          "B(l)" 
          "B(p)" 
          "B(c)"
          "A(g,c)"
  shows   "A(p,l)"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 20. Formalizar el siguiente argumento 
     Carlos afeita a todos los habitantes de Las Chinas que no se
     afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
     Chinas. Por consiguiente, Carlos no afeita a nadie.
  Usar A(x,y) para x afeita a y
       C(x)   para x es un habitante de Las Chinas
       c      para Carlos
   ------------------------------------------------------------------ *}

lemma ejercicio_20:
  assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
          "C(c)"
  shows   "¬(∃x. A(c,x))"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 21. Formalizar el siguiente argumento
     Quien desprecia a todos los fanáticos desprecia también a todos los
     políticos. Alguien no desprecia a un determinado político. Por
     consiguiente, hay un fanático al que no todo el mundo desprecia.
   Usar D(x,y) para x desprecia a y
        F(x)   para x es fanático
        P(x)   para x es político
   ------------------------------------------------------------------ *}

lemma ejercicio_21:
  assumes "∀x. (∀y. F(y) ⟶ D(x,y)) ⟶  (∀y. P(y) ⟶ D(x,y))"
          "∃x y. P(y) ∧ ¬D(x,y)"
  shows   "∃x. F(x) ∧ ¬(∀y. D(y,x))"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 22. Formalizar el siguiente argumento
     El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
     se ama a sí mismo.
  Usar A(x,y) para x ama a y
       H(x)   para x es un hombre
       P(x)   para x es puro
   ------------------------------------------------------------------ *}

lemma ejercicio_22:
  assumes "∀x. H(x) ∧ P(x) ⟶ (∀y. P(y) ⟶ A(x,y))"
  shows   "∀x. H(x) ∧ P(x) ⟶ A(x,x)"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 23. 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_23:
  assumes "¬(∃x. P(x) ∧ R(x))"
          "∀x. P(x) ∧ ¬Q(x) ⟶ R(x)"
  shows   "P(a) ⟶ Q(a)"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 24. Formalizar el siguiente argumento
     1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
        existen algunos ejemplares de estos animales. 
     2. También hay algunas semillas y las semillas son plantas. 
     3. A todo animal le gusta o bien comer todo tipo de plantas o bien
        le gusta comerse a todos los animales más pequeños que él mismo
        que gustan de comer algunas plantas. 
     4. Las orugas y los caracoles son mucho más pequeños que los
        pájaros, que son mucho más pequeños que los zorros que a su vez
        son mucho más pequeños que los lobos. 
     5. A los lobos no les gusta comer ni zorros ni semillas, mientras
        que a los pájaros les gusta comer orugas pero no caracoles. 
     6. Las orugas y los caracoles gustan de comer algunas plantas. 
     7. Luego, existe un animal al que le gusta comerse un animal al que
        le gusta comer semillas.  
  Usar A(x)    para x es un animal
       Ca(x)   para x es un caracol
       Co(x,y) para x le gusta comerse a y
       L(x)    para x es un lobo
       M(x,y)  para x es más pequeño que y
       Or(x)   para x es una oruga
       Pa(x)   para x es un pájaro
       Pl(x)   para x es una planta
       S(x)    para x es una semilla
       Z(x)    para x es un zorro
  ------------------------------------------------------------------ *}

lemma ejercicio_24:
  assumes
   "∀x. L(x) ⟶ A(x)"
   "∀x. Z(x) ⟶ A(x)"
   "∀x. Pa(x) ⟶ A(x)"
   "∀x. Or(x) ⟶ A(x)"
   "∀x. Ca(x) ⟶ A(x)"
   "∃x. L(x)"
   "∃x. Z(x)"
   "∃x. Pa(x)"
   "∃x. Or(x)"
   "∃x. Ca(x)"
   "∃x. S(x)"
   "∀x. S(x) ⟶ Pl(x)"
   "∀x. A(x) ⟶ 
        (∀y. Pl(y) ⟶ Co(x,y)) ∨ 
        (∀y. A(y) ∧ M(y,x) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(x,y))"
   "∀x y. Pa(y) ∧ (Ca(x) ∨ Or(x)) ⟶ M(x,y)"
   "∀x y. Pa(x) ∧ Z(y) ⟶ M(x,y)"
   "∀x y. Z(x) ∧ L(y) ⟶ M(x,y)"
   "∀x y. L(x) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(x,y)"
   "∀x y. Pa(x) ∧ Or(y) ⟶ Co(x,y)"
   "∀x y. Pa(x) ∧ Ca(y) ⟶ ¬Co(x,y)"
   "∀x. Or(x) ∨ Ca(x) ⟶ (∃y. Pl(y) ∧ Co(x,y))"
  shows
   "∃x y. A(x) ∧ A(y) ∧ (∃z. S(z) ∧ Co(y,z) ∧ Co(x,y))"
using assms
by meson

section {* Ejercicios con igualdad *}

text {* --------------------------------------------------------------- 
  Ejercicio 25. 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_25:
  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

text {* --------------------------------------------------------------- 
  Ejercicio 26. Formalizar el siguiente argumento 
     Sólo hay un sofista que enseña gratuitamente, y éste es
     Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
     argumenta mejor que algún sofista que enseña gratuitamente. Si una
     persona argumenta mejor que otra segunda, entonces la segunda no
     argumenta mejor que la primera. Por consiguiente, Platón no es un
     sofista. 
  Usar G(x)   para x enseña gratuitamente
       M(x,y) para x argumenta mejor que y
       S(x)   para x es un sofista
       p      para Platón
       s      para Sócrates
  ------------------------------------------------------------------ *}

lemma ejercicio_26:
  assumes "∃y. (∀x. S(x) ∧ G(x) ⟷ x=y) ∧ y=s" 
          "∀x. S(x) ∧ x ≠ s ⟶ M(s,x)" 
          "∃x. S(x) ∧ G(x) ∧ M(p,x)"  
          "∀x y. M(x,y) ⟶ ¬M(y,x)"
  shows "¬S(p)"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 27. 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_27:
  assumes "∀x. F(x) ⟶ P(x)"
          "∀x. P(x) ⟶ L(x)"
          "F(n)"
          "¬L(m)"
  shows   "n ≠ m"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 28. Formalizar el siguiente argumento 
     Los padres son mayores que los hijos. Juan es el padre de Luis. Por
     tanto, Juan es mayor que Luis.
  Usar M(x,y) para x es mayor que y
       p(x)   para el padre de x
       j      para Juan
       l      para Luis
  ------------------------------------------------------------------ *}

lemma ejercicio_28:
  assumes "∀x. M(p(x),x)"
          "j = p(l)"
shows     "M(j,l)"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 29. Formalizar el siguiente argumento 
     El esposo de la hermana de Toni es Roberto. La hermana de Toni es
     María. Por tanto, el esposo de María es Roberto. 
  Usar e(x) para el esposo de x
       h    para la hermana de Toni
       m    para María
       r    para Roberto
  ------------------------------------------------------------------ *}

lemma ejercicio_29:
  assumes "e(h) = r"
          "h = m"
  shows   "e(m) = r"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 30. Formalizar el siguiente argumento 
     Luis y Jaime tienen el mismo padre. La madre de Rosa es
     Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
     la madre de Rosa ama al padre de Luis.
  Usar A(x,y) para x ama a y
       m(x)   para la madre de x
       p(x)   para el padre de x
       c      para Carlos
       e      para Eva
       j      para Jaime
       l      para Luis
       r      para Rosa
  ------------------------------------------------------------------ *}

lemma ejercicio_30:
  assumes "p(l) = p(j)"
          "m(r) = e"
          "A(e,c)"
          "c = p(j)"
  shows   "A(m(r),p(l))"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 31. Formalizar el siguiente argumento 
     Si dos personas son hermanos, entonces tienen la misma madre y el
     mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
     de Juan es la madre del padre de Luis.
  Usar H(x,y) para x es hermano de y
       m(x)   para la madre de x
       p(x)   para el padre de x
       j      para Juan
       l      para Luis
   ------------------------------------------------------------------ *}

lemma ejercicio_31:
  assumes "∀x y. H(x,y) ⟶ m(x) = m(y) ∧ p(x) = p(y)"
          "H(j,l)"
  shows   "m(p(j)) = m(p(l))"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 32. Formalizar el siguiente argumento 
     Todos los miembros del claustro son asturianos. El secretario forma
     parte del claustro. El señor Martínez es el secretario. Por tanto,
     el señor Martínez es asturiano.
  Usar C(x) para x es miembro del claustro
       A(x) para x es asturiano
       s    para el secretario
       m    para el señor Martínez
   ------------------------------------------------------------------ *}

lemma ejercicio_32:
  assumes "∀x. C(x) ⟶ A(x)"
          "C(s)"
          "m = s"
  shows   "A(m)"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 33. 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_33:
  assumes "V(e)"
          "a = p"
          "C(e) ∨ F(a)"
          "∀x. C(x) ⟶ ¬V(x)"
   shows  "F(p)"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 34. Formalizar el siguiente argumento 
     La luna hoy es redonda. La luna de hace dos semanas tenía forma de
     cuarto creciente. Luna no hay más que una, es decir, siempre es la
     misma. Luego existe algo que es a la vez redondo y con forma de
     cuarto creciente. 
  Usar L(x) para la luna del momento x
       R(x) para x es redonda
       C(x) para x tiene forma de cuarto creciente
       h    para hoy
       d    para hace dos semanas
  ------------------------------------------------------------------ *}

lemma ejercicio_34:
  assumes "R(l(h))"
          "C(l(d))"
          "∀x y. l(x) = l(y)"
  shows   "∃x. R(x) ∧ C(x)"
using assms
by metis

text {* --------------------------------------------------------------- 
  Ejercicio 35. Formalizar el siguiente argumento 
     Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
     delgado y Guillermo no. Luego, Juana no está casada con Guillermo. 
  Usar D(x)   para x es delgado
       C(x,y) para x está casada con y
       g      para Guillermo
       j      para Juana
       t      para Tomás
  ------------------------------------------------------------------ *}

lemma ejercicio_35:
  assumes "∃x. ∀y. C(j,y) ⟷ y = x" 
          "C(j,t)" 
          "D(t) ∧ ¬D(g)"
  shows   "¬C(j,g)"
using assms
by auto

text {* --------------------------------------------------------------- 
  Ejercicio 36. Formalizar el siguiente argumento 
     Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
     pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
     más que Sultán resolverá problemas que Sultán no puede resolver. 
     Todos los chimpancés distintos de Sultán trabajan más que Sultán. 
     Por consiguiente, Sultán no obtendrá un plátano.
  Usar Pl(x)  para x obtiene el plátano
       Pr(x)  para x es un problema
       R(x,y) para x resuelve y
       T(x,y) para x trabaja más que y
       c      para Chitón
       s      para Sultán
  ------------------------------------------------------------------ *}

lemma ejercicio_36:
  assumes "s ≠ c"
          "Pl(s) ⟶ (∀x. Pr(x) ⟶ R(s,x))"
          "T(c,s) ⟶ (∃x. Pr(x) ∧ R(c,x) ∧ ¬R(s,x))" 
          "∀x. x ≠ s ⟶ T(x,s)"
  shows   "¬Pl(s)"
using assms
by metis

end
</source>