산술에서 흐름을 목격하기

초록 증명 이론의 역사에서 우아한 성과 중 하나는 산술 이론의 증명 가능 총 재귀 함수들을 증명 이론적 서수로 특성화하여 함수의 시간 복잡성을 측정하는 방법입니다. 불행히도, 이 장치는 약한 이론에 적용할 수 있을 만큼 세밀하지 않으며, 강한 이론의 경계 정의를 가진 제한된 함수들을 포착하는 데에도 부족합니다. 본 논문에서는 강한 이론과 약한 이론의 산술에 대한 경계 정리를 다루기 위해 그러한 장치를 개발합니다. 첫 번째 부분에서는 PA+ TI(_{})의 증명 가능 총 함수와 그것이 효율적으로 정의 가능하고 경계가 있는 함수를 포착하기 위한 서수 분석의 세분화된 버전을 제공합니다. 대략적으로, 우리는 계산 가능한 함수들을 아래의 서수에 의해 인덱스가 매겨지고 수정에 따라 감소하는 초기 다항식 시간 값에 대한 일련의 PV-증명 다항식 시간 수정에 의해 계산 가능한 함수로 식별합니다. 두 번째 부분에서는 l k를 선택하여 이론 Tᵏ₂ (resp. Sᵏ₂)에서 제한된 정의를 가진 함수를 포착하기 위해 유사한 기법을 사용하여 명시적인 PV₊-₋ +₁-증명 승리 전략으로 시작하는 l-턴 게임 사이의 기하급수적으로 (resp. 다항식적으로) 긴 일련의 PV₊-₋ +₁-증명 축소에 의해 계산 가능한 함수로서 함수를 정의합니다.