chapter ‹R7: Lógica de de primer orden con igualdad: deducción natural,
formalización y argumentación con Isabelle/HOL ›
theory R7
imports Main
begin
text ‹
Demostrar o refutar los siguientes lemas usando sólo las reglas
básicas de deducción natural de la lógica proposicional, de los
cuantificadores y de la igualdad:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
. excluded_middle:(¬P ∨ P)
· allE: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allI: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
· trans: ⟦r = s; s = t⟧ ⟹ r = t
· sym: s = t ⟹ t = s
· not_sym: t ≠ s ⟹ s ≠ t
· ssubst: ⟦t = s; P s⟧ ⟹ P t
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
· arg_cong: x = y ⟹ f x = f y
· fun_cong: f = g ⟹ f x = g x
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y
›
text ‹
Se usarán las reglas notnotI y mt que demostramos a continuación.
›
lemma notnotI: "P ⟹ ¬¬ P"
by auto
lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto
section ‹ Ejercicios sobre igualdad ›
text ‹ ---------------------------------------------------------------
Ejercicio 1. Demostrar o refutar
P a ⟹ ∀x. x = a ⟶ P x
------------------------------------------------------------------ ›
lemma ejercicio_1:
assumes "P a"
shows "∀x. x = a ⟶ P x"
oops
text ‹ ---------------------------------------------------------------
Ejercicio 2. Demostrar o refutar
∃x y. R x y ∨ R y x; ¬(∃x. R x x)⟧ ⟹ ∃x y. x ≠ y
------------------------------------------------------------------ ›
lemma ejercicio_2:
fixes R :: "'c ⇒ 'c ⇒ bool"
assumes "∃x y. R x y ∨ R y x"
"¬(∃x. R x x)"
shows "∃(x::'c) y. x ≠ y"
oops
text ‹ ---------------------------------------------------------------
Ejercicio 3. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)}
⊢ P (f a) a (f a)
------------------------------------------------------------------ ›
lemma ejercicio_3:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "P (f a) a (f a)"
oops
text ‹ ---------------------------------------------------------------
Ejercicio 4. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)⟧
⊢ ∃z. P (f a) z (f (f a))
------------------------------------------------------------------ ›
lemma ejercicio_4:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
oops
text ‹ ---------------------------------------------------------------
Ejercicio 5. Demostrar o refutar
{∀y. Q a y,
∀x y. Q x y ⟶ Q (s x) (s y)}
⊢ ∃z. Qa z ∧ Q z (s (s a))
------------------------------------------------------------------ ›
lemma ejercicio_5:
assumes "∀y. Q a y"
"∀x y. Q x y ⟶ Q (s x) (s y)"
shows "∃z. Q a z ∧ Q z (s (s a))"
oops
text ‹ ---------------------------------------------------------------
Ejercicio 6. Demostrar o refutar
{x = f x, odd (f x)} ⊢ odd x
------------------------------------------------------------------ ›
lemma ejercicio_6:
assumes "x = f x" and
"odd (f x)"
shows "odd x"
oops
text ‹ ---------------------------------------------------------------
Ejercicio 7. Demostrar o refutar
{x = f x, triple (f x) (f x) x} ⊢ triple x x x
------------------------------------------------------------------ ›
lemma ejercicio_7:
assumes "x = f x" and
"triple (f x) (f x) x"
shows "triple x x x"
oops
text ‹ ---------------------------------------------------------------
Ejercicio 8. Demostrar o refutar
{∀x. ∀y. ∀z. (R (R(x, y), z) = R(x, R(y,z))),
∀x. ∀y. ∀z. R(x, y) = R(z, x) ⟶ y = z } ⊢ ∀x. ∀y. R(x,y) = R(y,x)
------------------------------------------------------------------ ›
lemma ejercicio_89:
assumes "∀x. ∀y. ∀z. (R (R(x, y), z) = R(x, R(y,z)))"
"∀x. ∀y. ∀z. R(x, y) = R(z, x) ⟶ y = z"
shows "∀x. ∀y. R(x,y) = R(y,x)"
oops
section ‹ Formalización y argumentación: LPO con igualdad›
text ‹---------------------------------------------------------------------
El objetivo de esta sección formalizar y decidir automáticamente
(con auto, blast, metis, meson o quickcheck) la corrección de los
argumentos.
Para comprobar las formalizaciones, en cada ejercicios se indica
su posición en APLI2 https://www.glc.us.es/apli2 correspondiente
a la sigla de la sección LPOI = Lógica de primer orden con igualdad.
›
text ‹---------------------------------------------------------------
Ejercicio 9. [LPOI-1 en APLI2] Formalizar, y decidir la corrección,
del 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 10. [LPOI-2 en APLI2] Formalizar, y decidir la corrección,
del 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
------------------------------------------------------------------›
text ‹---------------------------------------------------------------
Ejercicio 11. [LPOI-3 en APLI2] Formalizar, y decidir la corrección,
del 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 12. [LPOI-5 en APLI2] Formalizar, y decidir la corrección,
del 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
------------------------------------------------------------------›
text ‹---------------------------------------------------------------
Ejercicio 13. [LPOI-6 en APLI2] Formalizar, y decidir la corrección,
del 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
------------------------------------------------------------------›
text ‹---------------------------------------------------------------
Ejercicio 14. [LPOI-8 en APLI2] Formalizar, y decidir la corrección,
del 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
------------------------------------------------------------------›
text ‹---------------------------------------------------------------
Ejercicio 15. [LPOI-9 en APLI2] Formalizar, y decidir la corrección,
del 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
------------------------------------------------------------------›
text ‹---------------------------------------------------------------
Ejercicio 16. [LPOI-10 en APLI2] Formalizar, y decidir la corrección,
del 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
------------------------------------------------------------------›
text ‹---------------------------------------------------------------
Ejercicio 17. [LPOI-11 en APLI2] Formalizar, y decidir la corrección,
del 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
------------------------------------------------------------------›
text ‹---------------------------------------------------------------
Ejercicio 18. [LPOI-12 en APLI2] Formalizar, y decidir la corrección,
del 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
------------------------------------------------------------------›
text ‹---------------------------------------------------------------
Ejercicio 19. [LPOI-13 en APLI2] Formalizar, y decidir la corrección,
del 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
------------------------------------------------------------------›
end
![Lógica matemática y fundamentos [Curso 2019-20]](/~jalonso/imagenes/logoUS.jpg)