Relación 10
De Razonamiento automático (2013-14)
Revisión del 20:49 25 ene 2014 de Marescpla (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"
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
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
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
⊢ ((p ⟶ q) ⟶ p) ⟶ p
------------------------------------------------------------------ *}
-- "diecabmen1"
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
--"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
text {* ---------------------------------------------------------------
Ejercicio 7. Demostrar
¬q ⟶ ¬p ⊢ p ⟶ q
------------------------------------------------------------------ *}
-- "diecabmen1"
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
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
text {* ---------------------------------------------------------------
Ejercicio 9. Demostrar
¬(¬p ∨ ¬q) ⊢ p ∧ q
------------------------------------------------------------------ *}
-- "diecabmen1"
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
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
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
end