프리넥스 표준형(Prenex normal form)은 수리논리학에서 사용되는 1차 논리 공식의 표준형 중 하나로, 모든 한정 기호(전칭 기호 ∀, 존재 기호 ∃)가 공식의 가장 앞부분에 위치하고 그 뒤에 한정 기호를 포함하지 않는 부분(매트릭스)이 오는 형태를 말한다.
정의
프리넥스 표준형인 1차 술어 논리 공식은 다음과 같은 구조로 이루어진다.
$$ \phi = \phi_{\text{prefix}} ; \phi_{\text{matrix}} $$
- 접두사(prefix): 기호 ∃와 ∀ 및 변수만을 포함하는 문자열이다. 논리곱(∧)이나 등호(=) 등 다른 연산이나 관계 기호는 포함되지 않는다.
- 매트릭스(matrix): 기호 ∀를 포함하지 않는 문자열이다. 변수와 부정(¬), 논리곱(∧), 등호(=) 및 기타 연산·관계 기호만으로 구성된다.
변환 알고리즘
모든 1차 논리 공식은 프리넥스 표준형인 명제와 동치이며, 주어진 공식과 동치인 프리넥스 표준형은 다음과 같은 과정을 통해 구할 수 있다. 편의상 모든 논리합(∨)이나 함의(⇒)는 논리곱(∧) 및 부정(¬)으로 먼저 나타낸다.
- $( \forall x : \phi ) \land \psi$ → $\forall x' : ( \phi[x'/x] \land \psi )$
(단, $x'$은 $\psi$에 포함되지 않는 임의의 변수) - $( \exists x : \phi ) \land \psi$ → $\exists x' : ( \phi[x'/x] \land \psi )$
(단, $x'$은 $\psi$에 포함되지 않는 임의의 변수) - $\lnot \exists x : \phi$ → $\forall x : \lnot \phi$
- $\lnot \forall x : \phi$ → $\exists x : \lnot \phi$
이 변환을 반복 적용하면 모든 한정 기호를 공식의 앞부분으로 끌어낼 수 있다.
역사와 어원
"프리넥스"(prenex)라는 용어는 라틴어 praenexus(묶인, 고정된)에서 유래하였다. 이 용어는 다비트 힐베르트(David Hilbert)와 파울 베르나이스(Paul Bernays)가 1938년에 저술한 《수학의 기초》(Grundlagen der Mathematik)에서 최초로 사용되었다.
활용
프리넥스 표준형은 1차 논리 공식을 분석하거나 증명 이론에서 공식을 표준화하는 데 사용된다. 특히 모든 한정 기호가 전칭 기호(∀)만으로 이루어진 프리넥스 표준형을 스콜렘 표준형(Skolem normal form)이라고 하며, 이는 자동 정리 증명 및 논리 프로그래밍 분야에서 중요하게 활용된다.
