문을 여는 열쇠가 있다는 것과, 어느 열쇠인지 아는 것은 어떻게 다를까요?

같은 문에 빨간 열쇠가 맞는지 파란 열쇠가 맞는지 아직 모른다고 합시다. 가능한 상황은 두 가지입니다. 첫 상황에서는 빨강만 맞고, 둘째 상황에서는 파랑만 맞습니다. 두 상황 모두 열쇠가 하나 있지만, 지금 하나를 집어 확실히 맞는다고 할 수는 없습니다.

논리학에서는 이렇게 현재 정보로 구별하지 못하는 상황들을 놓고 지식을 검사합니다. 어느 상황에서도 같은 답이 통하는지가 이 글의 질문입니다. 왕옌징의 논문은 그 답을 고르는 일과 모든 관련 상황에서 확인하는 일을 하나의 기호로 묶어 연구합니다.

P(x)를 “열쇠 x로 이 문이 열린다”로 정하겠습니다. ∃x는 “어떤 x가 있다”, □는 “현재 가능하다고 보는 모든 상황에서”로 읽습니다. 이 사례에서 □P(x)는 고정한 열쇠 x가 모든 관련 상황에서 문을 연다는 뜻입니다.

∃x□P(x)는 먼저 열쇠 하나를 고른 뒤 모든 상황에서 그 열쇠를 검사합니다. 논문의 □ˣP(x)는 이 두 연산을 묶은 표기입니다. □는 이 사례에서 지식으로 해석하며, 논문은 더 일반적인 접근 관계도 다룹니다.

이번에는 빨간 열쇠가 상황 A와 B에서 모두 문을 연다고 합시다. 파란 열쇠는 B에서만 맞습니다. 빨강을 골라 두 행을 확인하면 ∃x□P(x)를 만족하는 답을 찾은 것입니다.

상황 A와 B 중 무엇이 실제인지 몰라도, 빨강이 맞는다는 사실은 압니다. 모든 상황에서 확인한 대상은 같은 빨간 열쇠입니다. “같은 답”이라는 조건을 표의 한 열을 끝까지 읽는 것으로 확인할 수 있습니다.

□∃xP(x)는 각 상황 안에서 열쇠를 찾습니다. 상황 A에서는 빨강, B에서는 파랑을 골라도 됩니다. ∃x□P(x)는 상황들을 검사하기 전에 하나를 고르므로 모든 행에서 같은 열쇠가 맞아야 합니다.

1번 문답의 표는 □∃xP(x)가 참이면서 ∃x□P(x)가 거짓인 예입니다. 이런 예를 반례라고 합니다. “각 상황에 답이 있다면 공통 답도 있다”라는 추론이 성립하지 않음을 보여 줍니다.

민서는 초대된 사람이고, 준호가 초대되었는지는 모른다고 합시다. 이때 “초대된 사람 한 명을 말해 달라”에는 민서라고 답할 수 있습니다. “누가 초대되었는지 전부 알려 달라”에는 정보가 부족합니다.

앞의 읽기를 한 답을 아는 읽기(mention-some), 뒤의 읽기를 모든 관련 대상의 해당 여부를 아는 읽기(mention-all)라고 부릅니다. □ˣ Invited(x)는 앞의 요구를 표현합니다. Invited(x)는 x가 초대되었다는 뜻입니다. 질문이 요구하는 답의 범위를 먼저 정해야 정확하게 형식화할 수 있습니다.

논문의 기본 모형은 증가 영역을 허용합니다. 현재 고를 수 있는 대상이 다음 접근 상황에서도 남아 있고, 새 대상은 추가될 수 있습니다. 따라서 처음부터 모든 상황의 대상 집합이 같다고 가정하는 것은 아닙니다.

반면 지식을 S5라는 조건으로 다루는 부분에서는 서로 접근 가능한 상황들의 대상 집합이 같아집니다. 한쪽으로 갈 때도, 반대쪽으로 갈 때도 대상 집합이 포함되어야 하기 때문입니다. 앞의 열쇠 예에서는 비교를 쉽게 하려고 두 열쇠를 모든 상황에서 공통으로 사용했습니다.

논문은 ∃□-bisimulation을 정의해 원자식의 일치와 함께 후보 선택과 세계 이동을 맞춥니다. 한쪽에서 대상을 고르고 세계를 옮기면 다른 쪽도 대응 선택과 이동을 해야 합니다.

이 관계로 연결된 지점은 새 언어의 같은 식을 만족합니다. 표현력이 무엇을 구별하고 무엇을 보지 못하는지를 구조적으로 설명합니다.

서로 다른 두 표가 같은 질문에 늘 같은 답을 주는지 살펴보는 일입니다. 쌍모사(bisimulation)는 단순히 행 수를 맞추는 것이 아니라, 대상 선택과 가능한 상황의 이동을 서로 대응시키는 관계입니다. 이 관계의 정확한 선택 순서가 원문 정의에 들어 있습니다.

예를 들어 “맞는 열쇠 하나를 알지만, 파랑은 틀릴 수도 있다”를 검사한다고 합시다. 빨강을 공통 답으로 두고, 파랑이 안 맞는 상황을 하나 마련하면 두 요구가 함께 가능한지 살펴볼 수 있습니다.

원문의 판정 절차는 필요한 증인과 반례를 체계적으로 마련하는 방식입니다. 증인은 존재 요구를 충족하는 대상이고, 반례 상황은 모든 경우에 성립한다는 주장을 깨는 상황입니다. 등호 없는 기본 언어의 유한 나무 모형 결과가 이 절차를 뒷받침합니다.

동일성 기호가 없는 기본 언어의 만족가능성 문제는 임의 모형에서 PSPACE 완전입니다. 기본 명제 양상논리와 같은 복잡도 등급을 유지한다는 점이 결과의 장점입니다.

표현력이 늘었다고 계산이 항상 한 단계 더 어려워지는 것은 아닙니다. 다만 이 결론은 논문이 정한 언어와 모형 조건에 붙어 있습니다.

PSPACE는 입력 길이의 다항식만큼 작업 공간을 쓰는 계산으로 해결할 수 있는 문제들의 등급입니다. 완전하다는 말에는 그 등급의 다른 문제만큼 어렵다는 하한도 포함됩니다. 실제 실행 시간이 짧다는 뜻과는 구별해야 합니다.

S5는 지식을 이상화해서 다루는 논리 체계입니다. 아는 것은 참이고, 자신이 아는지 모르는지도 안다는 강한 조건을 둡니다. 모형에서는 가능한 상황을 잇는 관계를 동치관계로 정합니다.

동치관계는 자기 자신과 연결되고, 연결을 거꾸로 따라갈 수 있고, 두 연결을 이어 갈 수 있는 관계입니다. 이 조건 아래에서 논문은 □와 □ˣ를 함께 다루는 공리와 증명 규칙을 제시합니다. 실제 사람의 모든 앎이 이 이상화에 맞는다고 가정해서는 안 됩니다.

등호를 허용하면 x≈y로 두 변수가 같은 대상을 가리킨다고 적습니다. 예를 들어 x와 y에 모두 빨간 열쇠를 배정했다면 P(x)와 P(y)는 같은 열쇠에 대한 조건입니다. 원문은 이 동일성과 대입을 다루는 공리를 제시합니다.

여기서 빨강과 파랑은 설명을 위해 대상에 붙인 이름입니다. 논문의 기본 언어는 상수 기호와 함수 기호를 제외합니다. 일상적인 고유 이름까지 원문이 모두 분석했다고 소개하면 연구 범위를 넘어섭니다.

건전성은 규칙으로 증명한 식이 모형에서도 타당하다는 성질이고, 완전성은 모든 타당식을 그 규칙으로 증명할 수 있다는 성질입니다. 모든 입력의 가능 여부를 유한 시간 안에 판정한다는 성질은 별도로 확인해야 합니다.

논문은 등호 없는 기본 언어를 임의의 증가 영역 모형에서 검사하는 경우와, S5 조건을 부여한 지식 언어를 구별합니다. 후자의 일반 만족가능성은 결정불가능하다는 결과를 보입니다. 등호를 추가해야만 그 어려움이 생기는 것도 아닙니다.

먼저 한 답이면 충분한지, 모든 답을 알아야 하는지 정합니다. 다음으로 같은 답이 모든 가능세계에서 유지되어야 하는지, 세계마다 다른 답도 허용하는지 살핍니다.

아래 활동은 형식화 전에 자연어의 읽기를 고르는 절차입니다. 번역을 먼저 고정하면 서로 다른 질문을 같은 기호로 덮을 수 있습니다.

상황마다 맞는 열쇠가 있어도 그 열쇠가 달라지면 지금 공통 답을 고를 수 없습니다. 빨간 열쇠가 모든 관련 상황에서 맞으면, 실제 상황을 아직 구별하지 못해도 빨강을 선택할 수 있습니다.

이 차이를 ∃와 □의 순서로 표현하고, 어떤 조건에서 그런 문장을 검사할 수 있는지 따지는 것이 이번 논문의 논리학적 질문입니다. 자연어를 옮길 때는 답 하나가 필요한지, 전체 목록이 필요한지, 어떤 상황과 대상을 비교할지 함께 정해야 합니다.