enero 2020 – Calculemus

Teorema de Nicómaco

PorJosé A. Alonso 30 enero 202021 agosto 2021

Demostrar el teorema de Nicómaco que afirma que la suma de los cubos de los n primeros números naturales es igual que el cuadrado de la suma de los n primeros números naturales; es decir, para todo número natural n se tiene que

1³ + 2³ + ... + n³ = (1 + 2 + ... + n)²

1	1³ + 2³ + ... + n³ = (1 + 2 + ... + n)²

Soluciones con Isabelle/HOL

theory Teorema_de_Nicomaco
imports Main
begin

(* (suma n) es la suma de los primeros números naturales. *)
fun suma :: "nat ⇒ nat" where
  "suma 0 = 0"
| "suma (Suc n) = suma n + Suc n"

(* (sumaCubos n) es la suma de los cubos primeros números naturales. *)
fun sumaCubos :: "nat ⇒ nat" where
  "sumaCubos 0 = 0"
| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* Fórmula para la suma *)
lemma "2 * suma n = n^2 + n"
proof (induct n)
  show "2 * suma 0 = 0^2 + 0" by simp
next
  fix n
  assume "2 * suma n = n^2 + n"
  then have "2 * suma (Suc n) = n^2 + n + 2 + 2 * n"
    by simp
  also have "… = (Suc n)^2 + Suc n"
    by (simp add: power2_eq_square)
  finally show "2 * suma (Suc n) = (Suc n)^2 + Suc n"
    by this
qed

(* Demostración automática de la propiedad anterior *)
lemma formula_suma:
  "2 * suma n = n^2 + n"
  by (induct n) (auto simp add: power2_eq_square)

lemma "4 * sumaCubos n = (n^2 + n)^2"
proof (induct n)
  show "4 * sumaCubos 0 = (0^2 + 0)^2"
    by simp
next
  fix n
  assume "4 * sumaCubos n = (n^2 + n)^2"
  then have "4 * sumaCubos (Suc n) = (n^2 + n)^2 + 4 * (Suc n)^3"
    by simp
  then show "4 * sumaCubos (Suc n) = ((Suc n)^2 + Suc n)^2"
  by (simp add: algebra_simps
                power2_eq_square
                power3_eq_cube )
qed

(* Demostración automática de la propiedad anterior *)
lemma formula_sumaCubos:
  "4 * sumaCubos n = (n^2 + n)^2"
  by (induct n) (auto simp add: algebra_simps
                                power2_eq_square
                                power3_eq_cube)

(* Lema auxiliar *)
lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2"
  by (simp add: power2_eq_square)

(* Teorema de Nicómaco *)
theorem teorema_de_Nicomaco:
  "sumaCubos n = (suma n)^2"
  by (simp only: formula_suma formula_sumaCubos aux)

end

theory Teorema_de_Nicomaco

imports Main

begin

(* (suma n) es la suma de los primeros números naturales. *)

fun suma :: "nat ⇒ nat" where

"suma 0 = 0"

| "suma (Suc n) = suma n + Suc n"

(* (sumaCubos n) es la suma de los cubos primeros números naturales. *)

fun sumaCubos :: "nat ⇒ nat" where

"sumaCubos 0 = 0"

| "sumaCubos (Suc n) = sumaCubos n + (Suc n)^3"

(* Fórmula para la suma *)

lemma "2 * suma n = n^2 + n"

proof (induct n)

show "2 * suma 0 = 0^2 + 0" by simp

fix n

assume "2 * suma n = n^2 + n"

then have "2 * suma (Suc n) = n^2 + n + 2 + 2 * n"

by simp

also have "… = (Suc n)^2 + Suc n"

by (simp add: power2_eq_square)

finally show "2 * suma (Suc n) = (Suc n)^2 + Suc n"

by this

qed

(* Demostración automática de la propiedad anterior *)

lemma formula_suma:

"2 * suma n = n^2 + n"

by (induct n) (auto simp add: power2_eq_square)

lemma "4 * sumaCubos n = (n^2 + n)^2"

proof (induct n)

show "4 * sumaCubos 0 = (0^2 + 0)^2"

by simp

fix n

assume "4 * sumaCubos n = (n^2 + n)^2"

then have "4 * sumaCubos (Suc n) = (n^2 + n)^2 + 4 * (Suc n)^3"

by simp

then show "4 * sumaCubos (Suc n) = ((Suc n)^2 + Suc n)^2"

by (simp add: algebra_simps

power2_eq_square

power3_eq_cube )

qed

(* Demostración automática de la propiedad anterior *)

lemma formula_sumaCubos:

"4 * sumaCubos n = (n^2 + n)^2"

by (induct n) (auto simp add: algebra_simps

power2_eq_square

power3_eq_cube)

(* Lema auxiliar *)

lemma aux: "4 * (m::nat) = (2 * n)^2 ⟹ m = n^2"

by (simp add: power2_eq_square)

(* Teorema de Nicómaco *)

theorem teorema_de_Nicomaco:

"sumaCubos n = (suma n)^2"

by (simp only: formula_suma formula_sumaCubos aux)

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

Reto f (f (f b)) = f b

PorJosé A. Alonso 24 enero 202021 agosto 2021

El problema de hoy está basado en el reto Daily Challenge #168 que se planteó ayer. El reto consiste en demostrar que si f es una función de los booleanos en los booleanos, entonces para todo b se verifica que f (f (f b)) = f b.

Concretamente, el reto consiste en completar la siguiente demostración

lemma 
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  sorry

lemma

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

sorry

Soluciones con Isabelle/HOL

theory reto

imports Main
begin

(* 1ª solución *)

lemma "∀(f :: bool ⇒ bool). f (f (f b)) = f b"
  by smt

(* 2ª solución *)

lemma 
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  by smt

(* 3ª solución *)

lemma
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  by (cases b; cases "f True"; cases "f False"; simp)

(* 4ª solución *)

lemma
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
proof (cases "f True"; cases "f False"; cases b)
  assume "f True" "f False" "b"
  then have "f b = True" by simp
  then show "f (f (f b)) = f b" using ‹f True› by simp 
next
  assume "f True" "f False" "¬ b"
  then have "f b = True" by simp
  then show "f (f (f b)) = f b" using ‹f True› ‹f False› ‹¬ b› by simp 
next
  assume "f True" "¬ f False" "b"
  then have "f b = True" by simp
  then show "f (f (f b)) = f b" using ‹f True› ‹¬ f False› ‹b› by simp 
next
  assume "f True" "¬ f False" "¬ b"
  then have "f b = False" by simp
  then show "f (f (f b)) = f b" using ‹f True› ‹¬ f False› ‹¬ b› by simp 
next 
  assume "¬ f True" "f False" "b"
  then have "f b = False" by simp
  then show "f (f (f b)) = f b" using ‹¬ f True› ‹f False› ‹b› by simp 
next
  assume "¬ f True" "f False" "¬ b"
  then have "f b = True" by simp
  then show "f (f (f b)) = f b" using ‹¬ f True› ‹f False› ‹¬ b› by simp 
next
  assume "¬ f True" "¬ f False" "b"
  then have "f b = False" by simp
  then show "f (f (f b)) = f b" using ‹¬ f True› ‹¬ f False› ‹b› by simp 
next
  assume "¬ f True" "¬ f False" "¬ b"
  then have "f b = False" by simp
  then show "f (f (f b)) = f b" using ‹¬ f True› ‹¬ f False› ‹¬b› by simp 
qed

(* 5ª solución *)

lemma
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
proof (cases "f True"; cases "f False"; cases b)
  assume "f True" "f False" "b"
  have "f (f (f b)) = f (f (f True))" using ‹b› by simp
  also have "… = f (f True)" using ‹f True› by simp
  also have "… = f True" using ‹f True› by simp
  also have "… = f b" using ‹b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "f True" "f False" "¬ b"
  have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp
  also have "… = f (f True)" using ‹f False› by simp
  also have "… = f True" using ‹f True› by simp
  also have "… = f False" using ‹f True› ‹f False› by simp
  also have "… = f b" using ‹¬ b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "f True" "¬ f False" "b"
  have "f (f (f b)) = f (f (f True))" using ‹b› by simp
  also have "… = f (f True)" using ‹f True› by simp
  also have "… = f True" using ‹f True› by simp
  also have "… = f b" using ‹b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "f True" "¬ f False" "¬ b"
  have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp
  also have "… = f (f False)" using ‹¬ f False› by simp
  also have "… = f False" using ‹¬ f False› by simp
  also have "… = f b" using ‹¬ b› by simp
  finally show "f (f (f b)) = f b" by this 
next 
  assume "¬ f True" "f False" "b"
  have "f (f (f b)) = f (f (f True))" using ‹b› by simp
  also have "… = f (f False)" using ‹¬ f True› by simp
  also have "… = f True" using ‹f False› by simp
  also have "… = f b" using ‹b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "¬ f True" "f False" "¬ b"
  have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp
  also have "… = f (f True)" using ‹f False› by simp
  also have "… = f False" using ‹¬ f True› by simp
  also have "… = f b" using ‹¬ b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "¬ f True" "¬ f False" "b"
  have "f (f (f b)) = f (f (f True))" using ‹b› by simp
  also have "… = f (f False)" using ‹¬ f True› by simp
  also have "… = f False" using ‹¬ f False› by simp
  also have "… = False" using ‹¬ f False› by simp
  also have "… = f True" using ‹¬ f True› by simp
  also have "… = f b" using ‹b› by simp
  finally show "f (f (f b)) = f b" by this 
next
  assume "¬ f True" "¬ f False" "¬ b"
  have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp
  also have "… = f (f False)" using ‹¬ f False› by simp
  also have "… = f False" using ‹¬ f False› by simp
  also have "… = f b" using ‹¬ b› by simp
  finally show "f (f (f b)) = f b" by this 
qed

(* 6ª solución *)

theorem
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b" 
proof (cases b)
  assume b: b
  show ?thesis
  proof (cases "f True")
    assume ft: "f True"
    show ?thesis
      using b ft by auto
  next
    assume ft: "¬ f True"
    show ?thesis
    proof (cases "f False")
      assume ff: "f False"
      show ?thesis
        using b ft ff by auto
    next
      assume ff: "¬ f False"
      show ?thesis
        using b ft ff by auto
    qed
  qed
next
  assume b: "¬ b"
  show ?thesis
  proof (cases "f True")
    assume ft: "f True"
    show ?thesis
    proof (cases "f False")
      assume ff: "f False"
      show ?thesis
        using b ft ff by auto
    next
      assume ff: "¬ f False"
      show ?thesis
        using b ft ff by auto
    qed
  next
    assume ft: "¬ f True"
    show ?thesis
    proof (cases "f False")
      assume ff: "f False"
      show ?thesis
        using b ft ff by auto
    next
      assume ff: "¬ f False"
      show ?thesis
        using b ft ff by auto
    qed
  qed
qed

(* 7ª solución *)

theorem
  fixes f :: "bool ⇒ bool"
  shows "f (f (f b)) = f b"
  by (cases b "f True" "f False"
      rule: bool.exhaust [ case_product bool.exhaust
                         , case_product bool.exhaust])
    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

theory reto

imports Main

begin

(* 1ª solución *)

lemma "∀(f :: bool ⇒ bool). f (f (f b)) = f b"

by smt

(* 2ª solución *)

lemma

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

by smt

(* 3ª solución *)

lemma

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

by (cases b; cases "f True"; cases "f False"; simp)

(* 4ª solución *)

lemma

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

proof (cases "f True"; cases "f False"; cases b)

assume "f True" "f False" "b"

then have "f b = True" by simp

then show "f (f (f b)) = f b" using ‹f True› by simp

assume "f True" "f False" "¬ b"

then have "f b = True" by simp

then show "f (f (f b)) = f b" using ‹f True› ‹f False› ‹¬ b› by simp

assume "f True" "¬ f False" "b"

then have "f b = True" by simp

then show "f (f (f b)) = f b" using ‹f True› ‹¬ f False› ‹b› by simp

assume "f True" "¬ f False" "¬ b"

then have "f b = False" by simp

then show "f (f (f b)) = f b" using ‹f True› ‹¬ f False› ‹¬ b› by simp

assume "¬ f True" "f False" "b"

then have "f b = False" by simp

then show "f (f (f b)) = f b" using ‹¬ f True› ‹f False› ‹b› by simp

assume "¬ f True" "f False" "¬ b"

then have "f b = True" by simp

then show "f (f (f b)) = f b" using ‹¬ f True› ‹f False› ‹¬ b› by simp

assume "¬ f True" "¬ f False" "b"

then have "f b = False" by simp

then show "f (f (f b)) = f b" using ‹¬ f True› ‹¬ f False› ‹b› by simp

assume "¬ f True" "¬ f False" "¬ b"

then have "f b = False" by simp

then show "f (f (f b)) = f b" using ‹¬ f True› ‹¬ f False› ‹¬b› by simp

qed

(* 5ª solución *)

lemma

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

proof (cases "f True"; cases "f False"; cases b)

assume "f True" "f False" "b"

have "f (f (f b)) = f (f (f True))" using ‹b› by simp

also have "… = f (f True)" using ‹f True› by simp

also have "… = f True" using ‹f True› by simp

also have "… = f b" using ‹b› by simp

finally show "f (f (f b)) = f b" by this

assume "f True" "f False" "¬ b"

have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp

also have "… = f (f True)" using ‹f False› by simp

also have "… = f True" using ‹f True› by simp

also have "… = f False" using ‹f True› ‹f False› by simp

also have "… = f b" using ‹¬ b› by simp

finally show "f (f (f b)) = f b" by this

assume "f True" "¬ f False" "b"

have "f (f (f b)) = f (f (f True))" using ‹b› by simp

also have "… = f (f True)" using ‹f True› by simp

also have "… = f True" using ‹f True› by simp

also have "… = f b" using ‹b› by simp

finally show "f (f (f b)) = f b" by this

assume "f True" "¬ f False" "¬ b"

have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp

also have "… = f (f False)" using ‹¬ f False› by simp

also have "… = f False" using ‹¬ f False› by simp

also have "… = f b" using ‹¬ b› by simp

finally show "f (f (f b)) = f b" by this

assume "¬ f True" "f False" "b"

have "f (f (f b)) = f (f (f True))" using ‹b› by simp

also have "… = f (f False)" using ‹¬ f True› by simp

also have "… = f True" using ‹f False› by simp

also have "… = f b" using ‹b› by simp

finally show "f (f (f b)) = f b" by this

assume "¬ f True" "f False" "¬ b"

have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp

also have "… = f (f True)" using ‹f False› by simp

also have "… = f False" using ‹¬ f True› by simp

also have "… = f b" using ‹¬ b› by simp

finally show "f (f (f b)) = f b" by this

assume "¬ f True" "¬ f False" "b"

have "f (f (f b)) = f (f (f True))" using ‹b› by simp

also have "… = f (f False)" using ‹¬ f True› by simp

also have "… = f False" using ‹¬ f False› by simp

also have "… = False" using ‹¬ f False› by simp

also have "… = f True" using ‹¬ f True› by simp

also have "… = f b" using ‹b› by simp

finally show "f (f (f b)) = f b" by this

assume "¬ f True" "¬ f False" "¬ b"

have "f (f (f b)) = f (f (f False))" using ‹¬b› by simp

also have "… = f (f False)" using ‹¬ f False› by simp

also have "… = f False" using ‹¬ f False› by simp

also have "… = f b" using ‹¬ b› by simp

finally show "f (f (f b)) = f b" by this

qed

(* 6ª solución *)

theorem

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

proof (cases b)

assume b: b

show ?thesis

proof (cases "f True")

assume ft: "f True"

show ?thesis

using b ft by auto

assume ft: "¬ f True"

show ?thesis

proof (cases "f False")

assume ff: "f False"

show ?thesis

using b ft ff by auto

assume ff: "¬ f False"

show ?thesis

using b ft ff by auto

qed

assume b: "¬ b"

show ?thesis

proof (cases "f True")

assume ft: "f True"

show ?thesis

proof (cases "f False")

assume ff: "f False"

show ?thesis

using b ft ff by auto

assume ff: "¬ f False"

show ?thesis

using b ft ff by auto

qed

assume ft: "¬ f True"

show ?thesis

proof (cases "f False")

assume ff: "f False"

show ?thesis

using b ft ff by auto

assume ff: "¬ f False"

show ?thesis

using b ft ff by auto

qed

(* 7ª solución *)

theorem

fixes f :: "bool ⇒ bool"

shows "f (f (f b)) = f b"

by (cases b "f True" "f False"

rule: bool.exhaust [ case_product bool.exhaust

, case_product bool.exhaust])

auto

end

Otras soluciones

Se pueden escribir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang="isar"> y otra con </pre>

Celebración del día mundial de la lógica

PorJosé A. Alonso 14 enero 202021 agosto 2021

Decidir si es cierto que

Existe una Universidad tal que si en dicha Universidad se celebra el Día Mundial de la Lógica (DML), entonces en todas las Universidades se celebra el DML.

En la formalización usar C(x) para representar que en la Universidad x se celebra el DML.

Soluciones

theory Celebracion_del_DML
imports Main

begin

(* 1ª solución (automática) *)
lemma "∃x. (C x ⟶ (∀y. C y))"
  by simp

(* 2ª solución (estructurada) *)
lemma "∃x. (C x ⟶ (∀y. C y))"
proof -
  have "¬ (∀y. C y) ∨ (∀y. C y)" ..
  then show "∃x. (C x ⟶ (∀y. C y))"
  proof 
    assume "¬ (∀y. C y)"
    then have "∃y. ¬(C y)" by simp
    then obtain a where "¬ C a" ..
    then have "C a ⟶ (∀y. C y)" by simp
    then show "∃x. (C x ⟶ (∀y. C y))" ..
  next
    assume "∀y. C y"
    then show "∃x. (C x ⟶ (∀y. C y))" by simp
  qed
qed

(* 3ª solución (detallada con lemas auxiliares) *)

lemma aux1:
  assumes "¬ (∀y. C y)"
  shows "∃y. ¬(C y)"
proof (rule ccontr)
  assume "∄y. ¬ C y"
  have "∀y. C y"
  proof 
    fix a
    show "C a"
    proof (rule ccontr)
      assume "¬ C a"
      then have "∃y. ¬ C y" by (rule exI)
      with ‹∄y. ¬ C y› show False by (rule notE)
    qed 
  qed
  with assms show False by (rule notE)
qed

lemma aux2:
  assumes "¬P"
  shows   "P ⟶ Q"
proof
  assume "P"
  with assms show "Q" by (rule notE)
qed

lemma aux3:
  assumes "∄x. P x"
  shows   "∀x. ¬ P x"
proof
  fix a
  show "¬ P a"
  proof 
    assume "P a"
    then have "∃x. P x" by (rule exI)
    with assms show False by (rule notE)
  qed 
qed

lemma aux4:
  assumes "Q"
  shows   "∃x. (P x ⟶ Q)"
proof (rule ccontr)
  assume "∄x. (P x ⟶ Q)"
  then have "∀x. ¬ (P x ⟶ Q)" by (rule aux3)
  then have "¬ (P a ⟶ Q)" by (rule allE)
  moreover
  have "P a ⟶ Q"
  proof
    assume "P a"
    show "Q" using assms by this
  qed
  ultimately show False by (rule notE)
qed

lemma "∃x. (C x ⟶ (∀y. C y))"
proof -
  have "¬ (∀y. C y) ∨ (∀y. C y)" ..
  then show "∃x. (C x ⟶ (∀y. C y))"
  proof 
    assume "¬ (∀y. C y)"
    then have "∃y. ¬(C y)" by (rule aux1)
    then obtain a where "¬ C a" by (rule exE)
    then have "C a ⟶ (∀y. C y)" by (rule aux2)
    then show "∃x. (C x ⟶ (∀y. C y))" by (rule exI)
  next
    assume "∀y. C y"
    then show "∃x. (C x ⟶ (∀y. C y))" by (rule aux4)
  qed
qed

end

100

theory Celebracion_del_DML

imports Main

begin

(* 1ª solución (automática) *)

lemma "∃x. (C x ⟶ (∀y. C y))"

by simp

(* 2ª solución (estructurada) *)

lemma "∃x. (C x ⟶ (∀y. C y))"

proof -

have "¬ (∀y. C y) ∨ (∀y. C y)" ..

then show "∃x. (C x ⟶ (∀y. C y))"

proof

assume "¬ (∀y. C y)"

then have "∃y. ¬(C y)" by simp

then obtain a where "¬ C a" ..

then have "C a ⟶ (∀y. C y)" by simp

then show "∃x. (C x ⟶ (∀y. C y))" ..

assume "∀y. C y"

then show "∃x. (C x ⟶ (∀y. C y))" by simp

qed

(* 3ª solución (detallada con lemas auxiliares) *)

lemma aux1:

assumes "¬ (∀y. C y)"

shows "∃y. ¬(C y)"

proof (rule ccontr)

assume "∄y. ¬ C y"

have "∀y. C y"

proof

fix a

show "C a"

proof (rule ccontr)

assume "¬ C a"

then have "∃y. ¬ C y" by (rule exI)

with ‹∄y. ¬ C y› show False by (rule notE)

qed

with assms show False by (rule notE)

qed

lemma aux2:

assumes "¬P"

shows "P ⟶ Q"

proof

assume "P"

with assms show "Q" by (rule notE)

qed

lemma aux3:

assumes "∄x. P x"

shows "∀x. ¬ P x"

proof

fix a

show "¬ P a"

proof

assume "P a"

then have "∃x. P x" by (rule exI)

with assms show False by (rule notE)

qed

lemma aux4:

assumes "Q"

shows "∃x. (P x ⟶ Q)"

proof (rule ccontr)

assume "∄x. (P x ⟶ Q)"

then have "∀x. ¬ (P x ⟶ Q)" by (rule aux3)

then have "¬ (P a ⟶ Q)" by (rule allE)

moreover

have "P a ⟶ Q"

proof

assume "P a"

show "Q" using assms by this

qed

ultimately show False by (rule notE)

qed

lemma "∃x. (C x ⟶ (∀y. C y))"

proof -

have "¬ (∀y. C y) ∨ (∀y. C y)" ..

then show "∃x. (C x ⟶ (∀y. C y))"

proof

assume "¬ (∀y. C y)"

then have "∃y. ¬(C y)" by (rule aux1)

then obtain a where "¬ C a" by (rule exE)

then have "C a ⟶ (∀y. C y)" by (rule aux2)

then show "∃x. (C x ⟶ (∀y. C y))" by (rule exI)

assume "∀y. C y"

then show "∃x. (C x ⟶ (∀y. C y))" by (rule aux4)

qed

end

Nota

Se pueden añadir otras soluciones en los comentarios.
El código se debe escribir entre una línea con <pre lang=»isar»> y otra con </pre>

Pensamiento

Si así fue, así pudo ser; si así fuera, así podría ser; pero como no es, no es. Eso es lógica.

Lewis Carroll

Día mundial de la lógica y Calculemus

PorJosé A. Alonso 14 enero 202021 agosto 2021

El Consejo Ejecutivo de la UNESCO ha proclamado el 14 de enero Día Mundial de la Lógica.

La fecha del 14 de enero se ha eligido para rendir homenaje a dos grandes lógicos del siglo XX: Kurt Gödel (que falleció el 14 de enero de 1978) y Alfred Tarski (que nació el 14 de enero de 1901).

Uniéndose a dicha celebración, hoy (14 de enero de 2020) comienza la andadura de este blog cuyo principal objetivo es servir de complemento a las asignaturas de

Lógica matemática y fundamentos (de 3º del Grado en Matemáticas) y
Razonamiento automático del Máster el Lógica, Computación e Inteligencia Artificial.

El plan es proponer cada semana un ejercicio de forma que los alumnos pueden escribir las soluciones en los comentarios utilizando Isabelle/HOL en la demostración.

El código se escribe entre una línea con <pre lang="isar"> y otra con </pre>