GLC T2R2b
De DAO (Demostración asistida por ordenador)
Revisión del 13:57 15 jul 2018 de Jalonso (discusión | contribuciones) (Texto reemplazado: «lang="isar"» por «lang="isabelle"»)
header {* T2R2b: Argumentación en lógica de primer orden *}
theory T2R2b
imports Main
begin
text {* ---------------------------------------------------------------
Ejercicio 16. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_16a:
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 blast
-- "La demostración estructurada es"
lemma ejercicio_16b:
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))"
proof
assume "D(m) ∧ A(m,a)"
hence "D(m)" ..
have "A(m,a)" using `D(m) ∧ A(m,a)` ..
have "A(m,b)"
proof (rule ccontr)
assume "¬A(m,b)"
with assms(4) have "∀x. ¬A(x,b)" ..
with assms(3) have "∀x. D(x) ⟶ ¬A(x,a)" ..
hence "D(m) ⟶ ¬A(m,a)" ..
hence "¬A(m,a)" using `D(m)` ..
thus False using `A(m,a)` ..
qed
with `A(m,a)` have "A(m,a) ∧ A(m,b)" ..
with `D(m)` have "D(m) ∧ A(m,a) ∧ A(m,b)" ..
hence "∃x. D(x) ∧ A(x,a) ∧ A(x,b)" ..
with assms(2) have "∀x. A(x,a)" ..
with assms(1) have "∀x. A(x,b)" ..
show "∀x. A(x,a) ∧ A(x,b)"
proof
fix c
show "A(c,a) ∧ A(c,b)"
proof
show "A(c,a)" using `∀x. A(x,a)` ..
next
show "A(c,b)" using `∀x. A(x,b)` ..
qed
qed
qed
-- "La demostración detallada es"
lemma ejercicio_16c:
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))"
proof (rule impI)
assume "D(m) ∧ A(m,a)"
hence "D(m)" by (rule conjunct1)
have "A(m,a)" using `D(m) ∧ A(m,a)` by (rule conjunct2)
have "A(m,b)"
proof (rule ccontr)
assume "¬A(m,b)"
with assms(4) have "∀x. ¬A(x,b)" by (rule mp)
with assms(3) have "∀x. D(x) ⟶ ¬A(x,a)" by (rule mp)
hence "D(m) ⟶ ¬A(m,a)" by (rule allE)
hence "¬A(m,a)" using `D(m)` by (rule mp)
thus False using `A(m,a)` by (rule notE)
qed
with `A(m,a)` have "A(m,a) ∧ A(m,b)" by (rule conjI)
with `D(m)` have "D(m) ∧ A(m,a) ∧ A(m,b)" by (rule conjI)
hence "∃x. D(x) ∧ A(x,a) ∧ A(x,b)" by (rule exI)
with assms(2) have "∀x. A(x,a)" by (rule mp)
with assms(1) have "∀x. A(x,b)" by (rule mp)
show "∀x. A(x,a) ∧ A(x,b)"
proof (rule allI)
fix c
show "A(c,a) ∧ A(c,b)"
proof (rule conjI)
show "A(c,a)" using `∀x. A(x,a)` by (rule allE)
next
show "A(c,b)" using `∀x. A(x,b)` by (rule allE)
qed
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 17. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_17a:
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 blast
-- "La demostración estructurada es"
lemma ejercicio_17b:
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)"
proof -
obtain a where a: "P(a) ∧ B(a) ∧ (∀y. M(y,a) ⟶ B(y))"
using assms(2) ..
have "P(a) ∧ ¬N(a)"
proof
show "P(a)" using a ..
next
have "B(a) ∧ (∀y. M(y,a) ⟶ B(y))" using a ..
hence "B(a)" ..
have "∀x. ¬(B(x) ∧ N(x))" using assms(4) by (rule no_ex)
hence "¬(B(a) ∧ N(a))" ..
show "¬N(a)"
proof
assume "N(a)"
with `B(a)` have "B(a) ∧ N(a)" ..
with `¬(B(a) ∧ N(a))` show False ..
qed
qed
hence "∃y. D(y) ∧ M(y,a)"
proof -
have "P(a) ∧ ¬N(a) ⟶ (∃y. D(y) ∧ M(y,a))" using assms(1) ..
thus "∃y. D(y) ∧ M(y,a)" using `P(a) ∧ ¬N(a)` ..
qed
then obtain b where "D(b) ∧ M(b,a)" ..
have "D(b) ∧ B(b)"
proof
show "D(b)" using `D(b) ∧ M(b,a)` ..
next
have "M(b,a)" using `D(b) ∧ M(b,a)` ..
have "B(a) ∧ (∀y. M(y,a) ⟶ B(y))" using a ..
hence "∀y. M(y,a) ⟶ B(y)" ..
hence "M(b,a) ⟶ B(b)" ..
thus "B(b)" using `M(b,a)` ..
qed
thus "∃x. D(x) ∧ B(x)" ..
qed
-- "La demostración estructurada es"
lemma ejercicio_17c:
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)"
proof -
obtain a where a: "P(a) ∧ B(a) ∧ (∀y. M(y,a) ⟶ B(y))"
using assms(2) by (rule exE)
have "P(a) ∧ ¬N(a)"
proof (rule conjI)
show "P(a)" using a by (rule conjunct1)
next
have "B(a) ∧ (∀y. M(y,a) ⟶ B(y))" using a by (rule conjunct2)
hence "B(a)" by (rule conjunct1)
have "∀x. ¬(B(x) ∧ N(x))" using assms(4) by (rule no_ex)
hence "¬(B(a) ∧ N(a))" by (rule allE)
show "¬N(a)"
proof (rule notI)
assume "N(a)"
with `B(a)` have "B(a) ∧ N(a)" by (rule conjI)
with `¬(B(a) ∧ N(a))` show False by (rule notE)
qed
qed
hence "∃y. D(y) ∧ M(y,a)"
proof -
have "P(a) ∧ ¬N(a) ⟶ (∃y. D(y) ∧ M(y,a))"
using assms(1) by (rule allE)
thus "∃y. D(y) ∧ M(y,a)" using `P(a) ∧ ¬N(a)` by (rule mp)
qed
then obtain b where "D(b) ∧ M(b,a)" by (rule exE)
have "D(b) ∧ B(b)"
proof (rule conjI)
show "D(b)" using `D(b) ∧ M(b,a)` by (rule conjunct1)
next
have "M(b,a)" using `D(b) ∧ M(b,a)` by (rule conjunct2)
have "B(a) ∧ (∀y. M(y,a) ⟶ B(y))" using a by (rule conjunct2)
hence "∀y. M(y,a) ⟶ B(y)" by (rule conjunct2)
hence "M(b,a) ⟶ B(b)" by (rule allE)
thus "B(b)" using `M(b,a)` by (rule mp)
qed
thus "∃x. D(x) ∧ B(x)" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 18. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_18a:
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 blast
-- "La demostración estructurada es"
lemma ejercicio_18b:
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)"
proof
assume "Hi(m,L)"
have "He(L,A)"
proof -
have "∀y. He(A,y) ⟶ He(y,A)" using assms(1) ..
hence "He(A,L) ⟶ He(L,A)" ..
thus "He(L,A)" using assms(6) ..
qed
have "Hi(a,L)"
proof -
have "∀y. Hi(m,y) ⟶ (∀z. He(z,m) ⟶ Hi(z,y))" using assms(4) ..
hence "Hi(m,L) ⟶ (∀z. He(z,m) ⟶ Hi(z,L))" ..
hence "∀z. He(z,m) ⟶ Hi(z,L)" using `Hi(m,L)` ..
hence "He(a,m) ⟶ Hi(a,L)" ..
thus "Hi(a,L)" using assms(7) ..
qed
have "¬Hi(a,L)"
proof -
have "Hi(a,A) ∧ He(L,A)" using assms(8) `He(L,A)` ..
have "∀y z. Hi(a,y) ∧ He(z,y) ⟶ ¬Hi(a,z)" using assms(3) ..
hence "∀z. Hi(a,A) ∧ He(z,A) ⟶ ¬Hi(a,z)" ..
hence "Hi(a,A) ∧ He(L,A) ⟶ ¬Hi(a,L)" ..
thus "¬Hi(a,L)" using `Hi(a,A) ∧ He(L,A)` ..
qed
thus False using `Hi(a,L)` ..
qed
-- "La demostración detallada es"
lemma ejercicio_18c:
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)"
proof (rule notI)
assume "Hi(m,L)"
have "He(L,A)"
proof -
have "∀y. He(A,y) ⟶ He(y,A)" using assms(1) by (rule allE)
hence "He(A,L) ⟶ He(L,A)" by (rule allE)
thus "He(L,A)" using assms(6) by (rule mp)
qed
have "Hi(a,L)"
proof -
have "∀y. Hi(m,y) ⟶ (∀z. He(z,m) ⟶ Hi(z,y))"
using assms(4) by (rule allE)
hence "Hi(m,L) ⟶ (∀z. He(z,m) ⟶ Hi(z,L))" by (rule allE)
hence "∀z. He(z,m) ⟶ Hi(z,L)" using `Hi(m,L)` by (rule mp)
hence "He(a,m) ⟶ Hi(a,L)" by (rule allE)
thus "Hi(a,L)" using assms(7) by (rule mp)
qed
have "¬Hi(a,L)"
proof -
have "Hi(a,A) ∧ He(L,A)" using assms(8) `He(L,A)` by (rule conjI)
have "∀y z. Hi(a,y) ∧ He(z,y) ⟶ ¬Hi(a,z)"
using assms(3) by (rule allE)
hence "∀z. Hi(a,A) ∧ He(z,A) ⟶ ¬Hi(a,z)" by (rule allE)
hence "Hi(a,A) ∧ He(L,A) ⟶ ¬Hi(a,L)" by (rule allE)
thus "¬Hi(a,L)" using `Hi(a,A) ∧ He(L,A)` by (rule mp)
qed
thus False using `Hi(a,L)` by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 19. [Problema del apisonador de Schubert (en inglés,
"Schubert’s steamroller")] Formalizar, y decidir la corrección, del
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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_19a:
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 meson
-- "La demostración estructurada es"
lemma ejercicio_19b:
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)"
proof -
have "A(l,g)"
proof -
have "B(g) ∧ (∃y. B(y) ∧ A(g,y)) ⟶ (∀z. B(z) ⟶ A(z,g))"
using assms(1) ..
have "B(c) ∧ A(g,c)" using assms(5,6) ..
hence "(∃y. B(y) ∧ A(g,y))" ..
with assms(2) have "B(g) ∧ (∃y. B(y) ∧ A(g,y))" ..
with `B(g) ∧ (∃y. B(y) ∧ A(g,y)) ⟶ (∀z. B(z) ⟶ A(z,g))`
have "(∀z. B(z) ⟶ A(z,g))" ..
hence "B(l) ⟶ A(l,g)" ..
thus "A(l,g)" using assms(3) ..
qed
have "B(l) ∧ (∃y. B(y) ∧ A(l,y)) ⟶ (∀z. B(z) ⟶ A(z,l))"
using assms(1) ..
have "B(g) ∧ A(l,g)" using assms(2) `A(l,g)` ..
hence "(∃y. B(y) ∧ A(l,y))" ..
with assms(3) have "B(l) ∧ (∃y. B(y) ∧ A(l,y))" ..
with `B(l) ∧ (∃y. B(y) ∧ A(l,y)) ⟶ (∀z. B(z) ⟶ A(z,l))`
have "(∀z. B(z) ⟶ A(z,l))" ..
hence "B(p) ⟶ A(p,l)" ..
thus "A(p,l)" using assms(4) ..
qed
-- "La demostración detallada es"
lemma ejercicio_19c:
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)"
proof -
have "A(l,g)"
proof -
have "B(g) ∧ (∃y. B(y) ∧ A(g,y)) ⟶ (∀z. B(z) ⟶ A(z,g))"
using assms(1) by (rule allE)
have "B(c) ∧ A(g,c)" using assms(5,6) by (rule conjI)
hence "(∃y. B(y) ∧ A(g,y))" by (rule exI)
with assms(2) have "B(g) ∧ (∃y. B(y) ∧ A(g,y))" by (rule conjI)
with `B(g) ∧ (∃y. B(y) ∧ A(g,y)) ⟶ (∀z. B(z) ⟶ A(z,g))`
have "(∀z. B(z) ⟶ A(z,g))" by (rule mp)
hence "B(l) ⟶ A(l,g)" by (rule allE)
thus "A(l,g)" using assms(3) by (rule mp)
qed
have "B(l) ∧ (∃y. B(y) ∧ A(l,y)) ⟶ (∀z. B(z) ⟶ A(z,l))"
using assms(1) by (rule allE)
have "B(g) ∧ A(l,g)" using assms(2) `A(l,g)` by (rule conjI)
hence "(∃y. B(y) ∧ A(l,y))" by (rule exI)
with assms(3) have "B(l) ∧ (∃y. B(y) ∧ A(l,y))" by (rule conjI)
with `B(l) ∧ (∃y. B(y) ∧ A(l,y)) ⟶ (∀z. B(z) ⟶ A(z,l))`
have "(∀z. B(z) ⟶ A(z,l))" by (rule mp)
hence "B(p) ⟶ A(p,l)" by (rule allE)
thus "A(p,l)" using assms(4) by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 20. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_20a:
assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
"C(c)"
shows "¬(∃x. A(c,x))"
using assms
by blast
-- "La demostración estructurada es"
lemma ejercicio_20b:
assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
"C(c)"
shows "¬(∃x. A(c,x))"
proof -
have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) ..
have "A(c,c)"
proof (rule ccontr)
assume "¬A(c,c)"
with assms(2) have "C(c) ∧ ¬A(c,c)" ..
with 1 have "A(c,c)" ..
with `¬A(c,c)` show False ..
qed
have "¬A(c,c)"
proof -
have "C(c) ∧ ¬A(c,c)" using 1 `A(c,c)` ..
thus "¬A(c,c)" ..
qed
thus "¬(∃x. A(c,x))" using `A(c,c)` ..
qed
-- "La demostración detallada es"
lemma ejercicio_20c:
assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
"C(c)"
shows "¬(∃x. A(c,x))"
proof -
have 1: "A(c,c) ⟷ C(c) ∧ ¬A(c,c)" using assms(1) by (rule allE)
have "A(c,c)"
proof (rule ccontr)
assume "¬A(c,c)"
with assms(2) have "C(c) ∧ ¬A(c,c)" by (rule conjI)
with 1 have "A(c,c)" by (rule iffD2)
with `¬A(c,c)` show False by (rule notE)
qed
have "¬A(c,c)"
proof -
have "C(c) ∧ ¬A(c,c)" using 1 `A(c,c)` by (rule iffD1)
thus "¬A(c,c)" by (rule conjunct2)
qed
thus "¬(∃x. A(c,x))" using `A(c,c)` by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 21. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_21a:
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 blast
-- "La demostración semiautomática es"
lemma ejercicio_21b:
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))"
proof -
obtain a where "∃y. P(y) ∧ ¬D(a,y)" using assms(2) ..
then obtain b where "P(b) ∧ ¬D(a,b)" ..
hence "¬(∀y. P(y) ⟶ D(a,y))" by auto
have "(∀y. F(y) ⟶ D(a,y)) ⟶ (∀y. P(y) ⟶ D(a,y))" using assms(1) ..
hence "¬(∀y. F(y) ⟶ D(a,y))" using `¬(∀y. P(y) ⟶ D(a,y))` by (rule mt)
hence "∃y. ¬(F(y) ⟶ D(a,y))" by (rule no_para_todo)
then obtain c where "¬(F(c) ⟶ D(a,c))" ..
hence "F(c) ∧ ¬(∀y. D(y,c))" by auto
thus "∃x. F(x) ∧ ¬(∀y. D(y,x))" ..
qed
-- "En la demostración estructurada usaremos el siguiente lema"
lemma no_implica:
assumes "¬(p ⟶ q)"
shows "p ∧ ¬q"
using assms
by auto
-- "La demostración estructurada del lema es"
lemma no_implica_1:
assumes "¬(p ⟶ q)"
shows "p ∧ ¬q"
proof
show "p"
proof (rule ccontr)
assume "¬p"
have "p ⟶ q"
proof
assume "p"
with `¬p` show "q" ..
qed
with assms show False ..
qed
next
show "¬q"
proof
assume "q"
have "p ⟶ q"
proof
assume "p"
show "q" using `q` .
qed
with assms show False ..
qed
qed
-- "La demostración detallada del lema es"
lemma no_implica_2:
assumes "¬(p ⟶ q)"
shows "p ∧ ¬q"
proof (rule conjI)
show "p"
proof (rule ccontr)
assume "¬p"
have "p ⟶ q"
proof (rule impI)
assume "p"
with `¬p` show "q" by (rule notE)
qed
with assms show False by (rule notE)
qed
next
show "¬q"
proof (rule notI)
assume "q"
have "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using `q` by this
qed
with assms show False by (rule notE)
qed
qed
-- "La demostración estructurada es"
lemma ejercicio_21c:
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))"
proof -
obtain a where "∃y. P(y) ∧ ¬D(a,y)" using assms(2) ..
then obtain b where b: "P(b) ∧ ¬D(a,b)" ..
have "¬(∀y. P(y) ⟶ D(a,y))"
proof
assume "∀y. P(y) ⟶ D(a,y)"
hence "P(b) ⟶ D(a,b)" ..
have "P(b)" using b ..
with `P(b) ⟶ D(a,b)` have "D(a,b)" ..
have "¬D(a,b)" using b ..
thus False using `D(a,b)` ..
qed
have "(∀y. F(y) ⟶ D(a,y)) ⟶ (∀y. P(y) ⟶ D(a,y))" using assms(1) ..
hence "¬(∀y. F(y) ⟶ D(a,y))" using `¬(∀y. P(y) ⟶ D(a,y))` by (rule mt)
hence "∃y. ¬(F(y) ⟶ D(a,y))" by (rule no_para_todo)
then obtain c where c: "¬(F(c) ⟶ D(a,c))" ..
have "F(c) ∧ ¬(∀y. D(y,c))"
proof
have "F(c) ∧ ¬D(a,c)" using c by (rule no_implica)
thus "F(c)" ..
next
show "¬(∀y. D(y,c))"
proof
assume "∀y. D(y,c)"
hence "D(a,c)" ..
have "F(c) ∧ ¬D(a,c)" using c by (rule no_implica)
hence "¬D(a,c)" ..
thus False using `D(a,c)` ..
qed
qed
thus "∃x. F(x) ∧ ¬(∀y. D(y,x))" ..
qed
-- "La demostración detallada es"
lemma ejercicio_21d:
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))"
proof -
obtain a where "∃y. P(y) ∧ ¬D(a,y)" using assms(2) by (rule exE)
then obtain b where b: "P(b) ∧ ¬D(a,b)" by (rule exE)
have "¬(∀y. P(y) ⟶ D(a,y))"
proof (rule notI)
assume "∀y. P(y) ⟶ D(a,y)"
hence "P(b) ⟶ D(a,b)" by (rule allE)
have "P(b)" using b by (rule conjunct1)
with `P(b) ⟶ D(a,b)` have "D(a,b)" by (rule mp)
have "¬D(a,b)" using b by (rule conjunct2)
thus False using `D(a,b)` by (rule notE)
qed
have "(∀y. F(y) ⟶ D(a,y)) ⟶ (∀y. P(y) ⟶ D(a,y))"
using assms(1) by (rule allE)
hence "¬(∀y. F(y) ⟶ D(a,y))" using `¬(∀y. P(y) ⟶ D(a,y))` by (rule mt)
hence "∃y. ¬(F(y) ⟶ D(a,y))" by (rule no_para_todo)
then obtain c where c: "¬(F(c) ⟶ D(a,c))" by (rule exE)
have "F(c) ∧ ¬(∀y. D(y,c))"
proof (rule conjI)
have "F(c) ∧ ¬D(a,c)" using c by (rule no_implica)
thus "F(c)" by (rule conjunct1)
next
show "¬(∀y. D(y,c))"
proof (rule notI)
assume "∀y. D(y,c)"
hence "D(a,c)" by (rule allE)
have "F(c) ∧ ¬D(a,c)" using c by (rule no_implica)
hence "¬D(a,c)" by (rule conjunct2)
thus False using `D(a,c)` by (rule notE)
qed
qed
thus "∃x. F(x) ∧ ¬(∀y. D(y,x))" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 22. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_22a:
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
-- "La demostración estructurada es"
lemma ejercicio_22b:
assumes "∀x. H(x) ∧ P(x) ⟶ (∀y. P(y) ⟶ A(x,y))"
shows "∀x. H(x) ∧ P(x) ⟶ A(x,x)"
proof
fix b
show "H(b) ∧ P(b) ⟶ A(b,b)"
proof
assume "H(b) ∧ P(b)"
hence "P(b)" ..
have "H(b) ∧ P(b) ⟶ (∀y. P(y) ⟶ A(b,y))" using assms ..
hence "∀y. P(y) ⟶ A(b,y)" using `H(b) ∧ P(b)` ..
hence "P(b) ⟶ A(b,b)" ..
thus "A(b,b)" using `P(b)` ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_22c:
assumes "∀x. H(x) ∧ P(x) ⟶ (∀y. P(y) ⟶ A(x,y))"
shows "∀x. H(x) ∧ P(x) ⟶ A(x,x)"
proof (rule allI)
fix b
show "H(b) ∧ P(b) ⟶ A(b,b)"
proof (rule impI)
assume "H(b) ∧ P(b)"
hence "P(b)" by (rule conjunct2)
have "H(b) ∧ P(b) ⟶ (∀y. P(y) ⟶ A(b,y))"
using assms by (rule allE)
hence "∀y. P(y) ⟶ A(b,y)" using `H(b) ∧ P(b)` by (rule mp)
hence "P(b) ⟶ A(b,b)" by (rule allE)
thus "A(b,b)" using `P(b)` by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 23. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_23a:
assumes "¬(∃x. P(x) ∧ R(x))"
"∀x. P(x) ∧ ¬Q(x) ⟶ R(x)"
shows "P(a) ⟶ Q(a)"
using assms
by auto
-- "La demostración estructurada es"
lemma ejercicio_23b:
assumes "¬(∃x. P(x) ∧ R(x))"
"∀x. P(x) ∧ ¬Q(x) ⟶ R(x)"
shows "P(a) ⟶ Q(a)"
proof
assume "P(a)"
show "Q(a)"
proof (rule ccontr)
assume "¬Q(a)"
with `P(a)` have "P(a) ∧ ¬Q(a)" ..
have "P(a) ∧ ¬Q(a) ⟶ R(a)" using assms(2) ..
hence "R(a)" using `P(a) ∧ ¬Q(a)` ..
with `P(a)` have "P(a) ∧ R(a)" ..
hence "∃x. P(x) ∧ R(x)" ..
with assms(1) show False ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_23c:
assumes "¬(∃x. P(x) ∧ R(x))"
"∀x. P(x) ∧ ¬Q(x) ⟶ R(x)"
shows "P(a) ⟶ Q(a)"
proof (rule impI)
assume "P(a)"
show "Q(a)"
proof (rule ccontr)
assume "¬Q(a)"
with `P(a)` have "P(a) ∧ ¬Q(a)" by (rule conjI)
have "P(a) ∧ ¬Q(a) ⟶ R(a)" using assms(2) by (rule allE)
hence "R(a)" using `P(a) ∧ ¬Q(a)` by (rule mp)
with `P(a)` have "P(a) ∧ R(a)" by (rule conjI)
hence "∃x. P(x) ∧ R(x)" by (rule exI)
with assms(1) show False by (rule notE)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 24. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_24a:
assumes
(* 1 *) "∀x. L(x) ⟶ A(x)"
(* 2 *) "∀x. Z(x) ⟶ A(x)"
(* 3 *) "∀x. Pa(x) ⟶ A(x)"
(* 4 *) "∀x. Or(x) ⟶ A(x)"
(* 5 *) "∀x. Ca(x) ⟶ A(x)"
(* 6 *) "∃x. L(x)"
(* 7 *) "∃x. Z(x)"
(* 8 *) "∃x. Pa(x)"
(* 9 *) "∃x. Or(x)"
(* 10 *) "∃x. Ca(x)"
(* 11 *) "∃x. S(x)"
(* 12 *) "∀x. S(x) ⟶ Pl(x)"
(* 13 *) "∀x. A(x) ⟶
(∀y. Pl(y) ⟶ Co(x,y)) ∨
(∀y. A(y) ∧ M(y,x) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(x,y))"
(* 14 *) "∀x y. Pa(y) ∧ (Ca(x) ∨ Or(x)) ⟶ M(x,y)"
(* 15 *) "∀x y. Pa(x) ∧ Z(y) ⟶ M(x,y)"
(* 16 *) "∀x y. Z(x) ∧ L(y) ⟶ M(x,y)"
(* 17 *) "∀x y. L(x) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(x,y)"
(* 18 *) "∀x y. Pa(x) ∧ Or(y) ⟶ Co(x,y)"
(* 19 *) "∀x y. Pa(x) ∧ Ca(y) ⟶ ¬Co(x,y)"
(* 20 *) "∀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
-- "La demostración semiautomática es"
lemma ejercicio_24b:
assumes
(* 1 *) "∀x. L(x) ⟶ A(x)"
(* 2 *) "∀x. Z(x) ⟶ A(x)"
(* 3 *) "∀x. Pa(x) ⟶ A(x)"
(* 4 *) "∀x. Or(x) ⟶ A(x)"
(* 5 *) "∀x. Ca(x) ⟶ A(x)"
(* 6 *) "∃x. L(x)"
(* 7 *) "∃x. Z(x)"
(* 8 *) "∃x. Pa(x)"
(* 9 *) "∃x. Or(x)"
(* 10 *) "∃x. Ca(x)"
(* 11 *) "∃x. S(x)"
(* 12 *) "∀x. S(x) ⟶ Pl(x)"
(* 13 *) "∀x. A(x) ⟶
(∀y. Pl(y) ⟶ Co(x,y)) ∨
(∀y. A(y) ∧ M(y,x) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(x,y))"
(* 14 *) "∀x y. Pa(y) ∧ (Ca(x) ∨ Or(x)) ⟶ M(x,y)"
(* 15 *) "∀x y. Pa(x) ∧ Z(y) ⟶ M(x,y)"
(* 16 *) "∀x y. Z(x) ∧ L(y) ⟶ M(x,y)"
(* 17 *) "∀x y. L(x) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(x,y)"
(* 18 *) "∀x y. Pa(x) ∧ Or(y) ⟶ Co(x,y)"
(* 19 *) "∀x y. Pa(x) ∧ Ca(y) ⟶ ¬Co(x,y)"
(* 20 *) "∀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))"
proof -
obtain l where l: "L(l)" using assms(6) ..
obtain z where z: "Z(z)" using assms(7) ..
obtain p where p: "Pa(p)" using assms(8) ..
obtain c where c: "Ca(c)" using assms(10) ..
obtain s where s: "S(s)" using assms(11) ..
have 1: "Co(p,s)" using p c s assms(3,5,12,13,14,19,20) by meson
have 2: "¬Co(z,s)" using z l s assms(1,2,12,16,17,13) by meson
have 3: "M(p,z)" using p z assms(15) by auto
have 4: "Co(z,p)" using z p s 1 2 3 assms(2,3,12,13) by meson
hence "Co(z,p) ∧ Co(p,s)" using 1 ..
thus "∃x y. A(x) ∧ A(y) ∧ (∃z. S(z) ∧ Co(y,z) ∧ Co(x,y))"
using z p s assms(2,3) by meson
qed
lemma instancia:
assumes "∀x. P(x) ⟶ Q(x)"
"P(a)"
shows "Q(a)"
proof -
have "P(a) ⟶ Q(a)" using assms(1) ..
thus "Q(a)" using assms(2) ..
qed
lemma mt2:
assumes "p ∧ q ∧ r ⟶ s"
"p"
"q"
"¬s"
shows "¬r"
proof
assume "r"
with `q` have "q ∧ r" ..
with `p` have "p ∧ q ∧ r" ..
with assms(1) have "s" ..
with `¬s` show False ..
qed
lemma mp3:
assumes "p ∧ q ∧ r ⟶ s"
"p"
"q"
"r"
shows "s"
proof -
have "q ∧ r" using assms(3,4) ..
with `p` have "p ∧ q ∧ r" ..
with assms(1) show "s" ..
qed
lemma conjI3:
assumes "p"
"q"
"r"
shows "p ∧ q ∧ r"
proof -
have "q ∧ r" using assms(2,3) ..
with `p` show "p ∧ q ∧ r" ..
qed
-- "La demostración estructurada es"
lemma ejercicio_24c:
assumes
(* 1 *) "∀x. L(x) ⟶ A(x)"
(* 2 *) "∀x. Z(x) ⟶ A(x)"
(* 3 *) "∀x. Pa(x) ⟶ A(x)"
(* 4 *) "∀x. Or(x) ⟶ A(x)"
(* 5 *) "∀x. Ca(x) ⟶ A(x)"
(* 6 *) "∃x. L(x)"
(* 7 *) "∃x. Z(x)"
(* 8 *) "∃x. Pa(x)"
(* 9 *) "∃x. Or(x)"
(* 10 *) "∃x. Ca(x)"
(* 11 *) "∃x. S(x)"
(* 12 *) "∀x. S(x) ⟶ Pl(x)"
(* 13 *) "∀x. A(x) ⟶
(∀y. Pl(y) ⟶ Co(x,y)) ∨
(∀y. A(y) ∧ M(y,x) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(x,y))"
(* 14 *) "∀x y. Pa(y) ∧ (Ca(x) ∨ Or(x)) ⟶ M(x,y)"
(* 15 *) "∀x y. Pa(x) ∧ Z(y) ⟶ M(x,y)"
(* 16 *) "∀x y. Z(x) ∧ L(y) ⟶ M(x,y)"
(* 17 *) "∀x y. L(x) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(x,y)"
(* 18 *) "∀x y. Pa(x) ∧ Or(y) ⟶ Co(x,y)"
(* 19 *) "∀x y. Pa(x) ∧ Ca(y) ⟶ ¬Co(x,y)"
(* 20 *) "∀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))"
proof -
obtain l where l: "L(l)" using assms(6) ..
obtain z where z: "Z(z)" using assms(7) ..
obtain p where p: "Pa(p)" using assms(8) ..
obtain c where c: "Ca(c)" using assms(10) ..
obtain s where s: "S(s)" using assms(11) ..
have 1: "Co(p,s)"
proof -
have "¬Co(p,c)"
proof -
have "Pa(p) ∧ Ca(c)" using p c ..
have "∀y. Pa(p) ∧ Ca(y) ⟶ ¬Co(p,y)" using assms(19) ..
hence "Pa(p) ∧ Ca(c) ⟶ ¬Co(p,c)" ..
thus "¬Co(p,c)" using `Pa(p) ∧ Ca(c)` ..
qed
have "∃y. Pl(y) ∧ Co(c,y)"
proof -
have "Or(c) ∨ Ca(c)" using c ..
have "Or(c) ∨ Ca(c) ⟶ (∃y. Pl(y) ∧ Co(c,y))" using assms(20) ..
thus "∃y. Pl(y) ∧ Co(c,y)" using `Or(c) ∨ Ca(c)` ..
qed
have "M(c,p)"
proof -
have "∀y. Pa(y) ∧ (Ca(c) ∨ Or(c)) ⟶ M(c,y)" using assms(14) ..
hence "Pa(p) ∧ (Ca(c) ∨ Or(c)) ⟶ M(c,p)" ..
have "Ca(c) ∨ Or(c)" using c ..
with p have "Pa(p) ∧ (Ca(c) ∨ Or(c))" ..
with `Pa(p) ∧ (Ca(c) ∨ Or(c)) ⟶ M(c,p)` show "M(c,p)" ..
qed
show "Co(p,s)"
proof -
have "A(p)" using assms(3) p by (rule instancia)
have "A(p) ⟶ (∀y. Pl(y) ⟶ Co(p,y)) ∨
(∀y. A(y) ∧ M(y,p) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(p,y))"
using assms(13) ..
hence "(∀y. Pl(y) ⟶ Co(p,y)) ∨
(∀y. A(y) ∧ M(y,p) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(p,y))"
using `A(p)` ..
thus "Co(p,s)"
proof
assume "∀y. Pl(y) ⟶ Co(p,y)"
hence "Pl(s) ⟶ Co(p,s)" ..
have "Pl(s)" using assms(12) s by (rule instancia)
with `Pl(s) ⟶ Co(p,s)` show "Co(p,s)" ..
next
assume "∀y. A(y) ∧ M(y,p) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(p,y)"
hence "A(c) ∧ M(c,p) ∧ (∃z. Pl(z) ∧ Co(c,z)) ⟶ Co(p,c)" ..
have "Co(p,c)"
proof -
have "A(c)" using assms(5) c by (rule instancia)
have "M(c,p) ∧ (∃z. Pl(z) ∧ Co(c,z))"
using `M(c,p)` `∃z. Pl(z) ∧ Co(c,z)` ..
with `A(c)` have "A(c) ∧ M(c,p) ∧ (∃z. Pl(z) ∧ Co(c,z))" ..
with `A(c) ∧ M(c,p) ∧ (∃z. Pl(z) ∧ Co(c,z)) ⟶ Co(p,c)`
show "Co(p,c)" ..
qed
with `¬Co(p,c)` show "Co(p,s)" ..
qed
qed
qed
have 2: "¬Co(z,s)"
proof -
have "M(z,l)"
proof -
have "Z(z) ∧ L(l)" using z l ..
have "∀y. Z(z) ∧ L(y) ⟶ M(z,y)" using assms(16) ..
hence "Z(z) ∧ L(l) ⟶ M(z,l)" ..
thus "M(z,l)" using `Z(z) ∧ L(l)` ..
qed
have "¬Co(l,z)"
proof -
have "∀y. L(l) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(l,y)" using assms(17) ..
hence "L(l) ∧ (Z(z)∨ S(z)) ⟶ ¬Co(l,z)" ..
have "Z(z)∨ S(z)" using z ..
with l have "L(l) ∧ (Z(z)∨ S(z))" ..
with `L(l) ∧ (Z(z)∨ S(z)) ⟶ ¬Co(l,z)` show "¬Co(l,z)" ..
qed
have "¬Co(l,s)"
proof -
have "∀y. L(l) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(l,y)" using assms(17) ..
hence "L(l) ∧ (Z(s)∨ S(s)) ⟶ ¬Co(l,s)" ..
have "Z(s)∨ S(s)" using s ..
with l have "L(l) ∧ (Z(s)∨ S(s))" ..
with `L(l) ∧ (Z(s)∨ S(s)) ⟶ ¬Co(l,s)` show "¬Co(l,s)" ..
qed
show "¬Co(z,s)"
proof -
have "A(l)" using assms(1) l by (rule instancia)
have "A(l) ⟶ (∀y. Pl(y) ⟶ Co(l,y)) ∨
(∀y. A(y) ∧ M(y,l) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(l,y))"
using assms(13) ..
hence "(∀y. Pl(y) ⟶ Co(l,y)) ∨
(∀y. A(y) ∧ M(y,l) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(l,y))"
using `A(l)` ..
thus "¬Co(z,s)"
proof
assume "∀y. Pl(y) ⟶ Co(l,y)"
hence "Pl(s) ⟶ Co(l,s)" ..
have "Pl(s)" using assms(12) s by (rule instancia)
with `Pl(s) ⟶ Co(l,s)` have "Co(l,s)" ..
with `¬Co(l,s)` show "¬Co(z,s)" ..
next
assume "∀y. A(y) ∧ M(y,l) ∧ (∃u. Pl(u) ∧ Co(y,u)) ⟶ Co(l,y)"
hence zl: "A(z) ∧ M(z,l) ∧ (∃u. Pl(u) ∧ Co(z,u)) ⟶ Co(l,z)" ..
have "A(z)" using assms(2) z by (rule instancia)
have "¬(∃u. Pl(u) ∧ Co(z,u))"
using zl `A(z)` `M(z,l)` `¬Co(l,z)` by (rule mt2)
show "¬Co(z,s)"
proof
assume "Co(z,s)"
have "Pl(s)" using assms(12) s by (rule instancia)
hence "Pl(s) ∧ Co(z,s)" using `Co(z,s)` ..
hence "∃u. Pl(u) ∧ Co(z,u)" ..
with `¬(∃u. Pl(u) ∧ Co(z,u))` show False ..
qed
qed
qed
qed
have 3: "M(p,z)"
proof -
have "Pa(p) ∧ Z(z)" using p z ..
have "∀y. Pa(p) ∧ Z(y) ⟶ M(p,y)" using assms(15) ..
hence "Pa(p) ∧ Z(z) ⟶ M(p,z)" ..
thus "M(p,z)" using `Pa(p) ∧ Z(z)` ..
qed
have 4: "Co(z,p)"
proof -
have "A(z)" using assms(2) z by (rule instancia)
have "A(z) ⟶ (∀y. Pl(y) ⟶ Co(z,y)) ∨
(∀y. A(y) ∧ M(y,z) ∧ (∃u. Pl(u) ∧ Co(y,u)) ⟶ Co(z,y))"
using assms(13) ..
hence "(∀y. Pl(y) ⟶ Co(z,y)) ∨
(∀y. A(y) ∧ M(y,z) ∧ (∃u. Pl(u) ∧ Co(y,u)) ⟶ Co(z,y))"
using `A(z)` ..
thus "Co(z,p)"
proof
assume "∀y. Pl(y) ⟶ Co(z,y)"
hence "Pl(s) ⟶ Co(z,s)" ..
have "Pl(s)" using assms(12) s by (rule instancia)
with `Pl(s) ⟶ Co(z,s)` have "Co(z,s)" ..
with `¬Co(z,s)` show "Co(z,p)" ..
next
assume "∀y. A(y) ∧ M(y,z) ∧ (∃u. Pl(u) ∧ Co(y,u)) ⟶ Co(z,y)"
hence pz: "A(p) ∧ M(p,z) ∧ (∃u. Pl(u) ∧ Co(p,u)) ⟶ Co(z,p)" ..
have "A(p)" using assms(3) p by (rule instancia)
have "∃u. Pl(u) ∧ Co(p,u)"
proof -
have "Pl(s)" using assms(12) s by (rule instancia)
hence "Pl(s) ∧ Co(p,s)" using `Co(p,s)` ..
thus "∃u. Pl(u) ∧ Co(p,u)" ..
qed
show "Co(z,p)" using pz `A(p)` `M(p,z)` `∃u. Pl(u) ∧ Co(p,u)`
by (rule mp3)
qed
qed
hence "Co(z,p) ∧ Co(p,s)" using 1 ..
show "∃x y. A(x) ∧ A(y) ∧ (∃u. S(u) ∧ Co(y,u) ∧ Co(x,y))"
proof -
have "A(z)" using assms(2) z by (rule instancia)
have "A(p)" using assms(3) p by (rule instancia)
have "S(s) ∧ Co(p,s) ∧ Co(z,p)" using s `Co(p,s)` `Co(z,p)`
by (rule conjI3)
hence "∃u. S(u) ∧ Co(p,u) ∧ Co(z,p)" ..
have "A(z) ∧ A(p) ∧ (∃u. S(u) ∧ Co(p,u) ∧ Co(z,p))"
using `A(z)` `A(p)` `∃u. S(u) ∧ Co(p,u) ∧ Co(z,p)`
by (rule conjI3)
hence "∃y. A(z) ∧ A(y) ∧ (∃u. S(u) ∧ Co(y,u) ∧ Co(z,y))" ..
thus "∃x y. A(x) ∧ A(y) ∧ (∃u. S(u) ∧ Co(y,u) ∧ Co(x,y))" ..
qed
qed
end