chapter {* R7: Deducción natural de primer orden *}
theory R7_Deduccion_natural_de_primer_orden_alu
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
· 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
· 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, mt y not_ex 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
text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------ *}
(* benber *)
lemma
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof (rule ccontr)
assume "∄x. P a ⟶ Q x"
have "P a ⟶ (∃x. P a ⟶ Q x)"
proof
assume "P a"
with assms have "∃x. Q x" by (rule mp)
moreover have "⋀x. Q x ⟹ ∃x'. P a ⟶ Q x'"
proof -
fix x
assume "Q x"
hence "P a ⟶ Q x" by (rule impI)
thus "∃x'. P a ⟶ Q x'" by (rule exI)
qed
ultimately show "∃x. P a ⟶ Q x" by (rule exE)
qed
moreover note `∄x. P a ⟶ Q x`
ultimately have "¬(P a)" by (rule mt)
have "¬(P a) ⟶ (∃x. P a ⟶ Q x)"
proof
fix x
assume "¬(P a)"
have "P a ⟶ Q x"
proof
assume "P a"
with `¬(P a)` have "False" by (rule notE)
thus "Q x" by (rule FalseE)
qed
thus "∃x. P a ⟶ Q x" by (rule exI)
qed
moreover note `∄x. P a ⟶ Q x`
ultimately have "¬¬(P a)" by (rule mt)
moreover note `¬(P a)`
ultimately show "False" by (rule notE)
qed
(* alfmarcua *)
lemma ejercicio_52:
"p ∨ ¬p"
proof (rule ccontr)
assume 1: "¬(p ∨ ¬p)"
have 2: "¬p" proof (rule notI)
assume p hence 3: "p ∨ ¬p" by (rule disjI1)
show "False" using 1 3 by (rule notE)
qed
have 4: "p ∨ ¬p" using 2 by (rule disjI2)
show "False" using 1 4 by (rule notE)
qed
lemma ejercicio_1:
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof (rule disjE)
show "P a ∨ ¬ P a" by (rule ejercicio_52)
next
assume "P a"
have "∃x. Q x" using assms `P a` by (rule mp)
then obtain b where "Q b" by (rule exE)
have "P a ⟹ Q b" using `P a` `Q b` by simp
have "P a ⟶ Q b" using `P a ⟹ Q b` by (rule impI)
then show "∃x. P a ⟶ Q x" by (rule exI)
next
assume "¬ P a"
fix b
have "P a ⟶ Q b"
proof (rule impI)
assume "P a"
with `¬(P a)` have "False" by (rule notE)
then show "Q b" by (rule FalseE)
qed
thus "∃x. P a ⟶ Q x" by (rule exI)
qed
(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2
hugrubsan pabbergue enrparalv giafus1 antramhur *)
lemma ejercicio_1b:
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof (rule disjE)
show "¬P a ∨ P a" by (rule excluded_middle)
next
fix b
assume 3: "¬P a"
have "P a ⟶ Q b" proof (rule impI)
assume 4: "P a" show "Q b" using 3 4 by (rule notE)
qed
thus ?thesis by (rule exI)
next
assume 1: "P a"
have "∃x. Q x" using assms(1) 1 by (rule mp)
then obtain b where 2: "Q b" by (rule exE)
have "P a ⟶ Q b" proof (rule impI)
assume "P a" show "Q b" using 2 .
qed
thus ?thesis by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
{∀x y z. R x y ∧ R y z ⟶ R x z,
∀x. ¬(R x x)}
⊢ ∀x y. R x y ⟶ ¬(R y x)
------------------------------------------------------------------ *}
(* benber *)
lemma
assumes A1: "∀x y z. R x y ∧ R y z ⟶ R x z"
and A2: "∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof -
{
fix x y
{
assume "R x y"
have "¬ (R y x)"
proof (rule ccontr)
assume "¬ ¬ (R y x)"
hence "R y x" by (rule notnotD)
note `∀x y z. R x y ∧ R y z ⟶ R x z`
moreover have "∀ y z. R x y ∧ R y z ⟶ R x z ⟹ False"
proof -
assume "∀ y z. R x y ∧ R y z ⟶ R x z"
moreover have "∀ z. R x y ∧ R y z ⟶ R x z ⟹ False"
proof -
assume "∀ z. R x y ∧ R y z ⟶ R x z"
moreover have "R x y ∧ R y x ⟶ R x x ⟹ False"
proof -
assume "R x y ∧ R y x ⟶ R x x"
moreover {
note `R x y`
moreover note `R y x`
ultimately have "R x y ∧ R y x" by (rule conjI)
}
ultimately have "R x x" by (rule mp)
note `∀x. ¬(R x x)`
moreover {
assume "¬(R x x)"
moreover note `R x x`
ultimately have "False" by (rule notE)
}
ultimately show "False" by (rule allE)
qed
ultimately show "False" by (rule allE)
qed
ultimately show "False" by (rule allE)
qed
ultimately show "False" by (rule allE)
qed
}
hence "R x y ⟶ ¬ (R y x)" by (rule impI)
}
hence "⋀x. ∀y. R x y ⟶ ¬ (R y x)" by (rule allI)
thus ?thesis by (rule allI)
qed
(* alfmarcua marfruman1 enrparalv*)
lemma ejercicio_2:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof (rule allI)
fix a
show "∀y. R a y ⟶ ¬ R y a"
proof (rule allI, rule impI)
fix b
assume "R a b"
show "¬ R b a"
proof (rule notI)
assume "R b a"
have "R a b ∧ R b a" using `R a b` `R b a` by (rule conjI)
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
then have "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
then have "R a b ∧ R b a ⟶ R a a" by (rule allE)
then have "R a a" using `R a b ∧ R b a` by (rule mp)
have "¬ (R a a)" using assms(2) by (rule allE)
then show False using `R a a` by (rule notE)
qed
qed
qed
(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan
pabbergue giafus1 antramhur *)
lemma ejercicio_2b:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof (rule allI)
fix a
show "∀y. R a y ⟶ ¬(R y a)"
proof (rule allI)
fix b
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
hence 1: "R a b ∧ R b a ⟶ R a a" by (rule allE)
have 2: "¬(R a a)" using assms(2) by (rule allE)
show "R a b ⟶ ¬(R b a)" proof (rule impI)
assume 3: "R a b"
show "¬(R b a)"
proof (rule ccontr)
assume "¬¬R b a"
hence 4: "R b a" by (rule notnotD)
have 5: "R a b ∧ R b a" using 3 4 by (rule conjI)
have 6: "R a a" using 1 5 by (rule mp)
show False using 2 6 by (rule notE)
qed
qed
qed
qed
(* pabalagon *)
lemma ejercicio_2_2:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof -
{ fix a
{ fix b
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
hence "∀z. R a b ∧ R b z ⟶ R a z" by (rule allE)
hence 1: "R a b ∧ R b a ⟶ R a a" by (rule allE)
have 2: "¬(R a a)" using assms(2) by (rule allE)
have "R a b ⟶ ¬(R b a)" proof (rule impI)
assume 3: "R a b"
show "¬(R b a)"
proof (rule ccontr)
assume "¬¬R b a"
hence 4: "R b a" by (rule notnotD)
have 5: "R a b ∧ R b a" using 3 4 by (rule conjI)
have 6: "R a a" using 1 5 by (rule mp)
show False using 2 6 by (rule notE)
qed
qed}
hence "∀y. R a y ⟶ ¬(R y a)" by (rule allI)}
thus "∀x y. R x y ⟶ ¬(R y x)" by (rule allI)
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar o refutar
(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
------------------------------------------------------------------ *}
(* benber pabbergue*)
(* No es cierto si el universo consiste en más que un objeto. En ese
caso, asignar la igualdad (=) a P es un contraejemplo. *)
(* alfmarcua marfruman1 raffergon2 enrparalv*)
lemma ejercicio_3:
"(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
quickcheck
oops
(* pabalagon manperjim pabbergue josgomrom4 gleherlop hugrubsan giafus1
antramhur *)
text{*
Contraejemplo en los naturales, para todo x existe y tal que x < y, pero no
existe y tal que para todo x, x < y
*}
lemma ejercicio_3: "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
quickcheck
oops
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar o refutar
(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)
------------------------------------------------------------------ *}
(* benber *)
lemma "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
proof
assume "∃y. ∀x. P x y"
moreover have "⋀y. ∀x. P x y ⟹ ∀x. ∃y'. P x y'"
proof
fix x y
assume "∀x'. P x' y"
hence "P x y" by (rule allE)
thus "∃y'. P x y'" by (rule exI)
qed
ultimately show "∀x. ∃y. P x y" by (rule exE)
qed
(* alfmarcua marfruman1 raffergon2 enrparalv *)
lemma ejercicio_4:
"(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
proof (rule impI, rule allI)
fix a
assume "∃y. ∀x. P x y"
then obtain b where "∀x. P x b" by (rule exE)
then have "P a b" by (rule allE)
then show "∃y. P a y" by (rule exI)
qed
(* pabalagon manperjim josgomrom4 gleherlop hugrubsan pabbergue
antramhur *)
lemma ejercicio_4_2: "(∃y. ∀x. P x y) ⟶ (∀x. ∃y. P x y)"
proof (rule impI)
assume "∃y. ∀x. P x y"
moreover have "⋀y. ∀x. P x y ⟹ ∀x. ∃y. P x y"
proof
fix x0 y0
assume "∀x. P x y0"
hence "P x0 y0" by (rule allE)
thus "∃y. P x0 y" by (rule exI)
qed
ultimately show "∀x. ∃y. P x y" by (rule exE)
qed
text {* ---------------------------------------------------------------
Ejercicio 5. 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))
------------------------------------------------------------------ *}
(* benber *)
lemma
assumes A1: "∀ x. P a x x"
and A2: "∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
proof
from A2
have "∀y z. P a y z ⟶ P (f a) y (f z)" by (rule allE)
hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
moreover have "P a (f a) (f a)" using A1 by (rule allE)
ultimately show "P (f a) (f a) (f (f a))" by (rule mp)
qed
(* alfmarcua enrparalv *)
lemma ejercicio_5:
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))"
proof (rule exI, rule mp)
show "P a (f a) (f a)" using assms(1) by (rule allE)
next
have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
then have "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" by (rule allE)
then show "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" by (rule allE)
qed
(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2
hugrubsan pabbergue giafus1 antramhur *)
lemma ejercicio_5_2:
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))"
proof (rule exI)
have "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) ..
hence "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" ..
hence "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" ..
moreover have "P a (f a) (f a)" using assms(1) by (rule allE)
ultimately show "P (f a) (f a) (f (f a))" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 6. 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))
------------------------------------------------------------------ *}
(* benber alfmarcua giafus1 *)
lemma
assumes "∀y. Q a y"
and "∀x y. Q x y ⟶ Q (s x) (s y)"
shows "∃z. Q a z ∧ Q z (s (s a))"
proof
have "Q a a" using `∀y. Q a y` by (rule allE)
moreover have "Q a (s (s a))" using `∀y. Q a y` by (rule allE)
ultimately show "Q a a ∧ Q a (s (s a))" by (rule conjI)
qed
(* pabalagon manperjim josgomrom4 gleherlop marfruman1 raffergon2
hugrubsan pabbergue enrparalv antramhur *)
lemma ejercicio_6:
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))"
proof (rule exI)
have "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) by (rule allE)
hence "Q a (s a) ⟶ Q (s a) (s (s a))" by (rule allE)
moreover have "Q a (s a)" using assms(1) by (rule allE)
ultimately have "Q (s a) (s (s a))" by (rule mp)
with `Q a (s a)` show "Q a (s a) ∧ Q (s a) (s (s a))" by (rule conjI)
qed
text {* ---------------------------------------------------------------
Ejercicio 7. (En APLI2 el ejercicio 13 de LP) Formalizar, y demostrar
la corrección, del siguiente argumento
Si la válvula está abierta o la monitorización está preparada,
entonces se envía una señal de reconocimiento y un mensaje de
funcionamiento al controlador del ordenador. Si se envía un mensaje
de funcionamiento al controlador del ordenador o el sistema está en
estado normal, entonces se aceptan las órdenes del operador. Por lo
tanto, si la válvula está abierta, entonces se aceptan las órdenes
del operador.
Usar A : La válvula está abierta.
P : La monitorización está preparada.
R : Envía una señal de reconocimiento.
F : Envía un mensaje de funcionamiento.
N : El sistema está en estado normal.
Or : Se aceptan órdenes del operador.
------------------------------------------------------------------ *}
(* benber manperjim alfmarcua pabalagon marfruman1 josgomrom4 gleherlop
raffergon2 hugrubsan pabbergue enrparalv giafus1 antramhur *)
lemma
assumes "A ∨ P ⟶ R ∧ F"
and "F ∨ N ⟶ Or"
shows "A ⟶ Or"
proof
assume "A"
hence "A ∨ P" by (rule disjI1)
with `A ∨ P ⟶ R ∧ F` have "R ∧ F" by (rule mp)
hence "F" by (rule conjunct2)
hence "F ∨ N" by (rule disjI1)
with `F ∨ N ⟶ Or` show "Or" by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 8. (En APLI2 el ejercicio 5 de LP) Formalizar, y demostrar
la corrección, del siguiente argumento
En cierto experimento, cuando hemos empleado un fármaco A, el
paciente ha mejorado considerablemente en el caso, y sólo en el
caso, en que no se haya empleado también un fármaco B. Además, o se
ha empleado el fármaco A o se ha empleado el fármaco B. En
consecuencia, podemos afirmar que si no hemos empleado el fármaco
B, el paciente ha mejorado considerablemente.
Usar A: Hemos empleado el fármaco A.
B: Hemos empleado el fármaco B.
M: El paciente ha mejorado notablemente.
------------------------------------------------------------------ *}
(* benber *)
lemma
assumes "A ⟶ (M ⟷ ¬B)"
and "A ∨ B"
shows "¬B ⟶ M"
proof
assume "¬B"
note `A ∨ B`
moreover {
assume "A"
with `A ⟶ (M ⟷ ¬B)` have "M ⟷ ¬B" by (rule mp)
hence "¬B ⟹ M" by (rule iffD2)
hence "M" using `¬B` .
}
moreover {
note `¬B`
moreover assume "B"
ultimately have "M" by (rule notE)
}
ultimately show "M" by (rule disjE)
qed
(* alfmarcua marfruman1 *)
lemma ejercicio_8:
assumes "A ∧ ¬ B ⟶ M"
"A ∨ B"
shows "¬ B ⟶ M"
proof (rule impI)
assume "¬B"
show "M" using assms(2)
proof (rule disjE)
assume "A"
then have "A ∧ ¬ B" using `¬ B` by (rule conjI)
show "M" using assms(1) `A ∧ ¬ B` by (rule mp)
next
assume "B"
show "M" using `¬ B` `B` by (rule notE)
qed
qed
(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan
pabbergue enrparalv giafus1 antramhur *)
lemma ejercicio_8_2:
assumes "A ⟶ (M ⟷ ¬B)"
"A ∨ B"
shows "¬B ⟶ M"
using assms(2) proof (rule disjE)
assume 1: A
have 2: "M ⟷ ¬B" using assms(1) 1 by (rule mp)
show "¬B ⟶ M" proof (rule impI)
assume 3: "¬B" show M using 2 3 by (rule iffD2)
qed
next
assume 4: B
show ?thesis proof (rule impI)
assume "¬B" thus M using 4 by (rule notE)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 9. (En APLI2 el ejercicio 13 de LPO) 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
------------------------------------------------------------------ *}
(* benber *)
lemma
assumes "∀x. ¬ R x ⟶ R (p x)"
shows "∃x. R x ∧ R (p (p x))"
proof -
have 0: "p ∨ ¬ p" for p
proof (rule ccontr)
assume "¬ (p ∨ ¬ p)"
moreover {
have "p"
proof (rule ccontr)
assume "¬ p"
hence "p ∨ ¬ p" by (rule disjI2)
with `¬ (p ∨ ¬ p)` show "False" by (rule notE)
qed
hence "p ∨ ¬ p" by (rule disjI1)
}
ultimately show "False" by (rule notE)
qed
have "¬ R x ⟶ R (p x)" for x using assms(1) by (rule allE)
hence 1: "¬ R x ⟹ R (p x)" for x by (rule mp)
have 2: "⟦R y; ¬ R (p y)⟧ ⟹ ?thesis" for y
proof
assume "R y"
assume "¬ R (p y)"
hence "R (p (p y))" by (rule 1)
with `R y` show "R y ∧ R (p (p y))" by (rule conjI)
qed
have 3: "R y ⟹ ?thesis" for y
proof -
assume "R y"
have "R (p y) ∨ ¬ R (p y)" by (rule 0)
moreover {
assume "R (p y)"
have "R (p (p y)) ∨ ¬ R (p (p y))" by (rule 0)
moreover {
assume "R (p (p y))"
with `R y` have "R y ∧ R (p (p y))" by (rule conjI)
hence ?thesis by (rule exI)
}
moreover {
assume "¬ R (p (p y))"
with `R (p y)` have ?thesis by (rule 2)
}
ultimately have ?thesis by (rule disjE)
}
moreover {
assume "¬ R (p y)"
with `R y` have ?thesis by (rule 2)
}
ultimately show ?thesis by (rule disjE)
qed
fix y
have "R y ∨ ¬ R y" by (rule 0)
moreover {
assume "R y"
hence ?thesis by (rule 3)
}
moreover {
assume "¬ R y"
hence "R (p y)" by (rule 1)
hence ?thesis by (rule 3)
}
ultimately show ?thesis by (rule disjE)
qed
(* alfmarcua *)
lemma ejercicio_9_2:
assumes "∀ x. ¬ R x ⟶ R (p x)"
shows "∃x. R x ∧ R (p (p x))"
proof (rule disjE, rule ejercicio_52)
have prelemma:"(∃y. ¬ R (p y)) ⟶ ?thesis"
proof (rule impI)
assume "∃y. ¬ R (p y)"
then obtain b where "¬ R (p b)" by (rule exE)
have "¬ R (p b) ⟶ R (p (p b))" using assms by (rule allE)
then have "R (p (p b))" using `¬ R (p b)` by (rule mp)
have "¬ R b ⟶ R (p b)" using assms by (rule allE)
then have "¬¬ R b" using `¬ R (p b)` by (rule mt)
then have "R b" by (rule notnotD)
then have "R b ∧ R (p (p b))" using `R (p (p b))` by (rule conjI)
then show "∃x. R x ∧ R (p (p x))" by (rule exI)
qed
fix a
show "R (p a) ⟹ ?thesis"
proof (rule disjE, rule ejercicio_52)
assume "R (p a)"
show "R (p (p a)) ⟹ ?thesis"
proof (rule disjE, rule ejercicio_52)
assume "R (p (p (p a)))"
have "R (p a) ∧ R (p (p (p a)))" using `R (p a)` `R (p (p (p a)))` by (rule conjI)
then show ?thesis by (rule exI)
next
assume "¬ R (p (p (p a)))"
then have "∃y. ¬ R (p y)" by (rule exI)
show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
qed
next
assume "¬ R (p (p a))"
then have "∃y. ¬ R (p y)" by (rule exI)
show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
qed
assume "¬ R (p a)"
then have "∃y. ¬ R (p y)" by (rule exI)
show ?thesis using prelemma `∃y. ¬ R (p y)` by (rule mp)
qed
(* pabalagon manperjim marfruman1 josgomrom4 gleherlop raffergon2
hugrubsan pabbergue enrparalv giafus1 antramhur *)
lemma ejercicio_9_3:
assumes "∀x. ¬R x ⟶ R (p x)"
shows "∃x. R x ∧ R (p (p x))"
proof -
fix y
have s1: "⟦¬R (p y)⟧ ⟹ ?thesis" for y proof (rule exI)
assume 2: "¬R (p y)"
have "¬R (p y) ⟶ R (p (p y))" using assms(1) by (rule allE)
hence 3: "R (p (p y))" using 2 by (rule mp)
have "¬R y ⟶ R (p y)" using assms(1) by (rule allE)
hence "¬¬R y" using 2 by (rule mt)
hence "R y" by (rule notnotD)
thus "R y ∧ R (p (p y))" using 3 by (rule conjI)
qed
have s2: "R y ⟹ ?thesis" for y proof -
assume 2: "R y"
have "¬R (p y) ∨ R (p y)" by (rule excluded_middle)
thus ?thesis proof (rule disjE)
assume 3: "¬R (p y)" thus ?thesis by (rule s1)
next
assume 4: "R (p y)"
have "¬R (p (p y)) ∨ R (p (p y))" by (rule excluded_middle)
thus ?thesis proof (rule disjE)
assume "¬R (p (p y))" thus ?thesis by (rule s1)
next
assume "R (p (p y))"
with `R y` have "R y ∧ R (p (p y))" by (rule conjI)
thus ?thesis by (rule exI)
qed
qed
qed
have "¬R y ∨ R y" by (rule excluded_middle)
thus ?thesis proof (rule disjE)
assume 2: "R y" thus ?thesis by (rule s2)
next
assume 4: "¬R y"
have "¬R y ⟶ R (p y)" using assms(1) by (rule allE)
hence "R (p y)" using 4 by (rule mp)
thus ?thesis by (rule s2)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 10. (En APLI2 el ejercicio 10 de LPO) 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
------------------------------------------------------------------ *}
(* benber *)
lemma
assumes "∀x. Af x ⟶ (∀y. E y ⟶ Ap x y)"
and "∀x. E x ⟶ ¬ Ap j x"
shows "(∃x. E x ∧ N x) ⟶ ¬ Af j"
proof
assume "∃x. E x ∧ N x"
show "¬ Af j"
proof (rule ccontr)
assume "¬ ¬ Af j"
hence "Af j" by (rule notnotD)
note `∀x. Af x ⟶ (∀y. E y ⟶ Ap x y)`
hence "Af j ⟶ (∀x. E x ⟶ Ap j x)" by (rule allE)
moreover note `Af j`
ultimately have "∀x. E x ⟶ Ap j x" by (rule mp)
note `∃x. E x ∧ N x`
moreover have "E x ∧ N x ⟹ False" for x
proof -
assume "E x ∧ N x"
hence "E x" by (rule conjunct1)
note `∀x. E x ⟶ Ap j x`
hence "E x ⟶ Ap j x" by (rule allE)
hence "Ap j x" using `E x` by (rule mp)
note `∀x. E x ⟶ ¬ Ap j x`
hence "E x ⟶ ¬ Ap j x" by (rule allE)
hence "¬ Ap j x" using `E x` by (rule mp)
thus "False" using `Ap j x` by (rule notE)
qed
ultimately show "False" by (rule exE)
qed
qed
(* alfmarcua marfruman1 *)
lemma ejercicio_10_2:
assumes "∀x y. Af x ∧ E y ⟶ Ap x y"
"∀y. E y ⟶ ¬ Ap j y"
shows "(∃y. E y ∧ N y) ⟶ ¬ Af j"
proof (rule impI)
assume "∃x. E x ∧ N x"
then obtain a where "E a ∧ N a" by (rule exE)
then have "E a" by (rule conjunct1)
show "¬ Af j"
proof (rule notI, rule notE)
assume "Af j"
then show "Af j ∧ E a" using `E a` by (rule conjI)
next
have "E a ⟶ ¬ Ap j a" using assms(2) by (rule allE)
then have "¬ Ap j a" using `E a` by (rule mp)
have "∀y. Af j ∧ E y ⟶ Ap j y" using assms(1) by (rule allE)
then have "Af j ∧ E a ⟶ Ap j a" by (rule allE)
then show "¬ (Af j ∧ E a)" using `¬ Ap j a` by (rule mt)
qed
qed
(* pabalagon manperjim josgomrom4 gleherlop raffergon2 hugrubsan
pabbergue enrparalv giafus1 antramhur *)
lemma ejercicio_10_3:
assumes "∀x y. Af x ∧ E y ⟶ Ap x y"
"∀x y. x = j ∧ E y ⟶ ¬(Ap x y)"
shows "(∃ x. (E x ∧ N x)) ⟶ ¬(Af j)"
proof (rule impI)
assume 1: "∃x. E x ∧ N x"
show "¬(Af j)" proof (rule ccontr)
fix a
assume "¬¬Af j" hence 2: "Af j" by (rule notnotD)
obtain a where 3: "E a ∧ N a" using 1 by (rule exE)
hence 4: "E a" by (rule conjunct1)
have 5: "N a" using 3 by (rule conjunct2)
have "∀y. Af j ∧ E y ⟶ Ap j y" using assms(1) by (rule allE)
hence 6: "Af j ∧ E a ⟶ Ap j a" by (rule allE)
have 7: "Af j ∧ E a" using 2 4 by (rule conjI)
have 8: "Ap j a" using 6 7 by (rule mp)
have "∀y. j = j ∧ E y ⟶ ¬(Ap j y)" using assms(2) by (rule allE)
hence 9: "j = j ∧ E a ⟶ ¬(Ap j a)" by (rule allE)
have "j = j" by (rule refl)
hence 10: "j = j ∧ E a" using 4 by (rule conjI)
have "¬(Ap j a)" using 9 10 by (rule mp)
thus False using 8 by (rule notE)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 11. 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
------------------------------------------------------------------ *}
(* benber *)
lemma
assumes A1: "∀x. P x ⟶ R x"
and A2: "∀x. P x ⟶ (¬(Q x) ⟶ R x)"
and "¬(R a)"
shows "P a ⟶ Q a"
proof
have "P a ⟶ (¬(Q a) ⟶ R a)" using A2 by (rule allE)
moreover assume "P a"
ultimately have "¬(Q a) ⟶ R a" by (rule mp)
show "Q a"
proof (rule ccontr)
assume "¬(Q a)"
with `¬(Q a) ⟶ R a` have "R a" by (rule mp)
with `¬(R a)` show "False" by (rule notE)
qed
qed
(* alfmarcua *)
lemma ejercicio_11:
assumes "∄x. P x ∧ R x"
"∀x. P x ∧ (¬ Q x) ⟶ R x"
shows "P a ⟶ Q a"
proof (rule impI, rule ccontr)
assume "P a" "¬ Q a"
then have "P a ∧ (¬ Q a)" by (rule conjI)
have "P a ∧ (¬ Q a) ⟶ R a" using assms(2) by (rule allE)
then have "R a" using `P a ∧ (¬ Q a)` by (rule mp)
have "P a ∧ R a" using `P a` `R a` by (rule conjI)
then have "∃x. P x ∧ R x" by (rule exI)
show False using assms(1) `∃x. P x ∧ R x` by (rule notE)
qed
(* pabalagon manperjim marfruman1 josgomrom4 gleherlop hugrubsan
pabbergue enrparalv giafus1 antramhur *)
lemma ejercicio_11_2:
assumes "¬(∃x. P x ∧ R x)"
"∀x. P x ∧ ¬Q x ⟶ R x"
shows "P a ⟶ Q a"
proof (rule impI)
assume 1: "P a"
show "Q a" proof (rule ccontr)
assume 2: "¬Q a"
have 3: "P a ∧ ¬Q a" using 1 2 by (rule conjI)
have 4: "P a ∧ ¬ Q a ⟶R a" using assms(2) by (rule allE)
hence 5: "R a" using 3 by (rule mp)
have 6: "P a ∧ R a" using 1 5 by (rule conjI)
hence 7: "∃x. P x ∧ R x" by (rule exI)
show False using assms(1) 7 by (rule notE)
qed
qed
end
