참가자가 몇 명인지 몰라도, 각자 아는 내용을 논리로 검사할 수 있을까요?

민서와 준호가 회의에 참석했습니다. 민서는 지우의 참석을 알고, 준호는 민서의 참석을 안다고 합시다. 이름을 하나씩 적으면 현재 두 사람의 지식은 기록할 수 있습니다. 참가자가 바뀔 때마다 모두에게 적용할 조건도 다시 적어야 할까요?

“모든 참가자 x에게, x가 참석을 알고 있는 사람 y가 있다”라고 쓰면 참가자 수를 미리 정하지 않아도 됩니다. 여기서 변수는 사람을 가리킬 자리를 나타내는 x, y이고, 양화는 그 자리를 “모든 사람” 또는 “어떤 사람”에 대해 읽게 하는 일입니다.

이 논문은 사람을 나타내는 변수를 “누구의 관점에서 가능한가”를 표시하는 자리에도 넣습니다. 이런 언어를 항 양상논리라고 부릅니다. 연구의 핵심 질문은 이 언어에서 두 변수로 적은 조건을 만족하는 상황이 있는지 항상 판정할 수 있느냐는 것입니다.

민서는 초대장만 보았고 준호는 출석표까지 보았다고 합시다. 민서가 가진 정보로는 “지우 참석”과 “지우 불참”이 모두 가능합니다. 준호에게는 “지우 참석”만 가능합니다. 이런 현재 정보와 양립하는 상황을 가능세계로 나타냅니다.

P(y)를 “y가 참석했다”로 읽겠습니다. □ₓP(y)는 x가 가능하다고 보는 모든 상황에서 y가 참석했다는 뜻입니다. ◇ₓP(y)는 그중 적어도 한 상황에서 y가 참석했다는 뜻입니다. 아래첨자 x가 누구의 상황들을 검사할지 정합니다.

따라서 ∀x∃y□ₓP(y)는 “각 참가자마다, 모든 관련 상황에서 참석한 사람 하나를 고를 수 있다”로 읽습니다. 사람마다 고르는 y는 달라도 됩니다. 이 사례는 기호의 뜻을 보여 주는 편집부 모형입니다. 논문의 일반 접근 관계에 지식의 성질을 추가할 때는 그 조건을 따로 검토해야 합니다.

모형은 논리식을 검사할 수 있도록 대상과 관계를 정한 구조입니다. 앞의 회의에서는 참가자, 가능한 출석 상황, 각 참가자가 가능하다고 보는 상황, 상황별 참석 여부를 적습니다.

원문은 이 요소를 W, D, δ, R, ρ로 구별합니다. 이 기호를 외우기보다 무엇을 기록하는지 표와 연결해 읽으면 됩니다. 현재 상황에서 변수가 가리킬 사람은 그 상황의 참가자 집합 안에서 고릅니다.

x와 y는 여러 사람을 차례로 가리킬 수 있습니다. 참가자가 백 명이어도 “각 x에게 어떤 y가 있다”라고 적을 수 있습니다. 두 변수 제한은 식에 쓰는 서로 다른 변수 기호를 x, y로 제한한다는 뜻입니다.

안쪽의 ∃x가 x를 다시 묶으면 그 범위에서는 새로 선택한 사람을 가리킵니다. 바깥 x가 가리키던 사람까지 계속 기억하려면 다른 변수가 필요할 수 있습니다. 버튼을 눌러 식에 등장하는 변수 이름을 세어 보세요.

TML은 일차논리를 포함하므로 일반 만족가능성 문제는 결정불가능합니다. 단항 술어만 쓰거나 문법을 조금 줄여도 결정불가능성이 남는 조각이 알려져 있습니다.

그래서 저자들은 일차논리에서 잘 알려진 두 변수 조각 FO²를 출발점으로 삼습니다. 양상 색인을 더한 TML²도 같은 성질을 가질지는 자동으로 따라오지 않습니다.

여기서 만족가능은 조건에 맞는 모형이 하나라도 있다는 뜻입니다. “모두 참석했고, 누군가는 불참했다”는 두 조건은 같은 참석 기준으로 함께 만족시킬 수 없습니다. 결정 절차는 이런 가능 여부를 입력된 모든 식에 대해 끝내 답하는 절차입니다. 특정 회의 기록의 사실 확인과 구별해 읽어야 합니다.

두 변수 일차 양상논리 FOML²는 결정불가능합니다. 그 증명에는 보통 두 자유변수를 가진 식 전체에 자유 양상 □를 씌우는 표현이 쓰입니다.

TML²에서 양상은 반드시 x나 y로 색인됩니다. 제3의 변수 z가 없으면 두 자유변수 x,y를 그대로 둔 채 ∀z□ᶻP(x,y)처럼 자유 양상을 흉내 내기 어렵습니다. 이 표현력의 빈틈이 결정가능성 논증의 핵심입니다.

FO²는 “일차논리에서 변수 두 개만 쓰는 부분”, FOML²는 거기에 □를 더한 부분을 줄여 쓴 이름입니다. 여기서 자유 양상은 행위자 아래첨자가 없는 □를 뜻합니다. 이 차이는 결과를 이해하는 단서이며, 결정가능성 자체는 뒤의 모형 구성으로 증명합니다.

모든 상황에서 같은 참가자 집합을 사용하면 상수 영역 모형입니다. 접근 가능한 다음 상황에서 기존 참가자를 유지하면서 새 참가자를 더할 수 있으면 증가 영역 모형입니다. 이때 영역은 논리식이 사람을 선택하는 범위입니다.

예를 들어 {민서, 준호}에서 {민서, 준호, 지우}로 커지는 것은 증가 조건에 맞습니다. {민서}로 줄어드는 변화는 이 조건에 맞지 않습니다. 두 모형의 만족가능성은 논문의 번역을 통해 연결됩니다.

새 단항 술어 E를 넣어 “이 행위자가 이 세계에 존재한다”를 표시합니다. ∃xφ는 ∃x(E(x)∧Tr(φ))로 바꾸고, 양상 깊이만큼 E의 단조성을 보장하는 γφ를 덧붙입니다.

아래 활동은 번역이 양화 대상의 현재 존재를 놓치지 않는지 확인합니다. E를 빼면 미래에만 나타날 행위자를 현재의 증인으로 잘못 고를 수 있습니다.

E(x)는 참가자 명단에 체크하는 표시로 생각할 수 있습니다. 전체 목록에 지우가 있어도 현재 명단의 E(지우)가 거짓이면 지금의 ∃x에서 지우를 답으로 고를 수 없습니다. Tr(φ)는 원래 조건 φ를 새 언어로 옮긴 식을 뜻합니다. γφ는 접근을 따라 이미 존재하던 사람이 계속 존재한다는 조건을 필요한 깊이까지 붙인 식입니다.

논문은 Fine의 양상 정규형과 Scott의 FO² 정규형을 결합합니다. 양상 부분은 □ₓ·◇ₓ 및 □ᵧ·◇ᵧ의 요구를 묶고, 일차 부분은 ∀x∀yφ와 ∀x∃yψ 꼴의 요구를 모읍니다.

중간에는 한 변수만 양화되고 다른 변수가 자유인 식도 있어 이를 처리하는 항이 추가됩니다. 변환은 원식과 문법상 같아지는 것이 아니라 만족가능성이 같은 정규형을 만듭니다.

정규형은 검사할 요구를 일정한 형식으로 정돈한 식입니다. 예를 들어 “모든 x에게 y가 필요하다”는 요구와 “x의 모든 후속 상황에서 지켜야 한다”는 요구를 구별해 놓으면, 모형을 만들 때 사람과 상황 중 무엇을 더 마련해야 하는지 확인할 수 있습니다. 파인–스콧은 이 정돈 방법에 사용된 두 연구자의 이름입니다.

1-유형은 한 행위자에 관해 필요한 정보를 모으고, 2-유형은 두 행위자가 등장하는 조건에 필요한 정보를 모읍니다. 세계마다 필요한 유형과 존재 증인을 기록하면 개체를 전부 복사하지 않아도 됩니다.

같은 유형을 가진 행위자들이라도 ∀x∃y 요구의 증인 역할과 접근 관계의 대표 역할은 구분해야 합니다. 원문은 유형 수와 정규형의 존재 요구를 함께 계산합니다.

여기서 유형은 직업이나 성격 분류가 아닙니다. 검사 중인 식이 구별하는 정보의 묶음입니다. 두 사람이 현재 같은 참석 정보를 갖더라도 다른 상황으로 이어지는 관계나 필요한 상대가 다르면 그대로 합칠 수 없습니다. 원문의 유형 구성은 이런 양상 정보와 증인 역할까지 관리합니다.

정규형이 어떤 모형에서 만족된다면, 식의 크기와 유형 수로 계산되는 유한한 수의 행위자만 가진 모형에서도 만족된다는 성질입니다. 세계 수까지 곧바로 작다는 뜻은 아닙니다.

저자들은 양상 깊이에 따라 내려가며 각 세계에 필요한 유형 대표와 존재 증인을 보존합니다. 들어오는 접근 관계의 색인도 대표 선택에 포함해 진리값이 바뀌지 않게 합니다.

설명용으로 행위자 집합을 {a, b}로 고정해 봅시다. “모든 x가 P(x)”라는 조건은 P(a)와 P(b)를 모두 검사하는 것으로 바뀝니다. “어떤 x가 P(x)”는 둘 중 하나가 성립하는지 검사합니다.

논문의 증명은 필요한 행위자 수에 계산 가능한 상한을 주고, 유한한 이름으로 양화사를 펼쳐 명제 다중 양상논리의 판정 절차로 연결합니다. a, b는 이 설명에서 모형의 대상을 부르는 표지입니다. 원래 언어에 상수 기호를 임의로 추가한다는 뜻은 아닙니다.

논문이 제시한 상한은 2-EXPSPACE이고, FO² 만족가능성을 줄일 수 있어 NEXPTIME 하한이 나옵니다. 두 경계 사이가 벌어져 있어 정확한 복잡도는 이 논문에서 닫히지 않습니다.

아래 활동은 세 문장을 구분합니다. 결정가능성과 효율성, 그리고 정확한 복잡도 분류는 서로 다른 주장입니다.

2-EXPSPACE는 입력 길이에 대해 이중 지수 규모의 작업 공간을 허용하는 복잡도 등급이고, NEXPTIME은 비결정적 계산에서 지수 시간으로 표현되는 등급입니다. 이 논문은 그 사이에 문제의 난도가 놓인다고 보입니다. 현재의 결과만으로 빠른 실무 도구가 된다고 결론 내릴 수는 없습니다.

언어는 참가자가 계속 생기는 회의, 클라이언트가 드나드는 서버, 플레이어 수가 정해지지 않은 게임을 표현할 동기를 줍니다. 그러나 원문 결과는 이런 시스템의 성능이나 안전을 자동으로 증명하지 않습니다.

실제 적용에는 어떤 접근 관계가 지식·권한·통신을 뜻하는지, 행위자 영역이 상수인지 증가하는지, 등식과 상수를 제외해도 요구를 표현할 수 있는지 먼저 정해야 합니다.

참가자 수를 미리 정하지 않아도, 논문이 정한 두 변수 언어에서는 조건을 만족하는 모형의 존재 여부를 판정할 수 있습니다. 핵심은 필요한 사람과 관계를 보존하면서 검사 범위를 유한하게 줄이는 증명입니다.

적용 범위도 함께 적어야 합니다. 이 결과는 등식과 상수가 없는 두 변수 조각을 다룹니다. 사람의 고정 이름을 상수로 추가하거나 접근 관계에 새로운 조건을 붙이면 판정 가능성을 다시 확인해야 합니다. 앞의 회의 사례는 이런 표현과 검사 범위를 이해하기 위한 예입니다.