The Arithmetical Hierarchy

This file develops the iterated jump operator, the sets ∅⁽ⁿ⁾, and the levels Σ⁰ₙ, Π⁰ₙ, Δ⁰ₙ of the arithmetical hierarchy relative to oracle computability.

def Computability.TuringJump (n : ℕ) (f : ℕ →. ℕ) : ℕ →. ℕ

The iterated Turing jump: TuringJump n f is the n-fold jump of f.

Equations

• Computability.TuringJump 0 f = f
• Computability.TuringJump n_2.succ f = Computability.TuringJump n_2 f⌜

def Computability.arithJumpBase : ℕ → ℕ →. ℕ

The n-fold jump of the empty oracle (totally undefined). Used as an oracle function.

Equations

• Computability.arithJumpBase 0 = fun (x : ℕ) => Part.none
• Computability.arithJumpBase n_1.succ = Computability.arithJumpBase n_1⌜

def Computability.arithJumpSet (n : ℕ) : Set ℕ

The classical ∅⁽ⁿ⁾ set: the domain of the n-fold jump of the empty oracle.

Equations

• Computability.arithJumpSet n = (Computability.arithJumpBase n).Dom

@[reducible, inline]

abbrev Computability.K : Set ℕ

The halting set K = ∅', the domain of the first jump of the empty oracle.

Equations

• Computability.K = Computability.arithJumpSet 1

def Computability.decidableIn (O : Set (ℕ →. ℕ)) (A : Set ℕ) : Prop

A set A is decidable in O if its indicator is computable in O.

Equations

• Computability.decidableIn O A = ∃ (f : ℕ → Bool), Computability.ComputableIn O f ∧ ∀ (n : ℕ), A n ↔ f n = true

def Computability.Delta00 (A : Set ℕ) : Prop

The base level Δ⁰₀: sets decidable in the empty oracle.

Equations

• Computability.Delta00 A = Computability.decidableIn ∅ A

def Computability.Sigma00 (A : Set ℕ) : Prop

The base level Σ⁰₀, equal to Δ⁰₀.

Equations

• Computability.Sigma00 = Computability.Delta00

def Computability.Pi00 (A : Set ℕ) : Prop

The base level Π⁰₀, equal to Δ⁰₀.

Equations

• Computability.Pi00 = Computability.Delta00

def Computability.Sigma0 (n : ℕ) (A : Set ℕ) : Prop

The Σ⁰ₙ level of the arithmetical hierarchy.

Equations

• Σ⁰_ 0 A = Computability.decidableIn ∅ A
• Σ⁰_ n_2.succ A = Computability.recursivelyEnumerableIn {Computability.arithJumpBase n_2} A

def Computability.Pi0 (n : ℕ) (A : Set ℕ) : Prop

The Π⁰ₙ level: complements of Σ⁰ₙ sets.

Equations

• Π⁰_ n A = Σ⁰_ n Aᶜ

def Computability.Delta0 (n : ℕ) (A : Set ℕ) : Prop

The Δ⁰ₙ level: sets that are both Σ⁰ₙ and Π⁰ₙ.

Equations

• Δ⁰_ n A = (Σ⁰_ n A ∧ Π⁰_ n A)

def Computability.«termΣ⁰_» : Lean.ParserDescr

The Σ⁰ₙ level of the arithmetical hierarchy.

Equations

• Computability.«termΣ⁰_» = Lean.ParserDescr.node `Computability.«termΣ⁰_» 1024 (Lean.ParserDescr.symbol "Σ⁰_")

def Computability.«termΠ⁰_» : Lean.ParserDescr

The Π⁰ₙ level: complements of Σ⁰ₙ sets.

Equations

• Computability.«termΠ⁰_» = Lean.ParserDescr.node `Computability.«termΠ⁰_» 1024 (Lean.ParserDescr.symbol "Π⁰_")

def Computability.«termΔ⁰_» : Lean.ParserDescr

The Δ⁰ₙ level: sets that are both Σ⁰ₙ and Π⁰ₙ.

Equations

• Computability.«termΔ⁰_» = Lean.ParserDescr.node `Computability.«termΔ⁰_» 1024 (Lean.ParserDescr.symbol "Δ⁰_")