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

En la primera parte de 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 3 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 {*
  --------------------------------------------------------------------- 
  El objetivo de esta es relación formalizar y demostrar la corrección
  de los argumentos 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

text {* --------------------------------------------------------------- 
  Ejercicio 3. Formalizar, y demostrar la corrección, del siguiente
  argumento 
     Si no hay control de nacimientos, entonces la población crece
     ilimitadamente; pero si la población crece ilimitadamente,
     aumentará el índice de pobreza. Por consiguiente, si no hay control
     de nacimientos, aumentará el índice de pobreza. 
  Usar N: Hay control de nacimientos. 
       P: La población crece ilimitadamente,
       I: Aumentará el índice de pobreza. 
  ------------------------------------------------------------------ *}

-- "La demostración automática es"
lemma ejercicio_3_1:
  "⟦¬N ⟶ P; P ⟶ I⟧ ⟹ ¬N ⟶ I"
by auto

-- "La demostración estructurada es"
lemma ejercicio_3_2:
  assumes "¬N ⟶ P" 
          "P ⟶ I" 
  shows   "¬N ⟶ I"
proof
  assume "¬N"
  with assms(1) have "P" ..
  with assms(2) show "I" ..
qed

-- "La demostración detallada es"
lemma ejercicio_3_3:
  assumes "¬N ⟶ P" 
          "P ⟶ I" 
  shows   "¬N ⟶ I"
proof (rule impI)
  assume "¬N"
  with assms(1) have "P" by (rule mp)
  with assms(2) show "I" by (rule mp)
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

131

132

133

134

135

136

137

138

139

140

141

142

143

144

145

146

147

148

149

150

text {*

---------------------------------------------------------------------

El objetivo de esta es relación formalizar y demostrar la corrección

de los argumentos 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

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

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

argumento

Si no hay control de nacimientos, entonces la población crece

ilimitadamente; pero si la población crece ilimitadamente,

aumentará el índice de pobreza. Por consiguiente, si no hay control

de nacimientos, aumentará el índice de pobreza.

Usar N: Hay control de nacimientos.

P: La población crece ilimitadamente,

I: Aumentará el índice de pobreza.

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

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

lemma ejercicio_3_1:

"⟦¬N ⟶ P; P ⟶ I⟧ ⟹ ¬N ⟶ I"

by auto

-- "La demostración estructurada es"

lemma ejercicio_3_2:

assumes "¬N ⟶ P"

"P ⟶ I"

shows "¬N ⟶ I"

proof

assume "¬N"

with assms(1) have "P" ..

with assms(2) show "I" ..

qed

-- "La demostración detallada es"

lemma ejercicio_3_3:

assumes "¬N ⟶ P"

"P ⟶ I"

shows "¬N ⟶ I"

proof (rule impI)

assume "¬N"

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

with assms(2) show "I" by (rule mp)

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