스콜렘 표준형

수리논리학에서 스콜렘 표준형(Skolem normal form)은 보편 양화사만으로 이루어진 프리넥스 표준형 1차 논리식을 가리킨다.

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

개요

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

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

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

역사

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

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

같이 보기

• 프리넥스 표준형
• 양화사
• 자동 정리 증명