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.

structure mon : Type

An arbitrary monoid.

• func : (ℕ → ℕ) → Prop

  The functions under consideration (computable, primitive recursive, hyperarithmetic, etc.)

• id : self.func id
• comp : ∀ {f g : ℕ → ℕ}, self.func f → self.func g → self.func (f ∘ g)

theorem mon.id (self : mon) : self.func id

theorem mon.comp (self : mon) {f : ℕ → ℕ} {g : ℕ → ℕ} : self.func f → self.func g → self.func (f ∘ g)

def unitMon : mon

The unit monoid consists of id only. The corresponding degree structure has equality as its equivalence.

Equations

• unitMon = { func := fun (f : ℕ → ℕ) => f = id, id := unitMon.proof_1, comp := @unitMon.proof_2 }

def inlFun : ℕ → ℕ

Embedding on the left over ℕ.

Equations

• inlFun k = 2 * k

def inrFun : ℕ → ℕ

Embedding on the right over ℕ.

Equations

• inrFun k = 2 * k + 1

structure mon₁extends mon : Type

A monoid in which we can prove ⊕ is an upper bound, even if not the least one.

• 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

theorem mon₁.inl (self : mon₁) : self.func inlFun

theorem mon₁.inr (self : mon₁) : self.func inrFun

def injClone : mon₁

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

Equations

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

def m_reducible {m : mon} (A : ℕ → Bool) (B : ℕ → Bool) : Prop

Mapping (many-one) reducibility.

Equations

• (A ≤ₘ B) = ∃ (f : ℕ → ℕ), m.func f ∧ ∀ (x : ℕ), A x = B (f x)

Instances For

• instTransForallNatBoolM_reducible

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 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 v n = f v 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)

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
• zero: ∀ {A : ℕ →. ℕ}, Partrec_in (pure 0)
• succ: ∀ {A : ℕ →. ℕ}, Partrec_in ↑Nat.succ
• left: ∀ {A : ℕ →. ℕ}, Partrec_in fun (n : ℕ) => ↑(some (Nat.unpair n).1)
• right: ∀ {A : ℕ →. ℕ}, Partrec_in fun (n : ℕ) => ↑(some (Nat.unpair n).2)
• pair: ∀ {A f g : ℕ →. ℕ}, Partrec_in f → Partrec_in g → Partrec_in fun (n : ℕ) => Seq.seq (Nat.pair <$> f n) fun (x : Unit) => g n
• comp: ∀ {A f g : ℕ →. ℕ}, Partrec_in f → Partrec_in g → Partrec_in fun (n : ℕ) => g n >>= f
• prec: ∀ {A f g : ℕ →. ℕ}, Partrec_in f → Partrec_in g → Partrec_in (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 f → Partrec_in fun (a : ℕ) => Nat.rfind fun (n : ℕ) => (fun (m : ℕ) => decide (m = 0)) <$> f (Nat.pair a n)

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

Equations

• Computable_in f g = Partrec_in ↑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_equiv }

def 𝓓ₜ : Type

Equations

• 𝓓ₜ = Quotient 𝓓_setoid

Instances For

• instZero𝓓ₜ

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⟧ }

def turing_reducible' (A : ℕ →. ℕ) (B : ℕ →. ℕ) : Prop

Equations

• turing_reducible' A B = Partrec_in 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 m_equivalent {m : mon} (A : ℕ → Bool) (B : ℕ → Bool) : Prop

A ≡ₘ B ↔ A ≤ₘ B and B ≤ₘ A.

Equations

• (A ≡ₘ B) = (A ≤ₘ B ∧ B ≤ₘ A)

def «term_≤ₘ_» : Lean.TrailingParserDescr

A ≤ₘ B iff A is many-one reducible to B.

Equations

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

def «term_≡ₘ_» : Lean.TrailingParserDescr

A ≡ₘ B iff A is many-one equivalent to B.

Equations

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

theorem m_refl {m : mon} : Reflexive m_reducible

m-reducibility is reflexive.

theorem m_trans {m : mon} : Transitive m_reducible

m-reducibility is transitive.

instance instTransForallNatBoolM_reducible {m : mon} : Trans m_reducible m_reducible m_reducible

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

Equations

• instTransForallNatBoolM_reducible = { trans := ⋯ }

theorem m_equiv_refl {m : mon} : Reflexive m_equivalent

Many-one equivalence is reflexive.

theorem m_equiv_trans {m : mon} : Transitive m_equivalent

Many-one equivalence is transitive.

theorem m_equiv_symm {m : mon} : Symmetric m_equivalent

Many-one equivalence is symmetric.

theorem m_equiv_equiv {m : mon} : Equivalence m_equivalent

Many-one equivalence.

@[reducible, inline]

abbrev 𝓓setoid {m : mon} : Setoid (ℕ → Bool)

The degree structure 𝓓ₘ, using quotients

Quot is like Quotient when the relation is not necessarily an equivalence. We could do: def 𝓓ₘ' := Quot m_equivalent

Equations

• 𝓓setoid = { r := m_equivalent, iseqv := ⋯ }

@[reducible, inline]

abbrev 𝓓 {m : mon} : Type

The many-one degrees.

Equations

• 𝓓 = Quotient 𝓓setoid

Instances For

• instBot𝓓
• instPartialOrder𝓓
• instSemilatticeSup𝓓
• instTop𝓓
• instZero𝓓

theorem upper_cones_eq {m : mon} (A : ℕ → Bool) (B : ℕ → Bool) (h : A ≡ₘ B) : m_reducible A = m_reducible B

Equivalent reals have equal upper cones.

theorem degrees_eq {m : mon} (A : ℕ → Bool) (B : ℕ → Bool) (h : A ≡ₘ B) : m_equivalent A = m_equivalent B

Equivalent reals have equal degrees.

def le_m' {m : mon} (A : ℕ → Bool) (b : 𝓓) : Prop

As an auxiliary notion, we define [A]ₘ ≤ b to mean that the degree of A is below the degree b.

Equations

• le_m' A b = Quot.lift (m_reducible A) ⋯ b

def le_m {m : mon} (a : 𝓓) (b : 𝓓) : Prop

The ordering of the m-degrees.

Equations

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

theorem le_m_refl {m : mon} : Reflexive le_m

The ordering of m-degrees is reflexive.

theorem le_m_trans {m : mon} : Transitive le_m

The ordering of m-degrees is transitive.

def m_degrees_preorder {m : mon} : Preorder (ℕ → Bool)

m-reducibility is a preorder.

Equations

• m_degrees_preorder = Preorder.mk ⋯ ⋯ ⋯

instance instPartialOrder𝓓 {m : mon} : PartialOrder 𝓓

For example 𝓓₁ is a partial order (if not a semilattice).

Equations

• instPartialOrder𝓓 = PartialOrder.mk ⋯

instance instZero𝓓 {m : mon} : Zero 𝓓

The nontrivial computable sets form the m-degree 0.

Equations

• instZero𝓓 = { zero := ⟦fun (k : ℕ) => if k = 0 then true else false⟧ }

instance instBot𝓓 {m : mon} : Bot 𝓓

The degree ⟦∅⟧ₘ = ⊤.

Equations

• instBot𝓓 = { bot := ⟦fun (x : ℕ) => false⟧ }

instance instTop𝓓 {m : mon} : Top 𝓓

The degree ⟦ℕ⟧ₘ = ⊤.

Equations

• instTop𝓓 = { top := ⟦fun (x : ℕ) => true⟧ }

def join (A : ℕ → Bool) (B : ℕ → Bool) (k : ℕ) : Bool

The recursive join A ⊕ B.

(However, the symbol ⊕ has a different meaning in Lean.) It is really a shuffle or ♯ (backslash sha).

Equations

• (A ⊕ B) k = if Even k then A (k / 2) else B (k / 2)

def «term_⊕__1» : Lean.TrailingParserDescr

Make sure ♯ binds stronger than ≤ₘ.

Equations

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

theorem join_inl (A : ℕ → Bool) (B : ℕ → Bool) (k : ℕ) : (A ⊕ B) (inlFun k) = A k

Join works as desired on the left.

theorem join_inr (A : ℕ → Bool) (B : ℕ → Bool) (k : ℕ) : (A ⊕ B) (inrFun k) = B k

Join works as desired on the right.

theorem join_left {m : mon₁} (A : ℕ → Bool) (B : ℕ → Bool) : A ≤ₘ A ⊕ B

A ≤ₘ A ⊕ B.

theorem join_right {m : mon₁} (A : ℕ → Bool) (B : ℕ → Bool) : B ≤ₘ A ⊕ B

B ≤ₘ A ⊕ B.

noncomputable def botSwap {m : mon} : 𝓓 → 𝓓

A map on 𝓓ₘ that swaps ∅ and ℕ.

Equations

• botSwap a = if a = ⊥ then ⊤ else if a = ⊤ then ⊥ else a

theorem botSwap_inj {m : mon} : Function.Injective botSwap

Swapping ∅ and ℕ is injective on 𝓓ₘ.

theorem botSwap_surj {m : mon} : Function.Surjective botSwap

Swapping ∅ and ℕ is surjective on 𝓓ₘ.

theorem emp_not_below {m : mon} : ¬⊥ ≤ ⊤

In 𝓓ₘ, ⊥ is not below ⊤.

theorem univ_not_below {m : mon} : ¬⊤ ≤ ⊥

In 𝓓ₘ, ⊤ is not below ⊥.

theorem emp_min {m : mon} (a : 𝓓) (h : a ≤ ⊥) : a = ⊥

In 𝓓ₘ, ⊥ is a minimal element.

theorem univ_min {m : mon} (a : 𝓓) (h : a ≤ ⊤) : a = ⊤

In 𝓓ₘ, ⊤ is a minimal element.

def automorphism {α : Type} [PartialOrder α] (π : α → α) : Prop

An automorphism of a partial order is a bijection that preserves and reflects the order.

Equations

• automorphism π = (Function.Bijective π ∧ ∀ (a b : α), a ≤ b ↔ π a ≤ π b)

def cpl : (ℕ → Bool) → ℕ → Bool

The complement map on ℕ → Bool.

Equations

• cpl A k = !A k

def complementMap {m : mon} : 𝓓 → 𝓓

The complement map on 𝓓ₘ.

Equations

• complementMap = Quotient.lift (fun (A : ℕ → Bool) => ⟦cpl A⟧) ⋯

theorem emp_univ_m_degree {m : mon} : ⊥ ≠ ⊤

In 𝓓ₘ, ⊥ ≠ ⊤.

theorem botSwapNontrivial {m : mon} : botSwap ≠ id

The (⊥,⊤) swap map is not the identity.

def rigid (α : Type) [PartialOrder α] : Prop

A partial order is rigid if there are no nontrivial automorphisms.

Equations

• rigid α = ∀ (π : α → α), automorphism π → π = id

theorem half_primrec : Primrec fun (k : ℕ) => k / 2

Dividing-by-two is primitive recursive.

theorem primrec_even_equiv : PrimrecPred fun (k : ℕ) => k / 2 * 2 = k

An arithmetical characterization of "Even" is primitive recursive.

theorem even_div_two (a : ℕ) : a / 2 * 2 = a ↔ Even a

Characterizing "Even" arithmetically.

theorem even_primrec : PrimrecPred Even

"Even" is a primitive recursive predicate.

theorem primrec_join {f₁ : ℕ → ℕ} {f₂ : ℕ → ℕ} (hf₁ : Primrec f₁) (hf₂ : Primrec f₂) : Primrec fun (k : ℕ) => if Even k then f₁ (k / 2) else f₂ (k / 2)

The usual join of functions on ℕ is primitive recursive.

theorem computable_join {f₁ : ℕ → ℕ} {f₂ : ℕ → ℕ} (hf₁ : Computable f₁) (hf₂ : Computable f₂) : Computable fun (k : ℕ) => if Even k then f₁ (k / 2) else f₂ (k / 2)

The usual join of functions on ℕ is computable.

theorem getHasIte {m : mon₁} (hasIte₂ : ∀ {f₁ f₂ : ℕ → ℕ}, m.func f₁ → m.func f₂ → m.func fun (k : ℕ) => if Even k then f₁ (k / 2) else f₂ (k / 2)) (f : ℕ → ℕ) : m.func f → m.func fun (k : ℕ) => if Even k then f (k / 2) * 2 else k

An auxiliary lemma for proving that the join A₀ ⊕ A₁ is monotone in A₀ within the context of the monoid class mon₁.

def joinFun (f₁ : ℕ → ℕ) (f₂ : ℕ → ℕ) (k : ℕ) : ℕ

Coding two functions into one.

Equations

• joinFun f₁ f₂ k = if Even k then f₁ (k / 2) else f₂ (k / 2)

structure monₘextends mon₁ : Type

Requirement for a semilattice like 𝓓ₘ.

• 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

theorem monₘ.join (self : monₘ) {f₁ : ℕ → ℕ} {f₂ : ℕ → ℕ} : self.func f₁ → self.func f₂ → self.func (joinFun f₁ f₂)

theorem monₘ.const (self : monₘ) (c : ℕ) : self.func fun (x : ℕ) => c

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.

def comput : monₘ

The computable functions satisfy the requirement for a semilattice like 𝓓ₘ.

Equations

• comput = { func := Computable, id := comput.proof_1, comp := @comput.proof_2, inl := comput.proof_3, inr := comput.proof_4, join := ⋯, const := comput.proof_5 }

def primrec : monₘ

The primitive recursive functions satisfy the requirement for a semilattice like 𝓓ₘ.

Equations

• primrec = { func := Primrec, id := primrec.proof_1, comp := @primrec.proof_2, inl := Primrec.nat_double, inr := Primrec.nat_double_succ, join := ⋯, const := primrec.proof_3 }

def allMon : monₘ

The all-monoid, which will give us only three degrees, ⊥, ⊤ and 0.

Equations

• allMon = { func := fun (x : ℕ → ℕ) => True, id := trivial, comp := ⋯, inl := trivial, inr := trivial, join := ⋯, const := ⋯ }

theorem join_le_join {m : monₘ} {A₀ : ℕ → Bool} {A₁ : ℕ → Bool} (h : A₀ ≤ₘ A₁) (B : ℕ → Bool) : A₀ ⊕ B ≤ₘ A₁ ⊕ B

The join A₀ ⊕ A₁ is monotone in A₀.

theorem join_le {m : monₘ} {A : ℕ → Bool} {B : ℕ → Bool} {C : ℕ → Bool} (h₁ : A ≤ₘ C) (h₂ : B ≤ₘ C) : A ⊕ B ≤ₘ C

The join is bounded by each upper bound.

def join' {m : monₘ} (A : ℕ → Bool) (b : Quot m_equivalent) : Quot m_equivalent

The m-degree [A]ₘ ⊔ b.

Equations

• join' A b = Quot.lift (fun (a : ℕ → Bool) => Quot.mk m_equivalent (A ⊕ a)) ⋯ b

instance instSemilatticeSup𝓓 {m : monₘ} : SemilatticeSup 𝓓

𝓓ₘ is a join-semilattice.

Equations

• instSemilatticeSup𝓓 = SemilatticeSup.mk ⋯ ⋯ ⋯

theorem emp_univ {m : monₘ} (B : ℕ → Bool) (h_2 : ¬⟦B⟧ = ⟦fun (x : ℕ) => false⟧) : ⟦fun (x : ℕ) => true⟧ ≤ ⟦B⟧

This is false for 1-degrees. However, the complementing automorphism works there.

theorem univ_emp {m : monₘ} (B : ℕ → Bool) (h_2 : ⟦B⟧ ≠ ⊤) : ⊥ ≤ ⟦B⟧

In the m-degrees, if ⟦B⟧ ≠ ⊤ then ⊥ ≤ ⟦B⟧.

theorem complementMapIsNontrivial {m : mon} : complementMap ≠ id

The complement map is not the identity map of 𝓓ₘ.

theorem complementMap_surjective {m : mon} : Function.Surjective complementMap

The complement map is a surjective map of 𝓓ₘ.

theorem complementMap_injective {m : mon} : Function.Injective complementMap

The complement map is an injective map of 𝓓ₘ.

theorem complementMapIsAuto {m : mon} : automorphism complementMap

The complement map is an automorphism of 𝓓ₘ.

theorem notrigid {m : mon} : ¬rigid 𝓓

𝓓ₘ is not rigid.

theorem botSwapIsAuto {m : monₘ} : automorphism botSwap

Over a rich enough monoid, botSwap is an automorphism.

theorem emp_lt_zero {m : monₘ} : ⊥ < 0

In 𝓓ₘ, the degree of ∅ is less than 0.

theorem zero_one_m {E : monₘ} {b : Bool} (A : ℕ → Bool) : (A ≠ fun (x : ℕ) => b) ↔ (fun (x : ℕ) => !b) ≤ₘ A

∅ and ℕ are the minimal elements of 𝓓ₘ.

noncomputable def φ {e : Nat.Partrec.Code} : ℕ → Bool

The eth r.e. set

Equations

• φ n = decide (e.eval n).Dom

noncomputable def K : ℕ → Bool

Defining the halting set K as {e | φₑ(0)↓}. (There are other possible, essentially equivalent, definitions.)

Equations

• K e = decide ((Denumerable.ofNat Nat.Partrec.Code e).eval 0).Dom

theorem K_re : RePred fun (k : ℕ) => K k = true

The halting set K is r.e.

theorem Kbar_not_re : ¬RePred fun (k : ℕ) => (!K k) = true

The complement of the halting set K is not r.e.

theorem Kbar_not_computable : ¬Computable fun (k : ℕ) => !K k

The complement of the halting set K is not computable.

theorem K_not_computable : ¬Computable K

The halting set K is not computable.

def 𝓓ₘ : Type

Equations

• 𝓓ₘ = 𝓓

theorem compute_closed_m_downward (A : ℕ → Bool) (B : ℕ → Bool) (h : Computable B) (h₀ : A ≤ₘ B) : Computable A

If B is computable and A ≤ₘ B then A is computable.

theorem re_closed_m_downward {A : ℕ → Bool} {B : ℕ → Bool} (h : RePred fun (k : ℕ) => B k = true) (h₀ : A ≤ₘ B) : RePred fun (k : ℕ) => A k = true

If B is r.e. and A ≤ₘ B then A is r.e.

theorem Kbar_not_below_K : ¬(fun (k : ℕ) => decide ((!K k) = true)) ≤ₘ K

The complement of K is not m-reducible to K.