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

Ejercicio 5 (b)

2015-06-03T17:54:10Z

Jalonso:

<source lang="isar">
header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}

theory e5_2_sol
imports Main
begin

text {*
Apellidos:
Nombre:
*}

text {* Sustituye la palabra uvus por tu usuario de la Universidad de
Sevilla y graba el fichero con dicho usuario .thy
*}

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_middle:(¬P ∨ P)

· allE: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allI: (⋀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

lemma Ejercicio5:
shows "(∀x. P(x) ⟶ R(x,x)) ⟶ (∀x. ∃y. R(x,y) ∨ ¬P(y))"
proof (rule impI)
assume "∀x. P(x) ⟶ R(x,x)"
show "∀x. ∃y. R(x,y) ∨ ¬P(y)"
proof (rule allI)
fix a
have "¬P(a) ∨ P(a)" ..
then show "∃y. R(a,y) ∨ ¬P(y)"
proof (rule disjE)
assume "¬P(a)"
then have "R(a,a) ∨ ¬P(a)" by (rule disjI2)
then show "∃y. R(a,y) ∨ ¬P(y)" by (rule exI)
next
assume "P(a)"
have "P(a) ⟶ R(a,a)" using `∀x. P(x) ⟶ R(x,x)` by (rule allE)
then have "R(a,a)" using `P(a)` by (rule mp)
then have "R(a,a) ∨ ¬P(a)" by (rule disjI1)
then show "∃y. R(a,y) ∨ ¬P(y)" by (rule exI)
qed
qed
qed

end
</source>

Ejercicio 5 (b)

2015-06-03T17:53:49Z

Jalonso: Página creada con '<source lang="isar> header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *} theory e5_2_sol imports Main begin text {* Apellidos: Nombre: *} text...'

<source lang="isar>
header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}

theory e5_2_sol
imports Main
begin

text {*
Apellidos:
Nombre:
*}

text {* Sustituye la palabra uvus por tu usuario de la Universidad de
Sevilla y graba el fichero con dicho usuario .thy
*}

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_middle:(¬P ∨ P)

· allE: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allI: (⋀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

lemma Ejercicio5:
shows "(∀x. P(x) ⟶ R(x,x)) ⟶ (∀x. ∃y. R(x,y) ∨ ¬P(y))"
proof (rule impI)
assume "∀x. P(x) ⟶ R(x,x)"
show "∀x. ∃y. R(x,y) ∨ ¬P(y)"
proof (rule allI)
fix a
have "¬P(a) ∨ P(a)" ..
then show "∃y. R(a,y) ∨ ¬P(y)"
proof (rule disjE)
assume "¬P(a)"
then have "R(a,a) ∨ ¬P(a)" by (rule disjI2)
then show "∃y. R(a,y) ∨ ¬P(y)" by (rule exI)
next
assume "P(a)"
have "P(a) ⟶ R(a,a)" using `∀x. P(x) ⟶ R(x,x)` by (rule allE)
then have "R(a,a)" using `P(a)` by (rule mp)
then have "R(a,a) ∨ ¬P(a)" by (rule disjI1)
then show "∃y. R(a,y) ∨ ¬P(y)" by (rule exI)
qed
qed
qed

end
</source>

Ejercicio 5 (a)

2015-06-03T17:52:22Z

Jalonso:

Ejercicio 5 (a)

2015-06-03T17:49:58Z

Jalonso: Página creada con '<source lang="isar"> header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *} theory e5_1_sol imports Main begin text {* Apellidos: Nombre: *} tex...'

<source lang="isar">
header {* Examen de Lógica Matemática y Fundamentos (6 de abril de 2015) *}

theory e5_1_sol
imports Main
begin

text {*
Apellidos:
Nombre:
*}

text {* Sustituye la palabra uvus por tu usuario de la Universidad de
Sevilla y graba el fichero con dicho usuario .thy
*}

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: \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q
· conjunct1: P \<and> Q \<Longrightarrow> P
· conjunct2: P \<and> Q \<Longrightarrow> Q
· notnotD: \<not>\<not> P \<Longrightarrow> P
· mp: \<lbrakk>P \<longrightarrow> Q; P\<rbrakk> \<Longrightarrow> Q
· impI: (P \<Longrightarrow> Q) \<Longrightarrow> P \<longrightarrow> Q
· disjI1: P \<Longrightarrow> P \<or> Q
· disjI2: Q \<Longrightarrow> P \<or> Q
· disjE: \<lbrakk>P \<or> Q; P \<Longrightarrow> R; Q \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
· FalseE: False \<Longrightarrow> P
· notE: \<lbrakk>\<not>P; P\<rbrakk> \<Longrightarrow> R
· notI: (P \<Longrightarrow> False) \<Longrightarrow> \<not>P
· iffI: \<lbrakk>P \<Longrightarrow> Q; Q \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P = Q
· iffD1: \<lbrakk>Q = P; Q\<rbrakk> \<Longrightarrow> P
· iffD2: \<lbrakk>P = Q; Q\<rbrakk> \<Longrightarrow> P
· ccontr: (\<not>P \<Longrightarrow> False) \<Longrightarrow> P
. excluded_middle:(\<not>P \<or> P)

· allE: \<lbrakk>\<forall>x. P x; P x \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
· allI: (\<And>x. P x) \<Longrightarrow> \<forall>x. P x
· exI: P x \<Longrightarrow> \<exists>x. P x
· exE: \<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q

· refl: t = t
· subst: \<lbrakk>s = t; P s\<rbrakk> \<Longrightarrow> P t
· trans: \<lbrakk>r = s; s = t\<rbrakk> \<Longrightarrow> r = t
· sym: s = t \<Longrightarrow> t = s
· not_sym: t \<noteq> s \<Longrightarrow> s \<noteq> t
· ssubst: \<lbrakk>t = s; P s\<rbrakk> \<Longrightarrow> P t
· box_equals: \<lbrakk>a = b; a = c; b = d\<rbrakk> \<Longrightarrow> a: = d
· arg_cong: x = y \<Longrightarrow> f x = f y
· fun_cong: f = g \<Longrightarrow> f x = g x
· cong: \<lbrakk>f = g; x = y\<rbrakk> \<Longrightarrow> f x = g y
*}

text {*
Se usarán las reglas notnotI y mt que demostramos a continuación.
*}

lemma notnotI: "P \<Longrightarrow> \<not>\<not> P"
by auto

lemma mt: "\<lbrakk>F \<longrightarrow> G; \<not>G\<rbrakk> \<Longrightarrow> \<not>F"
by auto

lemma Ejercicio5:
shows "(\<exists>x. \<forall>y. \<not>(P(y) \<longrightarrow> R(x,y))) \<longrightarrow> \<not>(\<forall>x. P(x) \<longrightarrow> R(x,x))"
proof (rule impI)
assume "\<exists>x. \<forall>y. \<not>(P(y) \<longrightarrow> R(x,y))"
then obtain a where "\<forall>y. \<not>(P(y) \<longrightarrow> R(a,y))" by (rule exE)
show "\<not>(\<forall>x. P(x) \<longrightarrow> R(x,x))"
proof (rule notI)
assume "\<forall>x. P(x) \<longrightarrow> R(x,x)"
then have "P(a) \<longrightarrow> R(a,a)" by (rule allE)
have "\<not>(P(a) \<longrightarrow> R(a,a))" using `\<forall>y. \<not>(P(y) \<longrightarrow> R(a,y))` by (rule allE)
then show False using `P(a) \<longrightarrow> R(a,a)` by (rule notE)
qed
qed

end
</source>

Ejercicio 4 (b)

2015-06-03T17:48:40Z

Jalonso: Página creada con '<source lang="haskell"> -- --------------------------------------------------------------------- -- Gramática de fórmulas prosicionales -- -- --...'

<source lang="haskell">
-- ---------------------------------------------------------------------
-- Gramática de fórmulas prosicionales --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Se definen los siguientes tipos de datos:
-- * SimboloProposicional para representar los símbolos de proposiciones
-- * Prop para representar las fórmulas proposicionales usando los
-- constructores Atom, Neg, Conj, Disj, Impl y Equi para las fórmulas
-- atómicas, negaciones, conjunciones, implicaciones y equivalencias,
-- respectivamente.
-- ---------------------------------------------------------------------

type SimboloProposicional = String

data Prop = Atom SimboloProposicional
| Neg Prop
| Conj Prop Prop
| Disj Prop Prop
| Impl Prop Prop
| Equi Prop Prop
deriving (Eq,Ord)

instance Show Prop where
show (Atom p) = p
show (Neg p) = "no " ++ show p
show (Conj p q) = "(" ++ show p ++ " /\\ " ++ show q ++ ")"
show (Disj p q) = "(" ++ show p ++ " \\/ " ++ show q ++ ")"
show (Impl p q) = "(" ++ show p ++ " --> " ++ show q ++ ")"
show (Equi p q) = "(" ++ show p ++ " <--> " ++ show q ++ ")"

-- ---------------------------------------------------------------------
-- Se definen las siguientes fórmulas proposicionales
-- atómicas: p, p1, p2, q, r, s, t y u.
-- ---------------------------------------------------------------------

p, p1, p2, q, r, s, t, u :: Prop
p = Atom "p"
p1 = Atom "p1"
p2 = Atom "p2"
q = Atom "q"
r = Atom "r"
s = Atom "s"
t = Atom "t"
u = Atom "u"

-- ---------------------------------------------------------------------
-- Se define la función
-- no :: Prop -> Prop
-- tal que (no f) es la negación de f.
-- ---------------------------------------------------------------------

no :: Prop -> Prop
no = Neg

-- ---------------------------------------------------------------------
-- Se definen los siguientes operadores
-- (/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
-- tales que
-- f /\ g es la conjunción de f y g
-- f \/ g es la disyunción de f y g
-- f --> g es la implicación de f a g
-- f <--> g es la equivalencia entre f y g
-- ---------------------------------------------------------------------

infixr 5 \/
infixr 4 /\
infixr 3 -->
infixr 2 <-->
(/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
(/\) = Conj
(\/) = Disj
(-->) = Impl
(<-->) = Equi

-- ---------------------------------------------------------------------
-- Interpretaciones --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Se define el tipo de datos Interpretación para representar las
-- interpretaciones como listas de fórmulas atómicas.
-- ---------------------------------------------------------------------

type Interpretacion = [Prop]

-- ---------------------------------------------------------------------
-- Cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Definimos el tipo de datos Cláusula c como una par (pos, neg), donde
-- pos es la lista de los átomos correspondientes a los literales
-- positivos de c y neg la lista de los átomos correspondientes a los
-- literales negativos de c.
-- ---------------------------------------------------------------------

type Clausula = ([Prop],[Prop])

-- ---------------------------------------------------------------------
-- Ejercicio 1: Definir la función
-- esModeloClausula :: Interpretacion -> Clausula -> Bool
-- tal que (esModeloClausula i c) se verifica si i es modelo de c . Por
-- ejemplo,
-- esModeloClausula [p,r] ([p, q],[]) ==> True
-- esModeloClausula [r] ([p], [q]) ==> True
-- esModeloClausula [q,r] ([p], [q]) ==> False
-- esModeloClausula [q,r] ([],[]) ==> False
-- esModeloClausula [q,r] ([],[q]) ==> False
-- esModeloClausula [r] ([],[q]) ==> True
-- ---------------------------------------------------------------------

esModeloAtom :: Interpretacion -> Prop -> Bool
esModeloAtom i (Atom s) = elem (Atom s) i

esModeloClausula :: Interpretacion -> Clausula -> Bool
esModeloClausula i (pos,neg)
| null pos && null neg = False
| otherwise = or [esModeloAtom i a | a <- pos] ||
or [not (esModeloAtom i a) | a <-neg]

-- O bien:
esModeloClausula' :: Interpretacion -> Clausula -> Bool
esModeloClausula' i (pos,neg) =
or [elem x i | x <-pos] || or [notElem x i | x <- neg]
</source>

Ejercicio 4 (a)

2015-06-03T17:46:48Z

Jalonso: Página creada con '<source lang="haskell"> -- --------------------------------------------------------------------- -- Gramática de fórmulas prosicionales -- -- -...'

<source lang="haskell">

-- ---------------------------------------------------------------------
-- Gramática de fórmulas prosicionales --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Se definen los siguientes tipos de datos:
-- * SimboloProposicional para representar los símbolos de proposiciones
-- * Prop para representar las fórmulas proposicionales usando los
-- constructores Atom, Neg, Conj, Disj, Impl y Equi para las fórmulas
-- atómicas, negaciones, conjunciones, implicaciones y equivalencias,
-- respectivamente.
-- ---------------------------------------------------------------------

type SimboloProposicional = String

data Prop = Atom SimboloProposicional
| Neg Prop
| Conj Prop Prop
| Disj Prop Prop
| Impl Prop Prop
| Equi Prop Prop
deriving (Eq,Ord)

instance Show Prop where
show (Atom p) = p
show (Neg p) = "no " ++ show p
show (Conj p q) = "(" ++ show p ++ " /\\ " ++ show q ++ ")"
show (Disj p q) = "(" ++ show p ++ " \\/ " ++ show q ++ ")"
show (Impl p q) = "(" ++ show p ++ " --> " ++ show q ++ ")"
show (Equi p q) = "(" ++ show p ++ " <--> " ++ show q ++ ")"

-- ---------------------------------------------------------------------
-- Se definen las siguientes fórmulas proposicionales
-- atómicas: p, p1, p2, q, r, s, t y u.
-- ---------------------------------------------------------------------

p, p1, p2, q, r, s, t, u :: Prop
p = Atom "p"
p1 = Atom "p1"
p2 = Atom "p2"
q = Atom "q"
r = Atom "r"
s = Atom "s"
t = Atom "t"
u = Atom "u"

-- ---------------------------------------------------------------------
-- Se define la función
-- no :: Prop -> Prop
-- tal que (no f) es la negación de f.
-- ---------------------------------------------------------------------

no :: Prop -> Prop
no = Neg

-- ---------------------------------------------------------------------
-- Se definen los siguientes operadores
-- (/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
-- tales que
-- f /\ g es la conjunción de f y g
-- f \/ g es la disyunción de f y g
-- f --> g es la implicación de f a g
-- f <--> g es la equivalencia entre f y g
-- ---------------------------------------------------------------------

infixr 5 \/
infixr 4 /\
infixr 3 -->
infixr 2 <-->
(/\), (\/), (-->), (<-->) :: Prop -> Prop -> Prop
(/\) = Conj
(\/) = Disj
(-->) = Impl
(<-->) = Equi

-- ---------------------------------------------------------------------
-- Interpretaciones --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Se define el tipo de datos Interpretación para representar las
-- interpretaciones como listas de pares (átomo,booleano).
-- ---------------------------------------------------------------------

type Interpretacion = [(Prop,Bool)]

-- ---------------------------------------------------------------------
-- Se define el tipo de dato Literal como sinónimo de fórmula.
-- ---------------------------------------------------------------------

type Literal = Prop

-- ---------------------------------------------------------------------
-- Cláusulas --
-- ---------------------------------------------------------------------

-- ---------------------------------------------------------------------
-- Se define el tipo de datos Cláusula como una lista de literales.
-- ---------------------------------------------------------------------

type Clausula = [Literal]

-- ---------------------------------------------------------------------
-- Ejercicio 4. Definir la función
-- esModeloClausula :: Interpretacion -> Cláusula -> Bool
-- tal que (esModeloClausula i c) se verifica si i es modelo de c . Por
-- ejemplo,
-- esModeloClausula [(p,True),(q,False),(r,True)] [p, q] == True
-- esModeloClausula [(p,False),(q,False),(r,True)] [p, no q] == True
-- esModeloClausula [(p,False),(q,True),(r,True)] [p, no q] == False
-- esModeloClausula [(p,False),(q,True),(r,True)] [] == False
-- esModeloClausula [(p,False),(q,True),(r,True)] [no q] == False
-- esModeloClausula [(p,False),(q,False),(r,True)] [no q] == True
-- ---------------------------------------------------------------------

esModeloClausula :: Interpretacion -> Clausula -> Bool
esModeloClausula i c = or [esModeloLiteral i l | l <- c]

esModeloLiteral :: Interpretacion -> Literal -> Bool
esModeloLiteral i (Atom s) = busca (Atom s) i
esModeloLiteral i (Neg (Atom s)) = not (esModeloLiteral i (Atom s))

busca :: Eq t1 => t1 -> [(t1, t)] -> t
busca p i = head [v | (a,v) <- i, a == p]
</pre>

Relación 16

2015-05-22T08:36:35Z

Jalonso:

=== Relación 16: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:

reflexiva: ∀x R(x,x)
simétrica: ∀x ∀y (R(x,y) → R(y,x))
transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))
notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un padre rico, entonces existe una persona rica que tiene un abuelo rico. Usar la relación R(x) para representar que x es rico, y la función p(x) para representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes
inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes
inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.'''

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan al menos dos elementos.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan dos elementos como máximo.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente dos elementos.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente tres elementos.

----

'''Solución:'''

----
'''Ejercicio 5.''' Se considera la siguiente argumentación:

<blockquote>
Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero que le impida el paso. A algunas personas motorizadas que intentan entrar en un país le impiden el paso únicamente personas motorizadas. Ninguna persona motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.
</blockquote>

Las premisas pueden formalizarse por:
∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y,x)))
∃x(M(x) ∧ E(x) ∧ ∀y(I(y,x) → M(y)))
∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 6.''' Decidir por resolución si la la fórmula ∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas
: S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),P(a, f (a)) ∧ P( f (b), b)}.
En el caso de que no lo sea, construir a partir de la resolución un modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

Relación 16

2015-05-22T08:35:06Z

Jalonso:

=== Relación 16: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:

reflexiva: ∀x R(x,x)
simétrica: ∀x ∀y (R(x,y) → R(y,x))
transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))
notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un padre rico, entonces existe una persona rica que tiene un abuelo rico. Usar la relación R(x) para representar que x es rico, y la función p(x) para representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes
inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes
inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.'''

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan al menos dos elementos.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan dos elementos como máximo.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente dos elementos.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente tres elementos.

----

'''Solución:'''

----
'''Ejercicio 5.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero que le impida el paso. A algunas personas motorizadas que intentan entrar en un país le impiden el paso únicamente personas motorizadas. Ninguna persona motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.

Las premisas pueden formalizarse por:
∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y,x)))
∃x(M(x) ∧ E(x) ∧ ∀y(I(y,x) → M(y)))
∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 6.''' Decidir por resolución si la la fórmula ∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas
: S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),P(a, f (a)) ∧ P( f (b), b)}.
En el caso de que no lo sea, construir a partir de la resolución un modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

Relación 16

2015-05-22T08:32:17Z

Jalonso:

=== Relación 16: Resolución en Lógica de primer orden ===

----
'''Ejercicio 1.''' Se consideran las siguientes fórmulas:

reflexiva: ∀x R(x,x)
simétrica: ∀x ∀y (R(x,y) → R(y,x))
transitiva: ∀x ∀y ∀z (R(x,y) ∧ R(y,z) → R(x,z))
notrivial: ∀x ∃ R(x,y)

* Demostrar que reflexiva no es consecuencia lógica de {transitiva, simétrica}.
* Demostrar por resolución que {transitiva, simétrica, notrivial}⊧ reflexiva.

----

'''Solución:'''

----
'''Ejercicio 2.''' Demostrar, por resolución, que si toda persona rica tiene un padre rico, entonces existe una persona rica que tiene un abuelo rico. Usar la relación R(x) para representar que x es rico, y la función p(x) para representar el padre de x.

----

'''Solución:'''

----
'''Ejercicio 3.''' Se considera la siguiente argumentación: “Hay estudiantes
inteligentes y hay estudiantes trabajadores. Por tanto, hay estudiantes
inteligentes y trabajadores”.

* Formalizar la argumentación usando los siguientes símbolos: P(x) para representar que x es un estudiante inteligente y Q(x) para representar que x es un estudiante trabajador.
* Decidir, mediante resolución, la validez de la argumentación mostrando una prueba o un contramodelo de Herbrand obtenido a partir de la resolución.

----

'''Solución:'''

----
'''Ejercicio 4.'''

* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan al menos dos elementos.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan dos elementos como máximo.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente dos elementos.
* Dar un ejemplo de una fórmula F tal que todos sus modelos tengan exactamente tres elementos.

----

'''Solución:'''

----
'''Ejercicio 5.''' Se considera la siguiente argumentación:

Quien intente entrar en un país y no tenga pasaporte, encontrará algún aduanero que le impida el paso. A algunas personas motorizadas que intentan entrar en un país le impiden el paso únicamente personas motorizadas. Ninguna persona motorizada tiene pasaporte. Por tanto, ciertos aduaneros están motorizados.

Las premisas pueden formalizarse por:
∀x(E(x) ∧ ¬P(x) → ∃y(A(y) ∧ I(y, x)))
∃x(M(x) ∧ E(x) ∧ ∀y(I(y, x) → M(y)))
∀x(M(x) → ¬P(x))

Decidir mediante resolución si el argumento es correcto.

----

'''Solución:'''

----
'''Ejercicio 6.''' Decidir por resolución si la la fórmula ∃x(P(x, a) ∧ P( f (x), b)) es consecuencia del conjunto de fórmulas
: S = { ∀x(P(a, x) → P(b, f (x))), ∀x(P( f (x), x) → (∀zP(z, b))),P(a, f (a)) ∧ P( f (b), b)}.
En el caso de que no lo sea, construir a partir de la resolución un modelo de Herbrand de S que no sea modelo de la fórmula.

----

'''Solución:'''

Relación 14

2015-05-15T07:22:36Z

Jalonso:

<source lang = "isar">
header {* R14: Argumentación y Deducción natural en lógica de primer orden *}

theory R14
imports Main
begin

text {* Ej. 1: Existe un hombre al que todos desprecian.
(a) Demostrar que existe al menos un hombre que se desprecia a sí mismo.
(b) ¿La conclusión sería cierta en el caso de que sólo supiéramos que
existe un hombre al que algunos desprecian?

Simbología: H(x): x es hombre, D(x,y): x desprecia a y. *}

text {* Ej. 2: Si todas las medicinas están contaminadas, entonces todos los
técnicos negligentes son unos bribones. Si hay medicinas contaminadas,
entonces todas las medicinas están contaminadas y son peligrosas. Todos los
germicidas son medicinas. Sólo los negligentes son distraídos.
(a) Demostrar que si cualquier técnico es distraído y si algunos germicidas
están contaminados, los técnicos son bribones.
(b) ¿Podemos asegurar lo mismo en el caso de que sólo supiéramos que hay
técnicos distraídos?

Simbología: M(x): x es medicina. C(x): x está contaminada,
T(x): x es técnico, N(x): x es un negligente,
B(x): x es un bribón, G(x): x es germicida,
D(x): x es distraído. *}

text {* Ej. 3: Ningún individuo que sea candidato será derrotado si hace una
buena campaña. Todo individuo que se postula es un candidato. Cualquier
candidato que no sea derrotado, será elegido. Todo individuo que sea elegido
hace una buena campaña.
(a) Demostrar que todo individuo que se postula será elegido si y
sólo si hace una buena campaña.
(b) Si algún individuo se postula, ¿habrá candidatos que no sean
elegidos?

Simbología: I(x): x es individuo, C(x): x es candidato,
D(x): x es derrotado, B(x): x hace una buena campaña,
P(x): x se postula, E(x): x es elegido. *}

text {* Ej. 4: Todo ejecutivo que sea poeta es un hombre
imaginativo. Todo hombre imaginativo es amante del riesgo. Si todo
amante del riesgo no es poeta, entonces, ningún poeta es amante del
riesgo.
(a) Demostrar que si todo hombre imaginativo no es poeta, entonces,
ningún ejecutivo es poeta.
(b) ¿Es cierto el recíproco?

Simbología: E(x): x es ejecutivo, P(x): x es poeta, I(x): x es imaginativo,
R(x): x es amante del riesgo. *}

end
</source>

Relación 6

2015-03-26T07:07:44Z

Jalonso:

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

----
'''Ejercicio 1.'''
Sea F la fórmula P(x) → P (a) , donde a es un símbolo de constante. ¿Es
F satisfacible? ¿Tiene modelos? ¿Es F una fórmula válida?

----

'''Solución:'''

----
'''Ejercicio 2.''' 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)} .
Decidir cuáles de las siguientes fórmulas de L son válidas en I:
* P(x) → ∃yQ(y,x).
* ∀xQ(f(x),x).
* Q(f(x),x) → Q(x,x).
* Q(x,y) → P(x).
----

'''Solución:'''

----
'''Ejercicio 3.''' 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:'''

Relación 6

2015-03-26T07:07:05Z

Jalonso:

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

----
'''Ejercicio 1.'''
Sea F la fórmula P(x) → P (a) , donde a es un símbolo de constante. ¿Es
F satisfacible? ¿Tiene modelos? ¿Es F una fórmula válida?

----

'''Solución:'''

----
'''Ejercicio 2.''' 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)} .
Decidir cuáles de las siguientes fórmulas de L son válidas en I:
* P(x) → ∃yQ(y,x).
* ∀xQ(f(x),x).
* Q(f(x),x) → Q(x,x).
* Q(x,y) → P(x).
----

'''Solución:'''

----
'''Ejercicio 3.''' 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:'''

Tema 8

2015-03-19T10:36:15Z

Jalonso: Página creada con '<source lang="Isar"> header {* Tema 8: Deducción natural en lógica de primer orden *} theory Tema8 imports Main begin text {* El objetivo de este tema es presentar la ded...'

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

theory Tema8
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 ejemlo_11b:
assumes "s = t"
shows "t = s"
using assms
by auto

end
</source>

Lógica matemática y fundamentos (2014-15)

2015-03-19T10:34:59Z

Jalonso:

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

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]] y [[Relación 2a |Solución colaborativa]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]] y [[Relación 2b |Solución colaborativa]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]] y [[Relación 3 |Solución colaborativa]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]] y [[Relación 4 |Solución colaborativa]]).
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]] y [[Relación 5 |Solución colaborativa]]).
=== Teorías Isabelle/HOL ===
* '''Tema 2''': [[Tema 2 | Deducción natural en lógica proposicional con Isabelle/HOL]].
* '''Tema 8''': [[Tema 8 | Deducción natural en lógica de primer orden con Isabelle/HOL]].

Tema 2

2015-03-05T07:38:43Z

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

<source lang="isar">
header {* 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>

Lógica matemática y fundamentos (2014-15)

2015-03-05T07:37:20Z

Jalonso:

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

* '''Relación 1(a)''': Iniciación a la programación con Haskell ([[Media:Rel_1.hs |Enunciado]] y [[Relación 1 |Solución colaborativa]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]] y [[Relación 2 |Solución colaborativa]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]] y [[Relación 2a |Solución colaborativa]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]] y [[Relación 2b |Solución colaborativa]]).

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