11.7 선언 도입 규칙

1. 절의 학술적 목표

본 절은 자연 연역 체계의 선언 도입 규칙(disjunction introduction rule, ∨I)을 학술적으로 검토하는 것을 목표로 한다. 선언 도입 규칙은 한 공식으로부터 그 공식을 성분으로 포함하는 선언을 도출하는 추론 규칙이며, 선언 연결자의 구성 조건을 형식화한다. 본 절은 선언 도입 규칙의 정식화, 의미론적 정당화, 적용, 예시, 특징, 학술적 의의를 체계적으로 정리한다.

2. 선언 도입 규칙의 학술적 정의

선언 도입 규칙은 한 공식 A가 이미 증명되었을 때, 임의의 공식 B에 대하여 선언 “A ∨ B” 또는 “B ∨ A“를 도출할 수 있음을 규정하는 규칙이다. 이 규칙은 선언 연결자 “∨“를 결론에 도입하는 규칙이며, 선언의 구성 조건을 형식화한다. 형식적으로, 선언 도입 규칙은 전제 A로부터 결론 “A ∨ B“로의 이행을 허용한다(Gentzen, 1935).

3. 선언 도입 규칙의 두 형태

선언 도입 규칙은 두 형태를 가진다. 첫째 형태는 A로부터 “A ∨ B“를 도출하는 규칙이고, 둘째 형태는 A로부터 “B ∨ A“를 도출하는 규칙이다. 두 형태는 각각 “∨I₁“과 “∨I₂“로 표기되거나, 단순히 “∨I“라는 이름으로 통합되기도 한다. 두 형태는 모두 타당하며, 도출된 선언에서 전제 A가 좌측에 위치하는지 우측에 위치하는지의 차이만 있다(Prawitz, 1965).

4. 선언 도입 규칙의 표준 표기

선언 도입 규칙의 표준 표기는 다음과 같다.

  A              A
───── (∨I₁)    ───── (∨I₂)
A ∨ B          B ∨ A

가로줄 위의 A는 전제이고, 가로줄 아래의 “A ∨ B” 또는 “B ∨ A“는 결론이다. 여기서 B는 전제에 나타나지 않는 임의의 공식이며, 선언의 반대 성분을 구성한다(Gentzen, 1935).

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

선언 도입 규칙은 선언의 진리 함수적 정의에 의하여 정당화된다. 선언 “A ∨ B“는 A가 참이거나 B가 참일 때 참이다. 따라서 A가 증명되었다면(즉, 참이라고 주장할 수 있다면), B의 진리값과 무관하게 “A ∨ B“도 참이라고 주장할 수 있다. 이러한 정당화는 선언 도입 규칙이 타당한 추론 규칙임을 보장한다. 진리 보존의 관점에서, 전제가 참이면 결론도 반드시 참이다(Mendelson, 2015).

6. 선언 도입 규칙의 단순 적용 예시

선언 도입 규칙의 단순 적용 예시는 다음과 같다. 전제로 “P“가 주어졌을 때, 선언 도입 규칙을 적용하여 “P ∨ Q“를 도출한다.

1. P          (전제)
2. P ∨ Q      (1, ∨I₁)

괄호 안의 “1, ∨I₁“은 결론이 1행에 첫째 형태의 선언 도입 규칙을 적용하여 얻어졌음을 의미한다. 여기서 Q는 임의의 공식이며, 원래 전제에 나타나지 않더라도 결론의 선언 성분으로 도입될 수 있다(Copi, Cohen, & McMahon, 2014).

7. 선언 도입 규칙의 정보 감소성

선언 도입 규칙은 정보 감소적 성격을 지닌다. 전제 A는 A의 구체적 사실을 주장하지만, 결론 “A ∨ B“는 A의 주장과 B의 주장 중 적어도 하나가 참이라는 약한 주장이다. 결론은 전제에 비하여 정보가 더 적으며, 이러한 정보 감소는 선언 도입 규칙의 특징이다. 그러나 이러한 약화는 자연 연역 증명의 다른 단계와 결합되어 유용한 추론을 구성할 수 있다(Prawitz, 1965).

8. 선언 도입 규칙의 복합 적용 예시

선언 도입 규칙의 복합 적용 예시는 다음과 같다. 전제로 “P ∧ Q“가 주어졌을 때, “P ∨ R“을 도출하는 증명은 다음과 같다.

1. P ∧ Q      (전제)
2. P          (1, ∧E₁)
3. P ∨ R      (2, ∨I₁)

이 증명은 연언 제거 규칙과 선언 도입 규칙의 결합을 보여 준다. 먼저 “P ∧ Q“로부터 “P“를 추출한 후, 그 “P“로부터 “P ∨ R“을 도입한다(Mendelson, 2015).

9. 선언 도입 규칙과 교환 법칙

선언 도입 규칙은 두 형태를 통하여 선언의 대칭적 도입을 허용한다. 즉, 전제 A로부터 “A ∨ B“와 “B ∨ A“를 모두 도출할 수 있다. 이 두 결론은 교환 법칙에 의하여 동치이지만, 구문적으로는 서로 다른 공식이다. 선언 도입 규칙의 두 형태는 교환 법칙의 형식적 증명에서 한 성분을 이룬다(Prawitz, 1965).

10. 선언 도입 규칙과 약화

선언 도입 규칙은 “약화(weakening)“의 한 형태로 간주될 수 있다. 약화는 강한 주장으로부터 약한 주장으로의 이행을 의미하며, 선언 도입은 A로부터 “A ∨ B”(더 약한 주장)로의 이행이다. 이러한 약화는 증명의 진행에서 결론의 형태를 조정하는 데 사용된다. 특히, 사례에 따른 증명(proof by cases)에서 선언 도입 규칙은 결론을 공통 형태로 맞추는 역할을 수행한다(Prawitz, 1965).

11. 선언 도입 규칙의 학술적 의의

선언 도입 규칙은 다음과 같은 학술적 의의를 가진다. 첫째, 그것은 선언 연결자의 구성 조건을 형식화하며, 선언의 의미를 부분적으로 정의한다. 둘째, 그것은 자연 연역 체계에서 가장 간단한 규칙 중 하나이지만, 정보 감소적 성격으로 인하여 고유한 특성을 가진다. 셋째, 그것은 조화 원리에 의하여 선언 제거 규칙과 대응하며, 두 규칙이 함께 선언의 의미를 완전히 정의한다. 넷째, 그것은 사례에 따른 증명의 구성에서 결론의 형태를 맞추는 데 사용된다(Gentzen, 1935).

12. 본 절의 결론적 정리

선언 도입 규칙은 한 공식 A로부터 임의의 공식 B에 대하여 “A ∨ B” 또는 “B ∨ A“를 도출할 수 있음을 규정하는 자연 연역 체계의 기본 규칙이다. 이 규칙은 두 형태를 가지며, 선언의 진리 함수적 정의에 의하여 정당화된다. 선언 도입 규칙은 정보 감소적 성격을 지니며, 전제에 비하여 더 약한 주장을 결론으로 도출한다. 이 규칙은 선언 제거 규칙과 조화 원리에 의하여 대응하며, 두 규칙이 함께 선언의 의미를 완전히 정의한다. 선언 도입 규칙은 다른 추론 규칙과 결합되어 복잡한 증명을 구성하는 데 활용된다. 학습자는 선언 도입 규칙의 정식화, 의미론적 정당화, 적용 방법을 정확히 이해하고, 자연 연역 증명에 활용할 수 있어야 한다.

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