On Modal Logics of Full Products of Neighborhood Frames

기술 요약: 이웃 프레임의 완전 곱에 관한 양상 논리

문제 정의
본 논문은 이웃 프레임(neighborhood frames)의 "완전 곱(full products)"과 관련된 양상 논리의 특징 규명을 다룬다. 크립키 프레임(Kripke frames) 및 위상 공간(특히 $S4$ 및 $D4$와 같은 체계)의 곱에 대한 논리는 잘 알려져 있는 반면, 더 약한 비정규 양상 논리(non-normal modal logics)의 맥락에서 완전 곱의 거동은 덜 탐구되었다.

표준 크립키 의미론에서 두 프레임의 완전 곱은 수평 및 수직 관계 외에 제3의 접근 관계(동기적 관계)를 도입한다. 이러한 구조는 일반적으로 교환 법칙($\square_1 \square_2 p \leftrightarrow \square_2 \square_1 p$) 및 수렴(convergence)과 같은 강력한 상호작용 원리를 검증한다. 이와 대조적으로, 크립키 의미론을 일반화하고 위상 의미론을 특수한 경우로 포함하는 이웃 의미론은 이러한 상호작용 원리가 반드시 성립하지 않는 곱을 구성할 수 있게 한다.

본 논문이 다루는 구체적인 문제는 $T$(반사적) 및 $D$(직렬적) 논리에 대한 완전 이웃 곱의 정확한 공리화를 결정하는 것이다. 저자들은 세 가지 이웃 함수(수평 $\square_1$, 수직 $\square_2$, 그리고 곱 $\square$)를 갖춘 $T$ 또는 $D$를 검증하는 이웃 프레임의 완전 곱으로부터 생성되는 삼중 양상 논리를 조사한다.

방법론
저자들은 의미론적 분석과 유계 모형(bounded morphisms)을 통한 완전성 증명을 결합하여 사용한다.

1. 정의 및 하한(Lower Bounds):
   논문은 두 이웃 프레임 $X$와 $Y$의 완전 이웃 곱 $X \times^+_n Y$를 정의한다. 이 구조는 구성 프레임으로부터 유도된 수평 및 수직 이웃 함수와, 구성 요소들의 이웃들의 곱에 의해 생성된 곱 이웃 함수를 포함한다.
   저자들은 유효한 공리를 식별함으로써 논리 $T \times^+_n T$와 $D \times^+_n D$의 하한을 설정한다. 그들은 상호작용 공제 $(mix) = \square p \to \square_1 \square_2 p \land \square_2 \square_1 p$를 도입한다. 저자들은 $T_3^m = T \otimes T \otimes T + (mix)$와 $D_3^m = D \otimes D \otimes D + (mix)$가 각각의 해당 완전 곱의 논리에 포함됨을 입증한다.

2. 무한 트리를 통한 완전성:
   상한(upper bounds)을 증명하기 위해(즉, 곱 논리가 $T_3^m$ 및 $D_3^m$에 포함됨을 보이기 위해), 저자들은 특정 무한 크립키 프레임을 구성한다:

   • $T^{r,m}_{\omega,\omega,\omega}$: 관계 $R, R_1, R_2$가 $R_1 \circ R_2, R_2 \circ R_1 \subseteq R$를 만족하는 반사적이고 무한 분기되는 트리.
   • $T^{i,m}_{\omega,\omega,\omega}$: 비반사적 대응체.
     저자들은 $T_3^m$이 $T^{r,m}_{\omega,\omega,\omega}$에 대해 건전하고 완전하며, $D_3^m$이 $T^{i,m}_{\omega,\omega,\omega}$에 대해 건전하고 완전함을 증명한다. 이는 상호작용 조건 $R_1 \circ R_2 \cup R_2 \circ R_1 \subseteq R$를 보존하는 여과(filtration) 기법을 통해 확립된 이 논리들의 유한 모델 성질(FMP)에 의존한다.

3. 이웃 프레임 구성 및 유계 모형:
   교환 공리를 부정하기 위해 필요한 이웃 프레임은 크립키 프레임으로부터 직접 유도될 수 없다는 점(크립키 유도 이웃 프레임은 교환 법칙을 보존함)이 중요한 기술적 난관이다. 이를 극복하기 위해, 저자들은 "의사 무한 수열"(특수 기호 $\star$로 결국 끝나는 자연수의 수열)에 기반한 특정 이웃 프레임 $N^r_\omega$와 $N^i_\omega$를 구성한다. 이 프레임들은 이웃들이 무한히 감소하는 엄격한 사슬을 형성하여, 어떤 상태도 최소 이웃을 갖지 않도록 함으로써 크립키적 성질을 깨뜨린다.
   마지막으로, 저자들은 이 이웃 프레임들의 완전 곱($N^r_\omega \times^+_n N^r_\omega$)에서 트리 $T^{r,m}_{\omega,\omega,\omega}$에 의해 유도된 이웃 프레임으로의 전사적 유계 모형을 정의한다. 이 모형은 트리에서 유효한 모든 공식이 곱에서도 유효함을 입증함으로써 상한을 확립한다.

주요 기여 및 결과
본 논문의 주요 기여는 $T$와 $D$에 대한 완전 이웃 곱의 정확한 공리화를 제공하는 것이다:

• 정리 1.4:

  • $T \times^+_n T = T \otimes T \otimes T + (mix)$
  • $D \times^+_n D = D \otimes D \otimes D + (mix)$

  여기서 $\otimes$는 논리의 융합(fusion)을 나타내며, $(mix)$는 상호작용 공제$\square p \to \square_1 \square_2 p \land \square_2 \square_1 p$이다.

• 위상 의미론과의 구별:
  본 논문은 위상 의미론(반사적 프레임에 대응)과 일반 이웃 의미론 사이의 결정적인 차이를 강조한다. 위상 의미론에서, 공제 $(sub) = \square p \to \square_1 p \land \square_2 p$는 완전 곱에서 유효하다. 저자들은 $S4 \otimes S4 \otimes S4$ 상에서 $(sub)$와$(mix)$가 동치임을 보여준다. 그러나 더 약한 직렬 논리$D$의 경우,$(sub)$는 완전 이웃 곱에서 **유효하지 않다**. 저자들은 크립키 프레임의 예시를 이웃 의미론으로 변형하여$(sub) \notin D \times^+_n D$인 반면,$(mix)$는 여전히 유효함을 보여주는 반례를 제시한다.

• 결정 가능성:
  결과로 도출된 논리들 $T_3^m$과 $D_3^m$에 대해 유한 모델 성질을 확립함으로써, 저자들은 이 논리들이 결정 가능하다는 결론을 내린다.

의의
본 논문은 위상적 설정에서의 알려진 $S4$ 및 $D4$의 곱 결과를 이웃 의미론의 틀 안에서 더 약한 체계($T$ 및 $D$)로 확장한다. 이는 일반적인 이웃 설정과 위상적 설정 간의 구조적 차이를 명확히 하며, 특히 완전 곱에서 $(sub)$공제의 유효성을 위한 기초 프레임의 반사성이 필수 조건임을 입증한다. 이 연구는 이러한 곱으로부터 발생하는 삼중 양상 논리에 대한 완전한 특징 규명을 제공하며, 비정규, 곱 기반 이웃 구조에서의 양상 상호작용에 관한 문헌의 공백을 메운다. 저자들은 직렬성에 의존하는 기법들이 직접 적용되지 않으므로, 이러한 결과를$K$나$K4$와 같은 비직렬 논리로 확장하는 것이 향로 과제로 남아 있다고 언급한다.