Effectivizing Lusin’s Theorem

RUSSELL MILLER

The paper discusses Turing degrees among other things. Here we formalize Turing reducibility (Degrees of unsolvability).

(Mathlib has a reduce.lean file that can be reconciled with this.)

This file introduces many-one reducibility (mapping reducibility) and proves its basic properties.

We work with a couple of classes of functions:

• mon (which includes both 𝓓₁ and 𝓓ₘ and any monoid of functions)
• mon₁ (which fits 𝓓₁ and 𝓓ₘ but not as general as mon₁)
• monₘ (which includes 𝓓ₘ but not 𝓓₁).

We show over mon₁ that the degrees are not rigid, using complementation.

Over monₘ we show that the degrees form an upper semilattice and has an automorphism that simply swaps ⊥ := ⟦∅⟧ₘ and ⊤ := ⟦ℕ⟧ₘ.

The halting problem K is defined in this context and its basic degree-theoretic properties established.

The Turing degrees 𝓓ₜ are constructed.

def injClone : mon₁

The injective functions can be used in defining 1-degrees, 𝓓₁.

Equations

• injClone = { func := Function.Injective, id := ⋯, comp := ⋯, inl := injClone._proof_1, inr := injClone._proof_2 }

instance instPrimcodableForallFinBool_marginis (n : ℕ) : Primcodable (Fin n → Bool)

Equations

• instPrimcodableForallFinBool_marginis n = Primcodable.finArrow

instance instPrimcodableForallFinBool_marginis_1 (u : ℕ → ℕ) (n : ℕ) : Primcodable (Fin (u n) → Bool)

Equations

• instPrimcodableForallFinBool_marginis_1 u n = Primcodable.finArrow

instance instPrimcodableForallFinSuccBool_marginis (k : ℕ) : Primcodable (Fin k.succ → Bool)

Equations

• instPrimcodableForallFinSuccBool_marginis k = Primcodable.finArrow

instance instDenumerableSigmaNatForallFinBool_marginis (u : ℕ → ℕ) : Denumerable ((n : ℕ) × (Fin (u n) → Bool))

Equations

• instDenumerableSigmaNatForallFinBool_marginis u = Denumerable.ofEncodableOfInfinite ((n : ℕ) × (Fin (u n) → Bool))

inductive Partrec_in (A : ℕ →. ℕ) : (ℕ →. ℕ) → Prop

• self {A : ℕ →. ℕ} : Partrec_in A A
• zero {A : ℕ →. ℕ} : Partrec_in A (pure 0)
• succ {A : ℕ →. ℕ} : Partrec_in A ↑Nat.succ
• left {A : ℕ →. ℕ} : Partrec_in A fun (n : ℕ) => ↑(some (Nat.unpair n).1)
• right {A : ℕ →. ℕ} : Partrec_in A fun (n : ℕ) => ↑(some (Nat.unpair n).2)
• pair {A f g : ℕ →. ℕ} : Partrec_in A f → Partrec_in A g → Partrec_in A fun (n : ℕ) => Nat.pair <$> f n <*> g n
• comp {A f g : ℕ →. ℕ} : Partrec_in A f → Partrec_in A g → Partrec_in A fun (n : ℕ) => g n >>= f
• prec {A f g : ℕ →. ℕ} : Partrec_in A f → Partrec_in A g → Partrec_in A (Nat.unpaired fun (a n : ℕ) => Nat.rec (f a) (fun (y : ℕ) (IH : Part ℕ) => do let i ← IH g (Nat.pair a (Nat.pair y i))) n)
• rfind {A f : ℕ →. ℕ} : Partrec_in A f → Partrec_in A fun (a : ℕ) => Nat.rfind fun (n : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> f (Nat.pair a n)

inductive Nat.Partrec_in.Code : Type

A relativized version of Nat.Partrec.Code.

• self : Code
• zero : Code
• succ : Code
• left : Code
• right : Code
• pair : Code → Code → Code
• comp : Code → Code → Code
• prec : Code → Code → Code
• rfind' : Code → Code

instance Nat.Partrec_in.Code.instInhabited : Inhabited Code

Equations

• Nat.Partrec_in.Code.instInhabited = { default := Nat.Partrec_in.Code.self }

def Nat.Partrec_in.Code.const : ℕ → Code

Returns a code for the constant function outputting a particular natural.

Equations

• Nat.Partrec_in.Code.const 0 = Nat.Partrec_in.Code.zero
• Nat.Partrec_in.Code.const n.succ = Nat.Partrec_in.Code.succ.comp (Nat.Partrec_in.Code.const n)

theorem Nat.Partrec_in.Code.const_inj {n₁ n₂ : ℕ} : Code.const n₁ = Code.const n₂ → n₁ = n₂

def Nat.Partrec_in.Code.id : Code

A code for the identity function.

Equations

• Nat.Partrec_in.Code.id = Nat.Partrec_in.Code.left.pair Nat.Partrec_in.Code.right

def Nat.Partrec_in.Code.curry (c : Code) (n : ℕ) : Code

Given a code c taking a pair as input, returns a code using n as the first argument to c.

Equations

• c.curry n = c.comp ((Nat.Partrec_in.Code.const n).pair Nat.Partrec_in.Code.id)

def Nat.Partrec_in.Code.encodeCode : Code → ℕ

An encoding of a Nat.Partrec.Code as a ℕ.

Equations

• Nat.Partrec_in.Code.self.encodeCode = 0
• Nat.Partrec_in.Code.zero.encodeCode = 1
• Nat.Partrec_in.Code.succ.encodeCode = 2
• Nat.Partrec_in.Code.left.encodeCode = 3
• Nat.Partrec_in.Code.right.encodeCode = 4
• (cf.pair cg).encodeCode = 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 5
• (cf.comp cg).encodeCode = 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode + 1) + 5
• (cf.prec cg).encodeCode = 2 * (2 * Nat.pair cf.encodeCode cg.encodeCode) + 1 + 5
• cf.rfind'.encodeCode = 2 * (2 * cf.encodeCode + 1) + 1 + 5

@[irreducible]

def Nat.Partrec_in.Code.ofNatCode : ℕ → Code

A decoder for Nat.Partrec_in.Code.encodeCode, taking any ℕ to the Nat.Partrec_in.Code it represents.

Equations

• One or more equations did not get rendered due to their size.
• Nat.Partrec_in.Code.ofNatCode 0 = Nat.Partrec_in.Code.self
• Nat.Partrec_in.Code.ofNatCode 1 = Nat.Partrec_in.Code.zero
• Nat.Partrec_in.Code.ofNatCode 2 = Nat.Partrec_in.Code.succ
• Nat.Partrec_in.Code.ofNatCode 3 = Nat.Partrec_in.Code.left
• Nat.Partrec_in.Code.ofNatCode 4 = Nat.Partrec_in.Code.right

instance Nat.Partrec_in.Code.instDenumerable : Denumerable Code

Equations

• One or more equations did not get rendered due to their size.

theorem Nat.Partrec_in.Code.encodeCode_eq : Encodable.encode = encodeCode

theorem Nat.Partrec_in.Code.ofNatCode_eq : Denumerable.ofNat Code = ofNatCode

theorem Nat.Partrec_in.Code.encode_lt_pair (cf cg : Code) : Encodable.encode cf < Encodable.encode (cf.pair cg) ∧ Encodable.encode cg < Encodable.encode (cf.pair cg)

theorem Nat.Partrec_in.Code.encode_lt_comp (cf cg : Code) : Encodable.encode cf < Encodable.encode (cf.comp cg) ∧ Encodable.encode cg < Encodable.encode (cf.comp cg)

theorem Nat.Partrec_in.Code.encode_lt_prec (cf cg : Code) : Encodable.encode cf < Encodable.encode (cf.prec cg) ∧ Encodable.encode cg < Encodable.encode (cf.prec cg)

theorem Nat.Partrec_in.Code.encode_lt_rfind' (cf : Code) : Encodable.encode cf < Encodable.encode cf.rfind'

theorem Nat.Partrec_in.Code.primrec₂_pair : Primrec₂ pair

theorem Nat.Partrec_in.Code.primrec₂_comp : Primrec₂ comp

theorem Nat.Partrec_in.Code.primrec₂_prec : Primrec₂ prec

theorem Nat.Partrec_in.Code.primrec_rfind' : Primrec rfind'

def Nat.Partrec_in.Code.eval (A : ℕ →. ℕ) : Code → ℕ →. ℕ

Equations

• One or more equations did not get rendered due to their size.
• Nat.Partrec_in.Code.eval A Nat.Partrec_in.Code.self = A
• Nat.Partrec_in.Code.eval A Nat.Partrec_in.Code.zero = pure 0
• Nat.Partrec_in.Code.eval A Nat.Partrec_in.Code.succ = ↑Nat.succ
• Nat.Partrec_in.Code.eval A Nat.Partrec_in.Code.left = ↑fun (n : ℕ) => (Nat.unpair n).1
• Nat.Partrec_in.Code.eval A Nat.Partrec_in.Code.right = ↑fun (n : ℕ) => (Nat.unpair n).2
• Nat.Partrec_in.Code.eval A (cf.pair cg) = fun (n : ℕ) => Nat.pair <$> Nat.Partrec_in.Code.eval A cf n <*> Nat.Partrec_in.Code.eval A cg n
• Nat.Partrec_in.Code.eval A (cf.comp cg) = fun (n : ℕ) => Nat.Partrec_in.Code.eval A cg n >>= Nat.Partrec_in.Code.eval A cf

noncomputable def Nat.Partrec_in.Code.jump' (A : ℕ →. ℕ) : ℕ → Bool

Equations

• Nat.Partrec_in.Code.jump' A e = decide (Nat.Partrec_in.Code.eval A (Denumerable.ofNat Nat.Partrec_in.Code e) 0).Dom

noncomputable def Nat.Partrec_in.Code.jump (A : ℕ → Bool) : ℕ → Bool

Equations

• Nat.Partrec_in.Code.jump A x = Nat.Partrec_in.Code.jump' (fun (x : ℕ) => Part.some (A x).toNat) x

def Nat.Partrec_in.Code.REPred_in (A : ℕ →. ℕ) (p : ℕ → Prop) : Prop

Equations

• Nat.Partrec_in.Code.REPred_in A p = Partrec_in A fun (a : ℕ) => Part.assert (p a) fun (x : p a) => 0

def Computable_in (f g : ℕ → ℕ) : Prop

Equations

• Computable_in f g = Partrec_in ↑g ↑f

def T_reducible (A B : ℕ → Bool) : Prop

Equations

• T_reducible A B = Computable_in (fun (k : ℕ) => (A k).toNat) fun (k : ℕ) => (B k).toNat

def «term_≤ₜ_» : Lean.TrailingParserDescr

Equations

• «term_≤ₜ_» = Lean.ParserDescr.trailingNode `«term_≤ₜ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ₜ ") (Lean.ParserDescr.cat `term 51))

theorem computable_in_refl : Reflexive Computable_in

inductive use_bound {A : ℕ → ℕ} : (ℕ →. ℕ) → ℕ → ℕ → Prop

• compu {A : ℕ → ℕ} {g : ℕ →. ℕ} {k : ℕ} : Nat.Partrec g → use_bound g k 0
• self {A : ℕ → ℕ} {k : ℕ} : use_bound (↑A) k k.succ
• pair {A : ℕ → ℕ} {f g : ℕ →. ℕ} {k uf ug : ℕ} : use_bound f k uf → use_bound g k ug → use_bound (fun (n : ℕ) => Nat.pair <$> f n <*> g n) k (max uf ug)
• comp {A : ℕ → ℕ} {f g : ℕ →. ℕ} {k uf ug : ℕ} (h : g k ≠ Part.none) : use_bound f ((g k).get ⋯) uf → use_bound g k ug → use_bound (fun (n : ℕ) => g n >>= f) k (max uf ug)

theorem computable_in_trans : Transitive Computable_in

∀ B, B ≤ₜ C → (∀ A, A ≤ₜ B → A ≤ₜ C).

def T_equivalent (A B : ℕ → Bool) : Prop

Equations

• T_equivalent A B = (T_reducible A B ∧ T_reducible B A)

instance 𝓓_setoid : Setoid (ℕ → Bool)

Equations

• 𝓓_setoid = { r := T_equivalent, iseqv := T_equiv }

def 𝓓ₜ : Type

Equations

• 𝓓ₜ = Quotient 𝓓_setoid

instance instZero𝓓ₜ : Zero 𝓓ₜ

The Turing degree 0 contains all computable sets, but by definition it is just the Turing degree of ∅.

Equations

• instZero𝓓ₜ = { zero := ⟦fun (x : ℕ) => false⟧ }

theorem T_refl : Reflexive T_reducible

instance instTransForallNatBoolT_reducible : Trans T_reducible T_reducible T_reducible

To do calc proofs with m-reducibility we create a Trans instance.

Equations

• instTransForallNatBoolT_reducible = { trans := @instTransForallNatBoolT_reducible._proof_1 }

theorem T_trans : Transitive T_reducible

T-reducibility is transitive.

theorem T_upper_cones_eq (A B : ℕ → Bool) (h : T_equivalent A B) : T_reducible A = T_reducible B

Equivalent reals have equal upper cones.

theorem T_degrees_eq (A B : ℕ → Bool) (h : T_equivalent A B) : T_equivalent A = T_equivalent B

Equivalent reals have equal degrees.

theorem T_reducible_congr_equiv (A C D : ℕ → Bool) (hCD : T_equivalent C D) : T_reducible A C = T_reducible A D

def le_T' (A : ℕ → Bool) (b : 𝓓ₜ) : Prop

As an auxiliary notion, we define [A]ₜ ≤ b.

Equations

• le_T' A b = Quot.lift (T_reducible A) ⋯ b

theorem T_reducible_congr_equiv' (b : 𝓓ₜ) (C D : ℕ → Bool) (hCD : T_equivalent C D) : le_T' C b = le_T' D b

def le_T (a b : 𝓓ₜ) : Prop

The ordering of the T-degrees.

Equations

• le_T a b = Quot.lift (fun (a : ℕ → Bool) => le_T' a b) ⋯ a

theorem le_T_refl : Reflexive le_T

The ordering of T-degrees is reflexive.

theorem le_T_trans : Transitive le_T

The ordering of T-degrees is transitive.

def T_degrees_preorder : Preorder (ℕ → Bool)

T-reducibility is a preorder.

Equations

• T_degrees_preorder = { le := T_reducible, le_refl := T_refl, le_trans := T_trans, lt_iff_le_not_ge := T_degrees_preorder._proof_1 }

instance instPartialOrder𝓓ₜ : PartialOrder 𝓓ₜ

𝓓ₜ is a partial order.

Equations

• instPartialOrder𝓓ₜ = { le := le_T, le_refl := le_T_refl, le_trans := le_T_trans, lt_iff_le_not_ge := instPartialOrder𝓓ₜ._proof_1, le_antisymm := instPartialOrder𝓓ₜ._proof_2 }

instance instZero𝓓ₜ_1 : Zero 𝓓ₜ

The nontrivial computable sets form the T-degree 0.

Equations

• instZero𝓓ₜ_1 = { zero := ⟦fun (x : ℕ) => false⟧ }

theorem idExists : Nonempty ↑{π : 𝓓ₜ → 𝓓ₜ | automorphism π}

def «term_⊕__2» : Lean.TrailingParserDescr

Make sure ♯ binds stronger than ≤ₘ.

Equations

• «term_⊕__2» = Lean.ParserDescr.trailingNode `«term_⊕__2» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ ") (Lean.ParserDescr.cat `term 71))