11.11 부정 도입 규칙

11.11 부정 도입 규칙

1. 절의 학술적 목표

본 절은 자연 연역 체계의 부정 도입 규칙(negation introduction rule, ¬I)을 학술적으로 검토하는 것을 목표로 한다. 부정 도입 규칙은 가정으로부터 모순이 도출되었을 때 그 가정의 부정을 결론으로 도출하는 추론 규칙이며, 귀류법(reductio ad absurdum)의 형식화이다. 본 절은 부정 도입 규칙의 정식화, 역사적 배경, 의미론적 정당화, 적용, 예시, 학술적 의의를 체계적으로 정리한다.

2. 부정 도입 규칙의 학술적 정의

부정 도입 규칙은 가정 A 하에서 모순(⊥)이 도출되었을 때, 가정 A를 해소하고 그 부정 “¬A“를 결론으로 도출할 수 있음을 규정하는 규칙이다. 여기서 모순은 “B ∧ ¬B“와 같은 명시적 모순이거나, 형식적 거짓 기호 ⊥로 표현된다. 이 규칙은 부정 연결자 “¬“를 결론에 도입하는 규칙이며, 귀류법의 형식화이다(Gentzen, 1935).

3. 부정 도입 규칙의 표준 표기

부정 도입 규칙의 표준 표기는 다음과 같다.

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

대괄호 안의 A는 일시적으로 도입된 가정이고, ⊥은 그 가정 하에서 도출된 모순이며, “¬A“는 가정 A가 해소된 후의 결론이다. 규칙의 적용 시점에서 가정 A는 해소되며, 결론 “¬A“는 더 이상 가정 A에 의존하지 않는다(Gentzen, 1935).

4. 부정 도입 규칙의 역사적 배경

부정 도입 규칙은 귀류법이라는 이름으로 고대로부터 알려진 증명 방법의 형식화이다. 귀류법은 “어떤 명제의 부정을 가정하여 모순이 도출되면 원래의 명제가 참이다“라는 원리로, 아리스토텔레스의 『Prior Analytics』와 유클리드의 『Elements』에서 체계적으로 사용되었다. 특히 유클리드의 “2의 제곱근의 무리수 증명“은 귀류법의 고전적 예시이다. 자연 연역 체계는 이러한 고대의 증명 방법을 형식적으로 체계화한다(Aristoteles, trans. 1984).

5. 부정 도입 규칙의 의미론적 정당화

부정 도입 규칙은 모순의 원리와 부정의 진리 함수적 정의에 의하여 정당화된다. 만약 A의 가정이 모순을 초래한다면, A는 참일 수 없다(모순은 참일 수 없으므로). 따라서 “¬A“가 성립한다. 이러한 정당화는 부정 도입 규칙이 타당한 추론 규칙임을 보장한다. 의미론적으로, 이는 “A가 참이라고 하면 모순이 따라 나오므로 A는 참이 아니다“라는 원리의 형식화이다(Mendelson, 2015).

6. 부정 도입 규칙과 귀류법

부정 도입 규칙은 귀류법의 직접적 형식화이다. 귀류법은 수학적 증명에서 가장 강력하고 자주 사용되는 증명 방법 중 하나이며, 직접 증명이 어려운 명제를 간접적으로 증명하는 데 유용하다. 부정 도입 규칙은 이러한 귀류법을 자연 연역 체계 내에서 엄밀히 형식화함으로써, 귀류법 증명을 기계적이고 검증 가능한 절차로 변환한다(Prawitz, 1965).

7. 부정 도입 규칙의 단순 적용 예시

부정 도입 규칙의 단순 적용 예시는 다음과 같다. 전제로 “P → Q“와 “¬Q“가 주어졌을 때, “¬P“를 도출하는 증명(후건 부정)은 다음과 같다.

1. P → Q          (전제)
2. ¬Q             (전제)
3. [P]            (가정)
4. Q              (1, 3, →E)
5. Q ∧ ¬Q         (4, 2, ∧I)
6. ⊥              (5, ⊥I)
7. ¬P             (3-6, ¬I)

이 증명은 P를 가정한 후 모순을 도출하고, 가정 P를 해소하여 “¬P“를 결론으로 얻는다. 이 증명은 후건 부정(modus tollens)의 자연 연역 증명이다(Copi, Cohen, & McMahon, 2014).

8. 모순의 표현

부정 도입 규칙에서 모순은 두 가지 방식으로 표현될 수 있다. 첫째, 명시적 모순 “B ∧ ¬B“의 형태. 둘째, 형식적 거짓 기호 ⊥로 추상화된 형태. 두 표현은 의미론적으로 동등하며, 자연 연역 체계의 설계에 따라 선택된다. ⊥ 기호를 사용하는 체계에서는 “B ∧ ¬B“로부터 ⊥로의 이행을 허용하는 별도의 규칙(모순 도입 규칙)이 필요할 수 있다(Prawitz, 1965).

9. 부정 도입 규칙의 복합 적용 예시

부정 도입 규칙의 복합 적용 예시는 다음과 같다. 전제 없이 “¬(P ∧ ¬P)”(모순률)를 도출하는 증명은 다음과 같다.

1. [P ∧ ¬P]       (가정)
2. P              (1, ∧E₁)
3. ¬P             (1, ∧E₂)
4. ⊥              (2, 3, ⊥I)
5. ¬(P ∧ ¬P)      (1-4, ¬I)

이 증명은 “P ∧ ¬P“를 가정하면 즉시 모순이 도출되므로, 가정을 해소하여 “¬(P ∧ ¬P)“를 결론으로 얻는다. 이 증명은 모순률이 자연 연역 체계에서 형식적으로 증명 가능한 정리임을 보여 준다(Mendelson, 2015).

10. 부정 도입 규칙과 직관주의 논리

부정 도입 규칙은 고전 논리와 직관주의 논리 모두에서 기본 규칙으로 인정된다. 두 논리 체계의 차이는 부정 도입 규칙 자체가 아니라 이중 부정 제거 규칙(“¬¬A로부터 A“의 도출)의 수용 여부에 있다. 고전 논리는 이중 부정 제거를 허용하지만, 직관주의 논리는 이를 일반적으로 허용하지 않는다. 따라서 부정 도입 규칙은 “¬A“를 증명하는 직접적 방법으로 두 체계에서 공통으로 사용된다(Heyting, 1956).

11. 부정 도입 규칙의 학술적 의의

부정 도입 규칙은 다음과 같은 학술적 의의를 가진다. 첫째, 그것은 부정 연결자의 구성 조건을 형식화하며, 부정의 의미를 정의한다. 둘째, 그것은 귀류법을 자연 연역 체계 내에서 형식화한다. 셋째, 그것은 자연 연역 체계에서 가정의 도입과 해소를 활용하는 규칙이다. 넷째, 그것은 부정 제거 규칙과 조화 원리에 의하여 대응하며, 두 규칙이 함께 부정의 의미를 완전히 정의한다. 다섯째, 그것은 고전 논리와 직관주의 논리 모두에서 기본 규칙으로 인정된다(Gentzen, 1935).

12. 본 절의 결론적 정리

부정 도입 규칙은 가정 A 하에서 모순이 도출되었을 때, 가정 A를 해소하고 “¬A“를 결론으로 도출할 수 있음을 규정하는 자연 연역 체계의 기본 규칙이다. 이 규칙은 귀류법의 형식화이며, 모순의 원리와 부정의 진리 함수적 정의에 의하여 정당화된다. 부정 도입 규칙의 적용 시점에서 가정은 해소되며, 결론은 더 이상 그 가정에 의존하지 않는다. 이 규칙은 자연 연역 체계에서 가정의 도입과 해소를 활용하는 규칙이며, 부정 제거 규칙과 함께 부정의 의미를 완전히 정의한다. 학습자는 부정 도입 규칙의 정식화, 역사적 배경, 의미론적 정당화, 적용 방법을 정확히 이해하고, 자연 연역 증명에 활용할 수 있어야 한다.

13. 출처

  • Aristoteles. (trans. 1984). The Complete Works of Aristotle (J. Barnes, Ed.). Princeton: Princeton University Press.
  • 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