Relación 10
De Razonamiento automático (2013-14)
Revisión del 01:21 27 ene 2014 de Pabflomar (discusión | contribuciones)
header {* R10: Deducción natural proposicional *}
theory R10
imports Main
begin
text {*
---------------------------------------------------------------------
El objetivo de esta relación es lemas usando sólo las reglas básicas
de deducción natural de la lógica proposicional.
Los ejercicios son los de la asignatura de "Lógica informática" que se
encuentran en http://goo.gl/yrPLn
Las reglas básicas de la deducción natural son las siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
· excluded_middle: ¬P ∨ P
---------------------------------------------------------------------
*}
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
p ∨ q, ¬q ⊢ p
------------------------------------------------------------------ *}
--"marescpla, pabflomar"
lemma 01:
assumes 1: "p ∨ q"
and 2: "¬q"
shows "p"
using 1
proof (rule disjE)
{assume "p"
then show "p".}
next
{assume "q"
with 2 show "p" by (rule notE)}
qed
--"diecabmen1 maresccas4"
lemma Ejercicio_1:
assumes "p ∨ q"
"¬q"
shows "p"
using assms(1)
proof (rule disjE)
assume "p"
then show "p" .
next
assume "q"
with `¬q` show "p" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 2. Demostrar
p ∧ q ⊢ ¬(¬p ∨ ¬q)
------------------------------------------------------------------ *}
--"marescpla, pabflomar"
lemma 02:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof (rule ccontr)
assume "¬¬(¬p ∨ ¬q)"
then have 1: "(¬p ∨ ¬q)" by (rule notnotD)
show "False"
using 1
proof (rule disjE)
{assume I: "¬p"
have "p" using assms(1) by (rule conjunct1)
with I show "False"..}
{assume II: "¬q"
have "q" using assms(1) by (rule conjunct2)
with II show "False" ..}
qed
qed
--"diecabmen1 maresccas4"
lemma Ejercicio_2:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof
assume 1: "¬p ∨ ¬q"
show False
using 1
proof (rule disjE)
assume "¬p"
have "p" using assms ..
with `¬p` show False ..
next
assume "¬q"
have "q" using assms ..
with `¬q` show False ..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 3. Demostrar
¬(p ∨ q) ⊢ ¬p ∧ ¬q
------------------------------------------------------------------ *}
-- "maresccas4"
lemma
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof
{ assume "p"
then have "p ∨ q" ..
with `¬(p ∨ q)` have False ..}
thus "¬p" ..
next
{ assume "q"
then have "p ∨ q" ..
with `¬(p ∨ q)` have False ..}
thus "¬q" ..
qed
-- "diecabmen1 pabflomar"
lemma Ejercicio_3:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof -
{ assume "p"
then have "p ∨ q" ..
with assms have False ..}
then have "¬p" ..
{ assume "q"
then have "p ∨ q" ..
with assms have False ..}
then have "¬q" ..
with `¬p` show "¬p ∧ ¬q" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 4. Demostrar
¬p ∧ ¬q ⊢ ¬(p ∨ q)
------------------------------------------------------------------ *}
-- "maresccas4"
lemma
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume "p ∨ q"
show False
using `p ∨ q`
proof
assume "p"
have "¬p" using `¬p ∧ ¬q` ..
thus False using `p` ..
next
assume "q"
have "¬q" using `¬p ∧ ¬q` ..
thus False using `q` ..
qed
qed
-- "diecabmen1"
lemma Ejercicio_4:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume "p ∨ q"
show False
using `p ∨ q`
proof
assume "p"
have "¬p" using assms ..
then show False using `p` ..
next
assume "q"
have "¬q" using assms ..
then show False using `q` ..
qed
qed
--"marescpla"
lemma 04:
assumes 1:"¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule ccontr)
have 2: "¬p" using 1 by (rule conjunct1)
have 3: "¬q" using 1 by (rule conjunct2)
assume "¬¬(p ∨ q)"
then have 4:"(p ∨ q)" by (rule notnotD)
then show False
proof (rule disjE)
note 4
{assume "p"
with 2 show False ..}
{assume "q"
with 3 show False ..}
qed
qed
-- "pabflomar"
lemma ej4_pfm:
assumes 0:"¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof
assume 1:"p ∨ q"
show False
using 1
proof
assume 1:"p"
have 2: "¬p" using 0 by (rule conjunct1)
then show False using `p` ..
next
assume 1:"q"
have 2: "¬q" using 0 by (rule conjunct2)
then show False using `q` ..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
¬p ∨ ¬q ⊢ ¬(p ∧ q)
------------------------------------------------------------------ *}
-- "maresccas4 diecabmen1"
lemma
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof
assume "p ∧ q"
show False
using `¬p ∨ ¬q`
proof
assume "¬p"
have "p" using `p ∧ q` ..
with `¬p`show False ..
next
assume "¬q"
have "q" using `p ∧ q` ..
with `¬q` show False ..
qed
qed
--"marescpla"
lemma 05:
assumes 1:"¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule ccontr)
assume "¬¬(p ∧ q)"
then have 4:"(p ∧ q)" by (rule notnotD)
have p using 4 by (rule conjunct1)
have q using 4 by (rule conjunct2)
show False
using 1
proof (rule disjE)
{assume "¬p"
then show False using `p` ..}
{assume "¬q"
then show False using `q`..}
qed
qed
-- "pabflomar"
lemma ej5_pfm:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof
assume "p ∧ q"
show False
using `¬p ∨ ¬q`
proof
assume "¬p"
have "p" using `p ∧ q` by (rule conjunct1)
with `¬p` show False by (rule notE)
next
assume "¬q"
have "q" using `p ∧ q` by (rule conjunct2)
with `¬q` show False by (rule notE)
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}
-- "diecabmen1 maresccas4 pabflomar"
lemma Ejercicio_6:
shows "((p ⟶ q) ⟶ p) ⟶ p"
proof
assume "(p ⟶ q) ⟶ p"
show "p"
proof (rule ccontr)
assume "¬p"
with `(p ⟶ q) ⟶ p` have "¬(p ⟶ q)" by (rule mt)
{ assume "p"
with `¬p` have False ..
then have "q" ..}
then have "p ⟶ q" ..
with `¬(p ⟶ q)` show False ..
qed
qed
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "diecabmen1 pabflomar"
lemma Ejercicio_7:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
{ assume "¬q"
with assms have "¬p" ..
then have False using `p` ..}
then show "q" by (rule ccontr)
qed
--"marescpla"
lemma 07:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
{assume 1: "p"
{assume "¬q"
with assms have "¬p" ..
then have "False" using 1 ..}
then have "¬¬q" by (rule notI)
then show "q" by (rule notnotD)}
qed
-- "maresccas4"
lemma
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof
assume "p"
then have "¬¬p" by (rule notnotI)
with assms(1) have "¬¬q" by (rule mt)
then show "q" by (rule notnotD)
qed
text {* ---------------------------------------------------------------
Ejercicio 8. Demostrar
¬(¬p ∧ ¬q) ⊢ p ∨ q
------------------------------------------------------------------ *}
-- "diecabmen1"
lemma Ejercicio_8:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
have "¬p ∨ p" ..
{ assume "p"
then have "p ∨ q" ..}
{ assume "¬p"
have "¬q ∨ q" ..
{ assume "q"
then have "p ∨ q" ..}
{ assume "¬q"
with `¬p` have "¬p ∧ ¬q" ..
with assms have False ..
then have "p ∨ q" ..}
with `¬q ∨ q` have "p ∨ q" using `q ⟹ p ∨ q` ..}
with `¬p ∨ p` show "p ∨ q" using `p ⟹ p ∨ q` ..
qed
--"marescpla pabflomar (No se usar otro lema sin usar el simp) maresccas4 (rule 03, en lugar de simp)"
{* Marco lleva razón. *}
lemma 08:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof (rule ccontr)
assume "¬(p ∨ q)"
then have "¬p ∧ ¬q" by (simp add: 03)
with assms show "False" ..
qed
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
-- "diecabmen1, maresccas4"
lemma Ejercicio_9:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
{ assume "¬p"
then have "¬p ∨ ¬q" ..
with assms have False ..}
then show "p" by (rule ccontr)
{ assume "¬q"
then have "¬p ∨ ¬q" ..
with assms have False ..}
then show "q" by (rule ccontr)
qed
-- "pabflomar"
lemma ej9_pfm:
assumes " ¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
have 1: "¬¬p ∧ ¬¬q" using assms by (rule ej3_pfm)
have 2: "¬¬p" using 1 by (rule conjunct1)
have 3: "¬¬q" using 1 by (rule conjunct2)
show "p" using 2 by (rule notnotD)
show "q" using 3 by (rule notnotD)
qed
text {* ---------------------------------------------------------------
Ejercicio 10. Demostrar
¬(p ∧ q) ⊢ ¬p ∨ ¬q
------------------------------------------------------------------ *}
-- "diecabmen1"
lemma Ejercicio_10:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have "¬p ∨ p" ..
{ assume "p"
have "¬q ∨ q" ..
{ assume "q"
with `p` have "p ∧ q" ..
with assms have False ..
then have "¬p ∨ ¬q" ..}
{ assume "¬q"
then have "¬p ∨ ¬q" ..}
with `¬q ∨ q` have "¬p ∨ ¬q" using `q ⟹ ¬ p ∨ ¬ q` ..}
{ assume "¬p"
then have "¬p ∨ ¬q" ..}
with `¬p ∨ p` show "¬p ∨ ¬q" using ` p ⟹ ¬ p ∨ ¬ q` ..
qed
-- "maresccas4"
lemma a10:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof
{ assume "¬p"
then have "¬p ∨ ¬q" ..
with `¬(¬p ∨ ¬q)` have False ..}
hence "¬¬p" ..
thus "p" by (rule notnotD)
{ assume "¬q"
then have "¬p ∨ ¬q" ..
with `¬(¬p ∨ ¬q)` have False ..}
hence "¬¬q" ..
thus "q" by (rule notnotD)
qed
lemma 10:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof (rule ccontr)
assume "¬(¬p ∨ ¬q)"
then have "p ∧ q" by (rule a10)
with assms(1) show False ..
qed
text {* -----
Ejercicio 9 haciendo uso del Ejercicio 10
----------*}
lemma
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule ccontr)
assume "¬(p ∧ q)"
then have "¬p ∨ ¬q" by (rule 10)
with assms(1) show False ..
qed
text {* ---------------------------------------------------------------
Ejercicio 11. Demostrar
⊢ (p ⟶ q) ∨ (q ⟶ p)
------------------------------------------------------------------ *}
-- "diecabmen1"
lemma Ejercicio_11:
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬(p ⟶ q) ∨ (p ⟶ q)" ..
{ assume "(p ⟶ q)"
then have "(p ⟶ q) ∨ (q ⟶ p)" ..}
{ assume "¬(p ⟶ q)"
{ assume "q"
{ assume "p"
have "q" using `q` .}
then have "p ⟶ q" ..
with `¬(p ⟶ q)` have False ..
then have "p" ..}
then have "q ⟶ p" ..
then have "(p ⟶ q) ∨ (q ⟶ p)" ..}
with `¬(p ⟶ q) ∨ (p ⟶ q)` show "(p ⟶ q) ∨ (q ⟶ p)" using `p ⟶ q ⟹ (p ⟶ q) ∨ (q ⟶ p)` ..
qed
-- "maresccas4"
lemma
shows "(p ⟶ q) ∨ (q ⟶ p)"
proof -
have 1:"¬(p ⟶ q) ∨ (p ⟶ q)" ..
show "(p ⟶ q) ∨ (q ⟶ p)"
using 1
proof
assume "p ⟶ q"
then show "(p ⟶ q) ∨ (q ⟶ p)" ..
next
{ assume "¬(p ⟶ q)"
{ assume "q"
{ assume "p"
have "q" using `q` .}
then have "p ⟶ q" ..
with `¬(p ⟶ q)` have False ..
then have "p" .. }
then have "q ⟶ p" ..
then show "(p ⟶ q) ∨ (q ⟶ p)" ..}
qed
qed
end