11.8 선언 제거 규칙

11.8 선언 제거 규칙

1. 절의 학술적 목표

본 절은 자연 연역 체계의 선언 제거 규칙(disjunction elimination rule, ∨E)을 학술적으로 검토하는 것을 목표로 한다. 선언 제거 규칙은 선언 공식으로부터 결론을 도출하는 추론 규칙이며, 사례에 따른 증명(proof by cases)의 형식화이다. 본 절은 선언 제거 규칙의 정식화, 의미론적 정당화, 구조, 적용, 예시, 학술적 의의를 체계적으로 정리한다.

2. 선언 제거 규칙의 학술적 정의

선언 제거 규칙은 선언 “A ∨ B“가 증명되었고, A로부터 C가 도출되며, B로부터 C가 도출될 때, C를 결론으로 도출할 수 있음을 규정하는 규칙이다. 이 규칙은 선언 연결자 “∨“를 전제에서 제거하여 공통의 결론 C를 얻는 규칙이며, 사례에 따른 증명의 형식화이다. 선언 제거 규칙은 자연 연역 체계에서 가정의 도입과 해소를 포함하는 대표적 규칙이다(Gentzen, 1935).

3. 선언 제거 규칙의 표준 표기

선언 제거 규칙의 표준 표기는 다음과 같다.

             [A]    [B]
              ⋮      ⋮
A ∨ B         C      C
─────────────────────── (∨E)
           C

여기서 “A ∨ B“는 주어진 전제이고, 대괄호 안의 A와 B는 각각 일시적으로 도입된 가정이다. 각 가정으로부터 공통의 결론 C가 도출되며, 최종 결론 C는 두 가정이 해소된 후에 얻어진다. 이 표기는 겐첸의 자연 연역 체계의 표준 형식이다(Gentzen, 1935).

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

선언 제거 규칙은 선언의 진리 함수적 정의와 사례 분석의 원리에 의하여 정당화된다. 선언 “A ∨ B“가 참이면 A가 참이거나 B가 참(혹은 둘 다)이다. 만약 A가 참인 경우에도 C가 성립하고, B가 참인 경우에도 C가 성립한다면, 어느 경우든 C가 성립한다. 따라서 “A ∨ B“와 두 사례에서의 C의 도출이 주어지면 C가 결론으로 도출된다. 이러한 정당화는 선언 제거 규칙이 타당한 추론 규칙임을 보장한다(Mendelson, 2015).

5. 사례에 따른 증명으로서의 선언 제거

선언 제거 규칙은 사례에 따른 증명의 형식화이다. 수학과 일상적 추론에서 “A 또는 B이다. 만약 A라면 C이다. 만약 B라도 C이다. 따라서 C이다“라는 형식의 추론은 매우 흔하다. 이러한 추론 방식을 자연 연역에서 형식적으로 체계화한 것이 선언 제거 규칙이다. 이 규칙은 경우를 나누어 각 경우에서 동일한 결론을 도출한 후, 그 공통 결론을 주장하는 방법을 제공한다(Prawitz, 1965).

6. 선언 제거 규칙의 구조적 복잡성

선언 제거 규칙은 다른 제거 규칙들에 비하여 구조적으로 더 복잡하다. 그 이유는 두 개의 부수적 증명(A로부터 C의 도출과 B로부터 C의 도출)을 포함하며, 가정의 도입과 해소가 필요하기 때문이다. 이러한 구조적 복잡성은 선언 연결자의 의미(불확정적 선택 또는 둘 중 하나)를 반영하며, 선언의 사용이 연언의 사용보다 더 간접적임을 보여 준다(Gentzen, 1935).

7. 선언 제거 규칙의 단순 적용 예시

선언 제거 규칙의 단순 적용 예시는 다음과 같다. 전제로 “P ∨ Q”, “P → R”, “Q → R“이 주어졌을 때, “R“을 도출하는 증명은 다음과 같다.

1. P ∨ Q          (전제)
2. P → R          (전제)
3. Q → R          (전제)
4. [P]            (가정)
5. R              (2, 4, →E)
6. [Q]            (가정)
7. R              (3, 6, →E)
8. R              (1, 4-5, 6-7, ∨E)

이 증명은 “P ∨ Q“의 각 사례(P와 Q)에서 R을 도출한 후, 선언 제거 규칙을 적용하여 R을 최종 결론으로 얻는다(Copi, Cohen, & McMahon, 2014).

8. 선언 제거 규칙과 가정의 해소

선언 제거 규칙의 중요한 특징은 가정의 해소이다. 증명 중에 일시적으로 도입된 가정 A와 B는 선언 제거 규칙의 적용 시점에서 해소되며, 최종 결론 C는 이 두 가정에 의존하지 않는다. 가정의 해소는 자연 연역 체계에서 증명의 의존성을 관리하는 중요한 장치이며, 증명의 최종 결론이 어떤 가정에 의존하는지를 명확히 한다(Prawitz, 1965).

9. 선언 제거 규칙과 교환 법칙

선언 제거 규칙은 선언의 교환 법칙의 자연 연역 증명에 사용된다. 전제로 “P ∨ Q“가 주어졌을 때, “Q ∨ P“를 도출하는 증명은 다음과 같다.

1. P ∨ Q          (전제)
2. [P]            (가정)
3. Q ∨ P          (2, ∨I₂)
4. [Q]            (가정)
5. Q ∨ P          (4, ∨I₁)
6. Q ∨ P          (1, 2-3, 4-5, ∨E)

이 증명은 선언 제거 규칙과 선언 도입 규칙의 결합으로 교환 법칙을 형식적으로 증명한다(Mendelson, 2015).

10. 선언 제거 규칙의 일반화

선언 제거 규칙은 세 개 이상의 성분을 가진 선언에 대해서도 일반화될 수 있다. “A₁ ∨ A₂ ∨ … ∨ Aₙ“에 대하여, 각 Aᵢ로부터 공통의 결론 C가 도출되면 C를 결론으로 얻을 수 있다. 이러한 일반화는 결합 법칙과 함께 사용되면 여러 사례를 나누는 증명에 편리하다. 일반화된 형태는 원시 규칙의 반복적 적용으로 환원된다(Prawitz, 1965).

11. 선언 제거 규칙의 학술적 의의

선언 제거 규칙은 다음과 같은 학술적 의의를 가진다. 첫째, 그것은 선언 연결자의 분해 조건을 형식화하며, 선언 도입 규칙과 함께 선언의 의미를 완전히 정의한다. 둘째, 그것은 사례에 따른 증명 방식을 형식적으로 체계화한다. 셋째, 그것은 자연 연역 체계에서 가정의 도입과 해소를 활용하는 대표적 규칙이다. 넷째, 그것은 조화 원리에 의하여 선언 도입 규칙과 대응하며, 정상화 정리의 환원 단계에서 중요한 역할을 한다(Gentzen, 1935).

12. 본 절의 결론적 정리

선언 제거 규칙은 선언 “A ∨ B”, A로부터 C의 도출, B로부터 C의 도출이 주어졌을 때 C를 결론으로 도출할 수 있음을 규정하는 자연 연역 체계의 기본 규칙이다. 이 규칙은 사례에 따른 증명의 형식화이며, 선언의 진리 함수적 정의와 사례 분석의 원리에 의하여 정당화된다. 선언 제거 규칙은 가정의 도입과 해소를 포함하여 구조적으로 복잡하지만, 선언 연결자의 사용 방법을 명확히 규정한다. 이 규칙은 선언 도입 규칙과 조화 원리에 의하여 대응하며, 두 규칙이 함께 선언의 의미를 완전히 정의한다. 학습자는 선언 제거 규칙의 정식화, 의미론적 정당화, 구조, 적용 방법을 정확히 이해하고, 자연 연역 증명에 활용할 수 있어야 한다.

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