역수학

이 글은 검증을 위해 인용구가 추가로 필요하다. 신뢰할 수 있는 출처에 인용문을 추가하여 이 기사를 개선할 수 있도록 도와주십시오. 공급되지 않은 재료는 도전하여 제거할 수 있다. 출처 찾기: "역수학" – 뉴스 · 신문 · 책 · 학자 · JSTOR (2016년 10월) (이 템플릿 메시지를 제거하는 방법과 시기 학습)

역수학은 수학의 이론들을 증명하기 위해 어떤 공리가 필요한지를 결정하는 수학 논리학의 프로그램이다.그것의 정의 방법은 공리에서 이론들을 도출하는 일반적인 수학적 관행과는 대조적으로 "이론에서 공리로 되돌아가는" 것으로 간단히 설명할 수 있다.그것은 충분한 조건으로부터 필요한 조건을 조각하는 것으로 개념화될 수 있다.

역수학 프로그램은 선택의 공리와 조른의 보조마사가 ZF 세트 이론보다 동등하다는 고전적 정리 등 세트 이론의 결과에 의해 예시되었다.그러나 역수학의 목표는 정해진 이론에 대한 가능한 공리보다는 수학의 일반적인 이론의 가능한 공리들을 연구하는 것이다.

역수학은 보통 2차 산술의 서브시스템을 사용하여 수행되는데, 여기서 그 정의와 방법의 많은 부분이 건설적 분석과 증명 이론의 이전 작품에서 영감을 얻는다.2차 산술의 사용은 또한 재귀 이론의 많은 기술들을 사용할 수 있게 한다; 역수학의 많은 결과들은 계산 가능한 분석에서 상응하는 결과를 가지고 있다.고차 역수학에서는 고차 산술의 서브시스템과 연관된 풍부한 언어에 초점을 맞춘다.^{[clarification needed]}

이 프로그램은 하비 프리드먼(1975, 1976년)에 의해 설립되었고 스티브 심슨이 도입하였다.이 주제에 대한 표준 참조는 심슨(2009년)이고, 비전문가를 위한 소개는 스틸웰(2018년)이다.고차 역수학에 대한 소개와 함께 창간논문도 콜렌바흐(2005)이다.

통칙, 일반원칙

역수학에서, 사람들은 틀 언어와 기본 이론, 즉 핵심 공리 체계로 시작하는데, 이것은 너무 약해서 흥미를 가질 수 있는 대부분의 이론들을 증명할 수는 없지만, 여전히 이러한 이론들을 진술하는 데 필요한 정의를 개발할 수 있을 만큼 충분히 강력하다.예를 들어, "실수의 모든 경계 순서는 우월성을 가지고 있다"라는 정리를 연구하기 위해서는 실수와 실수의 순서를 말할 수 있는 베이스 시스템을 사용할 필요가 있다.

베이스 시스템에서는 명시할 수 있지만 베이스 시스템에서는 증명할 수 없는 각각의 정리에 대해, 그 정리를 증명하는 데 필요한 특정 공리 시스템(베이스 시스템보다 더 강한)을 결정하는 것이 목표다.정리 T를 증명하기 위해 시스템 S가 필요하다는 것을 보여주기 위해서는 두 가지 증거가 필요하다.첫 번째 증거는 T가 S로부터 증명될 수 있다는 것을 보여준다; 이것은 시스템 S에서 수행될 수 있다는 명분과 함께 일반적인 수학적 증명이다.역전이라고 알려진 두 번째 증거는 T자체가 S를 내포하고 있다는 것을 보여준다; 이 증거는 베이스 시스템에서 수행된다.이 반전은 T를 증명하면서, 베이스 시스템을 확장하는 어떤 공리 시스템 S′도 S보다 약할 수 없다는 것을 확립한다.

2차 산술의 사용

대부분의 역수학 연구는 2차 산술의 서브시스템에 초점을 맞추고 있다.역수학 연구의 본체는 2차 산술의 약한 서브시스템이 거의 모든 학부 수준의 수학을 공식화하기에 충분하다는 것을 확립했다.2차 산술에서 모든 물체는 자연수 또는 자연수 집합으로 나타낼 수 있다.예를 들어, 실수에 대한 이론들을 증명하기 위해서, 실수는 각각 자연수의 집합으로 표현될 수 있는 합리적인 숫자의 카우치 시퀀스로 표현될 수 있다.

역수학에서 가장 흔히 고려되는 공리계는 이해 체계라고 불리는 공리 체계를 사용하여 정의된다.그러한 계획은 주어진 복잡성의 공식에 의해 정의될 수 있는 자연수의 집합이 존재한다고 명시한다.이 맥락에서 수식의 복잡성은 산술적 계층 구조와 분석 계층 구조를 사용하여 측정한다.

세트이론을 베이스 시스템으로 삼아 역수학을 하지 않는 이유는 세트이론의 언어가 너무 표현력이 뛰어나기 때문이다.극히 복잡한 자연수 집합은 집합 이론의 언어에서 간단한 공식으로 정의할 수 있다(임의 집합에 대해 정량화할 수 있다).2차 산술의 맥락에서, 포스트의 정리 같은 결과는 공식의 복잡성과 그것이 정의하는 세트의 (비)계산성 사이에 밀접한 연관을 확립한다.

2차 산수를 사용하는 또 다른 효과는 일반적인 수학 이론들을 산술 내에서 표현할 수 있는 형태로 제한할 필요가 있다는 것이다.예를 들어 2차 산술은 "모든 계산 가능한 벡터 공간에는 기본이 있다"는 원리를 표현할 수 있지만 "모든 벡터 공간에는 기본이 있다"는 원리는 표현할 수 없다.실용적인 측면에서 이것은 대수학과 결합론의 이론은 계산 가능한 구조로 제한되는 반면, 분석과 위상의 이론은 분리 가능한 공간으로 제한된다는 것을 의미한다.일반적인 형태의 선택 공리를 암시하는 많은 원리(예: "모든 벡터 공간에는 기본이 있다")는 제한될 때 2차 산술의 약한 서브시스템에서 증명할 수 있게 된다.예를 들어, "모든 분야는 대수적 폐쇄를 가지고 있다"는 ZF 세트 이론에서는 증명할 수 없지만, "모든 셀 수 있는 장은 대수적 폐쇄를 가지고 있다"는 제한된 형태는 RCA에서₀ 증명할 수 있는데, 이는 역수학에서 일반적으로 사용되는 가장 약한 시스템이다.

고차 산술의 사용

울리히 콜렌바흐가 시작한 최근 일련의 고차 역수학 연구는 고차 산술의 하위 시스템에 초점을 맞추고 있다.^[1]고차 산술의 풍부한 언어 때문에 2차 산술에서 흔히 쓰이는 표현(일명 '코드')의 사용이 크게 줄어든다.예를 들어 칸토어 공간의 연속 함수는 이진 시퀀스를 이진 시퀀스에 매핑하는 함수에 불과하며, 이 함수는 연속성의 통상적인 '엡실론-델타' 정의도 만족시킨다.

고차 역수학에는 (2차) 이해 체계의 고차 버전이 포함된다.그러한 고차 공리는 주어진 복잡성의 공식의 진실이나 허위를 결정하는 기능의 존재를 기술한다.이러한 맥락에서 수식의 복잡성은 산술적 계층 구조와 분석 계층 구조를 사용하여 측정하기도 한다.2차 산술의 주요 서브시스템 중 고차원의 상대방은 일반적으로 원래의 2차 시스템과 동일한 2차 문장(또는 큰 부분집합)을 증명한다.^[2]예를 들어, RCA라고^ω
₀ 불리는 고차 역수학의 기본 이론은 언어에 이르기까지 RCA와₀ 같은 문장을 증명한다.

앞 단락에서 언급한 바와 같이 2차 이해 공리는 고차 프레임워크에 쉽게 일반화된다.그러나 기본 공간의 콤팩트함을 표현하는 이론은 2차 및 고차 산술에서 상당히 다르게 작용한다. 한 편으로 계산 가능한 커버/2차 산술 언어로 제한될 경우 다음 절부터 WKL에서₀ 단위 간격의 콤팩트함을 증명할 수 있다.한편, 헤아릴 수 없는 커버/고차 산술 언어의 경우, 단위 구간의 압축성은 (완전한) 2차 산술로부터만 증명할 수 있다.^[3]다른 덮개 레마(예: 린델뢰프, 비탈리, 베시코비치 등)는 동일한 동작을 보이며, 게이지 적분의 많은 기본 성질은 기저 공간의 압축성과 동등하다.

2차 산술의 빅 5 서브시스템

2차 산수는 자연수와 자연수의 집합에 대한 형식적인 이론이다.유효 폴란드 공간의 점뿐만 아니라 카운트 가능한 고리, 그룹, 필드 등 많은 수학적인 물체는 자연수 집합으로 나타낼 수 있으며, 이 표현은 2차 산술에서 연구할 수 있다.

역수학은 2차 산술의 여러 하위 시스템을 이용한다.전형적인 역수학 정리는 특정한 수학 정리 T가 약한 서브시스템 B에 대한 2차 산술의 특정 서브시스템 S와 동등하다는 것을 보여준다.이 약한 시스템 B는 결과의 기본 시스템으로 알려져 있다. 역수학 결과가 의미를 가지기 위해서는 이 시스템 자체가 수학적 정리 T를 증명할 수 없어야 한다.^{[citation needed]}

심슨(2009)은 역수학에서 자주 발생하는 '빅 파이브'라고 부르는 2차 산술의 5가지 특정 서브시스템을 기술하고 있다.강도를 증가시키기 위해, 이러한 시스템은 초기 명칭인 RCA₀, WKL₀, ACA₀, ATR₀, and-CA에¹
₁₀ 의해 명명된다.

다음 표는 "빅 5" 시스템을^[4] 요약하고 상대 시스템을 고차 산술로 나열한다.^[2]후자는 일반적으로 원래의 2차 시스템과 동일한 2차 문장(또는 큰 부분집합)을 증명한다.^[2]

서브시스템	의 약자	순서형	대략 에 해당한다.	평.	고차상대방
RCA0	재귀 이해 공리	ωω	건설수학(비숍)	기본 이론	RCAω 0; RCA와0 동일한 2차 문장 입증
WKL0	약한 키니그의 보조정리	ωω	피니티즘적 환원주의 (힐버트)	PRA보다 보수적이다(resp).π0 2 (resp)용 RCA0.π1 1)문장	팬 기능, 연속 기능에 대해$$ ${\displaystyle {2N\mathbb{}}^{}}$ ${\$ 스타일 $2^{\mathb{N}}}$에 대해 균일한 연속성 계수 계산
ACA0	산술 이해 공리	ε0	사전주의 (Weyl, Feferman)	산술 문장에 대한 Peano 산술보다 보수적	'튜링 점프' 기능 $\exists {\displaystyle {\mathrm{}}^{}}$ ${\displaystyle {2\mathrm{}}^{}}$ ${\$ $R{\displaystyle \mathbb{}}$ ${\$에 불연속 함수의 존재를 나타낸다$$.
ATR0	산술적 초핀라이트 재귀	Γ0	약탈적 환원주의(프리드먼, 심슨)	fer1 1 문장에 대한 Feferman의 시스템 IR보다 보수적임	'transfinite recursion' 기능은 ATR에0 의해 존재한다고 주장된 세트를 출력한다.
π-CA1 10	π1 1 이해공리	Ψ0(Ωω)	충동주의		Suslin 기능 S ${\displaystyle {2\mathrm{}}^{}}$ ${\$개는 π-포뮬라1 1(이차 파라미터에 제한됨)를 결정한다$$.

이러한 명칭의 첨자는 유도 방식이 완전한 2차 유도 방식에서 제한되었음을 의미한다.^[5]예를 들어 ACA는₀ 유도 공리(0 ∈ X ∧ ∧ ∀n(n ∈ X → n + 1 ∈ X) → ∀n ∈ X를 포함한다.이는 2차 산술의 완전한 이해 공리와 함께 어떤 2차 공식 for에 대해 (φ(0) (n(φ)(n) → +(n+1) → nn(n)의 보편적 폐쇄에 의해 주어지는 2차 산술 유도 체계를 의미한다.그러나 ACA는₀ 완전한 이해 공리를 가지고 있지 않으며 첨자는 완전한 2차 유도 체계를 가지고 있지 않다는 것을 상기시킨다.이 제한은 중요한데, 유도가 제한된 시스템은 완전한 2차 유도 계획을 가진 시스템보다 입증 이론 서수치가 훨씬 낮다.

기본 시스템 RCA₀

RCA는₀ 로빈슨 산술의 공리, σ⁰
₁ 공식의 유도, Δ⁰
₁ 공식의 이해인 2차 산술의 단편이다.

하위시스템 RCA는₀ 역수학의 베이스시스템으로 가장 많이 사용되는 시스템이다.이니셜 "RCA"는 "재귀적 이해 공리"를 의미하며, 여기서 "재귀적"은 재귀 함수와 같이 "계산 가능"을 의미한다.이 이름은₀ RCA가 비공식적으로 "계산 가능한 수학"에 해당하기 때문에 사용된다.특히, RCA에₀ 존재한다고 증명될 수 있는 자연수 집합은 계산이 가능하므로, 비컴퓨팅 집합이 존재함을 암시하는 어떤 정리도 RCA에서는₀ 증명할 수 없다.이 정도까지 RCA는₀ 배제된 중간 법칙을 포함한 고전적 논리의 이론이기 때문에 구성주의 프로그램의 요건을 충족시키지 못하지만 건설적인 시스템이다.

(컴퓨팅되지 않은 세트가 존재한다는 것을 증명하지 못하는) 그것의 약점에도 불구하고, RCA는₀ 최소한의 논리적 강도만을 필요로 하는 많은 고전적인 이론들을 입증하기에 충분하다.이러한 이론들은 어떤 의미에서는 이미 기초 체계에서 증명할 수 있는 것이기 때문에 역수학 사업의 범위 아래에 있다.RCA에서₀ 증명할 수 있는 고전적 이론은 다음과 같다.

• 자연수, 정수 및 합리적인 수(예: 후자가 순서 필드를 형성함)의 기본 특성.
• 실제 숫자의 기본 특성(실수는 Archimedious 순서 필드; 길이가 0인 닫힌 간격의 내포된 순서는 교차점에 단일 점을 가지고 있으며, 실제 숫자는 계산할 수 없다).
• 완전한 분리 가능한 메트릭스 공간에 대한 바이어 범주 정리(분리성 조건은 2차 산술 언어에서조차 정리를 기술하기 위해 필요하다).
• 연속 실제 함수에 대한 중간 값 정리.
• 분리 가능한 바나흐 공간에 대한 일련의 연속 선형 연산자를 위한 바나흐-슈타인하우스 정리.
• 괴델의 완전성 정리의 약한 버전(문장의 집합에 대해서는, 셀 수 있는 언어로, 그 결과로 이미 닫혀 있다.)
• 셀 수 있는 필드에 대한 대수적 폐쇄의 존재(그러나 그것의 고유성은 아님).
• 셀 수 있는 주문 필드의 실제 폐쇄의 존재와 고유성.

RCA의₀ 1차적 부분(설정된 변수를 포함하지 않는 시스템의 이론)은 1차적 Peano 산술의 이론 집합이며, 유도는 σ⁰
₁ 공식으로 제한된다.그것은 RCA가₀ 그렇듯이 완전한 1차 순서의 페아노 산술에서 확실히 일관성이 있다.

약한 Kignig의 보조정리 WKL₀

서브시스템 WKL은₀ RCA₀ + Kőnig의 약한 형태의 보조정리, 즉 완전한 이항 트리(0과 1의 모든 유한 시퀀스의 트리)의 모든 무한 하위 트리가 무한 경로를 가지고 있다는 진술로 구성된다.약한 Kőnig의 보조마차로 알려진 이 명제는 2차 산술의 언어로 명기하기 쉽다.WKL은₀ 또한 σ⁰
₁ 분리의 원리로 정의될 수 있다(배타적인 자유변수 n의 formulas⁰
₁ 공식 2개를 감안할 때, n을 만족시키는 모든 n을 포함하는 클래스가 있고 n을 만족시키는 클래스는 없다).

용어에 관한 다음 말이 순서다.'약한 Kőnig의 보조정리'라는 용어는 이항 트리의 어떤 무한 하위 트리가든 무한한 경로를 가지고 있다는 문장을 말한다.이 공리가 RCA에₀ 추가되면 결과 서브시스템은 WKL이라고₀ 불린다.한편으로 특정 공리와 기본 공리와 유도를 포함한 하위 시스템 간의 유사한 구분이 아래에 기술된 보다 강력한 하위 시스템에 대해 이루어진다.

어떤 의미에서 약한 Kőnig의 보조마차는 선택의 공리의 한 형태다(그러나 언급된 바와 같이 선택의 공리 없이 고전적인 제르멜로-Fraenkel 집합론에서 증명할 수 있다).그것은 건설적이라는 말의 어떤 의미에서는 건설적으로 타당하지 않다.

WKL이₀ 실제로 (증명이₀ 불가능한) RCA보다 강하다는 것을 보여주기 위해서는, 비컴퓨팅 세트가 존재함을 암시하는 WKL의₀ 정리를 보여주는 것으로 충분하다.이것은 어렵지 않다; WKL은₀ 효과적으로 분리할 수 없는 재귀적으로 열거할 수 있는 집합에 대한 분리 집합의 존재를 암시한다.

알고 보니₀ RCA와₀ WKL은 같은 1차 문장을 입증한다는 의미인 1차 부분을 갖고 있다.그러나 WKL은₀ RCA로부터₀ 따르지 않는 많은 수의 고전적인 수학 결과를 증명할 수 있다.이러한 결과는 1차 진술로 표현할 수 없지만 2차 진술로 표현할 수 있다.

다음 결과는 약한 Kőnig의 보조정리(lema)에 해당하며, 따라서 RCA에₀ 대한 WKL에₀ 해당한다.

• 닫힌 단위 실제 간격에 대한 하이네-보렐 정리, 즉 일련의 열린 간격에 의한 모든 커버는 유한한 하위 커버링을 갖는다.
• 완전 경계 분리 가능한 전체 메트릭 공간(커버가 일련의 열린 공에 의해 이루어지는 경우)에 대한 하이네-보렐 정리.
• 닫힌 단위 간격(또는 위와 같이 소형 분리 가능한 메트릭 공간)에 대한 연속 실제 함수가 경계(또는: 경계 및 한계 도달)된다.
• 닫힌 단위 간격의 연속적인 실제 함수는 다항식(합리적 계수 포함)으로 균일하게 근사할 수 있다.
• 닫힌 단위 간격의 연속 실제 함수는 균일하게 연속적이다.
• 닫힌 단위 간격의 연속적인 실제 기능은 Riemann 통합이 가능하다.
• 브루워 고정 지점 정리(폐쇄 단위 간격의 복사본의 유한한 생산물에 대한 연속 기능용).
• 형태에서의 분리 가능한 한-바나흐 정리: 분리 가능한 바나흐 공간의 하위 공간에 경계된 선형 형태는 전체 공간의 경계된 선형 형태까지 확장된다.
• 요르단 곡선 정리
• 괴델의 완전성 정리(계산 가능한 언어의 경우).
• 길이가 Ω인 {0,1}인 오픈(또는 짝수) 게임에 대한 결정력.
• 모든 계산 가능한 교환반지는 최상의 이상을 가지고 있다.
• 공식적으로 셀 수 있는 모든 실제 분야는 주문할 수 있다.
• 대수적 폐쇄의 고유성(계산 가능한 필드의 경우).

산술 이해 ACA₀

ACA는₀ 산술 공식에 대한 이해도("산술 이해도 공리"라고도 한다)를 더한 RCA이다₀.즉, ACA는₀ 임의의 산술적 공식(변수 집합은 포함하지 않지만, 한계 집합 변수가 없는 공식)을 만족시키는 자연수 집합을 형성할 수 있도록 한다.실제로 완전한 산술적 이해를 얻기 위해 Ⅱ 공식에₁ 대한 이해 체계를 RCA에₀ 추가하는 것으로 충분하다.

ACA의₀ 1차적 부분은 정확히 1차적 페아노 산술이고, ACA는₀ 1차적 페아노 산술의 보수적 확장이다.그 두 체제는 (약체제에)ACA에는₀ 검증 가능한₀ 이론들이 있지만, ACA에서는 증명할 수 없는 이론들이 있지만 ACAA는 서술적 수학의 틀로 생각할 수 있다.자연수에 대한 대부분의 근본적인 결과들과 많은 다른 수학적인 이론들은 이 시스템에서 증명될 수 있다.

ACA가₀ WKL보다₀ 강하다고 보는 한 가지 방법은 모든 산술 세트를 포함하지 않은 WKL 모델을 보여주는₀ 것이다.실제로 낮은 세트에 비해 낮은 세트가 낮기 때문에 낮은 베이스 정리를 이용해 전체적으로 낮은 세트로 구성된 WKL₀ 모델을 구축할 수 있다.

다음의 주장은 RCA에₀ 대한 ACA와₀ 동등하다.

• 실수의 순차적 완전성(실수의 경계 증가 순서는 모두 한계가 있음)
• 더 볼자노-위어스트라스 정리.
• 아스콜리의 정리: 단위 간격의 실제 기능의 경계 등거리 순서는 균일하게 수렴 순서가 있다.
• 모든 계산 가능한 정류 링은 최고의 이상을 가지고 있다.
• 합리적(또는 모든 계산 가능한 필드) 위에 있는 모든 계산 가능한 벡터 공간에는 기초가 있다.
• 모든 셀 수 있는 분야는 초월적 기초를 가지고 있다.
• Kőnig의 보조정리(위에서 설명한 약한 버전에 비해 임의의 미세한 가지치기 나무의 경우).
• 램지의 정리의 특정 형태와 같은 조합론에서의 다양한 정리.^[6]

산술 초지분 재귀 ATR₀

ATR₀ 시스템은 ACA에₀ 비공식적으로 모든 산술 함수(자유수 변수 n과 자유수량 변수 X를 갖는 산술 공식, 이 공식을 만족하는 n의 집합으로 X를 가져오는 연산자로 간주됨)를 모든 집합에서 시작하여 카운트 가능한 순서에 따라 완전하게 반복할 수 있다는 공리를 추가한다.ATR은₀ a₀¹
₁ 분리의 원리와 ACA에 걸쳐 동등하다.ATR은₀ 귀납적이며, 사전적 시스템의 우월성인 증명-이론적 서수 $\gamma {\displaystyle {\mathrm{}}_{}}$ ${\$을 가지고 있다$.$

ATR은₀ ACA의₀ 일관성을 증명하고, 따라서 괴델의 정리로는 엄격히 더 강하다.

다음의 주장은 RCA에₀ 대한 ATR과₀ 동일하다.

• 어떤 두 개의 셀 수 있는 웰 오더도 비교가 된다.즉, 그것들은 이형성이거나 다른 하나의 적절한 초기 부분과 이형성이라는 것이다.
• 셀 수 있는 아벨 집단을 위한 울름의 정리.
• 완전한 분리 가능한 메트릭 공간의 모든 마운트 불가능한 닫힌 부분 집합이 완벽한 닫힌 집합을 포함한다는 것을 기술하는 완벽한 집합 정리.
• 루신의 분리 정리(본질적으로 σ¹
  ₁ 분리).
• Baire 공간의 오픈 세트에 대한 결정성.

π¹
₁ 이해 π-CA¹
₁₀

π-CA는¹
₁₀ 산술적인 트랜스핀라이트 재귀보다 강하며 완전히 임프로덕션적이다.그것은 RCA와₀ π¹
₁ 공식에 대한 이해도로 구성된다.

어떤 의미에서 ,-CA의¹
₁₀ 이해는 산술적인 초지순 재귀( ( separation¹
₁)에 대한 것이다. ACA는₀ 약한 Kőnig의 보조정리(MEMA⁰
₁ 분리)에 대한 것이기 때문이다.그것은 강한 귀납적 주장을 사용하는 증거들이 있는 서술적 집합 이론의 여러 진술과 같다; 이 동등성은 이러한 귀납적 주장들이 제거될 수 없음을 보여준다.

다음의 이론은 RCA에₀ 대한 π-CA에¹
₁₀ 해당한다.

• 칸토르-벤딕슨 정리(모든 폐쇄형 부동산 집합은 완벽한 집합과 카운트할 수 있는 집합의 조합이다).
• 셀 수 있는 모든 아벨 집단은 분리할 수 없는 집단과 축소된 집단의 직접적인 합이다.

추가 시스템

• 재귀적 이해보다 약한 시스템을 정의할 수 있다.약한 시스템 RCA는^*
  ₀ 기본 함수 산술 EFA(기본 공리 + 지수 연산이 있는 고농축 언어의 Δ⁰
  ₀ 유도)와⁰
  ₁ Δ 이해로 구성된다.RCA를^*
  ₀ 통해, 앞에서 정의한 재귀적 이해(즉, σ⁰
  ₁ 유도를 사용한)는 다항식(countable field)이 미세하게 많은 뿌리만을 가지고 있다는 진술과 동등하며, 미세하게 생성된 아벨리아 그룹에 대한 분류 정리에 해당한다.시스템 RCA는^*
  ₀ EFA와 동일한 증명 이론 서수 Ω을³ 가지고 있으며 π⁰
  ₂ 문장의 경우 EFA보다 보수적이다.
• 약한 약한 Kőnig의 보조정리란 무한 이항 트리의 하위 트리는 무한 경로가 없는 무한 이항 트리의 하위 트리는 길이에 있는 잎의 점증적으로 사라지는 비율을 가지고 있다는 것을 말한다(길이 n의 잎의 수에 대한 균일한 추정치를 가지고 있다).등가 제형은 양성 측정치가 있는 칸토어 공간의 모든 부분집합이 비어 있지 않다는 것이다(RCA에서는₀ 이것이 증명할 수 없다).WWKL은₀ 이 공리를 RCA에₀ 붙임으로써 얻어진다.단위 실제 간격을 일련의 간격에 의해 포함하면 길이의 합이 적어도 하나 이상이라는 문구와 동등하다.WWKL의₀ 모델 이론은 알고리즘적으로 무작위 시퀀스 이론과 밀접하게 연결되어 있다.특히 RCA₀ 모델은 모든 세트 X에 대해 X에 상대적인 1랜덤의 집합 Y가 있는 경우에만 약한 Kőnig의 보조마크를 만족시킨다.
• DNR(직관적으로 "비재귀적"의 줄임말)은 RCA에₀ 모든 세트에 상대적인 대각선 비재귀 함수의 존재를 주장하는 공리를 추가한다.즉, DNR은 모든 집합 A에 대해 전체 함수 f가 존재하며, 이는 모든 e에 대해 오라클 A가 있는 부분 재귀 함수가 f와 같지 않다는 것을 명시한다.DNR은 엄격히 WWKL보다 약하다(Lempp et al., 2004).
• Δ-compension은¹
  ₁ 산술적 초지느러미 재귀와 유사하며, 재귀적 이해는 약한 Kignig의 보조정리기가 되기 때문이다.최소 Ω-모델로서 초산술 세트를 가지고 있다.산술적인 초고분자 재귀는 Δ-compension을¹
  ₁ 증명하지만 그 반대는 아니다.
• σ-선택은¹
  ₁ η(n,X)이 각 n에 대해 만족하는 X가 존재하는 σ¹
  ₁ 공식인 경우, n(n_n,X)가 각 n에 대해 보유하는 such(n,X)와 같은 집합 X가_n 있다는 진술이다. σ-선택은¹
  ₁ 또한 초산학 집합을 최소 Ω-모델로 한다.산술적인 초고분자 재귀는 Ⅱ선택을¹
  ₁ 증명하지만 그 반대는 아니다.
• HBU("마운트할 수 없는 하이네-보렐"의 줄임말)는 장치 간격의 (열린 커버) 압축성을 나타내며, 장착할 수 없는 커버를 포함한다.HBU의 후자는 3차 산술 언어로만 표현할 수 있게 만든다.사촌의 정리(1895)는 HBU를 내포하고 있으며, 이러한 정리들은 사촌과 린델뢰프 때문에 동일한 커버 개념을 사용한다.HBU는 증명하기 어렵다: 일반적인 이해 공리의 계층 구조 측면에서 HBU의 증명은 완전한 2차 산술을 필요로 한다.^[3]
• 무한 그래프에 대한 램지의 정리는 빅5 서브시스템 중 하나에 속하지 않으며, 입증 강도가 다양한 다른 약한 변형들도 많이 있다.^[6]

Ω-models 및 β-models

Ω 모델의 Ω은 음이 아닌 정수(또는 유한한 서수)의 집합을 의미한다.Ω 모델은 1차 부품이 페아노 산술의 표준 모델이지만 2차 부품이 비표준일 수 있는 2차 산술의 파편을 위한 모델이다.보다 정확히 말하면 Ω 모델은 Ω의 하위 집합 S⊆2에^ω 의해 주어진다.1차 변수는 통상 Ω의 원소로 해석되며 +, ×는 통상적인 의미를 갖는 반면 2차 변수는 S의 원소로 해석된다.정수의 모든 부분 집합으로 구성되기 위해 S만 취하는 표준 Ω 모델이 있다.그러나 다른 Ω-model도 있다. 예를 들어, RCA는₀ 최소 Ω-model을 가지고 있다. 여기서 S는 Ω의 재귀적 하위 집합으로 구성된다.

β 모델은 π¹
₁ 문장과 σ¹
₁ 문장에 대한 표준 Ω 모델(파라미터 포함)과 동등한 Ω 모델이다.

비 Ω 모델도 유용하며, 특히 보존 이론의 증명에는 유용하다.

참고 항목

• 폐쇄형 표현식 § 숫자형식에서 변환
• 유도, 경계 및 최소 수 원리
• 수학적 최적화
• 순서형 분석
• 기호 회귀

메모들

참조

• Ambos-Spies, K.; Kjos-Hanssen, B.; Lempp, S.; Slaman, T.A. (2004), "Comparing DNR and WWKL", Journal of Symbolic Logic, 69 (4): 1089, arXiv:1408.2281, doi:10.2178/jsl/1102022212, S2CID 17582399.
• Friedman, Harvey (1975), "Some systems of second-order arithmetic and their use", Proceedings of the International Congress of Mathematicians (Vancouver, B. C., 1974), Vol. 1, Canad. Math. Congress, Montreal, Que., pp. 235–242, MR 0429508
• Friedman, Harvey (1976), Baldwin, John; Martin, D. A.; Soare, R. I.; Tait, W. W. (eds.), "Systems of second-order arithmetic with restricted induction, I, II", Meeting of the Association for Symbolic Logic, The Journal of Symbolic Logic, 41 (2): 557–559, doi:10.2307/2272259, JSTOR 2272259
• Hirschfeldt, Denis R. (2014), Slicing the Truth, Lecture Notes Series of the Institute for Mathematical Sciences, National University of Singapore, vol. 28, World Scientific
• Hunter, James (2008), Reverse Topology (PDF) (PhD thesis), University of Wisconsin–Madison
• Kohlenbach, Ulrich (2005), "Higher order reverse mathematics", in Simpson, Stephen G (ed.), Higher Order Reverse Mathematics, Reverse Mathematics 2001 (PDF), Lecture notes in Logic, Cambridge University Press, pp. 281–295, CiteSeerX 10.1.1.643.551, doi:10.1017/9781316755846.018, ISBN 9781316755846
• Normann, Dag; Sanders, Sam (2018), "On the mathematical and foundational significance of the uncountable", Journal of Mathematical Logic, 19: 1950001, arXiv:1711.08939, doi:10.1142/S0219061319500016, S2CID 119120366
• Simpson, Stephen G. (2009), Subsystems of second-order arithmetic, Perspectives in Logic (2nd ed.), Cambridge University Press, doi:10.1017/CBO9780511581007, ISBN 978-0-521-88439-6, MR 2517689
• Stillwell, John (2018), Reverse Mathematics, proofs from the inside out, Princeton University Press, ISBN 978-0-691-17717-5
• Solomon, Reed (1999), "Ordered groups: a case study in reverse mathematics", The Bulletin of Symbolic Logic, 5 (1): 45–58, CiteSeerX 10.1.1.364.9553, doi:10.2307/421140, ISSN 1079-8986, JSTOR 421140, MR 1681895

외부 링크

• 하비 프리드먼의 홈페이지
• 스티븐 G. 심슨의 홈페이지
• 역수학동물원