두 규칙에서 한 조건을 지우면, 왜 새로운 결론이 따라올까요?

P처럼 원자 문장을 그대로 쓰거나 ¬P처럼 그 부정을 쓴 것을 리터럴이라고 부릅니다. 여러 리터럴을 ∨로 잇는 한 묶음이 절(clause)입니다. P∨Q와 ¬P∨R은 각각 절이고, P 하나만으로도 절을 만들 수 있습니다. 이 글의 앞부분에서는 P·Q·R의 참과 거짓만 다룹니다.

여러 절을 목록에 나란히 두면 그 목록의 모든 절을 만족해야 한다고 약속합니다. 따라서 한 절 안의 ∨와 절 목록 사이의 ‘그리고’를 구별해야 합니다. [P∨Q, ¬P∨R]은 두 문장을 모두 요구합니다. 이를 P∨Q∨¬P∨R 한 문장으로 합치면 요구가 약해져 다른 문제가 됩니다.

이처럼 모양을 맞추면 컴퓨터는 상보적인 리터럴 P와 ¬P를 찾고, 나머지 리터럴을 모으는 일정한 절차를 실행할 수 있습니다. 임의의 자연어를 자동으로 정확한 절로 바꾸었다는 뜻은 아닙니다. 무엇을 P로 표현했는지와 어떤 규칙을 전제로 삼았는지는 사람이 먼저 확인해야 합니다.

P가 참인 경우부터 보겠습니다. 둘째 전제 ¬P∨R에서 ¬P는 거짓이 됩니다. 그런데 그 전제를 참으로 놓았으므로 R이 참이어야 합니다. 따라서 Q가 무엇이든 Q∨R은 참입니다. P가 참인 갈래에서는 둘째 전제가 결론을 지켜 줍니다.

P가 거짓인 경우에는 첫째 전제 P∨Q가 Q를 참으로 만듭니다. 그러면 R의 값을 몰라도 Q∨R이 참입니다. 고전적인 두 값 논리에서 P는 참 또는 거짓이므로 두 경우를 모두 확인했습니다. 두 전제가 함께 참인데 결론만 거짓인 경우는 없습니다.

이 성질이 추론 규칙의 건전성입니다. 결론이 우연히 맞는 입력 한 개를 찾았다는 뜻이 아니라, 전제를 함께 만족하는 모든 입력에서 결론이 참이라는 뜻입니다. 다음 실험은 여덟 가지 P·Q·R 값을 직접 바꾸면서 이 구별을 보여 줍니다.

그렇게 하면 정보가 줄어들 수 있습니다. P=참, Q=참, R=거짓을 넣어 보세요. Q∨R은 참이지만 ¬P∨R은 거짓입니다. 새 결론을 만족한다고 해서 원래 두 전제를 모두 만족하는 것은 아닙니다. 앞에서 증명한 방향을 거꾸로 읽을 수 없습니다.

해소에서 안전한 기본 조작은 원래 절들을 보존하면서 그 절들에 따라오는 해소절을 추가하는 것입니다. 원래 절들의 모형, 곧 그 절들을 모두 참으로 만드는 값 배정은 추가한 해소절도 만족합니다. 그래서 절을 추가해도 원래 문제를 만족하는 배정을 잃지 않습니다.

추론 프로그램을 읽을 때에는 ‘따라오는 문장’과 ‘동치인 대체식’을 구별해야 합니다. 특정한 삭제 전략에는 별도의 정당화가 필요합니다. 이 글의 실험은 이전 절을 지우지 않고 번호와 부모 절을 남겨, 매 단계의 근거를 되짚을 수 있게 합니다.

P와 ¬P를 각각 하나의 절로 함께 요구해 보겠습니다. 두 절을 해소하면 남길 리터럴이 없어서 빈 절 []을 얻습니다. 절은 안에 든 리터럴 가운데 적어도 하나가 참이어야 만족됩니다. 빈 절에는 참이 될 리터럴이 하나도 없으므로 어떤 배정도 빈 절을 만족하지 못합니다.

따라서 참을 보존하는 해소를 통해 빈 절을 얻었다면, 출발한 절들을 모두 만족하는 배정이 없다는 결론을 내릴 수 있습니다. 만약 그런 배정이 있었다면 모든 해소절을 만족해야 하고 결국 빈 절도 만족해야 해서 모순이 생기기 때문입니다.

‘빈 절 하나가 있는 목록’과 ‘절이 하나도 없는 목록’은 반대 상황입니다. 요구할 절이 전혀 없는 빈 목록은 어떤 배정도 어기지 않습니다. 반면 빈 절이 들어 있는 목록은 만족할 수 없는 조건을 포함합니다. 화면에서는 빈 절을 []이라고 명시해 이 둘을 섞지 않겠습니다.

원래 세 전제 P∨Q, ¬P∨R, ¬Q∨R에서 R이 따라오는지 묻습니다. 원래 전제들을 모두 만족하면서 R만 거짓인 배정이 존재한다면 R은 보장되지 않습니다. 그러므로 전제 목록에 ¬R을 추가해 그런 배정이 가능한지 조사할 수 있습니다.

추가한 목록에서 빈 절이 나오면 원래 전제와 ¬R을 동시에 만족하는 배정은 없습니다. 따라서 원래 전제를 만족하는 배정에서는 R이 참입니다. 이런 방식이 반박에 의한 증명입니다. 목표를 일단 부정했기 때문에, 마지막의 모순이 무엇을 부정하는지 정확히 따라가야 합니다.

원래 전제 자체가 모순인 경우에도 이 절차는 빈 절에 도달할 수 있습니다. 이때 형식적으로 R이 따라오더라도 전제의 현실적인 적절성이 확보된 것은 아닙니다. 지금의 세 전제는 예를 들어 P=참, Q=거짓, R=참에서 함께 만족됩니다. 출발 조건의 일관성도 따로 확인할 수 있습니다.

먼저 ¬P∨R과 ¬R을 해소하면 ¬P가 됩니다. ¬Q∨R과 ¬R을 해소하면 ¬Q가 됩니다. 행사 허가를 부정한 가정 아래에서는 실내 승인도 야외 승인도 없다는 결과가 나온 것입니다. 각 단계에서는 R과 ¬R 한 쌍만 연결했습니다.

이제 첫 전제 P∨Q와 방금 얻은 ¬P를 해소하면 Q가 남습니다. 그런데 앞에서 ¬Q도 얻었으므로 Q와 ¬Q를 해소해 빈 절을 얻습니다. 이 네 번의 추론이 원래 전제에 ¬R을 추가한 목록의 불만족성을 보여 줍니다.

실험은 모든 가능한 부모 쌍을 일정한 순서로 검사하므로 화면의 증명 순서는 이 설명과 다를 수 있습니다. 중요한 것은 각 행의 부모 번호, 없앤 상보 리터럴, 새 절이 규칙에 맞는지입니다. 같은 결론에 이르는 다른 해소 경로도 검산할 수 있습니다.

¬Q∨R을 빼고 P∨Q, ¬P∨R, ¬R만 남겨 보겠습니다. P=거짓, Q=참, R=거짓이면 세 절이 모두 참입니다. 야외 승인은 있지만 그 승인이 행사 허가로 이어진다는 규칙이 사라졌기 때문에 이런 배정이 가능합니다.

이 배정은 남은 전제가 R을 보장하지 않는다는 반례입니다. 단순히 프로그램이 아직 빈 절을 못 찾았다는 보고보다 강한 근거입니다. 값을 각 절에 대입해서 누구나 동시에 참이 되는지 검산할 수 있기 때문입니다.

두 번째 실험에서 ‘야외 승인 규칙 포함’을 끄면 이런 배정과 해소 기록이 함께 나옵니다. ‘목표의 부정 ¬R 추가’를 끄면 원래 전제 자체의 만족 여부를 조사하게 됩니다. 어떤 질문을 계산 중인지 입력 목록을 보며 구별하세요.

이 실험에는 P·Q·R 세 원자만 있습니다. 해소는 새로운 원자를 만들어 내지 않습니다. 같은 리터럴의 중복은 지우고 P와 ¬P를 함께 가진 항진적인 절은 제외합니다. 그러면 각 원자는 한 절에서 긍정 리터럴로 있거나, 부정 리터럴로 있거나, 아예 없거나 하는 세 상태 가운데 하나입니다.

따라서 빈 절까지 포함해 서로 다른 절은 최대 3³=27개입니다. 이미 가진 절은 다시 추가하지 않고, 가능한 부모 쌍과 연결 원자를 모두 검사하면 결국 새 절이 더 생기지 않습니다. 빈 절이 먼저 나오면 불만족이고, 완전히 포화되었는데도 빈 절이 없으면 이 유한 명제 문제는 만족 가능합니다.

화면은 별도로 여덟 가지 진리 배정을 모두 검사해 만족하는 배정도 제시합니다. 해소 기록과 진리표 검사가 같은 결론을 내리는지 대조할 수 있습니다. 이 종료 설명은 원자가 세 개로 고정된 이번 계산에 관한 것이며, 곧 나올 함수 기호가 있는 일반 1차 논리에 그대로 옮길 수 없습니다.

1차 논리에서는 문장 안에 대상과 변수, 함수가 들어갑니다. P(a)는 대상 a가 성질 P를 가진다는 식이고 P(x)는 변수 x를 가진 식입니다. 해소하려는 두 리터럴의 부호가 반대여도, 안쪽 원자식이 적절한 치환 아래 같아지는지 먼저 확인해야 합니다. 이 절 표기에서는 나타난 변수를 해당 절 전체에 전칭으로 묶어 읽습니다. 따라서 Q(x)는 모든 대상에 관한 주장이며, Q(a)는 특정 상수 a에 관한 주장입니다.

예를 들어 P(a)와 ¬P(x)∨Q(x)를 연결하려면 x에 a를 넣습니다. 그 치환은 P(x) 안에만 적용하는 것이 아니라 같은 절의 Q(x)에도 적용해야 하므로 남는 절은 Q(a)입니다. Q(x)를 그대로 두면 원래보다 넓은 대상을 말하게 되어 추론이 틀릴 수 있습니다.

서로 다른 부모 절에서 우연히 같은 변수 이름을 썼다면, 원전의 절차는 먼저 변수들을 구분되도록 바꿉니다. 서로 독립적인 변수의 이름이 같다는 이유로 동일한 대상을 강제해서는 안 됩니다. 그 뒤 필요한 치환을 계산하는 작업을 단일화(unification)라고 합니다.

두 식의 바깥 술어가 P이고 인수가 두 개씩이므로 첫 인수끼리, 둘째 인수끼리 맞춥니다. 첫 인수 x와 a가 같아지려면 x에 a를 넣어야 합니다. 그 치환을 적용하면 둘째 인수 f(x)는 f(a)가 됩니다. 따라서 y에는 f(a)를 넣습니다.

결과는 {x↦a, y↦f(a)}이고 두 식은 모두 P(a,f(a))가 됩니다. x를 바꾼 뒤에도 y를 이전의 f(x)와 독립적으로 취급하면 안 됩니다. 치환들이 서로에게 미치는 영향을 반영해 마지막 형태를 정리해야 합니다.

가장 일반적인 단일화는 필요한 일치만 강제하고 불필요한 추가 조건을 넣지 않는다는 생각입니다. 이 예에서는 상수 a와 함수 f가 정해져 있으므로 두 대입이 그대로 결정됩니다. 원전의 일반 단일화 정리는 이 한 예보다 넓습니다. 아래 실험은 정해 둔 유한 항들의 비교 과정을 보여 줍니다.

유한한 항을 사용하는 지금의 문법에서는 x와 f(x)를 같은 항으로 만들 수 없습니다. x에 어떤 유한 항 t를 넣으면 오른쪽은 f(t)가 됩니다. f(t)는 t를 한 겹 더 감싼 구조이므로 t와 동일한 유한 구문 트리가 아닙니다.

그래서 변수를 어떤 항으로 바꾸기 전에 그 항 안에 같은 변수가 들어 있는지 검사합니다. 이를 출현 검사(occurs check)라고 합니다. x↦f(x)를 무심코 허용하면 치환을 펼칠 때 f(f(f(…)))처럼 끝이 없는 구조를 요구하게 됩니다.

이 실패는 방정식의 실수 해가 없다는 말과 다릅니다. f가 어떤 수학 함수인지 해석한 뒤 f(t)=t의 해를 구하는 문제와, 해석하기 전 유한 기호 표현을 동일하게 만드는 문제는 서로 다릅니다. 다음 고정점 글을 읽을 때에도 ‘같아진다’의 기준을 먼저 확인해 보세요.

명제 실험에서는 두 절에서 상보적인 리터럴 한 쌍을 고르면 충분했습니다. 1차 논리의 일반 완전성 결과를 설명할 때에는 이 화면의 작은 규칙만 그대로 가리키면 안 됩니다. 변수의 이름을 분리하고, 치환을 절 전체에 적용하며, 같은 방향의 리터럴을 단일화해 묶는 처리도 필요합니다.

로빈슨의 원전은 부모 절에서 비어 있지 않은 리터럴 부분집합들을 선택하고, 부호를 맞춘 원자식들을 가장 일반적으로 단일화하는 일반화된 해소절을 정의합니다. 현대적인 제시에서는 이 역할을 이항 해소와 인수분해(factoring) 규칙으로 나누어 설명하기도 합니다. 정확히 어떤 체계를 쓰는지에 따라 완전성 주장의 대상이 달라집니다.

이 글의 세 번째 실험은 단일화 계산만 담당합니다. 첫째·둘째 실험의 명제 해소와 결합해 범용 1차 증명기를 완성한 것은 아닙니다. 예제의 성공을 원전 전체 정리의 구현 검증으로 오해하지 않도록, 계산하는 언어와 규칙을 나누어 적습니다.

반박 완전성은 불만족인 절 집합에 대해 필요한 해소 반박이 존재한다는 성질입니다. 그 증명을 실제 탐색으로 찾으려면 특정 후보를 영원히 건너뛰지 않는 공정한 탐색도 필요합니다. 증명이 있다는 사실과 어느 전략이 얼마나 빨리 찾는지는 별도의 문제입니다.

함수 기호가 있으면 Q(a), Q(f(a)), Q(f(f(a)))처럼 점점 깊은 항이 생길 수 있습니다. Q(a)와 ¬Q(x)∨Q(f(x))는 이런 연쇄를 만들지만, Q가 모든 대상에서 참인 해석으로 만족할 수 있습니다. 새 결과가 계속 나오는 상황을 이번 세 원자의 27절 경계로 제한할 수 없습니다.

따라서 일반 1차 논리에서는 일정 시간 동안 빈 절이 나오지 않았다는 이유만으로 만족 가능하다고 판정해서는 안 됩니다. 유한 명제 실험의 완전 포화, 실제 반례 해석의 제시, 일반 탐색의 시간 제한은 서로 다른 종료 사유입니다. 화면이나 보고서는 어떤 사유로 멈췄는지 알려 주어야 합니다.

첫째, 입력한 절 목록과 목표의 부정을 확인합니다. 자연어의 조건이 빠졌거나 ∨와 ‘모두’를 혼동하면 프로그램이 계산을 정확하게 해도 다른 질문에 답하게 됩니다. 야외 승인 규칙을 뺐을 때 반례가 생긴 이유가 여기에 있습니다.

둘째, 각 해소절의 부모와 연결 원자, 필요한 치환을 확인합니다. 결론만 ‘증명됨’이라고 써 있는 것보다 번호가 붙은 추론 기록이 검토에 도움이 됩니다. 단일화에서 같은 변수의 모든 출현을 함께 바꾸었는지, 출현 검사를 통과했는지도 확인할 수 있습니다.

셋째, 결과의 범위를 기록합니다. 이번 실험의 포화는 P·Q·R에 한정된 계산이고, 단일화 실험은 유한 항에 한정됩니다. 우리는 ‘공통된 말을 지운다’는 첫 직관을 전제를 보존하는 해소 규칙, 실제 반박 기록, 치환 조건으로 나누어 검산했습니다. 이 기록이 있어야 다른 사람이 같은 결론을 재현할 수 있습니다.