On Variable-Bounded Non-Linear Expansions of Presburger Arithmetic

기술적 요약: 프레저 산술의 변수 경계 비선형 확장

문제 제기
프레저 산술 (정수와 덧셈 및 순서를 갖는 1 차 논리 이론) 은 결정 가능하다. 그러나 제곱수의 집합 ($Z^2$) 이나 일반적인 다항식 치역과 같은 비선형 술어에 의한 확장은 일반적으로 결정 불가능한 것으로 알려져 있다. 이러한 결정 불가능성은 이러한 이론 내에서 곱셈을 인코딩할 수 있는 능력에서 비롯된다. 이러한 확장의 존재적 단편의 결정 가능성은 여전히 주요한 미해결 문제 (예: 제곱수에 관한 뷔히의 추측) 로 남아 있지만, 본 논문은 결정 가능성을 회복하기 위한 다른 경로를 탐구한다: 변수의 수를 제한하는 것이다.

저자들은 단항 다항식 술어들의 가족을 갖는 프레저 산술의 변수 경계 확장에 초점을 맞춘다. 구체적으로, 서로 다른 변수의 수가 상수 $k$로 제한된 단편들 (기호로 $FO_k$, $\exists FO_k$, $SMT_k$) 을 조사한다. 핵심적인 어려움은 단일 변수 ($k=1$) 의 경우조차 두 다항식 술어가 교차하는지 여부 (예: $f(u) = g(v)$) 를 결정하는 것이 일반적으로 미해결인 힐베르트 제 10 문제의 극도로 제한된 사례라는 점이다.

방법론
본 논문은 이러한 변수 경계 단편 내의 제약 조건들의 해집합을 분석하기 위해 정수론적, 대수기하학적, 그리고 측도론적 기법들을 결합하여 사용한다.

1. 전처리 및 축소: 결정 절차는 임의의 문장을 제약 조건들의 논리곱 (conjunction) 에 관한 만족 가능성 문제로 축소하는 것으로 시작한다. 이러한 제약 조건들은 선형 부등식 ($x > c$), 모듈로 산술 ($x \equiv_m c$), 그리고 $R(ax+b)$또는 그 부정$\neg R(ax+b)$ 형태의 다항식 술어를 포함한다. 저자들은 중국인의 나머지 정리를 활용하여 모듈로 제약 조건들을 통합하고, 유계 구간을 제거하기 위한 경우 분석을 수행하여, 문제를 무계 영역에서의 제약 조건들의 만족 가능성 결정으로 축소한다.
2. 양수 제약 조건 처리: 방법론의 핵심은 양수 다항식 제약 조건들의 시스템에 대한 해집합을 특징짓는 것이다.
   • 고정된 거듭제곱 (예: $Z_k = \{n^k\}$) 의 경우, 저자들은 초타원 디오판토스 방정식에 관한 결과를 활용한다. 두 가지 그러한 제약 조건들의 교집합은 (차수가 충분히 높다면) 유한 집합이거나, 차수가 2 인 경우 선형 재귀 수열 (LRS) 로 매개변수화된 집합임을 보인다.
   • 최대 3 차의 일반 다항식의 경우, 분석은 결과적으로 생성되는 대수 곡선의 종수 (genus) 에 의존한다. 3 차 다항식을 포함하는 시스템은 종종 종수 1 (타원 곡선) 이나 그 이상의 곡선으로 이어지며, 시겔의 정리나 베이커의 경계에 의해 정수 점이 유한하게 존재한다. 2 차 다항식을 포함하는 시스템은 펠 방정식과 관련되며, 그 해들은 가역적 LRS 를 형성한다.
3. 부정 제약 조건 처리 (밀도 논증): 중요한 통찰은 양수 제약 조건들의 해집합이 무한할 때, 부정 제약 조건을 위반하는 (즉, 부정된 술어의 양수 버전을 만족하는) 해들의 집합은 원래 해집합 내에서 상대 밀도가 0이라는 것이다.
   • 다항식 치역의 경우, 치역의 성장률은 다항식적이지만, "금지된" 집합 (다른 다항식에서 비롯된 경우) 은 종종 다른 속도로 성장하거나 희소하다.
   • 해집합이 LRS 인 경우, 저자들은 "금지된" 해들의 인덱스가 산술 급수를 이룬다는 것을 증명한다. 이를 통해 밀도가 0 인 부분집합을 제외하고도 해가 남아 있는지 여부를 효과적으로 확인할 수 있다.
4. 중복 및 병합: 저자들은 "중복된" 및 "유사한" 제약 조건에 대한 개념을 정의한다. 중복된 제약 조건은 폐기할 수 있으며, 유사한 제약 조건은 $p$-진估值과 중국인의 나머지 정리를 사용하여 단일 제약 조건으로 병합할 수 있어, 밀도 논증을 적용하기 전에 시스템을 단순화한다.

주요 기여 및 결과

본 논문은 단일 변수 이론 ($k=1$) 에 대해 두 가지 주요 결정 가능성 결과를 확립한다:

1. 고정된 거듭제곱을 갖는 결정 가능성: 이론 $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (Z_k)_{k\ge 2} \rangle$은 결정 가능하다. 이 결과는 초타원 디오판토스 방정식 ($w^k - nz^j = N$) 의 가해성과 그러한 방정식들의 시스템이 유한한 해를 갖거나 LRS 로 매개변수화된 해를 갖는다는 사실에 의존한다.
2. 저차 다항식을 갖는 결정 가능성: 이론 $FO_1\langle \mathbb{Z}; 0, 1, +, -, <, (\equiv_m)_{m\ge 2}, (R_i)_i \rangle$은 결정 가능하다. 여기서 각 $R_i$는 최대 3 차의 정수값 다항식의 치역에 해당한다. 이 결과는 연관된 대수 곡선의 낮은 종수 (종수 0 또는 1) 와 동시 펠 방정식의 해 구조를 활용한다.

결정 불가능성 결과
이러한 긍정적 결과의 경계를 규명하기 위해, 본 논문은 변수 제한이 해제되거나 특정 술어들이 결합될 때의 결정 불가능성 증명을 제공한다:

• 존재적 단편 $SMT_2\langle \mathbb{Z}; 0, 1, +, -, Z^2 \rangle$은 결정 불가능하다. 이는 뷔히의 추측의 부정을 인코딩하여 제한된 수의 변수를 사용하여 곱셈을 정의할 수 있음을 보여줌으로써 증명된다.
• 존스의 보편적 디오판토스 방정식과 뷔히의 추측에 대한 샤오의 최근 증명을 사용하여, 저자들은 변수 수가 훨씬 더 많은 이론들 (예: $Z^2$를 갖는 $SMT_{600}$ 또는 $SMT_{2200}$) 이 결정 불가능함을 확립한다.

의의
본 논문의 의의는 프레저 산술의 비선형 확장 내에서 결정 가능성을 회복할 수 있는 정확한 경계를 규명하는 데 있다. 변수의 수를 하나로 제한함으로써, 저자들은 정수 점의 유한성 (종수 $\ge 2$인 곡선에서의) 과 선형 재귀 수열 이론과 같은 디오판토스 기하학의 심오한 결과들이 결정 절차를 구성하기에 충분함을 보여준다.

이 연구는 이분법을 강조한다: 일반적인 비선형 확장은 결정 불가능하며, 두 변수와 제곱수를 갖는 존재적 단편조차도 결정 불가능하지만, 단일 변수 사례는 광범위한 술어 가족에 대해 처리 가능하다. 저자들은 이러한 결과를 두 개 또는 세 개의 변수로 확장하는 것은 3 개의 변수와 $Z^2$를 필요로 하는 완전한 오일러 벽돌의 존재나 2 개의 변수와 $Z^3$를 필요로 하는 세 세제곱의 합 문제와 같은 유명한 미해결 문제들에 의해 방해받고 있다고 지적한다. 따라서 본 논문은 변수 제한에 의해 구속된 산술 이론의 계산 복잡성을 이해하기 위한 엄밀한 프레임워크를 제공한다.