Lindström Maximality for Fitting's Finite Heyting-Valued Modal Logic with Exact Truth Tests

기술 요약: 정확한 진릿값 테스트를 포함한 Fitting의 유한 헤이팅 값 양상 논리에 대한 Lindström 극대성

문제 제기
본 논문은 고정된 유한 헤이팅 대수($L$) 위에서의 Fitting의 양상 논리, 즉 다가 양상 논리의 표현력의 한계를 규명하는 문제를 다룬다. 고전적 양상 논리와 유한 MTL-체인(선형 순서 대수) 위의 다가 논리에 대해서는 Lindström 스타일의 극대성 정리가 존재하지만, 비선형 사례에 대한 상응하는 결과는 누락되어 있었다. 이전 연구인 Badia와 Olkhovikov의 작업은 최상위 원소(1)의 유일한 직전 원소를 활용하여 지정된 값과 지정되지 않은 값을 분리함으로써 MTL-체인에 대한 극대성을 확립했다. 이러한 접근 방식은 선형성을 결여하거나 1 아래에 단일한 코아톰(coatom)을 갖지 않을 수 있는 임의의 유한 헤이팅 대수에는 적용하기 어렵다. 핵심적인 문제는, 모든 값에 대한 원시 진릿값 상수를 사용하는 대신 단항 정확한 진릿값 테스트($T_\ell$)를 사용하는 Maruyama의 Fitting 논리 제시 방식이, 대수가 체(chain)라고 가정하지 않고도 추상적 확장들 사이에서 극대성을 유지하는지 여부를 결정하는 것이다.

방법론
저자는 고전적 및 다가 Lindström 정리로부터 변형된 모델 이론적 접근 방ков를 채택한다. 방법론은 다음과 같다:

1. 기초 논리 정의: 크리스프(crisp) 크립키 프레임 위에서 공식이 유한 헤이팅 대수 $L$의 값을 갖는 Maruyama 버전의 Fitting 논리($FML_L$)를 활용한다. 언어에는 $\phi$의 값이 $\ell$일 때만 1로 평가되는 단항 정확한 진릿값 테스트 $T_\ell$가 포함된다.
2. 유도된 불 대수 연산자 도입: 체 의존적인 분리 메커니즘을 대체하기 위해, 저자는 불 대수 값 테스트를 정의한다:
   • $D\phi := T_1\phi$ ($\phi$가 지정되었거나/1과 같을 때 참)
   • $N\phi := T_0(T_1\phi)$ ($\phi$가 지정되지 않았거나/1과 같지 않을 때 참)
   • 유도된 존재 양상 연산자 $\Diamond_1 \phi := T_0(\Box N\phi)$ (접근 가능한 상태 중 $\phi$가 1의 값을 갖는 상태가 존재함을 나타냄)
3. 추상적 확장: 저자는 세 가지 모델 이론적 성질(컴팩트성, 타르스키 합집합 성질, 그리고 쌍생성(bisimulation)에 대한 강한 불변성)을 만족하는 $FML_L$의 추상적 확장 $\mathcal{L}$을 고려한다.
4. 포화 및 언러벨링(Unravelling): 증명은 언러벨링 기법을 사용하여 포화된 기본 확장(saturated elementary extensions)을 구축한다. 저자는 "후속자 타입(successor types)"을 정의하기 위해 유도된 양상 연산자 $\Diamond_1$을 활용하며, 이러한 타입들이 실현되는 모델을 구축하기 위해 컴팩트성과 타르스키 합집합 성질을 이용한다.
5. 결정 정리(Decision Lemma): 핵심 단계인 "결정 정리"는 $(D\psi, N\psi)$ 쌍을 사용하여 기초 논리로부터의 어떠한 가설적 새로운 공식을 분리한다. 이는 체 기반 증명에서 사용된 "1의 직전 원소" 논리를 대체한다.

주요 기여 및 결과

• Lindström 극대성 정리: 주요 결과(정리 1)는 임의의 유한 헤이팅 대수 $L$에 대하여, 컴팩트하고 타르스키 합집합 성질을 가지며 쌍생성에 대해 강하게 불변인 모든 추상적 확장 중에서 Maruyama 버전의 Fitting 논리가 1-표현력에 대해 극대적임을 명시한다.
• 선형성 가정의 제거: 본 논문은 선형 순서 대수(MTL-체인)의 범위를 일반적인 유한 헤이팅 대수로 성공적으로 확장한다. 증명은 정확한 진릿값 테스트가 선형성이나 구별된 코아톰을 요구하지 않고도 충분한 분리력을 제공함을 보여준다.
• 정확한 값 정의 가능성: 극대성 정리의 결과로서(따름 정리 1), 저자는 확장 $\mathcal{L}$의 임의의 공식 $\phi$와 임의의 값 $\ell \in L$에 대하여, $\phi$가 정확한 값 $\ell$을 갖는 지점 모델(pointed models)의 집합이 기초 논리 $FML_L$의 공식에 의해 정의 가능함을 증명한다. 구체적으로 "정확한 값 파이버(exact-value fibre)"는 정의 가능하지만, 저자는 이것이 $\phi$의 전체 $L$-값 의미론을 재현하는 단일 공식의 존재를 반드시 함의하는 것은 아니라고 언급한다.
• 포화 모델에 대한 헤니-밀너 성질: 저자는 $FML_L$-포화 모델에 대하여 양상 동치(modal equivalence)가 쌍생성(bisimulation)을 함의함을 입증하여, 표준적인 헤니-밀너 현상을 이 다가 설정으로 확장한다.

의의 및 주장
본 논문은 비선형 대수 위에서의 다가 양상 논리에 관한 문헌의 공백을 해결한다고 주장한다. 정확한 진릿값 테스트($T_\ell$)가 지정된 값과 지정되지 않은 값을 분리할 수 있는 불 대수 결정 쌍($D\phi, N\phi$)을 제공함으로써, 저자는 기초 구조(특히 선형성)가 Lindström 극대성을 위한 필수 조건이 아님을 보여준다.

그 의의는 다음과 같다:

1. 일반화: 제한적인 유한 체(chain) 설정을 넘어 더 넓은 클래스인 유한 헤이팅 대수로 Lindström 정리의 범위를 확장하였다.
2. 메커니즘 식별: 비선형 설정에서 값의 분리와 포화 논증을 위한 핵심 메커니즘으로서 정확한 진릿값 테스트로부터 유도된 불 대수 값 테스트를 식별하였다.
3. 정의 가능성: 기초 논리가 "합리적인" 확장 내의 임의의 공식에 대해 정확한 값 파이버를 정의할 수 있을 만큼 충분히 표현력이 높음을 입증함으로써, Maruyama 제시 방식의 견고함을 강화하였다.

저자는 향후 연구 방향에 대해 겸허한 태도를 유지하며, 타르스키 합집합 성질을 완화할 수 있는지, $L$-값(퍼지) 접근 가능 관계를 어떻게 다룰 것인지, 그리고 별개의 정확한 값 정의들을 전체 의미론을 재현하는 단일 공식으로 통합할 수 있는지와 같은 열린 질문들을 언급하였다.