11.17 자연 연역을 통한 정리 증명
1. 절의 학술적 목표
본 절은 자연 연역 체계를 사용하여 명제 논리의 주요 정리(theorem)를 증명하는 방법을 학술적으로 검토하는 것을 목표로 한다. 정리 증명은 자연 연역 체계의 실제 활용 사례이며, 전제 없이 순수하게 추론 규칙의 적용만으로 논리적 진리를 증명하는 절차이다. 본 절은 정리의 개념, 증명 전략, 주요 정리의 증명 예시, 증명의 구성 원리, 학술적 의의를 체계적으로 정리한다.
2. 정리의 학술적 정의
자연 연역 체계에서 정리(theorem)란 전제 없이 순수하게 추론 규칙의 적용만으로 증명 가능한 공식을 의미한다. 형식적으로, 공식 A가 자연 연역 체계의 정리라는 것은 “⊢ A“로 표기되며, 이는 빈 가정 집합으로부터 A가 도출됨을 의미한다. 정리는 항진식(tautology)과 대응하며, 건전성 정리와 완전성 정리에 의하여 고전 명제 논리의 자연 연역 체계에서는 정리와 항진식이 동일한 공식 집합을 이룬다(Mendelson, 2015).
3. 정리 증명의 일반적 전략
정리 증명의 일반적 전략은 다음과 같다. 첫째, 결론의 주 연결자를 확인하고, 그 연결자의 도입 규칙을 사용하여 증명을 역방향으로 설계한다. 둘째, 필요한 경우 가정을 도입하여 조건 증명 또는 귀류법을 구성한다. 셋째, 각 가정 하에서 필요한 중간 공식을 도출하고, 최종적으로 가정을 해소하여 결론을 얻는다. 넷째, 증명이 완료되면 가정의 해소가 올바르게 이루어졌는지와 모든 단계가 정당한 규칙의 적용인지를 검토한다. 이러한 전략은 자연 연역 증명의 표준적 구성 방법이다(Prawitz, 1965).
4. 동일률 “P → P“의 증명
동일률 “P → P“는 자연 연역 체계에서 가장 단순한 정리이다. 증명은 다음과 같다.
1. [P] (가정)
2. P (1, 반복)
3. P → P (1-2, →I)
이 증명은 P의 가정 하에서 P가 직접 도출되므로, 조건 도입 규칙으로 “P → P“를 전제 없이 도출한다. 동일률은 자연 연역 체계의 가장 기본적인 정리이며, 조건 도입 규칙의 가장 단순한 적용을 보여 준다(Copi, Cohen, & McMahon, 2014).
5. 모순률 “¬(P ∧ ¬P)“의 증명
모순률 “¬(P ∧ ¬P)“의 증명은 다음과 같다.
1. [P ∧ ¬P] (가정)
2. P (1, ∧E₁)
3. ¬P (1, ∧E₂)
4. ⊥ (2, 3, ¬E)
5. ¬(P ∧ ¬P) (1-4, ¬I)
이 증명은 “P ∧ ¬P“를 가정하여 모순을 도출하고, 부정 도입 규칙으로 “¬(P ∧ ¬P)“를 결론으로 얻는다. 모순률은 고전 논리와 직관주의 논리 모두에서 정리이며, 부정 도입 규칙의 표준적 적용을 보여 준다(Mendelson, 2015).
6. 배중률 “P ∨ ¬P“의 증명
배중률 “P ∨ ¬P“는 고전 논리의 대표적 정리이며, 증명은 이중 부정 제거 규칙을 활용한다. 증명은 다음과 같다.
1. [¬(P ∨ ¬P)] (가정)
2. [P] (가정)
3. P ∨ ¬P (2, ∨I₁)
4. ⊥ (3, 1, ¬E)
5. ¬P (2-4, ¬I)
6. P ∨ ¬P (5, ∨I₂)
7. ⊥ (6, 1, ¬E)
8. ¬¬(P ∨ ¬P) (1-7, ¬I)
9. P ∨ ¬P (8, ¬¬E)
이 증명은 “¬(P ∨ ¬P)“를 가정하여 모순을 도출하고, 부정 도입 규칙으로 “¬¬(P ∨ ¬P)“를 얻은 후, 이중 부정 제거 규칙으로 “P ∨ ¬P“를 결론으로 도출한다. 배중률의 증명은 이중 부정 제거 규칙을 본질적으로 필요로 하며, 직관주의 논리에서는 일반적으로 정리가 아니다(Heyting, 1956).
7. 대우 법칙 “(P → Q) → (¬Q → ¬P)“의 증명
대우 법칙 “(P → Q) → (¬Q → ¬P)“의 증명은 다음과 같다.
1. [P → Q] (가정)
2. [¬Q] (가정)
3. [P] (가정)
4. Q (1, 3, →E)
5. ⊥ (4, 2, ¬E)
6. ¬P (3-5, ¬I)
7. ¬Q → ¬P (2-6, →I)
8. (P → Q) → (¬Q → ¬P) (1-7, →I)
이 증명은 세 개의 가정이 중첩되어 도입되고, 내부부터 외부로 순차적으로 해소된다. 대우 법칙은 고전 논리와 직관주의 논리 모두에서 정리이며, 조건 도입 규칙과 부정 도입 규칙의 결합을 보여 준다(Copi, Cohen, & McMahon, 2014).
8. 드 모르간 법칙 “¬(P ∨ Q) → (¬P ∧ ¬Q)“의 증명
드 모르간 법칙 “¬(P ∨ Q) → (¬P ∧ ¬Q)“의 증명은 다음과 같다.
1. [¬(P ∨ Q)] (가정)
2. [P] (가정)
3. P ∨ Q (2, ∨I₁)
4. ⊥ (3, 1, ¬E)
5. ¬P (2-4, ¬I)
6. [Q] (가정)
7. P ∨ Q (6, ∨I₂)
8. ⊥ (7, 1, ¬E)
9. ¬Q (6-8, ¬I)
10. ¬P ∧ ¬Q (5, 9, ∧I)
11. ¬(P ∨ Q) → (¬P ∧ ¬Q) (1-10, →I)
이 증명은 선언 도입 규칙, 부정 도입 규칙, 연언 도입 규칙, 조건 도입 규칙의 결합으로 이루어지며, 드 모르간 법칙의 한 방향을 형식적으로 증명한다. 이 방향은 고전 논리와 직관주의 논리 모두에서 정리이다(Mendelson, 2015).
9. 가설적 삼단논법의 증명
가설적 삼단논법 “(P → Q) → ((Q → R) → (P → R))“의 증명은 다음과 같다.
1. [P → Q] (가정)
2. [Q → R] (가정)
3. [P] (가정)
4. Q (1, 3, →E)
5. R (2, 4, →E)
6. P → R (3-5, →I)
7. (Q → R) → (P → R) (2-6, →I)
8. (P → Q) → ((Q → R) → (P → R)) (1-7, →I)
이 증명은 세 개의 중첩된 가정과 조건 제거 규칙의 연쇄 적용, 그리고 세 번의 조건 도입 규칙의 적용으로 이루어진다. 가설적 삼단논법은 조건의 추이성을 형식화하는 고전적 정리이다(Copi, Cohen, & McMahon, 2014).
10. 정리 증명의 구성 원리
자연 연역 체계에서 정리를 증명하는 일반적 원리는 다음과 같다. 첫째, 결론의 논리적 구조를 분석하여 주 연결자를 확인한다. 둘째, 주 연결자의 도입 규칙을 증명의 마지막 단계로 설정한다. 셋째, 그 도입 규칙의 전제를 증명의 중간 목표로 삼고, 이를 도출하기 위한 가정과 하위 증명을 구성한다. 넷째, 하위 증명에서 필요한 경우 같은 전략을 재귀적으로 적용한다. 다섯째, 모든 가정이 올바르게 해소되었는지 확인한다. 이러한 역방향 분석 전략은 자연 연역 증명의 표준적 구성 방법이다(Prawitz, 1965).
11. 자연 연역을 통한 정리 증명의 학술적 의의
자연 연역을 통한 정리 증명은 다음과 같은 학술적 의의를 가진다. 첫째, 그것은 자연 연역 체계의 이론적 능력을 실제로 입증한다. 둘째, 그것은 명제 논리의 주요 정리들(동일률, 모순률, 배중률, 대우 법칙, 드 모르간 법칙, 가설적 삼단논법 등)이 자연 연역 체계에서 형식적으로 증명 가능함을 보여 준다. 셋째, 그것은 건전성 정리와 완전성 정리의 맥락에서 자연 연역 체계의 정리와 고전 명제 논리의 항진식이 동일함을 실증한다. 넷째, 그것은 학습자가 자연 연역 체계의 추론 규칙을 체계적으로 활용하는 능력을 기를 수 있게 한다. 다섯째, 그것은 수학적 정리 증명의 형식적 기초를 제공한다(Mendelson, 2015).
12. 본 절의 결론적 정리
자연 연역 체계에서 정리란 전제 없이 순수하게 추론 규칙의 적용만으로 증명 가능한 공식이며, 고전 명제 논리의 항진식과 대응한다. 정리 증명의 일반적 전략은 결론의 주 연결자에 대응하는 도입 규칙을 마지막 단계로 설정하고, 필요한 가정을 도입하여 하위 증명을 구성한 후 가정을 해소하는 역방향 분석이다. 동일률 “P → P”, 모순률 “¬(P ∧ ¬P)”, 배중률 “P ∨ ¬P”, 대우 법칙, 드 모르간 법칙, 가설적 삼단논법 등 주요 정리는 자연 연역 체계에서 형식적으로 증명 가능하다. 배중률의 증명은 이중 부정 제거 규칙을 본질적으로 필요로 하며, 고전 논리와 직관주의 논리의 차이를 보여 준다. 학습자는 정리의 개념, 증명 전략, 주요 정리의 증명 방법, 구성 원리를 정확히 이해하고, 자연 연역 체계를 활용하여 새로운 정리를 독립적으로 증명할 수 있어야 한다.
13. 출처
- Gentzen, G. (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39, 176–210, 405–431.
- Heyting, A. (1956). Intuitionism: An Introduction. Amsterdam: North-Holland.
- Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study. Stockholm: Almqvist & Wiksell.
- Copi, I. M., Cohen, C., & McMahon, K. (2014). Introduction to Logic (14th ed.). London: Routledge.
- Mendelson, E. (2015). Introduction to Mathematical Logic (6th ed.). Boca Raton: CRC Press.
14. 버전
- 문서 버전: 1.0
- 작성 기준일: 2026-04-15