완전성

3. 구문론적 완전성

건전성의 역으로서 완전성이란 "의미론적 귀결이 구문론적 귀결을 함의한다"는 것을 의미한다. 형식 체계 S에서 다음이 항상 성립하면 S가 '''완전'''(complete^영어)하다고 한다.

:$\backslash models\_\{\backslash mathcal\; S\}\; \backslash varphi\; \backslash implies\; \backslash vdash\_\{\backslash mathcal\; S\}\; \backslash varphi$

괴델의 완전성 정리에 따르면 잘 정의된 1차 논리 체계에서는 귀결 명제의 집합이 항상 모형을 가지므로 완전성이 성립한다.

형식 체계의 언어 내에서 구성되는 임의의 문장 $\backslash varphi$에 대하여, 형식 체계 내에서 $\backslash varphi$ 혹은 $\backslash lnot\; \backslash varphi$가 반드시 도출되는 성질을 구문론적 완전성(syntactical completeness)이라 한다. 불완전성 정리는 어떠한 형식 체계가 재귀(recursion)의 개념을 나타낼 수 있을 정도로 강력하다면, 무모순성과 구문론적 완전성을 동시에 가질 수 없음을 의미한다.

형식적 시스템 ''구문론적 완전성'' 또는 ''연역적 완전성'' 또는 ''최대 완전성''을 갖는다는 것은 시스템의 언어에 속하는 각 문장 (닫힌 공식) φ에 대해 φ 또는 ¬φ가 의 정리일 경우를 말한다. 이는 ''부정 완전성''이라고도 하며, 의미적 완전성보다 더 강력하다. 다른 의미에서, 형식적 시스템은 증명할 수 없는 문장을 일관성을 도입하지 않고 추가할 수 없을 때에만 ''구문론적 완전성''을 갖는다. 진리 함수 명제 논리와 일차 술어 논리는 의미적으로 완전하지만 구문론적으로 완전하지 않다(예를 들어, 단일 명제 변수 '''A'''로 구성된 명제 논리 명제는 정리가 아니며, 그 부정 또한 아니다). 괴델의 불완전성 정리는 계산 가능한 시스템 중 페아노 산술과 같이 충분히 강력한 시스템은 일관적이면서 구문론적으로 완전할 수 없음을 보여준다.

4. 반증 완전성

형식적 시스템 $\backslash mathcal\{S\}$가 모든 만족 불가능한 공식 집합으로부터 ''거짓''을 도출할 수 있다면 '''반증 완전'''하다고 한다. 즉, 다음과 같다.

::$\backslash Gamma\; \backslash models\_\{\backslash mathcal\; S\}\; \backslash bot\; \backslash to\backslash \; \backslash Gamma\; \backslash vdash\_\{\backslash mathcal\; S\}\; \backslash bot.$^[2]

모든 강한 완전성을 가진 시스템은 반증 완전하기도 하다. 직관적으로, 강한 완전성은 공식 집합 $\backslash Gamma$가 주어졌을 때, $\backslash Gamma$의 모든 의미론적 결과 $\backslash varphi$를 "계산"하는 것이 가능하다는 것을 의미하며, 반증 완전성은 공식 집합 $\backslash Gamma$와 공식 $\backslash varphi$가 주어졌을 때, $\backslash varphi$가 $\backslash Gamma$의 의미론적 결과인지 "확인"하는 것이 가능하다는 것을 의미한다.

반증 완전 시스템의 예로는 혼 절에 대한 SLD 해법, 등식 절 일차 논리에 대한 중첩 계산, 절 집합에 대한 로빈슨의 해법 등이 있다.^[3] 로빈슨의 해법은 강한 완전성을 가지지 않는다. 예를 들어, $\backslash \{\; a\; \backslash \}\; \backslash models\; a\; \backslash lor\; b$는 일차 논리의 명제 부분집합에서도 성립하지만, $a\; \backslash lor\; b$는 해법에 의해 $\backslash \{\; a\; \backslash \}$에서 도출될 수 없다. 하지만, $\backslash \{\; a,\; \backslash lnot\; (a\; \backslash lor\; b)\; \backslash \}\; \backslash vdash\; \backslash bot$는 도출될 수 있다.

5. 기타 완전성

건전성의 역으로서 완전성이란 "의미론적 귀결이 구문론적 귀결을 함의한다"는 것을 의미한다. 괴델의 완전성 정리에 따르면 잘 정의된 1차 논리 체계에서는 귀결 명제의 집합이 항상 모형을 가지므로 완전성이 성립한다. 완전성에 대한 역의 속성은 견실성이라고 한다. 시스템은 속성에 관하여 견실하다면(대부분 의미론적 타당성), 해당 시스템의 각 정리가 그 속성을 갖는다.^[1]

5. 1. 표현 완전성

5. 2. 함수적 완전성

5. 3. 구조적 완전성

5. 4. 모형 완전성

참조

_[1] 서적 1996
_[2] 서적 Principles of Automated Theorem Proving Wiley 1991
_[3] 서적 Artificial Intelligence: A Modern Approach Prentice Hall 1995