사람마다 다르겠지만, 초심자가 논리를 접하면서 처음 매료되는 부분이 있다면 아마 그 형식적 엄밀함이 아닐까 생각한다. 단 몇 가지 공리와 추론 규칙으로 완결되는 간결함, 모든 단계의 타당성이 기계적으로 결정되는 정확성, 전제가 결론을 절대적으로 보장하는 신뢰성 같은 것. 그런데 이런 부분에 매력을 느끼고 교재를 구해서 논리학, 즉 연역 체계 자체를 탐구하는 메타논리를 공부하기 시작하면, 여타 수학 분과와 다름없이 자연어와 직관에 의존하는 비형식적 증명에 다소 실망하게 되지. 형식적 증명을 다루는 학문이 어째서 형식적 증명을 사용하지 않는 걸까?


그 이유는 뭐, 논리 체계의 불완전성을 포함해서 여러가지가 있겠지만... 가장 큰 이유는 형식적 증명이 끔찍한 양의 노동을 요구한다는 것이겠지. 그 대표적 사례가 수학의 집합론 기반 형식화를 시도했던 부르바키 학파의 좌절 같은 것일 테고. 그런데 이런 이야기는 지식사를 읽다 보면 흔히 접하게 되지만, 그 작업의 예시를 보여주는 경우는 별로 없다. 형식적 증명의 분량은 구체적으로 어느 정도인 걸까? 한 번은 궁금해져서 간단한 실험을 해 봤다. 논리학 개론에서 흔히 사용하는 Fitch식 자연연역으로 기초적인 정리, 예를 들어 자연수 덧셈의 교환 법칙을 증명해 본다면 어떻게 될까?


  1 //Law of Identity

  2 ∀ n ( n = n )

  3 //Definition, Natural Numbers

  4 ∀ n ( n ∈ N <=> ( n = O \\/ ∃ m ( m ∈ N /\\ n = S m ) ) )

  5 //Definition(1), Addition of Natural Numbers

  6 ∀ n ( n ∈ N ==> O + n = n )

  7 //Definition(2), Addition of Natural Numbers

  8 ∀ n ( n ∈ N ==> ∀ m ( m ∈ N ==> S n + m = S ( n + m ) ) )

  9 //Axiom of Induction

 10 ∀ P ( ( P O /\\ ∀ n ( n ∈ N ==> ( P n ==> P ( S n ) ) ) ) ==> ∀ n ( n ∈ N ==> P n ) )

 11 //Definition, Qn

 12 ∀ n ( n ∈ N ==> ( Q n <=> ∀ m ( m ∈ N ==> n + m = m + n ) ) )

 13 //Definition, Rn

 14 ∀ n ( n ∈ N ==> ( R n <=> n + O = n ) )

 15 //Definition, Tn

 16 ∀ n ( n ∈ N ==> ( T n <=> ∀ m ( m ∈ N ==> n + S m = S ( n + m ) ) ) )

 17 //Universal Instantiation, 2

 18 O = O

 19 //Disjunction Introduction, 18

 20 O = O \\/ ∃ m ( m ∈ N ==> ( O = S m ) )

 21 //Universal Instantiation, 4

 22 O ∈ N <=> ( O = O \\/ ∃ m ( m ∈ N ==> ( O = S m ) ) )

 23 //Biconditional Elimination, 22

 24 O ∈ N <== ( O = O \\/ ∃ m ( m ∈ N ==> ( O = S m ) ) )

 25 //Modus Ponens, 24, 2O

 26 O ∈ N

 27 //Universal Instantiation, 14

 28 O ∈ N ==> ( R O <=> O + O = O )

 29 //Modus Ponens, 28, 26

 30 R O <=> O + O = O

 31 //Biconditional Elimination, 3O

 32 R O <== O + O = O

 33 //Universal Instantiation, 6

 34 O ∈ N ==> O + O = O

 35 //Modus Ponens, 34, 26

 36 O + O = O

 37 //Modus Ponens, 32, 36

 38 R O

 39 | //Hypothesis

 40 | x ∈ N

 41 |---------------

 42 | //Universal Instantiation, 2

 43 | S x = S x

 44 | //Conjunction Introduction, 4O, 43

 45 | x ∈ N /\\ S x = S x

 46 | //Existential Generalization, 45

 47 | ∃ m ( m ∈ N /\\ S x = S m )

 48 | //Disjunction Introduction, 47

 49 | S x = O \\/ ∃ m ( m ∈ N /\\ S x = S m )

 50 | //Universal Instantiation, 4

 51 | S x ∈ N <=> ( S x = O \\/ ∃ m ( m ∈ N /\\ S x = S m ) )

 52 | //Biconditional Elimination, 51

 53 | S x ∈ N <== ( S x = O \\/ ∃ m ( m ∈ N /\\ S x = S m ) )

 54 | //Modus Ponens, 53, 49

 55 | S x ∈ N

 56 //Conditional Introduction, 4O-55

 57 x ∈ N ==> S x ∈ N

 58 //Universal Generalization, 57

 59 ∀ n ( n ∈ N ==> S n ∈ N )

 60 | //Hypothesis

 61 | x ∈ N

 62 |---------------

 63 || //Hypothesis

 64 || R x

 65 ||---------------

 66 || //Universal Instantiation, 14

 67 || x ∈ N ==> ( R x <=> x + O = x )

 68 || //Modus Ponens, 67, 61

 69 || R x <=> x + O = x

 70 || //Biconditional Elimination, 69

 71 || R x ==> x + O = x

 72 || //Modus Ponens, 71, 64

 73 || x + O = x

 74 || //Universal Instantiation, 2

 75 || S x = S x

 76 || //Substitution, 75, 73

 77 || S ( x + O ) = S x

 78 || //Universal Instantiaion, 8

 79 || x ∈ N ==> ∀ m ( m ∈ N ==> S x + m = S ( x + m ) )

 80 || //Modus Ponens, 79, 61

 81 || ∀ m ( m ∈ N ==> S x + m = S ( x + m ) )

 82 || //Universal Instantiation, 81

 83 || O ∈ N ==> S x + O = S ( x + O )

 84 || //Modus Ponens, 83, 26

 85 || S x + O = S ( x + O )

 86 || //Substitution, 85, 77

 87 || S x + O = S x

 88 || //Universal Instantiation, 59

 89 || x ∈ N ==> S x ∈ N

 90 || //Modus Ponens, 89, 61

 91 || S x ∈ N

 92 || //Universal Instantiation, 14

 93 || S x ∈ N ==> ( R ( S x ) <=> S x + O = S x )

 94 || //Modus Ponens, 93, 91

 95 || R ( S x ) <=> S x + O = S x

 96 || //Biconditional Elimination, 95

 97 || R ( S x ) <== S x + O = S x

 98 || //Modus Ponens, 97, 87

 99 || R ( S x )

100 | //Conditional Introduction, 64-99

101 | R x ==> R ( S x )

102 //Conditional Introduction, 61-1O1

103 x ∈ N ==> ( R x ==> R ( S x ) )

104 //Universal Generalization, 1O3

105 ∀ n ( n ∈ N ==> ( R n ==> R ( S n ) ) )

106 //Conjunction Introduction, 38, 1O5

107 R O /\\ ∀ n ( n ∈ N ==> ( R n ==> R ( S n ) ) )

108 //Universal Instantiation, 1O

109 ( R O /\\ ∀ n ( n ∈ N ==> ( R n ==> R ( S n ) ) ) ) ==> ∀ n ( n ∈ N ==> R n )

110 //Modus Ponens, 1O9, 1O7

111 ∀ n ( n ∈ N ==> R n )

112 | //Hypothesis

113 | x ∈ N

114 |---------------

115 | //Universal Instantiation, 111

116 | x ∈ N ==> R x

117 | //Modus Ponens, 116, 113

118 | R x

119 | //Universal Instantiation, 14

120 | x ∈ N ==> ( R x <=> x + O = x )

121 | //Modus Ponens, 12O, 113

122 | R x <=> x + O = x

123 | //Biconditional Elimination, 122

124 | R x ==> x + O = x

125 | //Modus Ponens, 124, 118

126 | x + O = x

127 //Conditional Introduction, 113-126

128 x ∈ N ==> x + O = x

129 //Universal Generalization, 128

130 ∀ n ( n ∈ N ==> n + O = n )

131 | //Hypothesis

132 | y ∈ N

133 |---------------

134 | //Universal Instantiation, 6

135 | y ∈ N ==> O + y = y

136 | //Modus Ponens, 135, 132

137 | O + y = y

138 | //Universal Instantiation, 13O

139 | y ∈ N ==> y + O = y

140 | //Modus Ponens, 139, 132

141 | y + O = y

142 | //Substitution, 137, 141

143 | O + y = y + O

144 //Conditional Introduction, 132-143

145 y ∈ N ==> O + y = y + O

146 //Universal Generalization, 145

147 ∀ m ( m ∈ N ==> O + m = m + O )

148 //Universal Instantiation, 12

149 O ∈ N ==> ( Q O <=> ∀ m ( m ∈ N ==> O + m = m + O ) )

150 //Modus Ponens, 149, 26

151 Q O <=> ∀ m ( m ∈ N ==> O + m = m + O )

152 //Biconditional Elimination, 151

153 Q O <== ∀ m ( m ∈ N ==> O + m = m + O )

154 //Modus Ponens, 153, 147

155 Q O

156 | //Hypothesis

157 | y ∈ N

158 |---------------

159 | //Universal Instantiation, 59

160 | y ∈ N ==> S y ∈ N

161 | //Modus Ponens, 160, 157

162 | S y ∈ N

163 | //Universal Instantiation, 6

164 | S y ∈ N ==> O + S y = S y

165 | //Modus Ponens, 164, 162

166 | O + S y = S y

167 | //Universal Instantiation, 6

168 | y ∈ N ==> O + y = y

169 | //Modus Ponens, 168, 157

170 | O + y = y

171 | //Substitution, 166, 170

172 | O + S y = S ( O + y )

173 //Conditional Introduction, 157-172

174 y ∈ N ==> O + S y = S ( O + y )

175 //Universal Generalization, 174

176 ∀ m ( m ∈ N ==> O + S m = S ( O + m ) )

177 //Universal Instantiation, 16

178 O ∈ N ==> ( T O <=> ∀ m ( m ∈ N ==> O + S m = S ( O + m ) ) )

179 //Modus Ponens, 178, 26

180 T O <=> ∀ m ( m ∈ N ==> O + S m = S ( O + m ) )

181 //Biconditional Elimination, 180

182 T O <== ∀ m ( m ∈ N ==> O + S m = S ( O + m ) )

183 //Modus Ponens, 182, 176

184 T O

185 | //Hypothesis

186 | x ∈ N

187 |---------------

188 || //Hypothesis

189 || T x

190 ||---------------

191 || //Universal Instantiation, 16

192 || x ∈ N ==> ( T x <=> ∀ m ( m ∈ N ==> x + S m = S ( x + m ) ) )

193 || //Modus Ponens, 192, 186

194 || T x <=> ∀ m ( m ∈ N ==> x + S m = S ( x + m ) )

195 || //Biconditional Elimination, 194

196 || T x ==> ∀ m ( m ∈ N ==> x + S m = S ( x + m ) )

197 || //Modus Ponens, 196, 189

198 || ∀ m ( m ∈ N ==> x + S m = S ( x + m ) )

199 ||| //Hypothesis

200 ||| y ∈ N

201 |||---------------

202 ||| //Universal Instantiation, 198

203 ||| y ∈ N ==> x + S y = S ( x + y )

204 ||| //Modus Ponens, 203, 200

205 ||| x + S y = S ( x + y )

206 ||| //Universal Instantiation, 59

207 ||| y ∈ N ==> S y ∈ N

208 ||| //Modus Ponens, 207, 200

209 ||| S y ∈ N

210 ||| //Universal Instantiation, 8

211 ||| x ∈ N ==> ∀ m ( m ∈ N ==> S x + m = S ( x + m ) )

212 ||| //Modus Ponens, 211, 186

213 ||| ∀ m ( m ∈ N ==> S x + m = S ( x + m ) )

214 ||| //Universal Instantiation, 213

215 ||| y ∈ N ==> S x + y = S ( x + y )

216 ||| //Modus Ponens, 215, 200

217 ||| S x + y = S ( x + y )

218 ||| //Universal Instantiation, 8

219 ||| x ∈ N ==> ∀ m ( m ∈ N ==> S x + m = S ( x + m ) )

220 ||| //Modus Ponens, 219, 186

221 ||| ∀ m ( m ∈ N ==> S x + m = S ( x + m ) )

222 ||| //Universal Instantiation, 221

223 ||| S y ∈ N ==> S x + S y = S ( x + S y )

224 ||| //Modus Ponens, 223, 209

225 ||| S x + S y = S ( x + S y )

226 ||| //Substitution, 225, 205

227 ||| S x + S y = S ( S ( x + y ) )

228 ||| //Substitution, 227, 217

229 ||| S x + S y = S ( S x + y )

230 || //Conditional Introduction, 200-229

231 || y ∈ N ==> S x + S y = S ( S x + y )

232 || //Universal Instantiation, 231

233 || ∀ m ( m ∈ N ==> S x + S m = S ( S x + m ) )

234 || //Universal Instantiation, 59

235 || x ∈ N ==> S x ∈ N

236 || //Modus Ponens, 235, 186

237 || S x ∈ N

238 || //Universal Instantiation, 16

239 || S x ∈ N ==> ( T ( S x ) <=> ∀ m ( m ∈ N ==> S x + S m = S ( S x + m ) ) )

240 || //Modus Ponens, 239, 237

241 || T ( S x ) <=> ∀ m ( m ∈ N ==> S x + S m = S ( S x + m ) )

242 || //Biconditional Elimination,

243 || T ( S x ) <== ∀ m ( m ∈ N ==> S x + S m = S ( S x + m ) )

244 || //Modus Ponens, 243, 233

245 || T ( S x )

246 | //Conditional Introduction, 189-245

247 | T x ==> T ( S x )

248 //Conditional Introduction, 186-247

249 x ∈ N ==>( T x ==> T ( S x ) )

250 //Universal Generalization, 249

251 ∀ n ( n ∈ N ==> ( T n ==> T ( S n ) ) )

252 //Conjunction Introduction, 184, 251

253 T O /\\ ∀ n ( n ∈ N ==> ( T n ==> T ( S n ) ) )

254 //Universal Instantiation, 10

255 ( T O /\\ ∀ n ( n ∈ N ==> ( T n ==> T ( S n ) ) ) ) ==> ∀ n ( n ∈ N ==> T n )

256 //Modus Ponens, 255, 253

257 ∀ n ( n ∈ N ==> T n )

258 | //Hypothesis

259 | x ∈ N

260 |---------------

261 | //Universal Instantiation, 16

262 | x ∈ N ==> ( T x <=> ∀ m ( m ∈ N ==> x + S m = S ( x + m ) ) )

263 | //Modus Ponens, 262, 259

264 | T x <=> ∀ m ( m ∈ N ==> x + S m = S ( x + m ) )

265 | //Biconditional Elimination, 264

266 | T x ==> ∀ m ( m ∈ N ==> x + S m = S ( x + m ) )

267 | //Universal Instantiation, 257

268 | x ∈ N ==> T x

269 | //Modus Ponens, 268, 259

270 | T x

271 | //Modus Ponens, 266, 270

272 | ∀ m ( m ∈ N ==> x + S m = S ( x + m ) )

273 //Conditional Introduction, 259, 272

274 x ∈ N ==> ∀ m ( m ∈ N ==> x + S m = S ( x + m ) )

275 //Universal Generalization, 274

276 ∀ n ( n ∈ N ==> ∀ m ( m ∈ N ==> n + S m = S ( n + m ) ) )

277 | //Hypothesis

278 | x ∈ N

279 |---------------

280 || //Hypothesis

281 || Q x

282 ||---------------

283 || //Universal Instantiation, 12

284 || x ∈ N ==> ( Q x <=> ∀ m ( m ∈ N ==> x + m = m + x ) )

285 || //Modus Ponens, 284, 278

286 || Q x <=> ∀ m ( m ∈ N ==> x + m = m + x )

287 || //Biconditional Elimination, 286

288 || Q x ==> ∀ m ( m ∈ N ==> x + m = m + x )

289 || //Modus Ponens, 288, 281

290 || ∀ m ( m ∈ N ==> x + m = m + x )

291 ||| //Hypothesis

292 ||| y ∈ N

293 |||---------------

294 ||| //Universal Instantiation, 8

295 ||| y ∈ N ==> ∀ m ( m ∈ N ==> S y + m = S ( y + m ) )

296 ||| //Modus Ponens, 295, 292

297 ||| ∀ m ( m ∈ N ==> S y + m = S ( y + m ) )

298 ||| //Universal Instantiation, 297

299 ||| x ∈ N ==> S y + x = S ( y + x )

300 ||| //Modus Ponens, 299, 278

301 ||| S y + x = S ( y + x )

302 ||| //Universal Instantiation, 276

303 ||| y ∈ N ==> ∀ m ( m ∈ N ==> y + S m = S ( y + m ) )

304 ||| //Modus Ponens, 303, 292

305 ||| ∀ m ( m ∈ N ==> y + S m = S ( y + m ) )

306 ||| //Universal Instantiation, 305

307 ||| x ∈ N ==> y + S x = S ( y + x )

308 ||| //Modus Ponens, 307, 278

309 ||| y + S x = S ( y + x )

310 ||| //Universal Instantiation, 2

311 ||| S ( x + y ) = S ( x + y )

312 ||| //Universal Instantiation, 290

313 ||| y ∈ N ==> x + y = y + x

314 ||| //Modus Ponens, 313, 292

315 ||| x + y = y + x

316 ||| //Substitution, 311, 315

317 ||| S ( x + y ) = S ( y + x )

318 ||| //Universal Instantiation, 8

319 ||| x ∈ N ==> ∀ m ( m ∈ N ==> S x + m = S ( x + m ) )

320 ||| //Modus Ponens, 318, 278

321 ||| ∀ m ( m ∈ N ==> S x + m = S ( x + m ) )

322 ||| //Universal Instantiation, 321

323 ||| y ∈ N ==> S x + y = S ( x + y )

324 ||| //Modus Ponens, 323, 292

325 ||| S x + y = S ( x + y )

326 ||| //Substitution, 317, 325

327 ||| S x + y = S ( y + x )

328 ||| //Substitution, 327, 309

329 ||| S x + y = y + S x

330 || //Conditional Introduction, 292-329

331 || y ∈ N ==> S x + y = y + S x

332 || //Universal Generalization, 331

333 || ∀ m ( m ∈ N ==> S x + m = m + S x )

334 || //Universal Instantiation, 59

335 || x ∈ N ==> S x ∈ N

336 || //Modus Ponens, 335, 278

337 || S x ∈ N

338 || //Universal Instantiation, 12

339 || S x ∈ N ==> ( Q ( S x ) <=> ∀ m ( m ∈ N ==> S x + m = m + S x ) )

340 || //Modus Ponens, 339, 337

341 || Q ( S x ) <=> ∀ m ( m ∈ N ==> S x + m = m + S x )

342 || //Biconditional Elimination, 341

343 || Q ( S x ) <== ∀ m ( m ∈ N ==> S x + m = m + S x )

344 || //Modus Ponens, 343, 333

345 || Q ( S x )

346 | //Conditional Introduction, 281, 345

347 | Q x ==> Q ( S x )

348 //Conditional Introduction, 278, 347

349 x ∈ N ==> ( Q x ==> Q ( S x ) )

350 //Universal Generalization, 349

351 ∀ n ( n ∈ N ==> ( Q n ==> Q ( S n ) ) )

352 //Conjunction Introduction, 155, 351

353 Q O /\\ ∀ n ( n ∈ N ==> ( Q n ==> Q ( S n ) ) )

354 //Universal Instantiation, 10

355 ( Q O /\\ ∀ n ( n ∈ N ==> ( Q n ==> Q ( S n ) ) ) ) ==> ∀ n ( n ∈ N ==> Q n )

356 //Modus Ponens, 355, 353

357 ∀ n ( n ∈ N ==> Q n )

358 | //Hypothesis

359 | x ∈ N

360 |---------------

361 | //Universal Instantiation, 12

362 | x ∈ N ==> ( Q x <=> ∀ m ( m ∈ N ==> x + m = m + x ) )

363 | //Modus Ponens, 362, 359

364 | Q x <=> ∀ m ( m ∈ N ==> x + m = m + x )

365 | //Biconditional Elimination, 364

366 | Q x ==> ∀ m ( m ∈ N ==> x + m = m + x )

367 | //Universal Instantiation, 357

368 | x ∈ N ==> Q x

369 | //Modus Ponens, 368, 359

370 | Q x

371 | //Modus Ponens, 366, 370

372 | ∀ m ( m ∈ N ==> x + m = m + x )

373 //Conditional Introduction, 359-372

374 x ∈ N ==> ∀ m ( m ∈ N ==> x + m = m + x )

375 //Universal Generalization, 374

376 ∀ n ( n ∈ N ==> ∀ m ( m ∈ N ==> n + m = m + n ) )


대충 이렇게 된다. 물론 이것이 최적의 증명은 아니겠지만 아무리 최적화를 하더라도 사람이 할 일이 아닌 건 확실하지. 아직까지 절대 다수의 증명이 비형식적인 것도 자연스러운 일일 테고.


그렇다면 완전한 형식화는 어디까지나 이론적으로만 가능한 이상으로 남겨둘 수 밖에 없는 걸까? 꼭 그렇지는 않다. 과거와 달리 이제는 증명의 상당 부분을 자동화할 수 있다는 결정적 차이점이 있기 때문이지. 이런 용도로 쓰이는 소프트웨어를 일반적으로 증명 보조기 (proof assistant) 라고 하는데, 대표적 증명 보조기인 Coq를 사용한 교환법칙의 증명은 다음과 같다.


  1 Inductive nat : Type :=

  2   | O : nat

  3   | S : nat -> nat.

  4

  5 Fixpoint add (n m : nat) : nat :=

  6   match n with

  7   | O => m

  8   | S n' => S ( add n' m )

  9   end.

 10

 11 Theorem add_0_r : forall n : nat, add n O = n.

 12   intros n. induction n as [| n'].

 13   reflexivity. simpl. rewrite -> IHn'.

 14   reflexivity. Qed.

 15

 16 Theorem increment_r : forall n m : nat, add n ( S m ) = S ( add n m ).

 17   intros n m. induction n as [| n'].

 18   reflexivity. simpl. rewrite -> IHn'.

 19   reflexivity. Qed.

 20

 21 Theorem add_comm : forall n m : nat, add n m = add m n.

 22   intros n m. induction n as [| n'].

 23   rewrite -> add_0_r. reflexivity.

 24   simpl. rewrite -> increment_r.

 25   rewrite -> IHn'. reflexivity. Qed.


여전히 컴팩트하다고 말하긴 어렵지만, 이 정도면 충분히 도전해 볼 만한 수준 아닐까? 실제로 60년대의 Automath 프로젝트를 시작으로 증명 보조기를 이용해서 수학을 형식화하는 노력은 꾸준히 이어져 왔고, 근래에는 점점 복잡해지는 증명의 정확성을 인간이 검증하기 어려워짐에 따라 이 분야에 대한 관심도 늘어나고 있지. 최근의 동향에 대해서는 Nautilus 에서 좋은 기사(http://nautil.us/issue/24/error/in-mathematics-mistakes-arent-what-they-used-to-be?utm_source=ticker&utm_medium=article&utm_campaign=in-mathematics-mistakes-arent-what-they-used-to-be)를 써서 정리해 놓았는데, 흥미가 있는 사람은 읽어 봐도 괜찮을 것 같다.