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 }

@[implicit_reducible]

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

Equations

• instFintypeForallFinBool_marginis u n = Pi.instFintype

@[implicit_reducible]

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

Equations

• instFintypeForallForallFinBool_marginis u n = Pi.instFintype

@[implicit_reducible]

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

Equations

• instPrimcodableForallFinBool_marginis n = Primcodable.finArrow

@[implicit_reducible]

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

Equations

• instPrimcodableForallFinBool_marginis_1 u n = Primcodable.finArrow

@[implicit_reducible]

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

Equations

• instPrimcodableForallFinSuccBool_marginis k = Primcodable.finArrow

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance instPrimcodableForallFinOfNatNatBool_marginis : Primcodable (Fin 2 → Bool)

Equations

• instPrimcodableForallFinOfNatNatBool_marginis = Primcodable.finArrow

@[implicit_reducible]

instance instEncodableForallBool_marginis : Encodable (Bool → Bool)

Equations

• instEncodableForallBool_marginis = Encodable.fintypeArrowOfEncodable

@[implicit_reducible]

instance instEncodableListBool_marginis : Encodable (List Bool)

Equations

• instEncodableListBool_marginis = List.encodable

@[implicit_reducible]

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 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 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 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 getPart (σ : List Bool) (k : ℕ) : Part Bool

Equations

• getPart σ k = ↑σ[k]?

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 : ℕ) => 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

@[implicit_reducible]

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

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

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

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)

def T_equiv : Equivalence T_equivalent

Equations

• T_equiv = ⋯

@[implicit_reducible]

instance 𝓓_setoid : Setoid (ℕ → Bool)

Equations

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

def 𝓓ₜ : Type

Equations

• 𝓓ₜ = Quotient 𝓓_setoid

@[implicit_reducible]

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

@[implicit_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 }

@[implicit_reducible]

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 }

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance blah₂ : Primcodable (Bool → Bool)

Equations

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

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

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

Equations

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