header {* T2R2a: Argumentación en lógica de primer orden *}
theory T2R2a
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar y demostrar la corrección
de los argumentos usando sólo las reglas básicas de deducción natural
de la lógica de primer orden (sin usar el método auto).
Las reglas básicas de la deducción natural son las siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· 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
· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q
---------------------------------------------------------------------
*}
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
lemma no_ex: "¬(∃x. P(x)) ⟹ ∀x. ¬P(x)"
by auto
lemma no_para_todo: "¬(∀x. P(x)) ⟹ ∃x. ¬P(x)"
by auto
text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar, y demostrar la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_1a:
"⟦H(s); ∀x. H(x) ⟶ M(x)⟧ ⟹ M(s)"
by auto
-- "La demostración estructurada es"
lemma ejercicio_1b:
assumes "H(s)"
"∀x. H(x) ⟶ M(x)"
shows "M(s)"
proof -
have "H(s) ⟶ M(s)" using assms(2) ..
thus "M(s)" using assms(1) ..
qed
-- "La demostración detallada es"
lemma ejercicio_1c:
assumes "H(s)"
"∀x. H(x) ⟶ M(x)"
shows "M(s)"
proof -
have "H(s) ⟶ M(s)" using assms(2) by (rule allE)
thus "M(s)" using assms(1) by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar, y decidir la corrección, del 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_2a:
"(∃x. I(x)) ∧ (∃x. T(x)) ⟹ ∃x. I(x) ∧ T(x)"
quickcheck
oops
text {*
El argumento es incorrecto como muestra el siguiente contraejemplo:
I = {a1}
T = {a2}
*}
text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar, y decidir la corrección, del 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_3a:
"⟦∀x. P(x) ⟶ V(x);
∀x y. V(x) ∧ V(y) ⟶ x=y;
∀x y. P(x) ∧ P(y) ⟶ x=y⟧
⟹ ∃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, y decidir la corrección, del 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_4a:
"⟦∀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))⟧
⟹ ∃x. A(x) ∧ Co(x)"
by metis
-- "La demostración estructurada es"
lemma ejercicio_4b:
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)"
proof -
obtain a where a: "Co(a) ∧ E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))"
using assms(2) ..
have "∃y. A(y) ∧ Ca(y,a)"
proof -
have "E(a) ∧ ¬V(a) ⟶ (∃y. A(y) ∧ Ca(y,a))" using assms(1) ..
moreover
have "E(a) ∧ ¬V(a)"
proof
have "E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" using a ..
thus "E(a)" ..
next
have "∀x. ¬(Co(x) ∧ V(x))" using assms(3) by (rule no_ex)
hence "¬(Co(a) ∧ V(a))" ..
have "Co(a)" using a ..
show "¬V(a)"
proof
assume "V(a)"
with `Co(a)` have "Co(a) ∧ V(a)" ..
with `¬(Co(a) ∧ V(a))` show False ..
qed
qed
ultimately show "∃y. A(y) ∧ Ca(y,a)" ..
qed
then obtain b where "A(b) ∧ Ca(b,a)" ..
hence "A(b)" ..
moreover
have "Co(b)"
proof -
have "E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" using a ..
hence "∀y. Ca(y,a) ⟶ Co(y)" ..
hence "Ca(b,a) ⟶ Co(b)" ..
have "Ca(b,a)" using `A(b) ∧ Ca(b,a)` ..
with `Ca(b,a) ⟶ Co(b)` show "Co(b)" ..
qed
ultimately have "A(b) ∧ Co(b)" ..
thus "∃x. A(x) ∧ Co(x)" ..
qed
-- "La demostración detallada es"
lemma ejercicio_4c:
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)"
proof -
obtain a where a: "Co(a) ∧ E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))"
using assms(2) by (rule exE)
have "∃y. A(y) ∧ Ca(y,a)"
proof -
have "E(a) ∧ ¬V(a) ⟶ (∃y. A(y) ∧ Ca(y,a))" using assms(1) by (rule allE)
moreover
have "E(a) ∧ ¬V(a)"
proof
have "E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" using a by (rule conjunct2)
thus "E(a)" by (rule conjunct1)
next
have "∀x. ¬(Co(x) ∧ V(x))" using assms(3) by (rule no_ex)
hence "¬(Co(a) ∧ V(a))" by (rule allE)
have "Co(a)" using a by (rule conjunct1)
show "¬V(a)"
proof (rule notI)
assume "V(a)"
with `Co(a)` have "Co(a) ∧ V(a)" by (rule conjI)
with `¬(Co(a) ∧ V(a))` show False by (rule notE)
qed
qed
ultimately show "∃y. A(y) ∧ Ca(y,a)" by (rule mp)
qed
then obtain b where "A(b) ∧ Ca(b,a)" by (rule exE)
hence "A(b)" by (rule conjunct1)
moreover
have "Co(b)"
proof -
have "E(a) ∧ (∀y. Ca(y,a) ⟶ Co(y))" using a by (rule conjunct2)
hence "∀y. Ca(y,a) ⟶ Co(y)" by (rule conjunct2)
hence "Ca(b,a) ⟶ Co(b)" by (rule allE)
have "Ca(b,a)" using `A(b) ∧ Ca(b,a)` by (rule conjunct2)
with `Ca(b,a) ⟶ Co(b)` show "Co(b)" by (rule mp)
qed
ultimately have "A(b) ∧ Co(b)" by (rule conjI)
thus "∃x. A(x) ∧ Co(x)" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_5a:
"⟦T(j,m); T(j,p)⟧ ⟹ ∃x. T(x,m) ∧ T(x,p)"
by auto
-- "La demostración estructurada es"
lemma ejercicio_5b:
assumes "T(j,m)"
"T(j,p)"
shows "∃x. T(x,m) ∧ T(x,p)"
proof
show "T(j,m) ∧ T(j,p)" using assms ..
qed
-- "La demostración detallada es"
lemma ejercicio_5c:
assumes "T(j,m)"
"T(j,p)"
shows "∃x. T(x,m) ∧ T(x,p)"
proof (rule exI)
show "T(j,m) ∧ T(j,p)" using assms by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_6a:
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
-- "La demostración estructurada es"
lemma ejercicio_6b:
fixes H P :: "'a × 'a ⇒ bool"
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)"
proof -
have "H(l,j) ∧ P(c,l) ⟶ P(c,j)"
proof -
have "∀y z. H(l,y) ∧ P(z,l) ⟶ P(z,y)" using assms(2) ..
hence "∀z. H(l,j) ∧ P(z,l) ⟶ P(z,j)" ..
thus "H(l,j) ∧ P(c,l) ⟶ P(c,j)" ..
qed
moreover
have "H(l,j) ∧ P(c,l)"
proof
have "∀y. H(j,y) ⟶ H(y,j)" using assms(1) ..
hence "H(j,l) ⟶ H(l,j)" ..
thus "H(l,j)" using assms(3) ..
next
show "P(c,l)" using assms(4) .
qed
ultimately show "P(c,j)" ..
qed
-- "La demostración detallada es"
lemma ejercicio_6c:
fixes H P :: "'a × 'a ⇒ bool"
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)"
proof -
have "H(l,j) ∧ P(c,l) ⟶ P(c,j)"
proof -
have "∀y z. H(l,y) ∧ P(z,l) ⟶ P(z,y)" using assms(2) by (rule allE)
hence "∀z. H(l,j) ∧ P(z,l) ⟶ P(z,j)" by (rule allE)
thus "H(l,j) ∧ P(c,l) ⟶ P(c,j)" by (rule allE)
qed
moreover
have "H(l,j) ∧ P(c,l)"
proof (rule conjI)
have "∀y. H(j,y) ⟶ H(y,j)" using assms(1) by (rule allE)
hence "H(j,l) ⟶ H(l,j)" by (rule allE)
thus "H(l,j)" using assms(3) by (rule mp)
next
show "P(c,l)" using assms(4) by this
qed
ultimately show "P(c,j)" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar, y decidir la corrección, del 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_7a:
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
-- "La demostración estructurada es"
lemma ejercicio_7b:
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)"
proof
fix a
show "D(a,t) ⟶ S(a)"
proof
assume "D(a,t)"
have "∀x. Pr(x) ⟶ A(x)" using assms(1) assms(3) ..
hence "Pr(t) ⟶ A(t)" ..
hence "A(t)" using assms(4) ..
have "A(t) ⟶ (∀y. D(y,t) ⟶ S(y))" using assms(2) ..
hence "∀y. D(y,t) ⟶ S(y)" using `A(t)` ..
hence "D(a,t) ⟶ S(a)" ..
thus "S(a)" using `D(a,t)` ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_7c:
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)"
proof (rule allI)
fix a
show "D(a,t) ⟶ S(a)"
proof (rule impI)
assume "D(a,t)"
have "∀x. Pr(x) ⟶ A(x)" using assms(1) assms(3) by (rule mp)
hence "Pr(t) ⟶ A(t)" by (rule allE)
hence "A(t)" using assms(4) by (rule mp)
have "A(t) ⟶ (∀y. D(y,t) ⟶ S(y))" using assms(2) by (rule allE)
hence "∀y. D(y,t) ⟶ S(y)" using `A(t)` by (rule mp)
hence "D(a,t) ⟶ S(a)" by (rule allE)
thus "S(a)" using `D(a,t)` by (rule mp)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar, y decidir la corrección, del 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_8a:
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 blast
-- "La demostración estructurada es"
lemma ejercicio_8b:
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)"
proof -
obtain a where a: "M(a) ∧ E(a) ∧ (∀y. I(y,a) ⟶ M(y))" using assms(2) ..
hence "M(a)" ..
have "M(a) ⟶ ¬P(a)" using assms(3) ..
hence "¬P(a)" using `M(a)` ..
have a1: "E(a) ∧ (∀y. I(y,a) ⟶ M(y))" using a ..
hence "E(a)" ..
hence "E(a) ∧ ¬P(a)" using `¬P(a)` ..
have "E(a) ∧ ¬P(a) ⟶ (∃y. A(y) ∧ I(y,a))" using assms(1) ..
hence "∃y. A(y) ∧ I(y,a)" using `E(a) ∧ ¬P(a)`..
then obtain b where b: "A(b) ∧ I(b,a)" ..
have "A(b) ∧ M(b)"
proof
show "A(b)" using b ..
next
have "I(b,a)" using b ..
have "∀y. I(y,a) ⟶ M(y)" using a1 ..
hence "I(b,a) ⟶ M(b)" ..
thus "M(b)" using `I(b,a)` ..
qed
thus "∃x. A(x) ∧ M(x)" ..
qed
-- "La demostración detallada es"
lemma ejercicio_8c:
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)"
proof -
obtain a where a: "M(a) ∧ E(a) ∧ (∀y. I(y,a) ⟶ M(y))"
using assms(2) by (rule exE)
hence "M(a)" by (rule conjunct1)
have "M(a) ⟶ ¬P(a)" using assms(3) by (rule allE)
hence "¬P(a)" using `M(a)` by (rule mp)
have a1: "E(a) ∧ (∀y. I(y,a) ⟶ M(y))" using a by (rule conjunct2)
hence "E(a)" by (rule conjunct1)
hence "E(a) ∧ ¬P(a)" using `¬P(a)` by (rule conjI)
have "E(a) ∧ ¬P(a) ⟶ (∃y. A(y) ∧ I(y,a))"
using assms(1) by (rule allE)
hence "∃y. A(y) ∧ I(y,a)" using `E(a) ∧ ¬P(a)`by (rule mp)
then obtain b where b: "A(b) ∧ I(b,a)" by (rule exE)
have "A(b) ∧ M(b)"
proof (rule conjI)
show "A(b)" using b by (rule conjunct1)
next
have "I(b,a)" using b by (rule conjunct2)
have "∀y. I(y,a) ⟶ M(y)" using a1 by (rule conjunct2)
hence "I(b,a) ⟶ M(b)" by (rule allE)
thus "M(b)" using `I(b,a)`by (rule mp)
qed
thus "∃x. A(x) ∧ M(x)" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar, y decidir la corrección, del 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_9a:
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 blast
-- "La demostración estructurada es"
lemma ejercicio_9b:
assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
"∀x. E(x) ⟶ ¬Ap(j,x)"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
proof
assume "∃x. E(x) ∧ N(x)"
then obtain a where a: "E(a) ∧ N(a)" ..
show "¬Af(j)"
proof
assume "Af(j)"
have "Af(j) ⟶ (∀y. E(y) ⟶ Ap(j,y))" using assms(1) ..
hence "∀y. E(y) ⟶ Ap(j,y)" using `Af(j)` ..
hence "E(a) ⟶ Ap(j,a)" ..
have "E(a)" using a ..
with `E(a) ⟶ Ap(j,a)` have "Ap(j,a)" ..
have "E(a) ⟶ ¬Ap(j,a)" using assms(2) ..
hence "¬Ap(j,a)" using `E(a)` ..
thus False using `Ap(j,a)` ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_9c:
assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
"∀x. E(x) ⟶ ¬Ap(j,x)"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
proof (rule impI)
assume "∃x. E(x) ∧ N(x)"
then obtain a where a: "E(a) ∧ N(a)" by (rule exE)
show "¬Af(j)"
proof (rule notI)
assume "Af(j)"
have "Af(j) ⟶ (∀y. E(y) ⟶ Ap(j,y))" using assms(1) by (rule allE)
hence "∀y. E(y) ⟶ Ap(j,y)" using `Af(j)` by (rule mp)
hence "E(a) ⟶ Ap(j,a)" by (rule allE)
have "E(a)" using a by (rule conjunct1)
with `E(a) ⟶ Ap(j,a)` have "Ap(j,a)" by (rule mp)
have "E(a) ⟶ ¬Ap(j,a)" using assms(2) by (rule allE)
hence "¬Ap(j,a)" using `E(a)` by (rule mp)
thus False using `Ap(j,a)` by (rule notE)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar, y decidir la corrección, del 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_10a:
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 blast
-- "La demostración estructurada es"
lemma ejercicio_10b:
assumes "∀x. A(x) ∧ G(x) ⟶ L(x) ∧ V(x)"
"∃x. A(x) ∧ V(x) ∧ ¬L(x)"
shows "∃x. A(x) ∧ ¬G(x)"
proof -
obtain b where b: "A(b) ∧ V(b) ∧ ¬L(b)" using assms(2) ..
have "A(b) ∧ ¬G(b)"
proof
show "A(b)" using b ..
next
show "¬G(b)"
proof
assume "G(b)"
have "¬L(b)"
proof -
have "V(b) ∧ ¬L(b)" using b ..
thus "¬L(b)" ..
qed
moreover have "L(b)"
proof -
have "A(b) ∧ G(b) ⟶ L(b) ∧ V(b)" using assms(1) ..
have "A(b)" using b ..
hence "A(b) ∧ G(b)" using `G(b)` ..
with `A(b) ∧ G(b) ⟶ L(b) ∧ V(b)` have "L(b) ∧ V(b)" ..
thus "L(b)" ..
qed
ultimately show False ..
qed
qed
thus "∃x. A(x) ∧ ¬G(x)" ..
qed
-- "La demostración detallada es"
lemma ejercicio_10c:
assumes "∀x. A(x) ∧ G(x) ⟶ L(x) ∧ V(x)"
"∃x. A(x) ∧ V(x) ∧ ¬L(x)"
shows "∃x. A(x) ∧ ¬G(x)"
proof -
obtain b where b: "A(b) ∧ V(b) ∧ ¬L(b)" using assms(2) by (rule exE)
have "A(b) ∧ ¬G(b)"
proof (rule conjI)
show "A(b)" using b by (rule conjunct1)
next
show "¬G(b)"
proof (rule notI)
assume "G(b)"
have "¬L(b)"
proof -
have "V(b) ∧ ¬L(b)" using b by (rule conjunct2)
thus "¬L(b)" by (rule conjunct2)
qed
moreover have "L(b)"
proof -
have "A(b) ∧ G(b) ⟶ L(b) ∧ V(b)" using assms(1) by (rule allE)
have "A(b)" using b by (rule conjunct1)
hence "A(b) ∧ G(b)" using `G(b)` by (rule conjI)
with `A(b) ∧ G(b) ⟶ L(b) ∧ V(b)` have "L(b) ∧ V(b)" by (rule mp)
thus "L(b)" by (rule conjunct1)
qed
ultimately show False by (rule notE)
qed
qed
thus "∃x. A(x) ∧ ¬G(x)" by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_11a:
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 blast
-- "La demostración estructurada es"
lemma ejercicio_11b:
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))"
proof
fix a
have "¬E(a) ∨ E(a)" ..
thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))"
proof
assume "¬E(a)"
thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))" ..
next
assume "E(a)"
have "E(a) ⟶ C(a,m) ∧ ¬A(a,m)" using assms(3) ..
hence "C(a,m) ∧ ¬A(a,m)" using `E(a)` ..
hence "C(a,m)" ..
have "∀y. C(a,y) ⟶ A(a,y) ∨ I(a)" using assms(1) ..
hence "C(a,m) ⟶ A(a,m) ∨ I(a)" ..
hence "A(a,m) ∨ I(a)" using `C(a,m)` ..
hence "¬R(a)"
proof
assume "A(a,m)"
have "¬A(a,m)" using `C(a,m) ∧ ¬A(a,m)`..
thus "¬R(a)" using `A(a,m)` ..
next
assume "I(a)"
have "I(a) ⟶ ¬R(a)" using assms(2) ..
thus "¬R(a)" using `I(a)` ..
qed
with `C(a,m)` have "C(a,m) ∧ ¬R(a)" ..
thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))" ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_11c:
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))"
proof (rule allI)
fix a
have "¬E(a) ∨ E(a)" by (rule excluded_middle)
thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))"
proof (rule disjE)
assume "¬E(a)"
thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))" by (rule disjI1)
next
assume "E(a)"
have "E(a) ⟶ C(a,m) ∧ ¬A(a,m)" using assms(3) by (rule allE)
hence "C(a,m) ∧ ¬A(a,m)" using `E(a)` by (rule mp)
hence "C(a,m)" by (rule conjunct1)
have "∀y. C(a,y) ⟶ A(a,y) ∨ I(a)" using assms(1) by (rule allE)
hence "C(a,m) ⟶ A(a,m) ∨ I(a)" by (rule allE)
hence "A(a,m) ∨ I(a)" using `C(a,m)` by (rule mp)
hence "¬R(a)"
proof (rule disjE)
assume "A(a,m)"
have "¬A(a,m)" using `C(a,m) ∧ ¬A(a,m)`by (rule conjunct2)
thus "¬R(a)" using `A(a,m)` by (rule notE)
next
assume "I(a)"
have "I(a) ⟶ ¬R(a)" using assms(2) by (rule allE)
thus "¬R(a)" using `I(a)` by (rule mp)
qed
with `C(a,m)` have "C(a,m) ∧ ¬R(a)" by (rule conjI)
thus "¬E(a) ∨ (C(a,m) ∧ ¬R(a))" by (rule disjI2)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_12a:
assumes "∀x. ¬R(x) ⟶ R(p(x))"
shows "∃x. R(x) ∧ R(p(p(x)))"
using assms
by blast
-- "La demostración estructurada es"
lemma ejercicio_12b:
assumes "∀x. ¬R(x) ⟶ R(p(x))"
shows "∃x. R(x) ∧ R(p(p(x)))"
proof -
have "∃x. R(x)"
proof (rule ccontr)
assume "¬(∃x. R(x))"
hence "∀x. ¬R(x)" by (rule no_ex)
hence "¬R(a)" ..
have "¬R(a) ⟶ R(p(a))" using assms ..
hence "R(p(a))" using `¬R(a)` ..
hence "∃x. R(x)" ..
with `¬(∃x. R(x))` show False ..
qed
then obtain a where "R(a)" ..
have "¬R(p(p(a))) ∨ R(p(p(a)))" by (rule excluded_middle)
thus "∃x. R(x) ∧ R(p(p(x)))"
proof
assume "¬R(p(p(a)))"
have "R(p(a)) ∧ R(p(p(p(a))))"
proof
show "R(p(a))"
proof (rule ccontr)
assume "¬R(p(a))"
have "¬R(p(a)) ⟶ R(p(p(a)))" using assms ..
hence "R(p(p(a)))" using `¬R(p(a))` ..
with `¬R(p(p(a)))` show False ..
qed
next
show "R(p(p(p(a))))"
proof -
have "¬R(p(p(a))) ⟶ R(p(p(p(a))))" using assms ..
thus "R(p(p(p(a))))" using `¬R(p(p(a)))` ..
qed
qed
thus "∃x. R(x) ∧ R(p(p(x)))" ..
next
assume "R(p(p(a)))"
with `R(a)` have "R(a) ∧ R(p(p(a)))" ..
thus "∃x. R(x) ∧ R(p(p(x)))" ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_12c:
assumes "∀x. ¬R(x) ⟶ R(p(x))"
shows "∃x. R(x) ∧ R(p(p(x)))"
proof -
have "∃x. R(x)"
proof (rule ccontr)
assume "¬(∃x. R(x))"
hence "∀x. ¬R(x)" by (rule no_ex)
hence "¬R(a)" by (rule allE)
have "¬R(a) ⟶ R(p(a))" using assms by (rule allE)
hence "R(p(a))" using `¬R(a)` by (rule mp)
hence "∃x. R(x)" by (rule exI)
with `¬(∃x. R(x))` show False by (rule notE)
qed
then obtain a where "R(a)" by (rule exE)
have "¬R(p(p(a))) ∨ R(p(p(a)))" by (rule excluded_middle)
thus "∃x. R(x) ∧ R(p(p(x)))"
proof (rule disjE)
assume "¬R(p(p(a)))"
have "R(p(a)) ∧ R(p(p(p(a))))"
proof (rule conjI)
show "R(p(a))"
proof (rule ccontr)
assume "¬R(p(a))"
have "¬R(p(a)) ⟶ R(p(p(a)))" using assms by (rule allE)
hence "R(p(p(a)))" using `¬R(p(a))` by (rule mp)
with `¬R(p(p(a)))` show False by (rule notE)
qed
next
show "R(p(p(p(a))))"
proof -
have "¬R(p(p(a))) ⟶ R(p(p(p(a))))" using assms by (rule allE)
thus "R(p(p(p(a))))" using `¬R(p(p(a)))` by (rule mp)
qed
qed
thus "∃x. R(x) ∧ R(p(p(x)))" by (rule exI)
next
assume "R(p(p(a)))"
with `R(a)` have "R(a) ∧ R(p(p(a)))" by (rule conjI)
thus "∃x. R(x) ∧ R(p(p(x)))" by (rule exI)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 13. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_13a:
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, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_14a:
assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
"A(a)"
"¬Ob(b,a)"
shows "¬R(b)"
using assms
by blast
-- "La demostración estructurada es"
lemma ejercicio_14b:
fixes R A :: "'a ⇒ bool" and
Ob :: "'a × 'a ⇒ bool"
assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
"A(a)"
"¬Ob(b,a)"
shows "¬R(b)"
proof
assume "R(b)"
have "∀y. R(b) ∧ A(y) ⟶ Ob(b,y)" using assms(1) ..
hence "R(b) ∧ A(a) ⟶ Ob(b,a)" ..
have "R(b) ∧ A(a)" using `R(b)` assms(2) ..
with `R(b) ∧ A(a) ⟶ Ob(b,a)` have "Ob(b,a)" ..
with assms(3) show False ..
qed
-- "La demostración detallada es"
lemma ejercicio_14c:
fixes R A :: "'a ⇒ bool" and
Ob :: "'a × 'a ⇒ bool"
assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
"A(a)"
"¬Ob(b,a)"
shows "¬R(b)"
proof (rule notI)
assume "R(b)"
have "∀y. R(b) ∧ A(y) ⟶ Ob(b,y)" using assms(1) by (rule allE)
hence "R(b) ∧ A(a) ⟶ Ob(b,a)" by (rule allE)
have "R(b) ∧ A(a)" using `R(b)` assms(2) by (rule conjI)
with `R(b) ∧ A(a) ⟶ Ob(b,a)` have "Ob(b,a)" by (rule mp)
with assms(3) show False by (rule notE)
qed
text {* ---------------------------------------------------------------
Ejercicio 15. Formalizar, y decidir la corrección, del 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
------------------------------------------------------------------ *}
-- "La demostración automática es"
lemma ejercicio_15a:
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
-- "La demostración estructurada es"
lemma ejercicio_15b:
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)"
proof -
obtain a where a: "∀y. ¬C(a,y) ⟶ (∃z. T(z) ∨ P(z,y))"
using assms(1) ..
have "∃y. ¬C(a,y)" using assms(2) ..
then obtain b where "¬C(a,b)" ..
have "¬C(a,b) ⟶ (∃z. T(z) ∨ P(z,b))" using a ..
hence "∃z. T(z) ∨ P(z,b)" using `¬C(a,b)` ..
then obtain c where "T(c) ∨ P(c,b)" ..
thus "∃x. T(x)"
proof
assume "T(c)"
thus "∃x. T(x)" ..
next
assume "P(c,b)"
have "∀y. ¬P(c,y)" using assms(3) ..
hence "¬P(c,b)" ..
thus "∃x. T(x)" using `P(c,b)` ..
qed
qed
-- "La demostración detallada es"
lemma ejercicio_15c:
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)"
proof -
obtain a where a: "∀y. ¬C(a,y) ⟶ (∃z. T(z) ∨ P(z,y))"
using assms(1) by (rule exE)
have "∃y. ¬C(a,y)" using assms(2) by (rule allE)
then obtain b where "¬C(a,b)" by (rule exE)
have "¬C(a,b) ⟶ (∃z. T(z) ∨ P(z,b))" using a by (rule allE)
hence "∃z. T(z) ∨ P(z,b)" using `¬C(a,b)` by (rule mp)
then obtain c where "T(c) ∨ P(c,b)" by (rule exE)
thus "∃x. T(x)"
proof (rule disjE)
assume "T(c)"
thus "∃x. T(x)" by (rule exI)
next
assume "P(c,b)"
have "∀y. ¬P(c,y)" using assms(3) by (rule allE)
hence "¬P(c,b)" by (rule allE)
thus "∃x. T(x)" using `P(c,b)` by (rule notE)
qed
qed
end
