2차 산술

수학적 논리학에서 2차 산술은 자연수와 그 하위 집합을 공식화하는 자명계의 집합이다.그것은 수학의 많은 것, 전부는 아니지만 많은 것을 위한 기초로서 자명하게 정해진 이론에 대한 대안이다.null

3차 파라미터를 포함하는 2차 산술의 전구체는 데이비드 힐버트와 폴 버네이즈가 저서 그룬드라겐 데르메틱에서 소개하였다.2차 산술의 표준 공리화는 Z가₂ 나타낸다.null

2차 산술에는 1차 산술 상대인 페아노 산수가 포함되지만, 훨씬 더 강하다.페아노 산술과는 달리 2차 산술은 숫자 자체뿐만 아니라 자연수 집합에 대한 정량화가 가능하다.실수는 잘 알려진 방식으로 (무한) 자연수 집합으로 나타낼 수 있고, 2차 산술은 그러한 집합에 대해 정량화가 가능하기 때문에 2차 산술에서는 실수의 공식화가 가능하다.이 때문에 2차 산술은 '분석'이라고도 한다(Sieg 2013, 페이지 291).null

2차 산술은 또한 모든 원소가 자연수 또는 자연수 집합인 집합 이론의 약한 버전으로 볼 수 있다.제르멜로-프랑켈 집합론보다 훨씬 약하지만, 2차 산술은 본질적으로 그 언어에서 표현 가능한 고전 수학의 모든 결과를 증명할 수 있다.null

제2차 산술의 하위시스템은 제2차 산술 언어의 이론이며, 각 공리는 완전 제2차 산술(Z₂)의 정리다.이러한 하위시스템은 다양한 강도의 약한 하위시스템에서 얼마나 많은 고전수학을 도출할 수 있는지를 연구하는 연구 프로그램인 수학의 역전에 필수적이다.핵심 수학의 많은 부분이 이러한 약한 서브시스템에서 공식화될 수 있으며, 그 중 일부는 아래에 정의되어 있다.역수학은 또한 고전 수학이 비건설적인 범위와 방식을 명확히 한다.null

정의

구문

제2차 산술 언어는 두 갈래로 나뉜다.첫 번째 종류의 용어와 특히, 일반적으로 소문자로 표시되는 변수는 개인으로 구성되며, 의도된 해석은 자연수로 한다.다른 종류의 변수들, 다양하게 불리는 "set variables", "class variables" 또는 심지어 "predates"는 대소문자로 표시된다.그들은 개인의 계급/권위/속성을 가리키며, 따라서 자연수의 집합이라고 생각할 수 있다.개인과 세트 변수는 모두 보편적으로 또는 실존적으로 수량화할 수 있다.바운드 집합 변수가 없는 공식(즉, 세트 변수에 대한 정량자가 없음)을 산술이라고 한다.산술 공식에는 자유 집합 변수와 바인딩된 개별 변수가 있을 수 있다.null

개별 용어는 상수 0, 단항함수 S(후속함수), 이항 연산 +와 $\cdot {\displaystyle }$ ${\displaystyle \cdot$}($$추가 및 곱셈)에서 형성된다.후속 함수는 입력에 1을 추가한다.관계 = (평등)과 <(자연수의 비교)는 두 개인을 연관시키는 반면, 관계 ∈(멤버십)은 개인과 집합(또는 계급)을 연관시킨다.따라서 2차 산술의 언어는 에서 L={ +,= , , ,∈ ${\displaystyle {\l}=\0,S,+,\cdot ,=,<,\in$ 의 서명이 주어진다.

예를 들어 2차적인 산술 지식의 하나 공짜로 집합 변수 X이 산술적은,∀ n(n∈ X→ Sn∈ X){\displaystyle \forall n(n\in X\rightarrow Sn\in X)}, 올바른 형식의 분유와 원바운드. 구기에서 개별 변수 n( 하지만 바운드 집합 변수로 산술적 공식이 필요하다고)—whereas∃ X∀ n(n∈ X↔ n<>SS. S S S 0) ${\displaystyle \exists$ X$\forall$ n$(n\in X\left rightarrow$ n$<SSSSS0\cdot$ SSSS0$)}$은 산술적이지 않은 잘 구성된 공식으로, 한 바운드 변수 X와 하나의 바운드 개별 변수를 가지고 있다.

의미론

정량자에 대한 몇 가지 다른 해석이 가능하다.2차 논리학의 전체 의미론을 사용하여 2차 산술을 연구할 경우, 설정된 정량자 범위는 숫자 변수 범위의 모든 하위 집합에 걸쳐 있다.1차 논리(Henkin 의미론)의 의미론을 사용하여 2차 산술을 공식화하는 경우, 어떤 모델도 범위 내 설정된 변수에 대한 도메인을 포함하며, 이 도메인은 숫자 변수 영역의 전체 파워셋의 적절한 하위 집합일 수 있다(Shapiro 1991, 페이지 74–75).null

공리

기본

다음과 같은 공리는 기본 공리, 또는 때로는 로빈슨 공리로 알려져 있다.로빈슨 산술로 알려진 결과적인 1차 이론은 본질적으로 유도가 없는 페아노 산술이다.정량화된 변수에 대한 담화 영역은 N이 총칭하는 자연수로서, "0"이라고 하는$$구별된 멤버 $0{\displaystyle \mathrm{}}$ ${\displaystyle$ 0$}$을 포함한다.

원시 함수는 접두사 $S{\displaystyle }$ ${\displaystyle S$로 표시된 단항 계승함수와 각각 infix "+"와 ${\displaystyle }$ ${\displaystyle \cdot }"$로 표시된 두 개의 이진 연산, 덧셈과 곱셈이다.infix "<"로 표기되는 순서라는 원시적인 이항관계도 있다.null

후속 함수와 0을 지배하는 공리:

1. $\forall {\displaystyle \mathrm{}}$ ${\displaystyle m}$[${\displaystyle S}$ m${\displaystyle }$= ${\displaystyle 0}$→ ${\displaystyle \mathrm{\perp }}$ ${\displaystyle ]}$. ${\displaystyle \forall m[Sm=0\오른쪽$ 화살표 $\bot$ \bot $}}""$자연수의 후속은 0이 아니다")

2. $\forall {\displaystyle \mathrm{}}$ ${\displaystyle m}$ ${\displaystyle \mathrm{\forall }}$ ${\displaystyle n}$[${\displaystyle S}$ m${\displaystyle }$= ${\displaystyle S}$ ${\displaystyle n}$→ ${\displaystyle m]}$ . ${\displaystyle$\$forall$ m$\all n[Sm=Sn\rightarrow m=n].$$}("$후속 기능은 주입식")

3. $\forall {\displaystyle \mathrm{}}$ ${\displaystyle n}$[ ${\displaystyle 0}$= ${\displaystyle n}$ ${\displaystyle \mathrm{\vee }}$ m${\displaystyle }$[ ${\displaystyle S}$ m${\displaystyle }$= n ${\displaystyle ]}$. ${\displaystyle \for n[0=n]\lor \exists$ m$[Sm=n]].$$}("$모든 자연수는 0 또는 후계자")

재귀적으로 정의된 추가:

4. $\forall {\displaystyle \mathrm{}}$ ${\displaystyle m}$[ ${\displaystyle \mathrm{m}}$+ ${\displaystyle 0}$= ${\displaystyle m}$ ${\displaystyle ]}$. ${\displaystyle \forall m[m+0=m].$$}$

5. $\forall {\displaystyle \mathrm{}}$ ${\displaystyle m}$ ${\displaystyle \forall }$ ${\displaystyle n}$ [ m${\displaystyle }$+ ${\displaystyle S}$ ${\displaystyle n}$= S${\displaystyle }$( ${\displaystyle m}$+ ${\displaystyle n}$)${\displaystyle ]}$ . ${\displaystyle \forall m\forall n[m+Sn=$S($m+n]).$$}$

반복적으로 정의된 곱하기:

6. $\forall {\displaystyle \mathrm{}}$ ${\displaystyle m}$[ ${\displaystyle m}$ ${\displaystyle \cdot }$ ${\displaystyle 0}$= ${\displaystyle 0}$ ${\displaystyle ]}$. ${\displaystyle \forall m[m\cdot$ 0$=0].$$}$

7. $\forall {\displaystyle \mathrm{}}$ ${\displaystyle m}$ ${\displaystyle \forall }$ n [ ${\displaystyle m}$ ${\displaystyle \cdot }$ ${\displaystyle S}$ ${\displaystyle n}$=${\displaystyle }$( ${\displaystyle m}$ ${\displaystyle \cdot }$ ${\displaystyle n}$)${\displaystyle }$+ ${\displaystyle m]}$ . ${\displaystyle$\$forall$ n$[m\cdot Sn=(m\cdot$ n$)+m].$$}$

주문 관계 "<"를 지배하는 공리:

8. [ < → . ${\displaystyle \forall m[m<0\오른쪽$ 화살표 $\bot$ \bot $]}("$자연수가 0보다 작지 않음")

9. < m= ) . ${\displaystyle \forall n\all m[m<Sn\lor m=n].$$}$

10. [ = 0< . ${\displaystyle \forall n[0=n\lor 0<n].$$}("$모든 자연수가 0이거나 0보다 큼)"

. n[ m< n = n) < n ${\displaystyle \forall m\forall n[(Sm<n\lor Sm=n)\좌우타로우 m<n].$$}$

이 공리들은 모두 일차적인 진술이다.즉, 모든 변수는 자연수에 걸쳐 있고 그 변수의 집합이 아니며, 산술적 변수보다 더 강한 사실이다.더구나 공리 3에는 실존적 정량자가 한 명밖에 없다.공리 1과 2는 유도의 공리 스키마와 함께 N의 일반적인 Peano-Dedekind 정의를 구성한다. 이러한 공리들에 유도의 어떤 종류의 공리 스키마를 더하면 공리 3, 10, 11이 중복된다.null

유도 및 이해 스키마

φ(n)이 자유수 변수 n과 가능한 다른 자유수나 세트 변수(서면 m과 X)를 가진 2차 산술 공식이라면, φ에 대한 유도 공리는 다음과 같은 공리다.

$\displaystyle \forall X((\varphi (0)\land \forall n(n)\barphi (n)\rightarrow \varphi (Sn)\rightarrow \forall n\varphi (n)}$

(전체) 2차 유도 계획은 모든 2차 공식에 걸쳐 이 공리의 모든 사례로 구성된다.null

유도 방식의 한 가지 중요한 예는 φ이 "${\displaystyle }$ ${\displaystyle \in }$ ${\displaystyle X}$ ${\displaystyle n\in X$ 공식일 때 n이 X의 멤버(X는 자유 집합 변수임). 이 경우 φ에 대한 유도 공리는 다음과 같다.

$\displaystyle \forall X(0\in X\land) \forall n(n\in X\rightarrow Sn\in X)\rightarrow \forall n(n\in X)}$

이 문장은 2차 유도 공리라고 불린다.null

φ(n)이 자유 변수 n과 다른 자유 변수를 가진 공식이지만 변수 Z는 아닌 경우, φ에 대한 이해 공리는 공식이다.

$[\displaystyle \exists Z\frontall n(n\in Z\좌우 이동 \varphi (n))]}$

이 공리는 φ(n)을 만족시키는 자연수의$$ Z${\displaystyle }$= ${\displaystyle \{n}$ ${\displaystyle \phi }$(${\displaystyle n)\}}$ ${\displaystyle$ Z$=\n \varphi (n)\}}$을(를) $세트화$할 수 있게 한다.공식 φ이 변수 Z를 포함하지 않을 수 있다는 기술적 제한이 있다. 그렇지 않으면 공식 $n{\displaystyle }$ ${\displaystyle \notin }$ ${\displaystyle Z}$ ${\displaystyle$ n\n\$not \in Z}$이(가) 이해 공리로 이어질 수 있기$$ 때문이다.

${\displaystyle \mathrm{\exists }}$ ${\displaystyle Z}$ ${\displaystyle \mathrm{\forall }n}$(${\displaystyle n}$ ${\displaystyle \in }$ ${\displaystyle Z}$ ${\displaystyle \leftrightarrow }$ ${\displaystyle n}$ ${\displaystyle \leftrightarrow }$ Z${\displaystyle }$) ${\displaystyle \exists$ Z$\forall n(n\in$ Z$\eputrightarrow$ n$\n\in Z$

일관성이 없는 거야이 협약은 이 조항의 나머지 부분에 상정되어 있다.null

풀 시스템

2차 산술의 형식 이론(2차 산술의 언어)은 기본 공리, 모든 공식 φ에 대한 이해 공리(산술 또는 기타), 2차 유도 공리로 구성된다.이 이론은 때때로 아래에 정의되어 있는 하위 시스템과 구별하기 위해 완전한 2차 산술이라고 불린다.완전한 2차 의미론들은 가능한 모든 집합이 존재한다는 것을 의미하기 때문에, 이해 공리는 이러한 의미론을 채택할 때 연역계통의 일부로 간주될 수 있다(Shapiro 1991년, 페이지 66).null

모델

이 절에서는 1차 의미론적 2차 산수를 설명한다.집합을 M(개별 변수의 범위를 이룬다)의 2차 연산입니다. 언어를 함께 일정한 0(M의 요소), M에서 M, M에 두 이항 연산+및 M, 이진 관계 대해·;에 함수 S, M,의 하위 집합의 컬렉션을 D과의 상징이 모델 M{\displaystyle{{M\mathcal}}}.t설정된 변수의 범위.D를 생략하면 1차 산술 언어의 모델이 만들어진다.null

D가 M의 풀 파워셋일 때 모델 $M{\displaystyle \mathcal{}}$ ${\$을 풀 모델이라고 한다$$.완전한 2차 방정식의 사용은 2차 산술 모형을 전체 모델로 제한하는 것과 동등하다.사실 2차 산술의 공리는 풀 모델이 하나밖에 없다.이는 2차 유도 공리를 가진 페아노 공리가 2차 유도의 의미론 아래 하나의 모델만 가지고 있다는 데서 비롯된다.null

정의 가능한 함수

2차 산술에서 가능한 총 1차 함수는 시스템 F에서 나타낼 수 있는 함수와 정확히 동일하다(Girard and Taylor 1987, 페이지 122–123).거의 동등하게 시스템 F는 괴델의 시스템 T가 변증법 해석에서 1차 산술에 어떻게 대응하는지 평행한 방식으로 2차 산술에 해당하는 함수 이론이다.null

더 많은 종류의 모델

2차 산술 언어의 모형이 일정한 속성을 가지고 있을 때, 다음과 같은 다른 명칭으로도 불릴 수 있다.

• M이 통상적인 연산이 있는 자연수의 일반적인 집합인 경우, $M{\displaystyle \mathcal{}}$ ${\${\$mathcal{M}}$을 Ω-model이라고 한다$$.이 경우 모델은 Ω-모델을 완전히 결정하기에 충분하기 때문에 D로 식별할 수 있다.통상적인 구조와 그 모든 하위 집합을 가진 자연수의 일반적인 집합인 독특한 풀 $\Omega {\displaystyle }$ ${\displaystyle \omega}$-모델을$$ 2차 산술의 의도된 모델 또는 표준 모델이라고 부른다.^[1]
• 만약 M}(\omega)}11P(ω){\displaystyle M\prec_{1}^{1}{{P\mathcal}≺ 2차적인 산술 지식의 언어의 모델 M{M\displaystyle}는 β-model, 즉 M{M\displaystyle}에서 M{M\displaystyle}하면 만족된다 매개 변수를 사용하여 Σ11-statements들에 만족할 것과 같다라고 불린다. 월e ^[2]풀 모델(β는 β-shrewdness에서와 같이 이 이름으로 서수를 대신하는 것이 아니라 글자일 뿐이다.)β-model과 관련하여 절대적인 개념으로는 "${\displaystyle \Omega }$ ${\displaystyle \times }$ [\$displaystyle A\subseteq \time \omega }$이(가) 순서가 잘 된 인코딩$$"^[3]과 "A$Ω$ ${\displaystyle \times }$ ${\displaystyle \Omega }$ ${\displaystystyle \time \omega$}이(가 나무$$)"가 있다.^[2]
• 위의 결과는 βn-model의 n∈ N{\displaystylen\in \mathbb{N}의 위와 같이 ≺ 11{\displaystyle \prec_{1}^{1}를 제외하고 같은 정의 개념},}에≺ n1{\displaystyle \prec_{n}^{1}에 의해}교체하는 경우, 즉 Σ 11{\displaystyle \Sigma_{1}^{1}}rep.은 연장되었다l${\displaystyle {\sigma n}_{}^{}}$ ${\displaystyle {\mathrm{}}_{}^{}}$ ${\$ 이 정의를 사용하는 β-model은₀ Ω-model과 동일하다$.$^[2][4]

서브시스템

2차 산술의 명명된 서브시스템이 많다.null

서브시스템 이름의 첨자 0은 완전한 2차 유도 방식(Friedman 1976년)의 제한된 부분만을 포함하고 있음을 나타낸다.그러한 제한은 시스템의 입증-이론적 강도를 현저히 낮춘다.예를 들어 아래에서 설명한 시스템 ACA는₀ 페아노 산술과 동일하다.ACA₀ + 완전한 2차 유도 체계로 구성된 해당 이론 ACA는 페아노 산술보다 강하다.null

산술 이해

잘 연구된 서브시스템 중 많은 부분이 모델의 폐쇄 속성과 관련이 있다.예를 들어 튜링 점프에서는 풀 2차 산술의 모든 Ω 모델이 닫힌다고 볼 수 있지만 튜링 점프에서는 닫힌 모든 Ω 모델이 풀 2차 산술의 모델인 것은 아니다.하위 시스템 ACA에는₀ 튜링 점프에 따른 폐쇄 개념을 포착하기에 충분한 공리가 포함되어 있다.null

ACA는₀ 기본 공리, 산술 이해 공리 체계(즉, 모든 산술 공식 φ에 대한 이해 공리) 및 일반적인 2차 유도 공리로 구성된 이론으로 정의된다.즉, 모든 산술 공식 axi에 대한 유도 공리를 포함하는 것과 같다.null

튜링 점프, 튜링 환원성 및 튜링 조인(Simpson 2009, 페이지 311–313)에 따라 S가 닫힌 경우에만 Ω의 서브셋 집합 S가 ACA의₀ Ω 모델을 결정한다는 것을 보여줄 수 있다.null

ACA의₀ 첨자 0은 유도 공리 체계의 모든 인스턴스가 이 하위 시스템을 포함하지는 않음을 나타낸다.이는 유도 공리의 모든 인스턴스를 자동으로 만족시키는 Ω-models에 아무런 차이가 없다.그러나 그것은 비 Ω-models의 연구에서는 중요하다.모든 공식에 대한 ACA₀+유도로 구성된 시스템을 첨자가 없는 ACA라고 부르기도 한다.null

시스템 ACA는₀ 1차 산술(또는 1차 산술)의 보수적인 확장으로서, 기본 공리로 정의되며, 1차 산술(또는 1차 산술)에 1차 유도 공리 체계(모든 공식에 대해, 클래스 변수를 전혀 허용하지 않음, 바인딩 또는 기타를 포함하지 않음)를 더한 것이다.특히 제한된 유도 스키마 때문에 1차 산술과 동일한 증명-이론적 서수 ε을₀ 가지고 있다.null

수식에 대한 산술적 계층 구조

공식은 모든 정량자가 ∀n<t> 또는 ∃n<t> 형식인 경우(여기서 n은 정량화되고 t는 개별적인 용어인 경우)에서 경계가 있는 산술 또는 Δ라고⁰₀ 부른다.

$\displaystyle \forall n<t(\cdots )}$

의 약자

${\displaystyle \forall n(n<t\rightarrow \cdots )}$

그리고

$\displaystyle \put n<t(\cdots )}$

의 약자

(< ) ${\displaystyle$\ \$n(n<t\land \cdots$

공식은 ∃m_•(φ)형식의 경우 σ⁰₁⁰₁(또는 σ₁₁), ∀(또는 π)이라고 하며, 여기서 φ은_• 산술적 한정식이고 m은 개별 변수(φ)이다( free에서 자유롭다).보다 일반적으로는 π에⁰_n−1⁰_n−1 실존적, 각각 보편적, 개별적 정량자(및 σ과⁰₀⁰₀ π은 모두 Δ에⁰₀ 상당함)를 더하여 얻은 공식을 σ이라고⁰_n 한다⁰_n.건설에 의해, 이 모든 공식은 산술적인 것이며(클래스 변수는 절대 구속되지 않는다) 사실, 스콜렘 혼전 양식에 공식을 넣음으로써 모든 산술 공식은 충분히 큰 n에 대한 σ⁰_n 또는 π⁰_n 공식과 동등하다는 것을 알 수 있다.

재귀 이해

서브시스템 RCA는₀ ACA보다₀ 약한 시스템이며 역수학에서 기본 시스템으로 자주 사용된다.기본 공리, , 유도 방식⁰₁ 및 Δ⁰₁ 이해 방식 등으로 구성된다.전기 용어는 명확하다: σ⁰₁ 유도 체계는 모든 formula⁰₁ 공식 φ에 대한 유도 공리다.Δ⁰₁ 공식 같은 것이 없기 때문에 Δ⁰₁ 이해라는 용어는 더 복잡하다.대신에 Δ⁰₁ 이해 체계는 Δ⁰₁ 공식에 해당하는 모든 Δ⁰₁ 공식에 대한 이해 공리를 주장한다.이 계획은 모든 σ⁰₁ 공식 φ과 모든 π⁰₁ 공식 ψ에 대해 다음과 같은 공리를 포함한다.

${\displaystyle \all m\forall X(\forall n(\varphi(n)\좌측 화살표 \psi(n))\우측 화살표 \exists Z(n\in Z\좌측 화살표 \varphi(n))})}$

RCA의₀ 1차 결과 집합은 유도가 σ⁰₁ 공식으로 제한되는 페아노 산술의 서브시스템 Iς과₁ 동일하다.반대로 Ⅱ는₁ $\pi {\displaystyle {\mathrm{}}_{}^{}}$ 2 ${\displaystyle {\mathrm{}}_{}^{}}$ ${\$ 문장에$$ 대한 원시 재귀산술(PRA)보다 보수적이다.더욱이, ${\displaystyle {\mathrm{R}}_{}}$ C ${\displaystyle {\mathrm{A}}_{}}$ ${\displaystyle {\mathrm{}}_{}}${\$displaystyle \mathrm{RCA} _{0}$의 증명-이론 서수는 Ω으로$$^ω PRA와 동일하다.null

튜링 환원성 및 튜링 결합에 따라 S가 닫힌 경우에만 Ω의 서브셋 집합 S가 RCA의₀ Ω 모델을 결정한다는 것을 알 수 있다.특히 계산 가능한 모든 하위 집합 Ω을 수집하면 RCA의₀ Ω 모델을 얻을 수 있다.이것이 이 시스템의 이름 뒤에 있는 동기인 것이다. 만약 RCA를₀ 사용하여 세트가 존재한다는 것이 증명될 수 있다면, 그 세트는 재귀적(즉, 계산 가능)이다.null

약한 시스템

때때로 RCA보다₀ 더 약한 시스템이 필요하다.그러한 시스템 중 하나는 다음과 같이 정의된다: 먼저 지수함수로 산술 언어를 증강해야 한다(강력한 시스템에서는 일반적인 트릭에 의한 덧셈과 곱셈의 관점에서 지수화를 정의할 수 있지만, 시스템이 너무 약해지면 이것은 더 이상 가능하지 않다). 그리고 ex를 정의하는 명백한 공리에 의한 기본 공리.곱셈에서 유도하는 연역. 그 다음 시스템은 (농축된) 기본 공리, Δ⁰₁ 이해, Δ⁰₀ 유도로 구성된다.null

더 강력한 시스템

ACA에서₀, 2차 산술의 각 공식은 충분히 큰 n에 대한 σ¹_n 또는 π¹_n 공식과 동등하다.시스템 π-confection은¹₁ 기본 공리와 더불어 모든 π¹₁ 공식 φ에 대한 일반적인 2차 유도 공리와 이해 공리로 구성된 시스템이다.이는 σ-분해에¹₁ 해당한다(반면 Δ-분해와⁰₁ 유사하게 정의되는 Δ-분해가¹₁ 약하다).null

투영 결정성

투사결정성은 2인 1조로 움직이는 완벽한 정보게임마다 정수, 게임 길이 Ω, 투사적인 보수가 결정되는데, 이는 선수들 중 한 명이 승리 전략을 가지고 있다는 주장이다.(플레이가 성과급 세트에 속할 경우 첫 번째 선수가 승리하고, 그렇지 않을 경우 두 번째 선수가 승리한다.)set는 projective ifff (언어로서) 2차 산술 언어의 공식에 의해 표현 가능하며, 실수는 매개변수로 허용되므로, projective 결정성은₂ Z 언어의 스키마로서 표현 가능하다.null

2차 산술 언어로 표현할 수 있는 많은 자연 명제는 Z와₂ 심지어 ZFC와는 독립적이지만 투영적인 결정력으로부터 증명할 수 있다.예로는 co 2 ${\displaystyle {\mathrm{}}_{}^{}}$ ${\$ 세트$$, , ${\displaystyle {3\mathrm{}}_{}^{}}$ 1 ${\$1} 균일화 등을 위한 Baire의 속성, 측정 가능성 등이 있다.약한 기초 이론(예: RCA₀)에 비해 투사 결정성은 이해를 내포하고 본질적으로 완전한 2차 산술 이론을 제공한다. 투사 결정성을 가진 Z와₂ 독립적인 Z₂ 언어의 자연문장은 찾기 어렵다(Woodin 2001).null

ZFC + {n Woodin 추기경: n은 자연수}은(는) 투사 결정성을 가진 Z보다₂ 보수적이다. 즉, 2차 산술 언어의 경우 Z에서₂ 투사 결정성을 증명할 수 있다는 말은 ZFC + {n Woodin 추기경: nN}이(가) 있다.

코딩수학

2차 산수는 자연수와 자연수 집합을 직접 공식화한다.그러나, 코딩 기법을 통해 간접적으로 다른 수학적 사물을 공식화할 수 있는데, 이는 Weyl이 처음 주목한 사실(Simpson 2009, 페이지 16)이다.정수, 합리적 수, 실수는 모두 하위시스템 RCA에서₀ 완전 분리 가능한 메트릭스 공간과 이들 사이의 연속적인 함수와 함께 공식화될 수 있다(Simpson 2009, II장).null

역수학의 연구 프로그램은 수학의 이러한 공식화를 2차 산술에 사용하여 수학 이론의 입증에 필요한 설정 존재 공리를 연구한다(Simpson 2009, 페이지 32).예를 들어, 실체에서 실체까지의 기능에 대한 중간값 정리는 RCA₀ (Simpson 2009, 페이지 87)에서 증명할 수 있는 반면, 볼자노–위어스트라스 정리는 RCA를₀ 통한 ACA에₀ 해당한다(Simpson 2009, 페이지 34).null

앞서 언급한 코딩은 (Kohlenbach 2002, 섹션 4)와 같이 고차 베이스 이론과 약한 코이닉의 보조정리 이론을 가정하는 것과 같이 연속적이고 총체적인 기능에 잘 통한다.아마도 예상한 바와 같이 위상이나 측정 이론의 경우, 코딩은 예를 들어 (헌터, 2008) 또는 (노만-샌더, 2019)에서 탐구한 바와 같이 문제가 없는 것은 아니다.그러나 리만 통합 함수를 코딩하는 것조차 문제로 이어진다: (노만-샌더스, 2020)에서 보듯이, 리만 적분에 대한 아르젤라의 수렴 정리를 증명하는 데 필요한 최소(압축) 공리는 2차 코드 사용 여부에 따라 *매우* 다르다.null

참고 항목

• 파리-해링턴 정리
• 프레스버거 산술
• 트루 산술

참조

• 버지스, J. P. (2005) 프린스턴 대학 출판부의 Fixing Frege.
• 버스, S. R.(1998), 증명 이론 핸드북, 엘스비에르.null ISBN0-444-89840-9
• 프리드먼, H. (1976년), "유도가 제한된 2차 산술의 시스템," I, II(추출물).기호논리학 저널, v. 41, 페이지 557– 559. JStor
• Girard, L., Taylor(1987), Croofs and Types, Cambridge University Press.
• 힐버트, D., 버네이즈, P. (1934), 그룬들라겐 데르메틱, 스프링거-베를라크.MR0237246
• Hunter, James, Higher order Reverse Topology, Statement, University of Madisonxonsince [1]
• 콜렌바흐, U., 상위 유형의 기초와 수학적인 사용, Reflections on the foundation of mathematics, 렉트.Notes 로그, 제15권, ASL, 2002 페이지 92–116.
• Dag Normann과 Sam Sanders, 측정 이론에서의 표현, arXiv: 1902.02756, (2019)
• Dag Normann과 Sam Sanders, $\mathb{R}$, arxiv: [2], (2020), 페이지 37.
• 지그, W. (2013), 힐버트의 프로그램 & 비욘드, 옥스포드 대학 출판부.
• 샤피로, S. (1991), 근본주의가 없는 재단, 옥스퍼드 대학 출판부.ISBN 0-19-825029-0
• Simpson, S. G. (2009) 2차 산술의 서브시스템, 2차판, Perspects in Logic, Cambridge University Press.ISBN 978-0-521-88439-6 MR2517689
• 타케우티, G. (1975) 증명 이론 ISBN 0-444-10492-5
• W. H. (2001) 우딘, "연속 가설, 제1부", 미국수학협회의 통지서, 대 48 n. 6.