대입은 언제 식의 뜻을 지켜 주나요?

비교할 대상을 정확히 정해야 합니다. 3편의 구조를 다시 쓰겠습니다. P는 서류 제출, Q는 확인 도장, f는 지정 연락인, R은 인사한 관계입니다. 이름과 배정도 아래처럼 고정합니다.

기본 g에서 P(x)는 참입니다. 그런데 x 자리에 b를 써 넣은 P(b)는 거짓입니다. bᴹ는 보라이고 보라는 P가 아니기 때문입니다. 안전하게 대입했다고 해서 원래 식과 같은 배정에서 같은 값을 갖는다는 보장은 없습니다.

P(b)를 원래 g에서 읽는 결과는, x의 배정을 b가 가리키는 보라로 바꾸고 원래 P(x)를 읽는 결과와 같습니다. 두 경우 모두 보라가 서류를 냈는지 확인합니다. 이 두 계산 경로가 일치한다는 것이 이번 편의 목표입니다.

A[t/x]는 “식 A의 자유로운 x 자리에 항 t를 대입한 결과”라고 읽습니다. t/x는 분수가 아닙니다. A는 식 전체를, t는 항 전체를 대신 부르는 설명용 표시입니다. 양화사에 이미 묶인 x의 출현은 이 대입으로 바꾸지 않습니다.

눈에 보이는 글자를 모두 바꾸는 작업이 아니기 때문입니다. 이 전체 식에서 x는 ∀x가 맡습니다. 다만 전칭문에서 그 양화사를 벗겨 몸통 R(x,y)를 따로 보면, 몸통의 x는 자유 출현입니다. 어느 식 전체를 A로 삼았는지 먼저 확인하세요.

한 번의 대입에서는 원래 식이나 항에 있던 대상 자리만 바꿉니다. 넣을 항 f(x) 안의 x를 끝없이 다시 바꾸지 않습니다. 예를 들어 원래 항 f(x)의 안쪽 x 한 자리에 f(x)를 한 번 넣으면 f(f(x))가 됩니다.

네. 항의 재귀적 대입은 다음처럼 정합니다. x를 만나면 t를 내놓고, 다른 변수와 상수는 그대로 둡니다. 함수항에서는 각 입력 항에 대입한 결과를 같은 함수기호로 다시 묶습니다. 이 정의가 “한 번의 대입”의 범위를 정해 줍니다.

그렇게 글자만 바꾸면, 원래 바깥 배정에서 값을 받아야 할 넣은 y가 ∃y에 붙잡힙니다. 이것이 변수 포획입니다. 이번 편에서는 포획이 생기는 이런 교체를 허용된 대입으로 취급하지 않습니다. 구체적인 값을 비교해 보겠습니다.

그렇습니다. 두 자리의 역할이 유지되어야 합니다. 그런데 포획된 식은 하나의 양화사가 R의 두 자리를 함께 움직여 “자기 자신에게 인사한 사람”을 찾게 만들었습니다. 원래 넣으려던 항 y의 바깥 값이 사라졌습니다.

항 t가 식 A의 x에 대입 가능하다, 영어로 “free for x in A”라고 할 조건은 다음과 같습니다. A의 자유로운 x의 어느 출현도, t에 들어 있는 변수를 묶는 양화사의 범위 안에 놓여 있지 않아야 합니다. 항에는 양화사가 없으므로 항의 변수들을 그대로 살피면 됩니다.

맞습니다. 대입할 자리로 들어가는 길에 그 양화사가 있는지를 봅니다. 같은 글자가 다른 범위에 등장한다고 곧바로 충돌하지는 않습니다. 반대로 자유로운 x가 여러 곳에 있으면 그 자리들을 모두 확인해야 합니다.

안쪽 양화사의 변수 이름을 안전하게 바꿀 수 있습니다. 식과 넣을 항에 쓰이지 않은 z를 골라 ∃zR(x,z)로 적습니다. 이 이름 변경은 같은 대상을 찾는 조건을 유지합니다. 그다음 자유로운 x에 y를 넣으면 ∃zR(y,z)가 됩니다.

안전한 속박변수 이름 변경은 모든 같은 구조와 배정에서 원래 식과 같은 만족 여부를 갖습니다. 흔히 알파 변환이라고 부릅니다. 바깥의 자유변수는 그대로 두고, 담당 양화사와 그 양화사가 묶는 출현만 함께 바꾼다는 조건이 중요합니다.

t가 A의 x에 대입 가능하다고 합시다. 먼저 원래 M,g에서 t의 값을 구해 d=⟦t⟧ᴹ,g라고 부르겠습니다. d는 언어에 새로 넣은 이름이 아니라 영역 안의 한 대상을 설명하는 표시입니다. 대입 보조정리는 아래 두 경로의 만족 여부가 같다고 말합니다.

정확합니다. 왼쪽과 오른쪽은 서로 다른 중간 단계를 거쳐 같은 대상들을 살펴봅니다. ⊨의 왼쪽에 적힌 배정까지 비교해야 이 정리의 뜻이 보입니다. A와 A[t/x]가 늘 논리적으로 동치다라는 말로 줄이면 잘못된 주장이 됩니다.

달라질 수 있으므로 순서를 지켜야 합니다. 정리는 원래 g에서 t의 값을 먼저 구합니다. 기본 g(x)=아라에서 f(x)의 값은 보라입니다. 따라서 d는 보라이고, 오른쪽에서는 x에 보라를 준 배정을 씁니다. 갱신한 뒤 f(x)를 다시 계산해 d를 바꾸지 않습니다.

그래서 원래 g라는 표시가 필요합니다. 그 재계산은 원래 정리와 다른 작업입니다. 한 번의 대입과 한 번의 배정 갱신을 비교해야 하며, 중간에 새 항값을 구해 다시 갱신하는 단계를 덧붙이지 않습니다.

네. 술어는 항들의 값을 받으므로, 대입 전후의 항값이 맞는지 먼저 보겠습니다. s와 t는 각각 항 전체를 대신하는 표시이고, d는 원래 g에서 구한 t의 값입니다. 항에 대해서는 양화사가 없으므로 포획 조건을 따로 검사할 곳도 없습니다.

u는 f(u)를 구성하는 더 작은 항입니다. 2편의 재귀적 구성에 맞추어, 작은 구성요소들에서 성질이 성립한다고 놓고 큰 항에서도 성립함을 보입니다. 이것이 구조에 따른 귀납의 한 단계입니다. 여러 자리 함수도 각 입력 항에 같은 설명을 적용합니다.

두 경로에서 s가 같은 대상을 가리키므로 같은 Pᴹ의 포함 여부를 확인합니다. R(s,u)라면 같은 순서쌍을 Rᴹ와 비교하고, s=u라면 같은 두 항값의 동일성을 비교합니다. 이로써 원자식의 경우를 얻습니다.

더 작은 B와 C 각각에 대해 정리가 모든 적절한 배정에서 성립한다고 가정합니다. 왼쪽의 B[t/x]와 C[t/x]가 원래 g에서 모두 만족되는 조건은, 오른쪽의 원래 B와 C가 같은 갱신 배정에서 모두 만족되는 조건과 같습니다. 양쪽을 ∧로 묶으면 전체 식의 정리가 됩니다.

맞습니다. 식 전체에서 x의 출현은 그 ∀x에 묶이므로 (∀xB)[t/x]는 그대로 ∀xB입니다. 오른쪽에서 먼저 x를 d로 갱신하더라도, ∀x는 몸통을 읽을 때 다시 각 후보 e로 x를 갱신합니다.

그렇습니다. ∃xB인 경우에도 같은 설명이 통합니다. 두 경로가 같은 후보 e에서 같은 몸통을 평가하므로, 증거가 있는지의 답도 같습니다. 일치 보조정리로 “전체 식에 자유 x가 없어서 시작 x 값에 의존하지 않는다”고 설명해도 됩니다.

바로 여기서 쓰입니다. 먼저 x가 B에 자유롭게 등장하는 경우를 보겠습니다. t가 A의 x에 대입 가능하려면 z가 t에 들어 있지 않아야 합니다. 그래야 z의 값을 어떤 e로 바꾸어도 t의 값은 원래 d와 같습니다. 항의 변수 값에 대한 일치 성질을 사용합니다.

맞습니다. 그리고 ∃z의 경우에는 표의 “모든 e”를 “어떤 e”로 바꾸어 같은 과정을 밟습니다. x가 B에 자유롭게 등장하지 않는 경우에는 대입 결과가 그대로이고, 두 배정은 식의 모든 자유변수에 같은 값을 주므로 일치 보조정리로 바로 처리할 수 있습니다. 그 경우까지 z가 t에 없다고 요구할 필요는 없습니다.

관련이 있습니다. 일반적인 몸통 A와 대입 가능한 항 t를 생각해 보세요. M,g⊨∀xA라면 영역의 모든 d에서 몸통이 만족됩니다. 특히 원래 g에서 구한 t의 값도 영역 안에 있으므로 그 d를 고를 수 있습니다. 대입 보조정리는 그 몸통 평가를 M,g⊨A[t/x]로 옮겨 줍니다.

네. 모든 항값이 D 안의 대상이므로 양화사가 살피는 후보로 사용할 수 있습니다. 이 설명은 대입 가능성 조건도 함께 유지합니다. 전칭 도입이나 존재 제거의 새 이름 조건까지 자동으로 해결한 것은 아니며, 그 규칙들의 참 보존은 이후에 별도로 살펴보겠습니다.

좋습니다. 아래 문제는 모두 1절의 기본 M,g를 사용합니다. 먼저 자유로운 x의 자리, 다음으로 넣을 항의 변수, 마지막으로 그 자리까지 지나는 양화사를 확인하세요. 조건을 충족하면 식을 바꾸고 원래 배정에서 계산합니다.

각 작업이 무엇을 바꾸는지 적어 보세요. 특히 대입 보조정리의 두 변에서 식과 배정 중 어느 쪽이 바뀌었는지를 찾아보면, “같은 뜻”이라는 말을 너무 넓게 쓰는 실수를 줄일 수 있습니다.

이번에는 한 규칙의 작은 조건이 왜 필요한지 의미에서 확인했습니다. 다음 편에서는 명제논리의 추론 규칙 하나하나가 참을 보존하는지 살펴보고, 그 사실을 증명 전체의 길이에 대한 귀납으로 이어 보겠습니다. 양화 규칙 전체의 참 보존을 살필 때에도 오늘의 대입 보조정리가 다시 쓰입니다.