ファイル置き場 Sendai Logic Homepage 101210izawa

(1)

高階算術における逆数学

井澤昇平

東北大学理学研究科数学専攻東北大学基礎論セミナー２０１０ねん１２がつ１０にち

(2)

The plan of the contents of my thesis.

Introduction.

The formal system finite type arithemetic and axioms in finite type arithmetic.

Cardinalities in finite type arithmetic. The hierarchy of comprehension axioms. The hierarchy of choice axioms.

Reverse mathematics.

(3)

The formal system finite type arithmetic.

1. The formal system finite type arithmetic.

1

The formal system finite type arithmetic.

2

Cardinalities in finite type arithmetic.

3

The hierarchy of comprehension and choice axioms.

4

Reverse mathematics.

(4)

Finite type arithmetic is a formal system based on typed λ-calculus. sorts.

1 _M

0 ←→ N

2 _M

σ→τ ←→ the set of all maps Mσ to Mτ

where σ and τ are given sorts.

In short, 0 → 0 is denoted by 1. similarly n → 0 is denoted by n + 1. σ1 → (σ2 → τ ) is denoted by (σ1, σ2) → τ .

(5)

Language.

(Constants) 0, S, R0

(λ-abstractions) λx^σ.t^τ (the sort is σ → τ .) (Applications) t^σ→τ(s^σ) (the sort is τ .)

where t and s are given terms, x is a variable symbol.

The notation x^σ means x is a σ-sort variable, t^τ means t is a τ -sort term etc.

axiom of λ-calculus. (λ-reduction)

(λx^σ.t^τ)(s^σ) = t[s/x]. (extensionality)

∀x^σ→τ∀y^σ→τ(x = y ↔ ∀z^σ(x(z) = y(z))).

(6)

RCA^ω₀ is the axiom consists of the following formulas. The axiom of λ-calculus.

∀x⁰(∃y⁰(x = S(y)) ↔ x ̸= 0), ∀x⁰∀y⁰(S(x) = S(y) → x = y) (Existence of primitive recursion operator.)

∀f¹∀n⁰∀m⁰

[ R0(f, n)(0) = n,

R0(f, n)(S(m)) = f (m, R0(f, n)(m)). ]

(Induction axiom.)

∀A¹(0 ∈ A ∧ ∀n⁰(n ∈ A → S(n) ∈ A) → ∀n(n ∈ A)). (Axiom of choice for (1, 0).)

∀A^(1,0)→0[(∀x¹∃y⁰(x, y) ∈ A) → (∃F^1→0∀x(x, F (x)) ∈ A)].

(7)

Definition.

Q^σ-CA^τ: ∃X^{τ →0}∀x^τ(x ∈ X ↔ ϕ(x))

where ϕ is described by =0, Boolean connections and σ variable quantifiers ∃y^σ, ∀y^σ.

Eσ→0 : ∃E^(σ→0)→0∀x^σ→0(x ∈ E ↔ ∀y^σx(y) = 0) FAC^σ,τ:

∀A^{(σ,τ )→0}(∀x^σ∃y^τ((x, y) ∈ A) → ∃F^σ→τ((x, F (x)) ∈ A)). GAC^σ,τ:

∀A^{(σ,τ )→0}∃G^{(σ,τ )→0}

( G ⊂ A

∧∀x(∃y; (x, y) ∈ A → ∃!y; (x, y) ∈ G) )

.

Proposition.

{Q^σ-CA^τ}τ is equivalent to (Eσ→0) over RCA^ω₀.

(8)

Cardinalities in finite type arithmetic.

2. Cardinalities in finite type arithmetic.

1

The formal system finite type arithmetic.

2

Cardinalities in finite type arithmetic.

3

The hierarchy of comprehension and choice axioms.

4

Reverse mathematics.

(9)

We say A^σ→0 a σ-set if ∀x^σ; A(x) ≤ 1. Definition. (Cardinalities of sets) Let A, B be σ-set, τ -set respectively.

A ≤sB :⇐⇒ A = ◦/ ∨ ∃P^{τ →σ}∀x ∈ A∃y ∈ B(P (y) = x). (A is smaller than B in the sense of surjection.)

A ≤i B :⇐⇒ ∃I^σ→τ∀x, y ∈ A(I(x) ∈ B ∧ (x ̸= y → I(x) ̸= I(y))).

(A is smaller than B in the sense of injection.) A ≤ B :⇐⇒ ∃P^{τ →σ}, I^σ→τ(∀x ∈ A; (P (I(x)) = x). (A is smaller than B in the sense of retraction.)

A ≡ B :⇐⇒ ∃F^{τ →σ}, G^σ→τ(∀x ∈ A; F (G(x)) = x ∧ ∀y ∈ B; G(F (y)) = y).

(A has the same cardinality to B in the sense of inverse mappings.)

(10)

Definition. (the rank of sorts)

The rank of sort is defined as follows inductively. rank(0) := 0

rank(σ → τ ) := max(rank(σ) + 1, rank(τ )) Notation: i^σ→0_σ := λx^σ.1⁰

i.e. iσ is the set of all σ-sort elements.

In the standard model, the rank(σ) is corresponded to the

cardinality of iσ. That is, the domain of σ-sort of standard model has the same cardinality of the set obtained from a countable set by rank(σ)-times power set operator.

(11)

Theorem

1 _RCA^ω

0 ^{⊢ i}^σ ^{≤ i}^σ^′ if rank(σ) ≤ rank(σ^′). Especially, i_σ _{≤ i}_rank(σ)_{≤ i}_σ for all sort σ.

2 _RCA^ω

0 ^{⊢ i}ⁿ⁺¹ ^̸≤^s ⁱⁿ^.

3 _RCA^ω

0 ^{⊢ i}^σ ^{≡ i}¹ if rank(σ) = 1.

As the corollary of 1, ”the higher rank sentence implies the lower rank sentence” in many ”natural” families of sentences. E.g. Proposition.

Let σ, σ^′, τ, τ^′ be sorts and assume rank(σ) ≤ rank(σ^′),

rank(τ ) ≤ rank(τ^′). Then the following statements are provable in RCA^ω₀.

1 _(E

σ^′→0) → (Eσ→0).

2 _FAC^σ^′^,τ^′ _{→ FAC}^σ,τ_. 3 _GAC^σ^′^,τ^′ _{→ GAC}^σ,τ_.

(12)

The hierarchy of comprehension and choice axioms.

3. The hierarchy of comprehension and choice

axioms.

1

The formal system finite type arithmetic.

2

Cardinalities in finite type arithmetic.

3

The hierarchy of comprehension and choice axioms.

4

Reverse mathematics.

(13)

Theorem.

Let n ≥ 1 and T be a (universal closure of) Q^≤n−1-formula. Then the following holds.

RCA^ω₀ + En+1+ T ⊢ Con(RCA^ω₀ + En+ T ). Thus, RCA^ω₀ + En does not imply En+1.

(14)

Proposition.

The following implications is provable in RCA^ω₀.

1 _E

n+2^{+ GAC}^n+1,n ^{⇒ E}n+1+ n-GWO + n-TR.

2 _E

n+1+ n-GWO ⇒ En+1+ GAC^n+1,n. Theorem.

RCA^ω₀ + En+1+ n-GWO + n-TR ⊢ Con(RCA^ω₀ + En+1+ n-GWO).

(15)

Definition.

1 (σ-GWO) ∃ <, G

( W O(iσ, <)

∧ G = {(X, y)|X ⊂ in, y = minX} )

2 _(σ-TR)

∀A, X, <; W O(X, <) → ∃Y ∀x^σ, α^σ;

(x, α) ∈ Y ↔ (α ∈ X ∧ (x, {(y, β)|β < α, (y, β) ∈ Y }) ∈ A) Here W O(X, <) is the assertion that < is a well-ordering on a set X.

{(y, β)|β < α, (y, β) ∈ Y }) ∈ A is described as the following form:

∃Z((x, Z) ∈ A ∧ ∀y, β;

(y, β) ∈ Z ↔ (β ∈ X ∧ β < α ∧ (y, {(z, γ)|γ < β, (z, γ) ∈ Z}) ∈ Z)) Thus RCA^ω₀ + En+2 ⊢ n-TR holds.

(16)

4. Reverse mathematics.

1

The formal system finite type arithmetic.

2

Cardinalities in finite type arithmetic.

3

The hierarchy of comprehension and choice axioms.

4

Reverse mathematics.

(17)

Graph type formalization and Function type formalization. existence of free algebras.

reverse mathematical results.

(18)

Graph type formalization 1/2

Example./Definition.

A graph type n abelian group is a pair (A, =A, +A, 0A, −A) s.t.

1 _A^n→0 _{is a set.}

2 ₌

A is an equivalence relation on A.

3 ₊

A⊂ A × A × A, etc.

4 ∀a, b ∈ A∃c ∈ A; (a, b, c) ∈ +A 5 _{If a}

1 =Aa2, b1 =Ab2, (a1, b1, c1) then (a2, b2, c2) ∈ +A↔c1 =A c2.

6 _{a +}

Ab =Ad, d +Ac =Af, b +Ac =Ae, a +Ae =A g → f =Ag. etc.

(19)

Graph type formalization 2/2

A graph type homomorphism F of abelian group from A to B is

1 _{F ⊂ A × B.}

2 ∀a ∈ A∃b ∈ B; (a, b) ∈ F .

3 _{If (a}

1, b1) ∈ F, a1 =A a2 then (a2, b2) ∈ F → b1 =B b2.

4 _{F (a}

1+Aa2) =B F (a1) +BF (a2).

(20)

Function type formalization

A function type n abelian group is a pair (A, =A, +A, 0A, −A) s.t.

1 _An→0 _{is a set.}

2 ₌

A is an equivalence relation on A.

3 ₊^(n,n)→n

A s.t. a, b ∈ A → a +Ab ∈ Aetc.

4 _{If a}

1 =Aa2, b1 =Ab2 then a1+ b1 =A a2+Ab2.

5 _{(a +}

Ab) +Ac =Aa +A(b +Ac). etc.

A function type homomorphism F from A to B is

1 a ∈ A → F (a) ∈ B.

2 _{If a}

1 =Aa2 then F (a1) =B F (a2).

(21)

Existence of free algebras.

Proposition.

Following assertion is provable in

(RCA^ω₀ + En+ ∆ⁿ₁-CAⁿ+ Σⁿ₁-IA/RCA^ω₀ + En+ n-FPR). For every n-set A, there exists a (graph/function) type free abelian group freely generated by A

Similar statements holds for ring, lattice etc.

We write BASEⁿ RCA^ω₀ + En+ ∆ⁿ₁-CAⁿ+ Σⁿ₁-IA when we consider graph type formalization and RCA^ω₀ + En+ n-FPR when we consider function type formalization.

(22)

Definition. (∆ⁿ₁-CAⁿ)

∀A∀B

[ ∀xⁿ(∃yⁿ; (x, y) ∈ A) ↔ (∀zⁿ; (x, z) ∈ B))

→ ∃X∀x(x ∈ X ↔ ∃y; (x, y) ∈ A)

]

Definition. (Σ^σ₁-IA)

∀A^(0,σ)→0





( ∃x^σ; (0⁰, x) ∈ A

∧ ∀k(∃x; (k, x) ∈ A → ∃x; (S(k), x) ∈ A) )

→ ∀k∃x; (k, x) ∈ A





Definition. (σ-FPR)

∃R(σ,(0,σ)→σ)→(0→σ)

σ ∀x^σ∀f^(0,σ)→σ∀k⁰ ( Rσ(x, f )(0) = x

∧ Rσ(x, f )(S(k)) = f (k, Rσ(x, f )(k)) )

(23)

reverse mathematics 1/3

Proposition.

The following implications holds in BASEⁿ. RCA^ω₀ + E_n+1+ n-TR + n-GWO (or n-FWO)

⇒ Every n-type non-zero commutative ring has a maximal ideal.

⇒ Qⁿ-CAⁿ. Qⁿ-CAⁿ / E_n+1

⇔ There exists [a subgroup 2A / a functional A maps 2A] for all n-type abelian group.

Here 2A = {a ∈ A|∃x ∈ A; x + x = a}.

(24)

reverse mathematics 2/3

Proposition. (Graph type only)

The following implications holds in BASEⁿ. RCA^ω₀ + En+1+ n-TR + n-GWO (or n-FWO)

⇒ Every n-type vector space over a n-type field has a basis. Every n-type vector space over a n-type field has a basis +Qⁿ-CAⁿ ⇒ MC^n,n.

Every n-type vector space over a n-type field has a basis +GAC^n,n ⇒ Qⁿ-CAⁿ.

(25)

Definition. (Multiple choice) MC^σ,τ:∀A^{(σ,τ )→0}







∀x∃y((x, y) ∈ A)

→ ∃F^{(σ,τ )→0}







F ⊂ A

∧∀x∃y((x, y) ∈ F )

∧

( ∀x∃t⁰∃z^0→τ∀y^τ((x, y) ∈ F

↔ ∃s < t(y = z(s)))

)













(26)

reverse mathematics 3/3

Theorem.

The following statements are equivalent over RCA^ω₀ + En+1.

1 (consistency principle) For every binary mess M on in, there exists a function in → {0, 1} which is consistent with M .

2 Every n-type non-zero commutative ring has a prime ideal.

3 (completeness theorem) Every consistent theory on a n-type language has a model.

4 (compactness theorem) Every theory on a n-type language that every finite subset has a model has a model.

(27)

Definition.

Binary mess on a set A is a set M of functions satisfies following conditions;

A member of M is a function from a finite subset of A to {0, 1}.

For every finite subset B of A, there exists t ∈ M such that dom(t) = B.

t|B ∈ M for every t ∈ M and B ⊂ dom(t). Remark.

Consistency principle seems to play the role similar to WKL.

(28)

1 Ulrich Kohlenbach, Higher Order Reverse Mathematics, Lecture Notes in Logic, 2001

2 James Hunter, Higher-Order Reverse Topology, Ph.D Thesis University of Wisconsin, 2008

3 Stephen G. Simpson, Subsystems of Second Order Arithmetic second edition, Springer-Verlag, 2009

4 Thomas J. Jech, The Axiom of Choice, North-Holland, 1973

5 Andreas Blass, Existence of Bases Implies the Axiom of Choice, Contemporary Mathematics, vol 31(1984)