컴퓨터공학 300 주제 시리즈의 003번째 글이다. 전체 지도는 여기.

한 줄 요약

증명은 이미 참으로 인정된 사실에서 출발해 논리 규칙만으로 결론에 도달하는 글이다. 가장 많이 쓰는 세 가지 길은 가정에서 결론으로 바로 가는 직접 증명, 결론의 부정에서 가정의 부정으로 가는 대우 증명, 결론을 부정해 모순을 끌어내는 귀류법이다.

왜 필요한가

테스트는 “이 입력들에서는 맞았다” 를 보여 준다. 증명은 “모든 입력에서 맞다” 를 보여 준다. 정렬 알고리즘이 항상 정렬된 결과를 내는지, 이진 탐색이 무한 루프에 빠지지 않는지, 암호 체계가 복호화에 성공하는지는 테스트만으로는 확신할 수 없다.

현업 개발자가 정식 증명을 매일 쓰지는 않는다. 그래도 “이 루프는 왜 끝나는가”, “이 락 순서에서는 왜 교착이 없는가” 를 말로 설명할 수 있어야 리뷰를 통과하고 장애를 막는다. 그 설명의 뼈대가 증명 기법이다.

핵심 개념

증명의 재료

  • 정의: 용어의 뜻. “정수 n 이 짝수다” ⇔ “n = 2k 인 정수 k 가 있다”.
  • 공리·이미 증명된 정리: 출발점으로 쓸 수 있는 사실.
  • 추론 규칙: 가장 기본은 전건 긍정(modus ponens). p 가 참이고 p → q 가 참이면 q 도 참이다.

증명이 막히면 대개 정의를 식으로 바꾸지 않아서다. “짝수”, “나누어떨어진다”, “유리수” 를 보면 먼저 정의대로 풀어 쓰는 습관을 들인다.

1. 직접 증명

p → q 를 보이려고 p 를 가정하고, 한 단계씩 q 에 도달한다.

정리. n 이 홀수면 n² 도 홀수다.

증명. n 이 홀수이므로 n = 2k + 1 인 정수 k 가 있다. 그러면 n² = 4k² + 4k + 1 = 2(2k² + 2k) + 1 이다. 2k² + 2k 는 정수이므로 n² 은 홀수다. ∎

2. 대우 증명

p → q 는 대우 ¬q → ¬p 와 논리적으로 동치다(001번 글의 진리표). 그래서 ¬q 를 가정하고 ¬p 를 보여도 된다. 결론 쪽 정보가 더 다루기 쉬울 때 쓴다.

정리. n² 이 짝수면 n 도 짝수다.

증명. 대우 “n 이 홀수면 n² 도 홀수다” 를 보이면 된다. 이는 바로 위에서 직접 증명했다. ∎

직접 증명으로 시도하면 “n² = 2m 이다” 에서 n 에 대해 말할 방법이 막막하다. 대우로 뒤집으니 한 줄이 된다.

3. 귀류법(모순에 의한 증명)

명제 P 를 보이려고 ¬P 를 가정하고, 그로부터 어떤 명제와 그 부정이 동시에 참이라는 모순을 끌어낸다. ¬P → (r ∧ ¬r) 가 참이면 ¬P 는 거짓일 수밖에 없다.

정리. √2 는 무리수다.

증명. √2 가 유리수라고 가정하자. 그러면 √2 = a/b 이고 a, b 는 서로소인 정수(b ≠ 0)로 쓸 수 있다. 양변을 제곱하면 a² = 2b² 이므로 a² 은 짝수, 위 정리에 따라 a 도 짝수다. a = 2c 로 두면 4c² = 2b², 즉 b² = 2c² 이므로 b 도 짝수다. a 와 b 가 모두 짝수이므로 서로소라는 가정과 모순이다. ∎

정리. 소수는 무한히 많다.

증명. 소수가 유한하다고 가정하고 그 전부를 p₁, …, pₙ 이라 하자. N = p₁p₂…pₙ + 1 을 생각한다. N 은 1 보다 크므로 어떤 소수 q 로 나누어떨어진다. q 는 목록 안의 어떤 pᵢ 다. pᵢ 는 p₁…pₙ 을 나누고 N 도 나누므로 둘의 차인 1 도 나눠야 한다. 이는 모순이다. ∎

주의할 점: N 자체가 소수라는 주장이 아니다. 2·3·5·7·11·13 + 1 = 30031 = 59 × 509 다. 증명은 “목록 밖의 소인수가 있다” 만 보인다.

세 기법 비교

기법 가정 도달 목표 잘 맞는 상황
직접 p q 정의를 풀면 길이 보일 때
대우 ¬q ¬p 결론의 부정이 더 구체적일 때
귀류 ¬P (또는 p ∧ ¬q) 모순 “없다”, “무한하다”, “무리수다” 처럼 부정형 결론

그 밖에 알아 둘 것

  • 반례에 의한 반증: ∀ 명제는 반례 하나로 깨진다. “모든 n 에 대해 n² + n + 41 은 소수다” 는 n = 40 에서 40² + 40 + 41 = 41² 이 되어 거짓이다.
  • 경우 나누기: n 이 짝수인 경우와 홀수인 경우를 따로 증명한다. 모든 경우를 빠짐없이 덮는지 확인해야 한다.
  • 필요충분조건(⇔): 양방향을 각각 증명한다.
  • 흔한 오류: 역을 증명하고 원래 명제를 증명했다고 착각하기, 결론을 가정에 몰래 넣기(순환 논증), 몇 개의 예로 일반 명제를 “증명” 하기.

직접 해 보기

컴퓨터는 증명을 대신하지는 못하지만, 증명할 가치가 있는지 반례를 찾는 데는 탁월하다. 위의 n² + n + 41 예를 직접 탐색해 보자. 그리고 증명이 다룬 30031 의 인수분해도 확인한다.

def is_prime(n):
    if n < 2:
        return False
    d = 2
    while d * d <= n:
        if n % d == 0:
            return False
        d += 1
    return True

# 반례 탐색: n^2 + n + 41
first_fail = next(n for n in range(1000) if not is_prime(n*n + n + 41))
print("첫 반례 n =", first_fail, "값 =", first_fail**2 + first_fail + 41)

# 유클리드 증명의 N
N = 2*3*5*7*11*13 + 1
print(N, is_prime(N), [d for d in range(2, 600) if N % d == 0])

# 대우 정리를 작은 범위에서 확인: n^2 짝수 -> n 짝수
print(all((n*n) % 2 == 1 or n % 2 == 0 for n in range(-1000, 1001)))

실행 결과다.

첫 반례 n = 40 값 = 1681
30031 False [59, 509]
True

마지막 줄의 True 는 증명이 아니다. -1000 부터 1000 까지에서 반례가 없다는 뜻일 뿐이다. 모든 정수에 대해 참이라는 보장은 앞의 대우 증명이 준다. 이 구분이 이 글의 요점이다.

현업에서는

  • 루프 불변식과 종료. 이진 탐색 코드를 리뷰할 때 “lo ≤ 정답 위치 ≤ hi 가 매 반복 유지된다(불변식)” 와 “hi - lo 가 매번 줄어든다(종료)” 를 말할 수 있으면 off-by-one 버그가 대부분 걸러진다. 불변식 유지는 직접 증명, 종료는 다음 글의 귀납법과 같은 구조다.
  • 교착 상태가 없음을 보이기. “모든 스레드가 락을 같은 전역 순서로 잡는다면 교착이 없다” 는 귀류법으로 보인다. 교착이 있다고 가정하면 대기 그래프에 순환이 생기고, 순환을 따라가면 순서가 자기 자신보다 앞서야 하는 모순이 나온다.
  • 증명 보조기. Lean 같은 증명 보조기는 사람이 쓴 증명을 기계가 한 단계씩 검사한다(Theorem Proving in Lean 4). 컴파일러 검증, 암호 라이브러리 검증 같은 분야에서 쓰인다.
  • 장애 회고. “이 설정이 원인이 아니라면 X 로그가 남았어야 한다. X 로그가 없다. 따라서 이 설정이 원인이다.” 이 추론은 대우를 이용한 것이다. 그런데 전제(“원인이 아니면 X 가 남는다”)가 실제로 참인지는 따로 확인해야 한다. 논리가 맞아도 전제가 틀리면 결론은 믿을 수 없다.

확인 문제

  1. “n 이 3 의 배수면 n² 도 3 의 배수다” 를 직접 증명하라.
  2. “n² 이 3 의 배수가 아니면 n 도 3 의 배수가 아니다” 는 1 번과 어떤 관계인가?
  3. “두 짝수의 합은 짝수다” 를 예 몇 개로 확인한 것이 증명이 아닌 이유는?
  4. “가장 큰 정수는 없다” 를 귀류법으로 증명하라.

풀이

  1. n = 3k 면 n² = 9k² = 3(3k²) 이므로 3 의 배수다.
  2. 1 번의 대우다. 따라서 1 번이 증명되면 자동으로 참이다.
  3. 유한 개의 예는 ∀ 명제의 모든 경우를 덮지 못한다. 정의(2a + 2b = 2(a + b))로 풀어야 증명이다.
  4. 가장 큰 정수 M 이 있다고 가정하자. M + 1 도 정수이고 M + 1 > M 이므로 M 이 가장 크다는 가정과 모순이다.

더 읽을거리 (References)