LMF2014: Ejercicios de formalización en lógica de primer orden con Isabelle/HOL
En la segunda parte de la clase de hoy del curso Lógica matemática y fundamentos se ha explicado cómo formalizar en lógica de primer orden los argumentos de los ejercicios 8, 12 y 26 de la relación 5.
Los ejercicios y sus soluciones se muestran a continuación:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 |
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 ------------------------------------------------------------------ *} 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)" oops 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)))" oops 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)" oops |