프리넥스 표준형

틀:위키데이터 속성 추적 수리논리학에서 프리넥스 표준형(prenex標準型, 틀:Llang)은 모든 한정 기호가 앞에 와 있는 1차 논리 공식의 형태이다.

정의

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

$\varphi ={\varphi }_{\text{prefix}}{\varphi }_{\text{matrix}}$

여기서

• ${\varphi }_{\text{prefix}}$는 기호 $\mathrm{\exists }$와 $\mathrm{\forall }$ 및 변수만을 포함하는 문자열이다. 특히, $\wedge$나 $=$ 및 기타 연산·관계를 포함하지 않는다. 이를 $\varphi$의 접두사(틀:Llang)라고 한다.
• ${\varphi }_{\text{matrix}}$는 기호 $\mathrm{\forall }$을 포함하지 않는 문자열이다. 즉, 변수와 $\mathrm{\neg }$, $\wedge$, $=$ 및 기타 연산·관계만으로 구성된다. 이를 $\varphi$의 매트릭스(틀:Llang)라고 한다.

알고리즘

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

• $(\mathrm{\forall }x:\varphi )\wedge \psi$를 $\mathrm{\forall }{x}^{\prime }:(\varphi [x^{\prime }/x]\wedge \psi )$로 변환시킨다. 여기서 $x^{\prime }$은 $\psi$에 포함되지 않는 임의의 변수이다.
• $(\mathrm{\exists }x:\varphi )\wedge \psi$를 $\mathrm{\exists }{x}^{\prime }:(\varphi [x^{\prime }/x]\wedge \psi )$로 변환시킨다. 여기서 $x^{\prime }$은 $\psi$에 포함되지 않는 임의의 변수이다.
• $\mathrm{\neg }\mathrm{\exists }x:\varphi$를 $\mathrm{\forall }x:\mathrm{\neg }\varphi$로 변환시킨다.
• $\mathrm{\neg }\mathrm{\forall }x:\varphi$를 $\mathrm{\exists }x:\mathrm{\neg }\varphi$로 변환시킨다.

역사와 어원

프리넥스(틀:Llang)라는 단어는 틀:Llang(묶인, 고정된)에서 왔다. 이 용어는 다비트 힐베르트와 파울 베르나이스의 1938년 저서 《수학의 기초》(틀:Llang)에서 최초로 사용하였다.

같이 보기

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

외부 링크

• 틀:매스월드
• 틀:웹 인용