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

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

2018-07-16T12:29:36Z

WikiSysop:

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]]).
* '''Relación 1(b)''': Tema 1. ([[R2 |Enunciado]]).
* '''Relación 2(a)''': Sintaxis y semántica de la lógica proposicional en Haskell. ([[Media:SintaxisSemantica.hs |Enunciado]]).
* '''Relación 2(b)''': Tema 1: cuestiones ([[R2b |Enunciado]]).
* '''Relación 3''': Deducción natural proposicional con Isabelle/HOL. ([[Rel_3 |Enunciado]]).
* '''Relación 4''': Deducción natural en lógica de primer con Isabelle/HOL. ([[Rel_4 |Enunciado]]).
* '''Relación 5''': Formalización de argumentos en lógica de primer orden. ([[Rel_5 |Enunciado]]).
* '''<font style="background:#FFFF00">Relación 5 (resuelta)</font>''':[[Relación 5 (resuelta) |Solución]].
* '''Relación 6''': Sintaxis y semántica de la Lógica de primer orden ([[R6 |Enunciado]]).
* '''Relación 7''': Tableros semánticos proposicionales en Haskell. ([[Media:TablerosSemanticos.hs |Enunciado]]).
* '''Relación 8''': Cuestiones sobre tableros semánticos ([[R8 |Enunciado]]).
* '''Relación 9''': Formas normales en lógica proposicional en Haskell ([[Media:FormasNormales.hs |Enunciado]]).
* '''Relación 10''': Cuestiones. ([[R10 |Enunciado]]).
* '''Relación 11''': Cláusulas proposicionales en Haskell. ([[Media:Clausulas.hs |Enunciado]]).
* '''Relación 12''': Resolución proposicional en Haskell. ([[Media:ResolucionProposicional.hs |Enunciado]]).
* '''Relación 13''': Cuestiones. ([[R13 |Enunciado]]).
* '''Relación 14''': Argumentación y Deducción natural en lógica de primer orden.([[R14 |Enunciado]]).
* '''Relación 15''': Tableros semánticos en lógica de primer orden.([[R15 |Enunciado]]).
* '''Relación 16''': Resolución en lógica de primer orden.([[R16 |Enunciado]]).
* '''Segundo examen (resuelto)''':([[Ejercicio 4 (a) |Solución_4a]], [[Ejercicio 4 (b)|Solución_4b]],[[Ejercicio 5 (a) |Solución_5a]] y [[Ejercicio 5 (b) |Solución_5b]]).

=== 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

2018-07-16T12:27:12Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang="isabelle">
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>

Relación 5

2018-07-16T12:27:11Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang="isabelle">
header {* R5: Argumentación en lógica de primer orden *}

theory R5_sol
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar en lógica de primer orden
argumentos expresados en lenguaje natural.

Antes de escribir la soluciones, comprobar con APLI2 la corrección de la
formalización.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar el siguiente argumento
Sócrates es un hombre.
Los hombres son mortales.
Luego, Sócrates es mortal.
Usar s para Sócrates
H(x) para x es un hombre
M(x) para x es mortal
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio1
assumes "H(s)"
"H(x) ⟶ M(x)"
shows "M(s)"
oops

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar el siguiente argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio2
assumes "(∃x. I(x)) ∧ (∃x. T(x))"
shows "∃x. I(x) ∧ T(x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar el siguiente argumento
Todos los participantes son vencedores. Hay como máximo un
vencedor. Hay como máximo un participante. Por lo tanto, hay
exactamente un participante.
Usar P(x) para x es un participante
V(x) para x es un vencedor
------------------------------------------------------------------ *}
lemma ejercicio3:
assumes 1: "∀x. (P(x)⟶V(x))" and
2: "(¬(∃x. V(x))) ∨ (∃x. (V(x) ∧ (∀y. (V(y) ⟶ x=y))))" and
3: "(¬(∃x. P(x))) ∨ (∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y))))"
shows "∃x. (P(x) ∧ (∀y. (P(y) ⟶ x=y)))"
proof -
obtain a where 4: "(Co(a) ∧ E(a)) ∧ (∀y. (Ca(y,a)⟶Co(y)))" using 2 by (rule exE)
have 5: "Co(a) ∧ E(a)" using 4 by (rule conjunct1)
have 6: "Co(a)" using 5 by (rule conjunct1)
have 7: "E(a)" using 5 by (rule conjunct2)
have 8: "∀y. (Ca(y,a)⟶Co(y))" using 4 by (rule conjunct2)
have 9: "Co(a) ⟶ ¬V(a)" using 3 by (rule allE)
have 10: "¬V(a)" using 9 6 by (rule mp)
have 11: "(E(a)∧ ¬V(a)) ⟶ (∃y. (A(y) ∧ Ca(y,a)))" using 1 by (rule allE)
have 12: "E(a) ∧ ¬V(a)" using 7 10 by (rule conjI)
have 13: "∃y. (A(y) ∧ Ca(y,a))" using 11 12 by (rule mp)
obtain b where 14: "A(b) ∧ Ca(b,a)" using 13 by (rule exE)
have 15: "A(b)" using 14 by (rule conjunct1)
have 16: "Ca(b,a)⟶Co(b)" using 8 by (rule allE)
have 17: "Ca(b,a)" using 14 by (rule conjunct2)
have 18: "Co(b)" using 16 17 by (rule mp)
have 19: "A(b) ∧ Co(b)" using 15 18 by (rule conjI)
show 20: "∃x. (A(x) ∧ Co(x))" using 19 by (rule exI)
qed

-- Alba González Parra

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar el siguiente argumento
Todo aquel que entre en el país y no sea un VIP será cacheado por
un aduanero. Hay un contrabandista que entra en el país y que solo
podrá ser cacheado por contrabandistas. Ningún contrabandista es un
VIP. Por tanto, algún aduanero es contrabandista.
Usar A(x) para x es aduanero
Ca(x,y) para x cachea a y
Co(x) para x es contrabandista
E(x) para x entra en el pais
V(x) para x es un VIP
------------------------------------------------------------------ *}
lemma ejercicio4:
assumes 1: "∀x. ((E(x) ∧ ¬V(x)) ⟶ (∃y. (A(y) ∧ Ca(y,x))))" and
2: "∃x. ((Co(x) ∧ E(x)) ∧ (∀y. (Ca(y,x) ⟶ Co(y))))" and
3: "∀x. (Co(x)⟶ ¬V(x))"
shows "∃x. (A(x) ∧ Co(x))"
oops

-- Alba González Parra

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar el siguiente argumento
Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
María y a Pedro.
Usar j para Juan
m para María
p para Pedro
T(x,y) para x teme a y
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio5
assumes "T(j,m)"
"T(j,p)"
shows "∃x. T(x,m) ∧ T(x,p)"
oops

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar el siguiente argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio6
assumes "∀x y z. H(x,y) ⟶ P(z,x) ∧ P(z,y)"
"H(x,y) → H(y,x)"
"H(j,l)"
"P(c,l)"
shows "P(c,j)"
oops

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar el siguiente argumento
La existencia de algún canal de TV pública, supone un acicate para
cualquier canal de TV privada; el que un canal de TV tenga un
acicate, supone una gran satisfacción para cualquiera de sus
directivos; en Madrid hay varios canales públicos de TV; TV5 es un
canal de TV privada; por tanto, todos los directivos de TV5 están
satisfechos.
Usar Pu(x) para x es un canal de TV pública
Pr(x) para x es un canal de TV privada
A(x) para x posee un acicate
D(x,y) para x es un directivo del canal y
S(x) para x está satisfecho
t para TV5
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_7:
assumes "∀x. ∀y. (Pu x ∧ Pr y ⟶ A y)"
"∀x. ∀y. (A x ∧ D y x) ⟶ S y"
"∃x. Pu x"
"Pr t"
shows "∀x. D x t ⟶ S x"
oops

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar el siguiente argumento
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.
Usar E(x) para x entra en un país
P(x) para x tiene pasaporte
A(x) para x es aduanero
I(x,y) para x impide el paso a y
M(x) para x está motorizada
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio8
assumes "∀x. E(x) ∧ ¬P(x) ⟶ ∃z. A(z) ∧ I(z,x)"
"∃x. M(x) ⟶ ∃z. M(z) ∧ I(z,x)"
"M(x) ⟶ ¬P(x)"
shows "∃x. A(x) ∧ M(x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar el siguiente argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio9
assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
"∀x. E(x) ⟶ ¬Ap(j,x)"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
oops

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar el siguiente argumento
Ningún aristócrata debe ser condenado a galeras a menos que sus
crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
hay aristócratas que han cometido crímenes vergonzosos aunque su
forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
que no está condenado a galeras.
Usar A(x) para x es aristócrata
G(x) para x está condenado a galeras
L(x) para x lleva una vida licenciosa
V(x) para x ha cometido crímenes vergonzoso
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar el siguiente argumento
Todo individuo que esté conforme con el contenido de cualquier
acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
políticos. Cualquiera que se inhiba de los asuntos políticos, no
participará en el próximo referéndum. Todo español, está conforme
con el acuerdo internacional de Maastricht, al que sin embargo no
apoya. Por tanto, cualquier individuo o no es español, o en otro
caso, está conforme con el contenido del acuerdo internacional de
Maastricht y no participará en el próximo referéndum.
Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
A(x,y) para la persona x apoya el acuerdo y
I(x) para la persona x se inibe de asuntos políticos
R(x) para la persona x participará en el próximo referéndum
E(x) para la persona x es española
m para el acuerdo de Maastricht
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_11:
assumes "∀x. ∀y. (C x y ⟶ (A x y ∨ I x))"
"∀x. (I x ⟶ ¬(R x))"
"∀x. (E x ⟶ (C x m ∧ ¬(A x m)))"
shows "∀x. (¬(E x) ∨ (C x m ∧ ¬(R x)))"
oops

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar el siguiente argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}

-- Adrian Guerra

lemma ejercicio_12:
assumes "∀x. ¬(R x) ⟶ R (p x)"
shows "∃x. (R x ∧ R(p (p x)))"
oops

text {* ---------------------------------------------------------------
Ejercicio 13. Formalizar el siguiente argumento
Todo deprimido que estima a un submarinista es listo. Cualquiera
que se estime a sí mismo es listo. Ningún deprimido se estima a sí
mismo. Por tanto, ningún deprimido estima a un submarinista.
Usar D(x) para x está deprimido
E(x,y) para x estima a y
L(x) para x es listo
S(x) para x es submarinista
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_13:
assumes "∀x. ∀y. ((D x ∧ S y ∧ E x y) ⟶ L x)"
"∀x. (E x x ⟶ L x)"
"¬(∃x. (D x ∧ E x x))"
shows "¬(∃x. ∃y. (D x ∧ S y ∧ E x y))"
oops

text {* ---------------------------------------------------------------
Ejercicio 14. Formalizar el siguiente argumento
Todos los robots obedecen a los amigos del programador jefe.
Alvaro es amigo del programador jefe, pero Benito no le
obedece. Por tanto, Benito no es un robot.
Usar R(x) para x es un robot
Ob(x,y) para x obedece a y
A(x) para x es amigo del programador jefe
b para Benito
a para Alvaro
------------------------------------------------------------------ *}

-- Adrian Guerra

lemma ejercicio_14:
assumes "∀x. ∀y. ((A x ∧ R y) ⟶ Ob y x)"
"A a"
"¬(Ob b a)"
shows "¬(R b)"
oops

text {* ---------------------------------------------------------------
Ejercicio 15. Formalizar el siguiente argumento
En una pecera nadan una serie de peces. Se observa que:
* Hay algún pez x que para cualquier pez y, si el pez x no se come
al pez y entonces existe un pez z tal que z es un tiburón o bien
z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
Por tanto, existe algún tiburón en la pecera.
Usar C(x,y) para x se come a y
P(x,y) para x protege a y
T(x) para x es un tiburón
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_15:
assumes "∃x. (∀y. (¬(C x y) ⟶ (∃z. (T z ∨ P z y))))"
"¬(∃x. (∀y. C x y))"
"¬(∃x. (∃y. P x y))"
shows "∃x. T x"
oops

text {* ---------------------------------------------------------------
Ejercicio 16. Formalizar el siguiente argumento
Supongamos conocidos los siguientes hechos acerca del número de
aprobados de dos asignaturas A y B:
* Si todos los alumnos aprueban la asignatura A, entonces todos
aprueban la asignatura B.
* Si algún delegado de la clase aprueba A y B, entonces todos los
alumnos aprueban A.
* Si nadie aprueba B, entonces ningún delegado aprueba A.
* Si Manuel no aprueba B, entonces nadie aprueba B.
Por tanto, si Manuel es un delegado y aprueba la asignatura A,
entonces todos los alumnos aprueban las asignaturas A y B.
Usar A(x,y) para x aprueba la asignatura y
D(x) para x es delegado
m para Manuel
a para la asignatura A
b para la asignatura B
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_16:
assumes "(∀x. (A x a)) ⟶ (∀y.(A x b))"
"(∃x. (D x ∧ A x a ∧ A x b)) ⟶ (∀y. A y a)"
"¬(∃x. A x b) ⟶ ¬((∃y. (D y ∧ A y a)))"
"¬(A m b) ⟶ ¬(∃x. A x b)"
shows "(D m ∧ A m a) ⟶ (∀x. (A x a ∧ A x b))"
oops

text {* ---------------------------------------------------------------
Ejercicio 17. Formalizar el siguiente argumento
En cierto país oriental se ha celebrado la fase final del
campeonato mundial de fútbol. Cierto diario deportivo ha publicado
las siguientes estadísticas de tan magno acontecimiento:
* A todos los porteros que no vistieron camiseta negra les marcó un
gol algún delantero europeo.
* Algún portero jugó con botas blancas y sólo le marcaron goles
jugadores con botas blancas.
* Ningún portero se marcó un gol a sí mismo.
* Ningún jugador con botas blancas vistió camiseta negra.
Por tanto, algún delantero europeo jugó con botas blancas.
Usar P(x) para x es portero
D(x) para x es delantero europeo
N(x) para x viste camiseta negra
B(x) para x juega con botas blancas
M(x,y) para x marcó un gol a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Formalizar el siguiente argumento
Las relaciones de parentesco verifican la siguientes propiedades
generales:
* Si x es hermano de y, entonces y es hermano de x.
* Todo el mundo es hijo de alguien.
* Nadie es hijo del hermano de su padre.
* Cualquier padre de una persona es también padre de todos los
hermanos de esa persona.
* Nadie es hijo ni hermano de sí mismo.
Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
Usar A para Don Antonio
He(x,y) para x es hermano de y
Hi(x,y) para x es hijo de y
L para Don Luis
a para Antoñito
m para Manolito
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_18:
assumes "∀x. ∀y. (He x y ⟷ He y x)"
"∀x. (∃y. Hi y x)"
"¬(∃x y z. (He x y ∧ Hi z x ∧ Hi z y))"
"∀x y z. ((Hi y x ∧ He y z) ⟶ Hi z x)"
"¬(∃x. (He x x ∨ Hi x x))"
"He A L"
"He a m"
"Hi a A"
shows "¬(Hi m L)"
oops

text {* ---------------------------------------------------------------
Ejercicio 19. [Problema del apisonador de Schubert (en inglés,
"Schubert’s steamroller")] Formalizar el siguiente argumento
Si uno de los miembros del club afeita a algún otro (incluido a
sí mismo), entonces todos los miembros del club lo han afeitado
a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
Petruccio y Cesare pertenecen al club de barberos. Guido ha
afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
Usar g para Guido
l para Lorenzo
p para Petruccio
c para Cesare
B(x) para x es un miembro del club de barberos
A(x,y) para x ha afeitado a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Formalizar el siguiente argumento
Carlos afeita a todos los habitantes de Las Chinas que no se
afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
Chinas. Por consiguiente, Carlos no afeita a nadie.
Usar A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_20:
assumes "∀x. ((C x ∧ ¬(A x x)) ⟷ A c x)"
"C c"
shows "¬(∃x. A c x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 21. Formalizar el siguiente argumento
Quien desprecia a todos los fanáticos desprecia también a todos los
políticos. Alguien no desprecia a un determinado político. Por
consiguiente, hay un fanático al que no todo el mundo desprecia.
Usar D(x,y) para x desprecia a y
F(x) para x es fanático
P(x) para x es político
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 22. Formalizar el siguiente argumento
El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
se ama a sí mismo.
Usar A(x,y) para x ama a y
H(x) para x es un hombre
P(x) para x es puro
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_22:
assumes "∀x. ∀y. ((P x ∧ H y ∧ P y) ⟶ A x y)"
shows "∀x. ((H x ∧ P x) ⟶ A x x)"
oops

text {* ---------------------------------------------------------------
Ejercicio 23. Formalizar el siguiente argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}

-- Adrián Guerra

lemma ejercicio_23:
assumes "¬(∃x. (P x ∧ R x))"
"∀x. ((P x ∧ ¬(Q x))⟶ R x)"
shows "P a ⟶ Q a"
oops

text {* ---------------------------------------------------------------
Ejercicio 24. Formalizar el siguiente argumento
1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
existen algunos ejemplares de estos animales.
2. También hay algunas semillas y las semillas son plantas.
3. A todo animal le gusta o bien comer todo tipo de plantas o bien
le gusta comerse a todos los animales más pequeños que él mismo
que gustan de comer algunas plantas.
4. Las orugas y los caracoles son mucho más pequeños que los
pájaros, que son mucho más pequeños que los zorros que a su vez
son mucho más pequeños que los lobos.
5. A los lobos no les gusta comer ni zorros ni semillas, mientras
que a los pájaros les gusta comer orugas pero no caracoles.
6. Las orugas y los caracoles gustan de comer algunas plantas.
7. Luego, existe un animal al que le gusta comerse un animal al que
le gusta comer semillas.
Usar A(x) para x es un animal
Ca(x) para x es un caracol
Co(x,y) para x le gusta comerse a y
L(x) para x es un lobo
M(x,y) para x es más pequeño que y
Or(x) para x es una oruga
Pa(x) para x es un pájaro
Pl(x) para x es una planta
S(x) para x es una semilla
Z(x) para x es un zorro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 25. Formalizar el siguiente argumento
Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
primera. Hay como máximo una persona que ama a Rosa. Por tanto,
Paco es Curro.
Usar A(x,y) para x ama a y
S(x,y) para x simpatiza con y
a para Ana
c para Curro
p para Paco
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 26. Formalizar el siguiente argumento
Sólo hay un sofista que enseña gratuitamente, y éste es
Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
argumenta mejor que algún sofista que enseña gratuitamente. Si una
persona argumenta mejor que otra segunda, entonces la segunda no
argumenta mejor que la primera. Por consiguiente, Platón no es un
sofista.
Usar G(x) para x enseña gratuitamente
M(x,y) para x argumenta mejor que y
S(x) para x es un sofista
p para Platón
s para Sócrates
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Formalizar el siguiente argumento
Todos los filósofos se han preguntado qué es la filosofía. Los que
se preguntan qué es la filosofía se vuelven locos. Nietzsche es
filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
Nietzsche y su maestro son diferentes personas.
Usar F(x) para x es filósofo
L(x) para x se vuelve loco
P(x) para x se ha preguntado qué es la filosofía.
m para el maestro de Nietzsche
n para Nietzsche
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 28. Formalizar el siguiente argumento
Los padres son mayores que los hijos. Juan es el padre de Luis. Por
tanto, Juan es mayor que Luis.
Usar M(x,y) para x es mayor que y
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Formalizar el siguiente argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 30. Formalizar el siguiente argumento
Luis y Jaime tienen el mismo padre. La madre de Rosa es
Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
la madre de Rosa ama al padre de Luis.
Usar A(x,y) para x ama a y
m(x) para la madre de x
p(x) para el padre de x
c para Carlos
e para Eva
j para Jaime
l para Luis
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. Formalizar el siguiente argumento
Si dos personas son hermanos, entonces tienen la misma madre y el
mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
de Juan es la madre del padre de Luis.
Usar H(x,y) para x es hermano de y
m(x) para la madre de x
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 32. Formalizar el siguiente argumento
Todos los miembros del claustro son asturianos. El secretario forma
parte del claustro. El señor Martínez es el secretario. Por tanto,
el señor Martínez es asturiano.
Usar C(x) para x es miembro del claustro
A(x) para x es asturiano
s para el secretario
m para el señor Martínez
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 33. Formalizar el siguiente argumento
Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
de la defensa. O Eduardo estaba en clase o Antonio dio falso
testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
primer testigo de la defensa dio falso testimonio.
Usar C(x) para x estaba en clase
F(x) para x dio falso testimonio
V(x) para x pudo haber visto al asesino
a para Antonio
e para Eduardo
p para el primer testigo de la defensa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 34. Formalizar el siguiente argumento
La luna hoy es redonda. La luna de hace dos semanas tenía forma de
cuarto creciente. Luna no hay más que una, es decir, siempre es la
misma. Luego existe algo que es a la vez redondo y con forma de
cuarto creciente.
Usar L(x) para la luna del momento x
R(x) para x es redonda
C(x) para x tiene forma de cuarto creciente
h para hoy
d para hace dos semanas
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 35. Formalizar el siguiente argumento
Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
delgado y Guillermo no. Luego, Juana no está casada con Guillermo.
Usar D(x) para x es delgado
C(x,y) para x está casada con y
g para Guillermo
j para Juana
t para Tomás
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 36. Formalizar el siguiente argumento
Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
más que Sultán resolverá problemas que Sultán no puede resolver.
Todos los chimpancés distintos de Sultán trabajan más que Sultán.
Por consiguiente, Sultán no obtendrá un plátano.
Usar Pl(x) para x obtiene el plátano
Pr(x) para x es un problema
R(x,y) para x resuelve y
T(x,y) para x trabaja más que y
c para Chitón
s para Sultán
------------------------------------------------------------------ *}

end
</source>

Relación 5 (resuelta)

2018-07-16T12:27:11Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang = "isabelle">
header {* R5: Argumentación en lógica de primer orden *}

theory R5_sol
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar en lógica de primer orden
argumentos expresados en lenguaje natural.

Antes de escribir la soluciones, comprobar con APLI2 la corrección de
la formalización.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar el siguiente argumento
Sócrates es un hombre.
Los hombres son mortales.
Luego, Sócrates es mortal.
Usar s para Sócrates
H(x) para x es un hombre
M(x) para x es mortal
------------------------------------------------------------------ *}

lemma ejercicio_1:
assumes "H(s)"
"∀x. H(x) ⟶ M(x)"
shows "M(s)"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar el siguiente argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}

-- "La refutación automática es"
lemma ejercicio_2:
assumes "(∃x. I(x)) ∧ (∃x. T(x))"
shows "∃x. I(x) ∧ T(x)"
quickcheck
oops

text {*
El argumento es incorrecto como muestra el siguiente contraejemplo:
I = {a1}\<^isub>
T = {a2}
*}

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar el siguiente argumento
Todos los participantes son vencedores. Hay como máximo un
vencedor. Hay como máximo un participante. Por lo tanto, hay
exactamente un participante.
Usar P(x) para x es un participante
V(x) para x es un vencedor
------------------------------------------------------------------ *}

-- "La refutación automática es"
lemma ejercicio_3:
assumes "∀x. P(x) ⟶ V(x)"
"∀x y. V(x) ∧ V(y) ⟶ x=y"
"∀x y. P(x) ∧ P(y) ⟶ x=y"
shows "∃x. P(x) ∧ (∀y. P(y) ⟶ x=y)"
quickcheck
oops

text {*
El argumento es incorrecto como muestra el siguiente contraejemplo:
V = {}
P = {}
*}

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar el siguiente argumento
Todo aquel que entre en el país y no sea un VIP será cacheado por
un aduanero. Hay un contrabandista que entra en el país y que solo
podrá ser cacheado por contrabandistas. Ningún contrabandista es un
VIP. Por tanto, algún aduanero es contrabandista.
Usar A(x) para x es aduanero
Ca(x,y) para x cachea a y
Co(x) para x es contrabandista
E(x) para x entra en el pais
V(x) para x es un VIP
------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_4:
assumes "∀x. E(x) ∧ ¬V(x) ⟶ (∃y. A(y) ∧ Ca(y,x))"
"∃x. Co(x) ∧ E(x) ∧ (∀y. Ca(y,x) ⟶ Co(y))"
"¬(∃x. Co(x) ∧ V(x))"
shows "∃x. A(x) ∧ Co(x)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar el siguiente argumento
Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
María y a Pedro.
Usar j para Juan
m para María
p para Pedro
T(x,y) para x teme a y
------------------------------------------------------------------ *}

lemma ejercicio_5:
assumes "T(j,m)"
"T(j,p)"
shows "∃x. T(x,m) ∧ T(x,p)"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar el siguiente argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}

lemma ejercicio_6:
assumes "∀x y. H(x,y) ⟶ H(y,x)"
"∀x y z. H(x,y) ∧ P(z,x) ⟶ P(z,y)"
"H(j,l)"
"P(c,l)"
shows "P(c,j)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar el siguiente argumento
La existencia de algún canal de TV pública, supone un acicate para
cualquier canal de TV privada; el que un canal de TV tenga un
acicate, supone una gran satisfacción para cualquiera de sus
directivos; en Madrid hay varios canales públicos de TV; TV5 es un
canal de TV privada; por tanto, todos los directivos de TV5 están
satisfechos.
Usar Pu(x) para x es un canal de TV pública
Pr(x) para x es un canal de TV privada
A(x) para x posee un acicate
D(x,y) para x es un directivo del canal y
S(x) para x está satisfecho
t para TV5
------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_7:
assumes "(∃x. Pu(x)) ⟶ (∀x. Pr(x) ⟶ A(x))"
"∀x. A(x) ⟶ (∀y. D(y,x) ⟶ S(y))"
"∃x. Pu(x)"
"Pr(t)"
shows "∀x. D(x,t) ⟶ S(x)"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar el siguiente argumento
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.
Usar E(x) para x entra en un país
P(x) para x tiene pasaporte
A(x) para x es aduanero
I(x,y) para x impide el paso a y
M(x) para x está motorizada
------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_8:
assumes "∀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)"
shows "∃x. A(x) ∧ M(x)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar el siguiente argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_9:
assumes "∀x. Af(x) ⟶ (∀y. E(y) ⟶ Ap(x,y))"
"∀x. E(x) ⟶ ¬Ap(j,x)"
shows "(∃x. E(x) ∧ N(x)) ⟶ ¬Af(j)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar el siguiente argumento
Ningún aristócrata debe ser condenado a galeras a menos que sus
crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
hay aristócratas que han cometido crímenes vergonzosos aunque su
forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
que no está condenado a galeras.
Usar A(x) para x es aristócrata
G(x) para x está condenado a galeras
L(x) para x lleva una vida licenciosa
V(x) para x ha cometido crímenes vergonzoso
------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_10:
assumes "∀x. A(x) ∧ G(x) ⟶ L(x) ∧ V(x)"
"∃x. A(x) ∧ V(x) ∧ ¬L(x)"
shows "∃x. A(x) ∧ ¬G(x)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar el siguiente argumento
Todo individuo que esté conforme con el contenido de cualquier
acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
políticos. Cualquiera que se inhiba de los asuntos políticos, no
participará en el próximo referéndum. Todo español, está conforme
con el acuerdo internacional de Maastricht, al que sin embargo no
apoya. Por tanto, cualquier individuo o no es español, o en otro
caso, está conforme con el contenido del acuerdo internacional de
Maastricht y no participará en el próximo referéndum.
Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
A(x,y) para la persona x apoya el acuerdo y
I(x) para la persona x se inibe de asuntos políticos
R(x) para la persona x participará en el próximo referéndum
E(x) para la persona x es española
m para el acuerdo de Maastricht
------------------------------------------------------------------ *}

lemma ejercicio_11:
assumes "∀x y. C(x,y) ⟶ A(x,y) ∨ I(x)"
"∀x. I(x) ⟶ ¬R(x)"
"∀x. E(x) ⟶ C(x,m) ∧ ¬A(x,m)"
shows "∀x. ¬E(x) ∨ (C(x,m) ∧ ¬R(x))"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar el siguiente argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}

lemma ejercicio_12:
assumes "∀x. ¬R(x) ⟶ R(p(x))"
shows "∃x. R(x) ∧ R(p(p(x)))"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 13. Formalizar el siguiente argumento
Todo deprimido que estima a un submarinista es listo. Cualquiera
que se estime a sí mismo es listo. Ningún deprimido se estima a sí
mismo. Por tanto, ningún deprimido estima a un submarinista.
Usar D(x) para x está deprimido
E(x,y) para x estima a y
L(x) para x es listo
S(x) para x es submarinista
------------------------------------------------------------------ *}

lemma ejercicio_13:
assumes "∀x. D(x) ∧ (∃y. S(y) ∧ E(x,y)) ⟶ L(x)"
"∀x. E(x,x) ⟶ L(x)"
"¬(∃x. D(x) ∧ E(x,x))"
shows "¬(∃x. D(x) ∧ (∃y. S(y) ∧ E(x,y)))"
quickcheck
oops

text {*
El argumento es incorrecto como muestra el siguiente contraejemplo:
Quickcheck found a counterexample:
D = {a2}
S = {a1}
E = {(a2,a1)}
L = {a2}
*}

text {* ---------------------------------------------------------------
Ejercicio 14. Formalizar el siguiente argumento
Todos los robots obedecen a los amigos del programador jefe.
Alvaro es amigo del programador jefe, pero Benito no le
obedece. Por tanto, Benito no es un robot.
Usar R(x) para x es un robot
Ob(x,y) para x obedece a y
A(x) para x es amigo del programador jefe
b para Benito
a para Alvaro
------------------------------------------------------------------ *}

lemma ejercicio_14:
assumes "∀x y. R(x) ∧ A(y) ⟶ Ob(x,y)"
"A(a)"
"¬Ob(b,a)"
shows "¬R(b)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 15. Formalizar el siguiente argumento
En una pecera nadan una serie de peces. Se observa que:
* Hay algún pez x que para cualquier pez y, si el pez x no se come
al pez y entonces existe un pez z tal que z es un tiburón o bien
z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
Por tanto, existe algún tiburón en la pecera.
Usar C(x,y) para x se come a y
P(x,y) para x protege a y
T(x) para x es un tiburón
------------------------------------------------------------------ *}

lemma ejercicio_15:
assumes "∃x. ∀y. ¬C(x,y) ⟶ (∃z. T(z) ∨ P(z,y))"
"∀x. ∃y. ¬C(x,y)"
"∀x y. ¬P(x,y)"
shows "∃x. T(x)"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 16. Formalizar el siguiente argumento
Supongamos conocidos los siguientes hechos acerca del número de
aprobados de dos asignaturas A y B:
* Si todos los alumnos aprueban la asignatura A, entonces todos
aprueban la asignatura B.
* Si algún delegado de la clase aprueba A y B, entonces todos los
alumnos aprueban A.
* Si nadie aprueba B, entonces ningún delegado aprueba A.
* Si Manuel no aprueba B, entonces nadie aprueba B.
Por tanto, si Manuel es un delegado y aprueba la asignatura A,
entonces todos los alumnos aprueban las asignaturas A y B.
Usar A(x,y) para x aprueba la asignatura y
D(x) para x es delegado
m para Manuel
a para la asignatura A
b para la asignatura B
------------------------------------------------------------------ *}

lemma ejercicio_16:
assumes "(∀x. A(x,a)) ⟶ (∀x. A(x,b))"
"(∃x. D(x) ∧ A(x,a) ∧ A(x,b)) ⟶ (∀x. A(x,a))"
"(∀x. ¬A(x,b)) ⟶ (∀x. D(x) ⟶ ¬A(x,a))"
"¬A(m,b) ⟶ (∀x. ¬A(x,b))"
shows "D(m) ∧ A(m,a) ⟶ (∀x. A(x,a) ∧ A(x,b))"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 17. Formalizar el siguiente argumento
En cierto país oriental se ha celebrado la fase final del
campeonato mundial de fútbol. Cierto diario deportivo ha publicado
las siguientes estadísticas de tan magno acontecimiento:
* A todos los porteros que no vistieron camiseta negra les marcó un
gol algún delantero europeo.
* Algún portero jugó con botas blancas y sólo le marcaron goles
jugadores con botas blancas.
* Ningún portero se marcó un gol a sí mismo.
* Ningún jugador con botas blancas vistió camiseta negra.
Por tanto, algún delantero europeo jugó con botas blancas.
Usar P(x) para x es portero
D(x) para x es delantero europeo
N(x) para x viste camiseta negra
B(x) para x juega con botas blancas
M(x,y) para x marcó un gol a y
------------------------------------------------------------------ *}

lemma ejercicio_17:
assumes "∀x. P(x) ∧ ¬N(x) ⟶ (∃y. D(y) ∧ M(y,x))"
"∃x. P(x) ∧ B(x) ∧ (∀y. M(y,x) ⟶ B(y))"
"¬(∃x. P(x) ∧ M(x,x))"
"¬(∃x. B(x) ∧ N(x))"
shows "∃x. D(x) ∧ B(x)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 18. Formalizar el siguiente argumento
Las relaciones de parentesco verifican la siguientes propiedades
generales:
* Si x es hermano de y, entonces y es hermano de x.
* Todo el mundo es hijo de alguien.
* Nadie es hijo del hermano de su padre.
* Cualquier padre de una persona es también padre de todos los
hermanos de esa persona.
* Nadie es hijo ni hermano de sí mismo.
Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
Usar A para Don Antonio
He(x,y) para x es hermano de y
Hi(x,y) para x es hijo de y
L para Don Luis
a para Antoñito
m para Manolito
------------------------------------------------------------------ *}

lemma ejercicio_18:
assumes "∀x y. He(x,y) ⟶ He(y,x)"
"∀x. ∃y. Hi(x,y)"
"∀x y z. Hi(x,y) ∧ He(z,y) ⟶ ¬Hi(x,z)"
"∀x y. Hi(x,y) ⟶ (∀z. He(z,x) ⟶ Hi(z,y))"
"∀x. ¬Hi(x,x) ∧ ¬He(x,x)"
"He(A,L)"
"He(a,m)"
"Hi(a,A)"
shows "¬Hi(m,L)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 19. [Problema del apisonador de Schubert (en inglés,
"Schubert’s steamroller")] Formalizar el siguiente argumento
Si uno de los miembros del club afeita a algún otro (incluido a
sí mismo), entonces todos los miembros del club lo han afeitado
a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
Petruccio y Cesare pertenecen al club de barberos. Guido ha
afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
Usar g para Guido
l para Lorenzo
p para Petruccio
c para Cesare
B(x) para x es un miembro del club de barberos
A(x,y) para x ha afeitado a y
------------------------------------------------------------------ *}

lemma ejercicio_19:
assumes "∀x. B(x) ∧ (∃y. B(y) ∧ A(x,y)) ⟶ (∀z. B(z) ⟶ A(z,x))"
"B(g)"
"B(l)"
"B(p)"
"B(c)"
"A(g,c)"
shows "A(p,l)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 20. Formalizar el siguiente argumento
Carlos afeita a todos los habitantes de Las Chinas que no se
afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
Chinas. Por consiguiente, Carlos no afeita a nadie.
Usar A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos
------------------------------------------------------------------ *}

lemma ejercicio_20:
assumes "∀x. A(c,x) ⟷ C(x) ∧ ¬A(x,x)"
"C(c)"
shows "¬(∃x. A(c,x))"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 21. Formalizar el siguiente argumento
Quien desprecia a todos los fanáticos desprecia también a todos los
políticos. Alguien no desprecia a un determinado político. Por
consiguiente, hay un fanático al que no todo el mundo desprecia.
Usar D(x,y) para x desprecia a y
F(x) para x es fanático
P(x) para x es político
------------------------------------------------------------------ *}

lemma ejercicio_21:
assumes "∀x. (∀y. F(y) ⟶ D(x,y)) ⟶ (∀y. P(y) ⟶ D(x,y))"
"∃x y. P(y) ∧ ¬D(x,y)"
shows "∃x. F(x) ∧ ¬(∀y. D(y,x))"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 22. Formalizar el siguiente argumento
El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
se ama a sí mismo.
Usar A(x,y) para x ama a y
H(x) para x es un hombre
P(x) para x es puro
------------------------------------------------------------------ *}

lemma ejercicio_22:
assumes "∀x. H(x) ∧ P(x) ⟶ (∀y. P(y) ⟶ A(x,y))"
shows "∀x. H(x) ∧ P(x) ⟶ A(x,x)"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 23. Formalizar el siguiente argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}

lemma ejercicio_23:
assumes "¬(∃x. P(x) ∧ R(x))"
"∀x. P(x) ∧ ¬Q(x) ⟶ R(x)"
shows "P(a) ⟶ Q(a)"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 24. Formalizar el siguiente argumento
1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
existen algunos ejemplares de estos animales.
2. También hay algunas semillas y las semillas son plantas.
3. A todo animal le gusta o bien comer todo tipo de plantas o bien
le gusta comerse a todos los animales más pequeños que él mismo
que gustan de comer algunas plantas.
4. Las orugas y los caracoles son mucho más pequeños que los
pájaros, que son mucho más pequeños que los zorros que a su vez
son mucho más pequeños que los lobos.
5. A los lobos no les gusta comer ni zorros ni semillas, mientras
que a los pájaros les gusta comer orugas pero no caracoles.
6. Las orugas y los caracoles gustan de comer algunas plantas.
7. Luego, existe un animal al que le gusta comerse un animal al que
le gusta comer semillas.
Usar A(x) para x es un animal
Ca(x) para x es un caracol
Co(x,y) para x le gusta comerse a y
L(x) para x es un lobo
M(x,y) para x es más pequeño que y
Or(x) para x es una oruga
Pa(x) para x es un pájaro
Pl(x) para x es una planta
S(x) para x es una semilla
Z(x) para x es un zorro
------------------------------------------------------------------ *}

lemma ejercicio_24:
assumes
"∀x. L(x) ⟶ A(x)"
"∀x. Z(x) ⟶ A(x)"
"∀x. Pa(x) ⟶ A(x)"
"∀x. Or(x) ⟶ A(x)"
"∀x. Ca(x) ⟶ A(x)"
"∃x. L(x)"
"∃x. Z(x)"
"∃x. Pa(x)"
"∃x. Or(x)"
"∃x. Ca(x)"
"∃x. S(x)"
"∀x. S(x) ⟶ Pl(x)"
"∀x. A(x) ⟶
(∀y. Pl(y) ⟶ Co(x,y)) ∨
(∀y. A(y) ∧ M(y,x) ∧ (∃z. Pl(z) ∧ Co(y,z)) ⟶ Co(x,y))"
"∀x y. Pa(y) ∧ (Ca(x) ∨ Or(x)) ⟶ M(x,y)"
"∀x y. Pa(x) ∧ Z(y) ⟶ M(x,y)"
"∀x y. Z(x) ∧ L(y) ⟶ M(x,y)"
"∀x y. L(x) ∧ (Z(y)∨ S(y)) ⟶ ¬Co(x,y)"
"∀x y. Pa(x) ∧ Or(y) ⟶ Co(x,y)"
"∀x y. Pa(x) ∧ Ca(y) ⟶ ¬Co(x,y)"
"∀x. Or(x) ∨ Ca(x) ⟶ (∃y. Pl(y) ∧ Co(x,y))"
shows
"∃x y. A(x) ∧ A(y) ∧ (∃z. S(z) ∧ Co(y,z) ∧ Co(x,y))"
using assms
by meson

section {* Ejercicios con igualdad *}

text {* ---------------------------------------------------------------
Ejercicio 25. Formalizar el siguiente argumento
Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
primera. Hay como máximo una persona que ama a Rosa. Por tanto,
Paco es Curro.
Usar A(x,y) para x ama a y
S(x,y) para x simpatiza con y
a para Ana
c para Curro
p para Paco
r para Rosa
------------------------------------------------------------------ *}

lemma ejercicio_25:
assumes "A(r,c)"
"¬S(p,a)"
"∀x. ¬S(x,a) ⟶ A(x,r)"
"∀x y. A(x,y) ⟶ A(y,x)"
"∀x y. A(x,r) ∧ A(y,r) ⟶ x=y"
shows "p = c"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 26. Formalizar el siguiente argumento
Sólo hay un sofista que enseña gratuitamente, y éste es
Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
argumenta mejor que algún sofista que enseña gratuitamente. Si una
persona argumenta mejor que otra segunda, entonces la segunda no
argumenta mejor que la primera. Por consiguiente, Platón no es un
sofista.
Usar G(x) para x enseña gratuitamente
M(x,y) para x argumenta mejor que y
S(x) para x es un sofista
p para Platón
s para Sócrates
------------------------------------------------------------------ *}

lemma ejercicio_26:
assumes "∃y. (∀x. S(x) ∧ G(x) ⟷ x=y) ∧ y=s"
"∀x. S(x) ∧ x ≠ s ⟶ M(s,x)"
"∃x. S(x) ∧ G(x) ∧ M(p,x)"
"∀x y. M(x,y) ⟶ ¬M(y,x)"
shows "¬S(p)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 27. Formalizar el siguiente argumento
Todos los filósofos se han preguntado qué es la filosofía. Los que
se preguntan qué es la filosofía se vuelven locos. Nietzsche es
filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
Nietzsche y su maestro son diferentes personas.
Usar F(x) para x es filósofo
L(x) para x se vuelve loco
P(x) para x se ha preguntado qué es la filosofía.
m para el maestro de Nietzsche
n para Nietzsche
------------------------------------------------------------------ *}

lemma ejercicio_27:
assumes "∀x. F(x) ⟶ P(x)"
"∀x. P(x) ⟶ L(x)"
"F(n)"
"¬L(m)"
shows "n ≠ m"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 28. Formalizar el siguiente argumento
Los padres son mayores que los hijos. Juan es el padre de Luis. Por
tanto, Juan es mayor que Luis.
Usar M(x,y) para x es mayor que y
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

lemma ejercicio_28:
assumes "∀x. M(p(x),x)"
"j = p(l)"
shows "M(j,l)"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 29. Formalizar el siguiente argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}

lemma ejercicio_29:
assumes "e(h) = r"
"h = m"
shows "e(m) = r"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 30. Formalizar el siguiente argumento
Luis y Jaime tienen el mismo padre. La madre de Rosa es
Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
la madre de Rosa ama al padre de Luis.
Usar A(x,y) para x ama a y
m(x) para la madre de x
p(x) para el padre de x
c para Carlos
e para Eva
j para Jaime
l para Luis
r para Rosa
------------------------------------------------------------------ *}

lemma ejercicio_30:
assumes "p(l) = p(j)"
"m(r) = e"
"A(e,c)"
"c = p(j)"
shows "A(m(r),p(l))"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 31. Formalizar el siguiente argumento
Si dos personas son hermanos, entonces tienen la misma madre y el
mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
de Juan es la madre del padre de Luis.
Usar H(x,y) para x es hermano de y
m(x) para la madre de x
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

lemma ejercicio_31:
assumes "∀x y. H(x,y) ⟶ m(x) = m(y) ∧ p(x) = p(y)"
"H(j,l)"
shows "m(p(j)) = m(p(l))"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 32. Formalizar el siguiente argumento
Todos los miembros del claustro son asturianos. El secretario forma
parte del claustro. El señor Martínez es el secretario. Por tanto,
el señor Martínez es asturiano.
Usar C(x) para x es miembro del claustro
A(x) para x es asturiano
s para el secretario
m para el señor Martínez
------------------------------------------------------------------ *}

lemma ejercicio_32:
assumes "∀x. C(x) ⟶ A(x)"
"C(s)"
"m = s"
shows "A(m)"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 33. Formalizar el siguiente argumento
Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
de la defensa. O Eduardo estaba en clase o Antonio dio falso
testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
primer testigo de la defensa dio falso testimonio.
Usar C(x) para x estaba en clase
F(x) para x dio falso testimonio
V(x) para x pudo haber visto al asesino
a para Antonio
e para Eduardo
p para el primer testigo de la defensa
------------------------------------------------------------------ *}

lemma ejercicio_33:
assumes "V(e)"
"a = p"
"C(e) ∨ F(a)"
"∀x. C(x) ⟶ ¬V(x)"
shows "F(p)"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 34. Formalizar el siguiente argumento
La luna hoy es redonda. La luna de hace dos semanas tenía forma de
cuarto creciente. Luna no hay más que una, es decir, siempre es la
misma. Luego existe algo que es a la vez redondo y con forma de
cuarto creciente.
Usar L(x) para la luna del momento x
R(x) para x es redonda
C(x) para x tiene forma de cuarto creciente
h para hoy
d para hace dos semanas
------------------------------------------------------------------ *}

lemma ejercicio_34:
assumes "R(l(h))"
"C(l(d))"
"∀x y. l(x) = l(y)"
shows "∃x. R(x) ∧ C(x)"
using assms
by metis

text {* ---------------------------------------------------------------
Ejercicio 35. Formalizar el siguiente argumento
Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
delgado y Guillermo no. Luego, Juana no está casada con Guillermo.
Usar D(x) para x es delgado
C(x,y) para x está casada con y
g para Guillermo
j para Juana
t para Tomás
------------------------------------------------------------------ *}

lemma ejercicio_35:
assumes "∃x. ∀y. C(j,y) ⟷ y = x"
"C(j,t)"
"D(t) ∧ ¬D(g)"
shows "¬C(j,g)"
using assms
by auto

text {* ---------------------------------------------------------------
Ejercicio 36. Formalizar el siguiente argumento
Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
más que Sultán resolverá problemas que Sultán no puede resolver.
Todos los chimpancés distintos de Sultán trabajan más que Sultán.
Por consiguiente, Sultán no obtendrá un plátano.
Usar Pl(x) para x obtiene el plátano
Pr(x) para x es un problema
R(x,y) para x resuelve y
T(x,y) para x trabaja más que y
c para Chitón
s para Sultán
------------------------------------------------------------------ *}

lemma ejercicio_36:
assumes "s ≠ c"
"Pl(s) ⟶ (∀x. Pr(x) ⟶ R(s,x))"
"T(c,s) ⟶ (∃x. Pr(x) ∧ R(c,x) ∧ ¬R(s,x))"
"∀x. x ≠ s ⟶ T(x,s)"
shows "¬Pl(s)"
using assms
by metis

end
</source>

Relación 3

2018-07-16T12:27:10Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang = "isabelle">
header {* R3: Deducción natural proposicional *}

theory R3
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es demostrar cada uno de los ejercicios
usando sólo las reglas básicas de deducción natural de la lógica
proposicional (sin usar el método auto).

Las reglas básicas de la deducción natural son las siguientes:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· notnotI: P ⟹ ¬¬ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· mt: ⟦F ⟶ G; ¬G⟧ ⟹ ¬F
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
---------------------------------------------------------------------
*}

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

lemma notnotI: "P ⟹ ¬¬ P"
by auto

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

section {* Implicaciones *}

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

lemma ejercicio_1:
assumes "p ⟶ q"
"p"
shows "q"
proof -
show "q" using assms(1) assms(2) by (rule mp)
qed

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

lemma ejercicio_2:
assumes "p ⟶ q"
"q ⟶ r"
"p"
shows "r"
proof - have 1: "q" using assms(1) assms(3) by (rule mp)
show "r" using assms(2) 1 by (rule mp)
qed

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

lemma ejercicio_3:
assumes "p ⟶ (q ⟶ r)"
"p ⟶ q"
"p"
shows "r"
proof -
have 1:"q⟶r" using assms(1) assms(3) by (rule mp)
have 2:"q" using assms(2) assms(3) by (rule mp)
show "r" using 1 2 by (rule mp)
qed

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

lemma ejercicio_4:
assumes "p ⟶ q"
"q ⟶ r"
shows "p ⟶ r"

proof -
{assume 1: "p"
have 2: "q" using assms(1) 1 by (rule mp)
have 3: "r" using assms(2) 2 by (rule mp)}
then show "p⟶r" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 5. Demostrar
p ⟶ (q ⟶ r) ⊢ q ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

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

proof-
{assume 1: "q"
{assume 2: "p"
have 3:"q⟶r" using assms(1) 2 by (rule mp)
have "r" using 3 1 by (rule mp)}
hence "p⟶r" by (rule impI)}
then show "q⟶(p⟶r)" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 6. Demostrar
p ⟶ (q ⟶ r) ⊢ (p ⟶ q) ⟶ (p ⟶ r)
------------------------------------------------------------------ *}

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

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

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

lemma ejercicio_7:
assumes "p"
shows "q ⟶ p"
proof-
{assume 1: "q"
note `p`}
thus "q⟶p" by (rule impI)
qed

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

lemma ejercicio_8:
"p ⟶ (q ⟶ p)"
proof-
{assume "p"
{assume "q"
note `p`}
hence "q⟶p" by (rule impI)}
thus "p⟶q⟶p" by (rule impI)
qed

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

lemma ejercicio_9:
assumes "p ⟶ q"
shows "(q ⟶ r) ⟶ (p ⟶ r)"

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

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

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

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

lemma ejercicio_11:
"(p ⟶ (q ⟶ r)) ⟶ ((p ⟶ q) ⟶ (p ⟶ r))"

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

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

lemma ejercicio_12:
assumes "(p ⟶ q) ⟶ r"
shows "p ⟶ (q ⟶ r)"

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

section {* Conjunciones *}

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

lemma ejercicio_13:
assumes "p"
"q"
shows "p ∧ q"
proof-
show "p∧q" using assms(1) assms(2) by (rule conjI)
qed

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

lemma ejercicio_14:
assumes "p ∧ q"
shows "p"
proof-
show "p" using assms(1) by (rule conjunct1)
qed

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

lemma ejercicio_15:
assumes "p ∧ q"
shows "q"
proof-
show "q" using assms(1) by (rule conjunct2)
qed

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

lemma ejercicio_16:
assumes "p ∧ (q ∧ r)"
shows "(p ∧ q) ∧ r"
proof -
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "q ∧ r" using assms(1) by (rule conjunct2)
have 3: "q" using 2 by (rule conjunct1)
have 4: "r" using 2 by (rule conjunct2)
have 5: "p ∧ q" using 1 3 by (rule conjI)
show "(p ∧ q) ∧ r" using 5 4 by (rule conjI)
qed

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

lemma ejercicio_17:
assumes "(p ∧ q) ∧ r"
shows "p ∧ (q ∧ r)"

proof-
have 1: "p ∧ q" using assms(1) by (rule conjunct1)
have 2: "r" using assms(1) by (rule conjunct2)
have 3: "p" using 1 by (rule conjunct1)
have 4: "q" using 1 by (rule conjunct2)
have 5: "q ∧ r" using 4 2 by (rule conjI)
show "p ∧(q ∧ r)" using 3 5 by (rule conjI)
qed

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

lemma ejercicio_18:
assumes "p ∧ q"
shows "p ⟶ q"

proof-
{assume "p"
have "q" using assms(1) by (rule conjunct2)}
thus "p⟶q" by (rule impI)
qed
text {* ---------------------------------------------------------------
Ejercicio 19. Demostrar
(p ⟶ q) ∧ (p ⟶ r) ⊢ p ⟶ q ∧ r
------------------------------------------------------------------ *}

lemma ejercicio_19:
assumes "(p ⟶ q) ∧ (p ⟶ r)"
shows "p ⟶ q ∧ r"

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

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

lemma ejercicio_20:
assumes "p ⟶ q ∧ r"
shows "(p ⟶ q) ∧ (p ⟶ r)"
proof (rule conjI)
{ assume 1: "p"
have 2: "q ∧ r" using assms(1) 1 by (rule mp)
have 3: "q" using 2 by (rule conjunct1)}
thus "p ⟶ q" by (rule impI)
next
{ assume 1: "p"
have 2: "q ∧ r" using assms(1) 1 by (rule mp)
have 3: "r" using 2 by (rule conjunct2)}
thus "p ⟶ r" by (rule impI)
qed

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

lemma ejercicio_22:
assumes "p ∧ q ⟶ r"
shows "p ⟶ (q ⟶ r)"
proof -
{ assume 1: "p"
{assume 2: "q"
have 3: "p ∧ q" using 1 2 by (rule conjI)
have 4: "r" using assms(1) 3 by (rule mp)}
then have 5: "q ⟶ r" by (rule impI)}
thus "p ⟶ (q ⟶ r)" by (rule impI)
qed

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

section {* Disyunciones *}

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

lemma ejercicio_33:
assumes "p ∧ (q ∨ r)"
shows "(p ∧ q) ∨ (p ∧ r)"
proof -
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "q ∨ r" using assms(1) by (rule conjunct2)
moreover
{ assume 3: "q"
have 4: "p ∧ q" using 1 3 by (rule conjI)
have 5: "(p ∧ q) ∨ (p ∧ r)" using 4 by (rule disjI1)}
moreover
{ assume 6: "r"
have 7: "p ∧ r" using 1 6 by (rule conjI)
have 8: "(p ∧ q) ∨ (p ∧ r)" using 7 by (rule disjI2)}
ultimately show "(p ∧ q) ∨ (p ∧ r)" by (rule disjE)
qed

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

lemma ejercicio_38:
assumes "p ∨ q ⟶ r"
shows "(p ⟶ r) ∧ (q ⟶ r)"
proof (rule conjI)
{ assume 1: "p"
have 2: "p ∨ q" using 1 by (rule disjI1)
have 3: "r" using assms(1) 2 by (rule mp)}
thus "p ⟶ r" by (rule impI)
next
{ assume 4: "q"
have 5: "p ∨ q" using 4 by (rule disjI2)
have 6: "r" using assms(1) 5 by (rule mp)}
thus "q ⟶ r" by (rule impI)
qed

section {* Negaciones *}

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof (rule ccontr)
assume 1: "¬¬(¬p ∧ ¬q)"
have 2: "¬p ∧ ¬q" using 1 by (rule notnotD)
have 3: "p ∨ q" using assms(1) by this
moreover
{ assume 4: "p"
have 5: "¬p" using 2 by (rule conjunct1)
have 6: "False" using 5 4 by (rule notE)}
moreover
{ assume 7: "q"
have 8: "¬q" using 2 by (rule conjunct2)
have 9: "False" using 8 7 by (rule notE)}
ultimately show "False" by (rule disjE)
qed

-- Miguel Peña Gallardo

lemma ejercicio_44:
assumes "p ∨ q"
shows "¬(¬p ∧ ¬q)"
proof-
{assume 1:"¬¬(¬p ∧ ¬q)"
have 2: "(¬p ∧ ¬q)" using 1 by (rule notnotD)
have 3: "¬p" using 2 by (rule conjunct1)
have 4: "¬q" using 2 by (rule conjunct2)
have "p∨q" using assms(1) by this
moreover
{assume 5: "p"
have 6: "False" using 3 5 by (rule notE)}
moreover
{assume 7: "q"
have 8: "False" using 4 7 by (rule notE)}
ultimately have "False" by (rule disjE)}
then show "¬(¬p ∧¬q)" by (rule ccontr)

qed

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

-- Francisco Javier Carmona

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"
proof (rule ccontr)
assume 1: "¬¬(¬p ∨ ¬q)"
have 2: "¬p ∨ ¬q" using 1 by (rule notnotD)
moreover
{assume 3: "¬p"
have 4: "p" using assms(1) by (rule conjunct1)
have 5: "False" using 3 4 by (rule notE)}
moreover
{ assume 6: "¬q"
have 7: "q" using assms(1) by (rule conjunct2)
have 8: "False" using 6 7 by (rule notE)}
ultimately show "False" by (rule disjE)
qed

--Miguel Peña Gallardo

lemma ejercicio_45:
assumes "p ∧ q"
shows "¬(¬p ∨ ¬q)"

proof-
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "q" using assms(1) by (rule conjunct2)
{assume 3: "¬¬(¬p∨¬q)"
have 4: "¬p ∨¬q" using 3 by (rule notnotD)
have "¬p ∨¬q" using 4 by this
moreover
{assume 5: "¬p"
have 6: "False" using 5 1 by (rule notE)}
moreover
{assume 7: "¬q"
have 8: "False" using 7 2 by (rule notE)}
ultimately have "False" by (rule disjE)}
then show "¬(¬p∨¬q)" by (rule ccontr)

qed

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

-- Francisco Javier Carmona

lemma ejercicio_46:
assumes "¬(p ∨ q)"
shows "¬p ∧ ¬q"
proof (rule conjI)
{assume 1: "¬¬p"
have 2: "p" using 1 by (rule notnotD)
have 3: "p ∨ q" using 2 by (rule disjI1)
have 4: "False" using assms(1) 3 by (rule notE)}
thus 5: "¬p" by (rule ccontr)
next
{ assume 6: "¬¬q"
have 7: "q" using 6 by (rule notnotD)
have 8: "p ∨ q" using 7 by (rule disjI2)
have 9: "False" using assms(1) 8 by (rule notE)}
thus 10: "¬q" by (rule ccontr)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_47:
assumes "¬p ∧ ¬q"
shows "¬(p ∨ q)"
proof (rule ccontr)
assume 1: "¬¬(p ∨ q)"
have 2: "p ∨ q" using 1 by (rule notnotD)
moreover
{ assume 3: "p"
have 4: "¬p" using assms(1) by (rule conjunct1)
have 5: "False" using 4 3 by (rule notE)}
moreover
{ assume 6: "q"
have 7: "¬q" using assms(1) by (rule conjunct2)
have 8: "False" using 7 6 by (rule notE)}
ultimately show "False" by (rule disjE)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_48:
assumes "¬p ∨ ¬q"
shows "¬(p ∧ q)"
proof (rule ccontr)
assume 1: "¬¬(p ∧ q)"
have 2: "(p ∧ q)" using 1 by (rule notnotD)
have 3: "¬p ∨ ¬q" using assms(1) by this
moreover
{ assume 4: "¬p"
have 5: "p" using 2 by (rule conjunct1)
have 6: "False" using 4 5 by (rule notE)}
moreover
{ assume 7: "¬q"
have 8: "q" using 2 by (rule conjunct2)
have 9: "False" using 7 8 by (rule notE)}
ultimately show "False" by (rule disjE)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_49:
"¬(p ∧ ¬p)"
proof -
{assume 1: "¬¬(p ∧ ¬p)"
have 2: "p ∧ ¬p" using 1 by (rule notnotD)
have 3: "p" using 2 by (rule conjunct1)
have 4: "¬p" using 2 by (rule conjunct2)
have 5: "False" using 4 3 by (rule notE)}
thus "¬(p ∧ ¬p)" by (rule ccontr)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_50:
assumes "p ∧ ¬p"
shows "q"
proof -
have 1: "p" using assms(1) by (rule conjunct1)
have 2: "¬p" using assms(1) by (rule conjunct2)
have 3: "False" using 2 1 by (rule notE)
show 4: "q" using 3 by (rule FalseE)
qed

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

-- Francisco Javier Carmona

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

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

-- Francisco Javier Carmona

lemma ejercicio_52:
"p ∨ ¬p"
proof -
have 1: "¬p ∨ p" by (rule excluded_middle)
moreover
{ assume 2: "¬p"
have 3: "p ∨ ¬p" using 2 by (rule disjI2)}
moreover
{ assume 4: "p"
have 5: "p ∨ ¬p" using 4 by (rule disjI1)}
ultimately show "p ∨ ¬p" by (rule disjE)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_53:
"((p ⟶ q) ⟶ p) ⟶ p"
proof -
{assume 1: "(p ⟶ q) ⟶ p"
{ assume 3: "¬p"
have 4: "¬(p ⟶ q)" using 1 3 by (rule mt)
{ assume 5: "p"
have 6: "False" using 3 5 by (rule notE)
have 7: "q" using 6 by (rule FalseE)}
hence 8: "p ⟶ q" by (rule impI)
have 9: "False" using 4 8 by (rule notE)}
hence 10: "p" by (rule ccontr)}
thus 11: "((p ⟶ q) ⟶ p) ⟶ p" by (rule impI)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_54:
assumes "¬q ⟶ ¬p"
shows "p ⟶ q"
proof (rule impI)
assume 1: "p"
have 2: "¬q ∨ q" by (rule excluded_middle)
moreover
{ assume 3: "¬q"
have 4: "¬p" using assms(1) 3 by (rule mp)
have 5: "False" using 4 1 by (rule notE)
have 6: "q" using 5 by (rule FalseE)}
moreover
{ assume 7: "q"
have 8: "q" using 7 by this}
ultimately show "q" by (rule disjE)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_55:
assumes "¬(¬p ∧ ¬q)"
shows "p ∨ q"
proof -
have 1: "¬p ∨ p" by (rule excluded_middle)
moreover
{ assume 2: "¬p"
have 3: "¬q ∨ q" by (rule excluded_middle)
moreover
{ assume 4: "¬q"
have 5: "¬p ∧ ¬ q" using 2 4 by (rule conjI)
have 6: "False" using assms(1) 5 by (rule notE)
have 7: "p ∨ q" using 6 by (rule FalseE)}
moreover
{ assume 8: "q"
have 9: "p ∨ q" using 8 by (rule disjI2)}
ultimately have "p ∨ q" by (rule disjE)}
moreover
{ assume 10: "p"
have 11: "p ∨ q" using 10 by (rule disjI1)}
ultimately show "p ∨ q" by (rule disjE)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_56:
assumes "¬(¬p ∨ ¬q)"
shows "p ∧ q"
proof (rule conjI)
{ assume 1: "¬p"
have 2: "¬p ∨ ¬q" using 1 by (rule disjI1)
have 3: "False" using assms(1) 2 by (rule notE)}
thus 4: "p" by (rule ccontr)
next
{ assume 5: "¬q"
have 6: "¬p ∨ ¬q" using 5 by (rule disjI2)
have 7: "False" using assms(1) 6 by (rule notE)}
thus 8: "q" by (rule ccontr)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_57:
assumes "¬(p ∧ q)"
shows "¬p ∨ ¬q"
proof -
have 1: "¬p ∨ p" by (rule excluded_middle)
moreover
{ assume 2: "¬p"
have 3: "¬p ∨ ¬q" using 2 by (rule disjI1)}
moreover
{ assume 4: "p"
have 5: "¬q ∨ q" by (rule excluded_middle)
moreover
{ assume 6: "¬q"
have 7: "¬p ∨ ¬q" using 6 by (rule disjI2)}
moreover
{ assume 8: "q"
have 9: "p ∧ q" using 4 8 by (rule conjI)
have 10: "False" using assms(1) 9 by (rule notE)
have 11: "¬p ∨ ¬q" using 10 by (rule FalseE)}
ultimately have "¬p ∨ ¬q" by (rule disjE)}
ultimately show "¬p ∨ ¬q" by (rule disjE)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_58:
"(p ⟶ q) ∨ (q ⟶ p)"
proof -
have "¬p ∨ p" by (rule excluded_middle)
moreover
{ assume "¬p"
{ assume "p"
with `¬p` have "False" by (rule notE)
hence "q" by (rule FalseE)}
hence "p ⟶ q" by (rule impI)
hence "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI1)}
moreover
{ assume 1: "p"
{ assume "q"
have "p" using 1 by this}
hence "q ⟶ p" by (rule impI)
hence "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjI2)}
ultimately show "(p ⟶ q) ∨ (q ⟶ p)" by (rule disjE)
qed

end

</source>

Relación 4

2018-07-16T12:27:10Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang ="isabelle">
header {* R4: Deducción natural de primer orden *}

theory R4
imports Main
begin

text {*
Demostrar o refutar los siguientes lemas usando sólo las reglas
básicas de deducción natural de la lógica proposicional, de los
cuantificadores y de la igualdad:
· conjI: ⟦P; Q⟧ ⟹ P ∧ Q
· conjunct1: P ∧ Q ⟹ P
· conjunct2: P ∧ Q ⟹ Q
· notnotD: ¬¬ P ⟹ P
· mp: ⟦P ⟶ Q; P⟧ ⟹ Q
· impI: (P ⟹ Q) ⟹ P ⟶ Q
· disjI1: P ⟹ P ∨ Q
· disjI2: Q ⟹ P ∨ Q
· disjE: ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
· FalseE: False ⟹ P
· notE: ⟦¬P; P⟧ ⟹ R
· notI: (P ⟹ False) ⟹ ¬P
· iffI: ⟦P ⟹ Q; Q ⟹ P⟧ ⟹ P = Q
· iffD1: ⟦Q = P; Q⟧ ⟹ P
· iffD2: ⟦P = Q; Q⟧ ⟹ P
· ccontr: (¬P ⟹ False) ⟹ P
· excluded_middel:(¬P ∨ P)

· allI: ⟦∀x. P x; P x ⟹ R⟧ ⟹ R
· allE: (⋀x. P x) ⟹ ∀x. P x
· exI: P x ⟹ ∃x. P x
· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

· refl: t = t
· subst: ⟦s = t; P s⟧ ⟹ P t
· trans: ⟦r = s; s = t⟧ ⟹ r = t
· sym: s = t ⟹ t = s
· not_sym: t ≠ s ⟹ s ≠ t
· ssubst: ⟦t = s; P s⟧ ⟹ P t
· box_equals: ⟦a = b; a = c; b = d⟧ ⟹ a: = d
· arg_cong: x = y ⟹ f x = f y
· fun_cong: f = g ⟹ f x = g x
· cong: ⟦f = g; x = y⟧ ⟹ f x = g y
*}

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

lemma notnotI: "P ⟹ ¬¬ P"
by auto

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

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

lemma ejercicio_1a:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. P x) ⟶ (∀x. Q x)"
proof (rule impI)
assume "∀x. P x"
{ fix a
have "P a ⟶ Q a" using assms by (rule allE)
have "P a" using `∀x. P x` by (rule allE)
have "Q a" using `P a ⟶ Q a` `P a` by (rule mp)}
thus "∀x. Q x" by (rule allI)
qed

-María Dolores Mateo

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

lemma ejercicio_2a:
assumes "∃x. ¬(P x)"
shows "¬(∀x. P x)"
proof
assume "∀x. P x"
obtain a where "¬ (P a)" using assms by (rule exE)
have "P a" using `∀x. P x` by (rule allE)
show "False" using `¬ (P a)` `P a` by (rule notE)
qed

-María Dolores Mateo

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

lemma ejercicio_3a:
assumes "∀x. P x"
shows "∀y. P y"
proof
{ fix a
show "P a" using assms by (rule allE)}
qed

-María Dolores Mateo

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

lemma ejercicio_4:
assumes "∀x. P x ⟶ Q x"
shows "(∀x. ¬(Q x)) ⟶ (∀x. ¬ (P x))"
proof
assume "∀x. ¬(Q x)"
{ fix a
have "P a ⟶ Q a" using assms by (rule allE)
have "¬ (Q a)" using `∀x. ¬(Q x)` by (rule allE)
have "¬(P a)" using `P a ⟶ Q a` `¬ (Q a)` by (rule mt)}
thus "∀x. ¬ (P x)" by (rule allI)
qed

-María Dolores Mateo

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

lemma ejercicio_5:
assumes "∀x. P x ⟶ ¬(Q x)"
shows "¬(∃x. P x ∧ Q x)"
proof
assume "∃x. P x ∧ Q x"
obtain a where "P a ∧ Q a" using `∃x. P x ∧ Q x` by (rule exE)
have "P a" using `P a ∧ Q a` by (rule conjE)
have "Q a" using `P a ∧ Q a` by (rule conjE)
have "P a ⟶ ¬(Q a)" using assms by (rule allE)
have "¬(Q a)" using `P a ⟶ ¬(Q a)` `P a` by (rule mp)
show "False" using `¬(Q a)` `Q a` by (rule notE)
qed

-María Dolores Mateo

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

lemma ejercicio_6:
assumes "∀x y. P x y"
shows "∀u v. P u v"

proof (rule allI)+
fix a b
have "∀y. P a y" using assms by (rule allE)
thus " P a b" by (rule allE)
qed

--Jaime Alberto

lemma ejercicio_6b:
assumes 1: "∀x y. P x y"
shows "∀u v. P u v"
proof -
{fix u0
{fix v0
have 2: "∀y. P u0 y" using 1 by (rule allE)
have 3: "P u0 v0" using 2 by (rule allE)}
then have 4: "∀v. P u0 v" by (rule allI)}
then show "∀u v. P u v" by (rule allI)
qed

-- Rocio Rodriguez

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

lemma ejercicio_7:
assumes "∃x y. P x y"
shows "∃u v. P u v"

proof -
obtain a where "∃y. P a y" using assms by (rule exE)
then obtain b where "P a b" by (rule exE)
hence "∃v. P a v" by (rule exI)
thus "∃u v. P u v" by (rule exI)
qed

--Jaime Alberto

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

lemma ejercicio_8:
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)
fix b
have "P a b" using `∀y. P a y` by (rule allE)
thus "∃x. P x b" by (rule exI)
qed

--Jaime Alberto

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

lemma ejercicio_9:
assumes "∃x. P a ⟶ Q x"
shows "P a ⟶ (∃x. Q x)"

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

--Jaime Alberto

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

lemma ejercicio_10a:
fixes P Q :: "'b ⇒ bool"
assumes "P a ⟶ (∃x. Q x)"
shows "∃x. P a ⟶ Q x"
oops

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

lemma ejercicio_11a:
assumes "(∃x. P x) ⟶ Q a"
shows "∀x. P x ⟶ Q a"

proof
fix b
show "P b ⟶ Q a"
proof
assume "P b"
hence "∃x. P x" by (rule exI)
show "Q a" using assms `∃x. P x` by (rule mp)
qed
qed

-- Jaime Alberto

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

lemma ejercicio_12a:
assumes "∀x. P x ⟶ Q a"
shows "∃x. P x ⟶ Q a"

proof -
fix b
have "P b ⟶ Q a" using assms by (rule allE)
thus "∃x. P x ⟶ Q a" by (rule exI)
qed

-- Jaime Alberto

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

lemma ejercicio_13a:
assumes "(∀x. P x) ∨ (∀x. Q x)"
shows "∀x. P x ∨ Q x"

proof
fix a
show "P a ∨ Q a" using assms
proof
assume "∀x. P x"
hence "P a" by (rule allE)
thus "P a ∨ Q a" by (rule disjI1)
next
assume "∀x. Q x"
hence "Q a" by (rule allE)
thus "P a ∨ Q a" by (rule disjI2)
qed
qed

-- Jaime Alberto

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

lemma ejercicio_14a:
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)
hence "P a" by (rule conjunct1)
thus "∃x. P x" by (rule exI)
have "Q a" using `P a ∧ Q a` by (rule conjunct2)
thus "∃x. Q x" by (rule exI)
qed

-- Jaime Alberto

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

lemma ejercicio_15a:
assumes "∀x y. P y ⟶ Q x"
shows "(∃y. P y) ⟶ (∀x. Q x)"

proof
assume "∃y. P y"
then obtain b where "P b" by (rule exE)
{fix a
have "∀y. P y ⟶ Q a" using assms by (rule allE)
hence "P b ⟶ Q a" by (rule allE)
have "Q a" using `P b ⟶ Q a` `P b` by (rule mp)}
thus "∀x. Q x" by (rule allI)
qed

-- Jaime Alberto

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

lemma ejercicio_16a:
assumes 1:"¬(∀x. ¬(P x))"
shows "∃x. P x"

proof-
fix x0
{assume 2: "¬(∃x. P x)"
{fix x1
{assume 3: "P x1"
have 4: "∃x. P x" using 3 by (rule exI)
have 5: "False" using 2 4 by (rule notE)}
then have 6: "¬ P x1" by (rule notI)}
then have 7: "∀x. ¬ P x" by (rule allI)
have 8: "False" using 1 7 by (rule notE)}
then show "∃x. P x" by (rule ccontr)
qed

-- Rocio Rodriguez

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

lemma ejercicio_17a:
assumes "∀x. ¬(P x)"
shows "¬(∃x. P x)"

proof
assume "∃x. P x"
then obtain a where "P a" by (rule exE)
have " ¬ (P a)" using assms by (rule allE)
show False using `¬(P a)` `P a` by (rule notE)
qed

--Jaime Alberto

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

lemma ejercicio_18a:
assumes "∃x. P x"
shows "¬(∀x. ¬(P x))"

proof
assume "∀x. ¬(P x)"
obtain a where "P a" using assms by (rule exE)
have "¬(P a)" using `∀x. ¬(P x)` by (rule allE)
show False using `¬(P a)` `P a`by (rule notE)
qed

-- Jaime Alberto

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

lemma ejercicio_19a:
assumes "P a ⟶ (∀x. Q x)"
shows "∀x. P a ⟶ Q x"

proof
fix b
show "P a ⟶ Q b"
proof
assume "P a"
have "∀x. Q x" using assms `P a` by (rule mp)
thus "Q b" by (rule allE)
qed
qed

--Jaime Alberto

text {* ---------------------------------------------------------------
Ejercicio 20. Demostrar
{∀x y z. R x y ∧ R y z ⟶ R x z,
∀x. ¬(R x x)}
⊢ ∀x y. R x y ⟶ ¬(R y x)
------------------------------------------------------------------ *}

lemma ejercicio_20a:
assumes "∀x y z. R x y ∧ R y z ⟶ R x z"
"∀x. ¬(R x x)"
shows "∀x y. R x y ⟶ ¬(R y x)"

proof (rule allI)+
fix a b
show "R a b ⟶ ¬(R b a )"
proof
assume 1:"R a b"
show"¬(R b a)"
proof
assume 2:"R b a"
have 3:"R a b ∧ R b a" using 1 2..
have "∀y z. R a y ∧ R y z ⟶ R a z" using assms(1)..
hence "∀z. R a b ∧ R b z ⟶ R a z"..
hence 4:"R a b ∧ R b a ⟶ R a a"..
have 5:"R a a" using 4 3..
have 6:" ¬(R a a)" using assms(2)..
show False using 6 5..
qed
qed
qed
--Jaime Alberto

text {* ---------------------------------------------------------------
Ejercicio 21. Demostrar
{∀x. P x ∨ Q x, ∃x. ¬(Q x), ∀x. R x ⟶ ¬(P x)} ⊢ ∃x. ¬(R x)
------------------------------------------------------------------ *}

lemma ejercicio_21a:
assumes "∀x. P x ∨ Q x"
"∃x. ¬(Q x)"
"∀x. R x ⟶ ¬(P x)"
shows "∃x. ¬(R x)"

proof-
obtain a where "¬(Q a)" using assms(2) by (rule exE)
have "P a ∨ Q a" using assms(1) by (rule allE)
show "∃x. ¬(R x)" using `P a ∨ Q a`
proof
assume "P a"
hence 1:"¬¬(P a)" by (rule notnotI)
have 2:"R a ⟶ ¬(P a)" using assms(3) by (rule allE)
have "¬(R a)" using 2 1 by (rule mt)
thus "∃x. ¬(R x)" by (rule exI)
next
assume "Q a"
have False using `¬(Q a)` `Q a` by (rule notE)
thus "∃x. ¬(R x)" by (rule ccontr)
qed
qed

-Jaime Alberto

text {* ---------------------------------------------------------------
Ejercicio 22. Demostrar
{∀x. P x ⟶ Q x ∨ R x, ¬(∃x. P x ∧ R x)} ⊢ ∀x. P x ⟶ Q x
------------------------------------------------------------------ *}

lemma ejercicio_22a:
assumes "∀x. P x ⟶ Q x ∨ R x"
"¬(∃x. P x ∧ R x)"
shows "∀x. P x ⟶ Q x"

proof
fix a
show "P a ⟶ Q a"
proof
assume 1:"P a"
have 2:"P a ⟶ Q a ∨ R a" using assms(1) by (rule allE)
have 3:"Q a ∨ R a" using 2 1 by (rule mp)
show "Q a" using 3
proof
assume "Q a"
next
assume 4:"R a"
have "P a ∧ R a" using 1 4 by (rule conjI)
hence 5:"∃x. P x ∧ R x" by (rule exI)
have False using assms(2) 5 by (rule notE)
thus "Q a" by (rule ccontr)
qed
qed
qed

--Jaime Alberto

text {* ---------------------------------------------------------------
Ejercicio 23. Demostrar
∃x y. R x y ∨ R y x ⊢ ∃x y. R x y
------------------------------------------------------------------ *}

lemma ejercicio_23a:
assumes "∃x y. R x y ∨ R y x"
shows "∃x y. R x y"

proof -
obtain a where "∃y. R a y ∨ R y a " using assms by (rule exE)
then obtain b where 1:"R a b ∨ R b a" by (rule exE)
show "∃x y. R x y" using 1
proof
assume "R a b"
hence "∃y. R a y" by (rule exI)
thus "∃x y. R x y" by (rule exI)
next
assume "R b a"
hence "∃y. R b y" by (rule exI)
thus "∃x y. R x y" by (rule exI)
qed
qed

--Jaime Alberto

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

lemma ejercicio_24a:
"(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"

proof
assume "∃x. ∀y. P x y"
then obtain a where 1:"∀y. P a y" by (rule exE)
{fix b
have "P a b" using 1 by (rule allE)
hence "∃x. P x b" by (rule exI)}
thus "∀y. ∃x. P x y" by (rule allI)
qed

-- Jaime Alberto

text {* ---------------------------------------------------------------
Ejercicio 25. Demostrar
(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)
------------------------------------------------------------------ *}

lemma ejercicio_25a:
"(∀x. P x ⟶ Q) ⟷ ((∃x. P x) ⟶ Q)"

proof
assume 1:"∀x. P x ⟶ Q"
show "(∃x. P x) ⟶ Q"
proof
assume "∃x. P x"
then obtain a where 3:"P a" by (rule exE)
have 4:"P a ⟶ Q"using 1 by (rule allE)
show "Q" using 4 3 by (rule mp)
qed
next
assume 5:"(∃x. P x) ⟶ Q"
show "∀x. P x ⟶ Q"
proof
fix a
show "P a⟶Q"
proof
assume "P a"
hence 6:"∃x. P x" by (rule exI)
show "Q" using 5 6 by (rule mp)
qed
qed
qed

--Jaime Alberto
text {* ---------------------------------------------------------------
Ejercicio 26. Demostrar
((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)
------------------------------------------------------------------ *}

lemma ejercicio_26a:
"((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
"((∀x. P x) ∧ (∀x. Q x)) ⟷ (∀x. P x ∧ Q x)"
proof
assume 0: "(∀x. P x) ∧ (∀x. Q x)"
have 1: "∀x. P x" using 0 by (rule conjunct1)
have 2: "∀x. Q x" using 0 by (rule conjunct2)
{fix a
have 3: "P a" using 1 by (rule allE)
have 4: "Q a" using 2 by (rule allE)
have 5: "P a ∧ Q a" using 3 4 by (rule conjI)}
thus "∀x. P x ∧ Q x" by (rule allI)
next
assume 0: "∀x. P x ∧ Q x"
{fix a
have 1: "P a ∧ Q a" using 0 by (rule allE)
have 2: "P a" using 1 by (rule conjunct1)}
hence 3: "∀x. P x" by (rule allI)
{fix a
have 4: "P a ∧ Q a" using 0 by (rule allE)
have 5: "Q a" using 4 by (rule conjunct2)}
hence 6: "∀x. Q x" by (rule allI)
show "(∀x. P x) ∧ (∀x. Q x)" using 3 6 by (rule conjI)
qed

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

lemma ejercicio_27a:
"((∀x. P x) ∨ (∀x. Q x)) ⟷ (∀x. P x ∨ Q x)"
proof
assume "(∀x. P x) ∨ (∀x. Q x)"
moreover
{assume "∀x. P x"
{fix a
have "P a" using `∀x. P x` by (rule allE)
have "P a ∨ Q a" using `P a` by (rule disjI1)}
hence "∀x. P x ∨ Q x" by (rule allI)}
moreover
{assume "∀x. Q x"
{fix a
have "Q a" using `∀x. Q x` by (rule allE)
have "P a ∨ Q a" using `Q a` by (rule disjI2)}
hence "∀x. P x ∨ Q x" by (rule allI)}
ultimately show "∀x. P x ∨ Q x" by (rule disjE)
next
assume "∀x. P x ∨ Q x"
oops

text{*
Consideremos los números naturales, ℕ. Sea P = "Ser par" y Q = "Ser impar". Claramente
∀x, P x ∨ Q x, pero es falso (∀x P x)∨(∀x Q x), pues no todo número es par
y no todo número es impar. Por tanto la propiedad, en general, es falsa. Es decir,
((∀x. P x) ∨ (∀x. Q x)) ⟶ (∀x. P x ∨ Q x) pero en general
(∀x. P x ∨ Q x) no implica ((∀x. P x) ∨ (∀x. Q x))
*}

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

lemma ejercicio_28a:
"((∃x. P x) ∨ (∃x. Q x)) ⟷ (∃x. P x ∨ Q x)"

proof
assume 1:"(∃x. P x) ∨ (∃x. Q x)"
show "∃x. P x ∨ Q x" using 1
proof
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
next
assume "∃x. P x ∨ Q x"
then obtain a where 2:"P a ∨ Q a" by (rule exE)
show "(∃x. P x) ∨ (∃x. Q x)" using 2
proof
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

-- Jaime Alberto

text {* ---------------------------------------------------------------
Ejercicio 29. Demostrar o refutar
(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)
------------------------------------------------------------------ *}

lemma ejercicio_29:

"(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)"
oops
text{*
Propiedad en general falsa. Sean los números naturales, y la propiedad P x y = "x + y es par". Claramente, para todo x, existe un y tal que P x y se verifica (baste tomar y = x). Pero, sea cual sea el y natural que tomemos, da igual el y que tomemos: no para todo elemento que le sumemos la suma será par.
*}

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

-- Francisco Javier Carmona

lemma ejercicio_30a:
"(¬(∀x. P x)) ⟷ (∃x. ¬P x)"
proof (rule iffI)
assume 1: "¬(∀x. P x)"
show "∃x. ¬P x"
proof (rule ccontr)
assume 2: "¬(∃x. ¬P x)"
show "False"
proof -
{ fix a
{ assume 3: "¬P a"
have 4: "∃x.¬ P x" using 3 by (rule exI)
have 5: "False" using 2 4 by (rule notE)}
hence 6: "P a" by (rule ccontr)}
hence 7: "∀x. P x" by (rule allI)
show 8: "False" using 1 7 by (rule notE)
qed
qed
next
assume 9: "∃x. ¬P x"
show "¬(∀x. P x)"
proof -
{assume 10: "¬¬(∀x. P x)"
have 11: "∀x. P x" using 10 by (rule notnotD)
obtain a where 12: "¬P a" using 9 by (rule exE)
have 13: "P a" using 11 by (rule allE)
have 14: "False" using 12 13 by (rule notE)}
thus 15: "¬(∀x. P x)" by (rule ccontr)
qed
qed

section {* Ejercicios sobre igualdad *}

text {* ---------------------------------------------------------------
Ejercicio 31. Demostrar o refutar
P a ⟹ ∀x. x = a ⟶ P x
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_31a:
assumes "P a"
shows "∀x. x = a ⟶ P x"
proof (rule allI)
fix b
show "b = a ⟶ P b"
proof (rule impI)
assume 1: "b = a"
show "P b"
proof -
have 2: "a = b" using 1 by (rule sym)
show 3: "P b" using 2 assms(1) by (rule subst)
qed
qed
qed

text {* ---------------------------------------------------------------
Ejercicio 32. Demostrar o refutar
∃x y. R x y ∨ R y x; ¬(∃x. R x x)⟧ ⟹ ∃x y. x ≠ y
------------------------------------------------------------------ *}

lemma ejercicio_32a:
fixes R :: "'c ⇒ 'c ⇒ bool"
assumes "∃x y. R x y ∨ R y x"
"¬(∃x. R x x)"
shows "∃(x::'c) y. x ≠ y"
oops

text {* ---------------------------------------------------------------
Ejercicio 33. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)}
⊢ P (f a) a (f a)
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_33a:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "P (f a) a (f a)"
proof -
have 1: "P a a a" using assms(1) by (rule allE)
have 2: "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
have 3: "∀z. P a a z ⟶ P (f a) a (f z)" using 2 by (rule allE)
have 4: "P a a a ⟶ P (f a) a (f a)" using 3 by (rule allE)
show 5: "P (f a) a (f a)" using 4 1 by (rule mp)
qed

text {* ---------------------------------------------------------------
Ejercicio 34. Demostrar o refutar
{∀x. P a x x,
∀x y z. P x y z ⟶ P (f x) y (f z)⟧
⊢ ∃z. P (f a) z (f (f a))
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_34a:
assumes "∀x. P a x x"
"∀x y z. P x y z ⟶ P (f x) y (f z)"
shows "∃z. P (f a) z (f (f a))"
proof -
have 1: "P a (f a) (f a)" using assms(1) by (rule allE)
have 2: "∀y z. P a y z ⟶ P (f a) y (f z)" using assms(2) by (rule allE)
have 3: "∀z. P a (f a) z ⟶ P (f a) (f a) (f z)" using 2 by (rule allE)
have 4: "P a (f a) (f a) ⟶ P (f a) (f a) (f (f a))" using 3 by (rule allE)
have 5: "P (f a) (f a) (f (f a))" using 4 1 by (rule mp)
show 6: "∃z. P (f a) z (f (f a))" using 5 by (rule exI)
qed

text {* ---------------------------------------------------------------
Ejercicio 35. Demostrar o refutar
{∀y. Q a y,
∀x y. Q x y ⟶ Q (s x) (s y)}
⊢ ∃z. Qa z ∧ Q z (s (s a))
------------------------------------------------------------------ *}

-- Francisco Javier Carmona

lemma ejercicio_35a:
assumes "∀y. Q a y"
"∀x y. Q x y ⟶ Q (s x) (s y)"
shows "∃z. Q a z ∧ Q z (s (s a))"
proof -
have 1: "Q a (s a)" using assms(1) by (rule allE)
have 2: "∀y. Q a y ⟶ Q (s a) (s y)" using assms(2) by (rule allE)
have 3: "Q a (s a) ⟶ Q (s a) (s (s a))" using 2 by (rule allE)
have 4: "Q (s a) (s (s a))" using 3 1 by (rule mp)
have 5: "Q a (s a) ∧ Q (s a) (s (s a))" using 1 4 by (rule conjI)
show 6: "∃z. Q a z ∧ Q z (s (s a))" using 5 by (rule exI)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_36a:
assumes "x = f x" and
"odd (f x)"
shows "odd x"
proof -
show "odd x" using assms(1) assms(2) by (rule ssubst)
qed

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

-- Francisco Javier Carmona

lemma ejercicio_37a:
assumes "x = f x" and
"triple (f x) (f x) x"
shows "triple x x x"
proof -
show "triple x x x" using assms(1) assms(2) by (rule ssubst)
qed

end

</source>

Rel 4

2018-07-16T12:27:09Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

Rel 5

2018-07-16T12:27:09Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang="isabelle">
header {* R5: Argumentación en lógica de primer orden *}

theory R5_sol
imports Main
begin

text {*
---------------------------------------------------------------------
El objetivo de esta relación es formalizar en lógica de primer orden
argumentos expresados en lenguaje natural.

Antes de escribir la soluciones, comprobar con APLI2 la corrección de la
formalización.
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 1. Formalizar el siguiente argumento
Sócrates es un hombre.
Los hombres son mortales.
Luego, Sócrates es mortal.
Usar s para Sócrates
H(x) para x es un hombre
M(x) para x es mortal
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 2. Formalizar el siguiente argumento
Hay estudiantes inteligentes y hay estudiantes trabajadores. Por
tanto, hay estudiantes inteligentes y trabajadores.
Usar I(x) para x es inteligente
T(x) para x es trabajador
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 3. Formalizar el siguiente argumento
Todos los participantes son vencedores. Hay como máximo un
vencedor. Hay como máximo un participante. Por lo tanto, hay
exactamente un participante.
Usar P(x) para x es un participante
V(x) para x es un vencedor
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 4. Formalizar el siguiente argumento
Todo aquel que entre en el país y no sea un VIP será cacheado por
un aduanero. Hay un contrabandista que entra en el país y que solo
podrá ser cacheado por contrabandistas. Ningún contrabandista es un
VIP. Por tanto, algún aduanero es contrabandista.
Usar A(x) para x es aduanero
Ca(x,y) para x cachea a y
Co(x) para x es contrabandista
E(x) para x entra en el pais
V(x) para x es un VIP
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 5. Formalizar el siguiente argumento
Juan teme a María. Pedro es temido por Juan. Luego, alguien teme a
María y a Pedro.
Usar j para Juan
m para María
p para Pedro
T(x,y) para x teme a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 6. Formalizar el siguiente argumento
Los hermanos tienen el mismo padre. Juan es hermano de Luis. Carlos
es padre de Luis. Por tanto, Carlos es padre de Juan.
Usar H(x,y) para x es hermano de y
P(x,y) para x es padre de y
j para Juan
l para Luis
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 7. Formalizar el siguiente argumento
La existencia de algún canal de TV pública, supone un acicate para
cualquier canal de TV privada; el que un canal de TV tenga un
acicate, supone una gran satisfacción para cualquiera de sus
directivos; en Madrid hay varios canales públicos de TV; TV5 es un
canal de TV privada; por tanto, todos los directivos de TV5 están
satisfechos.
Usar Pu(x) para x es un canal de TV pública
Pr(x) para x es un canal de TV privada
A(x) para x posee un acicate
D(x,y) para x es un directivo del canal y
S(x) para x está satisfecho
t para TV5
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 8. Formalizar el siguiente argumento
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.
Usar E(x) para x entra en un país
P(x) para x tiene pasaporte
A(x) para x es aduanero
I(x,y) para x impide el paso a y
M(x) para x está motorizada
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 9. Formalizar el siguiente argumento
Los aficionados al fútbol aplauden a cualquier futbolista
extranjero. Juanito no aplaude a futbolistas extranjeros. Por
tanto, si hay algún futbolista extranjero nacionalizado español,
Juanito no es aficionado al fútbol.
Usar Af(x) para x es aficicionado al fútbol
Ap(x,y) para x aplaude a y
E(x) para x es un futbolista extranjero
N(x) para x es un futbolista nacionalizado español
j para Juanito
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 10. Formalizar el siguiente argumento
Ningún aristócrata debe ser condenado a galeras a menos que sus
crímenes sean vergonzosos y lleve una vida licenciosa. En la ciudad
hay aristócratas que han cometido crímenes vergonzosos aunque su
forma de vida no sea licenciosa. Por tanto, hay algún aristócrata
que no está condenado a galeras.
Usar A(x) para x es aristócrata
G(x) para x está condenado a galeras
L(x) para x lleva una vida licenciosa
V(x) para x ha cometido crímenes vergonzoso
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 11. Formalizar el siguiente argumento
Todo individuo que esté conforme con el contenido de cualquier
acuerdo internacional lo apoya o se inhibe en absoluto de asuntos
políticos. Cualquiera que se inhiba de los asuntos políticos, no
participará en el próximo referéndum. Todo español, está conforme
con el acuerdo internacional de Maastricht, al que sin embargo no
apoya. Por tanto, cualquier individuo o no es español, o en otro
caso, está conforme con el contenido del acuerdo internacional de
Maastricht y no participará en el próximo referéndum.
Usar C(x,y) para la persona x conforme con el contenido del acuerdo y
A(x,y) para la persona x apoya el acuerdo y
I(x) para la persona x se inibe de asuntos políticos
R(x) para la persona x participará en el próximo referéndum
E(x) para la persona x es española
m para el acuerdo de Maastricht
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 12. Formalizar el siguiente argumento
Toda persona pobre tiene un padre rico. Por tanto, existe una
persona rica que tiene un abuelo rico.
Usar R(x) para x es rico
p(x) para el padre de x
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 13. Formalizar el siguiente argumento
Todo deprimido que estima a un submarinista es listo. Cualquiera
que se estime a sí mismo es listo. Ningún deprimido se estima a sí
mismo. Por tanto, ningún deprimido estima a un submarinista.
Usar D(x) para x está deprimido
E(x,y) para x estima a y
L(x) para x es listo
S(x) para x es submarinista
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 14. Formalizar el siguiente argumento
Todos los robots obedecen a los amigos del programador jefe.
Alvaro es amigo del programador jefe, pero Benito no le
obedece. Por tanto, Benito no es un robot.
Usar R(x) para x es un robot
Ob(x,y) para x obedece a y
A(x) para x es amigo del programador jefe
b para Benito
a para Alvaro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 15. Formalizar el siguiente argumento
En una pecera nadan una serie de peces. Se observa que:
* Hay algún pez x que para cualquier pez y, si el pez x no se come
al pez y entonces existe un pez z tal que z es un tiburón o bien
z protege al pez y.
* No hay ningún pez que se coma a todos los demás.
* Ningún pez protege a ningún otro.
Por tanto, existe algún tiburón en la pecera.
Usar C(x,y) para x se come a y
P(x,y) para x protege a y
T(x) para x es un tiburón
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 16. Formalizar el siguiente argumento
Supongamos conocidos los siguientes hechos acerca del número de
aprobados de dos asignaturas A y B:
* Si todos los alumnos aprueban la asignatura A, entonces todos
aprueban la asignatura B.
* Si algún delegado de la clase aprueba A y B, entonces todos los
alumnos aprueban A.
* Si nadie aprueba B, entonces ningún delegado aprueba A.
* Si Manuel no aprueba B, entonces nadie aprueba B.
Por tanto, si Manuel es un delegado y aprueba la asignatura A,
entonces todos los alumnos aprueban las asignaturas A y B.
Usar A(x,y) para x aprueba la asignatura y
D(x) para x es delegado
m para Manuel
a para la asignatura A
b para la asignatura B
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 17. Formalizar el siguiente argumento
En cierto país oriental se ha celebrado la fase final del
campeonato mundial de fútbol. Cierto diario deportivo ha publicado
las siguientes estadísticas de tan magno acontecimiento:
* A todos los porteros que no vistieron camiseta negra les marcó un
gol algún delantero europeo.
* Algún portero jugó con botas blancas y sólo le marcaron goles
jugadores con botas blancas.
* Ningún portero se marcó un gol a sí mismo.
* Ningún jugador con botas blancas vistió camiseta negra.
Por tanto, algún delantero europeo jugó con botas blancas.
Usar P(x) para x es portero
D(x) para x es delantero europeo
N(x) para x viste camiseta negra
B(x) para x juega con botas blancas
M(x,y) para x marcó un gol a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 18. Formalizar el siguiente argumento
Las relaciones de parentesco verifican la siguientes propiedades
generales:
* Si x es hermano de y, entonces y es hermano de x.
* Todo el mundo es hijo de alguien.
* Nadie es hijo del hermano de su padre.
* Cualquier padre de una persona es también padre de todos los
hermanos de esa persona.
* Nadie es hijo ni hermano de sí mismo.
Tenemos los siguientes miembros de la familia Peláez: Don Antonio,
Don Luis, Antoñito y Manolito y sabemos que Don Antonio y Don Luis
son hermanos, Antoñito y Manolito son hermanos, y Antoñito es hijo
de Don Antonio. Por tanto, Don Luis no es el padre de Manolito.
Usar A para Don Antonio
He(x,y) para x es hermano de y
Hi(x,y) para x es hijo de y
L para Don Luis
a para Antoñito
m para Manolito
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 19. [Problema del apisonador de Schubert (en inglés,
"Schubert’s steamroller")] Formalizar el siguiente argumento
Si uno de los miembros del club afeita a algún otro (incluido a
sí mismo), entonces todos los miembros del club lo han afeitado
a él (aunque no necesariamente al mismo tiempo). Guido, Lorenzo,
Petruccio y Cesare pertenecen al club de barberos. Guido ha
afeitado a Cesare. Por tanto, Petruccio ha afeitado a Lorenzo.
Usar g para Guido
l para Lorenzo
p para Petruccio
c para Cesare
B(x) para x es un miembro del club de barberos
A(x,y) para x ha afeitado a y
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 20. Formalizar el siguiente argumento
Carlos afeita a todos los habitantes de Las Chinas que no se
afeitan a sí mismo y sólo a ellos. Carlos es un habitante de las
Chinas. Por consiguiente, Carlos no afeita a nadie.
Usar A(x,y) para x afeita a y
C(x) para x es un habitante de Las Chinas
c para Carlos
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 21. Formalizar el siguiente argumento
Quien desprecia a todos los fanáticos desprecia también a todos los
políticos. Alguien no desprecia a un determinado político. Por
consiguiente, hay un fanático al que no todo el mundo desprecia.
Usar D(x,y) para x desprecia a y
F(x) para x es fanático
P(x) para x es político
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 22. Formalizar el siguiente argumento
El hombre puro ama todo lo que es puro. Por tanto, el hombre puro
se ama a sí mismo.
Usar A(x,y) para x ama a y
H(x) para x es un hombre
P(x) para x es puro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 23. Formalizar el siguiente argumento
Ningún socio del club está en deuda con el tesorero del club. Si
un socio del club no paga su cuota está en deuda con el tesorero
del club. Por tanto, si el tesorero del club es socio del club,
entonces paga su cuota.
Usar P(x) para x es socio del club
Q(x) para x paga su cuota
R(x) para x está en deuda con el tesorero
a para el tesorero del club
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 24. Formalizar el siguiente argumento
1. Los lobos, zorros, pájaros, orugas y caracoles son animales y
existen algunos ejemplares de estos animales.
2. También hay algunas semillas y las semillas son plantas.
3. A todo animal le gusta o bien comer todo tipo de plantas o bien
le gusta comerse a todos los animales más pequeños que él mismo
que gustan de comer algunas plantas.
4. Las orugas y los caracoles son mucho más pequeños que los
pájaros, que son mucho más pequeños que los zorros que a su vez
son mucho más pequeños que los lobos.
5. A los lobos no les gusta comer ni zorros ni semillas, mientras
que a los pájaros les gusta comer orugas pero no caracoles.
6. Las orugas y los caracoles gustan de comer algunas plantas.
7. Luego, existe un animal al que le gusta comerse un animal al que
le gusta comer semillas.
Usar A(x) para x es un animal
Ca(x) para x es un caracol
Co(x,y) para x le gusta comerse a y
L(x) para x es un lobo
M(x,y) para x es más pequeño que y
Or(x) para x es una oruga
Pa(x) para x es un pájaro
Pl(x) para x es una planta
S(x) para x es una semilla
Z(x) para x es un zorro
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 25. Formalizar el siguiente argumento
Rosa ama a Curro. Paco no simpatiza con Ana. Quien no simpatiza con
Ana ama a Rosa. Si una persona ama a otra, la segunda ama a la
primera. Hay como máximo una persona que ama a Rosa. Por tanto,
Paco es Curro.
Usar A(x,y) para x ama a y
S(x,y) para x simpatiza con y
a para Ana
c para Curro
p para Paco
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 26. Formalizar el siguiente argumento
Sólo hay un sofista que enseña gratuitamente, y éste es
Sócrates. Sócrates argumenta mejor que ningún otro sofista. Platón
argumenta mejor que algún sofista que enseña gratuitamente. Si una
persona argumenta mejor que otra segunda, entonces la segunda no
argumenta mejor que la primera. Por consiguiente, Platón no es un
sofista.
Usar G(x) para x enseña gratuitamente
M(x,y) para x argumenta mejor que y
S(x) para x es un sofista
p para Platón
s para Sócrates
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 27. Formalizar el siguiente argumento
Todos los filósofos se han preguntado qué es la filosofía. Los que
se preguntan qué es la filosofía se vuelven locos. Nietzsche es
filósofo. El maestro de Nietzsche no acabó loco. Por tanto,
Nietzsche y su maestro son diferentes personas.
Usar F(x) para x es filósofo
L(x) para x se vuelve loco
P(x) para x se ha preguntado qué es la filosofía.
m para el maestro de Nietzsche
n para Nietzsche
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 28. Formalizar el siguiente argumento
Los padres son mayores que los hijos. Juan es el padre de Luis. Por
tanto, Juan es mayor que Luis.
Usar M(x,y) para x es mayor que y
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 29. Formalizar el siguiente argumento
El esposo de la hermana de Toni es Roberto. La hermana de Toni es
María. Por tanto, el esposo de María es Roberto.
Usar e(x) para el esposo de x
h para la hermana de Toni
m para María
r para Roberto
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 30. Formalizar el siguiente argumento
Luis y Jaime tienen el mismo padre. La madre de Rosa es
Eva. Eva ama a Carlos. Carlos es el padre de Jaime. Por tanto,
la madre de Rosa ama al padre de Luis.
Usar A(x,y) para x ama a y
m(x) para la madre de x
p(x) para el padre de x
c para Carlos
e para Eva
j para Jaime
l para Luis
r para Rosa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 31. Formalizar el siguiente argumento
Si dos personas son hermanos, entonces tienen la misma madre y el
mismo padre. Juan es hermano de Luis. Por tanto, la madre del padre
de Juan es la madre del padre de Luis.
Usar H(x,y) para x es hermano de y
m(x) para la madre de x
p(x) para el padre de x
j para Juan
l para Luis
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 32. Formalizar el siguiente argumento
Todos los miembros del claustro son asturianos. El secretario forma
parte del claustro. El señor Martínez es el secretario. Por tanto,
el señor Martínez es asturiano.
Usar C(x) para x es miembro del claustro
A(x) para x es asturiano
s para el secretario
m para el señor Martínez
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 33. Formalizar el siguiente argumento
Eduardo pudo haber visto al asesino. Antonio fue el primer testigo
de la defensa. O Eduardo estaba en clase o Antonio dio falso
testimonio. Nadie en clase pudo haber visto al asesino. Luego, el
primer testigo de la defensa dio falso testimonio.
Usar C(x) para x estaba en clase
F(x) para x dio falso testimonio
V(x) para x pudo haber visto al asesino
a para Antonio
e para Eduardo
p para el primer testigo de la defensa
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 34. Formalizar el siguiente argumento
La luna hoy es redonda. La luna de hace dos semanas tenía forma de
cuarto creciente. Luna no hay más que una, es decir, siempre es la
misma. Luego existe algo que es a la vez redondo y con forma de
cuarto creciente.
Usar L(x) para la luna del momento x
R(x) para x es redonda
C(x) para x tiene forma de cuarto creciente
h para hoy
d para hace dos semanas
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 35. Formalizar el siguiente argumento
Juana sólo tiene un marido. Juana está casada con Tomás. Tomás es
delgado y Guillermo no. Luego, Juana no está casada con Guillermo.
Usar D(x) para x es delgado
C(x,y) para x está casada con y
g para Guillermo
j para Juana
t para Tomás
------------------------------------------------------------------ *}

text {* ---------------------------------------------------------------
Ejercicio 36. Formalizar el siguiente argumento
Sultán no es Chitón. Sultán no obtendrá un plátano a menos que
pueda resolver cualquier problema. Si el chimpancé Chitón trabaja
más que Sultán resolverá problemas que Sultán no puede resolver.
Todos los chimpancés distintos de Sultán trabajan más que Sultán.
Por consiguiente, Sultán no obtendrá un plátano.
Usar Pl(x) para x obtiene el plátano
Pr(x) para x es un problema
R(x,y) para x resuelve y
T(x,y) para x trabaja más que y
c para Chitón
s para Sultán
------------------------------------------------------------------ *}

end
</source>

Relación 14

2018-07-16T12:27:09Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang = "isabelle">
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>

Ejercicio 5 (a)

2018-07-16T12:27:08Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang="isabelle">
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: ⟦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. ∀y. ¬(P(y) ⟶ R(x,y))) ⟶ ¬(∀x. P(x) ⟶ R(x,x))"
proof (rule impI)
assume "∃x. ∀y. ¬(P(y) ⟶ R(x,y))"
then obtain a where "∀y. ¬(P(y) ⟶ R(a,y))" by (rule exE)
show "¬(∀x. P(x) ⟶ R(x,x))"
proof (rule notI)
assume "∀x. P(x) ⟶ R(x,x)"
then have "P(a) ⟶ R(a,a)" by (rule allE)
have "¬(P(a) ⟶ R(a,a))" using `∀y. ¬(P(y) ⟶ R(a,y))` by (rule allE)
then show False using `P(a) ⟶ R(a,a)` by (rule notE)
qed
qed

end
</source>

Ejercicio 5 (b)

2018-07-16T12:27:08Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang="isabelle">
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>

R14

2018-07-16T12:27:08Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

<source lang = "isabelle">
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. 27: 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>

Rel 3

2018-07-16T12:27:08Z

WikiSysop: Texto reemplazado: «isar» por «isabelle»

MediaWiki:Common.css

2018-07-16T12:26:16Z

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

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

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

2015-02-07T11:11:45Z

WikiSysop: Página creada con '== Relaciones de ejercicios == En esta página se publicarán las relaciones de ejercicios y sus soluciones colaborativas.'

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

MediaWiki:Mainpage

2015-02-07T11:10:30Z

WikiSysop: Página creada con 'Lógica matemática y fundamentos (2014-15)'

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

MediaWiki:Sidebar

2015-02-07T11:09:42Z

WikiSysop: Página creada con '* navigation ** mainpage|mainpage-description ** recentchanges-url|recentchanges * SEARCH * TOOLBOX * LANGUAGES'

* navigation
** mainpage|mainpage-description
** recentchanges-url|recentchanges
* SEARCH
* TOOLBOX
* LANGUAGES