에르브랑의 정리(Herbrand's theorem)는 수리논리학(mathematical logic)의 기본적인 결과 가운데 하나로, 프랑스의 논리학자 자크 에르브랑(Jacques Herbrand, 1908–1931)이 1930년 박사 학위 논문에서 제시하였다. 이 정리는 1차 논리(first-order logic)의 특정 부류의 공식을 명제 논리(propositional logic)로 환원할 수 있게 해 주며, 대부분의 자동 정리 증명(automatic theorem proving) 시스템의 논리적 토대를 이룬다.
정리의 내용
에르브랑 정리의 가장 널리 알려진 형태는 존재 양화사(∃)만을 포함하는 프레넥스 정규형(prenex normal form)의 공식에 대한 것이다. 구체적으로, 다음과 같은 공식을 고려한다.
(∃y₁, …, yₙ) F(y₁, …, yₙ)
여기서 F는 양화사를 포함하지 않는(quantifier-free) 1차 논리 공식이며, 추가적인 자유 변수를 포함할 수 있다. 이 버전의 에르브랑 정리는 위 공식이 유효(valid)하기 위한 필요충분조건이, 언어의 확장에서 항(term)들의 유한한 열 tᵢⱼ(1 ≤ i ≤ r, 1 ≤ j ≤ n)이 존재하여 다음 명제 논리식이 유효함을 주장한다.
F(t₁₁, …, t₁ₙ) ∨ … ∨ F(tᵣ₁, …, tᵣₙ)
이 명제 논리식을 해당 공식의 에르브랑 분리(Herbrand disjunction)라고 부른다. 비공식적으로 말하면, 존재 양화사만을 포함하는 프레넥스 형태의 공식 A가 1차 논리에서 증명 가능(유효)한 것은, A의 양화사 없는 하위 공식에 대한 대입 인스턴스(substitution instances)들로 구성된 선언(disjunction)이 명제 논리에서 항진식(tautology)일 때, 그리고 그때에만 성립한다.
일반성의 제한
존재 양화사만을 포함하는 프레넥스 형태로의 제한은 정리의 일반성을 제한하지 않는다. 임의의 1차 논리 공식은 프레넥스 형태로 변환될 수 있으며, 보편 양화사(∀)는 에르브랑화(Herbrandization)라는 과정을 통해 제거될 수 있기 때문이다. 에르브랑은 원래 1차 논리의 임의의 공식에 대해 이 정리를 증명하였으나, 위에 제시된 단순화된 버전이 더 널리 사용되고 있다.
증명 개요
정리의 비자명한 방향(유효성 → 에르브랑 분리의 존재)에 대한 증명은 다음과 같은 단계로 구성될 수 있다. 먼저 공식이 유효하다면, 겐첸(Gentzen)의 컷 제거 정리(cut-elimination theorem)에서 비롯된 컷 없는 시퀀트 계산(cut-free sequent calculus)의 완전성에 의해 컷 없는 증명이 존재한다. 그다음 잎(leaf)에서부터 아래로 작업하며 존재 양화사를 도입하는 추론을 제거하고, 이전에 양화된 공식에 대한 수축(contraction) 추론을 제거한다. 수축 제거는 시퀀트의 오른쪽에 F의 모든 관련 치환 인스턴스를 누적시켜, 결과적으로 ⊢ F(t₁₁, …, t₁ₙ), …, F(tᵣ₁, …, tᵣₙ)의 증명을 산출하며, 이로부터 에르브랑 분리를 얻을 수 있다. 단, 에르브랑의 원래 증명 당시에는 시퀀트 계산과 컷 제거 정리가 알려져 있지 않았으므로, 그는 더 복잡한 방법으로 정리를 증명해야 했다.
일반화
에르브랑 정리는 확장 트리 증명(expansion-tree proof)을 사용하여 고차 논리(higher-order logic)로 확장되었다. 또한 에르브랑 분리와 확장 트리 증명은 컷(cut)의 개념으로 확장되었으며, 에르브랑 분리는 에르브랑 시퀀트(Herbrand sequent)로 일반화되었다.
관련 개념
에르브랑 정리와 밀접하게 연관된 개념으로는 에르브랑 구조(Herbrand structure), 에르브랑 해석(Herbrand interpretation), 에르브랑 우주(Herbrand universe) 등이 있으며, 이들은 모두 자크 에르브랑의 이름을 따서 명명되었다. 에르브랑 정리는 또한 콤팩트성 정리(compactness theorem)와도 관련이 있다.
