스콜렘 표준형 문서 원본 보기

{{위키데이터 속성 추적}}
[[수리논리학]]에서 '''스콜렘 표준형'''(Skolem normal form)은 [[보편 양화사]]만으로 이루어진 [[프리넥스 표준형]] 1차 논리식을 가리킨다.

모든 1차 논리식들은 '''스콜렘화'''(Skolemization)라는 과정을 통해 그 충족가능성(satisfiability)을 변화시키지 않은 채 스콜렘 표준형으로 변환될 수 있다. 여기서 결과의 논리식이 반드시 원래의 식과 [[동치]]인 것은 아니나, 서로 모델론적으로는 일치한다: 곧, 어느 한 쪽이 충족가능하다는 것과 다른 쪽이 충족가능하다는 것이 동치이다. 스콜렘화는 논리적 진술로부터 [[존재 양화사]]를 모두 제거해나가는 방식으로 이루어진다.

== 개요 ==
우선 보편양화사의 범위에 들어가있지 않은 존재양화된 변수들을 새로운 상항을 도입함으로써 치환하는 것은 간단하게 생각할 수 있다. 예컨대 <math>\exists x P(x)</math>를 <math>P(c)</math>로 치환하며, 여기서 c는 나타난적 없는 새로운 상수여야 한다.

더 일반화하여 모든 존재양화된 변수들을 제거한다. y를 새로운 항 <math>f(x_1, ..., x_n)</math>로 치환할 수 있으며 여기서 f는 새로운 함수기호이다. 식이 프리넥스 표준형이므로 <math>x_1, ..., x_n</math>를 양화하는 보편양화사들 뒤에 y를 양화하는 양화사가 온다. (귀납법적으로) <math>x_1, ..., x_n</math> 등은 모두 보편양화되어 있다고 가정하면 이와 같이 y를 양화하는 존재양화사를 제거하고, 이러한 과정을 반복할 수 있다. 이때 이러한 함수 f를 '''스콜렘 함수'''라 한다.

[[2차 논리]]의 시점에서 보면 스콜렘화는 그러한 y의 존재와 적절한 함수 f의 존재가 동치인 것으로부터 성립하는 원리이다. 곧 <math>\forall x \exists y . R(x,y)</math>와 <math>\exists f \forall x . R(x,f(x))</math>의 동치를 이른다. 혹은 메타적 시점에서 모델의 존재와의 동치성으로도 볼 수 있다. 그러나 1차 논리에서 이는 모델론적 수단을 통해 간접적으로 이루어지며 따라서 충족가능성은 보존되나 동치성은 보장되지 않는다.

== 역사 ==
노르웨이의 수학자 [[토랄프 스콜렘]]의 이름을 따온 것이다.

한편 스콜렘화의 쌍대로서, [[자크 에르브랑]]의 에르브랑화(Herbrandization)가 있는데 이는 충족가능성은 보존하지 않으나 타당성은 보존한다.

== 같이 보기 ==
* [[프리넥스 표준형]]
* [[양화사]]
* [[자동 정리 증명]]

== 각주 ==
{{각주}}

{{토막글|수학}}

[[분류:모형 이론]]
[[분류:술어 논리]]