LMF2013: Ejercicios de argumentación en lógica proposicional con Isabelle/HOL

En la clase de hoy del curso Lógica matemática y fundamentos se ha explicado cómo formalizar en lógica proposicional los argumentos de los ejercicios 8 y 9 de la relación 4 y cómo demostrar con Isabelle/HOL su corrección.

Los ejercicios y sus soluciones se muestran a continuación:

text {* --------------------------------------------------------------- 
  Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si el general era leal, hubiera obedecido las órdenes, y si era
     inteligente las hubiera comprendido. O el general desobedeció las
     órdenes o no las comprendió. Luego, el general era desleal o no era
     inteligente. 
  Usar L:  El general es leal.
       Ob: El general obedece las órdenes.
       I:  El general es inteligente.
       C:  El general comprende las órdenes.
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_8_1:
  assumes "(L ⟶ Ob) ∧ (I ⟶ C)" 
          "¬Ob ∨ ¬C" 
  shows   "¬L ∨ ¬I"
using assms
by auto

-- "La demostración estructurada es"
lemma ejercicio_8_2:
  assumes "(L ⟶ Ob) ∧ (I ⟶ C)" 
          "¬Ob ∨ ¬C" 
  shows   "¬L ∨ ¬I"
using assms(2)
proof
  assume "¬Ob"
  have "L ⟶ Ob" using assms(1) ..
  hence "¬L" using `¬Ob` by (rule mt)
  thus "¬L ∨ ¬I" ..
next
  assume "¬C"
  have "I ⟶ C" using assms(1) ..
  hence "¬I" using `¬C` by (rule mt)
  thus "¬L ∨ ¬I" ..
qed

-- "La demostración detallada es"
lemma ejercicio_8_3:
  assumes "(L ⟶ Ob) ∧ (I ⟶ C)" 
          "¬Ob ∨ ¬C" 
  shows   "¬L ∨ ¬I"
using assms(2)
proof (rule disjE)
  assume "¬Ob"
  have "L ⟶ Ob" using assms(1) by (rule conjunct1)
  hence "¬L" using `¬Ob` by (rule mt)
  thus "¬L ∨ ¬I" by (rule disjI1)
next
  assume "¬C"
  have "I ⟶ C" using assms(1) by (rule conjunct2)
  hence "¬I" using `¬C` by (rule mt)
  thus "¬L ∨ ¬I" by (rule disjI2)
qed

text {* --------------------------------------------------------------- 
  Ejercicio 9. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo
     haría. Si Dios fuera incapaz de evitar el mal, no sería
     omnipotente; si no quisiera evitar el mal sería malévolo. Dios no
     evita el mal. Si Dios existe, es omnipotente y no es
     malévolo. Luego, Dios no existe. 
  Usar C:  Dios es capaz de evitar el mal.
       Q:  Dios quiere evitar el mal.
       Om: Dios es omnipotente.
       M:  Dios es malévolo.
       P:  Dios evita el mal.
       E:  Dios existe.
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_9_1:
  assumes "C ∧ Q ⟶ P" 
          "(¬C ⟶ ¬Om) ∧ (¬Q ⟶ M)" 
          "¬P" 
          "E ⟶ Om ∧ ¬M" 
  shows   "¬E"
using assms
by auto

-- "La demostración estructurada es"
lemma ejercicio_9_2:
  assumes "C ∧ Q ⟶ P" 
          "(¬C ⟶ ¬Om) ∧ (¬Q ⟶ M)" 
          "¬P" 
          "E ⟶ Om ∧ ¬M" 
  shows   "¬E"
proof
  assume "E"
  have "Om ∧ ¬M" using assms(4) `E` ..
  hence "Om" ..
  hence "¬¬Om" by (rule notnotI)
  have "¬C ⟶ ¬Om" using assms(2) ..
  hence "¬¬C" using `¬¬Om` by (rule mt)
  hence "C" by (rule notnotD)
  have "¬M" using `Om ∧ ¬M` ..
  have "¬Q ⟶ M" using assms(2) ..
  hence "¬¬Q" using `¬M` by (rule mt)
  hence "Q" by (rule notnotD)
  with `C` have "C ∧ Q" ..
  with assms(1) have "P" ..
  with assms(3) show False ..
qed

-- "La demostración detallada es"
lemma ejercicio_9_3:
  assumes "C ∧ Q ⟶ P" 
          "(¬C ⟶ ¬Om) ∧ (¬Q ⟶ M)" 
          "¬P" 
          "E ⟶ Om ∧ ¬M" 
  shows   "¬E"
proof (rule notI)
  assume "E"
  with assms(4) have "Om ∧ ¬M" by (rule mp)
  hence "Om" by (rule conjunct1)
  hence "¬¬Om" by (rule notnotI)
  have "¬C ⟶ ¬Om" using assms(2) by (rule conjunct1)
  hence "¬¬C" using `¬¬Om` by (rule mt)
  hence "C" by (rule notnotD)
  have "¬M" using `Om ∧ ¬M` by (rule conjunct2)
  have "¬Q ⟶ M" using assms(2) by (rule conjunct2)
  hence "¬¬Q" using `¬M` by (rule mt)
  hence "Q" by (rule notnotD)
  with `C` have "C ∧ Q" by (rule conjI)
  with assms(1) have "P" by (rule mp)
  with assms(3) show False by (rule notE)
qed

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

129

130

text {* ---------------------------------------------------------------

Ejercicio 8. Formalizar, y demostrar la corrección, del siguiente

argumento

Si el general era leal, hubiera obedecido las órdenes, y si era

inteligente las hubiera comprendido. O el general desobedeció las

órdenes o no las comprendió. Luego, el general era desleal o no era

inteligente.

Usar L: El general es leal.

Ob: El general obedece las órdenes.

I: El general es inteligente.

C: El general comprende las órdenes.

------------------------------------------------------------------ *}

-- "La demostración automática es"

lemma ejercicio_8_1:

assumes "(L ⟶ Ob) ∧ (I ⟶ C)"

"¬Ob ∨ ¬C"

shows "¬L ∨ ¬I"

using assms

by auto

-- "La demostración estructurada es"

lemma ejercicio_8_2:

assumes "(L ⟶ Ob) ∧ (I ⟶ C)"

"¬Ob ∨ ¬C"

shows "¬L ∨ ¬I"

using assms(2)

proof

assume "¬Ob"

have "L ⟶ Ob" using assms(1) ..

hence "¬L" using `¬Ob` by (rule mt)

thus "¬L ∨ ¬I" ..

assume "¬C"

have "I ⟶ C" using assms(1) ..

hence "¬I" using `¬C` by (rule mt)

thus "¬L ∨ ¬I" ..

qed

-- "La demostración detallada es"

lemma ejercicio_8_3:

assumes "(L ⟶ Ob) ∧ (I ⟶ C)"

"¬Ob ∨ ¬C"

shows "¬L ∨ ¬I"

using assms(2)

proof (rule disjE)

assume "¬Ob"

have "L ⟶ Ob" using assms(1) by (rule conjunct1)

hence "¬L" using `¬Ob` by (rule mt)

thus "¬L ∨ ¬I" by (rule disjI1)

assume "¬C"

have "I ⟶ C" using assms(1) by (rule conjunct2)

hence "¬I" using `¬C` by (rule mt)

thus "¬L ∨ ¬I" by (rule disjI2)

qed

text {* ---------------------------------------------------------------

Ejercicio 9. Formalizar, y demostrar la corrección, del siguiente

argumento

Si Dios fuera capaz de evitar el mal y quisiera hacerlo, lo

haría. Si Dios fuera incapaz de evitar el mal, no sería

omnipotente; si no quisiera evitar el mal sería malévolo. Dios no

evita el mal. Si Dios existe, es omnipotente y no es

malévolo. Luego, Dios no existe.

Usar C: Dios es capaz de evitar el mal.

Q: Dios quiere evitar el mal.

Om: Dios es omnipotente.

M: Dios es malévolo.

P: Dios evita el mal.

E: Dios existe.

------------------------------------------------------------------ *}

-- "La demostración automática es"

lemma ejercicio_9_1:

assumes "C ∧ Q ⟶ P"

"(¬C ⟶ ¬Om) ∧ (¬Q ⟶ M)"

"¬P"

"E ⟶ Om ∧ ¬M"

shows "¬E"

using assms

by auto

-- "La demostración estructurada es"

lemma ejercicio_9_2:

assumes "C ∧ Q ⟶ P"

"(¬C ⟶ ¬Om) ∧ (¬Q ⟶ M)"

"¬P"

"E ⟶ Om ∧ ¬M"

shows "¬E"

proof

assume "E"

have "Om ∧ ¬M" using assms(4) `E` ..

hence "Om" ..

hence "¬¬Om" by (rule notnotI)

have "¬C ⟶ ¬Om" using assms(2) ..

hence "¬¬C" using `¬¬Om` by (rule mt)

hence "C" by (rule notnotD)

have "¬M" using `Om ∧ ¬M` ..

have "¬Q ⟶ M" using assms(2) ..

hence "¬¬Q" using `¬M` by (rule mt)

hence "Q" by (rule notnotD)

with `C` have "C ∧ Q" ..

with assms(1) have "P" ..

with assms(3) show False ..

qed

-- "La demostración detallada es"

lemma ejercicio_9_3:

assumes "C ∧ Q ⟶ P"

"(¬C ⟶ ¬Om) ∧ (¬Q ⟶ M)"

"¬P"

"E ⟶ Om ∧ ¬M"

shows "¬E"

proof (rule notI)

assume "E"

with assms(4) have "Om ∧ ¬M" by (rule mp)

hence "Om" by (rule conjunct1)

hence "¬¬Om" by (rule notnotI)

have "¬C ⟶ ¬Om" using assms(2) by (rule conjunct1)

hence "¬¬C" using `¬¬Om` by (rule mt)

hence "C" by (rule notnotD)

have "¬M" using `Om ∧ ¬M` by (rule conjunct2)

have "¬Q ⟶ M" using assms(2) by (rule conjunct2)

hence "¬¬Q" using `¬M` by (rule mt)

hence "Q" by (rule notnotD)

with `C` have "C ∧ Q" by (rule conjI)

with assms(1) have "P" by (rule mp)

with assms(3) show False by (rule notE)

qed

Se puede imprimir o compartir con