건전성

논리학에서 건전성(영어: soundness)이란, 형식 체계 내에서 증명가능한 명제(즉 정리)가 의미론 상으로도 참이 되는 성질이다. 이는 논리학에서 완전성의 역개념이 된다.

정의

구문론적 귀결 관계 $\vdash$와 의미론적 귀결 관계 $\vDash$를 포함하는 형식 체계가 있다 하자. 임의의 논리식들의 집합 G와 논리식 p에 대하여. 다음이 항상 성립하면 형식 체계가 건전(영어: sound)하다고 한다.

• $G\vdash p$ 이면, $G\vDash p$이다.

건전성 정리의 증명

잘 정의된 명제 논리 체계에서는 건전성이 성립해야 한다. 흔히 논리체계에서는 건전성 정리(soundness theorem)가 간단한 귀납법에 의해 이루어지므로 완전성 정리의 증명보다 훨씬 간략하다. "모든 논리적 공리는 항진"이라는 것과 "모든 논리적 추론규칙(보통 전건 긍정을 포함)은 타당성을 가진다"는 보조정리를 바탕으로 증명은 쉽게 끝난다. 이 보조정리는 공리와 추론규칙마다 확인해보는 것으로 간단히 얻을 수 있으며, 이를 전제로 증명은 다음과 같이 완성된다.

증명:

(명제의 구성법과 증명관계가 귀납적으로 잘 정의되어 있다는 가정 하에) $G\vdash p$인 경우 p는 다음의 세 가지 경우 중 하나이다: 논리적 공리이거나, 전제 G의 원소이거나, 공리와 전제에 추론규칙들을 적용하여 나온 명제이거나.

1. p가 논리적 공리일 경우 위의 보조정리와 타당성의 정의에 의해 곧바로 $G\vDash p$ 을 얻는다.
2. p가 G의 원소인 경우에도 곧바로 $G\vDash p$ 을 얻는다.
3. 공리나 G의 원소에 추론규칙을 0번 사용하여 증명된 명제는 위의 2가지 경우에 해당하여 의미론적으로 참이다. 이제 추론규칙을 n번 적용하여 나온 명제들 $p_{1},p_{2},...,p_{i}$가 의미론적으로도 귀결인 것이 보여졌다고 가정하고 그러한 명제들에 임의의 추론규칙을 적용하여 나온 명제 q를 가정하면 보조정리에 의해 항진성이 보존되므로 q, 즉 추론규칙을 n+1번 적용하여 나온 임의의 명제도 항상 의미론적으로 참이다.

그렇다면 귀납법에 의해 모든 증명되는 명제는 의미론적으로 참이다.

잘 정의된 1차 논리에 대해서도 마찬가지로 양화사를 포함하는 공리나 추론규칙이 타당하다는 것만 추가로 보이면 비슷한 방식의 증명이 이루어질 수 있다. 완전성도 성립할 경우 이 논리체계에서 구문론적 참과 의미론적 참은 일치한다고 간주할 수 있다.

같이 보기

• 완전성
• 괴델의 완전성 정리

참고 문헌

• Herbert B. Enderton (2002), A mathematical introduction to logic, Academic Press(Elsevier)