12.12 이중 부정 제거와 귀류법

12.12 이중 부정 제거와 귀류법

1. 절의 학술적 목표

본 절은 이중 부정 제거 규칙(double negation elimination rule)과 귀류법(reductio ad absurdum)의 관계를 학술적으로 검토하는 것을 목표로 한다. 이중 부정 제거 규칙은 고전적(강한) 귀류법의 형식적 기초이며, 두 원리는 고전 논리에서 상호 환원 가능하다. 본 절은 이중 부정 제거 규칙의 정의, 귀류법과의 형식적 관계, 상호 환원, 의미론적 정당화, 예시, 직관주의 논리에서의 제한, 학술적 의의를 체계적으로 정리한다.

2. 이중 부정 제거 규칙의 학술적 정의

이중 부정 제거 규칙은 “¬¬A“로부터 A를 도출할 수 있음을 규정하는 추론 규칙이다. 형식적으로 이 규칙은 다음과 같이 표기된다.

¬¬A
──── (¬¬E)
 A

이 규칙은 “A가 거짓이 아니다“로부터 “A가 참이다“로의 추론을 허용하며, 고전 논리의 이원적 진리값 원리에 기반한다. 이중 부정 제거 규칙은 고전 논리의 특징적 규칙이며, 직관주의 논리에서는 일반적으로 수용되지 않는다(Mendelson, 2015).

3. 이중 부정 제거와 강한 귀류법의 동등성

이중 부정 제거 규칙과 강한 귀류법(고전적 귀류법)은 고전 논리에서 상호 환원 가능하며, 논리적으로 동등하다. 즉, 부정 도입 규칙이 주어진 전제 하에서 이중 부정 제거 규칙이 성립하면 강한 귀류법이 성립하고, 역으로 강한 귀류법이 성립하면 이중 부정 제거 규칙이 성립한다. 이러한 상호 환원은 두 원리가 고전 논리에서 동일한 증명 능력을 가짐을 보여 준다. 자연 연역 체계의 설계에서는 두 원리 중 하나를 기본 규칙으로 채택하고 다른 하나를 파생 규칙으로 도출하는 것이 일반적이다(Prawitz, 1965).

4. 강한 귀류법으로부터 이중 부정 제거의 도출

강한 귀류법을 기본 규칙으로 전제하면 이중 부정 제거 규칙은 다음과 같이 도출된다.

1. ¬¬A        (전제)
2. [¬A]       (가정)
3. ⊥          (2, 1, ¬E)
4. A          (2-3, RAA)

이 도출은 “¬A“를 가정하여 전제 “¬¬A“와의 부정 제거 규칙으로 모순을 얻은 후, 강한 귀류법으로 A를 결론으로 도출한다. 이 도출은 강한 귀류법이 이중 부정 제거 규칙을 포함함을 보여 준다(Prawitz, 1965).

5. 이중 부정 제거로부터 강한 귀류법의 도출

이중 부정 제거 규칙을 기본 규칙으로 전제하면 강한 귀류법은 부정 도입 규칙과 이중 부정 제거의 결합으로 다음과 같이 도출된다.

[¬A]
 ⋮
 ⊥
───── (¬I)
¬¬A
───── (¬¬E)
 A

이 도출은 “¬A“의 가정 하에서 모순이 도출되면 부정 도입 규칙으로 “¬¬A“가 얻어지고, 이중 부정 제거 규칙으로 A가 결론으로 도출됨을 보여 준다. 이 도출은 이중 부정 제거 규칙이 강한 귀류법을 포함함을 보여 준다(Mendelson, 2015).

6. 이중 부정 도입 규칙

이중 부정 제거 규칙의 역방향인 이중 부정 도입 규칙 “A로부터 ¬¬A“는 고전 논리와 직관주의 논리 모두에서 성립한다. 이 규칙의 증명은 다음과 같다.

1. A          (전제)
2. [¬A]       (가정)
3. ⊥          (1, 2, ¬E)
4. ¬¬A        (2-3, ¬I)

이 증명은 이중 부정 도입이 부정 도입 규칙의 직접 적용으로 도출됨을 보여 주며, 이 증명은 직관주의 논리에서도 유효하다. 이중 부정 도입은 두 논리 체계의 공통 원리이며, 이중 부정 제거와의 비대칭성은 직관주의 논리의 특징이다(Heyting, 1956).

7. 이중 부정 제거의 의미론적 정당화

이중 부정 제거의 의미론적 정당화는 고전 논리의 이원적 진리값 원리에 기반한다. 고전 명제 논리에서 각 명제는 참 또는 거짓의 두 값 중 하나를 가지며, “¬¬A“는 “A가 거짓이다“의 부정, 즉 “A가 거짓이 아니다“를 의미한다. 이원적 진리값 원리에 의하여 “A가 거짓이 아니다“는 “A가 참이다“와 동치이며, 따라서 “¬¬A“로부터 A로의 도출이 정당화된다. 이러한 정당화는 이중 부정 제거가 고전 논리의 이원성을 반영하는 규칙임을 보여 준다(Mendelson, 2015).

8. 직관주의 논리에서의 이중 부정 제거의 거부

직관주의 논리에서는 이중 부정 제거 규칙이 일반적으로 수용되지 않는다. 그 이유는 직관주의 논리의 의미론에서 “¬¬A“는 “A의 구성이 불가능하다는 가정은 모순을 초래한다“를 의미하며, 이는 “A를 실제로 구성할 수 있다“와 동등하지 않기 때문이다. 직관주의 논리는 수학적 진리를 구성적 증명과 동일시하므로, “A가 거짓이 아니다“로부터 “A가 참이다“로의 직접적 도출은 정당화되지 않는다. 이러한 거부는 직관주의 논리가 고전 논리보다 엄격한 구성적 조건을 요구함을 보여 준다(Heyting, 1956).

9. 특수한 경우의 이중 부정 제거

직관주의 논리에서 이중 부정 제거가 제한적으로 성립하는 경우가 있다. 첫째, 결정 가능한 명제(decidable propositions)에 대해서는 이중 부정 제거가 성립한다. 예를 들어, 정수의 산술적 성질(유한한 경우의 분석으로 결정 가능한 성질)에 대해서는 “¬¬A → A“가 증명 가능하다. 둘째, 부정 명제에 대해서는 “¬¬¬A → ¬A“가 직관주의적으로 성립한다. 이러한 제한적 성립은 이중 부정 제거가 일부 명제 유형에 대해서는 직관주의 논리에서도 유효함을 보여 준다(Heyting, 1956).

10. 이중 부정 제거와 배중률

이중 부정 제거 규칙과 배중률 “A ∨ ¬A“는 고전 논리에서 논리적으로 동등하다. 즉, 부정 도입 규칙이 주어진 전제 하에서 한 원리가 성립하면 다른 원리도 성립한다. 이러한 동등성은 두 원리가 고전 논리의 특징적 원리를 다른 각도에서 표현함을 보여 준다. 배중률은 명제의 진리값에 대한 직접적 주장이고, 이중 부정 제거는 부정의 해석에 대한 주장이다. 두 원리의 동등성은 고전 논리의 통일적 이해를 가능하게 한다(Mendelson, 2015).

11. 이중 부정 제거와 귀류법의 학술적 의의

이중 부정 제거와 귀류법의 관계는 다음과 같은 학술적 의의를 가진다. 첫째, 그것은 고전 논리의 두 특징적 원리(이중 부정 제거와 강한 귀류법)가 논리적으로 동등함을 보여 준다. 둘째, 그것은 자연 연역 체계의 설계에서 두 원리 중 하나를 기본 규칙으로 선택하는 근거를 제공한다. 셋째, 그것은 고전 논리와 직관주의 논리의 차이를 이중 부정 제거의 수용 여부로 간결하게 특징짓는다. 넷째, 그것은 구성적 수학과 비구성적 수학의 구별을 형식적으로 뒷받침한다. 다섯째, 그것은 증명 이론의 메타이론적 분석에서 중요한 역할을 한다(Prawitz, 1965).

12. 본 절의 결론적 정리

이중 부정 제거 규칙은 “¬¬A로부터 A“의 도출을 허용하는 규칙이며, 고전 논리의 특징적 규칙이다. 이중 부정 제거 규칙과 강한 귀류법은 고전 논리에서 상호 환원 가능하며, 논리적으로 동등하다. 강한 귀류법으로부터 이중 부정 제거는 “¬A“의 가정과 부정 제거 규칙의 결합으로 도출되고, 이중 부정 제거로부터 강한 귀류법은 부정 도입 규칙과 이중 부정 제거의 결합으로 도출된다. 이중 부정 제거는 고전 논리의 이원적 진리값 원리에 의하여 정당화되며, 직관주의 논리에서는 일반적으로 수용되지 않는다. 결정 가능한 명제에 대해서는 직관주의 논리에서도 이중 부정 제거가 제한적으로 성립한다. 이중 부정 제거 규칙은 배중률과 고전 논리에서 논리적으로 동등하다. 학습자는 이중 부정 제거의 정의, 귀류법과의 상호 환원, 의미론적 정당화, 직관주의 논리에서의 거부와 제한적 성립, 배중률과의 관계를 정확히 이해해야 한다.

13. 출처

  • Heyting, A. (1956). Intuitionism: An Introduction. Amsterdam: North-Holland.
  • Prawitz, D. (1965). Natural Deduction: A Proof-Theoretical Study. Stockholm: Almqvist & Wiksell.
  • Mendelson, E. (2015). Introduction to Mathematical Logic (6th ed.). Boca Raton: CRC Press.

14. 버전

  • 문서 버전: 1.0
  • 작성 기준일: 2026-04-15