An independence of the MIN principle from the PHP principle

기술적 요약: PHP 원리로부터의 MIN 원리의 독립성

문제 제기
본 논문은 명제 증명 복잡성과 유계 산술의 중심 주제인 증명 시스템의 상대적 강도 이해 및 증명 길이에 대한 하한 설정을 다룹니다. 구체적으로 저자는 상대화된 유계 산술의 틀 내에서 **최소화 원리 (MIN)**와 **비둘기집 원리 (PHP)**의 논리적 독립성을 조사합니다.

최소화 원리 $MIN(\triangleleft)$는 유한 구간 $[0, \dots, n)$ 위의 임의의 엄격한 선형 순서 $\triangleleft$가 최소 원소를 가진다고 주장합니다. 이 원리는 이론 $T^2_2(\triangleleft)$에서는 증명 가능하지만, 더 약한 부분 이론 $T^1_2(\triangleleft)$에서는 증명 불가능한 것으로 알려져 있습니다. 비둘기집 원리 $PHP$는 크기$n+1$인 집합에서 크기$n$인 집합으로의 단사 매핑이 존재하지 않는다고 명시합니다.$PHP$는$T_2(\alpha)$와 같은 강력한 이론에서도 증명 불가능하지만, 약한 확장 이론에서$MIN$에 대한 그 위상은 덜 명확합니다.

핵심 질문은 모든 $\Delta^b_1(\triangleleft)$ 공식에 대한 비둘기집 원리의 모든 사례를 추가한 이론 $T^1_2(\triangleleft)$ (기호: $PHP(\Delta^b_1(\triangleleft))$) 가 $MIN(\triangleleft)$를 증명하기에 충분한지 여부입니다. 본 논문은 이러한 확장이 불충분함을 입증하여 $T^1_2(\triangleleft) + PHP(\Delta^b_1(\triangleleft))$가 $MIN(\triangleleft)$를 증명하지 못함을 보일 것을 목표로 합니다.

방법론
증명은 진산술의 가산 비표준 모델 $M$ 위에서 세 당사자 간에 수행되는 게임으로 구조화된 모델론적 구성을 활용합니다. 목표는 특정 성질을 만족하면서 다른 성질은 위반하는 이항 관계 $\triangleleft$를 정의함으로써 부분 구조 $I \subset M$의 확장을 구성하는 것입니다.

1. 게임 프레임워크:
   구성은 세 명의 플레이어 간에 가산 수의 단계로 진행되는 게임 $G_O$로 간주됩니다.

   • $P_{MIN}$: $MIN(\triangleleft)$를 반증하기 위해 최소 원소가 없는 엄격한 선형 순서를 $[0, \dots, n)$ 위에 구성하는 것을 목표로 합니다.
   • $P_{IND}$: 결과 구조가 다항식 수학적 귀납법 ($\Sigma^b_1(\triangleleft)$-induction) 을 만족하여 $T^1_2(\triangleleft)$ 이론을 보존하도록 하는 것을 목표로 합니다.
   • $P_{PHP}$: 구조가 $\Delta^b_1(\triangleleft)$ 공식에 대한 비둘기집 원리의 모든 사례를 만족하도록 하는 것을 목표로 합니다.

   게임은 플레이어가 부분 순서 조건 $o \in O$ (서로 다른 숫자의 유한 시퀀스) 를 확장하는 라운드로 진행됩니다. 최종 관계 $\triangleleft$는 이러한 조건들의 합집합입니다.

2. 승리 전략:

   • $P_{MIN}$ 전략: 모든 원소가 결국 삽입되고 모든 원소가 더 작은 전유자를 가지도록 보장하는 외부 가산 큐를 사용하여 최소 원소가 없는 전순서를 보장합니다.
   • $P_{IND}$ 전략: Paris 와 Wilkie 의 고전적 결과 (Riis 에 의해 확장됨) 에 의존합니다. 이 결과에 따르면 임의의 $\Sigma^b_1$ 공식에 대해 증명이 존재한다면, 최소 수 원리를 보장하는 '정착' 조건을 찾을 수 있습니다.
   • $P_{PHP}$ 전략 (핵심 기여): 이는 기술적으로 가장 까다로운 부분입니다. 플레이어는 임의의 $\Delta^b_1(\triangleleft)$ 공식 $\phi$에 대해, $\phi$에 의해 정의된 관계가 더 큰 집합 $p$에서 더 작은 집합 $h$로의 단사 함수가 아니도록 해야 합니다.

3. 조합론적 분석 ("배열" 방법):
   $P_{PHP}$가 승리 전략을 가짐을 증명하기 위해 저자는 $(o, p, h)$-PHP-배열 개념을 도입합니다. 이는 $\Delta^b_1$ 공식에 대한 오라클 계산의 가능한 결과를 나타내는 정의 가능한 조건들의 가족입니다.

   • 증명은 이를 오라클 쿼리에 대한 결정 트리와 유사한 균일 트리로 확장함으로써 이러한 배열의 크기에 대한 하한을 설정합니다.
   • 강제법 포지드 (forcing poset) 에서 쌍대적으로 양립 불가능한 조건들의 집합 크기에 대한 상한을 설정합니다.
   • 이러한 상한과 하한을 비교함으로써 저자는 $p > h$인 경우 모순을 유도합니다: 유효한 배열의 존재는 $p \le h$를 의미합니다. 따라서 $p > h$인 경우, 플레이어 $P_{PHP}$는 항상 충돌을 찾거나 결손된 값을 발견함으로써 단사성을 위반하게 강제할 수 있으며, 이는 PHP 원리가 성립함을 보장합니다.

주요 기여 및 결과

• 주요 정리: 본 논문은 $T^1_2(\triangleleft) + PHP(\Delta^b_1(\triangleleft)) \nvdash \forall n MIN(\triangleleft)_n$임을 증명합니다.
  • 이 결과는 $MIN$을 증명하는$T^2_2(\triangleleft)$의 강도와 비둘기집 원리에 의해 확장된$T^1_2$의 확장을 분리합니다.
  • 이는 상대화된 설정에서 이론 $T^1_2(\triangleleft) + PHP(\Delta^b_1(\triangleleft))$와 $T^2_2(\triangleleft)$가 강도 면에서 비교 불가능함을 시사합니다: 전자는 $MIN$을 증명하지 못하며, 후자는 일반 PHP 를 증명하지 못합니다.
• 조합론적 기법: 본 논문은 PHP-배열과 MIN-트리를 포함하는 정교한 조합론적 방법을 개발합니다. 이 기법은 강제법 구성에서 조건 크기의 정밀한 계산을 가능하게 하여, 이전 하한 논증들을 개선하여 정확한 크기 추정을 제공합니다.
• 추가 분리: 방법론은 추가적인 독립성 결과를 입증하는 데 적용됩니다.
  • **이중 약한 비둘기집 원리 (dWPHP)**가 실패하는 $T^1_2(\alpha) + PHP(\Delta^b_1(\alpha))$의 모델을 구성할 수 있습니다.
  • **토너먼트 원리 (TOUR)**가 실패하는 모델을 구성할 수 있습니다.
  • 구성은 특정 부분집합에서 $\triangleleft$가 조밀한 선형 순서가 되는 모델을 생성하도록 수정될 수 있습니다.

의의 및 주장
본 논문은 인접한 이론 $T^i_2$와 $T^{i+1}_2$의 분리 및 $R(\log)$ 문제와 같은 유계 산술의 미해결 문제를 이해하기 위한 새로운 경로를 제공한다고 주장합니다. $T^1_2$에 비둘기집 원리를 추가하는 것이 최소화 원리를 산출하지 못함을 보여줌으로써, 이 작업은 약한 산술 이론을 강화하는 데 있어 조합론적 원리들의 한계를 부각시킵니다.

저자는 약한 비둘기집 원리 (WPHP) 가 [12] 의 결과들을 통해 MIN 과 같은 강력한 원리를 증명하기에 불충분한 것으로 알려져 있지만, 본 논문은 이를 강한 비둘기집 원리로 확장하여 $\Delta^b_1$ 공식으로 제한된 경우를 다룬다고 지적합니다. 그 의의는 다항식 시간 계산 가능한 그래프로 제한된 강한 PHP 조차도 최소화에 관한 $T^2_2$의 강도와의 간극을 메우지 못함을 입증하는 데 있습니다.

본 논문은 동일한 조합론적 방법들이 $MIN(\triangleleft)$로부터 $T^1_2(\triangleleft) + PHP'(\Delta^b_1(\triangleleft))$ (다중 함수를 허용하는 변형) 를 분리할 수 있는지 여부를 미해결 문제로 제기하며 마무리합니다. 저자는 행의 원소들이 반드시 양립 불가능하지 않은 배열에 대한 하한을 설정하는 데 어려움이 있음을 지적하며 불확실성을 표명합니다.