에르브랑 구조

1차 논리에서 에르브랑 구조 ${\displaystyle S}$(영어: Herbrand structure)는 어휘 ${\displaystyle \sigma }$(때로는 서명이라고도 함)에 대한 구조로, ${\displaystyle \sigma }$의 통사적 속성에 의해서만 정의된다. 아이디어는 항의 기호 문자열을 값으로 취하는 것이다. 예를 들어, 상수 기호 ${\displaystyle c}$의 표기는 단순히 "${\displaystyle c}$" (기호)이다. 이는 자크 에르브랑의 이름을 따서 명명되었다.

에르브랑 구조는 논리형 프로그래밍의 기초에서 중요한 역할을 한다.^[1]

에르브랑 해석 영역

정의

에르브랑 해석 영역은 에르브랑 구조에서 해석 영역 역할을 한다.

1. 1차 언어 ${\displaystyle L^{\sigma }}$의 에르브랑 해석 영역은 ${\displaystyle L^{\sigma }}$의 모든 바닥항들의 집합이다. 언어에 상수가 없으면, 임의의 새로운 상수를 추가하여 언어를 확장한다.

   • ${\displaystyle \sigma }$가 가산이고 0보다 큰 항수를 가진 함수 기호가 존재하면, 에르브랑 해석 영역은 가산 무한하다.
   • 1차 언어의 맥락에서 우리는 단순히 어휘 ${\displaystyle \sigma }$의 에르브랑 해석 영역이라고도 말한다.
2. 스콜렘 표준형의 닫힌 공식 ${\displaystyle F}$의 에르브랑 해석 영역은 ${\displaystyle F}$의 함수 기호와 상수를 사용하여 구성할 수 있는 모든 변수 없는 항들의 집합이다. ${\displaystyle F}$에 상수가 없으면, 임의의 새로운 상수를 추가하여 ${\displaystyle F}$를 확장한다.

   • 이 두 번째 정의는 계산적 분해 증명의 맥락에서 중요하다.

예시

어휘가 다음과 같은 1차 언어 ${\displaystyle L^{\sigma }}$가 있다고 하자.

• 상수 기호: ${\displaystyle c}$
• 함수 기호: ${\displaystyle f(\cdot ),\,g(\cdot )}$

그러면 ${\displaystyle L^{\sigma }}$ (또는 ${\displaystyle \sigma }$)의 에르브랑 해석 영역 ${\displaystyle H}$는 다음과 같다.

${\displaystyle H=\{c,f(c),g(c),f(f(c)),f(g(c)),g(f(c)),g(g(c)),\dots \}}$

관계 기호는 관계만 포함하는 공식이 해석 영역의 원소에 해당하지 않으므로 에르브랑 해석 영역과는 관련이 없다.^[2]

에르브랑 구조

에르브랑 구조는 에르브랑 해석 영역 위에 항들을 해석한다.

정의

어휘 ${\displaystyle \sigma }$와 해석 영역 ${\displaystyle U}$를 가진 구조 ${\displaystyle S}$가 있다고 하자. ${\displaystyle W}$는 ${\displaystyle \sigma }$에 대한 모든 항들의 집합이고, ${\displaystyle W_{0}}$는 모든 변수 없는 항들의 부분집합이라고 하자. ${\displaystyle S}$가 에르브랑 구조인 것은 다음을 만족할 때이다.

1. ${\displaystyle U=W_{0}}$
2. 모든 ${\displaystyle n}$항 함수 기호 ${\displaystyle f\in \sigma }$와 ${\displaystyle t_{1},\dots ,t_{n}\in W_{0}}$에 대해 ${\displaystyle f^{S}(t_{1},\dots ,t_{n})=f(t_{1},\dots ,t_{n})}$
3. ${\displaystyle \sigma }$의 모든 상수 ${\displaystyle c}$에 대해 ${\displaystyle c^{S}=c}$

비고

1. ${\displaystyle U}$는 ${\displaystyle \sigma }$의 에르브랑 해석 영역이다.
2. 이론 ${\displaystyle T}$의 모형인 에르브랑 구조는 ${\displaystyle T}$의 에르브랑 모형이라고 불린다.

예시

상수 기호 ${\displaystyle c}$와 단항 함수 기호 ${\displaystyle f(\,\cdot \,)}$에 대해 다음 해석을 가진다.

• ${\displaystyle U=\{c,fc,ffc,fffc,\dots \}}$
• ${\displaystyle fc\mapsto fc,ffc\mapsto ffc,\dots }$
• ${\displaystyle c\mapsto c}$

에르브랑 기저

§ 에르브랑 해석 영역에서 정의된 해석 영역과 § 에르브랑 구조에서 정의된 항의 표기 외에, 에르브랑 기저는 관계 기호를 표기함으로써 해석을 완성한다.

정의

에르브랑 구조에 대한 에르브랑 기저 ${\displaystyle {\mathcal {B}}_{H}}$는 인자 항이 에르브랑 해석 영역의 원소인 모든 원자 공식들의 집합이다.

예시

이항 관계 기호 ${\displaystyle R}$에 대해 위의 항들을 사용하면 다음과 같다.

${\displaystyle {\mathcal {B}}_{H}=\{R(c,c),R(fc,c),R(c,fc),R(fc,fc),R(ffc,c),\dots \}}$

같이 보기

• 에르브랑의 정리
• Herbrandization
• 에르브랑 해석