A non-uniform view of Craig interpolation in modal logics with linear frames

이 논문은 K4.3을 확장하는 일반적인 양상 논리들이 일반적으로 크레이그 보간 성질(Craig interpolation property)을 결핍하고 있음에도 불구하고, 임의의 주어진 두 공식에 대해 크레이그 보간자가 존재하는지 여부를 결정하는 특정 문제는 결정 가능하며 coNP-완비(coNP-complete)라는 점을 입증하며, 이 결과는 표준 선형 시간 흐름에 대한 프리오(Priorean) 시간 논리에도 확장 적용된다.

핵심

당신이 두 명의 용의자, 공식 A와 공식 B가 연루된 미스터리를 해결하려는 탐정이라고 상상해 보십시오. 당신은 A가 참이면 B도 반드시 참이어야 한다는 사실을 알고 있습니다 (A는 B를 함의합니다).

논리학의 세계에는 **크레이그 보간 성질(Craig Interpolation Property)**이라는 특별한 규칙이 있습니다. 이 규칙은 A가 B를 함의할 때마다, A와 B 사이에서 가교 역할을 하는 '중간자' 문장인 I가 반드시 존재해야 한다고 말합니다. 이 중간자 I는 다음과 같은 매우 구체적인 임무를 수행합니다:

1. I는 A와 B에 공통으로 등장하는 단어(변수)들만을 사용해야 합니다.
2. A는 I를 함의하고, I는 B를 함의해야 합니다.

이 중간자 I를 번역가라고 생각해 보십시오. 만약 A가 "영어"로 말하고 B가 "프랑스어"로 말한다면, 보간자 I는 공통된 언어의 단어들만을 사용하여 A의 의미가 논리적으로 B로 흘러 들어감을 증명하는 문장입니다.

문제: 사라진 다리

많은 논리 체계(표준 수학이나 기초 컴퓨터 논리 등)에서는 이 중간자 I가 항상 존재합니다. 하지만 이 논문의 저자들은 K4.3 및 그 친척 격인, 매우 까다로운 '선형적' 세계를 기술하는 특정 논리 가족을 살펴보고 있습니다. 이 논리들은 시간이 과거에서 미래로 흐르는 단 하나의 직선처럼 움직이는 선형적인 세계를 묘사합니다.

이러한 선형적 세계에서는 "다리 규칙"(크레이그 보간 성질)이 깨집니다. 즉, 때때로 A가 B를 함의함에도 불구하고, 규칙에 부합하는 중간자 문장 I가 존재하지 않는 경우가 발생합니다. 이는 마치 논리는 성립하지만, 공유된 어휘만을 사용하여 그 연결 고리를 요약할 수 있는 단 하나의 문장도 찾을 수 없는 대화를 나누는 것과 같습니다.

보통 어떤 논리가 이 규칙을 깨뜨리면, 연구자들은 손을 들어 올리며 이렇게 말하곤 합니다. "다리가 존재하지 않으니, 우리는 더 이상 이 연결 관계를 연구할 수 없다."

새로운 접근법: "다리가 존재하는가?" 게임

저자들은 "모든 문장 쌍에 대해 다리가 항상 존재하는가?"(그 답은 '아니오'입니다)라는 질문 대신, 더 실용적인 질문을 던지는 '비균일적(non-uniform)' 접근 방식을 취했습니다.

그들은 다음과 같이 물었습니다:
"이 특정한 두 문장 A와 B에 대해서, 다리가 존재하는가?"

이것은 마치 정비사에게 "이 공장의 모든 자동차에 엔진이 있는가?"라고 묻는 대신, "이 특정한 자동차에 작동하는 엔진이 있는가?"라고 묻는 것과 같습니다. 저자들은 이를 **보간자 존재 문제(Interpolant Existence Problem, IEP)**라고 부릅니다.

거대한 발견: 타당성 검사와 난이도가 같다

저자들은 놀라운 사실을 증명했습니다. 비록 이 논리들에서 "다리 규칙"은 깨져 있지만, 특정 문장 쌍에 대해 다리가 존재하는지 알아내는 것은 결코 엄청나게 어렵거나 불가능한 작업이 아니라는 점입니다.

컴퓨터 과학 용어로 말하자면, 다리가 존재하는지 판단하는 난이도는 원래의 문장(A가 B를 함의하는지)이 참인지 확인하는 난이도와 정확히 일치합니다. 그들은 이 복잡도를 coNP-complete라고 부릅니다.

비유:
강을 건너려고 한다고 상상해 보십시오.

• 기존의 관점: "다리가 끊겼으니, 당신은 절대 건널 수 없다."
• 저자들의 관점: "다리는 끊겼지만, 당신을 건너게 해줄 특정한 배가 존재하는지 확인할 수는 있다. 그리고 알고 보니, 그 배가 존재하는지 확인하는 것은 실제로 강이 존재하는지 확인하는 것만큼이나 쉽다."

저자들은 이 선형 논리들에서 다리가 존재하는지 찾아내는 것이 매우 어렵거나 불가능한 일이 아니라, 표준적인 컴퓨터로 효율적으로 처리할 수 있다는 것을 보여주었습니다. 이는 다른 유사한 논리 체계에서 다리의 존재 여부를 밝혀내는 것이 원래 문장의 참/거짓을 판별하는 것보다 훨씬 더 어렵다는 점을 고려할 때 매우 중요한 발견입니다.

방법론: "기술적 프레임(Descriptive Frame)" 지도

이를 해결하기 위해 저자들은 **기술적 프레임(descriptive frames)**이라는 도구를 사용했습니다. 이것은 논리적 세계를 보여주는 매우 상세하고 고해 resolución의 지도라고 상상해 보십시오.

• 때때로 이 지도들은 단순하고 유한한 선의 형태를 띱니다.
• 때로는, 머리와 무한한 꼬리를 가진 "올챙이" 모양처럼, 클러스터(점들의 집단)로 이루어진 무한한 사슬이 영원히 뻗어 나가는 형태를 띠기도 합니다.

저자들은 이러한 지도가 복잡해질 수 있음에도 불구하고, 다리가 존재하지 않는 "나쁜" 경우들은 항상 매우 구체적이고 이해 가능한 패턴을 따른다는 것을 발견했습니다. 그들은 이 무한하고 복잡한 지도들을, 진실을 알려주면서도 다리의 존재 여부를 결정할 수 있는 관리 가능한 크기의 다항식 크기(polynomial-sized) 버전으로 항상 축소할 수 있음을 증명했습니다.

그들은 이 방법을 다음의 경우들에 적용했습니다:

1. 표준 선형 논리: 직선의 논리 (K4.3).
2. 시간 논리: "미래"와 "과거"를 모두 다루는 논리 (예: 시간의 흐름). 그들은 정수(..., -2, -1, 0, 1, 2...), 유리수(분수), 실수(연속적인 숫자), 그리고 유한한 시간과 같은 특정 시간 흐름을 조사했습니다.

이 모든 경우에 대해, 저자들은 다리가 존재하는지 확인하는 것이 계산적으로 관리 가능한 수준(coNP-complete)임을 증명했습니다.

핵심 요약

이 논문은 "이 논리들은 보간 성질을 갖지 않는다"라는 부정적인 사실을 "특정한 상황에서 다리가 존재하는지 결정할 수 있는가?"라는 긍정적인 연구 질문으로 전환시켰습니다. 저자들은 이러한 선형적 세계에서 완벽한 다리가 항상 존재하지 않더라도, 특정 문장 쌍에 대해 다리가 존재하는지 효율적으로 판단할 수 있음을 보여주었습니다.

요약하자면: 이 선형적 세계에서 "완벽한 다리" 규칙이 깨졌다고 해서 우리가 암흑 속에 갇혀 있는 것은 아닙니다. 우리는 특정 문장 쌍에 대해 경로가 존재하는지 확인할 수 있는 신뢰할 수 있고 효율적인 손전등을 가지고 있습니다.

기술 요약

기술 요약: 선형 프레임을 가진 양상 논리에서의 비균일적 크레이그 보간법에 대한 관점

문제 정의
크레이그 보간 성질(Craig Interpolation Property, CIP)은 $\phi \to \psi$가 타당할 때, $\phi$와 $\psi$의 공유된 어휘만을 사용하는 보간자 $\iota$가 존재하여 $\phi \to \iota$와 $\iota \to \psi$ 또한 타당하게 만드는 논리의 근본적인 성질이다. 많은 K4.3(선형 전이 프레임의 논리)을 확장하는 정규 양상 논리들이, 특히 유계되지 않은 깊이의 프레임을 가진 경우 CIP를 결여하고 있다는 것은 잘 알려진 "부정적" 사실이다. 전통적으로 CIP의 부재는 해당 논리에 대한 보간자 연구를 종결시키는 요인이 되어 왔다.

본 논문은 이러한 CIP의 부재를 **보간자 존재 문제(Interpolant Existence Problem, IEP)**를 조사함으로써 하나의 연구 질문으로 재구성한다: 논리 $L$에서 $\phi \to \psi$가 타당할 때, $L$ 내에 크레이그 보간자가 존재하는가? 비균일적(non-uniform)인 CIP와 달리, IEP는 단순한 타당성 검사로 환원되지 않는데, 이는 함축의 타당성이 보간자의 존재를 보장하지 않기 때문이다. 본 논문이 다루는 핵심 질문은 IEP가 이들 논리의 타당성 문제(entailment)보다 계산적으로 더 어려운가 하는 점이다. 다른 논리들(예: 명사(nominals)를 포함한 양상 논리, 1차 논리의 파편들)에 대한 이전 연구들은 IEP가 훨씬 더 어려울 수 있음(예: 3ExpTime)을 시사했다. 본 논문은 K4.3을 포함하는 명제 양상 논리에서도 이러한 현상이 발생하는지 조사한다.

방법론
저자들은 **비시뮬레이션(bisimulations)**과 **기술적 프레임(descriptive frames)**에 기반한 비균일적 모델 이론적 접근 방식을 채택한다.

1. 비시뮬레이션 특성화: 본 논문은 $\phi \to \psi$가 $L$에서 보간자를 갖지 않을 조건이 $L$의 기술적 프레임에 기반한 두 모델 $M_1, M_2$가 존재하여, $M_1$은 $\phi$를 만족하고 $M_2$는 $\neg\psi$를 만족하며, 이 두 모델의 루트 포인트들이 **$\sigma$-비시뮬러(sigma-bisimilar)**인 것과 동치라는 기지(Theorem 3.2)를 활용한다(여기서 $\sigma$는 공유된 시그니처이다).
2. 기술적 프레임: 분석은 기술적 프레임(구별 가능성, 조밀성, 컴팩트성 조건을 만족하는 특정 대수적 내부 집합을 갖춘 프레임)의 구조에 크게 의존한다. 이는 GL.3 및 **Log{(N, <)}**와 같은 논리에서 CIP에 대한 반례가 표준 크립키 프레임으로는 증명될 수 없으며, 무한한 기술적 프레임을 필요로 하기 때문에 매우 중요하다.
3. 구조적 분해: 핵심적인 기술적 혁신은 이러한 비시뮬러 모델의 구조를 분석하는 것이다. 저자들은 모델들을 $\sigma$-블록($\sigma$-blocks, 특정 비시뮬레이션 속성을 가진 점들의 구간)으로 분할하고, 보간자의 부재를 입증하는 모든 비시뮬러 모델 쌍이 "준유한(quasi-finite)" 모델 쌍로 변환될 수 있음을 보여준다. 이 모델들은 원자적 프레임(유한 체인, 유한 클러스터, 또는 $C(\bigcirc_k, \bullet)$와 같은 "올챙이(tadpole)" 구조)에 기반한 **단순 모델(simple models)**의 순서 합(ordered sums)으로 구성된다.
4. 준다항 크기(Quasi-Polysize) 속성: 유한하게 공리화된 논리에 대해, 저자들은 이러한 증명 모델의 크기가 입력 공식과 논리의 공리 크기에 대한 다항식에 의해 제한될 수 있음을 증명한다. 이를 **준다항 크기 비시뮬러 모델 속성(quasi-polysize bisimilar model property)**이라 한다.

주요 기여 및 결과

• 결정 가능성 및 복잡도: 본 논문은 K4.3을 포함하는 모든 유한하게 공리화된 정규 양상 논리에 대해 IEP가 **결정 가능(decidable)**하며 **coNP-완비(coNP-complete)**임을 증명한다.

  • 이 결과는 IEP가 이들 논리의 타당성 문제(역시 coNP에 속함)보다 더 어렵지 않다는 점에서 유의미하다. 이는 최근 다른 논리적 틀에서 나타난 비균일적 보간 결과(IEP가 엄격히 더 어려운 경우)와 극명한 대조를 이룬다.
  • 증명은 비시뮬레이션 기준을 만족하는 다항 크기의 모델을 추측하고 논리의 공리들을 검증하는 비결정론적 알고리즘을 포함한다.

• 준다항 크기 비시뮬러 모델 속성: 저자들은 모든 유한하게 공리화된 K4.3의 확장들이 "준다항 크기 비시뮬러 모델 속성"을 가짐을 확립한다. 즉, 만약 보간자가 존재하지 않는다면, 원자적 프레임에 기반한 다항 개수의 단순 모델들의 순서 합으로서의 모델을 통해 이를 입증하는 비시뮬러 모델 쌍이 존재한다는 의미이다.

  • d-지속적 코파이널 서브프레임 논리(d-persistent cofinal subframe logics)(하나의 하위 클래스)의 경우, 이 속성은 더욱 강력하여, 모델들이 다항 크기의 표준 크립키 프레임인 **다항 크기 비시뮬러 모델 속성(polysize bisimilar model property)**을 가진다.

• 프리오어(Priorean) 시간 논리로의 확장: 방법론은 표준 시간 흐름 위에서의 프리오어 시간 논리(미래와 과거 양상 연산자를 모두 포함)로 확장된다:

  • Lin(모든 선형 프레임), LinQ(유리수), LinR(실수): 이 논리들은 다항 크기 비시뮬러 모델 속성을 가지며, IEP는 coNP-완비이다.
  • Lin<ω(유한 엄격 선형 순서) 및 LinZ(정수): 이 논리들은 다항 크기 속성을 갖지는 않지만 준다항 크기 비시뮬러 모델 속성을 가지며, 이들의 IEP 역시 coNP-완비임이 증명되었다.
  • 시간 논리에 대한 증명은 양방향 체인과 양방향의 리밋 클러스터(limit clusters)를 처리해야 하므로, 새로운 프레임 구성(예: 대칭적 "올챙이" 프레임 $C(\bullet, \bigcirc_k, \bullet)$)을 필요로 한다.

의의 및 주장
본 논문은 CIP가 결여된 대규모 양상 논리군(K4.3의 확장들)을 포괄하는 최초의 일반적인 크레이그 보간자 존재성에 관한 결과를 제공한다고 주장한다. IEP가 이들 논리에서 coNP-완비임을 보여줌으로써, 저자들은 CIP의 부재가 반드시 존재 문제의 복잡도 클래스를 높인다는 직관에 도전한다.

본 연구는 IEP의 복잡도가 CIP의 실패에 본질적으로 묶여 있는 것이 아니라, 그 실패를 입증하는 데 필요한 모델의 구조적 특성에 달려 있음을 시사한다. 저자들은 이를 IEP에 기초한 양상 논리 분류를 위한 단계로 위치시킨다.

본 논문은 자신의 증명이 보간자의 계산에 있어서 **비구성적(not constructive)**임을 명시한다. 즉, 존재 여부에 대한 결정 절차를 제공할 뿐, 보간자 자체를 계산하거나 그 크기의 상한을 도출하는 효율적인 알고리즘을 제공하지는 않는다. 또한 저자들은 증명에 있어 기술적 프레임이 필수적임을 강조하며, d-지속적이지는 않지만 강한 크립키 완전성(strong Kripke completeness)을 가진 논리(예: LinR)에서도 크립키 프레임이 IEP에 충분할 것인가라는 열린 질문을 제기한다.