건전성 문서 원본 보기

{{위키데이터 속성 추적}}
[[논리학]]에서 '''건전성'''({{llang|en|soundness}})이란, 형식 체계 내에서 증명가능한 명제(즉 정리)가 의미론 상으로도 참이 되는 성질이다. 이는 논리학에서 [[완전성]]의 역개념이 된다.

== 정의 ==
구문론적 귀결 관계 <math>\vdash</math>와 의미론적 귀결 관계 <math>\vDash</math>를 포함하는 [[형식 체계]]가 있다 하자. 임의의 [[논리식]]들의 집합 G와 논리식 p에 대하여. 다음이 항상 성립하면 형식 체계가 '''건전'''({{llang|en|sound}})하다고 한다.<ref name="a">Herbert B. Enderton (2002), ''A mathematical introduction to logic'', Academic Press(Elsevier), p.131.</ref>

* <math>G \vdash p</math> 이면, <math>G \vDash p</math>이다.

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

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

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

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

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

== 같이 보기 ==
* [[완전성]]
* [[괴델의 완전성 정리]]

== 각주 ==
<references/>

== 참고 문헌 ==
* Herbert B. Enderton (2002), ''A mathematical introduction to logic'', Academic Press(Elsevier)

[[분류:수학기초론 정리]]
[[분류:수리논리학]]
[[분류:모형 이론]]
[[분류:증명 이론]]
[[분류:연역]]
[[분류:논증]]
[[분류:논리학 개념]]