Lógica matemática y fundamentos (2017-18) - Contribuciones del usuario [es]

Lógica matemática y fundamentos (2017-18)

2020-04-25T18:36:53Z

Jalonso:

== Relaciones de ejercicios ==

En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.
* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]]).
* '''Relación 2''': Deducción natural en lógica proposicional. ([[R2 |Enunciado]]).
* '''Relación 3''': Deducción natural en lógica proposicional(2). ([[R3 |Enunciado]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R4.thy '''Relación 4''']: Deducción natural proposicional con Isabelle/HOL. ([[R4 |Enunciado]]).
* '''Relación 5''': Sintaxis y semántica de la Lógica de primer orden. ([[R5 |Enunciado]]).
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden (II). ([[R6 |Enunciado]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R7.thy '''Relación 7''']: Deducción natural en lógica de primer orden con Isabelle/HOL. ([[R7 |Enunciado]]).
* '''Relación 8''': Tableros semánticos. ([[R8 |Enunciado]]).
* '''Relación 9''': Resolución proposicional. ([[R9 |Enunciado]]).
* '''Relación 10''': Cuestiones. ([[R10 |Enunciado]]).
* '''Relación 11''': Resolución en lógica de primer orden. ([[R11 |Enunciado]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8a''': [[Tema 8a | Deducción natural en lógica de primer orden con Isabelle/HOL]].
<!--
* '''Tema 14''': [[Tema 14 | Programación funcional en Isabelle/HOL]] ([[Media:T14.thy |Teoría]]).
* '''Tema 15''': [[Tema 15 | Razonamiento sobre programas con Isabelle/HOL]] ([[Media:T15.thy |Teoría]]).

Tema 8a

2018-11-19T07:55:34Z

Jalonso: Página creada con «<source lang="isabelle"> chapter {* Tema 8: Deducción natural en lógica de primer orden *} theory T8b_Deduccion_natural_en_logica_de_primer_orden imports Main begin te…»

<source lang="isabelle">
chapter {* Tema 8: Deducción natural en lógica de primer orden *}

theory T8b_Deduccion_natural_en_logica_de_primer_orden
imports Main
begin

text {*
El objetivo de este tema es presentar la deducción natural en
lógica de primer orden con Isabelle/HOL. La presentación se
basa en los ejemplos de tema 8 del curso LMF que se encuentra
en http://goo.gl/uJj8d (que a su vez se basa en el libro de
Huth y Ryan "Logic in Computer Science" http://goo.gl/qsVpY ).

La página al lado de cada ejemplo indica la página de las
transparencias de LMF donde se encuentra la demostración. *}

section {* Reglas del cuantificador universal *}

text {*
Las reglas del cuantificador universal son
· allE: ⟦∀x. P x; P a ⟹ R⟧ ⟹ R
· allI: (⋀x. P x) ⟹ ∀x. P x
*}

text {*
Ejemplo 1 (p. 10). Demostrar que
P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c)
*}

-- "La demostración detallada es"
lemma ejemplo_1a:
assumes 1: "P(c)" and
2: "∀x. (P(x) ⟶ ¬Q(x))"
shows "¬Q(c)"
proof -
have 3: "P(c) ⟶ ¬Q(c)" using 2 by (rule allE)
show 4: "¬Q(c)" using 3 1 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejemplo_1b:
assumes "P(c)"
"∀x. (P(x) ⟶ ¬Q(x))"
shows "¬Q(c)"
proof -
have "P(c) ⟶ ¬Q(c)" using assms(2) ..
thus "¬Q(c)" using assms(1) ..
qed

-- "La demostración automática es"
lemma ejemplo_1c:
assumes "P(c)"
"∀x. (P(x) ⟶ ¬Q(x))"
shows "¬Q(c)"
using assms
by auto

text {*
Ejemplo 2 (p. 11). Demostrar que
∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x)
*}

-- "La demostración detallada es"
lemma ejemplo_2a:
assumes 1: "∀x. (P x ⟶ ¬(Q x))" and
2: "∀x. P x"
shows "∀x. ¬(Q x)"
proof -
{ fix a
have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
have 4: "P a" using 2 by (rule allE)
have 5: "¬(Q a)" using 3 4 by (rule mp) }
thus "∀x. ¬(Q x)" by (rule allI)
qed

-- "La demostración detallada hacia atrás es"
lemma ejemplo_2b:
assumes 1: "∀x. (P x ⟶ ¬(Q x))" and
2: "∀x. P x"
shows "∀x. ¬(Q x)"
proof (rule allI)
fix a
have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
have 4: "P a" using 2 by (rule allE)
show 5: "¬(Q a)" using 3 4 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejemplo_2c:
assumes "∀x. (P x ⟶ ¬(Q x))"
"∀x. P x"
shows "∀x. ¬(Q x)"
proof
fix a
have "P a" using assms(2) ..
have "P a ⟶ ¬(Q a)" using assms(1) ..
thus "¬(Q a)" using `P a` ..
qed

-- "La demostración automática es"
lemma ejemplo_2d:
assumes "∀x. (P x ⟶ ¬(Q x))"
"∀x. P x"
shows "∀x. ¬(Q x)"
using assms
by auto

section {* Reglas del cuantificador existencial *}

text {*
Las reglas del cuantificador existencial son
· exI: P a ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

En la regla exE la nueva variable se introduce mediante la declaración
"obtain ... where ... by (rule exE)"
*}

text {*
Ejemplo (p. 12). Demostrar que
∀x. P x ⊢ ∃x. P x
*}

-- "La demostración detallada es"
lemma ejemplo_3a:
assumes "∀x. P x"
shows "∃x. P x"
proof -
fix a
have "P a" using assms by (rule allE)
thus "∃x. P x" by (rule exI)
qed

-- "La demostración estructurada es"
lemma ejemplo_3b:
assumes "∀x. P x"
shows "∃x. P x"
proof -
fix a
have "P a" using assms ..
thus "∃x. P x" ..
qed

-- "La demostración estructurada se puede simplificar"
lemma ejemplo_3c:
assumes "∀x. P x"
shows "∃x. P x"
proof (rule exI)
fix a
show "P a" using assms ..
qed

-- "La demostración estructurada se puede simplificar aún más"
lemma ejemplo_3d:
assumes "∀x. P x"
shows "∃x. P x"
proof
fix a
show "P a" using assms ..
qed

-- "La demostración automática es"
lemma ejemplo_3e:
assumes "∀x. P x"
shows "∃x. P x"
using assms
by auto

text {*
Ejemplo 4 (p. 13). Demostrar
∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x
*}

-- "La demostración detallada es"
lemma ejemplo_4a:
assumes 1: "∀x. (P x ⟶ Q x)" and
2: "∃x. P x"
shows "∃x. Q x"
proof -
obtain a where 3: "P a" using 2 by (rule exE)
have 4: "P a ⟶ Q a" using 1 by (rule allE)
have 5: "Q a" using 4 3 by (rule mp)
thus 6: "∃x. Q x" by (rule exI)
qed

-- "La demostración estructurada es"
lemma ejemplo_4b:
assumes "∀x. (P x ⟶ Q x)"
"∃x. P x"
shows "∃x. Q x"
proof -
obtain a where "P a" using assms(2) ..
have "P a ⟶ Q a" using assms(1) ..
hence "Q a" using `P a` ..
thus "∃x. Q x" ..
qed

-- "La demostración automática es"
lemma ejemplo_4c:
assumes "∀x. (P x ⟶ Q x)"
"∃x. P x"
shows "∃x. Q x"
using assms
by auto

section {* Demostración de equivalencias *}

text {*
Ejemplo 5.1 (p. 15). Demostrar
¬∀x. P x ⊢ ∃x. ¬(P x) *}

-- "La demostración detallada es"
lemma ejemplo_5_1a:
assumes "¬(∀x. P(x))"
shows "∃x. ¬P(x)"
proof (rule ccontr)
assume "¬(∃x. ¬P(x))"
have "∀x. P(x)"
proof (rule allI)
fix a
show "P(a)"
proof (rule ccontr)
assume "¬P(a)"
hence "∃x. ¬P(x)" by (rule exI)
with `¬(∃x. ¬P(x))` show False by (rule notE)
qed
qed
with assms show False by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_5_1b:
assumes "¬(∀x. P(x))"
shows "∃x. ¬P(x)"
proof (rule ccontr)
assume "¬(∃x. ¬P(x))"
have "∀x. P(x)"
proof
fix a
show "P(a)"
proof (rule ccontr)
assume "¬P(a)"
hence "∃x. ¬P(x)" ..
with `¬(∃x. ¬P(x))` show False ..
qed
qed
with assms show False ..
qed

-- "La demostración automática es"
lemma ejemplo_5_1c:
assumes "¬(∀x. P(x))"
shows "∃x. ¬P(x)"
using assms
by auto

text {*
Ejemplo 5.2 (p. 16). Demostrar
∃x. ¬(P x) ⊢ ¬∀x. P x *}

-- "La demostración detallada es"
lemma ejemplo_5_2a:
assumes "∃x. ¬P(x)"
shows "¬(∀x. P(x))"
proof (rule notI)
assume "∀x. P(x)"
obtain a where "¬P(a)" using assms by (rule exE)
have "P(a)" using `∀x. P(x)` by (rule allE)
with `¬P(a)` show False by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_5_2b:
assumes "∃x. ¬P(x)"
shows "¬(∀x. P(x))"
proof
assume "∀x. P(x)"
obtain a where "¬P(a)" using assms ..
have "P(a)" using `∀x. P(x)` ..
with `¬P(a)` show False ..
qed

-- "La demostración automática es"
lemma ejemplo_5_2c:
assumes "∃x. ¬P(x)"
shows "¬(∀x. P(x))"
using assms
by auto

text {*
Ejemplo 5.3 (p. 17). Demostrar
⊢ ¬∀x. P x ⟷ ∃x. ¬(P x) *}

-- "La demostración detallada es"
lemma ejemplo_5_3a:
"(¬(∀x. P(x))) ⟷ (∃x. ¬P(x))"
proof (rule iffI)
assume "¬(∀x. P(x))"
thus "∃x. ¬P(x)" by (rule ejemplo_5_1a)
next
assume "∃x. ¬P(x)"
thus "¬(∀x. P(x))" by (rule ejemplo_5_2a)
qed

-- "La demostración automática es"
lemma ejemplo_5_3b:
"(¬(∀x. P(x))) ⟷ (∃x. ¬P(x))"
by auto

text {*
Ejemplo 6.1 (p. 18). Demostrar
∀x. P(x) ∧ Q(x) ⊢ (∀x. P(x)) ∧ (∀x. Q(x)) *}

-- "La demostración detallada es"
lemma ejemplo_6_1a:
assumes "∀x. P(x) ∧ Q(x)"
shows "(∀x. P(x)) ∧ (∀x. Q(x))"
proof (rule conjI)
show "∀x. P(x)"
proof (rule allI)
fix a
have "P(a) ∧ Q(a)" using assms by (rule allE)
thus "P(a)" by (rule conjunct1)
qed
next
show "∀x. Q(x)"
proof (rule allI)
fix a
have "P(a) ∧ Q(a)" using assms by (rule allE)
thus "Q(a)" by (rule conjunct2)
qed
qed

-- "La demostración estructurada es"
lemma ejemplo_6_1b:
assumes "∀x. P(x) ∧ Q(x)"
shows "(∀x. P(x)) ∧ (∀x. Q(x))"
proof
show "∀x. P(x)"
proof
fix a
have "P(a) ∧ Q(a)" using assms ..
thus "P(a)" ..
qed
next
show "∀x. Q(x)"
proof
fix a
have "P(a) ∧ Q(a)" using assms ..
thus "Q(a)" ..
qed
qed

-- "La demostración automática es"
lemma ejemplo_6_1c:
assumes "∀x. P(x) ∧ Q(x)"
shows "(∀x. P(x)) ∧ (∀x. Q(x))"
using assms
by auto

text {*
Ejemplo 6.2 (p. 19). Demostrar
(∀x. P(x)) ∧ (∀x. Q(x)) ⊢ ∀x. P(x) ∧ Q(x) *}

-- "La demostración detallada es"
lemma ejemplo_6_2a:
assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
shows "∀x. P(x) ∧ Q(x)"
proof (rule allI)
fix a
have "∀x. P(x)" using assms by (rule conjunct1)
hence "P(a)" by (rule allE)
have "∀x. Q(x)" using assms by (rule conjunct2)
hence "Q(a)" by (rule allE)
with `P(a)` show "P(a) ∧ Q(a)" by (rule conjI)
qed

-- "La demostración estructurada es"
lemma ejemplo_6_2b:
assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
shows "∀x. P(x) ∧ Q(x)"
proof
fix a
have "∀x. P(x)" using assms ..
hence "P(a)" by (rule allE)
have "∀x. Q(x)" using assms ..
hence "Q(a)" ..
with `P(a)` show "P(a) ∧ Q(a)" ..
qed

-- "La demostración automática es"
lemma ejemplo_6_2c:
assumes "(∀x. P(x)) ∧ (∀x. Q(x))"
shows "∀x. P(x) ∧ Q(x)"
using assms
by auto

text {*
Ejemplo 6.3 (p. 20). Demostrar
⊢ ∀x. P(x) ∧ Q(x) ⟷ (∀x. P(x)) ∧ (∀x. Q(x)) *}

-- "La demostración detallada es"
lemma ejemplo_6_3a:
"(∀x. P(x) ∧ Q(x)) ⟷ ((∀x. P(x)) ∧ (∀x. Q(x)))"
proof (rule iffI)
assume "∀x. P(x) ∧ Q(x)"
thus "(∀x. P(x)) ∧ (∀x. Q(x))" by (rule ejemplo_6_1a)
next
assume "(∀x. P(x)) ∧ (∀x. Q(x))"
thus "∀x. P(x) ∧ Q(x)" by (rule ejemplo_6_2a)
qed

text {*
Ejemplo 7.1 (p. 21). Demostrar
(∃x. P(x)) ∨ (∃x. Q(x)) ⊢ ∃x. P(x) ∨ Q(x) *}

-- "La demostración detallada es"
lemma ejemplo_7_1a:
assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
shows "∃x. P(x) ∨ Q(x)"
using assms
proof (rule disjE)
assume "∃x. P(x)"
then obtain a where "P(a)" by (rule exE)
hence "P(a) ∨ Q(a)" by (rule disjI1)
thus "∃x. P(x) ∨ Q(x)" by (rule exI)
next
assume "∃x. Q(x)"
then obtain a where "Q(a)" by (rule exE)
hence "P(a) ∨ Q(a)" by (rule disjI2)
thus "∃x. P(x) ∨ Q(x)" by (rule exI)
qed

-- "La demostración estructurada es"
lemma ejemplo_7_1b:
assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
shows "∃x. P(x) ∨ Q(x)"
using assms
proof
assume "∃x. P(x)"
then obtain a where "P(a)" ..
hence "P(a) ∨ Q(a)" ..
thus "∃x. P(x) ∨ Q(x)" ..
next
assume "∃x. Q(x)"
then obtain a where "Q(a)" ..
hence "P(a) ∨ Q(a)" ..
thus "∃x. P(x) ∨ Q(x)" ..
qed

-- "La demostración automática es"
lemma ejemplo_7_1c:
assumes "(∃x. P(x)) ∨ (∃x. Q(x))"
shows "∃x. P(x) ∨ Q(x)"
using assms
by auto

text {*
Ejemplo 7.2 (p. 22). Demostrar
∃x. P(x) ∨ Q(x) ⊢ (∃x. P(x)) ∨ (∃x. Q(x)) *}

-- "La demostración detallada es"
lemma ejemplo_7_2a:
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)
thus "(∃x. P(x)) ∨ (∃x. Q(x))"
proof (rule disjE)
assume "P(a)"
hence "∃x. P(x)" by (rule exI)
thus "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI1)
next
assume "Q(a)"
hence "∃x. Q(x)" by (rule exI)
thus "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI2)
qed
qed

-- "La demostración estructurada es"
lemma ejercicio_7_2b:
assumes "∃x. P(x) ∨ Q(x)"
shows "(∃x. P(x)) ∨ (∃x. Q(x))"
proof -
obtain a where "P(a) ∨ Q(a)" using assms ..
thus "(∃x. P(x)) ∨ (∃x. Q(x))"
proof
assume "P(a)"
hence "∃x. P(x)" ..
thus "(∃x. P(x)) ∨ (∃x. Q(x))" ..
next
assume "Q(a)"
hence "∃x. Q(x)" ..
thus "(∃x. P(x)) ∨ (∃x. Q(x))" ..
qed
qed

-- "La demostración automática es"
lemma ejercicio_7_2c:
assumes "∃x. P(x) ∨ Q(x)"
shows "(∃x. P(x)) ∨ (∃x. Q(x))"
using assms
by auto

text {*
Ejemplo 7.3 (p. 23). Demostrar
⊢ ((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x)) *}

-- "La demostración detallada es"
lemma ejemplo_7_3a:
"((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))"
proof (rule iffI)
assume "(∃x. P(x)) ∨ (∃x. Q(x))"
thus "∃x. P(x) ∨ Q(x)" by (rule ejemplo_7_1a)
next
assume "∃x. P(x) ∨ Q(x)"
thus "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule ejemplo_7_2a)
qed

-- "La demostración automática es"
lemma ejemplo_7_3b:
"((∃x. P(x)) ∨ (∃x. Q(x))) ⟷ (∃x. P(x) ∨ Q(x))"
using assms
by auto

text {*
Ejemplo 8.1 (p. 24). Demostrar
∃x y. P(x,y) ⊢ ∃y x. P(x,y) *}

-- "La demostración detallada es"
lemma ejemplo_8_1a:
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)
then obtain b where "P(a,b)" by (rule exE)
hence "∃x. P(x,b)" by (rule exI)
thus "∃y x. P(x,y)" by (rule exI)
qed

-- "La demostración estructurada es"
lemma ejemplo_8_1b:
assumes "∃x y. P(x,y)"
shows "∃y x. P(x,y)"
proof -
obtain a where "∃y. P(a,y)" using assms ..
then obtain b where "P(a,b)" ..
hence "∃x. P(x,b)" ..
thus "∃y x. P(x,y)" ..
qed

-- "La demostración automática es"
lemma ejemplo_8_1c:
assumes "∃x y. P(x,y)"
shows "∃y x. P(x,y)"
using assms
by auto

text {*
Ejemplo 8.2. Demostrar
∃y x. P(x,y) ⊢ ∃x y. P(x,y) *}

-- "La demostración detallada es"
lemma ejemplo_8_2a:
assumes "∃y x. P(x,y)"
shows "∃x y. P(x,y)"
proof -
obtain b where "∃x. P(x,b)" using assms by (rule exE)
then obtain a where "P(a,b)" by (rule exE)
hence "∃y. P(a,y)" by (rule exI)
thus "∃x y. P(x,y)" by (rule exI)
qed

-- "La demostración estructurada es"
lemma ejemplo_8_2b:
assumes "∃y x. P(x,y)"
shows "∃x y. P(x,y)"
proof -
obtain b where "∃x. P(x,b)" using assms ..
then obtain a where "P(a,b)" ..
hence "∃y. P(a,y)" ..
thus "∃x y. P(x,y)" ..
qed

-- "La demostración estructurada es"
lemma ejemplo_8_2c:
assumes "∃y x. P(x,y)"
shows "∃x y. P(x,y)"
using assms
by auto

text {*
Ejemplo 8.3 (p. 25). Demostrar
⊢ (∃x y. P(x,y)) ⟷ (∃y x. P(x,y)) *}

-- "La demostración detallada es"
lemma ejemplo_8_3a:
"(∃x y. P(x,y)) ⟷ (∃y x. P(x,y))"
proof (rule iffI)
assume "∃x y. P(x,y)"
thus "∃y x. P(x,y)" by (rule ejemplo_8_1a)
next
assume "∃y x. P(x,y)"
thus "∃x y. P(x,y)" by (rule ejemplo_8_2a)
qed

-- "La demostración automática es"
lemma ejemplo_8_3b:
"(∃x y. P(x,y)) ⟷ (∃y x. P(x,y))"
by auto

section {* Reglas de la igualdad *}

text {*
Las reglas básicas de la igualdad son:
· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
*}

text {*
Ejemplo 9 (p. 27). Demostrar
x+1 = 1+x, x+1 > 1 ⟶ x+1 > 0 ⊢ 1+x > 1 ⟶ 1+x > 0
*}

-- "La demostración detallada es"
lemma ejemplo_9a:
assumes "x+1 = 1+x"
"x+1 > 1 ⟶ x+1 > 0"
shows "1+x > 1 ⟶ 1+x > 0"
proof -
show "1+x > 1 ⟶ 1+x > 0" using assms by (rule subst)
qed

-- "La demostración estructurada es"
lemma ejemplo_9b:
assumes "x+1 = 1+x"
"x+1 > 1 ⟶ x+1 > 0"
shows "1+x > 1 ⟶ 1+x > 0"
using assms
by (rule subst)

-- "La demostración automática es"
lemma ejemplo_9c:
assumes "x+1 = 1+x"
"x+1 > 1 ⟶ x+1 > 0"
shows "1+x > 1 ⟶ 1+x > 0"
using assms
by auto

text {*
Ejemplo 10 (p. 27). Demostrar
x = y, y = z ⊢ x = z
*}

-- "La demostración detallada es"
lemma ejemplo_10a:
assumes "x = y"
"y = z"
shows "x = z"
proof -
show "x = z" using assms(2,1) by (rule subst)
qed

-- "La demostración estructurada es"
lemma ejemplo_10b:
assumes "x = y"
"y = z"
shows "x = z"
using assms(2,1)
by (rule subst)

-- "La demostración automática es"
lemma ejemplo_10c:
assumes "x = y"
"y = z"
shows "x = z"
using assms
by auto

text {*
Ejemplo 11 (p. 28). Demostrar
s = t ⊢ t = s
*}

-- "La demostración detallada es"
lemma ejemplo_11a:
assumes "s = t"
shows "t = s"
proof -
have "s = s" by (rule refl)
with assms show "t = s" by (rule subst)
qed

-- "La demostración automática es"
lemma ejemplo_11b:
assumes "s = t"
shows "t = s"
using assms
by auto

end
</source>

Lógica matemática y fundamentos (2017-18)

2018-11-19T07:55:02Z

Jalonso: /* Teorías Isabelle/HOL */

== Relaciones de ejercicios ==

En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.
* '''Relación 1''': Sintaxis y semántica de la lógica proposicional. ([[R1 |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 2''': Deducción natural en lógica proposicional. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 3''': Deducción natural en lógica proposicional(2). ([[R3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R4.thy '''Relación 4''']: Deducción natural proposicional con Isabelle/HOL. ([[R4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Sintaxis y semántica de la Lógica de primer orden. ([[R5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden (II). ([[R6 |Enunciado]] y [[Relación 6 |Solución colaborativa]]).
* [http://www.cs.us.es/~mjoseh/cursos/lmf-17/ejercicios/R7.thy '''Relación 7''']: Deducción natural en lógica de primer orden con Isabelle/HOL. ([[R7 |Enunciado]] y [[Relación 7 |Solución colaborativa]]).
* '''Relación 8''': Tableros semánticos. ([[R8 |Enunciado]] y [[Relación 8 |Solución colaborativa]]).
* '''Relación 9''': Resolución proposicional. ([[R9 |Enunciado]] y [[Relación 9 |Solución colaborativa]]).
* '''Relación 10''': Cuestiones. ([[R10 |Enunciado]] y [[Relación 10 |Solución colaborativa]]).
* '''Relación 11''': Resolución en lógica de primer orden. ([[R11 |Enunciado]] y [[Relación 11 |Solución colaborativa]]).

=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8a''': [[Tema 8a | Deducción natural en lógica de primer orden con Isabelle/HOL]].

Relación 7

2018-07-14T18:48:03Z

Jalonso:

<source lang = "isabelle">
chapter {* R7: Deducción natural en lógica de primer orden *}

theory R7
imports Main
begin

text {*
Demostrar o refutar los siguientes lemas usando sólo las reglas
básicas de deducción natural de la lógica proposicional, de los
cuantificadores y de la igualdad:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
· excluded_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: carmarria
assumes 1: "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof -
{assume 2: "! x. P x"
{fix a
have 3: "P a ⟶ Q a" using 1 by (rule allE)
have 4: "P a" using 2 by (rule allE)
have 5: "Q a" using 3 4 by (rule mp)
}
hence 6: "! x. Q x" by (rule allI)
}
thus "(! x. P x) ⟶ (! x. Q x)" by (rule impI)
qed

joslopjim4

assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof (rule impI)
assume "∀x. P x"
show "∀x. Q x"
proof (rule allI)
fix a
have "P a ⟶ Q a" using assms by (rule allE)
have "P a" using `∀x. P x` by (rule allE)
show "Q a" using `P a ⟶ Q a` `P a` by (rule mp)
qed
qed

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

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

joslopjim4

assumes "∃x. ¬(P x)"
shows "¬(∀x. P x)"
proof (rule ccontr)
assume "¬¬(∀x. P x)"
then have "∀x. P x" by (rule notnotD)
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

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

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

joslopjim4

assumes "∀x. P x"
shows "∀y. P y"
proof (rule allI)
fix a
show "P a" using assms by (rule allE)
qed

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

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

joslopjim4

assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof (rule impI)
assume "∀x. ¬(Q x)"
show "∀x. ¬ (P x)"
proof (rule allI)
fix a
have "¬(Q a)" using `∀x. ¬(Q x)` by (rule allE)
have "P a ⟶ Q a" using assms by (rule allE)
thus "¬(P a)" using `¬(Q a)` by (rule mt)
qed
qed

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

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

joslopjim4

assumes "∀x. P x ⟶ ¬(Q x)"
shows "¬(∃x. P x ∧ Q x)"
proof (rule ccontr)
assume "¬¬(∃x. P x ∧ Q x)"
then have "∃x. P x ∧ Q x" by (rule notnotD)
obtain b where "P b ∧ Q b" using `∃x. P x ∧ Q x` by (rule exE)
have "P b" using `P b ∧ Q b` by (rule conjunct1)
have "Q b" using `P b ∧ Q b` by (rule conjunct2)
have "P b ⟶ ¬(Q b)"
proof -
fix b
show "P b ⟶ ¬(Q b)" using assms by (rule allE)
qed
have "¬(Q b)" using `P b ⟶ ¬(Q b)` `P b` by (rule mp)
show False using `¬(Q b)` `Q b` by (rule notE)
qed

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

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

joslopjim4

assumes "∀x y. P x y"
shows "∀u v. P u v"
proof (rule allI)
fix a
have "∀y. P a y" using assms by (rule allE)
show "∀v. P a v"
proof (rule allI)
fix b
show "P a b" using `∀y. P a y` by (rule allE)
qed
qed

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

lemma ejercicio_7: carmarria
assumes 1: "∃x y. P x y"
shows "∃u v. P u v"
proof -
obtain a where 2: "? y. P a y" using 1 by (rule exE)
obtain b where 3: "P a b" using 2 by (rule exE)
have 4: "? v. P a v" using 3 by (rule exI)
show 5: "? u v. P u v" using 4 by (rule exI)
qed

joslopjim4

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)
obtain b where "P a b" using `∃y. P a y` by (rule exE)
then have "∃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: carmarria
assumes 1: "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
proof -
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)
}
thus "! y. ? x. P x y" by (rule allI)
qed

joslopjim4

assumes "∃x. ∀y. P x y"
shows "∀y. ∃x. P x y"
proof (rule allI)
fix b
obtain a where "∀y. P a y" using assms by (rule exE)
then have "P a b" by (rule allE)
then show "∃x. P x b" by (rule exI)
qed

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

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

joslopjim4

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

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

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

joslopjim4

fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
proof-
have "¬(P a) ∨ P a" by (rule excluded_middle)
thus "∃x. P a ⟶ Q x"
proof
assume "P a"
have "∃x. Q x" using assms `P a` by (rule mp)
obtain b where "Q b" using `∃x. Q x` by (rule exE)
have "P a ⟶ Q b"
proof
assume "P a"
show "Q b" using `Q b` by this
qed
show "∃x. P a ⟶ Q x" using `P a ⟶ Q b` by (rule exI)
next
assume "¬(P a)"
have "P a ⟶ Q a"
proof
assume "P a"
have False using `¬(P a)` `P a` by (rule notE)
thus "Q a" by (rule FalseE)
qed
show "∃x. P a ⟶ Q x" using `P a ⟶ Q a` by (rule exI)
qed
qed

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

lemma ejercicio_11a: carmarria
assumes 1:"(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"
proof-
{fix b
{assume 2: "P b"
have 3: "? x. P x" using 2 by (rule exI)
have 4: "Q a" using 1 3 by (rule mp)
}
hence 5: "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: carmarria
assumes 1: "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"
proof -
have 2: "P b ⟶ Q a" using 1 by (rule allE)
show 3: "? x. P x ⟶ Q a" using 2 by (rule exI)
qed

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

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

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

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

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

lemma ejercicio_15a: carmarria
assumes 1: "∀x y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"
proof -
{assume 2: "? y. P y"
{fix a
have 3: "! y. P y ⟶ Q a" using 1 by (rule allE)
obtain b where 4: "P b" using 2 by (rule exE)
have 5: "P b ⟶ Q a" using 3 by (rule allE)
have 6: "Q a" using 5 4 by (rule mp)
}
hence 7: "! 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: carmarria
assumes 1: "¬(∀x. ¬(P x))"
shows "∃x. P x"
proof -
{assume 2: "¬(? x. P x)"
{fix b
{assume 3: "P b"
have 4: "? x. P x" using 3 by (rule exI)
have 5: False using 2 4 by (rule notE)
}
hence 6: "¬(P b)" by (rule notI)
}
hence 7: "! x. ¬(P x)" by (rule allI)
have 8: False using 1 7 by (rule notE)
}
hence 9: "¬¬(? x. P x)" by (rule notI)
show "? x. P x" using 9 by (rule notnotD)
qed

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

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

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

lemma ejercicio_18a: carmarria
assumes 1: "∃x. P x"
shows "¬(∀x. ¬(P x))"
proof-
{assume 2: "! x. ¬(P x)"
obtain a where 3: "P a" using 1 by (rule exE)
have 4: "¬(P a)" using 2 by (rule allE)
have 5: False using 4 3 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: carmarria
assumes 1: "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"
proof -
{fix b
{assume 2: "P a"
have 3: "! x. Q x" using 1 2 by (rule mp)
have 4: "Q b" using 3 by (rule allE)
}
hence 5: "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: carmarria
assumes 1: "∀x y z. R x y ∧ R y z ⟶ R x z" and
2: "∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"
proof -
{fix a
{fix b
{assume 3: "R a b"
have 4: "! y z. R a y & R y z ⟶ R a z" using 1 by (rule allE)
have 5: "! z. R a b & R b z ⟶ R a z" using 4 by (rule allE)
have 6: "R a b & R b a ⟶ R a a" using 5 by (rule allE)
have 7: "¬(R a a)" using 2 by (rule allE)
have 8: "¬(R a b & R b a)" using 6 7 by (rule mt)
{assume 9: "R b a"
have 10: "R a b & R b a" using 3 9 by (rule conjI)
have 11: False using 8 10 by (rule notE)
}
hence 12: "¬(R b a)" by (rule notI)
}
hence 13: "R a b ⟶ ¬(R b a)" by (rule impI)
}
hence 14: "! 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: carmarria
assumes 1: "∀x. P x ∨ Q x" and
2: "∃x. ¬(Q x)" and
3: "∀x. R x ⟶ ¬(P x)"
shows "∃x. ¬(R x)"
proof -
obtain a where 4: "¬(Q a)" using 2 by (rule exE)
have 5: "P a | Q a" using 1 by (rule allE)
moreover {assume 6: "P a"
have 7: "¬¬(P a)" using 6 by (rule notnotI)
have 8: "R a ⟶ ¬(P a)" using 3 by (rule allE)
have 9: "¬(R a)" using 8 7 by (rule mt)
have 10: "? x. ¬(R x)" using 9 by (rule exI)
}
moreover {assume 10: "Q a"
have 11: False using 4 10 by (rule notE)
have 12: "? x. ¬(R x)" using 11 by (rule FalseE)
}
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: carmarria
assumes 1: "∀x. P x ⟶ Q x ∨ R x" and
2: "¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"
proof -
{fix a
{assume 3: "P a"
have 4: "P a ⟶ Q a | R a" using 1 by (rule allE)
have 5: "Q a | R a" using 4 3 by (rule mp)
moreover {assume 6: "Q a"
}
moreover {assume 7: "R a"
have 8: "P a & R a" using 3 7 by (rule conjI)
have 9: "? x. P x & R x" using 8 by (rule exI)
have 10: False using 2 9 by (rule notE)
have 11: "Q a" using 10 by (rule FalseE)
}
ultimately have 12: "Q a" by (rule disjE)
}
hence 13: "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: carmarria
assumes 1: "∃x y. R x y ∨ R y x"
shows "∃x y. R x y"
proof -
obtain a where 2: "? y. R a y | R y a" using 1 by (rule exE)
obtain b where 3: "R a b | R b a" using 2 by (rule exE)
moreover {assume 4: "R a b"
have 5: "? y. R a y" using 4 by (rule exI)
have 6: "? x y. R x y" using 5 by (rule exI)
}
moreover {assume 7: "R b a"
have 8: "? y. R b y" using 7 by (rule exI)
have 9: "? x y. R x y" using 8 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: carmarria
"(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
proof -
{assume 1: "? x. ! y. P x y"
{fix b
obtain a where 2: "! y. P a y" using 1 by (rule exE)
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: carmarria
"(∀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 6: "(? x. P x) ⟶ Q" by (rule impI)
}
next
{assume 7: "(? x. P x) ⟶ Q"
{fix a
{assume 8: "P a"
have 9: "? x. P x" using 8 by (rule exI)
have 10: Q using 7 9 by (rule mp)
}
hence 11: "P a ⟶ Q" by (rule impI)
}
thus 12: "! 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: carmarria
"((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
proof (rule iffI)
{assume 1: "((! x. P x) ∧ (! x. Q x))"
have 2: "! x. P x" using 1 by (rule conjunct1)
have 3: "! x. Q x" using 1 by (rule conjunct2)
{fix a
have 4: "P a" using 2 by (rule allE)
have 5: "Q a" using 3 by (rule allE)
have 6: "P a & Q a" using 4 5 by (rule conjI)
}
thus 7: "! x. P x & Q x" by (rule allI)
}
next
{assume 8: "! x. P x & Q x"
{fix a
have 9: "P a & Q a" using 8 by (rule allE)
have 10: "P a" using 9 by (rule conjunct1)
}
hence 11: "! x. P x" by (rule allI)
{fix a
have 12: "P a & Q a" using 8 by (rule allE)
have 13: "Q a" using 12 by (rule conjunct2)
}
hence 14: "! x. Q x" by (rule allI)
show "(! x. P x) & (! x. Q x)" using 11 14 by (rule conjI)
}
qed

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

lemma ejercicio_27a: carmarria
"((∀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"
{fix a
have 3: "P a" using 2 by (rule allE)
have 4: "P a | Q a" using 3 by (rule disjI1)
}
hence 5: "! x. P x | Q x" by (rule allI)
}
moreover {assume 6: "! x. Q x"
{fix a
have 7: "Q a" using 6 by (rule allE)
have 8:"P a | Q a" using 7 by (rule disjI2)
}
hence 9: "! x. P x | Q x" by (rule allI)
}
ultimately show "! x. P x | Q x" by (rule disjE)
}
next
{assume 10: "! x. P x | Q x"
oops

(* Si tomamos el universo {1,2}, P(x): x=1, Q(x): x=2. Tenemos que es verdad que
(∀x. x=1 ∨ x=2), pero no se cumple ni (∀x. x=1) ni (∀x. x=2), por lo tanto el bicondicional es falso *)

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

lemma ejercicio_28a: carmarria
"((∃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 14: "(? x. P x) | (? x. Q x)" using 13 by (rule disjI1)
}
moreover {assume 15: "Q a"
have 16: "? x. Q x" using 15 by (rule exI)
have 17: "(? x. P x) | (? x. Q x)" using 16 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: carmarria
"(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops
(* Si tomamos el universo {1,2} y P(x,y): x=y, entonces tenemos que (∀x. ∃y. x=y) pero no se cumple
que (∃y. ∀x. x=y) *)

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

lemma ejercicio_30a: carmarria
"(¬(∀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 6: "¬(¬P a)" by (rule notI)
have 7: "P a" using 6 by (rule notnotD)
}
hence 8: "! x. P x" by (rule allI)
have 9: False using 1 8 by (rule notE)
}
hence 10: "¬¬(? x. ¬(P x))" by (rule notI)
show "? x. ¬(P x)" using 10 by (rule notnotD)
}
next
{assume 11: "? x. ¬P x"
obtain a where 12: "¬P a" using 11 by (rule exE)
{assume 13: "! x. P x"
have 14: "P a" using 13 by (rule allE)
have 15: False using 12 14 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: carmarria
assumes 1: "P a"
shows "∀x. x = a ⟶ P x"
proof -
{fix b
{assume 2: "b = a"
have 3: "a = b" using 2 by (rule sym)
have 4: "P b" using 3 1 by (rule subst)
}
hence 5: "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: carmarria
fixes R :: "'c ⇒ 'c ⇒ bool"
assumes 1: "∃x y. R x y ∨ R y x" and
2: "¬(∃x. R x x)"
shows "∃(x::'c) y. x ≠ y"
proof -
obtain a where 3: "? y. R a y | R y a" using 1 by (rule exE)
obtain b where 4: "R a b | R b a" using 3 by (rule exE)
{assume 5: "a = b"
have 6: "R a b | R b a" using 4 by this
moreover {assume 7: "R a b"
have 8: "R b b" using 5 7 by (rule subst)
}
moreover {assume 9: "R b a"
have 10: "R b b" using 5 9 by (rule subst)
}
ultimately have 11: "R b b" by (rule disjE)
have 12: "? x. R x x" using 11 by (rule exI)
have 13: False using 2 12 by (rule notE)
}
hence 14: " a ≠ b " by (rule notI)
have 15: "? y. a ≠ y" using 14 by (rule exI)
show "? x y. (x ≠ y)" (* using 15 by (rule exI) *)
oops

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: carmarria
assumes 1: "∀x. P a x x" and
2: "∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "P (f a) a (f a)"
proof -
have 3: "P a a a" using 1 by (rule allE)
have 4: "! y z. P a y z ⟶ P (f a) y (f z)" using 2 by (rule allE)
have 5: "! z. P a a z ⟶ P (f a) a (f z)" using 4 by (rule allE)
have 6: "P a a a ⟶ P (f a) a (f a)" using 5 by (rule allE)
show "P (f a) a (f a)" using 6 3 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: carmarria
assumes 1: "∀x. P a x x" and
2: "∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
proof -
have 3: "P a (f a) (f a)" using 1 by (rule allE)
have 4: "! y z. P a y z ⟶ P (f a) y (f z)" using 2 by (rule allE)
have 5: "! z. P a (f a) z ⟶ P (f a) (f a) (f z)" using 4 by (rule allE)
have 6: "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" using 5 by (rule allE)
have 7: "P (f a) (f a) (f (f a))" using 6 3 by (rule mp)
show 8: "? z. P (f a) z (f (f a))" using 7 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: carmarria
assumes 1: "∀y. Q a y" and
2: "∀x y. Q x y ⟶ Q (s x) (s y)"
shows "∃z. Q a z ∧ Q z (s (s a))"
proof-
have 3: "! y. Q a y ⟶ Q (s a) (s y)" using 2 by (rule allE)
have 4: "Q a (s a) ⟶ Q (s a) (s (s a))" using 3 by (rule allE)
have 5: "Q a (s a)" using 1 by (rule allE)
have 6: "Q (s a) (s (s a))" using 4 5 by (rule mp)
have 7: "Q a (s a) & Q (s a) (s (s a))" using 5 6 by (rule conjI)
show "? z. Q a z & Q z (s (s a))" using 7 by (rule exI)
qed

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

lemma ejercicio_36a: carmarria
assumes 1: "x = f x" and
2: "odd (f x)"
shows "odd x"
proof -
have 3: "f x = x" using 1 by (rule sym)
show "odd x" using 3 2 by (rule subst)
qed

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

lemma ejercicio_37a: carmarria
assumes 1: "x = f x" and
2: "triple (f x) (f x) x"
shows "triple x x x"
proof -
have 3: "f x = x" using 1 by (rule sym)
show 4: "triple x x x" using 3 2 by (rule subst)
qed

end

</source>

R7

2018-07-14T18:47:46Z

Jalonso:

Relación 4

2018-07-14T18:47:22Z

Jalonso:

<source lang = "isabelle">

chapter {* R4: Deducción natural proposicional *}

theory R4
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: josrodjim2 carmarria inmbenber marmedmar3
assumes 1: "p ⟶ q" and
2: "p"
shows "q"

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

lemma ej_1: joslopjim4 marcabcar1
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: josrodjim2 carmarria inmbenber marmedmar3
assumes 1: "p ⟶ q" and
2: "q ⟶ r" and
3: "p"
shows "r"

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

lemma ej_2: joslopjim4 marcabcar1
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
proof -
have "q" using `p⟶q` `p` by (rule mp)
show "r" using `q⟶r` `q` by (rule mp)
qed

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

lemma ejercicio_3: josrodjim2 carmarria inmbenber marmedmar3
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p ⟶ q" and
3: "p"
shows "r"

proof-
have 4: "q" using 2 3 by (rule mp)
have 5: "(q ⟶ r)" using 1 3 by (rule mp)
show "r" using 5 4 by (rule mp)

qed

lemma ej_3: joslopjim4 marcabcar1
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
proof -
have "q" using `p⟶q` `p` by (rule mp)
have "q⟶r" using `p ⟶ (q ⟶ r)` `p` by (rule mp)
show "r" using `q⟶r` `q` by (rule mp)
qed

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

lemma ejercicio_4: josrodjim2
assumes 1: "p ⟶ q" and
2: "q ⟶ r"
shows "p ⟶ r"

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

oops

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

lemma ejercicio_4:marmedmar3
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
proof
assume "p"
with assms(1) have "q" by (rule mp)
with assms(2) show "r" by (rule mp)
qed

lemma ej_4: joslopjim4 marcabcar1
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"
proof (rule impI)
assume "p"
have "q" using assms(1) `p` by (rule mp)
show "r" using assms(2) `q` by (rule mp)
qed

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

lemma ejercicio_5: josrodjim2 (NO DA ERROR, PERO SI ALERTA)
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"

proof -

{ assume 2: "q"
{assume 3: "p"
have 4: "q ⟶r" using 1 3 by (rule mp)
have 5: "r" using 4 2 by (rule mp)}
hence 6: "p⟶r" using 3 5 by (rule impI)}
hence 7: "q ⟶ (p ⟶ r)" using 2 6 by (rule impI)
show "q ⟶ (p ⟶ r)" using 7 by this

oops

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

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

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

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

lemma ejercicio_5: marmedmar3
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof
assume "q"
show "(p ⟶ r)"
proof
assume "p"
with assms(1) have "(q ⟶ r)" by (rule mp)
thus "r" using `q` by (rule mp)
qed
qed

lemma ej_5: joslopjim4 marcabcar1
assumes "p ⟶ (q ⟶ r)"
shows "q ⟶ (p ⟶ r)"
proof (rule impI)
assume "q"
show "p⟶r"
proof (rule impI)
assume "p"
have "q⟶r" using `p ⟶ (q ⟶ r)` `p` by (rule mp)
show "r" using `q⟶r` `q` by (rule mp)
qed
qed

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

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

proof-

{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 7: "p⟶r" using 3 6 by (rule impI)}
hence 8: "(p ⟶ q) ⟶ (p ⟶ r)" using 2 7 by (rule impI)
show "(p ⟶ q) ⟶ (p ⟶ r)" using 8 by this
oops

lemma ejercicio_6: carmarria, inmbenber
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof -
{assume 2: "p ⟶ q"
{assume 3: "p"
have 4: "q" using 2 3 by (rule mp)
have 5: "q ⟶ r" using 1 3 by (rule mp)
have 6: "r" using 5 4 by (rule mp)
}
hence 7: "p ⟶ r" by (rule impI)
}
thus "(p ⟶ q) ⟶ (p ⟶ r)" by (rule impI)
qed

lemma ejercicio_6:marmedmar3
assumes 1: "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof
assume 2: "(p ⟶ q)"
show "(p ⟶ r)"
proof
assume 3: "p"
have 4: "q" using 2 3 by (rule mp)
have 5: "(q ⟶ r)" using 1 3 by (rule mp)
show "r" using 5 4 by (rule mp)
qed
qed

lemma ej_6: joslopjim4 marcabcar1
assumes "p ⟶ (q ⟶ r)"
shows "(p ⟶ q) ⟶ (p ⟶ r)"
proof (rule impI)
assume "(p⟶q)"
show "p⟶r"
proof (rule impI)
assume "p"
have "q⟶r" using `p ⟶ (q ⟶ r)` `p` by (rule mp)
have "q" using `p⟶q` `p` by (rule mp)
show "r" using `q⟶r` `q` by (rule mp)
qed
qed

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

lemma ejercicio_7: (NO SE QUE ESTA MAL)
assumes "p"
shows "q ⟶ p"

proof -

{ assume 2: "q"
have 3: "p" using 1
}
hence 4: "q⟶p" using 2 3 by (rule impI)

show "q⟶p" using 4 by this

oops

lemma ejercicio_7: carmarria, inmbenber
assumes 1: "p"
shows "q ⟶ p"
proof -
{assume 2: "q"
have 3: "p" using 1 by this}
thus "q ⟶ p" by (rule impI)
qed

lemma ejercicio_7:marmedmar3
assumes "p"
shows "q ⟶ p"
proof
assume "q"
show "p" using assms(1) by this
qed

lemma ej_7: joslopjim4 marcabcar1
assumes "p"
shows "q ⟶ p"
proof (rule impI)
assume "q"
show "p" using assms by this
qed

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

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

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

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

lemma ej_8: joslopjim4 marcabcar1
shows "p⟶(q⟶p)"
proof (rule impI)
assume "p"
show "q⟶p"
proof (rule impI)
assume "q"
show "p" using `p` by this
qed
qed

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

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

lemma ejercicio_9: marmedmar3
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof
assume "(q ⟶ r)"
show "(p ⟶ r)"
proof
assume "p"
with `(p ⟶ q)` have "q" by (rule mp)
with `(q ⟶ r)` show "r" by (rule mp)
qed
qed

lemma ej_9: joslopjim4 marcabcar1
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"
proof (rule impI)
assume "q⟶r"
show "p⟶r"
proof (rule impI)
assume "p"
have "q" using `p⟶q` `p` by (rule mp)
show "r" using `q⟶r` `q` by (rule mp)
qed
qed

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

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

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

lemma ejercicio_10: marmedmar3
assumes 1: "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof
assume 2: "r"
show "(q ⟶ (p ⟶ s))"
proof
assume 3: "q"
show "(p ⟶ s)"
proof
assume 4: "p"
have 5: "(q ⟶ (r ⟶ s))" using 1 4 by (rule mp)
have 6: "(r ⟶ s)" using 5 3 by (rule mp)
show "s" using 6 2 by (rule mp)
qed
qed
qed

lemma ej_10: joslopjim4 marcabcar1
assumes "p ⟶ (q ⟶ (r ⟶ s))"
shows "r ⟶ (q ⟶ (p ⟶ s))"
proof (rule impI)
assume "r"
show "q⟶(p⟶s)"
proof (rule impI)
assume "q"
show "p⟶s"
proof (rule impI)
assume "p"
have "q ⟶ (r ⟶ s)" using `p ⟶ (q ⟶ (r ⟶ s))` `p` by (rule mp)
have "r⟶s" using `q ⟶ (r ⟶ s)` `q` by (rule mp)
show "s" using `r-->s` `r` by (rule mp)
qed
qed
qed

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

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

lemma ejercicio_11: marmedmar3
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume 1: "(p ⟶ (q ⟶ r))"
show "((p ⟶ q) ⟶ (p ⟶ r))"
proof
assume 2: "(p ⟶ q)"
show "(p ⟶ r)"
proof
assume 3: "p"
have 4: "(q ⟶ r)" using 1 3 by (rule mp)
have 5: "q" using 2 3 by (rule mp)
show "r" using 4 5 by (rule mp)
qed
qed
qed

lemma ej_11: joslopjim4 marcabcar1
shows "(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"
proof (rule impI)
assume "p⟶(q⟶r)"
show "(p⟶q)⟶(p⟶r)"
proof (rule impI)
assume "p⟶q"
show "p⟶r"
proof (rule impI)
assume "p"
have "q" using `p⟶q` `p` by (rule mp)
have "q⟶r" using `p⟶(q⟶r)` `p` by (rule mp)
show "r" using `q⟶r` `q` by (rule mp)
qed
qed
qed

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

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

lemma ej_12: joslopjim4 marcabcar1
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume "p"
show "q⟶r"
proof (rule impI)
assume "q"
have "p⟶q"
proof (rule impI)
assume "p"
show "q" using `q` by this
qed
show "r" using `(p ⟶ q) ⟶ r` `p⟶q` by (rule mp)
qed
qed

section {* Conjunciones *}

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

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

proof-
show "p \<and> q" using assms(1) assms(2) by (rule conjI)
qed

lemma ej_13: joslopjim4 marcabcar1
assumes "p"
"q"
shows "p ∧ q"
proof-
show "p∧q" using `p` `q` by (rule conjI)
qed

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

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

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

lemma ej_14: joslopjim4 marcabcar1
assumes "p ∧ q"
shows "p"
proof -
show "p" using assms by (rule conjunct1)
qed

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

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

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

lemma ej_15: joslopjim4 marcabcar1
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: carmarria marmedmar3
assumes 1: "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof -
have 2: "q \<and> r" using 1 by (rule conjunct2)
have 3: p using 1 by (rule conjunct1)
have 4: q using 2 by (rule conjunct1)
have 5: r using 2 by (rule conjunct2)
have 6: "p \<and> q" using 3 4 by (rule conjI)
show "(p \<and> q) \<and> r" using 6 5 by (rule conjI)
qed

lemma ej_16: joslopjim4 marcabcar1
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof-
have "p" using assms by (rule conjunct1)
have "q∧r" using assms by (rule conjunct2)
have "q" using `q∧r` by (rule conjunct1)
have "r" using `q∧r` by (rule conjunct2)
have "p∧q" using `p` `q` by (rule conjI)
show "(p∧q)∧r" using `p∧q` `r` 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 (rule conjI)
have "p ∧ q" using assms ..
thus "p" ..
next
show "q ∧ r"
proof (rule conjI)
have "p ∧ q" using assms ..
thus "q" ..
next
show "r" using assms ..
qed
qed

lemma ejercicio_17: carmarria marmedmar3
assumes 1:"(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof-
have 2:"p \<and> q" using 1 by (rule conjunct1)
have 3: r using 1 by (rule conjunct2)
have 4: p using 2 by (rule conjunct1)
have 5: q using 2 by (rule conjunct2)
have 6: "q \<and> r" using 5 3 by (rule conjI)
show "p \<and> (q \<and> r)" using 4 6 by (rule conjI)
qed

lemma ej_17: joslopjim4 marcabcar1
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"
proof-
have "p∧q" using assms by (rule conjunct1)
have "r" using assms by (rule conjunct2)
have "p" using `p∧q` by (rule conjunct1)
have "q" using `p∧q` by (rule conjunct2)
have "q∧r" using `q` `r` by (rule conjI)
show "p∧(q∧r)" using `p` `q∧r` by (rule conjI)
qed

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

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

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

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

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

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

lemma ejercicio_19: marmedmar3
assumes 1: "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof
have 2: "(p ⟶ q)" using assms by (rule conjunct1)
have 3: "(p ⟶ r)" using assms by (rule conjunct2)
assume 4: "p"
with `(p ⟶ q)` have 5: "q" by (rule mp)
have 6: "r" using 3 4 by (rule mp)
show "q ∧ r" using 5 6 by (rule conjI)
qed

lemma ej_19: joslopjim4 marcabcar1
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"
proof (rule impI)
assume "p"
have "p⟶q" using assms by (rule conjunct1)
have "q" using `p⟶q` `p` by (rule mp)
have "p⟶r" using assms by (rule conjunct2)
have "r" using `p⟶r` `p` by (rule mp)
show "q∧r" using `q` `r` by (rule conjI)
qed

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

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

lemma ej_20: joslopjim4 marcabcar1
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof-
have "p⟶q"
proof
assume "p"
have "q∧r" using assms `p` by (rule mp)
show "q" using `q∧r` by (rule conjunct1)
qed
have "p⟶r"
proof
assume "p"
have "q∧r" using assms `p` by (rule mp)
show "r" using `q∧r` by (rule conjunct2)
qed
show "(p⟶q)∧(p⟶r)" using `p⟶q` `p⟶r` by (rule conjI)
qed

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

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

lemma ejercicio_21: marmedmar3
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
hence "p" by (rule conjunct1)
with assms have "(q ⟶ r)" by (rule mp)
have "q" using `p ∧ q` by (rule conjunct2)
with `(q ⟶ r)` show "r" by (rule mp)
qed

lemma ej_21: joslopjim4 marcabcar1
assumes "p ⟶ (q ⟶ r)"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume "p∧q"
have "p" using `p∧q` by (rule conjunct1)
have "q" using `p∧q` by (rule conjunct2)
have "q⟶r" using assms `p` by (rule mp)
show "r" using `q⟶r` `q` by (rule mp)
qed

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

lemma ejercicio_22: carmarria
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof -
{assume p
{assume q
have "p \<and> q" using `p` `q` by (rule conjI)
have r using assms(1) `p \<and> q` by (rule mp)
}
hence "q ⟶ r" by (rule impI)
}
thus "p ⟶ (q ⟶ r)" by (rule impI)
qed

lemma ejercicio_22: marmedmar3
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof
assume "p"
show "(q ⟶ r)"
proof
assume "q"
with `p` have "p ∧ q" by (rule conjI)
with assms show "r" by (rule mp)
qed
qed

lemma ej_22: joslopjim4 marcabcar1
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof (rule impI)
assume "p"
show "q⟶r"
proof (rule impI)
assume "q"
have "p∧q" using `p` `q` by (rule conjI)
show "r" using assms `p∧q` by (rule mp)
qed
qed

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

lemma ejercicio_23: carmarria
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof -
{assume "p \<and> q"
{assume p
have q using `p \<and> q` by (rule conjunct2)
}
hence "p ⟶ q" by (rule impI)
have r using assms(1) `p ⟶ q` by (rule mp)
}
thus "p \<and> q ⟶ r" by (rule impI)
qed

lemma ejercicio_23: marmedmar3
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof
assume "p ∧ q"
have "p" using `p ∧ q` by (rule conjunct1)
have "q" using `p ∧ q` by (rule conjunct2)
hence "(p ⟶ q)" by (rule impI)
with assms show "r" by (rule mp)
qed

lemma ej_23: joslopjim4 marcabcar1
assumes "(p ⟶ q) ⟶ r"
shows "p ∧ q ⟶ r"
proof (rule impI)
assume "p∧q"
have "p⟶q"
proof
assume "p"
show "q" using `p∧q` by (rule conjunct2)
qed
show "r" using assms `p⟶q` by (rule mp)
qed

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

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

lemma ejercicio_24: marmedmar3
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof
assume "(p ⟶ q)"
have "(q ⟶ r)" using assms by (rule conjunct2)
have "p" using assms by (rule conjunct1)
with `(p ⟶ q)` have "q" by (rule mp)
with `(q ⟶ r)` show "r" by (rule mp)
qed

lemma ej_24: joslopjim4 marcabcar1
assumes "p ∧ (q ⟶ r)"
shows "(p ⟶ q) ⟶ r"
proof (rule impI)
assume "p⟶q"
have "p" using assms by (rule conjunct1)
have "q⟶r" using assms by (rule conjunct2)
have "q" using `p⟶q` `p` by (rule mp)
show "r" using `q⟶r` `q` by (rule mp)
qed

section {* Disyunciones *}

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

lemma ejercicio_25: carmarria
assumes "p"
shows "p ∨ q"
proof -
show "p | q" using assms(1) by (rule disjI1)
qed

lemma ej_25: joslopjim4 marcabcar1
assumes "p"
shows "p ∨ q"
proof (rule disjI1)
show "p" using assms by this
qed

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

lemma ejercicio_26: carmarria
assumes "q"
shows "p ∨ q"
proof -
show "p | q" using assms(1) by (rule disjI2)
qed

lemma ej_26: joslopjim4 marcabcar1
assumes "q"
shows "p ∨ q"
proof (rule disjI2)
show "q" using assms by this
qed

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

lemma ejercicio_27: carmarria
assumes "p ∨ q"
shows "q ∨ p"
proof -
have "p | q" using assms(1) by this
moreover
{assume p
have "q | p" using `p` by (rule disjI2)
}
moreover
{assume q
have "q | p" using `q` by (rule disjI1)
}
ultimately show "q | p" by (rule disjE)
qed

lemma ej_27: joslopjim4 marcabcar1
assumes "p ∨ q"
shows "q ∨ p"
using assms
proof
assume "p"
then show "q∨p" by(rule disjI2)
next
assume "q"
show "q∨p" using `q` by(rule disjI1)
qed

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

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

lemma ej_28: joslopjim4 marcabcar1
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof (rule impI)
assume "p∨q"
show "p∨r"
using `p∨q`
proof
assume "p"
show "p∨r" using `p` by (rule disjI1)
next
assume "q"
have "r" using assms `q` by (rule mp)
show "p∨r" using `r` by (rule disjI2)
qed
qed

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

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

lemma ej_29: joslopjim4
assumes "p ∨ p"
shows "p"
proof (rule ccontr)
assume "¬p"
show False
using assms
proof
assume "p"
show False using `¬p` `p` by (rule notE)
next
assume "p"
show False using `¬p` `p` by (rule notE)
qed
qed

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

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

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

lemma ej_30: joslopjim4 marcabcar1
assumes "p"
shows "p ∨ p"
proof (rule disjI1)
show "p" using assms by this
qed

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

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

lemma ej_31: joslopjim4 marcabcar1
assumes "p ∨ (q ∨ r)"
shows "(p ∨ q) ∨ r"
using assms
proof
assume "p"
have "p∨q" using `p` by (rule disjI1)
thus "(p ∨ q) ∨ r" by (rule disjI1)
next
assume "q∨r"
show "(p ∨ q) ∨ r"
using `q∨r`
proof
assume "q"
have "p∨q" using `q` by (rule disjI2)
show "(p ∨ q) ∨ r" using `p∨q` by (rule disjI1)
next
assume "r"
show "(p ∨ q) ∨ r" using `r` by (rule disjI2)
qed
qed

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

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

lemma ej_32: joslopjim4 marcabcar1
assumes "(p ∨ q) ∨ r"
shows "p ∨ (q ∨ r)"
using assms
proof
assume "p∨q"
show "p ∨ (q ∨ r)"
using `p∨q`
proof
assume "p"
show "p ∨ (q ∨ r)" using `p` by (rule disjI1)
next
assume "q"
have "q∨r" using `q` by (rule disjI1)
show "p ∨ (q ∨ r)" using `q∨r` by (rule disjI2)
qed
next
assume "r"
have "q∨r" using `r` by (rule disjI2)
show "p ∨ (q ∨ r)" using `q∨r` by (rule disjI2)
qed

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

lemma ejercicio_33: carmarria
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)
moreover {assume 4: q
have 5: "p & q" using 2 4 by (rule conjI)
have 6: "(p & q) | (p & r)" using 5 by (rule disjI1)
}
moreover {assume 7: r
have 8: "p & r" using 2 7 by (rule conjI)
have 9: "(p & q) | (p & r)" using 8 by (rule disjI2)
}
ultimately show "(p & q) | (p & r)" by (rule disjE)
qed

lemma ej_33: joslopjim4 marcabcar1
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof-
have "p" using assms by (rule conjunct1)
have "q∨r" using assms by (rule conjunct2)
show "(p ∧ q) ∨ (p ∧ r)"
using `q∨r`
proof (rule disjE)
assume "q"
have "p∧q" using `p` `q` by (rule conjI)
show "(p ∧ q) ∨ (p ∧ r)" using `p∧q` by (rule disjI1)
next
assume "r"
have "p∧r" using `p` `r` by (rule conjI)
show "(p ∧ q) ∨ (p ∧ r)" using `p∧r` by (rule disjI2)
qed
qed

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

lemma ejercicio_34: carmarria
assumes 1: "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
proof -
have "(p & q) | (p & r)" using 1 by this
moreover {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)
have 6: "p & (q | r)" using 3 5 by (rule conjI)
}
moreover {assume 7: "p & r"
have 8: p using 7 by (rule conjunct1)
have 9: r using 7 by (rule conjunct2)
have 10: "q | r" using 9 by (rule disjI2)
have 11: "p & (q | r)" using 8 10 by (rule conjI)
}
ultimately show "p & (q | r)" by (rule disjE)
qed

lemma ej_34: joslopjim4 marcabcar1
assumes "(p ∧ q) ∨ (p ∧ r)"
shows "p ∧ (q ∨ r)"
using assms
proof
assume "p∧q"
have "p" using `p∧q` by (rule conjunct1)
have "q" using `p∧q` by (rule conjunct2)
have "q∨r" using `q` by (rule disjI1)
show "p∧(q∨r)" using `p` `q∨r` by (rule conjI)
next
assume "p∧r"
have "p" using `p∧r` by (rule conjunct1)
have "r" using `p∧r` by (rule conjunct2)
have "q∨r" using `r` by (rule disjI2)
show "p∧(q∨r)" using `p` `q∨r` by (rule conjI)
qed

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

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

lemma ej_35: joslopjim4 marcabcar1
assumes "p ∨ (q ∧ r)"
shows "(p ∨ q) ∧ (p ∨ r)"
using assms
proof (rule disjE)
assume "p"
have "p∨q" using `p` by (rule disjI1)
have "p∨r" using `p` by (rule disjI1)
show "(p ∨ q) ∧ (p ∨ r)" using `p∨q` `p∨r` by (rule conjI)
next
assume "q∧r"
have "q" using `q∧r` by (rule conjunct1)
have "r" using `q∧r` by (rule conjunct2)
have "p∨q" using `q` by (rule disjI2)
have "p∨r" using `r` by (rule disjI2)
show "(p ∨ q) ∧ (p ∨ r)" using `p∨q` `p∨r` by (rule conjI)
qed

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

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

lemma ej_36: joslopjim4 marcabcar1
assumes "(p ∨ q) ∧ (p ∨ r)"
shows "p ∨ (q ∧ r)"
proof-
have "p∨q" using assms by (rule conjunct1)
have "p∨r" using assms by (rule conjunct2)
show "p∨(q ∧ r)"
using `p∨r`
proof
assume "p"
show "p∨(q ∧ r)" using `p` by (rule disjI1)
next
assume "r"
show "p∨(q ∧ r)"
using `p∨q`
proof
assume "p"
show "p∨(q ∧ r)" using `p` by (rule disjI1)
next
assume "q"
have "q∧r" using `q` `r` by (rule conjI)
show "p∨(q ∧ r)" using `q∧r` by (rule disjI2)
qed
qed
qed

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

lemma ejercicio_37: carmarria
assumes 1: "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof -
have 2: "p ⟶ r" using 1 by (rule conjunct1)
have 3: "q ⟶ r" using 1 by (rule conjunct2)
{assume 4: "p | q"
moreover {assume 5: p
have 6: r using 2 5 by (rule mp)
}
moreover {assume 7: q
have 8: r using 3 7 by (rule mp)
}
ultimately have r by (rule disjE)
}
thus "p | q ⟶ r" by (rule impI)
qed

lemma ej_37: joslopjim4 marcabcar1
assumes "(p ⟶ r) ∧ (q ⟶ r)"
shows "p ∨ q ⟶ r"
proof (rule impI)
assume "p∨q"
have "p⟶r" using assms by (rule conjunct1)
have "q⟶r" using assms by (rule conjunct2)
show "r"
using `p∨q`
proof
assume "p"
show "r" using `p⟶r` `p` by (rule mp)
next
assume "q"
show "r" using `q⟶r` `q` by (rule mp)
qed
qed

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

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

lemma ej_38: joslopjim4 marcabcar1
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof-
have "p⟶r"
proof (rule impI)
assume "p"
have "p∨q" using `p` by (rule disjI1)
show "r" using assms `p∨q` by (rule mp)
qed
have "q⟶r"
proof (rule impI)
assume "q"
have "p∨q" using `q` by (rule disjI2)
show "r" using assms `p∨q` by (rule mp)
qed
show "(p ⟶ r) ∧ (q ⟶ r)" using `p⟶r` `q⟶r` by (rule conjI)
qed

section {* Negaciones *}

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

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

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

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

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

lemma ej_40: joslopjim4 marcabcar1
assumes "¬p"
shows "p ⟶ q"
proof (rule impI)
assume "p"
show "q" using assms `p` by (rule notE)
qed

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

lemma ejercicio_41: carmarria
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof -
{assume 2: "~q"
have 3: "~p" using 1 2 by (rule mt)
}
thus 4: "~q ⟶ ~p" by (rule impI)
qed

lemma ej_41: joslopjim4 marcabcar1
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof (rule impI)
assume "¬q"
show "¬p" using assms `¬q` by (rule mt)
qed

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

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

lemma ej_42: joslopjim4 marcabcar1
assumes "p∨q"
"¬q"
shows "p"
using assms(1)
proof
assume "p"
show "p" using `p` by this
next
assume "q"
show "p" using assms(2) `q` by (rule notE)
qed

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

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

lemma ej_43: joslopjim4 marcabcar1
assumes "p ∨ q"
"¬p"
shows "q"
using assms(1)
proof
assume "p"
show "q" using assms(2) `p` by (rule notE)
next
assume "q"
show "q" using `q` by this
qed

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

lemma ejercicio_44: carmarria
assumes 1: "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof -
have "p | q" using 1 by this
moreover {assume 2: p
{assume 3:"~p & ~q"
have 4: "~p" using 3 by (rule conjunct1)
have 5: False using 4 2 by (rule notE)
}
hence 6: "~(~p & ~q)" by (rule notI)
}
moreover {assume 7: q
{assume 8: "~p & ~q"
have 9: "~q" using 8 by (rule conjunct2)
have 10: False using 9 7 by (rule notE)
}
hence 11: "~(~p & ~q)" by (rule notI)
}
ultimately show "~(~p & ~q)" by (rule disjE)
qed

lemma ej_44: joslopjim4 marcabcar1
assumes "p∨q"
shows "¬(¬p∧¬q)"
proof (rule notI)
assume "¬p∧¬q"
show False
using assms
proof
assume "p"
have "¬p" using `¬p∧¬q` by (rule conjunct1)
show False using `¬p` `p` by (rule notE)
next
assume "q"
have "¬q" using `¬p∧¬q` by (rule conjunct2)
show False using `¬q` `q` by (rule notE)
qed
qed

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

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

lemma ej_45: joslopjim4 marcabcar1
assumes "p∧q"
shows "¬(¬p∨¬q)"
proof (rule notI)
assume "¬p∨¬q"
then show False
proof (rule disjE)
assume "¬p"
have "p" using assms by (rule conjunct1)
show False using `¬p` `p` by (rule notE)
next
assume "¬q"
have "q" using assms by (rule conjunct2)
show False using `¬q` `q` by (rule notE)
qed
qed

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

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

lemma ej_46: joslopjim4
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
show "¬p"
proof (rule ccontr)
assume "¬¬p"
have "p" using `¬¬p` by (rule notnotD)
have "p∨q" using `p` by (rule disjI1)
show False using assms `p∨q` by (rule notE)
qed
show "¬q"
proof (rule ccontr)
assume "¬¬q"
have "q" using `¬¬q` by (rule notnotD)
have "p∨q" using `q` by (rule disjI2)
show False using assms `p∨q` by (rule notE)
qed
qed

lemma ejercicio_46: marcabcar1
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
show "¬p"
proof (rule disjE)
show "p∨¬p" by (rule excluded_middle)
{assume "p"
have "p ∨ q" using `p` by (rule disjI1)
show "¬p" using `¬(p ∨ q)` and `p ∨ q` by (rule notE)}
next
{assume "¬p"
show "¬p" using `¬p` by this}
qed
show "¬q"
proof (rule disjE)
show "q∨¬q" by (rule excluded_middle)
{assume "q"
have "p ∨ q" using `q` by (rule disjI2)
show "¬q" using `¬(p ∨ q)` and `p ∨ q` by (rule notE)}
next
{assume "¬q"
show "¬q" using `¬q` by this}
qed
qed

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

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

lemma ej_47: joslopjim4 marcabcar1
assumes "¬p∧¬q"
shows "¬(p∨q)"
proof (rule notI)
assume "p∨q"
then show False
proof
assume "p"
have "¬p" using assms by (rule conjunct1)
show False using `¬p` `p` by (rule notE)
next
assume "q"
have "¬q" using assms by (rule conjunct2)
show False using `¬q` `q` by (rule notE)
qed
qed

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

lemma ejercicio_48: carmarria
assumes 1: "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof -
have "~p | ~q" using 1 by this
moreover {assume 2: "~p"
{assume 3: "p & q"
have 4: p using 3 by (rule conjunct1)
have 5: False using 2 4 by (rule notE)
}
hence 6: "~(p & q)" by (rule notI)
}
moreover {assume 7: "~q"
{assume 8: "p & q"
have 9: q using 8 by (rule conjunct2)
have 10: False using 7 9 by (rule notE)
}
hence 11: "~(p & q)" by (rule notI)
}
ultimately show "~(p & q)" by (rule disjE)
qed

lemma ej_48: joslopjim4 marcabcar1
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule notI)
assume "p∧q"
have "p" using `p∧q` by (rule conjunct1)
have "q" using `p∧q` by (rule conjunct2)
show False
using assms
proof
assume "¬p"
have "p" using `p∧q` by (rule conjunct1)
show False using `¬p` `p` by (rule notE)
next
assume "¬q"
have "q" using `p∧q` by (rule conjunct2)
show False using `¬q` `q` by (rule notE)
qed
qed

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

lemma ejercicio_49: carmarria
"¬(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

lemma ej_49: joslopjim4 marcacar1
shows "¬(p∧¬p)"
proof
assume "p∧¬p"
have "p" using `p∧¬p` by (rule conjunct1)
have "¬p" using `p∧¬p` by (rule conjunct2)
show False using `¬p` `p` by (rule notE)
qed

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

lemma ejercicio_50: carmarria
assumes 1: "p ∧ ¬p"
shows "q"
proof -
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)
show q using 4 by (rule FalseE)
qed

lemma ej_50: joslopjim4 marcabcar1
assumes "p∧¬p"
shows "q"
proof-
have "p" using `p∧¬p` by (rule conjunct1)
have "¬p" using `p∧¬p` by (rule conjunct2)
have False using `¬p` `p` by (rule notE)
then show "q" by (rule FalseE)
qed

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

lemma ejercicio_51: carmarria joslopjim4 marcabcar1
assumes "¬¬p"
shows "p"
proof -
show p using assms by (rule notnotD)
qed

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

lemma ejercicio_52: carmarria
"p ∨ ¬p"
proof -
{assume 1: "~(p | ~p)"
{assume 2: p
have 3: "p | ~p" using 2 by (rule disjI1)
have 4: False using 1 3 by (rule notE)
}
hence 5: "~p" by (rule notI)
have 6: "p | ~p" using 5 by (rule disjI2)
have 7: False using 1 6 by (rule notE)
}
hence 8: "~~(p | ~p)" by (rule notI)
show "p | ~p" using 8 by (rule notnotD)
qed

lemma ejercicio_52: marcabcar1
"p ∨ ¬p"
proof (rule ccontr)
{assume "¬(p ∨ ¬p)"
have "¬p"
proof (rule notI)
{assume "p"
have "p ∨ ¬p" using `p` by (rule disjI1)
show "False" using `¬(p ∨ ¬p)` and `(p ∨ ¬p)` by (rule notE)}
qed
have "p ∨ ¬p" using `¬p` by (rule disjI2)
show "False" using `¬(p ∨ ¬p)` and `p ∨ ¬p` by (rule notE)}
qed

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

lemma ej_53: joslopjim4
shows "((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
assume "(p ⟶ q) ⟶ p"
show "p"
proof (rule ccontr)
assume "¬p"
have "¬(p⟶q)" using `(p ⟶ q) ⟶ p` `¬p` by (rule mt)
have "p⟶q"
proof (rule impI)
assume "p"
show "q" using `¬p` `p` by (rule notE)
qed
show False using `¬(p⟶q)` `p⟶q` by (rule notE)
qed
qed

lemma ejercicio_53: carmarria
"((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: False using 2 4 by (rule notE)
have 6: q using 5 by (rule FalseE)
}
hence 7: "p ⟶q" by (rule impI)
have 8: False using 3 7 by (rule notE)
}
hence 9: "~~p" by (rule notI)
have 10: p using 9 by (rule notnotD)
}
thus "((p ⟶ q)⟶p)⟶p" by (rule impI)
qed

lemma ejercicio_53: marcabcar1
"((p ⟶ q) ⟶ p) ⟶ p"
proof (rule impI)
assume "(p ⟶ q) ⟶ p"
show "p"
proof (rule disjE)
show "p ∨ ¬p" by (rule excluded_middle)
{assume "p"
show "p" using `p` by this}
next
{assume "¬p"
have "¬(p⟶q)" using `(p ⟶ q) ⟶ p` and `¬p` by (rule mt)
have "p⟶q"
proof (rule impI)
{assume "p"
show "q" using `¬p` and `p` by (rule notE)}
qed
show "p" using `¬(p⟶q)` and `p⟶q` by (rule notE)}
qed

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

lemma ej_54: joslopjim4
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
assume "p"
have "¬¬p" using `p` by (rule notnotI)
have "¬¬q" using assms `¬¬p` by (rule mt)
show "q" using `¬¬q` by (rule notnotD)
qed

lemma ejercicio_54: carmarria
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ q"
proof -
{assume 2: p
have 3: "~~p" using 2 by (rule notnotI)
have 4: "~~q" using 1 3 by (rule mt)
have 5: q using 4 by (rule notnotD)
}
thus "p ⟶q" by (rule impI)
qed

lemma ejercicio_54: marcabcar1
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
{assume "p"
have "q∨¬q" by (rule excluded_middle)
show "q"
proof (rule disjE)
show "q ∨ ¬q" using `q ∨ ¬q` by this
{assume "q"
show "q" using `q` by this}
next
{assume "¬q"
have "¬p" using `¬q ⟶ ¬p` and `¬q` by (rule mp)
show "q" using `¬p` and `p` by (rule notE)}
qed}
qed

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

lemma ejercicio_55: carmarria
assumes 1: "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
{assume 2: "~(p | q)"
{assume 3: "~p"
{assume 4: "~q"
have 5: "~p & ~q" using 3 4 by (rule conjI)
have 6: False using 1 5 by (rule notE)
}
hence 7: "~~q" by (rule notI)
have 8: q using 7 by (rule notnotD)
have 9: "p | q" using 8 by (rule disjI2)
have 10: False using 2 9 by (rule notE)
}
hence 11: "~~p" by (rule notI)
have 12: p using 11 by(rule notnotD)
have 13: "p | q" using 12 by (rule disjI1)
have 14: False using 2 13 by (rule notE)
}
hence 15: "~~(p | q)" by (rule notI)
show "p | q" using 15 by (rule notnotD)
qed

lemma ej_55: joslopjim4
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof-
have "¬p∨p" by (rule excluded_middle)
thus "p∨q"
proof (rule disjE)
assume "¬p"
thus "p∨q"
proof-
have "¬q∨q" by (rule excluded_middle)
thus "p∨q"
proof
assume "¬q"
have "¬p∧¬q" using `¬p` `¬q` by (rule conjI)
have False using assms `¬p∧¬q` by (rule notE)
then show "p∨q" by (rule FalseE)
next
assume "q"
show "p∨q" using `q` by (rule disjI2)
qed
qed
next
assume "p"
show "p∨q" using `p` by (rule disjI1)
qed
qed

lemma ejercicio_55:marcabcar1
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule disjE)
show "p ∨ ¬p" by (rule excluded_middle)
{assume "p"
show "p ∨ q" using `p` by (rule disjI1)}
next
{assume "¬p"
show "p ∨ q"
proof (rule disjE)
show "q ∨ ¬q" by (rule excluded_middle)
{assume "q"
show "p ∨ q" using `q` by (rule disjI2)}
next
{assume "¬q"
have "¬p ∧ ¬q" using `¬p` and `¬q` by (rule conjI)
show "p ∨ q" using `¬(¬p ∧ ¬q)` and `(¬p ∧ ¬q)` by (rule notE)}
qed}
qed

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

lemma ejercicio_56: carmarria
assumes 1: "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof -
{assume 2: "~p"
have 3: "~p | ~q" using 2 by (rule disjI1)
have 4: False using 1 3 by (rule notE)
}
hence 5: "~~p" by (rule notI)
have 6: p using 5 by (rule notnotD)
{assume 7: "~q"
have 8: "~p | ~q" using 7 by (rule disjI2)
have 9: False using 1 8 by (rule notE)
}
hence 10: "~~q" by (rule notI)
have 11: q using 10 by (rule notnotD)
show 12: " p & q" using 6 11 by (rule conjI)
qed

lemma ej_56: joslopjim4 marcabcar1
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof-
have "¬p∨p" by (rule excluded_middle)
thus "p∧q"
proof
assume "¬p"
have "¬p∨¬q" using `¬p` by (rule disjI1)
have False using assms `¬p∨¬q` by (rule notE)
then show "p∧q" by (rule FalseE)
next
assume "p"
have "¬q∨q" by (rule excluded_middle)
thus "p∧q"
proof
assume "q"
show "p∧q" using `p` `q` by (rule conjI)
next
assume "¬q"
have "¬p∨¬q" using `¬q` by (rule disjI2)
have False using assms `¬p∨¬q` by (rule notE)
then show "p∧q" by (rule FalseE)
qed
qed
qed

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

lemma ejercicio_57: carmarria
assumes 1: "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
{assume 2: "~(~p | ~q)"
{assume 3: p
{assume 4: q
have 5: "p & q" using 3 4 by (rule conjI)
have 6: False using 1 5 by (rule notE)
}
hence 7: "~q" by (rule notI)
have 8: "~p | ~q" using 7 by (rule disjI2)
have 9: False using 2 8 by (rule notE)
}
hence 10: "~p" by (rule notI)
have 11: "~p | ~q" using 10 by (rule disjI1)
have 12: False using 2 11 by (rule notE)
}
hence 13: "~~(~p | ~q)" by (rule notI)
show "~p | ~q" using 13 by (rule notnotD)
qed

lemma ej_57: joslopjim4 marcabcar1
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof-
have "¬p∨p" by (rule excluded_middle)
thus "¬p∨¬q"
proof (rule disjE)
assume "¬p"
show "¬p∨¬q" using `¬p` by (rule disjI1)
next
assume "p"
have "¬q∨q" by (rule excluded_middle)
thus "¬p∨¬q"
proof (rule disjE)
assume "¬q"
show "¬p∨¬q" using `¬q` by (rule disjI2)
next
assume "q"
have "p∧q" using `p` `q` by (rule conjI)
have False using assms `p∧q` by (rule notE)
then show "¬p∨¬q" by (rule FalseE)
qed
qed
qed

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

lemma ej_58: joslopjim4 marcabcar1
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p∨p" by (rule excluded_middle)
thus "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjE)
assume "¬p"
show "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjI1)
show "p⟶q"
proof
assume "p"
show "q" using `¬p` `p` by (rule notE)
qed
qed
next
assume "p"
show "(p ⟶ q) ∨ (q ⟶ p)"
proof (rule disjI2)
show "q⟶p"
proof (rule impI)
assume "q"
show "p" using `p` by this
qed
qed
qed
qed

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

lemma ej_59: joslopjim4 marcabcar1
assumes "p∧¬(q⟶r)"
shows "(p∧q)∧¬r"
proof
show "p∧q"
proof
show "p" using assms by (rule conjunct1)
next
show "q"
proof (rule ccontr)
assume "¬q"
have "¬(q⟶r)" using assms by (rule conjunct2)
have "q⟶r"
proof
assume "q"
show "r" using `¬q` `q` by (rule notE)
qed
show False using `¬(q⟶r)` `q⟶r` by (rule notE)
qed
qed
next
show "¬r"
proof (rule notI)
assume "r"
have "q⟶r"
proof
assume "q"
show "r" using `r` by this
qed
have "¬(q⟶r)" using assms ..
thus False using `q⟶r` ..
qed
qed

end

</source>

R4

2018-07-14T18:46:54Z

Jalonso:

Tema 2

2018-07-14T18:45:36Z

Jalonso:

<source lang="isabelle">
chapter {* Tema 2: Deducción natural proposicional con Isabelle/HOL *}

theory T2
imports Main
begin

text {*
En este tema se presentan los ejemplos del tema de deducción natural
proposicional siguiendo la presentación de Huth y Ryan en su libro
"Logic in Computer Science" http://goo.gl/qsVpY y, más concretamente,
a la forma como se explica en la asignatura.

La página al lado de cada ejemplo indica la página de las transparencias
donde se encuentra la demostración. *}

subsection {* Reglas de la conjunción *}

text {*
Ejemplo 1 (p. 4). Demostrar que
p ∧ q, r ⊢ q ∧ r.
*}

-- "La demostración detallada es"
lemma ejemplo_1_1:
assumes 1: "p ∧ q" and
2: "r"
shows "q ∧ r"
proof -
have 3: "q" using 1 by (rule conjunct2)
show 4: "q ∧ r" using 3 2 by (rule conjI)
qed
thm ejemplo_1_1
text {*
Notas sobre el lenguaje: En la demostración anterior se ha usado
· "assumes" para indicar las hipótesis,
· "and" para separar las hipótesis,
· "shows" para indicar la conclusión,
· "proof" para iniciar la prueba,
· "qed" para terminar la pruebas,
· "-" (después de "proof") para no usar el método por defecto,
· "have" para establecer un paso,
· "using" para usar hechos en un paso,
· "by (rule ..)" para indicar la regla con la que se peueba un hecho,
· "show" para establecer la conclusión.

Notas sobre la lógica: Las reglas de la conjunción son
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
*}

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_2:
assumes 1: "p ∧ q" and
2: "r"
shows "q ∧ r"
proof -
have 3: "q" using 1 ..
show 4: "q ∧ r" using 3 2 ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· ".." para indicar que se prueba por la regla correspondiente. *}

text {* Se pueden eliminar las etiquetas como sigue *}

lemma ejemplo_1_3:
assumes "p ∧ q"
"r"
shows "q ∧ r"
proof -
have "q" using assms(1) ..
thus "q ∧ r" using assms(2) ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "assms(n)" para indicar la hipótesis n y
· "thus" para demostrar la conclusión usando el hecho anterior.
Además, no es necesario usar and entre las hipótesis. *}

text {* Se puede automatizar la demostración como sigue *}

lemma ejemplo_1_4:
assumes "p ∧ q"
"r"
shows "q ∧ r"
using assms
by auto

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "assms" para indicar las hipótesis y
· "by auto" para demostrar la conclusión automáticamente. *}

text {* Se puede automatizar totalmente la demostración como sigue *}

lemma ejemplo_1_5:
"⟦p ∧ q; r⟧ ⟹ q ∧ r"
by auto

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "⟦ ... ⟧" para representar las hipótesis,
· ";" para separar las hipótesis y
· "⟹" para separar las hipótesis de la conclusión. *}

text {* Se puede hacer la demostración por razonamiento hacia atrás,
como sigue *}

lemma ejemplo_1_6:
assumes "p ∧ q"
and "r"
shows "q ∧ r"
proof (rule conjI)
show "q" using assms(1) by (rule conjunct2)
next
show "r" using assms(2) by this
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "proof (rule r)" para indicar que se hará la demostración con la
regla r,
· "next" para indicar el comienzo de la prueba del siguiente
subobjetivo,
· "this" para indicar el hecho actual. *}

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_7:
assumes "p ∧ q"
"r"
shows "q ∧ r"
proof
show "q" using assms(1) ..
next
show "r" using assms(2) .
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "." para indicar por el hecho actual. *}

subsection {* Reglas de la doble negación *}

text {*
La regla de eliminación de la doble negación es
· notnotD: ¬¬ P ⟹ P

Para ajustarnos al tema de LI vamos a introducir la siguiente regla de
introducción de la doble negación
· notnotI: P ⟹ ¬¬ P
aunque, de momento, no detallamos su demostración.
*}

lemma notnotI [intro!]: "P ⟹ ¬¬ P"
by auto

text {*
Ejemplo 2. (p. 5)
p, ¬¬(q ∧ r) ⊢ ¬¬p ∧ r
*}

-- "La demostración detallada es"
lemma ejemplo_2_1:
assumes 1: "p" and
2: "¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof -
have 3: "¬¬p" using 1 by (rule notnotI)
have 4: "q ∧ r" using 2 by (rule notnotD)
have 5: "r" using 4 by (rule conjunct2)
show 6: "¬¬p ∧ r" using 3 5 by (rule conjI)
qed

-- "La demostración estructurada es"
lemma ejemplo_2_2:
assumes "p"
"¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof -
have "¬¬p" using assms(1) ..
have "q ∧ r" using assms(2) by (rule notnotD)
hence "r" ..
with `¬¬p` show "¬¬p ∧ r" ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "hence" para indicar que se tiene por el hecho anterior,
· `...` para referenciar un hecho y
· "with P show Q" para indicar que con el hecho anterior junto con el
hecho P se demuestra Q. *}

-- "La demostración automática es"
lemma ejemplo_2_3:
assumes "p"
"¬¬(q ∧ r)"
shows "¬¬p ∧ r"
using assms
by auto

text {* Se puede demostrar hacia atrás *}

lemma ejemplo_2_4:
assumes "p"
"¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof (rule conjI)
show "¬¬p" using assms(1) by (rule notnotI)
next
have "q ∧ r" using assms(2) by (rule notnotD)
thus "r" by (rule conjunct2)
qed

text {* Se puede eliminar las reglas en la demostración anterior, como
sigue: *}

lemma ejemplo_2_5:
assumes "p"
"¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof
show "¬¬p" using assms(1) ..
next
have "q ∧ r" using assms(2) by (rule notnotD)
thus "r" ..
qed

subsection {* Regla de eliminación del condicional *}

text {*
La regla de eliminación del condicional es la regla del modus ponens
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
*}

text {*
Ejemplo 3. (p. 6) Demostrar que
¬p ∧ q, ¬p ∧ q ⟶ r ∨ ¬p ⊢ r ∨ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_3_1:
assumes 1: "¬p ∧ q" and
2: "¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
proof -
show "r ∨ ¬p" using 2 1 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejemplo_3_2:
assumes "¬p ∧ q"
"¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
proof -
show "r ∨ ¬p" using assms(2,1) ..
qed

-- "La demostración automática es"
lemma ejemplo_3_3:
assumes "¬p ∧ q"
"¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
using assms
by auto

text {*
Ejemplo 4 (p. 6) Demostrar que
p, p ⟶ q, p ⟶ (q ⟶ r) ⊢ r
*}

-- "La demostración detallada es"
lemma ejemplo_4_1:
assumes 1: "p" and
2: "p ⟶ q" and
3: "p ⟶ (q ⟶ r)"
shows "r"
proof -
have 4: "q" using 2 1 by (rule mp)
have 5: "q ⟶ r" using 3 1 by (rule mp)
show 6: "r" using 5 4 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejemplo_4_2:
assumes "p"
"p ⟶ q"
"p ⟶ (q ⟶ r)"
shows "r"
proof -
have "q" using assms(2,1) ..
have "q ⟶ r" using assms(3,1) ..
thus "r" using `q` ..
qed

-- "La demostración automática es"
lemma ejemplo_4_3:
"⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r"
by auto

subsection {* Regla derivada del modus tollens *}

text {*
Para ajustarnos al tema de LI vamos a introducir la regla del modus
tollens
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
aunque, de momento, sin detallar su demostración.
*}

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text {*
Ejemplo 5 (p. 7). Demostrar
p ⟶ (q ⟶ r), p, ¬r ⊢ ¬q
*}

-- "La demostración detallada es"
lemma ejemplo_5_1:
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p" and
3: "¬r"
shows "¬q"
proof -
have 4: "q ⟶ r" using 1 2 by (rule mp)
show "¬q" using 4 3 by (rule mt)
qed

-- "La demostración estructurada es"
lemma ejemplo_5_2:
assumes "p ⟶ (q ⟶ r)"
"p"
"¬r"
shows "¬q"
proof -
have "q ⟶ r" using assms(1,2) ..
thus "¬q" using assms(3) by (rule mt)
qed

-- "La demostración automática es"
lemma ejemplo_5_3:
assumes "p ⟶ (q ⟶ r)"
"p"
"¬r"
shows "¬q"
using assms
by auto

text {*
Ejemplo 6. (p. 7) Demostrar
¬p ⟶ q, ¬q ⊢ p
*}

-- "La demostración detallada es"
lemma ejemplo_6_1:
assumes 1: "¬p ⟶ q" and
2: "¬q"
shows "p"
proof -
have 3: "¬¬p" using 1 2 by (rule mt)
show "p" using 3 by (rule notnotD)
qed

-- "La demostración estructurada es"
lemma ejemplo_6_2:
assumes "¬p ⟶ q"
"¬q"
shows "p"
proof -
have "¬¬p" using assms(1,2) by (rule mt)
thus "p" by (rule notnotD)
qed

-- "La demostración automática es"
lemma ejemplo_6_3:
"⟦¬p ⟶ q; ¬q⟧ ⟹ p"
by auto

text {*
Ejemplo 7. (p. 7) Demostrar
p ⟶ ¬q, q ⊢ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_7_1:
assumes 1: "p ⟶ ¬q" and
2: "q"
shows "¬p"
proof -
have 3: "¬¬q" using 2 by (rule notnotI)
show "¬p" using 1 3 by (rule mt)
qed

-- "La demostración detallada es"
lemma ejemplo_7_2:
assumes "p ⟶ ¬q"
"q"
shows "¬p"
proof -
have "¬¬q" using assms(2) by (rule notnotI)
with assms(1) show "¬p" by (rule mt)
qed

-- "La demostración estructurada es"
lemma ejemplo_7_3:
"⟦p ⟶ ¬q; q⟧ ⟹ ¬p"
by auto

subsection {* Regla de introducción del condicional *}

text {*
La regla de introducción del condicional es
· impI: (P ⟹ Q) ⟹ P ⟶ Q
*}

text {*
Ejemplo 8. (p. 8) Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_8_1:
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof -
{ assume 2: "¬q"
have "¬p" using 1 2 by (rule mt) }
thus "¬q ⟶ ¬p" by (rule impI)
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "{ ... }" para representar una caja. *}

-- "La demostración estructurada es"
lemma ejemplo_8_2:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof
assume "¬q"
with assms show "¬p" by (rule mt)
qed

-- "La demostración automática es"
lemma ejemplo_8_3:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
using assms
by auto

text {*
Ejemplo 9. (p. 9) Demostrar
¬q ⟶ ¬p ⊢ p ⟶ ¬¬q
*}

-- "La demostración detallada es"
lemma ejemplo_9_1:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
proof -
{ assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
have "¬¬q" using 1 3 by (rule mt) }
thus "p ⟶ ¬¬q" by (rule impI)
qed

-- "La demostración estructurada es"
lemma ejemplo_9_2:
assumes "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
proof
assume "p"
hence "¬¬p" by (rule notnotI)
with assms show "¬¬q" by (rule mt)
qed

-- "La demostración automática es"
lemma ejemplo_9_3:
assumes "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
using assms
by auto

text {*
Ejemplo 10 (p. 9). Demostrar
⊢ p ⟶ p
*}

-- "La demostración detallada es"
lemma ejemplo_10_1:
"p ⟶ p"
proof -
{ assume 1: "p"
have "p" using 1 by this }
thus "p ⟶ p" by (rule impI)
qed

-- "La demostración estructurada es"
lemma ejemplo_10_2:
"p ⟶ p"
proof (rule impI)
qed

-- "La demostración automática es"
lemma ejemplo_10_3:
"p ⟶ p"
by auto

text {*
Ejemplo 11 (p. 10) Demostrar
⊢ (q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))
*}

-- "La demostración detallada es"
lemma ejemplo_11_1:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof -
{ assume 1: "q ⟶ r"
{ assume 2: "¬q ⟶ ¬p"
{ assume 3: "p"
have 4: "¬¬p" using 3 by (rule notnotI)
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
have "r" using 1 6 by (rule mp) }
hence "p ⟶ r" by (rule impI) }
hence "(¬q ⟶ ¬p) ⟶ p ⟶ r" by (rule impI) }
thus "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ p ⟶ r)" by (rule impI)
qed

-- "La demostración hacia atrás es"
lemma ejemplo_11_2:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "q ⟶ r"
show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "¬q ⟶ ¬p"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "¬¬p" using 3 by (rule notnotI)
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
show "r" using 1 6 by (rule mp)
qed
qed
qed

-- "La demostración hacia atrás con reglas implícitas es"
lemma ejemplo_11_3:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof
assume 1: "q ⟶ r"
show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
proof
assume 2: "¬q ⟶ ¬p"
show "p ⟶ r"
proof
assume 3: "p"
have 4: "¬¬p" using 3 ..
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
show "r" using 1 6 ..
qed
qed
qed

-- "La demostración sin etiquetas es"
lemma ejemplo_11_4:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof
assume "q ⟶ r"
show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
proof
assume "¬q ⟶ ¬p"
show "p ⟶ r"
proof
assume "p"
hence "¬¬p" ..
with `¬q ⟶ ¬p` have "¬¬q" by (rule mt)
hence "q" by (rule notnotD)
with `q ⟶ r` show "r" ..
qed
qed
qed

-- "La demostración automática es"
lemma ejemplo_11_5:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
by auto

subsection {* Reglas de la disyunción *}

text {*
Las reglas de la introducción de la disyunción son
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
La regla de elimación de la disyunción es
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
*}

text {*
Ejemplo 12 (p. 11). Demostrar
p ∨ q ⊢ q ∨ p
*}

-- "La demostración detallada es"
lemma ejemplo_12_1:
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

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "moreover" para separar los bloques y
· "ultimately" para unir los resultados de los bloques. *}

-- "La demostración detallada con reglas implícitas es"
lemma ejemplo_12_2:
assumes "p ∨ q"
shows "q ∨ p"
proof -
note `p ∨ q`
moreover
{ assume "p"
hence "q ∨ p" .. }
moreover
{ assume "q"
hence "q ∨ p" .. }
ultimately show "q ∨ p" ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "note" para copiar un hecho. *}

-- "La demostración hacia atrás es"
lemma ejemplo_12_3:
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 3: "q"
show "q ∨ p" using 3 by (rule disjI1) }
qed

-- "La demostración hacia atrás con reglas implícitas es"
lemma ejemplo_12_4:
assumes "p ∨ q"
shows "q ∨ p"
using assms
proof
{ assume "p"
thus "q ∨ p" .. }
next
{ assume "q"
thus "q ∨ p" .. }
qed

-- "La demostración automática es"
lemma ejemplo_12_5:
assumes "p ∨ q"
shows "q ∨ p"
using assms
by auto

text {*
Ejemplo 13. (p. 12) Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
*}

-- "La demostración detallada es"
lemma ejemplo_13_1:
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

-- "La demostración estructurada es"
lemma ejemplo_13_2:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof
assume "p ∨ q"
thus "p ∨ r"
proof
{ assume "p"
thus "p ∨ r" .. }
next
{ assume "q"
have "r" using assms `q` ..
thus "p ∨ r" .. }
qed
qed

-- "La demostración automática es"
lemma ejemplo_13_3:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
using assms
by auto

subsection {* Regla de copia *}

text {*
Ejemplo 14 (p. 13). Demostrar
⊢ p ⟶ (q ⟶ p)
*}

-- "La demostración detallada es"
lemma ejemplo_14_1:
"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

-- "La demostración estructurada es"
lemma ejemplo_14_2:
"p ⟶ (q ⟶ p)"
proof
assume "p"
thus "q ⟶ p" ..
qed

-- "La demostración automática es"
lemma ejemplo_14_3:
"p ⟶ (q ⟶ p)"
by auto

subsection {* Reglas de la negación *}

text {*
La regla de eliminación de lo falso es
· FalseE: False ⟹ P
La regla de eliminación de la negación es
· notE: ⟦¬P; P⟧ ⟹ R
La regla de introducción de la negación es
· notI: (P ⟹ False) ⟹ ¬P
*}

text {*
Ejemplo 15 (p. 15). Demostrar
¬p ∨ q ⊢ p ⟶ q
*}

-- "La demostración detallada es"
lemma ejemplo_15_1:
assumes 1: "¬p ∨ q"
shows "p ⟶ q"
proof (rule impI)
assume 2: "p"
note 1
thus "q"
proof (rule disjE)
{ assume 3: "¬p"
show "q" using 3 2 by (rule notE) }
next
{ assume 4: "q"
show "q" using 4 by this}
qed
qed

-- "La demostración estructurada es"
lemma ejemplo_15_2:
assumes "¬p ∨ q"
shows "p ⟶ q"
proof
assume "p"
note `¬p ∨ q`
thus "q"
proof
{ assume "¬p"
thus "q" using `p` .. }
next
{ assume "q"
thus "q" . }
qed
qed

-- "La demostración automática es"
lemma ejemplo_15_3:
assumes "¬p ∨ q"
shows "p ⟶ q"
using assms
by auto

text {*
Ejemplo 16 (p. 16). Demostrar
p ⟶ q, p ⟶ ¬q ⊢ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_16_1:
assumes 1: "p ⟶ q" and
2: "p ⟶ ¬q"
shows "¬p"
proof (rule notI)
assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "¬q" using 2 3 by (rule mp)
show False using 5 4 by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_16_2:
assumes "p ⟶ q"
"p ⟶ ¬q"
shows "¬p"
proof
assume "p"
have "q" using assms(1) `p` ..
have "¬q" using assms(2) `p` ..
thus False using `q` ..
qed

-- "La demostración automática es"
lemma ejemplo_16_3:
assumes "p ⟶ q"
"p ⟶ ¬q"
shows "¬p"
using assms
by auto

subsection {* Reglas del bicondicional *}

text {*
La regla de introducción del bicondicional es
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P ⟷ Q
Las reglas de eliminación del bicondicional son
· iffD1: ⟦Q ⟷ P; Q⟧ ⟹ P
· iffD2: ⟦P ⟷ Q; Q⟧ ⟹ P
*}

text {*
Ejemplo 17 (p. 17) Demostrar
*}

-- "La demostración detallada es"
lemma ejemplo_17_1:
"(p ∧ q) ⟷ (q ∧ p)"
proof (rule iffI)
{ assume 1: "p ∧ q"
have 2: "p" using 1 by (rule conjunct1)
have 3: "q" using 1 by (rule conjunct2)
show "q ∧ p" using 3 2 by (rule conjI) }
next
{ assume 4: "q ∧ p"
have 5: "q" using 4 by (rule conjunct1)
have 6: "p" using 4 by (rule conjunct2)
show "p ∧ q" using 6 5 by (rule conjI) }
qed

-- "La demostración estructurada es"
lemma ejemplo_17_2:
"(p ∧ q) ⟷ (q ∧ p)"
proof
{ assume 1: "p ∧ q"
have "p" using 1 ..
have "q" using 1 ..
show "q ∧ p" using `q` `p` .. }
next
{ assume 2: "q ∧ p"
have "q" using 2 ..
have "p" using 2 ..
show "p ∧ q" using `p` `q` .. }
qed

-- "La demostración automática es"
lemma ejemplo_17_3:
"(p ∧ q) ⟷ (q ∧ p)"
by auto

text {*
Ejemplo 18 (p. 18). Demostrar
p ⟷ q, p ∨ q ⊢ p ∧ q
*}

-- "La demostración detallada es"
lemma ejemplo_18_1:
assumes 1: "p ⟷ q" and
2: "p ∨ q"
shows "p ∧ q"
using 2
proof (rule disjE)
{ assume 3: "p"
have 4: "q" using 1 3 by (rule iffD1)
show "p ∧ q" using 3 4 by (rule conjI) }
next
{ assume 5: "q"
have 6: "p" using 1 5 by (rule iffD2)
show "p ∧ q" using 6 5 by (rule conjI) }
qed

-- "La demostración estructurada es"
lemma ejemplo_18_2:
assumes "p ⟷ q"
"p ∨ q"
shows "p ∧ q"
using assms(2)
proof
{ assume "p"
with assms(1) have "q" ..
with `p` show "p ∧ q" .. }
next
{ assume "q"
with assms(1) have "p" ..
thus "p ∧ q" using `q` .. }
qed

-- "La demostración automática es"
lemma ejemplo_18_3:
assumes "p ⟷ q"
"p ∨ q"
shows "p ∧ q"
using assms
by auto

subsection {* Reglas derivadas *}

subsubsection {* Regla del modus tollens *}

text {*
Ejemplo 19 (p. 20) Demostrar la regla del modus tollens a partir de
las reglas básicas.
*}

-- "La demostración detallada es"
lemma ejemplo_20_1:
assumes 1: "F ⟶ G" and
2: "¬G"
shows "¬F"
proof (rule notI)
assume 3: "F"
have 4: "G" using 1 3 by (rule mp)
show False using 2 4 by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_20_2:
assumes "F ⟶ G"
"¬G"
shows "¬F"
proof
assume "F"
with assms(1) have "G" ..
with assms(2) show False ..
qed

-- "La demostración automática es"
lemma ejemplo_20_3:
assumes "F ⟶ G"
"¬G"
shows "¬F"
using assms
by auto

subsubsection {* Regla de la introducción de la doble negación *}

text {*
Ejemplo 21 (p. 21) Demostrar la regla de introducción de la doble
negación a partir de las reglas básicas.
*}

-- "La demostración detallada es"
lemma ejemplo_21_1:
assumes 1: "F"
shows "¬¬F"
proof (rule notI)
assume 2: "¬F"
show False using 2 1 by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_21_2:
assumes "F"
shows "¬¬F"
proof
assume "¬F"
thus False using assms ..
qed

-- "La demostración automática es"
lemma ejemplo_21_3:
assumes "F"
shows "¬¬F"
using assms
by auto

subsubsection {* Regla de reducción al absurdo *}

text {*
La regla de reducción al absurdo en Isabelle se correponde con la
regla clásica de contradicción
· ccontr: (¬P ⟹ False) ⟹ P
*}

subsubsection {* Ley del tercio excluso *}

text {*
La ley del tercio excluso es
· excluded_middle: ¬P ∨ P
*}

text {*
Ejemplo 22 (p. 23). Demostrar la ley del tercio excluso a partir de
las reglas básicas.
*}

-- "La demostración detallada es"
lemma ejemplo_22_1:
"F ∨ ¬F"
proof (rule ccontr)
assume 1: "¬(F ∨ ¬F)"
thus False
proof (rule notE)
show "F ∨ ¬F"
proof (rule disjI2)
show "¬F"
proof (rule notI)
assume 2: "F"
hence 3: "F ∨ ¬F" by (rule disjI1)
show False using 1 3 by (rule notE)
qed
qed
qed
qed

-- "La demostración estructurada es"
lemma ejemplo_22_2:
"F ∨ ¬F"
proof (rule ccontr)
assume "¬(F ∨ ¬F)"
thus False
proof (rule notE)
show "F ∨ ¬F"
proof (rule disjI2)
show "¬F"
proof (rule notI)
assume "F"
hence "F ∨ ¬F" ..
with `¬(F ∨ ¬F)`show False ..
qed
qed
qed
qed

-- "La demostración automática es"
lemma ejemplo_22_3:
"F ∨ ¬F"
using assms
by auto

text {*
Ejemplo 23 (p. 24). Demostrar
p ⟶ q ⊢ ¬p ∨ q
*}

-- "La demostración detallada es"
lemma ejemplo_23_1:
assumes 1: "p ⟶ q"
shows "¬p ∨ q"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "¬p ∨ q"
proof (rule disjE)
{ assume "¬p"
thus "¬p ∨ q" by (rule disjI1) }
next
{ assume 2: "p"
have "q" using 1 2 by (rule mp)
thus "¬p ∨ q" by (rule disjI2) }
qed
qed

-- "La demostración estructurada es"
lemma ejemplo_23_2:
assumes "p ⟶ q"
shows "¬p ∨ q"
proof -
have "¬p ∨ p" ..
thus "¬p ∨ q"
proof
{ assume "¬p"
thus "¬p ∨ q" .. }
next
{ assume "p"
with assms have "q" ..
thus "¬p ∨ q" .. }
qed
qed

-- "La demostración automática es"
lemma ejemplo_23_3:
assumes "p ⟶ q"
shows "¬p ∨ q"
using assms
by auto

subsection {* Demostraciones por contradicción *}

text {*
Ejemplo 24. Demostrar que
¬p, p ∨ q ⊢ q
*}

-- "La demostración detallada es"
lemma ejemplo_24_1:
assumes "¬p"
"p ∨ q"
shows "q"
using `p ∨ q`
proof (rule disjE)
assume "p"
with assms(1) show "q" by contradiction
next
assume "q"
thus "q" by assumption
qed

-- "La demostración estructurada es"
lemma ejemplo_24_2:
assumes "¬p"
"p ∨ q"
shows "q"
using `p ∨ q`
proof
assume "p"
with assms(1) show "q" ..
next
assume "q"
thus "q" .
qed

-- "La demostración automática es"
lemma ejemplo_24_3:
assumes "¬p"
"p ∨ q"
shows "q"
using assms
by auto

end
</source>

MediaWiki:Common.css

2018-07-14T13:53:37Z

Jalonso:

/* 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");

MediaWiki:Common.css

2018-07-14T13:28:16Z

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

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

R5

2018-03-25T08:25:29Z

Jalonso:

=== Relación 5: Sintaxis y semántica de la Lógica de primer orden ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento (ejercicio 5 de LPO de [http://www.glc.us.es/apli2/login/ APLI2], verificando la corrección de la solución:
* 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 lo tanto, algún aduanero es contrabandista.
----

'''Solución:'''

----
'''Ejercicio 2.''' Formalizar el siguiente argumento (ejercicio 15 de LPO de [http://www.glc.us.es/apli2/login/ APLI2], verificando la corrección de la solución:
* Todos los robots obedecen a los amigos del programador jefe.
* Alvaro es amigo del programador jefe.
* Benito no obedece a Alvaro.
* Benito no es un robot.
----

'''Solución:'''

----
'''Ejercicio 3.''' Formalizar el siguiente argumento (ejercicio 16 de LPO de [http://www.glc.us.es/apli2/login/ APPLI2]), verificando la corrección de la solución:
* Hay algún pez x que para cualquier pez y, si el pez x no se come al pez y entonces existe un pez z tal que z es un tiburón o bien z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
* Por lo tanto, existe algún tiburón en la pecera.
----

'''Solución:'''

----
'''Ejercicio 4.''' Formalizar el siguiente argumento (ejercicio 21 de LPO de [http://www.glc.us.es/apli2/login/ APPLI2]), verificando la corrección de la solución:
* Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí mismo y sólo a ellos.
* Carlos es un habitante de las Chinas.
* Por lo tanto, Carlos no afeita a nadie.
----

'''Solución:'''

----
'''Ejercicio 5.'''
Sea F la fórmula P(x) → P (a), donde a es un símbolo de constante. Dar un ejemplo de una interpretación en la que F sea verdadera. Y un ejemplo de una interpretación en la que F sea falsa.
----

'''Solución:'''

----
'''Ejercicio 6.'''
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de aridad 1), Q (de aridad 2) y un símbolo de función, f (de aridad 1). Sea I = (U, I) la estructura dada por:
* U = {a, b, c, d} ;
* I(P) = {a, b},
* I(Q) = {(a, b), (b, b), (c, b)},
* I(f) = {(a, b), (b, b), (c, a), (d, c)}.
¿Cuál es el valor de cada una de las siguientes fórmulas en dicha estructura?
* P(x) → ∃yQ(y,x).
* ∀xQ(f(x),x).
* Q(f(x),x) → Q(x,x).
* Q(x,y) → P(x).
----

'''Solución:'''

----
'''Ejercicio 7.'''
En el lenguaje con igualdad L = {a,f}, siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
* F₁ : = ∀x[f(x) ≠ a],
* F₂ : = ∀x∀y[f(x) = f(y) → x = y],
* F₃ : = ∀x[x ≠ a → ∃y[f(y) = x]] .

Probar que ninguna de estas fórmulas es consecuencia lógica de las dos restantes.
----

'''Solución:'''

----
'''Ejercicio 8.''' Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos. Generalizarlo a n cualquiera.
----

'''Solución:'''

R5

2018-03-25T08:23:21Z

Jalonso:

=== Relación 5: Sintaxis y semántica de la Lógica de primer orden ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento (ejercicio 5 de LPO de [http://www.glc.us.es/apli2/login/ APLI2], verificando la corrección de la solución:
* 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 lo tanto, algún aduanero es contrabandista.
----

'''Solución:'''

----
'''Ejercicio 2.''' Formalizar el siguiente argumento (ejercicio 15 de LPO de [http://www.glc.us.es/apli2/login/ APLI2], verificando la corrección de la solución:
* Todos los robots obedecen a los amigos del programador jefe.
* Alvaro es amigo del programador jefe.
* Benito no obedece a Alvaro.
* Benito no es un robot.
----

'''Solución:'''

----
'''Ejercicio 3.''' Formalizar el siguiente argumento (ejercicio 16 de LPO de [http://www.glc.us.es/apli2/login/ APPLI2]), verificando la corrección de la solución:
* Hay algún pez x que para cualquier pez y, si el pez x no se come al pez y entonces existe un pez z tal que z es un tiburón o bien z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
* Por lo tanto, existe algún tiburón en la pecera.
----

'''Solución:'''

----
'''Ejercicio 4.''' Formalizar el siguiente argumento (ejercicio 21 de LPO de [http://www.glc.us.es/apli2/login/ APPLI2]), verificando la corrección de la solución:
* Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí mismo y sólo a ellos.
* Carlos es un habitante de las Chinas.
* Por lo tanto, Carlos no afeita a nadie.
----

'''Solución:'''

----
'''Ejercicio 5.'''
Sea F la fórmula P(x) → P (a), donde a es un símbolo de constante. Dar un ejemplo de una interpretación en la que F sea verdadera. Y un ejemplo de una interpretación en la que F sea falsa.
----

'''Solución:'''

----
'''Ejercicio 6.'''
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de aridad 1), Q (de aridad 2) y un símbolo de función, f (de aridad 1). Sea I = (U, I) la estructura dada por:
* U = {a, b, c, d} ;
* I P) = {a, b},
* I Q) = {(a, b), (b, b), (c, b)},
* I f) = {(a, b), (b, b), (c, a), (d, c)}.
¿Cuál es el valor de cada una de las siguientes fórmulas en dicha estructura?
* P (x) → ∃yQ(y,x).
* ∀xQ(f(x),x).
* Q(f(x),x) → Q(x,x).
* Q(x,y) → P(x).
----

'''Solución:'''

----
'''Ejercicio 7.'''

En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
* F₁ : = ∀ x [ f ( x ) ≠ a ] ,
* F₂ : = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
* F₃ : = ∀ x [ x ≠ a → ∃ y [ f ( y ) = x ]] .

Probar que ninguna de estas fórmulas es consecuencia lógica de las dos restantes.
----

'''Solución:'''

----
'''Ejercicio 8.''' Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos. Generalizarlo a n cualquiera.

----

'''Solución:'''

R5

2018-03-25T08:16:31Z

Jalonso:

=== Relación 5: Sintaxis y semántica de la Lógica de primer orden ===

----
'''Ejercicio 1.''' Formalizar el siguiente argumento (ejercicio 5 de LPO de
APPLI2), verificando la corrección de la solución:

* 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 lo tanto, algún aduanero es contrabandista.
----

'''Solución:'''

----
'''Ejercicio 2.''' Formalizar el siguiente argumento (ejercicio 15 de LPO de
APPLI2), verificando la corrección de la solución:

* Todos los robots obedecen a los amigos del programador jefe.
* Alvaro es amigo del programador jefe.
* Benito no obedece a Alvaro.
* Benito no es un robot.

----

'''Solución:'''

----
'''Ejercicio 3.''' Formalizar el siguiente argumento (ejercicio 16 de LPO de
APPLI2), verificando la corrección de la solución:

* Hay algún pez x que para cualquier pez y, si el pez x no se come al pez y entonces existe un pez z tal que z es un tiburón o bien z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
* Por lo tanto, existe algún tiburón en la pecera.

----

'''Solución:'''

----
'''Ejercicio 4.''' Formalizar el siguiente argumento (ejercicio 21 de LPO de
APPLI2), verificando la corrección de la solución:

* Carlos afeita a todos los habitantes de Las Chinas que no se afeitan a sí mismo y sólo a ellos.
* Carlos es un habitante de las Chinas.
* Por lo tanto, Carlos no afeita a nadie.

----

'''Solución:'''

----
'''Ejercicio 5.'''
Sea F la fórmula P(x) → P (a) , donde a es un símbolo de constante. Dar un
ejemplo de una interpretación en la que F sea verdadera. Y un ejemplo de una
interpretación en la que F sea falsa.

----

'''Solución:'''

----
'''Ejercicio 6.'''
Sea L un lenguaje de primer orden con dos símbolos de predicado, P (de aridad
1), Q (de aridad 2) y un símbolo de función, f , de aridad 1. Sea I = ( U, I )
la estructura dada por:
U = { a, b, c, d } ;
I ( P ) = { a, b } ,
I ( Q ) = {( a, b ) , ( b, b ) , ( c, b )} ,
I ( f ) = {( a, b ) , ( b, b ) , ( c, a ) , ( d, c )} .
¿Cuál es el valor de cada una de las siguientes fórmulas en dicha estructura?
* P ( x ) → ∃ yQ ( y, x ) .
*. ∀ xQ ( f ( x ) , x ) .
* Q ( f ( x ) , x ) → Q ( x, x ) .
* Q ( x, y ) → P ( x ) .
----

'''Solución:'''

----
'''Ejercicio 7.'''

En el lenguaje con igualdad L = { a, f } , siendo f un símbolo de función
de aridad 1 y a una constante, se consideran las siguientes fórmulas:
* F₁ : = ∀ x [ f ( x ) ≠ a ] ,
* F₂ : = ∀ x ∀ y [ f ( x ) = f ( y ) → x = y ] ,
* F₃ : = ∀ x [ x ≠ a → ∃ y [ f ( y ) = x ]] .

Probar que ninguna de estas fórmulas es consecuencia lógica de las dos restantes.
----

'''Solución:'''

----
'''Ejercicio 8.''' Dar una fórmula F, tal que todo modelo de F tenga al menos 3 elementos. Generalizarlo a n cualquiera.

----

'''Solución:'''

Lógica matemática y fundamentos (2017-18)

2018-02-27T05:56:01Z

Jalonso: Protegió «Lógica matemática y fundamentos (2017-18)» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

Tema 2

2018-02-27T05:55:37Z

Jalonso: Protegió «Tema 2» ([edit=sysop] (indefinido) [move=sysop] (indefinido))

<source lang="isar">
chapter {* Tema 2: Deducción natural proposicional con Isabelle/HOL *}

theory T2
imports Main
begin

text {*
En este tema se presentan los ejemplos del tema de deducción natural
proposicional siguiendo la presentación de Huth y Ryan en su libro
"Logic in Computer Science" http://goo.gl/qsVpY y, más concretamente,
a la forma como se explica en la asignatura.

La página al lado de cada ejemplo indica la página de las transparencias
donde se encuentra la demostración. *}

subsection {* Reglas de la conjunción *}

text {*
Ejemplo 1 (p. 4). Demostrar que
p ∧ q, r ⊢ q ∧ r.
*}

-- "La demostración detallada es"
lemma ejemplo_1_1:
assumes 1: "p ∧ q" and
2: "r"
shows "q ∧ r"
proof -
have 3: "q" using 1 by (rule conjunct2)
show 4: "q ∧ r" using 3 2 by (rule conjI)
qed
thm ejemplo_1_1
text {*
Notas sobre el lenguaje: En la demostración anterior se ha usado
· "assumes" para indicar las hipótesis,
· "and" para separar las hipótesis,
· "shows" para indicar la conclusión,
· "proof" para iniciar la prueba,
· "qed" para terminar la pruebas,
· "-" (después de "proof") para no usar el método por defecto,
· "have" para establecer un paso,
· "using" para usar hechos en un paso,
· "by (rule ..)" para indicar la regla con la que se peueba un hecho,
· "show" para establecer la conclusión.

Notas sobre la lógica: Las reglas de la conjunción son
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
*}

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_2:
assumes 1: "p ∧ q" and
2: "r"
shows "q ∧ r"
proof -
have 3: "q" using 1 ..
show 4: "q ∧ r" using 3 2 ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· ".." para indicar que se prueba por la regla correspondiente. *}

text {* Se pueden eliminar las etiquetas como sigue *}

lemma ejemplo_1_3:
assumes "p ∧ q"
"r"
shows "q ∧ r"
proof -
have "q" using assms(1) ..
thus "q ∧ r" using assms(2) ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "assms(n)" para indicar la hipótesis n y
· "thus" para demostrar la conclusión usando el hecho anterior.
Además, no es necesario usar and entre las hipótesis. *}

text {* Se puede automatizar la demostración como sigue *}

lemma ejemplo_1_4:
assumes "p ∧ q"
"r"
shows "q ∧ r"
using assms
by auto

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "assms" para indicar las hipótesis y
· "by auto" para demostrar la conclusión automáticamente. *}

text {* Se puede automatizar totalmente la demostración como sigue *}

lemma ejemplo_1_5:
"⟦p ∧ q; r⟧ ⟹ q ∧ r"
by auto

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "⟦ ... ⟧" para representar las hipótesis,
· ";" para separar las hipótesis y
· "⟹" para separar las hipótesis de la conclusión. *}

text {* Se puede hacer la demostración por razonamiento hacia atrás,
como sigue *}

lemma ejemplo_1_6:
assumes "p ∧ q"
and "r"
shows "q ∧ r"
proof (rule conjI)
show "q" using assms(1) by (rule conjunct2)
next
show "r" using assms(2) by this
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "proof (rule r)" para indicar que se hará la demostración con la
regla r,
· "next" para indicar el comienzo de la prueba del siguiente
subobjetivo,
· "this" para indicar el hecho actual. *}

text {* Se pueden dejar implícitas las reglas como sigue *}

lemma ejemplo_1_7:
assumes "p ∧ q"
"r"
shows "q ∧ r"
proof
show "q" using assms(1) ..
next
show "r" using assms(2) .
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "." para indicar por el hecho actual. *}

subsection {* Reglas de la doble negación *}

text {*
La regla de eliminación de la doble negación es
· notnotD: ¬¬ P ⟹ P

Para ajustarnos al tema de LI vamos a introducir la siguiente regla de
introducción de la doble negación
· notnotI: P ⟹ ¬¬ P
aunque, de momento, no detallamos su demostración.
*}

lemma notnotI [intro!]: "P ⟹ ¬¬ P"
by auto

text {*
Ejemplo 2. (p. 5)
p, ¬¬(q ∧ r) ⊢ ¬¬p ∧ r
*}

-- "La demostración detallada es"
lemma ejemplo_2_1:
assumes 1: "p" and
2: "¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof -
have 3: "¬¬p" using 1 by (rule notnotI)
have 4: "q ∧ r" using 2 by (rule notnotD)
have 5: "r" using 4 by (rule conjunct2)
show 6: "¬¬p ∧ r" using 3 5 by (rule conjI)
qed

-- "La demostración estructurada es"
lemma ejemplo_2_2:
assumes "p"
"¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof -
have "¬¬p" using assms(1) ..
have "q ∧ r" using assms(2) by (rule notnotD)
hence "r" ..
with `¬¬p` show "¬¬p ∧ r" ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "hence" para indicar que se tiene por el hecho anterior,
· `...` para referenciar un hecho y
· "with P show Q" para indicar que con el hecho anterior junto con el
hecho P se demuestra Q. *}

-- "La demostración automática es"
lemma ejemplo_2_3:
assumes "p"
"¬¬(q ∧ r)"
shows "¬¬p ∧ r"
using assms
by auto

text {* Se puede demostrar hacia atrás *}

lemma ejemplo_2_4:
assumes "p"
"¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof (rule conjI)
show "¬¬p" using assms(1) by (rule notnotI)
next
have "q ∧ r" using assms(2) by (rule notnotD)
thus "r" by (rule conjunct2)
qed

text {* Se puede eliminar las reglas en la demostración anterior, como
sigue: *}

lemma ejemplo_2_5:
assumes "p"
"¬¬(q ∧ r)"
shows "¬¬p ∧ r"
proof
show "¬¬p" using assms(1) ..
next
have "q ∧ r" using assms(2) by (rule notnotD)
thus "r" ..
qed

subsection {* Regla de eliminación del condicional *}

text {*
La regla de eliminación del condicional es la regla del modus ponens
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
*}

text {*
Ejemplo 3. (p. 6) Demostrar que
¬p ∧ q, ¬p ∧ q ⟶ r ∨ ¬p ⊢ r ∨ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_3_1:
assumes 1: "¬p ∧ q" and
2: "¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
proof -
show "r ∨ ¬p" using 2 1 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejemplo_3_2:
assumes "¬p ∧ q"
"¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
proof -
show "r ∨ ¬p" using assms(2,1) ..
qed

-- "La demostración automática es"
lemma ejemplo_3_3:
assumes "¬p ∧ q"
"¬p ∧ q ⟶ r ∨ ¬p"
shows "r ∨ ¬p"
using assms
by auto

text {*
Ejemplo 4 (p. 6) Demostrar que
p, p ⟶ q, p ⟶ (q ⟶ r) ⊢ r
*}

-- "La demostración detallada es"
lemma ejemplo_4_1:
assumes 1: "p" and
2: "p ⟶ q" and
3: "p ⟶ (q ⟶ r)"
shows "r"
proof -
have 4: "q" using 2 1 by (rule mp)
have 5: "q ⟶ r" using 3 1 by (rule mp)
show 6: "r" using 5 4 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejemplo_4_2:
assumes "p"
"p ⟶ q"
"p ⟶ (q ⟶ r)"
shows "r"
proof -
have "q" using assms(2,1) ..
have "q ⟶ r" using assms(3,1) ..
thus "r" using `q` ..
qed

-- "La demostración automática es"
lemma ejemplo_4_3:
"⟦p; p ⟶ q; p ⟶ (q ⟶ r)⟧ ⟹ r"
by auto

subsection {* Regla derivada del modus tollens *}

text {*
Para ajustarnos al tema de LI vamos a introducir la regla del modus
tollens
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
aunque, de momento, sin detallar su demostración.
*}

lemma mt: "⟦F ⟶ G; ¬G⟧ ⟹ ¬F"
by auto

text {*
Ejemplo 5 (p. 7). Demostrar
p ⟶ (q ⟶ r), p, ¬r ⊢ ¬q
*}

-- "La demostración detallada es"
lemma ejemplo_5_1:
assumes 1: "p ⟶ (q ⟶ r)" and
2: "p" and
3: "¬r"
shows "¬q"
proof -
have 4: "q ⟶ r" using 1 2 by (rule mp)
show "¬q" using 4 3 by (rule mt)
qed

-- "La demostración estructurada es"
lemma ejemplo_5_2:
assumes "p ⟶ (q ⟶ r)"
"p"
"¬r"
shows "¬q"
proof -
have "q ⟶ r" using assms(1,2) ..
thus "¬q" using assms(3) by (rule mt)
qed

-- "La demostración automática es"
lemma ejemplo_5_3:
assumes "p ⟶ (q ⟶ r)"
"p"
"¬r"
shows "¬q"
using assms
by auto

text {*
Ejemplo 6. (p. 7) Demostrar
¬p ⟶ q, ¬q ⊢ p
*}

-- "La demostración detallada es"
lemma ejemplo_6_1:
assumes 1: "¬p ⟶ q" and
2: "¬q"
shows "p"
proof -
have 3: "¬¬p" using 1 2 by (rule mt)
show "p" using 3 by (rule notnotD)
qed

-- "La demostración estructurada es"
lemma ejemplo_6_2:
assumes "¬p ⟶ q"
"¬q"
shows "p"
proof -
have "¬¬p" using assms(1,2) by (rule mt)
thus "p" by (rule notnotD)
qed

-- "La demostración automática es"
lemma ejemplo_6_3:
"⟦¬p ⟶ q; ¬q⟧ ⟹ p"
by auto

text {*
Ejemplo 7. (p. 7) Demostrar
p ⟶ ¬q, q ⊢ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_7_1:
assumes 1: "p ⟶ ¬q" and
2: "q"
shows "¬p"
proof -
have 3: "¬¬q" using 2 by (rule notnotI)
show "¬p" using 1 3 by (rule mt)
qed

-- "La demostración detallada es"
lemma ejemplo_7_2:
assumes "p ⟶ ¬q"
"q"
shows "¬p"
proof -
have "¬¬q" using assms(2) by (rule notnotI)
with assms(1) show "¬p" by (rule mt)
qed

-- "La demostración estructurada es"
lemma ejemplo_7_3:
"⟦p ⟶ ¬q; q⟧ ⟹ ¬p"
by auto

subsection {* Regla de introducción del condicional *}

text {*
La regla de introducción del condicional es
· impI: (P ⟹ Q) ⟹ P ⟶ Q
*}

text {*
Ejemplo 8. (p. 8) Demostrar
p ⟶ q ⊢ ¬q ⟶ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_8_1:
assumes 1: "p ⟶ q"
shows "¬q ⟶ ¬p"
proof -
{ assume 2: "¬q"
have "¬p" using 1 2 by (rule mt) }
thus "¬q ⟶ ¬p" by (rule impI)
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "{ ... }" para representar una caja. *}

-- "La demostración estructurada es"
lemma ejemplo_8_2:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
proof
assume "¬q"
with assms show "¬p" by (rule mt)
qed

-- "La demostración automática es"
lemma ejemplo_8_3:
assumes "p ⟶ q"
shows "¬q ⟶ ¬p"
using assms
by auto

text {*
Ejemplo 9. (p. 9) Demostrar
¬q ⟶ ¬p ⊢ p ⟶ ¬¬q
*}

-- "La demostración detallada es"
lemma ejemplo_9_1:
assumes 1: "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
proof -
{ assume 2: "p"
have 3: "¬¬p" using 2 by (rule notnotI)
have "¬¬q" using 1 3 by (rule mt) }
thus "p ⟶ ¬¬q" by (rule impI)
qed

-- "La demostración estructurada es"
lemma ejemplo_9_2:
assumes "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
proof
assume "p"
hence "¬¬p" by (rule notnotI)
with assms show "¬¬q" by (rule mt)
qed

-- "La demostración automática es"
lemma ejemplo_9_3:
assumes "¬q ⟶ ¬p"
shows "p ⟶ ¬¬q"
using assms
by auto

text {*
Ejemplo 10 (p. 9). Demostrar
⊢ p ⟶ p
*}

-- "La demostración detallada es"
lemma ejemplo_10_1:
"p ⟶ p"
proof -
{ assume 1: "p"
have "p" using 1 by this }
thus "p ⟶ p" by (rule impI)
qed

-- "La demostración estructurada es"
lemma ejemplo_10_2:
"p ⟶ p"
proof (rule impI)
qed

-- "La demostración automática es"
lemma ejemplo_10_3:
"p ⟶ p"
by auto

text {*
Ejemplo 11 (p. 10) Demostrar
⊢ (q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))
*}

-- "La demostración detallada es"
lemma ejemplo_11_1:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof -
{ assume 1: "q ⟶ r"
{ assume 2: "¬q ⟶ ¬p"
{ assume 3: "p"
have 4: "¬¬p" using 3 by (rule notnotI)
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
have "r" using 1 6 by (rule mp) }
hence "p ⟶ r" by (rule impI) }
hence "(¬q ⟶ ¬p) ⟶ p ⟶ r" by (rule impI) }
thus "(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ p ⟶ r)" by (rule impI)
qed

-- "La demostración hacia atrás es"
lemma ejemplo_11_2:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof (rule impI)
assume 1: "q ⟶ r"
show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
proof (rule impI)
assume 2: "¬q ⟶ ¬p"
show "p ⟶ r"
proof (rule impI)
assume 3: "p"
have 4: "¬¬p" using 3 by (rule notnotI)
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
show "r" using 1 6 by (rule mp)
qed
qed
qed

-- "La demostración hacia atrás con reglas implícitas es"
lemma ejemplo_11_3:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof
assume 1: "q ⟶ r"
show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
proof
assume 2: "¬q ⟶ ¬p"
show "p ⟶ r"
proof
assume 3: "p"
have 4: "¬¬p" using 3 ..
have 5: "¬¬q" using 2 4 by (rule mt)
have 6: "q" using 5 by (rule notnotD)
show "r" using 1 6 ..
qed
qed
qed

-- "La demostración sin etiquetas es"
lemma ejemplo_11_4:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
proof
assume "q ⟶ r"
show "(¬q ⟶ ¬p) ⟶ (p ⟶ r)"
proof
assume "¬q ⟶ ¬p"
show "p ⟶ r"
proof
assume "p"
hence "¬¬p" ..
with `¬q ⟶ ¬p` have "¬¬q" by (rule mt)
hence "q" by (rule notnotD)
with `q ⟶ r` show "r" ..
qed
qed
qed

-- "La demostración automática es"
lemma ejemplo_11_5:
"(q ⟶ r) ⟶ ((¬q ⟶ ¬p) ⟶ (p ⟶ r))"
by auto

subsection {* Reglas de la disyunción *}

text {*
Las reglas de la introducción de la disyunción son
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
La regla de elimación de la disyunción es
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
*}

text {*
Ejemplo 12 (p. 11). Demostrar
p ∨ q ⊢ q ∨ p
*}

-- "La demostración detallada es"
lemma ejemplo_12_1:
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

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "moreover" para separar los bloques y
· "ultimately" para unir los resultados de los bloques. *}

-- "La demostración detallada con reglas implícitas es"
lemma ejemplo_12_2:
assumes "p ∨ q"
shows "q ∨ p"
proof -
note `p ∨ q`
moreover
{ assume "p"
hence "q ∨ p" .. }
moreover
{ assume "q"
hence "q ∨ p" .. }
ultimately show "q ∨ p" ..
qed

text {*
Nota sobre el lenguaje: En la demostración anterior se ha usado
· "note" para copiar un hecho. *}

-- "La demostración hacia atrás es"
lemma ejemplo_12_3:
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 3: "q"
show "q ∨ p" using 3 by (rule disjI1) }
qed

-- "La demostración hacia atrás con reglas implícitas es"
lemma ejemplo_12_4:
assumes "p ∨ q"
shows "q ∨ p"
using assms
proof
{ assume "p"
thus "q ∨ p" .. }
next
{ assume "q"
thus "q ∨ p" .. }
qed

-- "La demostración automática es"
lemma ejemplo_12_5:
assumes "p ∨ q"
shows "q ∨ p"
using assms
by auto

text {*
Ejemplo 13. (p. 12) Demostrar
q ⟶ r ⊢ p ∨ q ⟶ p ∨ r
*}

-- "La demostración detallada es"
lemma ejemplo_13_1:
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

-- "La demostración estructurada es"
lemma ejemplo_13_2:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
proof
assume "p ∨ q"
thus "p ∨ r"
proof
{ assume "p"
thus "p ∨ r" .. }
next
{ assume "q"
have "r" using assms `q` ..
thus "p ∨ r" .. }
qed
qed

-- "La demostración automática es"
lemma ejemplo_13_3:
assumes "q ⟶ r"
shows "p ∨ q ⟶ p ∨ r"
using assms
by auto

subsection {* Regla de copia *}

text {*
Ejemplo 14 (p. 13). Demostrar
⊢ p ⟶ (q ⟶ p)
*}

-- "La demostración detallada es"
lemma ejemplo_14_1:
"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

-- "La demostración estructurada es"
lemma ejemplo_14_2:
"p ⟶ (q ⟶ p)"
proof
assume "p"
thus "q ⟶ p" ..
qed

-- "La demostración automática es"
lemma ejemplo_14_3:
"p ⟶ (q ⟶ p)"
by auto

subsection {* Reglas de la negación *}

text {*
La regla de eliminación de lo falso es
· FalseE: False ⟹ P
La regla de eliminación de la negación es
· notE: ⟦¬P; P⟧ ⟹ R
La regla de introducción de la negación es
· notI: (P ⟹ False) ⟹ ¬P
*}

text {*
Ejemplo 15 (p. 15). Demostrar
¬p ∨ q ⊢ p ⟶ q
*}

-- "La demostración detallada es"
lemma ejemplo_15_1:
assumes 1: "¬p ∨ q"
shows "p ⟶ q"
proof (rule impI)
assume 2: "p"
note 1
thus "q"
proof (rule disjE)
{ assume 3: "¬p"
show "q" using 3 2 by (rule notE) }
next
{ assume 4: "q"
show "q" using 4 by this}
qed
qed

-- "La demostración estructurada es"
lemma ejemplo_15_2:
assumes "¬p ∨ q"
shows "p ⟶ q"
proof
assume "p"
note `¬p ∨ q`
thus "q"
proof
{ assume "¬p"
thus "q" using `p` .. }
next
{ assume "q"
thus "q" . }
qed
qed

-- "La demostración automática es"
lemma ejemplo_15_3:
assumes "¬p ∨ q"
shows "p ⟶ q"
using assms
by auto

text {*
Ejemplo 16 (p. 16). Demostrar
p ⟶ q, p ⟶ ¬q ⊢ ¬p
*}

-- "La demostración detallada es"
lemma ejemplo_16_1:
assumes 1: "p ⟶ q" and
2: "p ⟶ ¬q"
shows "¬p"
proof (rule notI)
assume 3: "p"
have 4: "q" using 1 3 by (rule mp)
have 5: "¬q" using 2 3 by (rule mp)
show False using 5 4 by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_16_2:
assumes "p ⟶ q"
"p ⟶ ¬q"
shows "¬p"
proof
assume "p"
have "q" using assms(1) `p` ..
have "¬q" using assms(2) `p` ..
thus False using `q` ..
qed

-- "La demostración automática es"
lemma ejemplo_16_3:
assumes "p ⟶ q"
"p ⟶ ¬q"
shows "¬p"
using assms
by auto

subsection {* Reglas del bicondicional *}

text {*
La regla de introducción del bicondicional es
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P ⟷ Q
Las reglas de eliminación del bicondicional son
· iffD1: ⟦Q ⟷ P; Q⟧ ⟹ P
· iffD2: ⟦P ⟷ Q; Q⟧ ⟹ P
*}

text {*
Ejemplo 17 (p. 17) Demostrar
*}

-- "La demostración detallada es"
lemma ejemplo_17_1:
"(p ∧ q) ⟷ (q ∧ p)"
proof (rule iffI)
{ assume 1: "p ∧ q"
have 2: "p" using 1 by (rule conjunct1)
have 3: "q" using 1 by (rule conjunct2)
show "q ∧ p" using 3 2 by (rule conjI) }
next
{ assume 4: "q ∧ p"
have 5: "q" using 4 by (rule conjunct1)
have 6: "p" using 4 by (rule conjunct2)
show "p ∧ q" using 6 5 by (rule conjI) }
qed

-- "La demostración estructurada es"
lemma ejemplo_17_2:
"(p ∧ q) ⟷ (q ∧ p)"
proof
{ assume 1: "p ∧ q"
have "p" using 1 ..
have "q" using 1 ..
show "q ∧ p" using `q` `p` .. }
next
{ assume 2: "q ∧ p"
have "q" using 2 ..
have "p" using 2 ..
show "p ∧ q" using `p` `q` .. }
qed

-- "La demostración automática es"
lemma ejemplo_17_3:
"(p ∧ q) ⟷ (q ∧ p)"
by auto

text {*
Ejemplo 18 (p. 18). Demostrar
p ⟷ q, p ∨ q ⊢ p ∧ q
*}

-- "La demostración detallada es"
lemma ejemplo_18_1:
assumes 1: "p ⟷ q" and
2: "p ∨ q"
shows "p ∧ q"
using 2
proof (rule disjE)
{ assume 3: "p"
have 4: "q" using 1 3 by (rule iffD1)
show "p ∧ q" using 3 4 by (rule conjI) }
next
{ assume 5: "q"
have 6: "p" using 1 5 by (rule iffD2)
show "p ∧ q" using 6 5 by (rule conjI) }
qed

-- "La demostración estructurada es"
lemma ejemplo_18_2:
assumes "p ⟷ q"
"p ∨ q"
shows "p ∧ q"
using assms(2)
proof
{ assume "p"
with assms(1) have "q" ..
with `p` show "p ∧ q" .. }
next
{ assume "q"
with assms(1) have "p" ..
thus "p ∧ q" using `q` .. }
qed

-- "La demostración automática es"
lemma ejemplo_18_3:
assumes "p ⟷ q"
"p ∨ q"
shows "p ∧ q"
using assms
by auto

subsection {* Reglas derivadas *}

subsubsection {* Regla del modus tollens *}

text {*
Ejemplo 19 (p. 20) Demostrar la regla del modus tollens a partir de
las reglas básicas.
*}

-- "La demostración detallada es"
lemma ejemplo_20_1:
assumes 1: "F ⟶ G" and
2: "¬G"
shows "¬F"
proof (rule notI)
assume 3: "F"
have 4: "G" using 1 3 by (rule mp)
show False using 2 4 by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_20_2:
assumes "F ⟶ G"
"¬G"
shows "¬F"
proof
assume "F"
with assms(1) have "G" ..
with assms(2) show False ..
qed

-- "La demostración automática es"
lemma ejemplo_20_3:
assumes "F ⟶ G"
"¬G"
shows "¬F"
using assms
by auto

subsubsection {* Regla de la introducción de la doble negación *}

text {*
Ejemplo 21 (p. 21) Demostrar la regla de introducción de la doble
negación a partir de las reglas básicas.
*}

-- "La demostración detallada es"
lemma ejemplo_21_1:
assumes 1: "F"
shows "¬¬F"
proof (rule notI)
assume 2: "¬F"
show False using 2 1 by (rule notE)
qed

-- "La demostración estructurada es"
lemma ejemplo_21_2:
assumes "F"
shows "¬¬F"
proof
assume "¬F"
thus False using assms ..
qed

-- "La demostración automática es"
lemma ejemplo_21_3:
assumes "F"
shows "¬¬F"
using assms
by auto

subsubsection {* Regla de reducción al absurdo *}

text {*
La regla de reducción al absurdo en Isabelle se correponde con la
regla clásica de contradicción
· ccontr: (¬P ⟹ False) ⟹ P
*}

subsubsection {* Ley del tercio excluso *}

text {*
La ley del tercio excluso es
· excluded_middle: ¬P ∨ P
*}

text {*
Ejemplo 22 (p. 23). Demostrar la ley del tercio excluso a partir de
las reglas básicas.
*}

-- "La demostración detallada es"
lemma ejemplo_22_1:
"F ∨ ¬F"
proof (rule ccontr)
assume 1: "¬(F ∨ ¬F)"
thus False
proof (rule notE)
show "F ∨ ¬F"
proof (rule disjI2)
show "¬F"
proof (rule notI)
assume 2: "F"
hence 3: "F ∨ ¬F" by (rule disjI1)
show False using 1 3 by (rule notE)
qed
qed
qed
qed

-- "La demostración estructurada es"
lemma ejemplo_22_2:
"F ∨ ¬F"
proof (rule ccontr)
assume "¬(F ∨ ¬F)"
thus False
proof (rule notE)
show "F ∨ ¬F"
proof (rule disjI2)
show "¬F"
proof (rule notI)
assume "F"
hence "F ∨ ¬F" ..
with `¬(F ∨ ¬F)`show False ..
qed
qed
qed
qed

-- "La demostración automática es"
lemma ejemplo_22_3:
"F ∨ ¬F"
using assms
by auto

text {*
Ejemplo 23 (p. 24). Demostrar
p ⟶ q ⊢ ¬p ∨ q
*}

-- "La demostración detallada es"
lemma ejemplo_23_1:
assumes 1: "p ⟶ q"
shows "¬p ∨ q"
proof -
have "¬p ∨ p" by (rule excluded_middle)
thus "¬p ∨ q"
proof (rule disjE)
{ assume "¬p"
thus "¬p ∨ q" by (rule disjI1) }
next
{ assume 2: "p"
have "q" using 1 2 by (rule mp)
thus "¬p ∨ q" by (rule disjI2) }
qed
qed

-- "La demostración estructurada es"
lemma ejemplo_23_2:
assumes "p ⟶ q"
shows "¬p ∨ q"
proof -
have "¬p ∨ p" ..
thus "¬p ∨ q"
proof
{ assume "¬p"
thus "¬p ∨ q" .. }
next
{ assume "p"
with assms have "q" ..
thus "¬p ∨ q" .. }
qed
qed

-- "La demostración automática es"
lemma ejemplo_23_3:
assumes "p ⟶ q"
shows "¬p ∨ q"
using assms
by auto

subsection {* Demostraciones por contradicción *}

text {*
Ejemplo 24. Demostrar que
¬p, p ∨ q ⊢ q
*}

-- "La demostración detallada es"
lemma ejemplo_24_1:
assumes "¬p"
"p ∨ q"
shows "q"
using `p ∨ q`
proof (rule disjE)
assume "p"
with assms(1) show "q" by contradiction
next
assume "q"
thus "q" by assumption
qed

-- "La demostración estructurada es"
lemma ejemplo_24_2:
assumes "¬p"
"p ∨ q"
shows "q"
using `p ∨ q`
proof
assume "p"
with assms(1) show "q" ..
next
assume "q"
thus "q" .
qed

-- "La demostración automática es"
lemma ejemplo_24_3:
assumes "¬p"
"p ∨ q"
shows "q"
using assms
by auto

end
</source>

Tema 2

2018-02-27T05:50:04Z

Jalonso: Página creada con '<source lang="isar"> chapter {* Tema 2: Deducción natural proposicional con Isabelle/HOL *} theory T2 imports Main begin text {* En este tema se presentan los ejemplos del...'

Lógica matemática y fundamentos (2017-18)

2018-02-27T05:40:26Z

Jalonso:

Archivo:R2E0a.png

2018-02-19T11:39:38Z

Jalonso:

Relación 2

2018-02-19T11:38:52Z

Jalonso: /* Relación 2: Deducción natural en lógica proposicional */

=== Relación 2: Deducción natural en lógica proposicional ===

----
'''Ejercicio 0.''' Demostrar mediante deducción natural:
: {p → q, p → r} ⊧ p → r
----

'''Solución:'''

[[Archivo:R2E0a.png]]

----
'''Ejercicio 1.''' Demostrar mediante deducción natural:
: (p → q) → r ⊧ p → (q → r)
----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar mediante deducción natural:
: (p → q) ∧ (p → r) ⊧ p → q ∧ r
----

'''Solución:'''

----
'''Ejercicio 3.''' Demostrar mediante deducción natural:
: (p → r) ∧ (q → r) ⊧ p ∨ q → r
----

'''Solución:'''

----
'''Ejercicio 4.''' Demostrar mediante deducción natural:
: {p → r, r → ¬ q} ⊧ ¬(p ∧ q)
----

'''Solución:'''

----
'''Ejercicio 5.''' Demostrar mediante deducción natural:
: ¬p ∧ ¬q ⊧ ¬(p ∨ q)
----

'''Solución:'''

----
'''Ejercicio 6.''' Demostrar mediante deducción natural:
: ⊧ ((p → q) → p)
----

'''Solución:'''

----
'''Ejercicio 7.''' Demostrar mediante deducción natural:
: (p → q) ∨ (q → p)
----

'''Solución:'''

----
'''Ejercicio 8.''' Demostrar mediante deducción natural:
: ¬(¬p ∧ ¬q) ⊧ p ∨ q
----

'''Solución:'''