프리넥스 표준형

수리논리학에서 프리넥스 표준형(prenex標準型, 영어: prenex normal form)은 모든 한정 기호가 앞에 와 있는 1차 논리 공식의 형태이다.

정의

프리넥스 표준형인 1차 술어 논리 공식은 다음과 같은 형태의 공식 ${\displaystyle \phi }$이다.

${\displaystyle \phi =\phi _{\text{prefix}}\phi _{\text{matrix}}}$

여기서

• ${\displaystyle \phi _{\text{prefix}}}$는 기호 ${\displaystyle \exists }$와 ${\displaystyle \forall }$ 및 변수만을 포함하는 문자열이다. 특히, ${\displaystyle \land }$나 ${\displaystyle =}$ 및 기타 연산·관계를 포함하지 않는다. 이를 ${\displaystyle \phi }$의 접두사(영어: prefix 프리픽스^[*])라고 한다.
• ${\displaystyle \phi _{\text{matrix}}}$는 기호 ${\displaystyle \forall }$을 포함하지 않는 문자열이다. 즉, 변수와 ${\displaystyle \lnot }$, ${\displaystyle \land }$, ${\displaystyle =}$ 및 기타 연산·관계만으로 구성된다. 이를 ${\displaystyle \phi }$의 매트릭스(영어: matrix)라고 한다.

알고리즘

모든 1차 논리 공식은 프리넥스 표준형인 명제와 동치이며, 주어진 공식과 동치인 프리넥스 표준형 공식은 다음과 같이 찾을 수 있다. 편의상, 모든 논리합(${\displaystyle \lor }$)이나 함의(${\displaystyle \implies }$)를 논리곱(${\displaystyle \land }$) 및 부정(${\displaystyle \lnot }$)으로 나타내자. 그렇다면 1차 논리 공식을 다음과 같이 변환시킨다.

• ${\displaystyle (\forall x\colon \phi )\land \psi }$를 ${\displaystyle \forall x'\colon (\phi [x'/x]\land \psi )}$로 변환시킨다. 여기서 ${\displaystyle x'}$은 ${\displaystyle \psi }$에 포함되지 않는 임의의 변수이다.
• ${\displaystyle (\exists x\colon \phi )\land \psi }$를 ${\displaystyle \exists x'\colon (\phi [x'/x]\land \psi )}$로 변환시킨다. 여기서 ${\displaystyle x'}$은 ${\displaystyle \psi }$에 포함되지 않는 임의의 변수이다.
• ${\displaystyle \lnot \exists x\colon \phi }$를 ${\displaystyle \forall x\colon \lnot \phi }$로 변환시킨다.
• ${\displaystyle \lnot \forall x\colon \phi }$를 ${\displaystyle \exists x\colon \lnot \phi }$로 변환시킨다.

역사와 어원

프리넥스(영어: prenex)라는 단어는 라틴어: praenexus 프라이넥수스^[*](묶인, 고정된)에서 왔다. 이 용어는 다비트 힐베르트와 파울 베르나이스의 1938년 저서 《수학의 기초》(영어: Grundlagen der Mathematik)에서 최초로 사용하였다.

같이 보기

• 1차 논리
• 스콜렘 표준형

외부 링크

• Weisstein, Eric Wolfgang. “Prenex normal form”. 《Wolfram MathWorld》 (영어). Wolfram Research. 
• Alexander, Sam. “Prenex Normal Form Generator” (영어). 2014년 9월 8일에 원본 문서에서 보존된 문서. 2015년 1월 1일에 확인함.