LMF2014: Deducción natural en lógica de primer orden

En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la primera parte de la deducción natural en la lógica de primer orden.

Las transparencias de estas clases son las páginas 1 a 13 del tema 8.

A la vez que se presentaba las reglas, se ha comentado su formalización en Isabelle/HOL. La teoría correspondiente es

header {* Tema 8: Deducción natural en lógica de primer orden *}

theory T8
imports Main 
begin

section {* Reglas del cuantificador universal *}

text {*
  Las reglas del cuantificador universal son
  · allE:    ⟦∀x. P x; P a ⟹ R⟧ ⟹ R
  · allI:    (⋀x. P x) ⟹ ∀x. P x
  *}

text {* 
  Ejemplo 1 (p. 10). Demostrar que
     P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c)
*}

-- "La demostración detallada es"
lemma ejemplo_1a: 
  assumes 1: "P(c)" and
          2: "∀x. (P(x) ⟶ ¬Q(x))"
  shows "¬Q(c)"
proof -
  have 3: "P(c) ⟶ ¬Q(c)" using 2 by (rule allE)
  show 4: "¬Q(c)" using 3 1 by (rule mp)
qed

-- "La demostración estructurada es"
lemma ejemplo_1b: 
  assumes "P(c)"
          "∀x. (P(x) ⟶ ¬Q(x))"
  shows "¬Q(c)"
proof -
  have "P(c) ⟶ ¬Q(c)" using assms(2) ..
  thus "¬Q(c)" using assms(1) ..
qed

-- "La demostración automática es"
lemma ejemplo_1c: 
  assumes "P(c)"
          "∀x. (P(x) ⟶ ¬Q(x))"
  shows "¬Q(c)"
using assms
by auto

text {* 
  Ejemplo 2 (p. 11). Demostrar que
     ∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x)
*}

-- "La demostración detallada es"
lemma ejemplo_2a: 
  assumes 1: "∀x. (P x ⟶ ¬(Q x))" and
          2: "∀x. P x"
  shows "∀x. ¬(Q x)"
proof -
  { fix a
    have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
    have 4: "P a" using 2 by (rule allE)
    have 5: "¬(Q a)" using 3 4 by (rule mp) }
  thus "∀x. ¬(Q x)" by (rule allI)
qed

-- "La demostración detallada hacia atrás es"
lemma ejemplo_2b: 
  assumes 1: "∀x. (P x ⟶ ¬(Q x))" and
          2: "∀x. P x"
  shows "∀x. ¬(Q x)"
proof (rule allI)
  fix a
  have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)
  have 4: "P a" using 2 by (rule allE)
  show 5: "¬(Q a)" using 3 4 by (rule mp) 
qed

-- "La demostración estructurada es"
lemma ejemplo_2c: 
  assumes "∀x. (P x ⟶ ¬(Q x))"
          "∀x. P x"
  shows "∀x. ¬(Q x)"
proof 
  fix a
  have "P a" using assms(2) ..
  have "P a ⟶ ¬(Q a)" using assms(1) ..
  thus "¬(Q a)" using `P a` ..
qed

-- "La demostración automática es"
lemma ejemplo_2d: 
  assumes "∀x. (P x ⟶ ¬(Q x))"
          "∀x. P x"
  shows   "∀x. ¬(Q x)"
using assms
by auto

section {* Reglas del cuantificador existencial *}

text {*
  Las reglas del cuantificador existencial son
  · exI:     P a ⟹ ∃x. P x
  · exE:     ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

  En la regla exE la nueva variable se introduce mediante la declaración 
  "obtain ... where ... by (rule exE)" 
  *}

text {* 
  Ejemplo  (p. 12). Demostrar que
     ∀x. P x ⊢ ∃x. P x
*}

-- "La demostración detallada es"
lemma ejemplo_3a:
  assumes "∀x. P x"
  shows "∃x. P x"
proof -
  fix a
  have "P a" using assms by (rule allE)
  thus "∃x. P x" by (rule exI)
qed

-- "La demostración estructurada es"
lemma ejemplo_3b:
  assumes "∀x. P x"
  shows "∃x. P x"
proof -
  fix a
  have "P a" using assms ..
  thus "∃x. P x" ..
qed

-- "La demostración estructurada se puede simplificar"
lemma ejemplo_3c:
  assumes "∀x. P x"
  shows "∃x. P x"
proof (rule exI)
  fix a
  show "P a" using assms ..
qed

-- "La demostración estructurada se puede simplificar aún más"
lemma ejemplo_3d:
  assumes "∀x. P x"
  shows "∃x. P x"
proof 
  fix a
  show "P a" using assms ..
qed

-- "La demostración automática es"
lemma ejemplo_3e:
  assumes "∀x. P x"
  shows "∃x. P x"
using assms
by auto

text {* 
  Ejemplo 4 (p. 13). Demostrar
     ∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x
*}

-- "La demostración detallada es"
lemma ejemplo_4a:
  assumes 1: "∀x. (P x ⟶ Q x)" and
          2: "∃x. P x"
  shows "∃x. Q x"
proof -
  obtain a where 3: "P a" using 2 by (rule exE)
  have 4: "P a ⟶ Q a" using 1 by (rule allE)
  have 5: "Q a" using 4 3 by (rule mp)
  thus 6: "∃x. Q x" by (rule exI)
qed

-- "La demostración estructurada es"
lemma ejemplo_4b:
  assumes "∀x. (P x ⟶ Q x)"
          "∃x. P x"
  shows "∃x. Q x"
proof -
  obtain a where "P a" using assms(2) ..
  have "P a ⟶ Q a" using assms(1) ..
  hence "Q a" using `P a` ..
  thus "∃x. Q x" ..
qed

-- "La demostración automática es"
lemma ejemplo_4c:
  assumes "∀x. (P x ⟶ Q x)"
          "∃x. P x"
  shows "∃x. Q x"
using assms
by auto

end

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

151

152

153

154

155

156

157

158

159

160

161

162

163

164

165

166

167

168

169

170

171

172

173

174

175

176

177

178

179

180

181

182

183

184

185

186

187

188

189

190

191

192

193

194

195

196

header {* Tema 8: Deducción natural en lógica de primer orden *}

theory T8

imports Main

begin

section {* Reglas del cuantificador universal *}

text {*

Las reglas del cuantificador universal son

· allE: ⟦∀x. P x; P a ⟹ R⟧ ⟹ R

· allI: (⋀x. P x) ⟹ ∀x. P x

text {*

Ejemplo 1 (p. 10). Demostrar que

P(c), ∀x. (P(x) ⟶ ¬Q(x)) ⊢ ¬Q(c)

-- "La demostración detallada es"

lemma ejemplo_1a:

assumes 1: "P(c)" and

2: "∀x. (P(x) ⟶ ¬Q(x))"

shows "¬Q(c)"

proof -

have 3: "P(c) ⟶ ¬Q(c)" using 2 by (rule allE)

show 4: "¬Q(c)" using 3 1 by (rule mp)

qed

-- "La demostración estructurada es"

lemma ejemplo_1b:

assumes "P(c)"

"∀x. (P(x) ⟶ ¬Q(x))"

shows "¬Q(c)"

proof -

have "P(c) ⟶ ¬Q(c)" using assms(2) ..

thus "¬Q(c)" using assms(1) ..

qed

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

lemma ejemplo_1c:

assumes "P(c)"

"∀x. (P(x) ⟶ ¬Q(x))"

shows "¬Q(c)"

using assms

by auto

text {*

Ejemplo 2 (p. 11). Demostrar que

∀x. (P x ⟶ ¬(Q x)), ∀x. P x ⊢ ∀x. ¬(Q x)

-- "La demostración detallada es"

lemma ejemplo_2a:

assumes 1: "∀x. (P x ⟶ ¬(Q x))" and

2: "∀x. P x"

shows "∀x. ¬(Q x)"

proof -

{ fix a

have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)

have 4: "P a" using 2 by (rule allE)

have 5: "¬(Q a)" using 3 4 by (rule mp) }

thus "∀x. ¬(Q x)" by (rule allI)

qed

-- "La demostración detallada hacia atrás es"

lemma ejemplo_2b:

assumes 1: "∀x. (P x ⟶ ¬(Q x))" and

2: "∀x. P x"

shows "∀x. ¬(Q x)"

proof (rule allI)

fix a

have 3: "P a ⟶ ¬(Q a)" using 1 by (rule allE)

have 4: "P a" using 2 by (rule allE)

show 5: "¬(Q a)" using 3 4 by (rule mp)

qed

-- "La demostración estructurada es"

lemma ejemplo_2c:

assumes "∀x. (P x ⟶ ¬(Q x))"

"∀x. P x"

shows "∀x. ¬(Q x)"

proof

fix a

have "P a" using assms(2) ..

have "P a ⟶ ¬(Q a)" using assms(1) ..

thus "¬(Q a)" using `P a` ..

qed

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

lemma ejemplo_2d:

assumes "∀x. (P x ⟶ ¬(Q x))"

"∀x. P x"

shows "∀x. ¬(Q x)"

using assms

by auto

section {* Reglas del cuantificador existencial *}

text {*

Las reglas del cuantificador existencial son

· exI: P a ⟹ ∃x. P x

· exE: ⟦∃x. P x; ⋀x. P x ⟹ Q⟧ ⟹ Q

En la regla exE la nueva variable se introduce mediante la declaración

"obtain ... where ... by (rule exE)"

text {*

Ejemplo (p. 12). Demostrar que

∀x. P x ⊢ ∃x. P x

-- "La demostración detallada es"

lemma ejemplo_3a:

assumes "∀x. P x"

shows "∃x. P x"

proof -

fix a

have "P a" using assms by (rule allE)

thus "∃x. P x" by (rule exI)

qed

-- "La demostración estructurada es"

lemma ejemplo_3b:

assumes "∀x. P x"

shows "∃x. P x"

proof -

fix a

have "P a" using assms ..

thus "∃x. P x" ..

qed

-- "La demostración estructurada se puede simplificar"

lemma ejemplo_3c:

assumes "∀x. P x"

shows "∃x. P x"

proof (rule exI)

fix a

show "P a" using assms ..

qed

-- "La demostración estructurada se puede simplificar aún más"

lemma ejemplo_3d:

assumes "∀x. P x"

shows "∃x. P x"

proof

fix a

show "P a" using assms ..

qed

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

lemma ejemplo_3e:

assumes "∀x. P x"

shows "∃x. P x"

using assms

by auto

text {*

Ejemplo 4 (p. 13). Demostrar

∀x. (P x ⟶ Q x), ∃x. P x ⊢ ∃x. Q x

-- "La demostración detallada es"

lemma ejemplo_4a:

assumes 1: "∀x. (P x ⟶ Q x)" and

2: "∃x. P x"

shows "∃x. Q x"

proof -

obtain a where 3: "P a" using 2 by (rule exE)

have 4: "P a ⟶ Q a" using 1 by (rule allE)

have 5: "Q a" using 4 3 by (rule mp)

thus 6: "∃x. Q x" by (rule exI)

qed

-- "La demostración estructurada es"

lemma ejemplo_4b:

assumes "∀x. (P x ⟶ Q x)"

"∃x. P x"

shows "∃x. Q x"

proof -

obtain a where "P a" using assms(2) ..

have "P a ⟶ Q a" using assms(1) ..

hence "Q a" using `P a` ..

thus "∃x. Q x" ..

qed

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

lemma ejemplo_4c:

assumes "∀x. (P x ⟶ Q x)"

"∃x. P x"

shows "∃x. Q x"

using assms

by auto

end

Se puede imprimir o compartir con