11.9 조건 도입 규칙

1. 절의 학술적 목표

본 절은 자연 연역 체계의 조건 도입 규칙(conditional introduction rule, →I)을 학술적으로 검토하는 것을 목표로 한다. 조건 도입 규칙은 가정으로부터 결론의 도출을 조건 공식으로 전환하는 추론 규칙이며, 자연 연역 체계에서 가정의 해소와 조건의 구성을 연결하는 핵심 규칙이다. 본 절은 조건 도입 규칙의 정식화, 의미론적 정당화, 가정의 해소, 적용, 예시, 학술적 의의를 체계적으로 정리한다.

2. 조건 도입 규칙의 학술적 정의

조건 도입 규칙은 가정 A 하에서 공식 B가 도출되었을 때, 가정 A를 해소하고 조건 “A → B“를 결론으로 도출할 수 있음을 규정하는 규칙이다. 이 규칙은 조건 연결자 “→“를 결론에 도입하는 규칙이며, 조건부 증명(conditional proof)의 형식화이다. 조건 도입 규칙은 자연 연역 체계에서 가정의 도입과 해소를 가장 직접적으로 활용하는 규칙 중 하나이다(Gentzen, 1935).

3. 조건 도입 규칙의 표준 표기

조건 도입 규칙의 표준 표기는 다음과 같다.

[A]
 ⋮
 B
───── (→I)
A → B

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

4. 조건 도입 규칙의 의미론적 정당화

조건 도입 규칙은 조건의 진리 함수적 정의와 연역 정리(deduction theorem)에 의하여 정당화된다. 조건 “A → B“는 A가 참이면 B도 참임을 주장한다. 따라서 A를 가정하여 B를 도출할 수 있다면, “A → B“가 성립한다고 결론지을 수 있다. 이러한 정당화는 의미론적으로 타당하며, 조건부 증명의 원리를 형식화한다(Mendelson, 2015).

5. 조건 도입 규칙과 조건부 증명

조건 도입 규칙은 조건부 증명의 형식화이다. 조건부 증명은 “A를 가정하면 B가 도출되므로, A이면 B이다“라는 형식의 추론이며, 수학적 증명에서 매우 흔히 사용된다. 자연 연역 체계는 이러한 조건부 증명을 가정의 도입과 해소를 통하여 형식적으로 체계화한다. 조건 도입 규칙은 자연 연역이 실제 수학적 추론에 가까움을 보여 주는 대표적 사례이다(Prawitz, 1965).

6. 조건 도입 규칙에서의 가정의 해소

조건 도입 규칙의 적용 시점에서 가정 A는 해소된다. 해소 이전에 A는 증명의 특정 범위 내에서 활성화되어 있으며, 그 범위 내의 모든 도출은 A에 의존한다. 해소 이후에 A는 더 이상 활성화되지 않으며, 결론 “A → B“는 A에 의존하지 않는다. 이러한 해소의 메커니즘은 증명의 논리적 의존성을 관리하는 중요한 장치이다. 해소된 가정의 범위는 일반적으로 대괄호나 블록 구조로 명시된다(Prawitz, 1965).

7. 조건 도입 규칙의 단순 적용 예시

조건 도입 규칙의 단순 적용 예시는 다음과 같다. 전제 없이 “P → P“를 도출하는 증명은 다음과 같다.

1. [P]        (가정)
2. P          (1, 반복)
3. P → P      (1-2, →I)

이 증명은 P를 가정하면 즉시 P가 도출되므로, 가정 P를 해소하고 “P → P“를 결론으로 얻는다. 이 증명은 조건 도입 규칙이 어떻게 가정에서 결론으로 이동하는지를 가장 단순한 형태로 보여 준다(Copi, Cohen, & McMahon, 2014).

8. 조건 도입 규칙의 복합 적용 예시

조건 도입 규칙의 복합 적용 예시는 다음과 같다. 전제로 “P → (Q → R)“이 주어졌을 때, “(P ∧ Q) → R“을 도출하는 증명은 다음과 같다.

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

이 증명은 조건 도입 규칙, 연언 제거 규칙, 조건 제거 규칙의 결합을 보여 준다. 가정 “P ∧ Q“의 도입으로부터 R이 도출되고, 가정의 해소로 “(P ∧ Q) → R“이 결론으로 얻어진다(Mendelson, 2015).

9. 조건 도입 규칙과 연역 정리

조건 도입 규칙은 연역 정리와 밀접한 관계를 가진다. 연역 정리는 “가정의 집합 Γ ∪ {A}로부터 B가 증명 가능하면, Γ로부터 A → B가 증명 가능하다“는 메타정리이다. 공리 체계에서 연역 정리는 증명 이론의 중요한 결과로 유도되지만, 자연 연역 체계에서는 조건 도입 규칙이 연역 정리를 기본 규칙으로 직접 내장한다. 이러한 차이는 자연 연역이 조건 증명을 형식화하는 데 더 적합함을 보여 준다(Prawitz, 1965).

10. 조건 도입 규칙의 중첩 적용

조건 도입 규칙은 중첩되어 적용될 수 있다. 예를 들어 “P → (Q → P)“의 증명은 다음과 같다.

1. [P]            (가정)
2. [Q]            (가정)
3. P              (1, 반복)
4. Q → P          (2-3, →I)
5. P → (Q → P)    (1-4, →I)

이 증명은 두 개의 가정 P와 Q가 중첩되어 도입되고, 두 번의 조건 도입 규칙의 적용으로 해소되는 방식을 보여 준다. 중첩된 가정의 해소는 올바른 순서(내부 가정 먼저, 외부 가정 나중)로 이루어져야 한다(Copi, Cohen, & McMahon, 2014).

11. 조건 도입 규칙의 학술적 의의

조건 도입 규칙은 다음과 같은 학술적 의의를 가진다. 첫째, 그것은 조건 연결자의 구성 조건을 형식화하며, 조건의 의미를 정의한다. 둘째, 그것은 조건부 증명의 원리를 형식적으로 체계화한다. 셋째, 그것은 자연 연역 체계에서 가정의 도입과 해소를 활용하는 대표적 규칙이다. 넷째, 그것은 연역 정리를 기본 규칙으로 내장함으로써 공리 체계의 간접적 접근을 피한다. 다섯째, 그것은 조건 제거 규칙과 조화 원리에 의하여 대응하며, 두 규칙이 함께 조건의 의미를 완전히 정의한다(Gentzen, 1935).

12. 본 절의 결론적 정리

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

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