chapter {* Tema 8b: 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) ..
then show "¬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) }
then show "∀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) ..
then show "¬(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)
then show "∃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 ..
then show "∃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)
then show 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) ..
then have "Q a" using `P a` ..
then show "∃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)"
then have "∃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)"
then have "∃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))"
then show "∃x. ¬P(x)" by (rule ejemplo_5_1a)
next
assume "∃x. ¬P(x)"
then show "¬(∀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)
then show "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)
then show "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 ..
then show "P(a)" ..
qed
next
show "∀x. Q(x)"
proof
fix a
have "P(a) ∧ Q(a)" using assms ..
then show "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)
then have "P(a)" by (rule allE)
have "∀x. Q(x)" using assms by (rule conjunct2)
then have "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 ..
then have "P(a)" by (rule allE)
have "∀x. Q(x)" using assms ..
then have "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)"
then show "(∀x. P(x)) ∧ (∀x. Q(x))" by (rule ejemplo_6_1a)
next
assume "(∀x. P(x)) ∧ (∀x. Q(x))"
then show "∀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)
then have "P(a) ∨ Q(a)" by (rule disjI1)
then show "∃x. P(x) ∨ Q(x)" by (rule exI)
next
assume "∃x. Q(x)"
then obtain a where "Q(a)" by (rule exE)
then have "P(a) ∨ Q(a)" by (rule disjI2)
then show "∃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)" ..
then have "P(a) ∨ Q(a)" ..
then show "∃x. P(x) ∨ Q(x)" ..
next
assume "∃x. Q(x)"
then obtain a where "Q(a)" ..
then have "P(a) ∨ Q(a)" ..
then show "∃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)
then show "(∃x. P(x)) ∨ (∃x. Q(x))"
proof (rule disjE)
assume "P(a)"
then have "∃x. P(x)" by (rule exI)
then show "(∃x. P(x)) ∨ (∃x. Q(x))" by (rule disjI1)
next
assume "Q(a)"
then have "∃x. Q(x)" by (rule exI)
then show "(∃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 ..
then show "(∃x. P(x)) ∨ (∃x. Q(x))"
proof
assume "P(a)"
then have "∃x. P(x)" ..
then show "(∃x. P(x)) ∨ (∃x. Q(x))" ..
next
assume "Q(a)"
then have "∃x. Q(x)" ..
then show "(∃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))"
then show "∃x. P(x) ∨ Q(x)" by (rule ejemplo_7_1a)
next
assume "∃x. P(x) ∨ Q(x)"
then show "(∃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)
then have "∃x. P(x,b)" by (rule exI)
then show "∃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)" ..
then have "∃x. P(x,b)" ..
then show "∃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)
then have "∃y. P(a,y)" by (rule exI)
then show "∃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)" ..
then have "∃y. P(a,y)" ..
then show "∃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)"
then show "∃y x. P(x,y)" by (rule ejemplo_8_1a)
next
assume "∃y x. P(x,y)"
then show "∃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
