문장마다 결정을 보태도 모순을 피할 수 있나요?

Γ={P(a)∨Q(a)}는 P(a)인지 Q(a)인지 결정하지 않습니다. 극대 일관 집합 T를 만들면 모든 닫힌 문장 A에 대해 A 또는 ¬A 중 정확히 한쪽이 속합니다. T는 또한 모순을 도출하지 않습니다.

A와 ¬A를 함께 넣으면 모순이 생깁니다. ‘모든 문장을 결정한다’는 것과 ‘서로 충돌하는 주장도 허용한다’는 것은 다릅니다.

셀 수 있는 언어라면 모든 닫힌 문장을 A₀,A₁,A₂,…로 나열할 수 있습니다. 처음 Γ로 시작하여 n번째 단계에서 Aₙ을 더해도 무모순이면 Aₙ을, 그렇지 않으면 ¬Aₙ을 더합니다. 그 선택은 단계마다 무모순성을 보존합니다.

확장 언어에서 만들어지는 문장까지 공정하게 열거해야 합니다. 언젠가 등장한 모든 문장을 유한한 어느 단계에서 만나도록 일정을 구성합니다.

Γ가 무모순이라면 두 경우가 모두 모순일 수 없습니다. 첫 경우의 모순 증명에서 Γ⊢¬A를, 두 번째에서 Γ⊢¬¬A를 얻습니다. 고전논리에서 이중부정을 제거하면 Γ에서 A와 ¬A를 모두 증명하게 되므로 Γ 자체가 모순입니다.

어느 쪽이 무모순인지 선택할 수 있다는 수학적 존재 명제는 종료하는 결정 알고리즘이 있다는 말과 다릅니다.

Γ₀⊆Γ₁⊆…의 합집합에 ⊥의 증명이 있다면 그 증명에 사용한 유한한 전제들은 어느 한 Γₙ에 모두 포함됩니다. 그러면 그 Γₙ도 모순이 되어 가정과 충돌합니다. 유한 증명의 성질이 무한 확장의 안전성을 지켜 줍니다.

각 문장 A는 열거의 특정 단계에서 검사되어 A 또는 ¬A 중 한쪽이 합집합 T에 들어갑니다. 따라서 T는 무모순하고 문장마다 결정하는 집합입니다.

그렇지 않습니다. A가 T에 없다면 문장 결정에 따라 ¬A가 T에 있어야 합니다. 그런데 T에서 A를 증명할 수 있으므로 T가 모순됩니다. 따라서 극대 일관 T는 도출 가능한 모든 문장을 포함합니다. 이것을 연역적 닫힘이라고 부릅니다.

일반 Γ가 이미 자신의 모든 도출 결과를 문자 그대로 포함한다고 약속할 필요는 없습니다. 극대 일관 집합 T에 관해 확립한 성질입니다.

A와 B 중 적어도 하나가 T에 있어야 합니다. 둘 다 없으면 ¬A와 ¬B가 T에 있어 A∨B와 충돌하기 때문입니다. 반대로 A가 T에 있으면 선언 도입으로 A∨B도 T에 들어갑니다.

물론입니다. A∨B는 둘 중 적어도 하나를 요구하므로 둘 모두인 경우도 포함합니다.

조건문이 참인 경우에는 A가 거짓이거나 B가 참이면 됩니다. 극대 일관 T에서 A→B가 들어 있다면 ¬A 또는 B 중 적어도 하나가 T에 있어야 합니다. 그렇지 않으면 A와 ¬B가 함께 T에 들어 조건문과 충돌합니다.

조건문 제거로 B가 도출되고 연역적 닫힘에 의해 B가 T에 속합니다.

확장 과정은 이전 문장을 삭제하지 않습니다. 따라서 ∃xA(x)→A(c)라는 헨킨 조건은 T에 남습니다. 만약 ∃xA(x)∈T라면 조건문 제거로 A(c)∈T입니다. T 안의 존재문마다 항으로 된 증인을 확보합니다.

그 조건만으로는 그렇게 결론내리지 않습니다. 증거 함의문의 앞부분이 참일 때 비로소 조건문 제거를 쓸 수 있습니다.

각 문장 A에 대해 A와 ¬A 중 한쪽을 수학적으로 선택할 수 있다는 사실은 입력 A에 대한 결정을 유한 시간 안에 계산할 수 있다는 말과 다릅니다. 구성의 선택 단계는 일반적인 결정 알고리즘을 전제하지 않습니다.

존재 증명과 효과적인 계산 절차는 다른 수준의 주장입니다. 15편에서 결정과 반결정의 차이를 따로 배우게 됩니다.

우선 극대 일관 확장은 자유변수가 없는 닫힌 문장을 대상으로 합니다. 열린 식의 만족은 변수 배정의 선택에 의존합니다. 항 모형을 만든 뒤 변수에 닫힌 항의 동치류를 배정하여 열린 식의 의미를 설명할 수 있습니다.

대입할 때는 변수 포획을 피해야 합니다. 닫힌 항 자체는 자유변수가 없으므로 포획 위험이 줄지만, 속박 변수를 조심스럽게 다루는 약속은 계속 유효합니다.

아직 영역·상수·함수·관계의 해석을 만들어야 합니다. 극대 일관 T는 여전히 문장들의 집합입니다. 다음 편에서 닫힌 항을 모형의 재료로 삼고 t=u∈T일 때 두 항을 같은 대상으로 다룹니다.

T의 문장 소속과 이 항 모형에서의 참이 일치한다는 것을 식의 구조에 대한 귀납으로 증명합니다.