12.4 귀류법의 형식적 구조
1. 절의 학술적 목표
본 절은 귀류법(reductio ad absurdum)의 형식적 구조를 학술적으로 검토하는 것을 목표로 한다. 귀류법의 형식적 구조는 자연 연역 체계 내에서 가정의 도입, 모순의 도출, 가정의 해소, 결론의 도출로 이루어지는 단계적 구성이다. 본 절은 귀류법의 표준 표기, 두 형태의 형식적 도식, 가정의 범위 관리, 예시, 자연 연역 체계 외의 형식화, 학술적 의의를 체계적으로 정리한다.
2. 귀류법의 표준 표기
귀류법의 표준 표기는 고전적(강한) 귀류법의 경우 다음과 같다.
[¬A]
⋮
⊥
───── (RAA)
A
대괄호 안의 “¬A“는 귀류법의 가정이며, ⊥은 그 가정 하에서 도출된 모순이고, A는 가정이 해소된 후의 결론이다. “RAA“는 “reductio ad absurdum“의 약자이며, 이 규칙을 지칭하는 표준적 명칭이다. 이 표기는 Gentzen의 자연 연역 체계에서 고전 논리의 귀류법을 형식화한 것이다(Gentzen, 1935).
3. 약한 귀류법의 형식적 도식
약한 귀류법(직관주의적 귀류법)의 형식적 도식은 다음과 같다.
[A]
⋮
⊥
───── (¬I)
¬A
대괄호 안의 A는 가정이며, ⊥은 그 가정 하에서 도출된 모순이고, “¬A“는 가정이 해소된 후의 결론이다. 이 도식은 부정 도입 규칙과 동일하며, 고전 논리와 직관주의 논리 모두에서 수용된다. 약한 귀류법과 강한 귀류법의 형식적 도식의 차이는 가정하는 명제(A 또는 ¬A)와 결론으로 도출되는 명제(¬A 또는 A)에 있다(Prawitz, 1965).
4. 귀류법의 단계적 구성
귀류법의 형식적 구조는 다음의 네 단계로 구성된다. 첫째, 가정의 도입: 증명하려는 명제 A에 대하여 “¬A”(강한 형태) 또는 A(약한 형태)를 가정으로 도입한다. 둘째, 모순의 도출: 도입된 가정과 기존의 전제 및 추론 규칙을 사용하여 모순 ⊥ 또는 명시적 모순 “B ∧ ¬B“를 도출한다. 셋째, 가정의 해소: 귀류법 규칙 또는 부정 도입 규칙의 적용 시점에서 가정을 해소한다. 넷째, 결론의 도출: 해소된 가정에 대응하는 결론(A 또는 ¬A)을 최종적으로 도출한다. 이러한 단계적 구성은 귀류법 증명의 표준적 패턴이다(Copi, Cohen, & McMahon, 2014).
5. 귀류법 증명에서의 가정의 범위
귀류법 증명에서 가정의 범위는 가정의 도입부터 해소까지의 증명 단계들을 포함한다. 이 범위 내에서 도출된 모든 공식은 가정에 의존하며, 범위 외부에서는 사용될 수 없다. 가정의 해소 시점에서 범위가 종료되고, 결론은 더 이상 가정에 의존하지 않는다. 가정의 범위는 자연 연역 체계의 표기 방식에 따라 대괄호, 블록 구조, 또는 의존성 목록으로 표시된다. 가정의 범위 관리는 귀류법 증명의 타당성을 보장하는 핵심 요소이다(Prawitz, 1965).
6. 강한 귀류법의 단순 예시
강한 귀류법의 단순 예시는 다음과 같다. 전제로 “¬P → ⊥”(즉 “¬P“는 모순을 초래한다는 가정)이 주어졌을 때, “P“를 도출하는 증명은 다음과 같다.
1. ¬P → ⊥ (전제)
2. [¬P] (가정)
3. ⊥ (1, 2, →E)
4. P (2-3, RAA)
이 증명은 “¬P“를 가정하여 모순을 도출한 후, 귀류법 규칙으로 P를 결론으로 얻는다. 이 증명은 강한 귀류법의 가장 단순한 적용 형태이다(Mendelson, 2015).
7. 약한 귀류법의 단순 예시
약한 귀류법의 단순 예시는 다음과 같다. 전제로 “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)
이 증명은 P를 가정하여 모순을 도출한 후, 부정 도입 규칙으로 “¬P“를 결론으로 얻는다. 이 증명은 약한 귀류법(부정 도입 규칙)의 표준적 적용 형태이며, 후건 부정(modus tollens)의 자연 연역 증명이기도 하다(Copi, Cohen, & McMahon, 2014).
8. 강한 귀류법의 복합 예시
강한 귀류법의 복합 예시는 배중률 “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, RAA)
이 증명은 “¬(P ∨ ¬P)“를 가정하여 모순을 도출하고, 강한 귀류법으로 “P ∨ ¬P“를 결론으로 얻는다. 이 증명은 배중률이 고전 논리에서 정리임을 보이며, 강한 귀류법이 직관주의 논리에서 일반적으로 수용되지 않는 이유를 반영한다(Mendelson, 2015).
9. 귀류법과 자연 연역 체계 외의 형식화
귀류법은 자연 연역 체계 외에도 다른 형식 체계에서 다양하게 형식화된다. 첫째, 순차 계산(sequent calculus)에서는 귀류법이 컷 규칙(cut rule) 또는 부정 규칙과 관련되어 표현된다. 둘째, 공리 체계에서는 귀류법이 이중 부정 제거 공리 “¬¬A → A” 또는 이에 상응하는 공리를 통하여 도출된다. 셋째, 구성적 논리 체계에서는 약한 귀류법만이 기본 규칙으로 채택되며, 강한 귀류법은 특정 조건 하에서만 유효하다. 이러한 다양한 형식화는 귀류법이 논리 체계에 따라 다른 형태로 표현됨을 보여 준다(Gentzen, 1935).
10. 귀류법의 형식적 구조와 증명의 복잡성
귀류법 증명은 직접 증명에 비하여 추가적인 구조적 복잡성을 가진다. 이 복잡성은 가정의 도입과 해소, 모순의 도출, 중첩된 하위 증명의 구성에서 비롯된다. 귀류법 증명은 일반적으로 직접 증명보다 길고 복잡하며, 증명의 각 단계가 가정의 범위 내에서 이루어지는지를 추적해야 한다. 그러나 귀류법은 직접 증명이 불가능하거나 매우 어려운 경우에 필수적인 증명 방법이며, 이러한 복잡성은 그 증명 능력의 대가이다(Prawitz, 1965).
11. 귀류법의 형식적 구조의 학술적 의의
귀류법의 형식적 구조는 다음과 같은 학술적 의의를 가진다. 첫째, 그것은 귀류법을 직관적 증명 방법에서 엄밀한 형식적 규칙으로 전환한다. 둘째, 그것은 가정의 도입과 해소의 메커니즘을 통하여 자연 연역 체계의 일반 원리를 따른다. 셋째, 그것은 약한 형태와 강한 형태의 구조적 차이를 명확히 보여 주며, 고전 논리와 직관주의 논리의 차이를 형식화한다. 넷째, 그것은 귀류법 증명의 단계적 구성과 가정의 범위 관리를 정확히 규정함으로써 증명의 타당성을 보장한다. 다섯째, 그것은 증명의 자동화와 형식적 검증의 기초를 제공한다(Mendelson, 2015).
12. 본 절의 결론적 정리
귀류법의 형식적 구조는 자연 연역 체계 내에서 가정의 도입, 모순의 도출, 가정의 해소, 결론의 도출로 이루어지는 단계적 구성이다. 강한 귀류법은 “¬A“를 가정하여 모순을 도출한 후 A를 결론으로 얻는 규칙이며, 약한 귀류법은 A를 가정하여 모순을 도출한 후 “¬A“를 결론으로 얻는 규칙이다. 두 형태는 각각 “RAA“와 “¬I“의 표준 표기로 형식화된다. 귀류법 증명의 가정의 범위는 가정의 도입부터 해소까지의 증명 단계들을 포함하며, 범위 관리는 증명의 타당성을 보장하는 핵심 요소이다. 귀류법은 자연 연역 체계 외에도 순차 계산과 공리 체계에서 다양하게 형식화된다. 학습자는 귀류법의 표준 표기, 단계적 구성, 가정의 범위 관리, 두 형태의 형식적 차이를 정확히 이해해야 한다.
13. 출처
- Gentzen, G. (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39, 176–210, 405–431.
- 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