양화 규칙을 포함한 증명 전체는 왜 믿을 수 있나요?

논증의 각 줄에는 이미 알려진 명제뿐 아니라 변수에 대한 주장도 나타납니다. Γ ⊢ B는 전제집합 Γ에서 B를 도출한다는 뜻이고, Γ ⊨ B는 Γ를 모두 만족하는 모든 모형과 관련 변수 배정에서 B가 참이라는 뜻입니다. Γ와 B가 문장이면 변수 배정을 따로 표시할 필요가 없습니다.

우리가 확인할 명제는 건전성입니다. 증명 규칙을 올바르게 적용하여 Γ ⊢ B를 얻었다면 Γ ⊨ B가 성립해야 합니다. 귀납의 대상은 증명에 놓인 줄의 수나 높이입니다.

건전성은 가능한 모든 모형을 대상으로 합니다. 어느 한 장면에서 규칙이 잘 작동했다는 관찰은 이해를 돕는 예이며, 일반적인 참 보존에는 규칙의 의미론적 이유가 필요합니다.

∀x A는 전체 영역 D의 모든 원소 d에 대해 M,g[x↦d] ⊨ A일 때 참입니다. ∃x A는 적어도 한 d에서 A가 참일 때 참입니다. g[x↦d]는 x에 배정한 값만 d로 바꾼 배정을 뜻합니다. 모형 M의 술어 해석과 상수 뜻은 유지됩니다.

이 수업의 영역 D는 비어 있지 않습니다. 함수 기호는 D에서 전체적으로 정의되며 동일성 =은 대상이 실제로 같다는 뜻입니다.

양화사가 x를 묶었으면 x의 배정을 바꿉니다. A 안에 자유롭게 나타난 y의 배정은 같은 값으로 둡니다. 이것이 다음 단계에서 안전한 대입이 필요한 이유입니다.

항 t가 식 A의 x 자리에 안전하게 들어갈 수 있다면 M,g ⊨ A[t/x]와 M,g[x↦⟦t⟧(M,g)] ⊨ A의 참거짓이 같습니다. ⟦t⟧(M,g)는 원래 배정 g에서 항 t가 가리키는 대상입니다. 속박 변수에 의해 t의 자유변수가 포획되면 이 보조정리는 사용할 수 없습니다.

먼저 원래 g에서 t의 값을 구하고, 그 값으로 x의 배정을 바꾼 뒤 A를 평가합니다. 대입 결과 안에서 t의 값을 다시 구하는 순서는 보조정리가 말하는 순서와 다릅니다.

모형과 배정에서 ∀x A가 참이라고 합시다. 전체 영역의 모든 d에서 A가 참이므로 원래 g에서 t가 가리키는 값 d에서도 A가 참입니다. 안전한 대입 보조정리를 적용하면 A[t/x]가 같은 모형과 원래 배정에서 참입니다. 이 논증은 항 t의 해석이 D에 속한다는 약속을 사용합니다.

예를 들어 영역 {0,1}에서 R(x,y)를 x와 y가 서로 다르다는 관계로 해석하면 ∀x∃y R(x,y)는 참입니다. 그런데 x 자리에 속박될 변수 y를 넣어 만든 ∃y R(y,y)는 거짓입니다. 그래서 안전한 대입 조건을 규칙에 붙입니다.

P(a)가 참이면 a가 가리키는 대상 d가 영역 D에 실제로 있습니다. 존재문의 x에 d를 배정했을 때 P(x)가 참이므로 ∃x P(x)가 참입니다. 일반형 A[t/x] ⊢ ∃x A에서도 t가 x 자리에 안전하게 들어가야 합니다.

이미 쓰던 이름이든 함수항이든 영역의 대상으로 해석되면 됩니다. 존재 도입은 어떤 대상을 하나 지목할 수 있다는 사실을 사용합니다. 특정 이름을 새로 만들 필요는 없습니다.

부분 증명에서 x를 임의 대상으로 다뤘고 아직 해제되지 않은 가정 Γ에 x가 자유롭게 나타나지 않을 때만 가능합니다. Γ를 참으로 만드는 배정 g에서 x의 값을 임의의 d로 바꾸어도 Γ는 참인 채 남습니다. 부분 증명이 건전하므로 그 바뀐 배정에서도 P(x)가 참입니다. d가 임의였으므로 ∀x P(x)가 참입니다.

영역 {아라, 보라}에서 P는 아라에게만 참이고 g(x)=아라라고 합시다. 가정 P(x)는 이 배정에서 참이지만 ∀x P(x)는 거짓입니다. P(x) ⊢ ∀xP(x)가 허용되지 않는 까닭입니다. 반대로 x가 Γ에 자유롭게 나타나지 않으면 이 반례의 출발점이 차단됩니다.

존재문에 증인이 있다는 사실은 압니다. 증인에게 새 이름 c를 붙여 P(c)를 임시 가정하고, 그 가정 아래에서 결론 B를 얻었다고 합시다. c가 존재문·다른 미해제 외부 가정·결론 B에 나타나지 않아야 B를 밖으로 내보낼 수 있습니다. 이때 c는 증인에게만 붙인 임시 표시이므로 B는 그 이름에 의존하지 않습니다.

처음 모형에서 존재문이 참이면 증인 d가 있습니다. 기존 해석을 유지하고 신선한 c만 d를 가리키게 확장합니다. 이 확장에서도 모든 외부 가정은 참입니다. 부분 증명의 건전성으로 B가 참이며 B에는 c가 없으므로 원래 해석에서도 B가 참입니다.

이름 c는 해석에서 이미 어떤 대상을 가리킬 수 있습니다. ∃xP(x)는 적어도 한 대상이 P를 만족한다고 말할 뿐 c의 해석이 그 대상이라고 지정하지 않습니다. 기존 이름을 증인으로 임의 지정하면 증명을 잘못 만듭니다.

D={아라, 보라}, P={아라}, c=보라라고 둡니다. ∃xP(x)는 참이고 P(c)는 거짓입니다. 마찬가지로 ∃xP(x)로부터 ∀xP(x)를 얻을 수 없습니다. 존재와 보편은 요구하는 증인의 범위가 다릅니다.

일차논리에서 =은 실제로 같은 대상이라는 의미입니다. a와 b라는 서로 다른 이름도 같은 대상을 가리킬 수 있습니다. 따라서 모든 항 t에 대해 t=t는 언제나 참이며, s=t와 P(s)가 참이면 P(t)도 참입니다. 이 규칙을 동일성 도입·제거라고 부릅니다.

함수도 대상으로부터 결과를 정하는 해석이므로 같은 입력은 같은 결과를 냅니다. s=t이면 f(s)=f(t)도 참입니다. 다만 대입할 식에 양화사가 있으면 변수 포획을 피하도록 적법한 위치만 바꿉니다.

원자식에서는 같은 대상이 같은 관계의 자리를 차지하기 때문입니다. 복합식이라면 연결사가 참거짓 계산을 보존하고, 양화사는 같은 영역의 원소를 차례로 확인하므로 대입의 효과가 식 전체로 퍼집니다. 안전한 대입과 속박변수 이름 변경을 전제로 하는 식 구조에 대한 귀납으로 동일성 치환의 건전성을 설명할 수 있습니다.

같은 대상이라는 전제가 먼저 있어야 합니다. a=b 없이 P(a)에서 P(b)로 이동하면 b가 다른 대상을 가리키는 반모형이 곧바로 만들어집니다.

먼저 증명 높이가 가장 작은 단계에서는 줄이 아직 해제되지 않은 가정이나 논리적 공리·동일성 반사성처럼 의미론적으로 올바른 출발점입니다. 다음으로 마지막 규칙 직전의 모든 부분 증명에 대해 ‘그 부분 증명의 미해제 가정이 참인 해석에서 결론도 참’이라고 가정합니다. 마지막 규칙이 연결사·∀·∃·동일성 중 무엇인지에 따라 앞서 확인한 참 보존 성질을 적용합니다.

각 유한 증명은 이 규칙들로 이루어지므로 증명의 구조에 대한 귀납을 끝낼 수 있습니다. 고전논리 특유의 이중부정 제거도 고전 이값 의미론에서 참을 보존합니다. 식에 자유변수가 있다면 모든 해석과 배정을 동일하게 고려합니다.

사례 검사는 계산을 교정하는 데 유용합니다. 귀납 증명은 가능한 모든 유한 증명 구조에서 출발점과 확장 규칙을 빠짐없이 확인한다는 점에서 다릅니다.

오늘 얻은 방향은 Γ ⊢ B ⇒ Γ ⊨ B입니다. 반대 방향은 완전성 정리에서 다룹니다. 그 준비로 ‘모순을 증명할 수 없는 문장들의 집합에 실제 모형이 있는가?’라는 질문을 세워야 합니다. 다음 편부터 헨킨의 새 이름과 항 모형으로 길을 엽니다.

오늘의 구조 귀납은 건전성의 증명입니다. 역방향에는 문장 집합을 확장하고 그것을 참으로 만드는 모형을 구성하는 별도의 논증이 필요합니다.