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 instFintypeForallFinBool_marginis (u : ℕ → ℕ) (n : ℕ) : Fintype (Fin (u n) → Bool)

Equations

• instFintypeForallFinBool_marginis u n = Pi.fintype

instance instFintypeForallForallFinBool_marginis (u : ℕ → ℕ) (n : ℕ) : Fintype ((Fin (u n) → Bool) → Bool)

Equations

• instFintypeForallForallFinBool_marginis u n = Pi.fintype

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))

instance instPrimcodableForallFinOfNatNatBool_marginis : Primcodable (Fin 2 → Bool)

Equations

• instPrimcodableForallFinOfNatNatBool_marginis = Primcodable.finArrow

instance instEncodableForallBool_marginis : Encodable (Bool → Bool)

Equations

• instEncodableForallBool_marginis = Encodable.fintypeArrowOfEncodable

instance instEncodableListBool_marginis : Encodable (List Bool)

Equations

• instEncodableListBool_marginis = List.encodable

instance instEncodableListFinOfNatNat_marginis : Encodable (List (Fin 2))

Equations

• instEncodableListFinOfNatNat_marginis = List.encodable

def turing_functional' (f : List Bool × ℕ → Part Bool) : Prop

Equations

• turing_functional' f = (Partrec f ∧ ∀ (u v : List Bool), u <+: v → f (v, 0) ≠ Part.none → f (u, 0) ≠ Part.none)

def isprefix (u : (k : ℕ) × (Fin k → Bool)) (v : (k : ℕ) × (Fin k → Bool)) : Prop

Thanks to ChatGPT.

Equations

• isprefix u v = ∃ (h : u.fst ≤ v.fst), u.snd = v.snd ∘ Fin.castLE h

def turingFunctional (f : (k : ℕ) × (Fin k → Bool) → ℕ → Part Bool) : Prop

Defining Turing functionals without using List.

Equations

• turingFunctional f = (Partrec₂ f ∧ ∀ (n : ℕ) (u v : (k : ℕ) × (Fin k → Bool)), isprefix u v → f u n ≠ Part.none → f u n = f v n)

def turingFunctional' (f : (k : ℕ) × (Fin k → Bool) → ℕ → Part Bool) : Prop

Equations

• turingFunctional' f = (Partrec₂ f ∧ ∀ (n l : ℕ) (k : Fin l.succ) (v : Fin l → Bool), f ⟨↑k, v ∘ Fin.castLE ⋯⟩ n ≠ Part.none → f ⟨↑k, v ∘ Fin.castLE ⋯⟩ n = f ⟨l, v⟩ n)

def turing_functional (f : List Bool → ℕ → Part Bool) : Prop

Equations

• turing_functional f = (Partrec₂ f ∧ ∀ (n : ℕ) (u v : List Bool), u <+: v → f u n ≠ Part.none → f u n = f v n)

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

Equations

• turingReducible A B = ∃ (φ : (k : ℕ) × (Fin k → Bool) → ℕ → Part Bool), turingFunctional φ ∧ ∀ (n : ℕ), ∃ (k : ℕ), φ ⟨k, fun (a : Fin k) => B ↑a⟩ n = ↑(some (A n))

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

Equations

• turing_reducible A B = ∃ (φ : List Bool → ℕ → Part Bool), turing_functional φ ∧ ∀ (n : ℕ), ∃ (k : ℕ), φ (List.ofFn fun (a : Fin k) => B ↑a) n = ↑(some (A n))

def get_part (σ : List Bool) (k : ℕ) : Part Bool

Equations

• get_part σ k = ↑(σ.get? k)

def getPart (σ : List Bool) (k : ℕ) : Part Bool

Equations

• getPart σ k = ↑σ[k]?

theorem for_refl : Partrec₂ get_part

theorem t_refl : Reflexive turing_reducible

def getlist' (β : ℕ → Part Bool) (l : ℕ) (h : ∀ (k : Fin l), β ↑k ≠ Part.none) : List Bool

Equations

• getlist' β l h = List.ofFn fun (k : Fin l) => (β ↑k).get ⋯

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 : ℕ) => Seq.seq (Nat.pair <$> f n) fun (x : Unit) => 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: Nat.Partrec_in.Code
• zero: Nat.Partrec_in.Code
• succ: Nat.Partrec_in.Code
• left: Nat.Partrec_in.Code
• right: Nat.Partrec_in.Code
• pair: Nat.Partrec_in.Code → Nat.Partrec_in.Code → Nat.Partrec_in.Code
• comp: Nat.Partrec_in.Code → Nat.Partrec_in.Code → Nat.Partrec_in.Code
• prec: Nat.Partrec_in.Code → Nat.Partrec_in.Code → Nat.Partrec_in.Code
• rfind': Nat.Partrec_in.Code → Nat.Partrec_in.Code

instance Nat.Partrec_in.Code.instInhabited : Inhabited Nat.Partrec_in.Code

Equations

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

def Nat.Partrec_in.Code.const : ℕ → Nat.Partrec_in.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₂ : ℕ} : Nat.Partrec_in.Code.const n₁ = Nat.Partrec_in.Code.const n₂ → n₁ = n₂

def Nat.Partrec_in.Code.id : Nat.Partrec_in.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 : Nat.Partrec_in.Code) (n : ℕ) : Nat.Partrec_in.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 : Nat.Partrec_in.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 : ℕ → Nat.Partrec_in.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 Nat.Partrec_in.Code

Equations

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

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

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

theorem Nat.Partrec_in.Code.encode_lt_pair (cf : Nat.Partrec_in.Code) (cg : Nat.Partrec_in.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 : Nat.Partrec_in.Code) (cg : Nat.Partrec_in.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 : Nat.Partrec_in.Code) (cg : Nat.Partrec_in.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 : Nat.Partrec_in.Code) : Encodable.encode cf < Encodable.encode cf.rfind'

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

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

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

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

def Nat.Partrec_in.Code.eval (A : ℕ →. ℕ) : Nat.Partrec_in.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 : ℕ) => Seq.seq (Nat.pair <$> Nat.Partrec_in.Code.eval A cf n) fun (x : Unit) => 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 : ℕ → Bool) (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 : ℕ) => Seq.seq (Nat.pair <$> f n) fun (x : Unit) => 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 : ℕ → Bool) (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 : ℕ → Bool) (B : ℕ → Bool) (h : T_equivalent A B) : T_reducible A = T_reducible B

Equivalent reals have equal upper cones.

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

Equivalent reals have equal degrees.

theorem T_reducible_congr_equiv (A : ℕ → Bool) (C : ℕ → Bool) (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 : ℕ → Bool) (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 = Preorder.mk T_refl T_trans T_degrees_preorder.proof_1

instance instPartialOrder𝓓ₜ : PartialOrder 𝓓ₜ

𝓓ₜ is a partial order.

Equations

• instPartialOrder𝓓ₜ = PartialOrder.mk 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 turing_reducible' (A : ℕ →. ℕ) (B : ℕ →. ℕ) : Prop

Equations

• turing_reducible' A B = Partrec_in B A

instance blah : Encodable (Bool → Bool)

Equations

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

theorem encode_decode (k : ℕ) : Encodable.encode (Encodable.decode k) = if k < 4 then k.succ else 0

instance blah₂ : Primcodable (Bool → Bool)

Equations

• blah₂ = Primcodable.mk blah₂.proof_4

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))

structure monₜₜextends monₘ : Type

• func : (ℕ → ℕ) → Prop
• id : self.func id
• comp : ∀ {f g : ℕ → ℕ}, self.func f → self.func g → self.func (f ∘ g)
• inl : self.func inlFun
• inr : self.func inrFun
• join : ∀ {f₁ f₂ : ℕ → ℕ}, self.func f₁ → self.func f₂ → self.func (joinFun f₁ f₂)
• const : ∀ (c : ℕ), self.func fun (x : ℕ) => c
• ttrefl : self.func fun (n : ℕ) => Encodable.encode ((Denumerable.ofNat ((k : ℕ) × (Fin k.succ → Bool)) n).snd ↑(Denumerable.ofNat ((k : ℕ) × (Fin k.succ → Bool)) n).fst)

theorem monₜₜ.ttrefl (self : monₜₜ) : self.func fun (n : ℕ) => Encodable.encode ((Denumerable.ofNat ((k : ℕ) × (Fin k.succ → Bool)) n).snd ↑(Denumerable.ofNat ((k : ℕ) × (Fin k.succ → Bool)) n).fst)

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

Equations

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