A New Ehrenfeucht-Fraïssé Game for Dependence Logic

기술 요약: 의존 논리(Dependence Logic)를 위한 새로운 에렌포이히트-프라이세(Ehrenfeucht–Fraïssé) 게임

문제 제기
의존 논리($D$)는 의존 원자 $=(\vec{x}, y)$를 추가하여 1차 논리를 확장한 것으로, 이는 $y$의 값이 $\vec{x}$의 값들에 의해 기능적으로 결정됨을 단언한다. $D$의 의미론은 일반적으로 할당들의 집합(팀) 위에서 공식이 평가되는 팀 의미론을 통해 정의된다. 따라서 [15]에서 제시된 의존 논리를 위한 에렌포이히트-프라이세(EF) 게임에 대한 이전의 시도들은, 플레이어가 전체 팀이나 할당들의 집합을 선택하는 "2차적(second-order)" 움직임에 의존했다. 저자들은 팀이 거대해질 수 있기 때문에 이러한 움직임이 계산적으로나 개념적으로 복잡하다고 주장한다. 본 논문은 의존 논리의 표현력을 유지하면서도, 고전적인 1차 논리의 EF 게임과 유사하게 플레이어의 움직임이 단일 요소로 구성되는, 의존 논리를 위한 "1차적(first-order)" EF 게임을 정의하는 것을 목표로 한다.

방법론
저자들은 두 구조 $A$와 $B$ 사이에서 진행되는 $EF^{dep}_n(A, B)$라고 명명된 새로운 게임을 도입한다. 방법론은 세 가지 주요 구성 요소로 이루어진다:

1. 게임 메커니즘:
   게임은 $n$ 라운드 동안 진행된다. 각 라운드 $k$에서, 플레이어 I(스포일러)은 $A$ 또는 $B$로부터 원소 $x_k$를 선택한다. 결정적으로, 플레이어 I은 또한 "의존 약속(dependence commitments)"의 집합 $W_k \subseteq \mathcal{P}(n)$와 원자적 공식의 집합 $U^+_k, U^-_k$를 선언해야 한다.

   • 만약 인덱스 집합 $\{i_0, \dots, i_{k-1}\} \in W_k$라면, 플레이어 I은 현재의 움직임 $x_k$가 동일한 모델 내에서의 이전 움직임들에 의해서만 결정된다고(즉, $x_k \in A$이면 $\{x_{i_0}, \dots, x_{i_{k-1}}\}$에 의해, 또는 $x_k \in B$이면 그에 대응하는 원소들에 의해 결정됨) 선언한다.
   • 플레이어 II(듀플리케이터)는 반대편 구조로부터 원소 $y_k$로 응답한다.
   • 단일 플레이에서의 플레이어 II의 승리 조건은 약속에 기반하지 않는다. 대신, 약속은 여러 플레이를 동시에 고려할 때만 평가된다.

2. 균등 승리 전략(Uniform Winning Strategies):
   핵-혁신은 플레이어 II의 균등 승리 전략을 정의하는 것이다. 전략이 균등하게 승리한다는 것은, 플레이어 I이 일관되게 플레이할 때(즉, 여러 플레이에 걸쳐 동일한 약속을 하고 동일한 원자적 공식들을 만족할 때), 플레이어 II의 응답이 선언된 의존 관계를 준수한다는 것을 의미한다. 구체적으로, 만약 두 플레이에서의 플레이어 I의 움직임이 $W_k$에 선언된 인덱스들에 대해 동일하다면, 플레이어 II의 응답 또한 반드시 동일해야 한다. 이 메커니즘은 플레이어가 전체 팀을 선택할 필요 없이 의존 원자의 기능적 성격을 포착할 수 있게 한다.

3. 보조 게임 및 동치성:
   성격 규정 결과를 증명하기 위해, 저자들은 인덱스된 팀들에 기반한 보조 게임 $EFD_n((A, X), (B, Y))$를 도입한다. 이 게임은 [15]의 게임을 수정한 것이지만, 움직임으로 팀 자체를 사용하는 대신 보충 함수(supplement functions, 팀이 어떻게 확장되는지를 정의함)를 사용한다. 저자들은 두 게임 사이에 가교를 구축한다:

   • 그들은 플레이어 II가 보조 게임 $EFD_n$에서 승리 전략을 가진다면, 새로운 게임 $EF^{dep}_n$에서도 균등 승리 전략을 보유함을 보인다.
   • 그들은 $EF^{dep}_n(A, B)$에서 균등 승리 전략의 존재가 양화사 순위(quantifier rank) $\le n$인 모든 의존 논리 문장에 대해 $A$에서 $B$로의 진릿값 보존과 동치임을 증명한다.

주요 기여 및 결과

• $EF^{dep}_n(A, B)$의 정의: 본 논문은 움직임이 팀이 아닌 단일 요소로 구성되는 새로운 EF 게임을 정의한다. 이는 이전의 정식화에서 발견된 "2차적" 움직임의 복잡성을 해결한다.
• 균등성 조건: 저자들은 "균등 승리 전략"이라는 개념을 도입하여, 플레이어 II의 응답이 여러 플레이에 걸쳐 플레이어 I이 선언한 기능적 의존성을 준수하도록 강제한다.
• 성격 규정 정리(Characterization Theorem): 주요 결과(정리 6.1)는 임의의 $n$에 대하여 두 구조 $A$와 $B$에 대해 플레이어 II가 $EF^{dep}_n(A, B)$에서 균등 승리 전략을 갖는 것이 $A$와 $B$가 의존 논리에서 원소 동치($A \equiv_D B$)인 것과 동치임을 확립한다.
• 1차적 움직임으로의 환원: 저자들은 의존 논리 의미론의 "2차적" 성격에도 불구하고, 전략이 균등성 조건을 만족한다면 게임이 1차적 움직임으로 수행될 수 있음을 입증한다.

의의 및 주장
본 논문은 1차 논리의 고전적 결과와 유사하게, 의존 논리의 원소 동치성에 대한 "1차적" 성격 규정을 제공한다고 주장한다. 그 의의는 게임 플레이 중에 거대한 팀을 조작하는 것을 피함으로써 의존 논리의 게임 이론적 분석을 단순화하는 데 있다.

저자들은 결과의 범위에 대해 겸허한 태도를 취한다. 그들은 다음과 같이 언급한다:

• 주요 결과의 증명은 의존 논리 문장의 특정 표준형(정리 2.5)에 의존하며, 이는 게임의 길이가 임의의 공식의 양화사 순위와 직접적으로 연결되지 않도록 한다는 점에서 다소 불만족스럽다는 점을 인정한다.
• 결과는 의존 논리의 하향 폐쇄성(downward closedness)(사실 2.3)에 크게 의존한다. 따라서 저자들은 이러한 결과가 포함 논리(inclusion logic)나 독립 논리(independence logic)와 같이 하향 폐쇄성이 없는 다른 팀 논리로 즉각적으로 확장될 수 없다고 명시한다.
• 향후 연구 과제로 포함 논리와 독립 논리를 위한 유사한 게임을 구축할 수 있는지 탐구하고, 표준형에 의존하지 않고 게임 길이를 양화사 순위와 더 밀접하게 연결할 수 있는지 조사할 것을 제안한다.

본 논문은 새로운 응용이나 실험적 제안을 제시하기보다는, 게임 의미론을 통한 의존 논리의 이론적 성격 규정에 엄격히 집중한다.