The Turing jump of a set

A set Z ⊆ ℕ is used as an oracle through its characteristic function, the total partial function Z.oracle. The jump Z.jump is the relative diagonal halting set Z' = {e | Φ_e^Z(e)↓}, where Φ_e^Z is the program numbered e of TauCeti.Oracle.Single.Code, evaluated relative to Z.oracle. The paired jump Z.pairedJump is the relative paired halting set K₀^Z = {⟨x, e⟩ | Φ_e^Z(x)↓}, with the input in the first coordinate of Nat.pair.

The main results are that the jump is a strict upper bound in the Turing order, that every set c.e. in Z reduces to it, and that the jump is monotone in the Turing order. These reductions are one-one reductions in the sense of Mathlib's OneOneReducible, and descend to Turing reducibility of the set oracles.

Main definitions

• Set.jump: the jump Z' of a set Z.
• Set.pairedJump: the paired halting set K₀^Z relative to a set Z.

Main results

• Set.oneOneReducible_jump_of_recursiveIn: every set c.e. in Z, that is, the domain of a partial function recursive in Z.oracle, reduces one-one to the jump; Set.turingReducible_jump_of_recursiveIn: so the jump decides it; Set.oneOneReducible_jump_of_rePred, Set.turingReducible_jump_of_rePred: in particular, every c.e. set reduces one-one and Turing to Z'.
• Set.oneOneEquiv_jump_pairedJump: the diagonal and paired halting sets relative to Z are one-one equivalent.
• Set.oneOneReducible_jump, Set.turingReducible_jump: Z reduces to its jump.
• Set.not_jump_turingReducible: the jump of Z is not computable relative to Z.
• Set.oneOneReducible_jump_jump, Set.turingReducible_jump_jump: if A is Turing reducible to B, then A' reduces one-one, and hence Turing, to B'.
• Set.oneOneEquiv_jump_jump, Set.turingEquivalent_jump_jump: Turing equivalent sets have one-one equivalent, and hence Turing equivalent, jumps.
• Set.degree_mem_Ioo_of_incomparable: Turing incomparable sets below (∅ : Set ℕ).jump have degrees strictly between the computable degree and (∅ : Set ℕ).jump.

References

• R. I. Soare, Recursively Enumerable Sets and Degrees, Springer, 1987, Chapter III.2.

def Set.jump (Z : Set ℕ) : Set ℕ

The jump Z' of a set Z: the indices e for which the program numbered e halts on input e relative to the oracle of Z.

def Set.pairedJump (Z : Set ℕ) : Set ℕ

The paired jump K₀^Z of a set Z: the numbers Nat.pair x e for which the program numbered e halts on input x relative to the oracle of Z.

@[simp]

theorem Set.mem_jump {Z : Set ℕ} {e : ℕ} : e ∈ Z.jump ↔ (TauCeti.Oracle.Single.Code.eval Z.oracle (Denumerable.ofNat TauCeti.Oracle.Single.Code e) e).Dom

e ∈ Z' when the program numbered e halts on input e relative to Z.

@[simp]

theorem Set.mem_pairedJump {Z : Set ℕ} {n : ℕ} : n ∈ Z.pairedJump ↔ (TauCeti.Oracle.Single.Code.eval Z.oracle (Denumerable.ofNat TauCeti.Oracle.Single.Code (Nat.unpair n).2) (Nat.unpair n).1).Dom

n ∈ K₀^Z when the program numbered by the second coordinate of n halts on the first coordinate relative to Z.

theorem Set.pair_mem_pairedJump {Z : Set ℕ} {x e : ℕ} : Nat.pair x e ∈ Z.pairedJump ↔ (TauCeti.Oracle.Single.Code.eval Z.oracle (Denumerable.ofNat TauCeti.Oracle.Single.Code e) x).Dom

Nat.pair x e ∈ K₀^Z when the program numbered e halts on input x relative to Z.

theorem Set.oneOneReducible_dom_eval_jump (Z : Set ℕ) : (fun (p : TauCeti.Oracle.Single.Code × ℕ) => (TauCeti.Oracle.Single.Code.eval Z.oracle p.1 p.2).Dom) ≤₁ fun (x : ℕ) => x ∈ Z.jump

Halting relative to Z reduces one-one to the jump of Z, uniformly in the program: the program c halts on x exactly when the program that ignores its input and runs c on x halts on its own number.

theorem Set.oneOneReducible_jump_of_recursiveIn (Z : Set ℕ) {f : ℕ →. ℕ} (hf : Nat.RecursiveIn {Z.oracle} f) : (fun (x : ℕ) => (f x).Dom) ≤₁ fun (x : ℕ) => x ∈ Z.jump

Every set c.e. in Z reduces one-one to the jump of Z: the domain of every partial function recursive in the oracle of Z reduces one-one to Z'.

theorem Set.turingReducible_jump_of_recursiveIn (Z : Set ℕ) {f : ℕ →. ℕ} (hf : Nat.RecursiveIn {Z.oracle} f) : TuringReducible {x : ℕ | (f x).Dom}.oracle Z.jump.oracle

The jump of Z decides every set c.e. in Z: the domain of a partial function recursive in the oracle of Z has an oracle Turing reducible to that of Z'.

theorem Set.oneOneReducible_jump_of_rePred (Z : Set ℕ) {A : Set ℕ} (hA : REPred fun (x : ℕ) => x ∈ A) : (fun (x : ℕ) => x ∈ A) ≤₁ fun (x : ℕ) => x ∈ Z.jump

Every c.e. set reduces one-one to the jump of Z.

theorem Set.turingReducible_jump_of_rePred (Z : Set ℕ) {A : Set ℕ} (hA : REPred fun (x : ℕ) => x ∈ A) : TuringReducible A.oracle Z.jump.oracle

The jump of Z decides every c.e. set.

theorem Set.oneOneEquiv_jump_pairedJump (Z : Set ℕ) : OneOneEquiv (fun (x : ℕ) => x ∈ Z.jump) fun (x : ℕ) => x ∈ Z.pairedJump

The diagonal and paired halting sets are one-one equivalent, relative to every set Z.

theorem Set.turingEquivalent_jump_pairedJump (Z : Set ℕ) : TuringEquivalent Z.jump.oracle Z.pairedJump.oracle

The diagonal and paired halting sets relative to Z have Turing equivalent oracles.

theorem Set.oneOneReducible_jump (Z : Set ℕ) : (fun (x : ℕ) => x ∈ Z) ≤₁ fun (x : ℕ) => x ∈ Z.jump

A set reduces one-one to its jump.

theorem Set.turingReducible_jump (Z : Set ℕ) : TuringReducible Z.oracle Z.jump.oracle

A set is Turing reducible to its jump.

theorem Set.not_jump_turingReducible (Z : Set ℕ) : ¬TuringReducible Z.jump.oracle Z.oracle

The jump is not computable relative to Z: the oracle of Z' is not Turing reducible to the oracle of Z.

theorem Set.recursiveIn_eval_diag (Z : Set ℕ) : Nat.RecursiveIn {Z.oracle} fun (e : ℕ) => TauCeti.Oracle.Single.Code.eval Z.oracle (Denumerable.ofNat TauCeti.Oracle.Single.Code e) e

Diagonal evaluation of the oracle-program numbering is recursive in the oracle of Z.

theorem Set.oneOneReducible_jump_jump {A B : Set ℕ} (h : TuringReducible A.oracle B.oracle) : (fun (x : ℕ) => x ∈ A.jump) ≤₁ fun (x : ℕ) => x ∈ B.jump

The jump is monotone: if A is Turing reducible to B, then A' reduces one-one to B'.

theorem Set.turingReducible_jump_jump {A B : Set ℕ} (h : TuringReducible A.oracle B.oracle) : TuringReducible A.jump.oracle B.jump.oracle

The jump is monotone: if A is Turing reducible to B, then so is A' to B'.

theorem Set.oneOneEquiv_jump_jump {A B : Set ℕ} (h : TuringEquivalent A.oracle B.oracle) : OneOneEquiv (fun (x : ℕ) => x ∈ A.jump) fun (x : ℕ) => x ∈ B.jump

Turing equivalent sets have one-one equivalent jumps.

theorem Set.turingEquivalent_jump_jump {A B : Set ℕ} (h : TuringEquivalent A.oracle B.oracle) : TuringEquivalent A.jump.oracle B.jump.oracle

Turing equivalent sets have Turing equivalent jumps.

theorem Set.degree_mem_Ioo_of_incomparable {A B : Set ℕ} (hA : TuringReducible A.oracle ∅.jump.oracle) (hB : TuringReducible B.oracle ∅.jump.oracle) (hAB : ¬TuringReducible A.oracle B.oracle) (hBA : ¬TuringReducible B.oracle A.oracle) : toAntisymmetrization TuringReducible A.oracle ∈ Ioo (toAntisymmetrization TuringReducible ∅.oracle) (toAntisymmetrization TuringReducible ∅.jump.oracle)

If A and B are Turing incomparable sets both Turing reducible to (∅ : Set ℕ).jump, then the Turing degree of A lies strictly between the computable degree and (∅ : Set ℕ).jump.