Many-one reducibility and its automorphisms

Main statements:

• m_reducible : m-reducibility
• `

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

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.

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_trans {m : mon} : Transitive m_reducible

m-reducibility is transitive.

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

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.

theorem m_reducible_congr_equiv {m : mon} (A : ℕ → Bool) (C : ℕ → Bool) (D : ℕ → Bool) (hCD : C ≡ₘ D) : (A ≤ₘ C) = (A ≤ₘ D)

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

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

Equations

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

theorem m_reducible_congr_equiv' {m : mon} (b : 𝓓) (C : ℕ → Bool) (D : ℕ → Bool) (hCD : C ≡ₘ D) : le_m' C b = le_m' D b

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

The ordering of the m-degrees.

Equations

• le_m a b = Quot.lift (fun (a : ℕ → Bool) => le_m' a 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))

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

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

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_inr' (A : ℕ → Bool) (B : ℕ → Bool) : (A ⊕ B) ∘ inrFun = B

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 }

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

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

def induces {m : mon} (f : 𝓓 → 𝓓) (F : (ℕ → Bool) → ℕ → Bool) : Prop

Equations

• induces f F = ∃ (hF : ∀ (A B : ℕ → Bool), A ≡ₘ B → F A ≡ₘ F B), f = Quotient.lift (fun (A : ℕ → Bool) => ⟦F A⟧) ⋯

def induced {m : mon} (f : 𝓓 → 𝓓) : Prop

Equations

• induced f = ∃ (F : (ℕ → Bool) → ℕ → Bool), induces f F

def induced₀ {m : mon} (π : 𝓓 → 𝓓) : Prop

Induced by a function on ℕ.

Equations

• induced₀ π = ∃ (f : ℕ → ℕ), induces π fun (A : ℕ → Bool) => A ∘ f

theorem id_induced₀ {m : mon} : induced₀ id

The identity automorphism is induced by a function on ℕ.

theorem complementMap_is_not_induced₀ {m : mon} : ¬induced₀ complementMap

The complement automorphism is not induced by a function on ℕ.

theorem complementMap_is_induced {m : mon} : induced complementMap

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

theorem botSwap_is_induced_helper {m : monₘ} {A : ℕ → Bool} {B : ℕ → Bool} (hAB : A ≡ₘ B) : (if A = fun (x : ℕ) => false then fun (x : ℕ) => true else if A = fun (x : ℕ) => true then fun (x : ℕ) => false else A) ≤ₘ if B = fun (x : ℕ) => false then fun (x : ℕ) => true else if B = fun (x : ℕ) => true then fun (x : ℕ) => false else B

theorem botSwap_is_induced {m : monₘ} : induced botSwap

The botSwap automorphism is induced by a function on reals.

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⟧ = ⊥) : ⊤ ≤ ⟦B⟧

If b ≠ ⊥ then ⊤ ≤ 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 cplAuto {m : mon} (A : ℕ → Bool) (B : ℕ → Bool) : A ≤ₘ B ↔ cpl A ≤ₘ cpl B

Complementation is an automorphism not only of the partial order 𝓓ₘ, but of the preorder m_reducible! (That is true for Turing degrees too. To rule out that there is an automorphism of the preorder for Turing degrees that maps something to an element of a different Turing degree we would have to rule out e.g. a homeomorphism inducing an automorphism. )

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 𝓓ₘ, since A ≠ ⊥ ↔ ⊤ ≤ A and A ≠ ⊤ ↔ ⊥ ≤ A.

theorem bot_property {E : monₘ} (a : 𝓓) : a ≠ ⊥ ↔ ⊤ ≤ a

theorem top_property {E : monₘ} (a : 𝓓) : a ≠ ⊤ ↔ ⊥ ≤ a

def is_minimal {α : Type u_1} [PartialOrder α] (a : α) : Prop

Equations

• is_minimal a = ∀ b ≤ a, b = a

theorem bot_is_minimal {E : monₘ} : is_minimal ⊥

April 17, 2025

theorem top_is_minimal {E : monₘ} : is_minimal ⊤

theorem only_two_minimals {E : monₘ} (a : 𝓓) : is_minimal a ↔ a = ⊤ ∨ a = ⊥

def is_least {α : Type u_1} [PartialOrder α] (a : α) : Prop

Equations

• is_least a = ∀ (b : α), a ≤ b

theorem no_least_if_two_minimal {α : Type u_1} [PartialOrder α] (u : α) (v : α) (huv : u ≠ v) (hu : is_minimal u) (hv : is_minimal v) (a : α) : ¬is_least a

theorem no_least_m_degree {E : monₘ} (a : 𝓓) : ¬is_least a

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.

noncomputable def Km : 𝓓

Equations

• Km = ⟦K⟧

noncomputable def Kbarm : 𝓓

Equations

• Kbarm = ⟦cpl K⟧

theorem Kbarm_not_below_Km : ¬Kbarm ≤ Km

theorem Km_not_below_Kbarm : ¬Km ≤ Kbarm

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

Two m-degrees are automorphic if some automorphism maps one to the other.

Equations

• automorphic a b = ∃ (π : 𝓓 → 𝓓), automorphism π ∧ π a = b

theorem kkbarautomorphic : automorphic Km Kbarm

theorem bijinvfun {α : Type u_1} [Nonempty α] (f : α → α) (h : Function.Bijective f) : Function.Bijective (Function.invFun f)

Surely this should already exist in Mathlib?

theorem automorphism_comp {m : mon} (π : 𝓓 → 𝓓) (hπ : automorphism π) (ρ : 𝓓 → 𝓓) (hρ : automorphism ρ) : automorphism (ρ ∘ π)

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

Equations

• automorphic_le a b = ∃ (c : 𝓓), a ≤ c ∧ automorphic b c

theorem automorphic_le_refl {m : mon} : Reflexive automorphic_le

theorem automorphic_le_trans {m : mon} : Transitive automorphic_le

instance instPreorder𝓓 {m : mon} : Preorder 𝓓

Equations

• instPreorder𝓓 = Preorder.mk ⋯ ⋯ ⋯

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

is this the same as just automorphic?

Equations

• automorphic_equiv a b = (automorphic_le a b ∧ automorphic_le b a)