참인 결론에는 언제나 증명이 있나요?

고전 일차논리의 완전성 정리는 Γ⊨B ⇒ Γ⊢B라고 읽습니다. 전제 집합 Γ를 모두 만족하는 모든 구조에서 B가 참이면, Γ로부터 B를 유한한 형식 증명으로 도출할 수 있다는 뜻입니다. 여기서 참은 우리가 머릿속에 그린 한 세계의 참이 아니라 모든 Γ-모형에서의 의미론적 귀결입니다.

아닙니다. 한 모형의 진리 M⊨B만으로 Γ에서 B를 도출할 수는 없습니다. B가 거짓인 다른 Γ-모형이 있을 수 있기 때문입니다. 완전성 정리의 전칭 조건을 빠뜨리지 않아야 합니다.

건전성은 Γ⊢B ⇒ Γ⊨B입니다. 증명에서 모든 모형의 참으로 이어집니다. 완전성은 Γ⊨B ⇒ Γ⊢B로, 모든 관련 모형의 참에서 증명을 찾아갑니다. 두 정리가 함께 성립하면 고전 일차논리에서 Γ⊢B ⇔ Γ⊨B가 됩니다. 다만 두 기호의 뜻은 여전히 서로 다릅니다.

건전성은 각 규칙이 참을 지킨다는 계산에 가깝습니다. 완전성은 가능한 모든 전제를 만족하는 구조에서 참인 명제가 형식 체계에서도 놓치지 않는다는 강한 주장입니다. 이를 보이려고 실제 모형을 만드는 먼 길을 돌아왔습니다.

Γ∪{¬B}를 생각합니다. 만약 이 집합이 모순된다면, ¬B를 임시 가정했을 때 ⊥이 도출됩니다. 가정을 해제해 Γ⊢¬¬B를 얻고 고전 논리의 이중부정 제거로 Γ⊢B가 됩니다. 이는 증명이 없다는 출발점과 충돌합니다. 그러므로 Γ에서 B를 도출할 수 없다면 Γ와 ¬B를 함께 놓아도 무모순입니다.

8~10편에서 확인한 헨킨 증거 이름, 극대 일관 확장, 항 모형과 진리 보조정리를 적용합니다. 그 결과 Γ∪{¬B}를 만족하는 모형 M이 생깁니다. M에서는 모든 Γ가 참이고 B는 거짓입니다.

방금 구성은 Γ⊬B ⇒ Γ⊭B를 보여 줍니다. 즉 Γ에서 B를 증명하지 못하면, Γ를 모두 만족하지만 B는 거짓인 모형을 하나 만들 수 있습니다. 이 명제의 대우를 취하면 Γ⊨B ⇒ Γ⊢B입니다. 이것이 완전성 정리의 핵심 결론입니다.

무모순한 집합이 있으면 실제 모형이 있다는 중간 정리가 필요하기 때문입니다. 단지 모순의 증명을 찾지 못했다는 실험 기록은 이런 모형 존재를 보장하지 못합니다.

그렇습니다. Γ 전체를 참으로 만드는 모형이 하나도 없으므로 ‘모든 Γ-모형에서 B가 참’이라는 문장은 반례가 없어 성립합니다. 고전 논리에서는 또한 Γ로부터 ⊥을 도출할 수 있고, 모순 제거 규칙으로 임의의 B를 도출할 수 있습니다. 건전성과 완전성의 양쪽 방향은 이 경우에도 일치합니다.

아닙니다. Γ-모형이 없기 때문에 성립하는 귀결과 아무 전제 없는 논리적 타당성 ⊨B는 구별해야 합니다. 예를 들어 단순 원자문 B는 논리적 타당성이 아닐 수 있습니다.

표준 일차논리의 의미론적 완전성은 전제 Γ의 크기를 유한하게 제한하지 않습니다. 다만 Γ⊢B가 성립하면 해당 증명은 언제나 유한하므로 Γ 중 실제 사용한 전제는 유한 개입니다. 그 유한 부분 Γ₀에 대해서도 Γ₀⊢B이고, 건전성으로 Γ₀⊨B입니다.

맞습니다. 이 성질을 만족 가능성의 언어로 바꾸면 콤팩트성 정리가 나옵니다. 다음 편에서는 모든 유한 부분이 만족 가능할 때 전체를 만족하는 모형이 있다는 것을 직접 확인하겠습니다.

일차논리의 유효한 증명들을 길이 순서로 열거하는 프로그램을 만들 수 있다는 점은 유용합니다. 어떤 B가 논리적 타당성이면 완전성에 따라 증명이 있으므로 충분히 오래 열거하면 발견합니다. 그러나 B가 타당하지 않다면 이 검색이 언제 끝날지 보장되지 않습니다. 완전성이 모든 입력의 예·아니요를 결정하는 알고리즘까지 보장하지는 않습니다.

계산 절차로 전제 Γ를 다루려면 공리 집합을 효과적으로 열거할 수 있다는 조건이 추가로 필요합니다. 완전성 정리 자체는 그런 계산 가능성의 가정을 요구하지 않습니다.

고전 논리에서 이 문장은 모든 모형에서 참이므로 ⊨P(a)∨¬P(a)입니다. 완전성에 따라 아무 전제 없이 증명할 수 있습니다. 한편 P(a)는 P의 외연에 a의 값이 포함되는 모형에서는 참이고, 포함되지 않는 모형에서는 거짓입니다. 따라서 ⊨P(a)는 성립하지 않으며 논리적 정리도 아닙니다.

논리적 타당성은 모든 해석에서 참을 보장합니다. 경험적 사실에 대한 문장은 특정한 해석이나 사실을 전제로 참일 수 있습니다. 두 종류의 참을 구별하면 증명 가능성에 관한 과장된 주장을 피할 수 있습니다.

지금 정리는 일차논리의 증명 체계가 의미론적 귀결을 모두 포착한다는 뜻입니다. 반면 특정 산술 이론 T가 완전하다는 말은 산술 문장 A마다 T⊢A 또는 T⊢¬A라는 뜻입니다. 두 완전성은 다른 속성을 가리킵니다. 일차논리 증명 체계가 완전해도 어떤 특정한 효과적 산술 이론은 미결정 문장을 가질 수 있습니다.

‘논리 전체의 의미론적 귀결과 증명’에 관한 정리인지, ‘선택한 이론이 문장마다 증명 또는 반증하는가’에 관한 정리인지 물어보면 됩니다. 용어가 같아도 대상이 다릅니다.

아닙니다. 영역 D={아라,보라}, P={아라}, Q={아라}로 놓으면 모든 P 대상은 Q이고 P인 대상이 하나 있습니다. 하지만 보라는 Q가 아니므로 ∀xQ(x)는 거짓입니다. 전제 둘 다 참이고 결론이 거짓인 구체적 반모형입니다. 따라서 건전성에 의해 그 결론을 전제에서 적법하게 증명할 수 없습니다.

같은 전제에서 ∃xQ(x)는 도출됩니다. 존재 제거로 P인 임시 증인을 잡아 Q를 얻은 뒤 존재 도입을 사용하며, 새 이름 조건을 지켜 존재 제거 부분 증명을 마무리합니다.

무한한 Γ가 한 문장 B를 강제로 참으로 만들면, 사실 Γ의 유한한 부분만으로도 B를 강제로 참으로 만든다는 점입니다. 유한한 증명을 갖는다는 성질을 거꾸로 읽은 결과입니다. 이제 ‘모든 유한 부분이 만족 가능하면 전체도 만족 가능한가?’라는 질문을 할 수 있습니다.

완전성과 건전성, 유한 증명이 함께 쓰입니다. 전체가 만족 불가능하다고 가정하면 완전성을 통해 유한한 모순 증명을 얻고, 그 증명에 쓰인 유한 전제들이 문제를 일으켰음을 보이겠습니다.