On existential Büchi arithmetic in two coprime bases

기술 요약: 두 개의 서로소인 기저를 가진 존재적 뷔키 산술(Existential Büchi Arithmetic)

문제 정의
본 논문은 순서, 덧셈, 그리고 두 개의 뷔키 술어(Büchi predicates)로 확장된 정수 집합 상의 1차 논리 존재적 단편(existential fragment) $\exists\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$의 결정 가능성(decidability)을 다룬다. 여기서 $V_z(x, y)$는 $y$가 $x$를 나누는 $z$의 가장 큰 거듭제곱일 때 성립한다.

이 논의의 배경은 Villemaire(1992)가 $\alpha$와 $\beta$가 곱셈적으로 독립(multiplicatively independent)일 때, 구조가 곱셈을 인코딩할 수 있으므로 $\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$의 전체 1차 이론이 결정 불가능함을 증명한 데서 시작된다. 후속 연구인 Hieronymi와 Schulz(2021)는 뷔키 술어를 더 약한 거듭제곱 술어($\alpha^\mathbb{N}, \beta^\mathbb{N}$)로 대체하더라도 이론이 결정 불가능하다는 것을 보여주었다. 그러나 Karimov 등(2025)은 곱셈적으로 독립인 기저들에 대해 거듭제곱 술어를 사용하는 이론의 존재적 단편은 결정 가능하다는 것을 입증했다.

본 논문이 다루는 열린 문제는 술어가 단순 거듭제곱 집합이 아닌 더 강력한 뷔키 술어($V_\alpha, V_\beta$)일 때도 존재적 단편이 결정 가능한가 하는 점이다. 저자는 기저 $\alpha$와 $\beta$가 **서로소(coprime)**인 경우에 대해 이 질문에 대한 답을 내놓는다.

방법론
증명은 존재적 공식(existential formula)을 거듭제곱 변수($z^n$)와 선형 거듭제곱 변수($x \cdot z^n$)를 포함하는 부등식 체계 및 모듈러 제약 조건으로 변환하는 양화사 제거(quantifier-elimination) 과정을 통해 진행된다. 방법론은 다음과 같은 몇 가지 핵심 수학적 도구와 구조적 축소를 활용한다:

1. 부등식 체계로의 축소:
   저자는 먼저 존재적 공식을 "순수 거듭제곱 변수"($z^n$)와 "선형 거듭제곱 변수"($x \cdot z^n$)를 포함하는 체계로 축소한다. 이 체계는 선형 부등식($Ax > v$)과 상수 모듈러스 또는 가변 모듈러스(형태: $d \cdot z^n$)를 가진 모듈러 제약 조건으로 구성된다.

2. 구조적 분해 (레벨 및 바텀 패밀리):
   변수의 복잡성을 관리하기 위해, 저자는 변수들을 상대적 크기에 따라 "레벨(levels)"로 나눈다. 동일한 레벨에 있는 변수들은 비율이 상수로 제한되지만, 서로 다른 레벨의 변수들은 임의로 큰 비율을 가질 수 있다.

   • 레벨(Levels): 다면체 $Ax > v$의 회귀 원뿔(recession cone)을 통해 정의된다.
   • 바텀 패밀리(Bottom Family): "작은 계수"를 가진 특정 변수들의 부분 집합으로, 이들은 함께 처리된다. 저자는 다면체의 이 변수들에 대한 투영이 "얇지(thin)" 않도록(즉, 특정 선형 방향으로 유계되지 않도록) 하는 "바텀 패밀리"를 정의한다.

3. 반복적 축소 및 정규화:
   알고리즘의 핵심은 체계를 특정 속성들(Properties 1–4c)을 만족하도록 축소하는 것이다. 이 속성들은 다음을 보장한다:

   • 변수들이 엄격하게 정렬됨 ($x_1 > \dots > x_t > 0$).
   • 다면체가 얇지 않음.
   • 가변 모듈러스를 가진 모듈러 제약 조건의 모듈러스 기저가 바텀 패밀리에 포함되지 않음.
   • 레벨들의 직교 부분 공간이 지수 기저에 관한 특정 비퇴화 조건을 만족함.

이러한 속성을 달성하기 위해 지수를 제한하는 **베이커 정리(Baker's theorem, 로그의 선형 형식에 관한 정리)**와 비율의 조밀성을 보장하는 디오판토스 근사론의 **크로네커 정리(Kronecker's theorem)**를 적용한다.

4. 모듈러 제약 조건 처리:
   가변 모듈러스($x \equiv c \pmod{z^n}$)를 가진 모듈러 제약 조건을 처리하는 것이 중요한 기술적 기여이다. 저자는 $\alpha$와 $\beta$의 서로소 성질에 의존하는 **보조정리 33(Lemma 33)**을 활용한다. 이 보조정리는 $\{\beta^n \pmod{\alpha^m}\}$의 잔여 집합(residues)이 큰 $m$에 대해 구조적으로 안정화됨을 명시한다. 이를 통해 저자는 지수를 "불리기(blow up)" 하여, 변수 모듈러스 제약 조건을 변수 스케일링을 통해 상수 모듈러스 제약 조건(또는 고정된 주기성을 가진 제약 조건)으로 효과적으로 변환할 수 있다.

5. 양화사 제거:
   체계가 정규화되고 모듈러스가 고정되면(또는 상수로 축소되면), 저자는 리프팅(lifting) 논증을 적용한다. 만약 체계가 만족 가능하다면, 바텀 패밀리 외부의 변수들이 충분히 큰 해가 존재함을 보여준다. 바텀 패밀리 내부의 나머지 변수들은 특정 모듈러 클래스 내의 선형 정수로 취급된다. 이 선형 변수들을 제거함으로써, 체계는 점진적으로 더 작은 변수 집합으로 축소되며, 결국 양화사가 없는 결정 단계에 이르게 된다.

주요 기여 및 결과

• 주요 정리: 본 논문은 서로소인 정수 $\alpha, \beta \ge 2$에 대하여 $\exists\text{FO}(\mathbb{Z}; <, +, V_\alpha, V_\beta)$가 결정 가능함을 증명한다.
• 기존 연구의 일반화: 이 결과는 거듭제곱 술어($\alpha^\mathbb{N}, \beta^\mathbb{N}$)에 적용되었던 Karimov 등의 결정 가능성 결과를 더 표현력이 높은 뷔키 술어 $V_\alpha, V_\beta$로 확장하며, 이때 서로소라는 더 강한 조건을 전제로 한다.
• 기술적 보조정리: 로그의 선형 독립성을 다루는 베이커 정리(보조정리 12)와 가변 모듈러스 제약 조건의 축소에 필수적인, 서로소인 기저의 거듭제곱에 대한 모듈러 구조를 설명하는 구체적인 보조정리(예: 보조정리 33)를 제공한다.
• 알고리즘적 구성: 증명은 구성적(constructive)이며, 양화사를 제거하기 위해 필요한 경계값, 분할 및 치환을 계산하는 방법을 제공한다.

의의 및 한계
본 논문은 서로소인 기저에 대한 Villemaire의 원래 확장 모델에 대한 존재적 단편의 결정 가능성 문제를 해결했다고 주장한다. 저자는 **서로소성(coprimality)**에 대한 의존성을 중요한 제약 사항으로 명시한다.

• 서로소성에 대한 의존성: 증명은 두 번의 과정에서 서로소성을 사용한다: 한 번은 베이커 정리(보조정리 12)의 적용에서, 더 결정적으로는 $\beta^n \pmod{\alpha^m}$의 구조에 관한 보조정리 33에서이다. 저자는 서로소가 아니면서 곱셈적으로 독립인 기저의 경우, 잔여 집합이 안정화되지 않고 선형적으로 증가하는 등 더 불규칙하게 행동하며, 이 문제를 어떻게 우회할 수 있을지 알지 못한다고 밝힌다.
• 범위: 이 결과는 존재적 단편에 국한된다. 전체 이론은 여전히 결정 불가능하다.
• 향후 방향: 저자는 세 개 이상의 거듭제곱 술어(예: 세 개의 거듭제곱 술어)로 확장하는 것은 로그의 선형 독립성을 다루기 위해 섀뉴엘 추측(Schanuel's conjecture)이 필요할 것이라고 언급한다. 또한, 일반적인 곱셈적 독립(비-서로소) 기저에 대한 문제는 여전히 미해결 상태이며, 아마도 베이커 정리의 $p$-진(p-adic) 버전을 포함한 새로운 아이디어가 필요할 것이라고 덧붙였다.

요약하자면, 이 논문은 존재적 뷔키 산술의 결정 가능성 경계선을 확립하여 거듭제곱 술어와 전체 뷔키 술어 사이의 간극을 메우지만, 곱셈적으로 독립이지만 서로소가 아닌 일반적인 경우에 대해서는 여전히 도전 과제로 남아 있음을 명시적으로 인정하고 있다.