11.15 가정의 도입과 해소

11.15 가정의 도입과 해소

1. 절의 학술적 목표

본 절은 자연 연역 체계에서 가정(assumption)의 도입(introduction)과 해소(discharge)의 메커니즘을 학술적으로 검토하는 것을 목표로 한다. 가정의 도입과 해소는 자연 연역 체계의 가장 특징적인 장치이며, 조건 도입 규칙, 부정 도입 규칙, 선언 제거 규칙 등 여러 규칙의 작동 방식을 결정한다. 본 절은 가정의 개념, 도입의 형식, 해소의 조건, 의존성 관리, 범위 표기, 예시, 학술적 의의를 체계적으로 정리한다.

2. 가정의 학술적 정의

가정이란 자연 연역 증명의 한 단계에서 일시적으로 도입되어 증명의 특정 범위 내에서만 유효한 공식을 의미한다. 가정은 전제(premise)와 구별되며, 전제는 증명 전체에 걸쳐 유효한 반면 가정은 일시적 범위 내에서만 유효하다. 가정은 “만약 A가 참이라면“이라는 형식의 가설적 추론을 형식화하기 위한 장치이며, 자연 연역 체계가 실제 수학적 추론을 반영하는 핵심 요소이다(Gentzen, 1935).

3. 가정의 도입 형식

가정의 도입은 자연 연역 증명의 임의의 시점에서 이루어질 수 있다. 가정이 도입될 때, 가정은 대괄호 “[A]” 또는 별도의 블록 구조로 표시되어 일반 전제 및 도출과 시각적으로 구별된다. 가정의 도입은 특정 규칙(예를 들어 조건 도입 규칙, 부정 도입 규칙, 선언 제거 규칙)의 적용을 준비하는 단계로 이루어지며, 가정이 도입되면 그 가정을 사용한 모든 후속 도출은 그 가정에 의존한다(Prawitz, 1965).

4. 가정의 해소 형식

가정의 해소는 특정 추론 규칙의 적용 시점에서 이루어진다. 해소는 가정을 증명에서 제거하는 것이 아니라, 결론이 더 이상 그 가정에 의존하지 않음을 선언하는 절차이다. 해소된 가정은 시각적으로 대괄호 “[A]“로 표시되거나 블록의 닫힘으로 표현되며, 해소된 가정은 이후의 도출에서 사용될 수 없다. 가정의 해소는 조건 도입 규칙, 부정 도입 규칙, 선언 제거 규칙 등에서 이루어진다(Gentzen, 1935).

5. 가정 해소의 조건

가정의 해소는 특정 조건 하에서만 허용된다. 첫째, 해소는 해당 가정을 도입할 때 지정된 규칙의 적용 시점에서만 이루어져야 한다. 둘째, 해소된 가정은 그 이전에 도출된 공식에 영향을 미치지 않으며, 결론은 해소 이후에 더 이상 그 가정에 의존하지 않는다. 셋째, 중첩된 가정은 올바른 순서로 해소되어야 하며, 일반적으로 내부 가정이 외부 가정보다 먼저 해소된다. 이러한 조건은 자연 연역 증명의 논리적 의존성을 정확히 관리하기 위한 것이다(Prawitz, 1965).

6. 가정의 의존성 관리

자연 연역 증명의 각 단계는 그 단계에서 활성화된 가정의 집합에 의존한다. 이 의존성은 증명의 논리적 구조를 결정하며, 결론이 어떤 가정 하에서 도출되었는지를 명시한다. 가정이 해소되면 결론의 의존성 집합에서 그 가정이 제거된다. 자연 연역 체계의 설계는 이러한 의존성을 정확히 추적하기 위한 표기 규약(대괄호, 블록 구조, 의존성 목록)을 채택한다. 의존성 관리의 정확성은 증명의 타당성을 보장하는 핵심 요소이다(Prawitz, 1965).

7. 가정의 범위 표기

가정의 범위는 자연 연역 체계의 설계에 따라 여러 방식으로 표기된다. 첫째, 대괄호 방식은 가정을 “[A]“로 표시하고 해소 시점에서 대괄호를 닫는 방식이다. 둘째, 블록 방식(플래그 표기, Jaśkowski의 표기)은 가정의 범위를 수직선 또는 들여쓰기로 구분된 블록으로 표시하는 방식이다. 셋째, 의존성 목록 방식은 각 도출 단계에 그 단계가 의존하는 가정의 번호 목록을 명시하는 방식이다. 세 방식은 모두 가정의 범위를 정확히 관리하며, 체계의 설계에 따라 선택된다(Jaśkowski, 1934).

8. 가정의 도입과 해소의 단순 예시

가정의 도입과 해소의 단순 예시는 다음과 같다. 전제 없이 “P → P“를 도출하는 증명은 다음과 같다.

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

이 증명에서 1행의 P는 가정으로 도입되고, 3행의 조건 도입 규칙 적용 시점에서 해소된다. 해소 이후 3행의 결론 “P → P“는 더 이상 가정 P에 의존하지 않으며, 전제 없이 증명 가능한 정리이다. 이 예시는 가정의 도입과 해소의 가장 단순한 형태를 보여 준다(Copi, Cohen, & McMahon, 2014).

9. 중첩된 가정의 도입과 해소

가정은 중첩되어 도입될 수 있다. 중첩된 가정의 도입과 해소의 예시는 다음과 같다. “P → (Q → P)“의 증명은 다음과 같다.

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

이 증명에서 1행의 P와 2행의 Q는 중첩된 가정이며, 4행에서 내부 가정 Q가 먼저 해소되고, 5행에서 외부 가정 P가 해소된다. 중첩된 가정의 해소는 내부부터 외부로의 순서로 이루어져야 한다(Mendelson, 2015).

10. 가정의 도입과 해소의 다양한 규칙에서의 역할

가정의 도입과 해소는 여러 추론 규칙에서 사용된다. 조건 도입 규칙은 가정 A 하에서 B가 도출되면 가정 A를 해소하고 “A → B“를 결론으로 도출한다. 부정 도입 규칙은 가정 A 하에서 모순이 도출되면 가정 A를 해소하고 “¬A“를 결론으로 도출한다. 선언 제거 규칙은 두 개의 가정 A와 B 하에서 각각 동일한 결론 C가 도출되면 두 가정을 해소하고 C를 결론으로 도출한다. 이러한 규칙들은 가정의 도입과 해소를 공통된 메커니즘으로 활용한다(Gentzen, 1935).

11. 가정의 도입과 해소의 학술적 의의

가정의 도입과 해소는 다음과 같은 학술적 의의를 가진다. 첫째, 그것은 자연 연역 체계를 공리 체계와 구별하는 가장 특징적인 장치이다. 둘째, 그것은 가설적 추론과 조건부 증명을 형식화하며, 실제 수학적 추론의 구조를 반영한다. 셋째, 그것은 증명의 논리적 의존성을 정확히 관리하는 메커니즘을 제공한다. 넷째, 그것은 조건 도입 규칙, 부정 도입 규칙, 선언 제거 규칙의 작동을 가능하게 한다. 다섯째, 그것은 연역 정리를 기본 규칙으로 내장함으로써 공리 체계의 간접적 접근을 피한다(Prawitz, 1965).

12. 본 절의 결론적 정리

가정의 도입과 해소는 자연 연역 체계에서 일시적으로 도입되어 특정 범위 내에서만 유효한 공식을 관리하는 메커니즘이다. 가정의 도입은 증명의 임의의 시점에서 이루어질 수 있으며, 가정의 해소는 조건 도입 규칙, 부정 도입 규칙, 선언 제거 규칙과 같은 특정 규칙의 적용 시점에서 이루어진다. 해소된 가정은 결론의 의존성에서 제거되며, 결론은 더 이상 그 가정에 의존하지 않는다. 자연 연역 체계는 대괄호 방식, 블록 방식, 의존성 목록 방식 등을 통하여 가정의 범위를 표기한다. 가정의 도입과 해소는 자연 연역 체계의 가장 특징적인 장치이며, 가설적 추론과 조건부 증명을 형식화한다. 학습자는 가정의 개념, 도입과 해소의 형식, 해소의 조건, 의존성 관리, 범위 표기를 정확히 이해하고, 자연 연역 증명에 활용할 수 있어야 한다.

13. 출처

  • Gentzen, G. (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift, 39, 176–210, 405–431.
  • Jaśkowski, S. (1934). On the rules of suppositions in formal logic. Studia Logica, 1, 5–32.
  • 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