에르브랑의 정리

에르브랑의 정리(Herbrand's theorem)는 자크 에르브랑이 1930년에 발표한 수리논리학의 근본적인 결과이다.^[1] 본질적으로 1차 논리를 명제 논리로 특정 유형의 환원을 가능하게 한다. 에르브랑 정리는 대부분의 자동 정리 증명기의 논리적 기초이다. 에르브랑은 원래 1차 논리의 임의의 공식에 대해 자신의 정리를 증명했지만^[2] 여기 제시된 더 간단한 버전은 프레넥스 형식으로 된 존재 기호만을 포함하는 공식으로 제한되어 더 인기를 얻었다.

서술

다음과 같은 1차 논리 공식이 있다고 하자.

${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$

여기서 ${\displaystyle F(y_{1},\ldots ,y_{n})}$는 양화사(quantifier)가 없는 식이지만, 추가적인 자유 변수를 포함할 수 있다. 에르브랑 정리의 이 버전은 위 공식이 타당한 것은 다음과 같은 유한한 항열 ${\displaystyle t_{ij}}$가 존재하는 경우에만 해당된다는 것을 진술한다. 이 항열은 언어의 확장 안에 있을 수 있으며,

${\displaystyle 1\leq i\leq r}$ 및 ${\displaystyle 1\leq j\leq n}$,

다음과 같은 조건이 충족된다:

${\displaystyle F(t_{11},\ldots ,t_{1n})\vee \ldots \vee F(t_{r1},\ldots ,t_{rn})}$

이 타당하다. 만약 타당하다면, 이를 다음의 에르브랑 분리합이라고 부른다.

${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n}).}$

비공식적으로: 존재 양화사만을 포함하는 프레넥스 형식의 공식 ${\displaystyle A}$가 1차 논리에서 증명 가능(타당)한 것은 ${\displaystyle A}$의 양화사 없는 하위 공식의 치환 인스턴스로 구성된 분리합이 항진식 (명제적으로 도출 가능)인 경우에만 해당된다.

존재 양화사만을 포함하는 프레넥스 형식의 공식으로 제한하는 것은 정리의 일반성을 제한하지 않는다. 공식은 프레넥스 형식으로 변환될 수 있고, 보편 양화사는 에르브랑화를 통해 제거될 수 있기 때문이다. 구조적 에르브랑화를 수행하면 프레넥스 형식으로의 변환을 피할 수 있다. 에르브랑 분리합에 허용되는 변수 의존성에 추가적인 제한을 가함으로써 에르브랑화를 피할 수도 있다.

증명 스케치

정리의 비자명한 방향에 대한 증명은 다음 단계에 따라 구성될 수 있다:

1. 공식 ${\displaystyle (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$가 타당하다면, 겐첸의 자름-제거 정리에서 비롯되는 시퀀트 계산의 자름 없는 완전성에 의해, ${\displaystyle \vdash (\exists y_{1},\ldots ,y_{n})F(y_{1},\ldots ,y_{n})}$의 자름 없는 증명이 존재한다.
2. 리프에서 시작하여 아래로 내려가면서 존재 양화사를 도입하는 추론을 제거한다.
3. 이전에 존재적으로 양화된 공식에 대한 수축 추론을 제거한다. 양화사 추론이 제거된 후, (이제 이전에 양화된 변수에 대해 항이 대입된) 공식들이 더 이상 동일하지 않을 수 있기 때문이다.
4. 수축 제거는 ${\displaystyle F(y_{1},\ldots ,y_{n})}$의 모든 관련 치환 인스턴스를 시퀀트의 오른쪽에 축적하여 ${\displaystyle \vdash F(t_{11},\ldots ,t_{1n}),\ldots ,F(t_{r1},\ldots ,t_{rn})}$의 증명을 초래하며, 여기서 에르브랑 분리합을 얻을 수 있다.

그러나 에르브랑이 증명을 하던 당시에는 시퀀트 계산과 자름-제거가 알려지지 않았기 때문에, 에르브랑은 더 복잡한 방식으로 자신의 정리를 증명해야 했다.

에르브랑 정리의 일반화

• 에르브랑 정리는 확장 트리 증명을 사용하여 고차 논리로 확장되었다.^[3] 확장 트리 증명의 심층 표현은 1차 논리로 제한될 때 에르브랑 분리합에 해당한다.
• 에르브랑 분리합과 확장 트리 증명은 자름 개념으로 확장되었다. 자름-제거의 복잡성 때문에, 자름을 포함하는 에르브랑 분리합은 표준 에르브랑 분리합보다 비초등적으로 작을 수 있다.
• 에르브랑 분리합은 에르브랑 시퀀스로 일반화되었으며, 에르브랑 정리를 시퀀스에 대해 진술할 수 있게 한다: "스콜렘화된 시퀀스가 파생될 수 있는 것은 에르브랑 시퀀스를 가질 때에만 가능하다."

같이 보기

• 에르브랑 구조
• 에르브랑 해석
• 에르브랑 유니버스
• 콤팩트성 정리