|
|
| Línea 1: |
Línea 1: |
| | <source lang = "isar"> | | <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> | | </source> |
