Lógica Matemática y fundamentos (2015-16) - Contribuciones del usuario [es]

Relación 5

2018-07-16T12:41:08Z

WikiSysop: Texto reemplazado: «Isar» por «isabelle»

<source lang = "isabelle">
header {* R5: Argumentación en lógica de primer orden *}

theory R5
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar en lógica de primer orden
argumentos expresados en lenguaje natural.

Antes de escribir la soluciones, comprobar con APLI2 la corrección de la
formalización.

Una vez formalizadas, probar que el razonamiento es correcto, o refutarlo
mediante un contraejemplo.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar el 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
------------------------------------------------------------------ *}

lemma ejercicio1
assumes "(∃x. I(x)) ∧ (∃x. T(x))"
shows "∃x. I(x) ∧ T(x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar el 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
------------------------------------------------------------------ *}
lemma ejercicio2:
assumes 1: "∀x. (P(x)⟶V(x))" and
2: "(¬(∃x. V(x))) ∨ (∃x. (V(x) ∧ (∀y. (V(y) ⟶ x=y))))" and
3: "(¬(∃x. P(x))) ∨ (∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y))))"
shows "∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y)))"
quickcheck
oops
text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar el 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
------------------------------------------------------------------ *}
lemma ejercicio_3:
assumes "∀x. (A x ∧ G x ⟶ V x ∧ L x)"
"∃x. (A x ∧ V x ∧ ¬L x)"
shows "∃x. (A x ∧ ¬G x)"
proof-
obtain b where 1 : "A b ∧ V b ∧ ¬L b" using assms(2) by (rule exE)
have 2 : "A b ∧ G b ⟶ V b ∧ L b" using assms(1) by (rule allE)
{assume 3 : "G b"
have 4 : "A b" using 1 by (rule conjunct1)
have 5 : "A b ∧ G b" using 4 3 by (rule conjI)
have 6 : "V b ∧ L b" using 2 5 by (rule mp)
have 7 : "L b" using 6 by (rule conjunct2)
have 8 : "V b ∧ ¬L b" using 1 by (rule conjunct2)
have 9 : "¬L b" using 8 by (rule conjunct2)
have "False" using 9 7 by (rule notE)}
hence 10 : "¬G b" by (rule notI)
have 11 : "A b" using 1 by (rule conjunct1)
have 12 : "A b ∧ ¬G b" using 11 10 by (rule conjI)
show "∃x. (A x ∧ ¬G x)" using 12 by (rule exI)
qed

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar el 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
------------------------------------------------------------------ *}
lemma ejercicio_4:
assumes "∀x y. (R x ∧ A y ⟶ Ob x y)"
"A a"
"¬Ob b a"
shows "¬R b"
proof-
{assume 1 : "R b"
have 2 : "∀y. R b ∧ A y ⟶ Ob b y" using assms(1) by (rule allE)
have 3 : "R b ∧ A a ⟶ Ob b a" using 2 by (rule allE)
have 4 : "R b ∧ A a" using 1 assms(2) by (rule conjI)
have 5 : "Ob b a" using 3 4 by (rule mp)
have "False" using assms(3) 5 by (rule notE)}
thus "¬R b" by (rule notI)
qed

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar el 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
------------------------------------------------------------------ *}
lemma ejercicio_5:
assumes "¬(∃x. P x ∧ R x)"
"∀x. (P x ∧ ¬Q x ⟶ R x)"
shows "P a ⟶ Q a"
proof-
{assume 1 : "P a"
{assume 2 : "¬Q a"
have 3 : "P a ∧ ¬Q a ⟶ R a" using assms(2) by (rule allE)
have 4 : "P a ∧ ¬Q a" using 1 2 by (rule conjI)
have 5 : "R a" using 3 4 by (rule mp)
have 6 : "P a ∧ R a" using 1 5 by (rule conjI)
have 7 : "∃x. P x ∧ R x" using 6 by (rule exI)
have "False" using assms(1) 7 by (rule notE)}
hence "Q a" by (rule ccontr)}
thus "P a ⟶ Q a" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar el 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
------------------------------------------------------------------ *}
lemma ejercicio6
assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
"∀x. E(x) ⟶ ¬Ap(j,x)"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
oops

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar el 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
------------------------------------------------------------------ *}
lemma ejercicio7:
assumes 1: "∀x. ((E(x) ∧ ¬V(x)) ⟶ (∃y. (A(y) ∧ Ca(y,x))))" and
2: "∃x. ((Co(x) ∧ E(x)) ∧ (∀y. (Ca(y,x) ⟶ Co(y))))" and
3: "∀x. (Co(x)⟶ ¬V(x))"
shows "∃x. (A(x) ∧ Co(x))"
proof -
obtain a where 4: "(Co(a) ∧ E(a)) ∧ (∀y. (Ca(y,a)⟶Co(y)))" using 2 by (rule exE)
have 5: "Co(a) ∧ E(a)" using 4 by (rule conjunct1)
have 6: "Co(a)" using 5 by (rule conjunct1)
have 7: "E(a)" using 5 by (rule conjunct2)
have 8: "∀y. (Ca(y,a)⟶Co(y))" using 4 by (rule conjunct2)
have 9: "Co(a) ⟶ ¬V(a)" using 3 by (rule allE)
have 10: "¬V(a)" using 9 6 by (rule mp)
have 11: "(E(a)∧ ¬V(a)) ⟶ (∃y. (A(y) ∧ Ca(y,a)))" using 1 by (rule allE)
have 12: "E(a) ∧ ¬V(a)" using 7 10 by (rule conjI)
have 13: "∃y. (A(y) ∧ Ca(y,a))" using 11 12 by (rule mp)
obtain b where 14: "A(b) ∧ Ca(b,a)" using 13 by (rule exE)
have 15: "A(b)" using 14 by (rule conjunct1)
have 16: "Ca(b,a)⟶Co(b)" using 8 by (rule allE)
have 17: "Ca(b,a)" using 14 by (rule conjunct2)
have 18: "Co(b)" using 16 17 by (rule mp)
have 19: "A(b) ∧ Co(b)" using 15 18 by (rule conjI)
show 20: "∃x. (A(x) ∧ Co(x))" using 19 by (rule exI)
qed

section {* Ejercicios con igualdad *}

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar el 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 9. Formalizar el 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 10. Formalizar el 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
------------------------------------------------------------------ *}

end
</source>

Rel 5

2018-07-16T12:41:07Z

WikiSysop: Texto reemplazado: «Isar» por «isabelle»

Relación 4

2018-07-16T12:41:07Z

WikiSysop: Texto reemplazado: «Isar» por «isabelle»

<source lang = "isabelle">
header {* R4: Deducción natural de primer orden *}

theory R4
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_middel:(¬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

· 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

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
∀x. P x ⟶ Q x ⊢ (∀x. P x) ⟶ (∀x. Q x)
------------------------------------------------------------------ *}

lemma ejercicio_1a:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof (rule impI)
assume 1: "∀x. P x"
show "∀x. Q x"
proof (rule allI)
{fix a
have 2: "P(a)" using 1 by (rule allE)
have 3: "P(a)⟶Q(a)" using assms by (rule allE)
show "Q a" using 3 2 by (rule mp)}
qed
qed

lemma ejercicio_1a:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof-
{assume 1 : "∀x. P x"
{fix a
have 2 : "P a" using 1 by (rule allE)
have 3 : "P a ⟶ Q a" using assms by (rule allE)
have 4 : "Q a" using 3 2 by (rule mp)}
hence 5 : "∀x. Q x" by (rule allI)}
thus "(∀x. P x) ⟶ (∀x. Q x)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
∃x. ¬(P x) ⊢ ¬(∀x. P x)
------------------------------------------------------------------ *}

lemma ejercicio_2a:
assumes "∃x. ¬(P x)"
shows "¬(∀x. P x)"
proof
assume "∀x. P x"
obtain a where "¬ (P a)" using assms by (rule exE)
have "P a" using `∀x. P x` by (rule allE)
show "False" using `¬ (P a)` `P a` by (rule notE)
qed

lemma ejercicio_2a:
assumes "∃x. ¬(P x)"
shows "¬(∀x. P x)"
proof-
{assume 1 : "∀x. P x"
obtain a where 2 : "¬ (P a)" using assms by (rule exE)
have 3 : "P a" using 1 by (rule allE)
have 4 : "False" using 2 3 by (rule notE)}
thus "¬(∀x. P x)" by (rule notI)
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
∀x. P x ⊢ ∀y. P y
------------------------------------------------------------------ *}

lemma ejercicio_3a:
assumes "∀x. P x"
shows "∀y. P y"
proof
{ fix a
show "P a" using assms by (rule allE)}
qed

lemma ejercicio_3a:
assumes "∀x. P x"
shows "∀y. P y"
proof-
{fix a
have 1 : "P a" using assms by (rule allE)}
thus "∀y. P y" by (rule allI)
qed

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
∀x. P x ⟶ Q x ⊢ (∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))
------------------------------------------------------------------ *}

lemma ejercicio_4:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof
assume "∀x. ¬(Q x)"
{ fix a
have "P a ⟶ Q a" using assms by (rule allE)
have "¬ (Q a)" using `∀x. ¬(Q x)` by (rule allE)
have "¬(P a)" using `P a ⟶ Q a` `¬ (Q a)` by (rule mt)}
thus "∀x. ¬ (P x)" by (rule allI)
qed

lemma ejercicio_4:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof-
{assume 1 : "∀x. ¬(Q x)"
{fix a
have 2 : "P a ⟶ Q a" using assms by (rule allE)
have 3 : "¬(Q a)" using 1 by (rule allE)
have 4 : "¬(P a)" using 2 3 by (rule mt)}
hence "∀x. ¬ (P x)" by (rule allI)}
thus "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))" by (rule impI)
qed

--*
proof(rule impI)
assume 1: "∀x. ¬(Q x)"
show "∀x. ¬(P x)"
proof-
{fix a
have 2: "P a ⟶ Q a" using assms by ( rule allE)
have 3: " ¬( Q a)" using 1 by ( rule allE)
have 4: " ¬( P a)" using 2 3 by ( rule mt)}
thus "∀x. ¬(P x)" by ( rule allI)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
∀x. P x ⟶ ¬(Q x) ⊢ ¬(∃x. P x ∧ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_5:
assumes "∀x. P x ⟶ ¬(Q x)"
shows "¬(∃x. P x ∧ Q x)"
proof
assume "∃x. P x ∧ Q x"
obtain a where "P a ∧ Q a" using `∃x. P x ∧ Q x` by (rule exE)
have "P a" using `P a ∧ Q a` by (rule conjE)
have "Q a" using `P a ∧ Q a` by (rule conjE)
have "P a ⟶ ¬(Q a)" using assms by (rule allE)
have "¬(Q a)" using `P a ⟶ ¬(Q a)` `P a` by (rule mp)
show "False" using `¬(Q a)` `Q a` by (rule notE)
qed

lemma ejercicio_5:
assumes "∀x. P x ⟶ ¬(Q x)"
shows "¬(∃x. P x ∧ Q x)"
proof-
{assume 1 : "∃x. P x ∧ Q x"
obtain a where 2 : "P a ∧ Q a" using 1 by (rule exE)
have 3 : "P a ⟶ ¬(Q a)" using assms by (rule allE)
have 4 : "P a" using 2 by (rule conjunct1)
have 5 : "Q a" using 2 by (rule conjunct2)
have 6 : "¬(Q a)" using 3 4 by (rule mp)
have 7 : "False" using 6 5 by (rule notE)}
thus "¬(∃x. P x ∧ Q x)" by (rule notI)
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
∀x y. P x y ⊢ ∀u v. P u v
------------------------------------------------------------------ *}

lemma ejercicio_6:
assumes "∀x y. P x y"
shows "∀u v. P u v"
proof (rule allI)+
fix a b
have "∀y. P a y" using assms by (rule allE)
thus " P a b" by (rule allE)
qed

lemma ejercicio_6:
assumes "∀x y. P x y"
shows "∀u v. P u v"
proof-
{fix a
{fix b
have 1 : " ∀y. P a y" using assms by (rule allE)
have 2 : "P a b" using 1 by (rule allE)}
hence "∀v. P a v" by (rule allI)}
thus "∀u v. P u v" by (rule allI)
qed

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
∃x y. P x y ⟹ ∃u v. P u v
------------------------------------------------------------------ *}

lemma ejercicio_7:
assumes "∃x y. P x y"
shows "∃u v. P u v"
proof -
obtain a where "∃y. P a y" using assms by (rule exE)
then obtain b where "P a b" by (rule exE)
hence "∃v. P a v" by (rule exI)
thus "∃u v. P u v" by (rule exI)
qed

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
∃x. ∀y. P x y ⊢ ∀y. ∃x. P x y
------------------------------------------------------------------ *}

lemma ejercicio_8:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
proof
obtain a where "∀y. P a y" using assms by (rule exE)
fix b
have "P a b" using `∀y. P a y` by (rule allE)
thus "∃x. P x b" by (rule exI)
qed

lemma ejercicio_8:
assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
proof-
obtain a where 1 : "∀y. P a y" using assms by (rule exE)
{fix b
have 2 : "P a b" using 1 by (rule allE)
have 3 : "∃x. P x b" using 2 by (rule exI)}
thus "∀y. ∃x. P x y" by (rule allI)
qed

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
∃x. P a ⟶ Q x ⊢ P a ⟶ (∃x. Q x)
------------------------------------------------------------------ *}

lemma ejercicio_9:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
proof
assume "P a"
obtain b where "P a ⟶ Q b" using assms by (rule exE)
have "Q b" using `P a ⟶ Q b` `P a` by (rule mp)
thus "∃x. Q x" by (rule exI)
qed

lemma ejercicio_9:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"
proof-
{assume 1 : "P a"
obtain b where 2 : "P a ⟶ Q b" using assms by (rule exE)
have 3 : "Q b" using 2 1 by (rule mp)
have 4 : "∃x. Q x" using 3 by (rule exI)}
thus "P a ⟶ (∃x. Q x)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
P a ⟶ (∃x. Q x) ⊢ ∃x. P a ⟶ Q x
------------------------------------------------------------------ *}

lemma ejercicio_10a:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof-
have 1 : "¬(P a) ∨ P a" by (rule excluded_middle)
moreover
{assume 2 : "¬(P a)"
{assume 3 : "P a"
have 4 : "Q b" using 2 3 by (rule notE)}
hence 5 : "P a ⟶ Q b" by (rule impI)
have 6 : "∃x. P a ⟶ Q x" using 5 by (rule exI)}
moreover
{assume 7 : "P a"
have 8 : "∃x. Q x" using assms 7 by (rule mp)
obtain b where 9 : "Q b" using 8 by (rule exE)
{assume 10 : "P a"
have 11 : "Q b" using 9 by this}
hence 12 : "P a ⟶ Q b" by (rule impI)
have 13 : "∃x. P a ⟶ Q x" using 12 by (rule exI)}
ultimately show "∃x. P a ⟶ Q x" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
(∃x. P x) ⟶ Q a ⊢ ∀x. P x ⟶ Q a
------------------------------------------------------------------ *}

lemma ejercicio_11a:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
proof
fix b
show "P b ⟶ Q a"
proof
assume "P b"
hence "∃x. P x" by (rule exI)
show "Q a" using assms `∃x. P x` by (rule mp)
qed
qed

lemma ejercicio_11a:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
proof-
{fix b
{assume 1 : "P b"
have 2 : "∃x. P x" using 1 by (rule exI)
have 3 : "Q a" using assms 2 by (rule mp)}
hence "P b ⟶ Q a" by (rule impI) }
thus "∀x. P x ⟶ Q a" by (rule allI)
qed

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
∀x. P x ⟶ Q a ⊢ ∃ x. P x ⟶ Q a
------------------------------------------------------------------ *}

lemma ejercicio_12a:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
proof -
fix b
have "P b ⟶ Q a" using assms by (rule allE)
thus "∃x. P x ⟶ Q a" by (rule exI)
qed

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
(∀x. P x) ∨ (∀x. Q x) ⊢ ∀x. P x ∨ Q x
------------------------------------------------------------------ *}

lemma ejercicio_13a:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
proof
fix a
show "P a ∨ Q a" using assms
proof
assume "∀x. P x"
hence "P a" by (rule allE)
thus "P a ∨ Q a" by (rule disjI1)
next
assume "∀x. Q x"
hence "Q a" by (rule allE)
thus "P a ∨ Q a" by (rule disjI2)
qed
qed

lemma ejercicio_13a:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"
proof-
have "(∀x. P x) ∨ (∀x. Q x)" using assms by this
moreover
{assume 1 : "∀x. P x"
{fix a
have 2 :"P a" using 1 by (rule allE)
have 3 : "P a ∨ Q a" using 2 by (rule disjI1)}
hence "∀x. P x ∨ Q x" by (rule allI)}
moreover
{assume 4 : "∀x. Q x"
{fix a
have 5 :"Q a" using 4 by (rule allE)
have 6 : "P a ∨ Q a" using 5 by (rule disjI2)}
hence "∀x. P x ∨ Q x" by (rule allI)}
ultimately show "∀x. P x ∨ Q x" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
∃x. P x ∧ Q x ⊢ (∃x. P x) ∧ (∃x. Q x)
------------------------------------------------------------------ *}

lemma ejercicio_14a:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
proof
obtain a where "P a ∧ Q a" using assms by (rule exE)
hence "P a" by (rule conjunct1)
thus "∃x. P x" by (rule exI)
have "Q a" using `P a ∧ Q a` by (rule conjunct2)
thus "∃x. Q x" by (rule exI)
qed

lemma ejercicio_14a:
assumes "∃x. P x ∧ Q x"
shows "(∃x. P x) ∧ (∃x. Q x)"
proof-
obtain a where 1 : "P a ∧ Q a" using assms by (rule exE)
have 2 : "P a" using 1 by (rule conjunct1)
have 3 : "∃x. P x" using 2 by (rule exI)
have 4 : "Q a" using 1 by (rule conjunct2)
have 5 : "∃x. Q x" using 4 by (rule exI)
show "(∃x. P x) ∧ (∃x. Q x)" using 3 5 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
∀x y. P y ⟶ Q x ⊢ (∃y. P y) ⟶ (∀x. Q x)
------------------------------------------------------------------ *}

lemma ejercicio_15a:
assumes "∀x y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
proof
assume "∃y. P y"
then obtain b where "P b" by (rule exE)
{fix a
have "∀y. P y ⟶ Q a" using assms by (rule allE)
hence "P b ⟶ Q a" by (rule allE)
have "Q a" using `P b ⟶ Q a` `P b` by (rule mp)}
thus "∀x. Q x" by (rule allI)
qed

lemma ejercicio_15a:
assumes "∀x y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
proof-
{assume 1 : "∃y. P y"
{fix a
obtain b where 2 : "P b" using 1 by (rule exE)
have 3 : "∀y. P y ⟶ Q a" using assms by (rule allE)
have 4 : "P b ⟶ Q a" using 3 by (rule allE)
have 5 : "Q a" using 4 2 by (rule mp)}
hence "∀x. Q x" by (rule allI)}
thus "(∃y. P y) ⟶ (∀x. Q x)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
¬(∀x. ¬(P x)) ⊢ ∃x. P x
------------------------------------------------------------------ *}

lemma ejercicio_16a:
assumes "¬(∀x. ¬(P x))"
shows "∃x. P x"
proof-
fix x0
{assume 2: "¬(∃x. P x)"
{fix x1
{assume 3: "P x1"
have 4: "∃x. P x" using 3 by (rule exI)
have 5: "False" using 2 4 by (rule notE)}
then have 6: "¬ P x1" by (rule notI)}
then have 7: "∀x. ¬ P x" by (rule allI)
have 8: "False" using 1 7 by (rule notE)}
then show "∃x. P x" by (rule ccontr)
qed

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
∀x. ¬(P x) ⊢ ¬(∃x. P x)
------------------------------------------------------------------ *}

lemma ejercicio_17a:
assumes "∀x. ¬(P x)"
shows "¬(∃x. P x)"

proof
assume "∃x. P x"
then obtain a where "P a" by (rule exE)
have " ¬ (P a)" using assms by (rule allE)
show False using `¬(P a)` `P a` by (rule notE)
qed

lemma ejercicio_17a:
assumes "∀x. ¬(P x)"
shows "¬(∃x. P x)"
proof-
{assume 1 : "∃x. P x"
obtain a where 2 : "P a" using 1 by (rule exE)
have 3 : "¬(P a)" using assms by (rule allE)
have 4 : "False" using 3 2 by (rule notE)}
thus "¬(∃x. P x)" by (rule notI)
qed

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
∃x. P x ⊢ ¬(∀x. ¬(P x))
------------------------------------------------------------------ *}

lemma ejercicio_18a:
assumes "∃x. P x"
shows "¬(∀x. ¬(P x))"
proof
assume "∀x. ¬(P x)"
obtain a where "P a" using assms by (rule exE)
have "¬(P a)" using `∀x. ¬(P x)` by (rule allE)
show False using `¬(P a)` `P a`by (rule notE)
qed

lemma ejercicio_18a:
assumes "∃x. P x"
shows "¬(∀x. ¬(P x))"
proof-
{assume 1 : "∀x. ¬(P x)"
obtain a where 2 : "P a" using assms by (rule exE)
have 3 : "¬(P a)" using 1 by (rule allE)
have 4 : "False" using 3 2 by (rule notE)}
thus "¬(∀x. ¬(P x))" by (rule notI)
qed

text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
P a ⟶ (∀x. Q x) ⊢ ∀x. P a ⟶ Q x
------------------------------------------------------------------ *}

lemma ejercicio_19a:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
proof
fix b
show "P a ⟶ Q b"
proof
assume "P a"
have "∀x. Q x" using assms `P a` by (rule mp)
thus "Q b" by (rule allE)
qed
qed

lemma ejercicio_19a:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
proof-
{fix b
{assume 1 : "P a"
have 2 : "∀x. Q x" using assms 1 by (rule mp)
have 3 : "Q b" using 2 by (rule allE)}
hence 4 : "P a ⟶ Q b" by (rule impI)}
thus "∀x. P a ⟶ Q x" by (rule allI)
qed

text {* ---------------------------------------------------------------
Ejercicio 20. 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)
------------------------------------------------------------------ *}

lemma ejercicio_20a:
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 b
show "R a b ⟶ ¬(R b a )"
proof
assume 1:"R a b"
show"¬(R b a)"
proof
assume 2:"R b a"
have 3:"R a b ∧ R b a" using 1 2..
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1)..
hence "∀z. R a b ∧ R b z ⟶ R a z"..
hence 4:"R a b ∧ R b a ⟶ R a a"..
have 5:"R a a" using 4 3..
have 6:" ¬(R a a)" using assms(2)..
show False using 6 5..
qed
qed
qed

lemma ejercicio_20a:
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
{assume 1 : "R a b"
{assume 2 : "R b a"
have 3 : "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1) by (rule allE)
have 4 : "∀z. R a b ∧ R b z ⟶ R a z" using 3 by (rule allE)
have 5 : "R a b ∧ R b a ⟶ R a a" using 4 by (rule allE)
have 6 : " R a b ∧ R b a" using 1 2 by (rule conjI)
have 7 : "R a a" using 5 6 by (rule mp)
have 8 : "¬(R a a)" using assms(2) by (rule allE)
have "False" using 8 7 by (rule notE)}
hence "¬(R b a)" by (rule notI)}
hence "R a b ⟶ ¬(R b a)" by (rule impI)}
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 21. Demostrar
{∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
------------------------------------------------------------------ *}

lemma ejercicio_21a:
assumes "∀x. P x ∨ Q x"
"∃x. ¬(Q x)"
"∀x. R x ⟶ ¬(P x)"
shows "∃x. ¬(R x)"
proof-
obtain a where "¬(Q a)" using assms(2) by (rule exE)
have "P a ∨ Q a" using assms(1) by (rule allE)
show "∃x. ¬(R x)" using `P a ∨ Q a`
proof
assume "P a"
hence 1:"¬¬(P a)" by (rule notnotI)
have 2:"R a ⟶ ¬(P a)" using assms(3) by (rule allE)
have "¬(R a)" using 2 1 by (rule mt)
thus "∃x. ¬(R x)" by (rule exI)
next
assume "Q a"
have False using `¬(Q a)` `Q a` by (rule notE)
thus "∃x. ¬(R x)" by (rule ccontr)
qed
qed

lemma ejercicio_21a:
assumes "∀x. P x ∨ Q x"
"∃x. ¬(Q x)"
"∀x. R x ⟶ ¬(P x)"
shows "∃x. ¬(R x)"
proof-
obtain a where 1 : "¬Q(a)" using assms(2) by (rule exE)
have 2 : "P a ∨ Q a" using assms(1) by (rule allE)
have "P a ∨ Q a" using 2 by this
moreover
{assume 3 : "P a"
have 4 : "R a ⟶ ¬(P a)" using assms(3) by (rule allE)
have 5 : "¬¬(P a)" using 3 by (rule notnotI)
have 6 : "¬(R a)" using 4 5 by (rule mt)
have "∃x. ¬(R x)" using 6 by (rule exI)}
moreover
{assume 7 : "Q a"
have "∃x. ¬(R x)" using 1 7 by (rule notE)}
ultimately show "∃x. ¬(R x)" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
{∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
------------------------------------------------------------------ *}

lemma ejercicio_22a:
assumes "∀x. P x ⟶ Q x ∨ R x"
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
proof
fix a
show "P a ⟶ Q a"
proof
assume 1:"P a"
have 2:"P a ⟶ Q a ∨ R a" using assms(1) by (rule allE)
have 3:"Q a ∨ R a" using 2 1 by (rule mp)
show "Q a" using 3
proof
assume "Q a"
next
assume 4:"R a"
have "P a ∧ R a" using 1 4 by (rule conjI)
hence 5:"∃x. P x ∧ R x" by (rule exI)
have False using assms(2) 5 by (rule notE)
thus "Q a" by (rule ccontr)
qed
qed
qed

lemma ejercicio_22a:
assumes "∀x. P x ⟶ Q x ∨ R x"
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
proof-
{fix a
{assume 1 : "P a"
have 2 : "P a ⟶ Q a ∨ R a" using assms(1) by (rule allE)
have 3 : "Q a ∨ R a" using 2 1 by (rule mp)
moreover
{assume 4 : "Q a"
have "Q a" using 4 by this}
moreover
{assume 5 : "R a"
have 6 : "P a ∧ R a" using 1 5 by (rule conjI)
have 7 : "∃x. P x ∧ R x" using 6 by (rule exI)
have "Q a" using assms(2) 7 by (rule notE)}
ultimately have "Q a" by (rule disjE)}
hence "P a ⟶ Q a" by (rule impI)}
thus "∀x. P x ⟶ Q x" by (rule allI)
qed

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
------------------------------------------------------------------ *}

lemma ejercicio_23a:
assumes "∃x y. R x y ∨ R y x"
shows "∃x y. R x y"
proof -
obtain a where "∃y. R a y ∨ R y a " using assms by (rule exE)
then obtain b where 1:"R a b ∨ R b a" by (rule exE)
show "∃x y. R x y" using 1
proof
assume "R a b"
hence "∃y. R a y" by (rule exI)
thus "∃x y. R x y" by (rule exI)
next
assume "R b a"
hence "∃y. R b y" by (rule exI)
thus "∃x y. R x y" by (rule exI)
qed
qed

lemma ejercicio_23a:
assumes "∃x y. R x y ∨ R y x"
shows "∃x y. R x y"
proof-
obtain a where 1 : "∃y. R a y ∨ R y a" using assms by (rule exE)
obtain b where 2: "R a b ∨ R b a" using 1 by (rule exE)
moreover
{assume 3 : "R a b"
have 4 : "∃y. R a y" using 3 by (rule exI)
have 5 : "∃x y. R x y" using 4 by (rule exI)}
moreover
{assume 6 : "R b a"
have 7 : "∃y. R b y" using 6 by (rule exI)
have 8 : "∃x y. R x y" using 7 by (rule exI)}
ultimately show "∃x y. R x y" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)
------------------------------------------------------------------ *}

lemma ejercicio_24a:
"(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof-
{assume 1 : "∃x. ∀y. P x y"
obtain a where 2 : "∀y. P a y" using 1 by (rule exE)
{fix b
have 3 : "P a b" using 2 by (rule allE)
have 4 : "∃x. P x b" using 3 by (rule exI)}
hence 5 : "∀y. ∃x. P x y" by (rule allI)}
thus "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
------------------------------------------------------------------ *}

lemma ejercicio_25a:
"(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"
proof (rule iffI)
{assume 1 : "∀x. P x ⟶ Q"
{assume 2 : "∃x. P x"
obtain a where 3 : "P a" using 2 by (rule exE)
have 4 : "P a ⟶ Q" using 1 by (rule allE)
have 5 : "Q" using 4 3 by (rule mp)}
thus "(∃x. P x) ⟶ Q" by (rule impI)}
next
{assume 6 : "(∃x. P x) ⟶ Q"
{fix a
{assume 7 : "P a"
have 8 : "∃x. P x" using 7 by (rule exI)
have 9 : "Q" using 6 8 by (rule mp)}
hence "P a ⟶ Q" by (rule impI)}
thus "∀x. P x ⟶ Q" by (rule allI)}
qed

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_26a:
"((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
proof (rule iffI)
{assume 1 : "(∀x. P x) ∧ (∀x. Q x)"
{fix a
have 2 : "∀x. P x" using 1 by (rule conjunct1)
have 3 : "P a" using 2 by (rule allE)
have 4 : "∀x. Q x" using 1 by (rule conjunct2)
have 5 : "Q a" using 4 by (rule allE)
have "P a ∧ Q a" using 3 5 by (rule conjI)}
thus "∀x. P x ∧ Q x" by (rule allI)}
next
{assume 6 : "∀x. P x ∧ Q x"
{fix a
have 7 : "P a ∧ Q a" using 6 by (rule allE)
have 8 : "P a" using 7 by (rule conjunct1)}
hence 9 : "∀x. P x" by (rule allI)
{fix a
have 10 : "P a ∧ Q a" using 6 by (rule allE)
have 11 : " Q a" using 10 by (rule conjunct2)}
hence 12: "∀x. Q x" by (rule allI)
show "(∀x. P x) ∧ (∀x. Q x)" using 9 12 by (rule conjI)}
qed

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar o refutar
((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_27a:
"((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar o refutar
((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_28a:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"
proof(rule iffI)
{assume 1 : "(∃x. P x) ∨ (∃x. Q x)"
moreover
{assume 2 : "∃x. P x"
obtain a where 3 : "P a" using 2 by (rule exE)
have 4 : "P a ∨ Q a" using 3 by (rule disjI1)
have 5 : "∃x. P x ∨ Q x" using 4 by (rule exI)}
moreover
{assume 6 : "∃x. Q x"
obtain a where 7 : "Q a" using 6 by (rule exE)
have 8 : "P a ∨ Q a" using 7 by (rule disjI2)
have 9 : "∃x. P x ∨ Q x" using 8 by (rule exI)}
ultimately show "∃x. P x ∨ Q x" by (rule disjE)}
next
{assume 10 : "∃x. P x ∨ Q x"
obtain a where 11 : "P a ∨ Q a" using 10 by (rule exE)
moreover
{assume 12 : "P a"
have 13 : "∃x. P x" using 12 by (rule exI)
have "(∃x. P x) ∨ (∃x. Q x)" using 13 by (rule disjI1)}
moreover
{assume 14 : "Q a"
have 15 : "∃x. Q x" using 14 by (rule exI)
have "(∃x. P x) ∨ (∃x. Q x)" using 15 by (rule disjI2)}
ultimately show "(∃x. P x) ∨ (∃x. Q x)" by (rule disjE)}
qed

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar o refutar
(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
------------------------------------------------------------------ *}

lemma ejercicio_29:

"(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops
text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar o refutar
(¬(∀x. P x)) ⟷ (∃x. ¬P x)
------------------------------------------------------------------ *}

lemma ejercicio_30a:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof (rule iffI)
assume 1: "¬(∀x. P x)"
show "∃x. ¬P x"
proof (rule ccontr)
assume 2: "¬(∃x. ¬P x)"
show "False"
proof -
{ fix a
{ assume 3: "¬P a"
have 4: "∃x.¬ P x" using 3 by (rule exI)
have 5: "False" using 2 4 by (rule notE)}
hence 6: "P a" by (rule ccontr)}
hence 7: "∀x. P x" by (rule allI)
show 8: "False" using 1 7 by (rule notE)
qed
qed
next
assume 9: "∃x. ¬P x"
show "¬(∀x. P x)"
proof -
{assume 10: "¬¬(∀x. P x)"
have 11: "∀x. P x" using 10 by (rule notnotD)
obtain a where 12: "¬P a" using 9 by (rule exE)
have 13: "P a" using 11 by (rule allE)
have 14: "False" using 12 13 by (rule notE)}
thus 15: "¬(∀x. P x)" by (rule ccontr)
qed
qed

lemma ejercicio_30a:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof(rule iffI)
{assume 1 : "¬(∀x. P x)"
{assume 2 : "¬(∃x. ¬P x)"
{fix a
{assume 3 : "¬ P a"
have 4 :"∃x. ¬P x" using 3 by (rule exI)
have 5 : "False" using 2 4 by (rule notE)}
hence "P a" by (rule ccontr)}
hence 6 : "∀x. P x" by (rule allI)
have "False" using 1 6 by (rule notE)}
thus "∃x. ¬P x" by (rule ccontr)}
next
{assume 7 : "∃x. ¬P x"
{assume 8 : "∀x. P x"
obtain a where 9 : "¬P a" using 7 by (rule exE)
have 10 : "P a" using 8 by (rule allE)
have "False" using 9 10 by (rule notE)}
thus "¬(∀x. P x)" by (rule notI)}
qed

section {* Ejercicios sobre igualdad *}

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar o refutar
P a ⟹ ∀x. x = a ⟶ P x
------------------------------------------------------------------ *}

lemma ejercicio_31a:
assumes "P a"
shows "∀x. x = a ⟶ P x"
proof (rule allI)
fix b
show "b = a ⟶ P b"
proof (rule impI)
assume 1: "b = a"
show "P b"
proof -
have 2: "a = b" using 1 by (rule sym)
show 3: "P b" using 2 assms(1) by (rule subst)
qed
qed
qed

lemma ejercicio_31a:
assumes "P a"
shows "∀x. x = a ⟶ P x"
proof-
{fix b
{assume 1 : "b = a"
have 3 : "P b" using 1 assms by (rule ssubst)}
hence "b = a ⟶ P b" by (rule impI)}
thus "∀x. x = a ⟶ P x" by (rule allI)
qed

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar o refutar
∃x y. R x y ∨ R y x; ¬(∃x. R x x)⟧ ⟹ ∃x y. x ≠ y
------------------------------------------------------------------ *}

lemma ejercicio_32a:
fixes R :: "'c ⇒ 'c ⇒ bool"
assumes "∃x y. R x y ∨ R y x"
"¬(∃x. R x x)"
shows "∃(x::'c) y. x ≠ y"
proof-
obtain a where 1 : "∃y. R a y ∨ R y a" using assms(1) by (rule exE)
obtain b where 2 : "R a b ∨ R b a" using 1 by (rule exE)
{assume 3 : "a = b"
have "R a b ∨ R b a" using 2 by this
moreover
{assume 4 : "R a b"
have 5 : "R b b" using 3 4 by (rule subst)
have 6 : "∃x. R x x" using 5 by (rule exI)
have "False" using assms(2) 6 by (rule notE)}
moreover
{assume 7 : "R b a"
have 8 : "R b b" using 3 7 by (rule subst)
have 9 : "∃x. R x x" using 8 by (rule exI)
have "False" using assms(2) 9 by (rule notE)}
ultimately have "False" by (rule disjE)}
hence 10 : "¬(a = b)" by (rule notI)
have 11 : "∃y. ¬(a = y)" using 10 by (rule exI)
show "∃(x::'c) y. x ≠ y" using 11 by (rule exI)
qed

text {* ---------------------------------------------------------------
Ejercicio 33. 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_33a:
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)"
proof -
have 1: "P a a a" using assms(1) by (rule allE)
have 2: "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
have 3: "∀z. P a a z ⟶ P (f a) a (f z)" using 2 by (rule allE)
have 4: "P a a a ⟶ P (f a) a (f a)" using 3 by (rule allE)
show 5: "P (f a) a (f a)" using 4 1 by (rule mp)
qed
text {* ---------------------------------------------------------------
Ejercicio 34. 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_34a:
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 -
have 1: "P a (f a) (f a)" using assms(1) by (rule allE)
have 2: "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
have 3: "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" using 2 by (rule allE)
have 4: "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" using 3 by (rule allE)
have 5: "P (f a) (f a) (f (f a))" using 4 1 by (rule mp)
show 6: "∃z. P (f a) z (f (f a))" using 5 by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 35. 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_35a:
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 -
have 1: "Q a (s a)" using assms(1) by (rule allE)
have 2: "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) by (rule allE)
have 3: "Q a (s a) ⟶ Q (s a) (s (s a))" using 2 by (rule allE)
have 4: "Q (s a) (s (s a))" using 3 1 by (rule mp)
have 5: "Q a (s a) ∧ Q (s a) (s (s a))" using 1 4 by (rule conjI)
show 6: "∃z. Q a z ∧ Q z (s (s a))" using 5 by (rule exI)
qed
text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar o refutar
{x = f x, odd (f x)} ⊢ odd x
------------------------------------------------------------------ *}

lemma ejercicio_36a:
assumes "x = f x" and
"odd (f x)"
shows "odd x"
proof -
show "odd x" using assms(1) assms(2) by (rule ssubst)
qed

text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar o refutar
{x = f x, triple (f x) (f x) x} ⊢ triple x x x
------------------------------------------------------------------ *}

lemma ejercicio_37a:
assumes "x = f x" and
"triple (f x) (f x) x"
shows "triple x x x"

proof -
show "triple x x x" using assms(1) assms(2) by (rule ssubst)
qed

end

</source>

Rel 4

2018-07-16T12:41:06Z

WikiSysop: Texto reemplazado: «Isar» por «isabelle»

Lógica matemática y fundamentos (2015-16)

2018-07-16T12:40:27Z

WikiSysop:

En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]]).
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]]).
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden ([[R6 |Enunciado]]).
* '''Relación 7''': Tableros semánticos proposicionales en Haskell. ([[Media:TablerosSemanticos.hs |Enunciado]]).
* '''Relación 8''': Cuestiones sobre tableros semánticos ([[R8 |Enunciado]]).
* '''Relación 9''': Cuestiones. ([[R9 |Enunciado]]).
* '''Relación 10''': Tableros semánticos en lógica de primer orden.([[R10 |Enunciado]]).
* '''Relación 11''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]]).
* '''Relación 12''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]]).
* '''Relación 13''': Cuestiones. ([[R13 |Enunciado]]).
* '''Relación 14''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]]).
* '''Relación 15''': Ejercicios de Lógica proposicional. ([[R15 sol | Una solución ]]).
* '''Relación 16''': Resolución en Lógica de primer orden. ([[R16 sol | Una solución ]]).

Relación 3

2018-07-16T12:38:08Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang = "isabelle">header {* R3: Deducción natural proposicional *}

theory R3
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es demostrar cada uno de los ejercicios
usando sólo las reglas básicas de deducción natural de la lógica
proposicional (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
---------------------------------------------------------------------
*}

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 {* Implicaciones *}

text {* ---------------------------------------------------------------
Ejercicio 1. Demostrar
p ⟶ q, p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_1:
assumes "p ⟶ q"
"p"
shows "q"

proof -
show "q" using assms(1,2) by (rule mp)
qed

lemma ejercicio_1_b:
assumes "p ⟶ q"
"p"
shows "q"
proof-
show "q" using assms(1) assms(2) by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ⟶ q, q ⟶ r, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_2:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"

proof-
have 1: "q" using assms(1,3) by (rule mp)
show "r" using assms(2) 1 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
p ⟶ (q ⟶ r), p ⟶ q, p ⊢ r
------------------------------------------------------------------ *}

lemma ejercicio_3:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"

proof-
have 1: "q" using assms(2,3) by (rule mp)
have 2: "q⟶r" using assms(1,3) by (rule mp)
show "r" using 2 1 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
p ⟶ q, q ⟶ r ⊢ p ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_4:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"

proof-
{assume 1: "p"
have 2: "q" using assms(1) 1 ..
have 3: "r" using assms(2) 2 ..}
thus "p⟶r" by (rule impI)
qed

lemma ejercicio_4:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
proof-
{assume 1 : "p"
have 2 : "q" using assms(1) 1 by (rule mp)
have 3 : "r" using assms(2) 2 by (rule mp)}
thus "p⟶r" by (rule impI)
qed

---**

proof(rule impI)
assume 1: "p"
have 2: "q" using assms(1) 1 by (rule mp)
show "r" using assms(2) 2 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_5:
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"

{assume 1: "q"
{assume 2: "p"
have 3: "q⟶r" using assms 2 by (rule mp)
have "r" using 3 1 by (rule mp)}
hence "p⟶r" by (rule impI)}
thus "(q⟶(p⟶r))" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_6:
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"

proof-
{assume 1:"p⟶q"
{assume 2: "p"
have 3: "q⟶r" using assms 2 by (rule mp)
have 4: "q" using 1 2 by (rule mp)
have "r" using 3 4 by (rule mp)}
hence "p⟶r" by (rule impI)}
thus "(p⟶q)⟶(p⟶r)" by (rule impI)
qed

---**
proof(rule impI)
assume 1: "p⟶q"
{assume 2: "p"
have 3: "q⟶r" using assms(1) 2 by (rule mp)
have 4: "q" using 1 2 by (rule mp)
have 5: "r" using 3 4 by (rule mp)}
then show"p⟶r" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
p ⊢ q ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"

proof-
{assume 1: "q"
have "p" using assms .}
thus "q⟶p" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
⊢ p ⟶ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_8:
"p ⟶ (q ⟶ p)"

proof-
{assume 1:"p"
{assume 2:"q"
have 3: "p" using 1 .}
hence "q⟶p" ..}
thus "p⟶(q⟶p)" ..
qed

lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
proof-
{assume 1 : "p"
{assume 2 : "q"
have 3 : "p" using 1 .}
hence "q⟶p" by (rule impI)}
thus "p⟶(q⟶p)" by (rule impI)
qed

lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
proof (rule impI)
assume 1: "p"
show "q ⟶ p"
proof (rule impI)
assume "q"
show "p" using 1 by this
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
p ⟶ q ⊢ (q ⟶ r) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_9:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"

proof-
{assume 1:"q⟶r"
{assume 2:"p"
have 3:"q" using assms 2 ..
have "r" using 1 3 ..}
hence "p⟶r" ..}
thus "(q⟶r)⟶(p⟶r) " ..
qed

lemma ejercicio_9:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof-
{assume 1 : "q⟶r"
{assume 2 : "p"
have 3 : "q" using assms(1) 2 by (rule mp)
have 4 : "r" using 1 3 by (rule mp)}
hence "p⟶r" by (rule impI)}
thus "(q⟶r)⟶(p⟶r)" by (rule impI)
qed

--**
proof(rule impI)
assume 1: "q⟶r"
{assume 2: "p"
have 3: "q" using assms 2 by (rule mp)
have 4: "r" using 1 3 by (rule mp)}
then show "p⟶r" by (rule impI)
qed

--**
(* aunque sé que hay algunos pasos innecesarios pero es otra forma de verlo.*)
proof-
{assume 1 : "q⟶r"
{assume 2 : "p"
{assume 3: "¬r"
have 4: "¬q" using 1 3 by (rule mt)
have 5: "q" using assms(1) 2 by (rule mp)
have 7: "False" using 4 5 by (rule notE)}
hence 6: "r" by (rule ccontr)}
hence 8 : "p⟶r" by (rule impI)}
thus "(q⟶r)⟶(p⟶r)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
p ⟶ (q ⟶ (r ⟶ s)) ⊢ r ⟶ (q ⟶ (p ⟶ s))
------------------------------------------------------------------ *}

lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"

proof-
{assume 1:"r"
{assume 2:"q"
{assume 3:"p"
have 4:"q⟶(r⟶s)" using assms 3 ..
have 5: "r⟶s" using 4 2 ..
have 6: "s" using 5 1 ..}
hence "p⟶s" ..}
hence "q⟶(p⟶s)" ..}
thus "r⟶(q⟶(p⟶s))" ..
qed

lemma ejercicio_10:
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof-
{assume 1 : "r"
{assume 2 : "q"
{assume 3 : "p"
have 4 : "q ⟶ (r ⟶ s)" using assms(1) 3 by (rule mp)
have 5 : "r⟶s" using 4 2 by (rule mp)
have 6 : "s" using 5 1 by (rule mp)}
hence "p⟶s" by (rule impI)}
hence "q⟶(p⟶s)" by (rule impI)}
thus "r⟶(q⟶(p⟶s))" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))
------------------------------------------------------------------ *}

lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"

proof (rule impI)
assume 3: "p⟶(q⟶r)"
show "(p⟶q)⟶(p⟶r)"
proof(rule impI)
assume 2:"p⟶q"
show "p⟶r"
proof (rule impI)
assume 1: "p"
have 4:"q" using 2 1 ..
have 5:"q⟶r" using 3 1 ..
show "r" using 5 4 ..
qed
qed
qed

lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof-
{assume 1 : "p ⟶ (q ⟶ r)"
{assume 2 : "p⟶q"
{assume 3 : "p"
have 4 : "q⟶r" using 1 3 by (rule mp)
have 5 : "q" using 2 3 by (rule mp)
have 6 : "r" using 4 5 by (rule mp)}
hence "p⟶r" by (rule impI)}
hence "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)}
thus "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 12. Demostrar
(p ⟶ q) ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_12:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"

proof-
{assume 1:"p"
{assume 3:"q"
have 4:"p" using 1 .
have 5:"q" using 3 .
then have 6:"p⟶q" ..
have "r" using assms 6 ..}
hence "q⟶r" ..}
thus "p⟶(q⟶r)" ..
qed

lemma ejercicio_12:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof-
{assume 1 : "p"
{assume 2 : "q"
{assume 3 : "p"
have 4 : "q" using 2 .}
hence 5 : "p⟶q" by (rule impI)
have 6 : "r" using assms(1) 5 by (rule mp)}
hence "q⟶r" by (rule impI)}
thus "p⟶(q⟶r)" by (rule impI)
qed

section {* Conjunciones *}

text {* ---------------------------------------------------------------
Ejercicio 13. Demostrar
p, q ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"

proof-
show "p∧q" using assms(1) assms(2) by (rule conjI)
qed

lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"
proof-
show "p ∧ q" using assms(1,2) by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 14. Demostrar
p ∧ q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_14:
assumes "p ∧ q"
shows "p"

proof-
show "p" using assms by (rule conjunct1)
qed

text {* ---------------------------------------------------------------
Ejercicio 15. Demostrar
p ∧ q ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_15:
assumes "p ∧ q"
shows "q"

proof-
show "q" using assms by (rule conjunct2)
qed

text {* ---------------------------------------------------------------
Ejercicio 16. Demostrar
p ∧ (q ∧ r) ⊢ (p ∧ q) ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"

proof-
have 1:"p" using assms by (rule conjunct1)
have 2:"q∧r" using assms by (rule conjunct2)
then have 3:"q" by (rule conjunct1)
have 4:"r" using 2 by (rule conjunct2)
have "p∧q" using 1 3 by (rule conjI)
then show "(p∧q)∧r" using 4 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 17. Demostrar
(p ∧ q) ∧ r ⊢ p ∧ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_17:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"

proof-
have 1:"p∧q" using assms by (rule conjunct1)
have 2:"r" using assms by (rule conjunct2)
have 3:"p" using 1 by (rule conjunct1)
have 4:"q" using 1 by (rule conjunct2)
have 5:"q∧r" using 4 2 by (rule conjI)
show "p∧(q∧r)" using 3 5 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 18. Demostrar
p ∧ q ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
proof-
have 1:"p" using assms ..
have 2:"q" using assms ..
then show "p⟶q" ..
qed

lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
proof-
{assume "p"
have "q" using assms by (rule conjunct2)}
thus "p⟶q" by (rule impI)
qed

--**

lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"
proof(rule impI)
assume 1: "p"
show "q" using assms by (rule conjunct2)
qed

text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_19:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof-
have 1:"p⟶q" using assms ..
have 2:"p⟶r" using assms ..
{assume 3:"p"
have 4:"q" using 1 3 ..
have 5:"r" using 2 3 ..
have 6:"q∧r" using 4 5 ..}
thus "p ⟶ q ∧ r" ..
qed

lemma ejercicio_19:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof-
{assume 1 : "p"
have 2 : "p⟶q" using assms by (rule conjunct1)
have 3 : "p⟶r" using assms by (rule conjunct2)
have 4 : "q" using 2 1 by (rule mp)
have 5 : "r" using 3 1 by (rule mp)
have 6 : "q ∧ r" using 4 5 by (rule conjI)}
thus "p⟶(q ∧ r)" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
p ⟶ q ∧ r ⊢ (p ⟶ q) ∧ (p ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_20:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"

proof-
{assume 1: p
have 2:"q∧r" using assms 1 ..
have "r" using 2 ..}
hence 1:"p⟶r" ..
{assume 1: p
have 2:"q∧r" using assms 1 ..
have "q" using 2 ..}
hence 2:"p⟶q" ..
then show "(p ⟶ q) ∧ (p ⟶ r)" using 1 ..
qed

lemma ejercicio_20:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof-
{assume 1 : "p"
have 2 : "q ∧ r" using assms 1 by (rule mp)
have 3 : "q" using 2 by (rule conjunct1)}
hence 4 : "p⟶q" by (rule impI)
{assume 5 : "p"
have 6 : "q ∧ r" using assms 5 by (rule mp)
have 7 : "r" using 6 by (rule conjunct2)}
hence 8 : "p⟶r" by (rule impI)
show "(p ⟶ q) ∧ (p ⟶ r)" using 4 8 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
p ⟶ (q ⟶ r) ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_21:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"

proof-
{assume 1:"p∧q"
have 2:"p" using 1 ..
have 3:"q⟶r" using assms 2 ..
have 4: "q" using 1 ..
have "r" using 3 4 ..}
thus "p∧q ⟶r" ..
qed

lemma ejercicio_21:
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof-
{assume 1 : "p ∧ q"
have 2 : "p" using 1 by (rule conjunct1)
have 3 : "q" using 1 by (rule conjunct2)
have 4 : "q⟶r" using assms 2 by (rule mp)
have 5 : "r" using 4 3 by (rule mp)}
thus "p ∧ q ⟶ r" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
p ∧ q ⟶ r ⊢ p ⟶ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_22:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"

proof-
{assume 1:"p"
{assume 2:"q"
have 3:"p∧q" using 1 2 ..
have "r" using assms 3 ..}
hence "q⟶r" ..}
thus "p⟶(q⟶r)" ..
qed

lemma ejercicio_22:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof-
{assume 1 : "p"
{assume 2 : "q"
have 3 : "p ∧ q" using 1 2 by (rule conjI)
have 4 : "r" using assms 3 by (rule mp)}
hence "q⟶r" by (rule impI)}
thus "p⟶(q⟶r)" by (rule impI)
qed

lemma ejercicio_22:
assumes 1:"p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume 2:"p"
show "q ⟶ r"
proof (rule impI)
assume 3:"q"
have 4:"p ∧ q" using 2 3 by (rule conjI)
show "r" using 1 4 by (rule mp)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
(p ⟶ q) ⟶ r ⊢ p ∧ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_23:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"

proof-
{assume 1:"p∧q"
have 2:"p" using 1 ..
{assume "p"
have 3: "q" using 1 ..}
hence 4:"p⟶q" ..
have "r" using assms 4 ..}
thus "p∧q ⟶r" ..
qed

lemma ejercicio_23:
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof-
{assume 1 : "p ∧ q"
{assume 2 : "p"
have 3 : "q" using 1 by (rule conjunct2)}
hence 4 : "p⟶q" by (rule impI)
have 5 : "r" using assms 4 by (rule mp)}
thus "p ∧ q ⟶ r" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 24. Demostrar
p ∧ (q ⟶ r) ⊢ (p ⟶ q) ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_24:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"

proof-
{assume 1: "p⟶q"
have 2:"p" using assms ..
have 3:"q⟶r" using assms..
have 4:"q" using 1 2 ..
have "r" using 3 4 ..}
thus "(p⟶q)⟶r" ..
qed

lemma ejercicio_24:
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof-
{assume 1 : "p⟶q"
have 2 : "p" using assms by (rule conjunct1)
have 3 : "q⟶r" using assms by (rule conjunct2)
have 4 : "q" using 1 2 by (rule mp)
have 5 : "r" using 3 4 by (rule mp)}
thus "(p⟶q)⟶r" by (rule impI)
qed

lemma ejercicio_24:
assumes 1:"p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof (rule impI)
assume 2:"p ⟶ q"
have 3:"p" using 1 by (rule conjunct1)
have 4:"q" using 2 3 by (rule mp)
have 5:"q ⟶ r" using 1 by (rule conjunct2)
show "r" using 5 4 by (rule mp)
qed

section {* Disyunciones *}

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
p ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_25:
assumes "p"
shows "p ∨ q"

proof-
show "p∨q" using assms by (rule disjI1)
qed

text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
q ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_26:
assumes "q"
shows "p ∨ q"

proof-
show "p∨q" using assms by (rule disjI2)
qed

text {* ---------------------------------------------------------------
Ejercicio 27. Demostrar
p ∨ q ⊢ q ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_27:
assumes "p ∨ q"
shows "q ∨ p"

proof -
have "p ∨ q" using assms by this
moreover
{ assume 2: "p"
have "q ∨ p" using 2 by (rule disjI2) }
moreover
{ assume 3: "q"
have "q ∨ p" using 3 by (rule disjI1) }
ultimately show "q ∨ p" by (rule disjE)
qed

lemma ejercicio_27:
assumes 1:"p ∨ q"
shows "q ∨ p"
using 1
proof (rule disjE)
{assume 2:"p"
show "q ∨ p" using 2 by (rule disjI2)}
next
{assume 4:"q"
show "q ∨ p" using 4 by (rule disjI1)}
qed

text {* ---------------------------------------------------------------
Ejercicio 28. Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_28:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof-
{assume "p ∨ q"
moreover
{ assume 1:"p"
have "p ∨ r" using 1 by (rule disjI1)}
moreover
{ assume 2:"q"
have 3:"r" using assms 2 by (rule mp)
have "p ∨ r" using 3 by (rule disjI2) }
ultimately have " p ∨ r" by (rule disjE)}
thus "p ∨ q ⟶ p ∨ r" by (rule impI)
qed

lemma ejercicio_28:
assumes 1:"q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
assume 2:"p ∨ q"
thus "p ∨ r"
proof (rule disjE)
{assume 3:"p"
show "p ∨ r" using 3 by (rule disjI1)}
next
{assume 4:"q"
have 5:"r" using 1 4 by (rule mp)
show "p ∨ r" using 5 by (rule disjI2)}
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar
p ∨ p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_29:
assumes "p ∨ p"
shows "p"

proof-
have 1: "p ∨ p" using assms by this
moreover
{assume 1:"p"
have "p" using 1 by this}
moreover
{assume 2:"p"
have "p" using 2 by this}
ultimately show "p" by (rule disjE)

qed
text{* Otra forma:
using assms
proof
assume "p"
thus "p" .
qed}

lemma ejercicio_29:
assumes "p ∨ p"
shows "p"
proof-
have "p ∨ p" using assms by this
moreover
{assume 1 : "p"
have "p" using 1 .}
moreover
{assume 2 : "p"
have "p" using 2 .}
ultimately show "p" by (rule disjE)
qed*}

lemma ejercicio_29:
assumes 1:"p ∨ p"
shows "p"
using 1
proof (rule disjE)
{assume 2:"p"
show "p" using 2 by this}
next
{assume 3:"p"
show "p" using 3 by this}
qed

text {* ---------------------------------------------------------------
Ejercicio 30. Demostrar
p ⊢ p ∨ p
------------------------------------------------------------------ *}

lemma ejercicio_30:
assumes "p"
shows "p ∨ p"
proof-
show "p ∨ p" using assms by (rule disjI1)
qed

text{* Otra forma:
using assms
proof
qed}

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar
p ∨ (q ∨ r) ⊢ (p ∨ q) ∨ r
------------------------------------------------------------------ *}

lemma ejercicio_31:
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
proof -
have "p ∨ (q ∨ r)" using assms(1) by this
moreover
{ assume 1: "p"
have 2: "p ∨ q" using 1 by (rule disjI1)
have 3: "(p ∨ q) ∨ r" using 2 by (rule disjI1)}
moreover
{ assume 4: "q ∨ r"
moreover
{ assume 5: "q"
have 6: "p ∨ q" using 5 by (rule disjI2)
have 7: "(p ∨ q) ∨ r" using 6 by (rule disjI1)}
moreover
{ assume 8: "r"
have 9: "(p ∨ q) ∨ r" using 8 by (rule disjI2)}
ultimately have "(p ∨ q) ∨ r" by (rule disjE)}
ultimately show "(p ∨ q) ∨ r" by (rule disjE)
qed

text{* Otra forma:
using assms
proof
assume "p"
then have "p∨q" ..
thus "(p∨q)∨r" ..
next
assume 1:"q∨r"
thus "(p ∨ q) ∨ r"
proof
assume "q"
then have "p∨q" ..
thus 1: "(p ∨ q) ∨ r" ..
next
assume "r"
then have 2:"(p∨q)∨r" ..
then have "q∨r⟶(p ∨ q) ∨ r" ..
thus "(p ∨ q) ∨ r" using 1 ..
qed}*}

lemma ejercicio_31:
assumes 1:"p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
using 1
proof (rule disjE)
{assume 2:"p"
have 3:"p ∨ q" using 2 by (rule disjI1)
show "(p ∨ q) ∨ r" using 3 by (rule disjI1)}
next
{assume 4:"q ∨ r"
thus "(p ∨ q) ∨ r"
proof (rule disjE)
{assume 5:"q"
have 6:"p ∨ q" using 5 by (rule disjI2)
show "(p ∨ q) ∨ r" using 6 by (rule disjI1)}
next
{assume 7:"r"
show "(p ∨ q) ∨ r" using 7 by (rule disjI2)}
qed}
qed

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar
(p ∨ q) ∨ r ⊢ p ∨ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_32:
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
proof -
have "(p ∨ q) ∨ r" using assms(1) by this
moreover
{ assume 1: "p ∨ q"
moreover
{ assume 2: "p"
have 3: "p ∨ (q ∨ r)" using 2 by (rule disjI1)}
moreover
{ assume 4: "q"
have 5: "q ∨ r" using 4 by (rule disjI1)
have 6: "p ∨ (q ∨ r)" using 5 by (rule disjI2)}
ultimately have "p ∨ (q ∨ r)" by (rule disjE)}
moreover
{ assume 7: "r"
have 8: "q ∨ r" using 7 by (rule disjI2)
have 9: "p ∨ (q ∨ r)" using 8 by (rule disjI2)}
ultimately show "p ∨ (q ∨ r)" by (rule disjE)
qed

lemma ejercicio_32:
assumes 1:"(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using 1
proof (rule disjE)
{assume 2:"p ∨ q"
thus "p ∨ (q ∨ r)"
proof (rule disjE)
{assume 3:"p"
show "p ∨ (q ∨ r)" using 3 by (rule disjI1)}
next
{assume 4:"q"
have 5:"q ∨ r" using 4 by (rule disjI1)
show "p ∨ (q ∨ r)" using 5 by (rule disjI2)}
qed}
next
{assume 6:"r"
have 7:"q ∨ r" using 6 by (rule disjI2)
show "p ∨ (q ∨ r)" using 7 by (rule disjI2)}
qed

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar
p ∧ (q ∨ r) ⊢ (p ∧ q) ∨ (p ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_33:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "q ∨ r" using assms(1) by (rule conjunct2)
moreover
{ assume 3: "q"
have 4: "p ∧ q" using 1 3 by (rule conjI)
have 5: "(p ∧ q) ∨ (p ∧ r)" using 4 by (rule disjI1)}
moreover
{ assume 6: "r"
have 7: "p ∧ r" using 1 6 by (rule conjI)
have 8: "(p ∧ q) ∨ (p ∧ r)" using 7 by (rule disjI2)}
ultimately show "(p ∧ q) ∨ (p ∧ r)" by (rule disjE)
qed

lemma ejercicio_33:
assumes 1:"p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 2:"p" using 1 by (rule conjunct1)
have 3:"q ∨ r" using 1 by (rule conjunct2)
thus "(p ∧ q) ∨ (p ∧ r)"
proof (rule disjE)
{assume 4:"q"
have 5:"p ∧ q" using 2 4 by (rule conjI)
show "(p ∧ q) ∨ (p ∧ r)" using 5 by (rule disjI1)}
next
{assume 6:"r"
have 7:"p ∧ r" using 2 6 by (rule conjI)
show "(p ∧ q) ∨ (p ∧ r)" using 7 by (rule disjI2)}
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar
(p ∧ q) ∨ (p ∧ r) ⊢ p ∧ (q ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_34:
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
proof -
have "(p ∧ q) ∨ (p ∧ r)" using assms(1) by this
moreover
{ assume 1: "p ∧ q"
have 2: "q" using 1 by (rule conjunct2)
have 3: "q ∨ r" using 2 by (rule disjI1)
have 4: "p" using 1 by (rule conjunct1)
have 5: "p ∧ (q ∨ r)" using 4 3 by (rule conjI)}
moreover
{ assume 6: "p ∧ r"
have 7: "r" using 6 by (rule conjunct2)
have 8: "q ∨ r" using 7 by (rule disjI2)
have 9: "p" using 6 by (rule conjunct1)
have 10: "p ∧ (q ∨ r)" using 9 8 by (rule conjI)}
ultimately show "p ∧ (q ∨ r)" by (rule disjE)
qed

lemma ejercicio_34:
assumes 1:"(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
using 1
proof (rule disjE)
{assume 2:"p ∧ q"
have 3:"p" using 2 by (rule conjunct1)
have 4:"q" using 2 by (rule conjunct2)
have 5:"q ∨ r" using 4 by (rule disjI1)
show "p ∧ (q ∨ r)" using 3 5 by (rule conjI)}
next
{assume 6:"p ∧ r"
have 7:"p" using 6 by (rule conjunct1)
have 8:"r" using 6 by (rule conjunct2)
have 9:"q ∨ r" using 8 by (rule disjI2)
show "p ∧ (q ∨ r)" using 7 9 by (rule conjI)}
qed

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar
p ∨ (q ∧ r) ⊢ (p ∨ q) ∧ (p ∨ r)
------------------------------------------------------------------ *}

lemma ejercicio_35:
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
proof -
have "p ∨ (q ∧ r)" using assms(1) by this
moreover
{ assume 1: "p"
have 2: "p ∨ q" using 1 by (rule disjI1)
have 3: "p ∨ r" using 1 by (rule disjI1)
have 4: "(p ∨ q) ∧ (p ∨ r)" using 2 3 by (rule conjI)}
moreover
{ assume 5: "q ∧ r"
have 6: "q" using 5 by (rule conjunct1)
have 7: "p ∨ q" using 6 by (rule disjI2)
have 8: "r" using 5 by (rule conjunct2)
have 9: "p ∨ r" using 8 by (rule disjI2)
have 10: "(p ∨ q) ∧ (p ∨ r)" using 7 9 by (rule conjI)}
ultimately show "(p ∨ q) ∧ (p ∨ r)" by (rule disjE)
qed

lemma ejercicio_35:
assumes 1:"p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
using 1
proof (rule disjE)
{assume 2:"p"
have 3:"p ∨ q" using 2 by (rule disjI1)
have 4:"p ∨ r" using 2 by (rule disjI1)
show "(p ∨ q) ∧ (p ∨ r)" using 3 4 by (rule conjI)}
next
{assume 5:"q ∧ r"
have 6:"q" using 5 by (rule conjunct1)
have 7:"r" using 5 by (rule conjunct2)
have 8:"p ∨ q" using 6 by (rule disjI2)
have 9:"p ∨ r" using 7 by (rule disjI2)
show "(p ∨ q) ∧ (p ∨ r)" using 8 9 by (rule conjI)}
qed

text {* ---------------------------------------------------------------
Ejercicio 36. Demostrar
(p ∨ q) ∧ (p ∨ r) ⊢ p ∨ (q ∧ r)
------------------------------------------------------------------ *}

lemma ejercicio_36:
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof-
have "(p ∨ q)" using assms by (rule conjunct1)
moreover
{assume 1:"p"
have "p ∨ (q ∧ r)" using 1 by (rule disjI1) }
moreover
{assume 1:"q"
have "(p ∨ r)" using assms by (rule conjunct2)
moreover
{assume 2:"p"
have "p ∨ (q ∧ r)" using 2 by (rule disjI1)}
moreover
{assume 2:"r"
have 3:"(q ∧ r)" using 1 2 by (rule conjI)
have "p ∨ (q ∧ r)" using 3 by (rule disjI2)}
ultimately have "p ∨ (q ∧ r)" by (rule disjE)}
ultimately show "p ∨ (q ∧ r)" by (rule disjE)
qed

------------------- ----------

proof-
have 1: "p∨q" using assms by (rule conjunct1)
thus "p∨(q∧r)"
proof(rule disjE)
{assume 3: "p"
show "p∨(q∧r)" using 3 by ( rule disjI1)}
next
{assume 4: "q"
have 5:"p∨r" using assms by (rule conjunct2)
thus "p∨(q∧r)"
proof(rule disjE)
{assume 6: "p"
show "p∨(q∧r)" using 6 by (rule disjI1)}
next
{assume 7: "r"
have 8: "q∧r" using 4 7 by (rule conjI)
show "p∨(q∧r)" using 8 by (rule disjI2)}
qed}
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 37. Demostrar
(p ⟶ r) ∧ (q ⟶ r) ⊢ p ∨ q ⟶ r
------------------------------------------------------------------ *}

lemma ejercicio_37:
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof-
{assume "p ∨ q"
moreover
{assume 1:"p"
have 2:"(p ⟶ r)" using assms by (rule conjunct1)
have "r" using 2 1 by (rule mp)}
moreover
{assume 1:"q"
have 2:"(q ⟶ r)" using assms by (rule conjunct2)
have "r" using 2 1 by (rule mp)}
ultimately have "r" by (rule disjE)}
thus "p ∨ q ⟶ r" by (rule impI)
qed

lemma ejercicio_37:
assumes 1:"(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof (rule impI)
assume 2:"p ∨ q"
thus "r"
proof (rule disjE)
{assume 3:"p"
have 4:"p ⟶ r" using 1 by (rule conjunct1)
show "r" using 4 3 by (rule mp)}
next
{assume 5:"q"
have 6:"q ⟶ r" using 1 by (rule conjunct2)
show "r" using 6 5 by (rule mp)}
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 38. Demostrar
p ∨ q ⟶ r ⊢ (p ⟶ r) ∧ (q ⟶ r)
------------------------------------------------------------------ *}

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof-
{assume 1 : "p"
have 2 : "p ∨ q" using 1 by (rule disjI1)
have 3 : "r" using assms 2 by (rule mp)}
hence 4 : "p⟶r" by (rule impI)
{assume 5 : "q"
have 6 : "p ∨ q" using 5 by (rule disjI2)
have 7 : "r" using assms 6 by (rule mp)}
hence 8 : "q⟶r" by (rule impI)
show "(p ⟶ r) ∧ (q ⟶ r)" using 4 8 by (rule conjI)
qed

section {* Negaciones *}

text {* ---------------------------------------------------------------
Ejercicio 39. Demostrar
p ⊢ ¬¬p
------------------------------------------------------------------ *}

lemma ejercicio_39:
assumes "p"
shows "¬¬p"
proof-
show "¬¬p" using assms by (rule notnotI)
qed

text {* ---------------------------------------------------------------
Ejercicio 40. Demostrar
¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"

proof-
{assume 1: "p"
have "q" using assms 1 ..}
thus "p⟶q" ..
qed
-------------------------------
lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"
proof-
{assume 1 : "p"
have 2 : "False" using assms 1 by (rule notE)
have 3 : "q" using 2 by (rule FalseE)}
thus "p⟶q" by (rule impI)
qed

------------------------------
lemma ejercicio_40:
assumes "¬p"
shows "p ⟶ q"

proof-
{assume 1: "p"
have 2: "q" using assms 1 by (rule notE)}
thus "p ⟶ q" by ( rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 41. Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_41:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof-
{assume 1:"¬q"
have "¬p" using assms 1 by (rule mt)}
thus "¬q ⟶ ¬p" ..
qed

text {* ---------------------------------------------------------------
Ejercicio 42. Demostrar
p∨q, ¬q ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"

using assms(1)
proof
assume "p"
thus "p" .
next
assume 1:"q"
show "p" using assms(2) 1 ..
qed

lemma ejercicio_42:
assumes "p∨q"
"¬q"
shows "p"
proof-
have "p ∨ q" using assms(1) by this
moreover
{assume 1 : "p"
have 2 : "p" using 1 .}
moreover
{assume 3 : "q"
have 4 : "¬q" using assms(2) .
have 5 : "False" using 4 3 by (rule notE)
have 6 : "p" using 5 by (rule FalseE)}
ultimately show "p" by (rule disjE)
qed

--------**---
using assms(1)
proof(rule disjE)
{assume 1: "p"
have "p" using 1 by this}
next
{assume 2: "q"
show "p" using assms(2) 2 by (rule notE)}
qed

text {* ---------------------------------------------------------------
Ejercicio 43. Demostrar
p ∨ q, ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"

using assms(1)
proof
assume "q"
thus "q" .
next
assume 1:"p"
show "q" using assms(2) 1 ..
qed

lemma ejercicio_43:
assumes "p ∨ q"
"¬p"
shows "q"
proof-
have "p ∨ q" using assms(1) by this
moreover
{assume 1 : "p"
have 2 : "¬p" using assms(2) .
have 3 : "False" using 2 1 by (rule notE)
have 4 : "q" using 3 by (rule FalseE)}
moreover
{assume 5 : "q"
have 6 : "q" using 5 .}
ultimately show "q" by (rule disjE)
qed

---**--
using assms(1)
proof(rule disjE)
assume 1: "p"
show "q" using assms(2) 1 by (rule notE)
next
assume 2:"p"
have "p" using 2 by this
qed

text {* ---------------------------------------------------------------
Ejercicio 44. Demostrar
p ∨ q ⊢ ¬(¬p ∧ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof-
{assume 1 : "¬p ∧ ¬q"
have "p ∨ q" using assms by this
moreover
{assume 2 : "p"
have 3 : "¬p" using 1 by (rule conjunct1)
have 4 : "False" using 3 2 by (rule notE)}
moreover
{assume 5 : "q"
have 6 : "¬q" using 1 by (rule conjunct2)
have 7 : "False" using 6 5 by (rule notE)}
ultimately have 8 : "False" by (rule disjE)}
thus "¬(¬p ∧ ¬q)" by (rule notI)
qed

---**
proof(rule notI)
assume 2 :"¬p∧¬q"
show False
using assms
proof(rule disjE)
{assume 1: "p"
have 3: "¬p" using 2 by (rule conjunct1)
show False using 3 1 by (rule notE)}
{assume 4: "q"
have 5: "¬q" using 2 by (rule conjunct2)
show False using 5 4 by (rule notE)}
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 45. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof-
{assume 1 : "¬p ∨ ¬q"
have "¬p ∨ ¬q" using 1 by this
moreover
{assume 2 : "¬p"
have 3 : "p" using assms by (rule conjunct1)
have 4 : "False" using 2 3 by (rule notE)}
moreover
{assume 5 : "¬q"
have 6 : "q" using assms by (rule conjunct2)
have 7 : "False" using 5 6 by (rule notE)}
ultimately have "False" by (rule disjE)}
thus "¬(¬p ∨ ¬q)" by (rule notI)
qed

---**

assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"

proof (rule notI)
assume 1: "¬p∨¬q"
show False
using 1
proof(rule disjE)
assume 2: "¬p"
have 3: "p" using assms by (rule conjunct1)
show False using 2 3 by (rule notE)
next
assume 4: "¬q"
have 5: "q" using assms by (rule conjunct2)
show False using 4 5 by (rule notE)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 46. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof-
{assume 1 : "p"
have 2 : "p ∨ q" using 1 by (rule disjI1)
have 3 : "False" using assms 2 by (rule notE)}
hence 4 : "¬p" by (rule notI)
{assume 5 : "q"
have 6 : "p ∨ q" using 5 by (rule disjI2)
have 7 : "False" using assms 6 by (rule notE)}
hence 8 : "¬q" by (rule notI)
show "¬p ∧ ¬q" using 4 8 by (rule conjI)
qed

(*Otra opción para usar tercio excluso*)

lemma ejercicio_46_2:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof -
have 1:"¬p | p" by (rule excluded_middle)
show "¬p & ¬q"
using 1
proof (rule disjE)
{assume 2:"¬p"
have 3:"¬q | q" by (rule excluded_middle)
show "¬p & ¬q"
using 3
proof (rule disjE)
{assume 4:"¬q"
with 2 show "¬p & ¬q" by (rule conjI)}
next
{assume "q"
then have "p | q" by (rule disjI2)
with assms show "¬p & ¬q" by (rule notE)}
qed
}
next
{assume 5:"p"
then have "p | q" by (rule disjI1)
with assms show "¬p & ¬q" by (rule notE)
}
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 47. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}

lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof-
{assume 1 : "p ∨ q"
have "p ∨ q" using 1 by this
moreover
{assume 2 : "p"
have 3 : "¬p" using assms by (rule conjunct1)
have 4 : "False" using 3 2 by (rule notE)}
moreover
{assume 5 : "q"
have 6 : "¬q" using assms by (rule conjunct2)
have 6 : "False" using 6 5 by (rule notE)}
ultimately have "False" by (rule disjE)}
thus "¬(p ∨ q)" by (rule notI)
qed

---**

proof(rule notI)
assume 1: "p∨q"
show False
using 1
proof(rule disjE)
{assume 2:"p"
have 3:"¬p" using assms by (rule conjunct1)
show "False" using 3 2 by (rule notE)}
next
{assume 5:"q"
have 6:"¬q" using assms by (rule conjunct2)
show "False" using 6 5 by (rule notE)}
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 48. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}

lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof-
{assume 1 : "p ∧ q"
have "¬p ∨ ¬q" using assms by this
moreover
{assume 2 : "¬p"
have 3 : "p" using 1 by (rule conjunct1)
have 4 : "False" using 2 3 by (rule notE)}
moreover
{assume 5 : "¬q"
have 6 : "q" using 1 by (rule conjunct2)
have 7 : "False" using 5 6 by (rule notE)}
ultimately have "False" by (rule disjE)}
thus "¬(p ∧ q)" by (rule notI)
qed

--**
lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"

proof(rule notI)
assume 1:"p∧q"
show False
using assms
proof(rule disjE)
assume 2:"¬p"
have 3: "p" using 1 by (rule conjunct1)
show False using 2 3 by (rule notE)
next
assume 4: "¬q"
have 5: "q" using 1 by (rule conjunct2)
show False using 4 5 by (rule notE)
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 49. Demostrar
⊢ ¬(p ∧ ¬p)
------------------------------------------------------------------ *}

lemma ejercicio_49:
"¬(p ∧ ¬p)"
proof-
{assume 1 : "p ∧ ¬p"
have 2 : "p" using 1 by (rule conjunct1)
have 3 : "¬p" using 1 by (rule conjunct2)
have 4 : "False" using 3 2 by (rule notE)}
thus "¬(p ∧ ¬p)" by (rule notI)
qed

---**

proof(rule notI)
assume 1: "p∧¬p"
have 2: "p" using 1 by (rule conjunct1)
have 3: "¬p" using 1 by (rule conjunct2)
show False using 3 2 by (rule notE)
qed

text {* ---------------------------------------------------------------
Ejercicio 50. Demostrar
p ∧ ¬p ⊢ q
------------------------------------------------------------------ *}

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"

proof-
have 1 : "p" using assms by (rule conjunct1)
have 2 : "¬p" using assms by (rule conjunct2)
show "q" using 2 1 by (rule notE)
qed

text {* ---------------------------------------------------------------
Ejercicio 51. Demostrar
¬¬p ⊢ p
------------------------------------------------------------------ *}

lemma ejercicio_51:
assumes "¬¬p"
shows "p"

proof-
show "p" using assms by (rule notnotD)
qed

--**

lemma ejercicio_51:
assumes "¬¬p"
shows "p"
proof(rule ccontr)
assume 1: "¬p"
show False using assms 1 by (rule notE)
qed

text {* ---------------------------------------------------------------
Ejercicio 52. Demostrar
⊢ p ∨ ¬p
------------------------------------------------------------------ *}

lemma ejercicio_52:
"p ∨ ¬p"

proof-
have 1: "¬p∨p" by (rule excluded_middle)
have 2: "¬p∨p" using 1 by this
moreover
{assume 3: "¬p"
have 4: "p∨¬p" using 3 by (rule disjI2)}
moreover
{assume 5: "p"
have 6: "p∨¬p" using 5 by (rule disjI1)}
ultimately show "p∨¬p" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 53. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
proof-
{assume 1 : "(p ⟶ q) ⟶ p"
{assume 2 : "¬p"
have 3 : "¬(p⟶q)" using 1 2 by (rule mt)
{assume 4 : "p"
have 5 : "q" using 2 4 by (rule notE)}
hence 6 : "p⟶q" by (rule impI)
have 7 : "False" using 3 6 by (rule notE)}
hence 8 : "p" by (rule ccontr)}
thus "((p ⟶ q) ⟶ p) ⟶ p" by (rule impI)
qed

text {* ---------------------------------------------------------------
Ejercicio 54. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof-
{assume 1 : "p"
{assume 2 : "¬q"
have 3 : "¬p" using assms 2 by (rule mp)
have 4 : "False" using 3 1 by (rule notE)}
hence 5 : "q" by (rule ccontr)}
thus "p⟶q" by (rule impI)
qed

---**

proof(rule impI)
assume 1: "p"
have 2 : "¬¬p" using 1 by (rule notnotI)
have 3: "¬¬q" using assms 2 by (rule mt)
show "q" using 3 by (rule notnotD)
qed

text {* ---------------------------------------------------------------
Ejercicio 55. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof-
have 1 : "¬p ∨ p" by (rule excluded_middle)
have "¬p ∨ p" using 1 by this
moreover
{assume 2 : "¬p"
have 3 : "¬q ∨ q" by (rule excluded_middle)
have "¬q ∨ q" using 3 by this
moreover
{assume 4 : "¬q"
have 5 : "¬p ∧ ¬q" using 2 4 by (rule conjI)
have 6 : "False" using assms 5 by (rule notE)
have 7 : "p ∨ q" using 6 by (rule FalseE)}
moreover
{assume 8 : "q"
have 9 : "p ∨ q" using 8 by (rule disjI2)}
ultimately have "p ∨ q" by (rule disjE)}
moreover
{assume 10 : "p"
have 11 : "p ∨ q" using 10 by (rule disjI1)}
ultimately show "p ∨ q" by (rule disjE)
qed

(*Otra forma*)

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
have 1:"¬p | p" by (rule excluded_middle)
show "p | q" using 1
proof (rule disjE)
{assume 2:"¬p"
have 3:"¬q | q" by (rule excluded_middle)
show "p | q" using 3
proof (rule disjE)
{assume "q"
thus "p | q" by (rule disjI2)}
next
{assume "¬q"
with 2 have 4:"¬p & ¬q" by (rule conjI)
show "p | q" using assms 4 by (rule notE)}
qed}
next
{assume "p"
thus "p|q" by (rule disjI1)}
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 56. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}

lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof-
{assume 1 : "¬p"
have 2 : "¬p ∨ ¬q" using 1 by (rule disjI1)
have 3 : "False" using assms 2 by (rule notE)}
hence 4 : "p" by (rule ccontr)
{assume 5 : "¬q"
have 6 : "¬p ∨ ¬q" using 5 by (rule disjI2)
have 7 : "False" using assms 6 by (rule notE)}
hence 8 : "q" by (rule ccontr)
show "p ∧ q" using 4 8 by (rule conjI)
qed

--**
proof-
{assume 1: "¬p"
have 2: "¬p∨¬q"using 1 by (rule disjI1)
have 3: "False" using assms 2 by (rule notE)}
hence 8: "p" by (rule ccontr)
{assume 4: "¬q"
have 5: "¬p∨¬q" using 4 by (rule disjI2)
have 6: "False" using assms 5 by (rule notE)}
hence 9: "q" by (rule ccontr)
show "p∧q" using 8 9 by (rule conjI)
qed

text {* ---------------------------------------------------------------
Ejercicio 57. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}

lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof-
have 1 : "¬p ∨ p" by (rule excluded_middle)
have "¬p ∨ p" using 1 by this
moreover
{assume 2 : "¬p"
have 3 : "¬p ∨ ¬q" using 2 by (rule disjI1)}
moreover
{assume 4 : "p"
have 5 : "¬q ∨ q" by (rule excluded_middle)
have "¬q ∨ q" using 5 by this
moreover
{assume 6 : "¬q"
have 7 : "¬p ∨ ¬q" using 6 by (rule disjI2)}
moreover
{assume 8 : "q"
have 9 : "p ∧ q" using 4 8 by (rule conjI)
have 10 : "False" using assms 9 by (rule notE)
have 11 : "¬p ∨ ¬q" using 10 by (rule FalseE)}
ultimately have "¬p ∨ ¬q" by (rule disjE)}
ultimately show "¬p ∨ ¬q" by (rule disjE)
qed

text {* ---------------------------------------------------------------
Ejercicio 58. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"

proof-
have 1 : "¬(p ⟶ q) ∨ (p ⟶ q)" by (rule excluded_middle)
have "¬(p ⟶ q) ∨ (p ⟶ q)" using 1 by this
moreover
{assume 2 : "¬(p ⟶ q)"
{assume 3 : "q"
{assume 4 : "p"
have 5 : "q" using 3 .}
hence 6 : "p⟶q" by (rule impI)
have 7 : "p" using 2 6 by (rule notE)}
hence 8 : "q⟶p" by (rule impI)
have 9 : "(p ⟶ q) ∨ (q ⟶ p)" using 8 by (rule disjI2)}
moreover
{assume 10 : "p ⟶ q"
have 11 : "(p ⟶ q) ∨ (q ⟶ p)" using 10 by (rule disjI1)}
ultimately show "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjE)
qed

end
</source>

Rel 3

2018-07-16T12:38:07Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

MediaWiki:Common.css

2018-07-16T12:37:24Z

WikiSysop: Página creada con «/* Los estilos CSS colocados aquí se aplicarán a todas las apariencias */ @import url("/~jalonso/font-awesome-4.7.0/css/font-awesome.min.css");»

/* Los estilos CSS colocados aquí se aplicarán a todas las apariencias */
@import url("/~jalonso/font-awesome-4.7.0/css/font-awesome.min.css");

Lógica matemática y fundamentos (2015-16)

2016-02-16T11:39:26Z

WikiSysop: Página creada con '== Relaciones de ejercicios == En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas. * '''Relación 1(a)''': Iniciación a la programació...'

== Relaciones de ejercicios ==
En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).

MediaWiki:Mainpage

2016-02-16T11:38:08Z

WikiSysop: Página creada con 'Lógica matemática y fundamentos (2015-16)'

Lógica matemática y fundamentos (2015-16)

MediaWiki:Sidebar

2016-02-16T11:37:20Z

WikiSysop: Página creada con '* navigation ** mainpage|mainpage-description ** recentchanges-url|recentchanges * SEARCH * TOOLBOX * LANGUAGES'

* navigation
** mainpage|mainpage-description
** recentchanges-url|recentchanges
* SEARCH
* TOOLBOX
* LANGUAGES