11.12 부정 제거 규칙

11.12 부정 제거 규칙

1. 절의 학술적 목표

본 절은 자연 연역 체계의 부정 제거 규칙(negation elimination rule, ¬E)을 학술적으로 검토하는 것을 목표로 한다. 부정 제거 규칙은 명제와 그 부정의 결합으로부터 모순을 도출하는 추론 규칙이며, 또한 고전 논리에서는 이중 부정 제거를 통하여 임의의 공식을 도출하는 규칙을 포함한다. 본 절은 부정 제거 규칙의 정식화, 의미론적 정당화, 구조, 적용, 예시, 직관주의 논리와의 관계, 학술적 의의를 체계적으로 정리한다.

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

부정 제거 규칙은 두 가지 형태로 이해된다. 첫째 형태는 명제 A와 그 부정 “¬A“가 모두 증명되었을 때, 모순 ⊥을 도출할 수 있음을 규정한다. 둘째 형태는 고전 논리에서 이중 부정 “¬¬A“로부터 A를 도출할 수 있음을 규정하는 규칙이며, 이중 부정 제거 규칙이라 불린다. 자연 연역 체계의 설계에 따라 두 형태 중 하나 또는 모두가 부정 제거 규칙으로 채택된다(Gentzen, 1935).

3. 부정 제거 규칙의 표준 표기

부정 제거 규칙의 두 형태에 대한 표준 표기는 다음과 같다. 첫째 형태(모순 도출):

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

둘째 형태(이중 부정 제거):

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

전자는 고전 논리와 직관주의 논리 모두에서 기본 규칙으로 인정되지만, 후자는 고전 논리에서만 기본 규칙으로 인정된다(Gentzen, 1935).

4. 부정 제거 규칙의 의미론적 정당화

부정 제거 규칙의 첫째 형태(모순 도출)는 모순의 원리에 의하여 정당화된다. A와 “¬A“가 동시에 참일 수 없으므로, 두 공식이 모두 증명되면 모순이 도출된다. 이 정당화는 고전 논리와 직관주의 논리 모두에서 유효하다. 둘째 형태(이중 부정 제거)는 고전 논리의 이원적 진리값 원리에 의하여 정당화된다. “¬¬A“는 “A가 거짓이 아니다“를 의미하며, 고전 논리에서 이는 “A가 참이다“와 동치이다(Mendelson, 2015).

5. 모순 도출 규칙과 귀류법

부정 제거 규칙의 첫째 형태는 귀류법의 핵심 단계를 제공한다. 귀류법 증명에서는 가정을 도입한 후 그 가정과 모순되는 공식을 도출하고, 부정 제거 규칙으로 모순 ⊥을 얻는다. 그 다음 부정 도입 규칙으로 가정의 부정을 결론으로 도출한다. 따라서 부정 제거 규칙과 부정 도입 규칙은 귀류법의 두 단계를 구성하며, 두 규칙의 결합으로 완전한 귀류법 증명이 이루어진다(Prawitz, 1965).

6. 폭발 원리

자연 연역 체계에서 모순으로부터 임의의 공식을 도출하는 규칙을 폭발 원리(ex falso quodlibet 또는 principle of explosion)라 한다. 폭발 원리의 표기는 다음과 같다.

⊥
── (⊥E)
A

여기서 A는 임의의 공식이다. 폭발 원리는 고전 논리와 직관주의 논리 모두에서 기본 규칙으로 인정되며, “모순으로부터는 무엇이든 따라 나온다“라는 원리의 형식화이다. 폭발 원리는 부정 제거 규칙의 일종으로 간주되거나, 별도의 모순 제거 규칙으로 취급된다(Mendelson, 2015).

7. 부정 제거 규칙의 단순 적용 예시

부정 제거 규칙의 첫째 형태의 단순 적용 예시는 다음과 같다. 전제로 “P“와 “¬P“가 주어졌을 때, 임의의 공식 “Q“를 도출하는 증명은 다음과 같다.

1. P          (전제)
2. ¬P         (전제)
3. ⊥          (1, 2, ¬E)
4. Q          (3, ⊥E)

이 증명은 부정 제거 규칙과 폭발 원리의 결합으로 모순된 전제로부터 임의의 결론을 도출할 수 있음을 보여 준다(Copi, Cohen, & McMahon, 2014).

8. 이중 부정 제거 규칙의 적용 예시

이중 부정 제거 규칙의 적용 예시는 다음과 같다. 전제로 “¬¬P“가 주어졌을 때, “P“를 도출하는 증명은 다음과 같다.

1. ¬¬P        (전제)
2. P          (1, ¬¬E)

이 증명은 이중 부정 제거 규칙의 단순한 한 단계 적용으로 이루어진다. 고전 논리에서 이 규칙은 배중률(P ∨ ¬P)의 증명과 밀접한 관계를 가지며, 고전 논리의 특징적 규칙이다(Mendelson, 2015).

9. 직관주의 논리와의 관계

직관주의 논리에서는 부정 제거 규칙의 첫째 형태(모순 도출)는 수용되지만, 둘째 형태(이중 부정 제거)는 일반적으로 수용되지 않는다. 직관주의 논리는 “A가 거짓이 아니다“라는 주장과 “A가 참이다“라는 주장을 동일시하지 않으므로, “¬¬A“로부터 A를 직접 도출할 수 없다. 이러한 차이는 직관주의 논리가 구성적 증명 가능성을 강조하기 때문이다. 직관주의 논리와 고전 논리의 차이는 이중 부정 제거 규칙의 수용 여부로 간결하게 특징지어진다(Heyting, 1956).

10. 부정 제거 규칙과 부정 도입 규칙의 조화

부정 제거 규칙의 첫째 형태는 부정 도입 규칙과 조화 원리에 의하여 대응한다. 부정 도입 규칙은 가정 A 하에서 모순이 도출되면 “¬A“를 구성하는 방법을 제공하고, 부정 제거 규칙의 첫째 형태는 A와 “¬A“로부터 모순을 도출하는 방법을 제공한다. 두 규칙의 결합은 부정 연결자의 의미를 부분적으로 정의한다. 이중 부정 제거 규칙은 이러한 조화의 범위를 벗어나며, 고전 논리의 추가적 원리로 간주된다(Prawitz, 1965).

11. 부정 제거 규칙의 학술적 의의

부정 제거 규칙은 다음과 같은 학술적 의의를 가진다. 첫째, 그것은 부정 연결자의 분해 조건을 형식화한다. 둘째, 그것은 귀류법 증명의 핵심 단계를 제공한다. 셋째, 그것은 폭발 원리와 결합되어 모순으로부터의 추론을 형식화한다. 넷째, 이중 부정 제거 규칙은 고전 논리와 직관주의 논리를 구별하는 핵심 규칙이다. 다섯째, 부정 제거 규칙의 두 형태는 부정의 두 측면(모순 인식과 이원적 진리값)을 반영한다(Gentzen, 1935).

12. 본 절의 결론적 정리

부정 제거 규칙은 자연 연역 체계에서 두 형태로 이해된다. 첫째 형태는 명제 A와 그 부정 “¬A“로부터 모순 ⊥을 도출하는 규칙이며, 고전 논리와 직관주의 논리 모두에서 기본 규칙이다. 둘째 형태는 이중 부정 “¬¬A“로부터 A를 도출하는 이중 부정 제거 규칙이며, 고전 논리에서만 기본 규칙이다. 첫째 형태는 부정 도입 규칙과 함께 귀류법을 구성하며, 폭발 원리와 결합되어 모순 추론을 형식화한다. 이중 부정 제거 규칙은 고전 논리와 직관주의 논리를 구별하는 핵심 규칙이다. 학습자는 부정 제거 규칙의 두 형태, 의미론적 정당화, 적용 방법, 두 논리 체계에서의 위상을 정확히 이해하고, 자연 연역 증명에 활용할 수 있어야 한다.

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