Weihrauch Degrees

Origin. Klaus Weihrauch introduced the reducibility in the late 1980s within his Type-2 Theory of Effectivity; it circulated in two unpublished 1992 technical reports, "The degrees of discontinuity of some translators between representations of the real numbers" (ICSI TR-92-050, Berkeley) and "The TTE-interpretation of three hierarchies of omniscience principles" (Informatik Berichte 130, FernUniversität Hagen), and in Hagen theses of von Stein, Mylatz, Brattka, Hertling and Pauly. The modern theory dates from Gherardi and Marcone, "How incomputable is the separable Hahn-Banach theorem?" (Notre Dame Journal of Formal Logic 50(4): 393–425, 2009), which generalized the reducibility to multi-valued problems and proposed it as a uniform version of reverse mathematics, and from Brattka and Gherardi, "Weihrauch degrees, omniscience principles and weak computability" (Journal of Symbolic Logic 76(1): 143–176, 2011) and "Effective choice and boundedness principles in computable analysis" (Bulletin of Symbolic Logic 17(1): 73–117, 2011); Pauly, "On the (semi)lattices induced by continuous reducibilities" (Mathematical Logic Quarterly 56(5): 488–502, 2010), supplied the lattice structure independently. Brattka, Gherardi and Pauly's survey "Weihrauch Complexity in Computable Analysis" (2018) fixes the state of the subject.

Models. A calibration of the uniform computational content of theorems. A theorem of the form ∀x ∈ D ∃y P(x,y) becomes a problem — the partial multi-valued function on represented spaces sending each instance x to its set of solutions y — and f ≤_W g holds when f can be computed by one application of g together with computable pre- and post-processing of names. The degrees measure what a single use of one theorem contributes to another, uniformly in the instance: where Turing Degrees compare sets by unrestricted oracle access and Reverse Mathematics compares theorems by provability over RCA₀, Weihrauch degrees compare theorems as transformations, counting uses and forbidding non-uniform case distinctions. The subject grows out of Computable Analysis, whose central fact — computable implies continuous — makes discontinuous theorems non-computable and raises the question this lattice answers: how discontinuous, and in what way.

Formalism.

Reducibility: f ≤_W g iff there are computable H, K on Baire space with H⟨id, GK⟩ a realizer of f whenever G is a realizer of g. Strong variant f ≤_sW g: HGK, without access to the original input in post-processing. f is computable iff f ≤_W id; Theorem: f ≤_W g iff a Turing machine computes f using exactly one application of g.

Lattice structure: Weihrauch degrees form a distributive lattice: supremum ⊔ (coproduct), infimum ⊓, bottom 0; 1 = the computable problems. No greatest degree (given the axiom of choice for Baire space), and no non-trivial countable suprema (Higuchi and Pauly); neither a Brouwer nor a Heyting algebra. Operations: product f × g (both in parallel), finite parallelization f*, parallelization f̂ (countably many in parallel — a closure operator), compositional product f ∗ g = max{f₀ ∘ g₀ : f₀ ≤_W f, g₀ ≤_W g} (Brattka, Gherardi and Marcone), implication as its adjoint (Brattka and Pauly). Jump f′: the same problem with input names weakened to limits of names (Brattka, Gherardi and Marcone 2012); monotone for ≤_sW, not for ≤_W.

Omniscience benchmarks: LPO: decide whether an infinite sequence contains a 0 — the limited principle of omniscience. LLPO: for a sequence with at most one non-zero entry, name a parity class containing only zeros. C₂ ≡_sW LLPO <_W LPO <_W C_ℕ.

Choice: C_X: given a closed A ⊆ X (by negative information), find a point in A. C_ℕ ≡ limℕ: computability with finitely many mind changes; f ≤_W C_ℕ iff f is so computable. C_2ℕ ≡_sW WKL ≡_sW L̂LPO: f ≤_W C_2ℕ iff f is non-deterministically computable; for single-valued f into metric spaces, f ≤_W C_2ℕ implies f computable. C_ℝ ≡_sW C_ℕ × C_2ℕ. PC_2ℕ ≡_sW WWKL: positive-measure choice, Las Vegas computability. C_ℕℕ: choice on Baire space, the top of the classified region. lim ≡_sW L̂PO ≡_sW J ≡_sW EC: f ≤_W lim iff f is limit computable; f ≤_W lim^[n] iff f is effectively Σ⁰ₙ₊₁-measurable.

Classified theorems: IVT ≡sW CC[0,1] — connected choice on the unit interval (Brattka and Gherardi). Brouwer fixed point: BFT₁ ≡_sW IVT; BFT_n ≡sW CC[0,1]ⁿ ≡_sW C_2ℕ for n ≥ 2 (Brattka, Le Roux, Miller and Pauly). Hahn–Banach ≡_sW WKL ≡_sW C_2ℕ (Gherardi and Marcone 2009). Monotone convergence theorem MCT ≡_W lim; so too differentiation and the Radon–Nikodym derivative. Bolzano–Weierstraß BWT_ℝ ≡_sW C′_2ℕ, the jump of WKL (Brattka, Gherardi and Marcone 2012); Kőnig's lemma KL likewise. Baire category theorem: the forward form BCT₀ is computable, the contrapositive BCT₁ ≡_W C_ℕ (Brattka, Hendtlass and Kreuzer, NDJFL 59(4), 2018). Nash equilibria NASH ≡sW AoUC*[0,1] (Pauly).

Reverse-mathematics counterparts: C₁ ~ RCA₀*; LLPO*≡ C₂* ≡ K_ℕ ~ BΣ⁰₁; C_ℕ ~ IΣ⁰₁; WKL ~ WKL₀; WWKL ~ WWKL₀; lim and its powers lim^[n] ~ ACA₀; UC_ℕℕ and C_ℕℕ ~ ATR₀. Counterparts of Π¹₁-CA₀ not yet systematically developed.

Symbols.

Metatheory. The degrees under ≤_W form a distributive lattice — the lower semilattice found by Brattka and Gherardi, the upper by Pauly (2010) — with no non-trivial countable suprema, so the lattice is not complete and is neither a Brouwer nor a Heyting algebra (Higuchi and Pauly); the strong degrees form a non-distributive lattice under Dzhafarov's box sum. The compositional product exists as a maximum (Brattka, Gherardi and Marcone) and is adjoint to an implication (Brattka and Pauly), giving the lattice a residuation on the composition side though not on ⊓ or ×. The jump generates the hierarchy theorems: C₂⁽ⁿ⁾ <_W LPO⁽ⁿ⁾ <_W C₂⁽ⁿ⁺¹⁾ and C_2ℕ⁽ⁿ⁾ <_W lim⁽ⁿ⁾ <_W C_2ℕ⁽ⁿ⁺¹⁾, and f ≤W lim^[n] characterizes effective Σ⁰ₙ₊₁-measurability, so the lattice refines the effective Borel hierarchy as many-one degrees refine the Kleene hierarchy. The Medvedev lattice embeds, and through it the Turing and enumeration degrees. Against reverse mathematics the comparison is exact in both directions: most classifications refine the Big Five picture — WKL₀'s cluster becomes the C_2ℕ degree, where Hahn–Banach lands uniformly just as it does proof-theoretically — but uniformity and resource-sensitivity split what provability merges. The intermediate value theorem is provable in RCA₀ yet IVT is discontinuous and non-computable, equivalent to CC[0,1]; Brouwer's theorem matches its WKL₀ placement uniformly only from dimension two up, where BFT_n ≡_sW C_2ℕ, while dimension one is IVT itself and sits strictly below; ACA₀, one system, splits into the strictly increasing family lim <_W BWT ≡_sW C′_2ℕ <_W lim′ <_W ⋯ because classical provability does not count applications; and the two formalizations of the Baire category theorem, interchangeable over RCA₀, sit at 1 and at C_ℕ. Kawamura and Cook (STOC 2010) built the polynomial-time analogue.

Applies to. Classifying theorems of analysis — intermediate value, fixed points, Hahn–Banach, convergence theorems, covering theorems — by uniform computational content. Computable analysis: the degrees of discontinuity its continuity theorem calls for. A uniform, resource-sensitive counterpart to reverse mathematics, and a classical counterpart of constructive reverse mathematics, where LPO, LLPO and Markov's principle are the named milestones. Classifying computability-theoretic constructions (Martin-Löf randomness, 1-genericity, diagonal non-computability) as quotients of problems above C₂. Complexity theory in analysis through the Kawamura–Cook framework.

Limitations. The lattice is not complete — countable suprema almost never exist — there is no top element once the axiom of choice is assumed, and a straightforward jump inversion theorem fails. The jump is monotone only for strong reducibility, and ordinary Weihrauch reducibility can reverse under jumps. Uniformity is also a restriction: a theorem non-uniformly trivial can sit high (IVT has computable outputs instance by instance when the function is fixed), so a Weihrauch classification measures the uniform problem, not the theorem's every reading, and placements are sensitive to formalization — BCT₀ against BCT₁ is a choice of contrapositive, invisible to reverse mathematics and two degrees apart here. Below first-order strength the lattice is coarse where constructive reverse mathematics is fine: Markov's principle and BD-ℕ, rejected constructively, are computable problems and lie at 1. The region above ATR₀'s counterparts is largely uncharted, with no systematic Π¹₁-CA₀ analogue. And the framework needs represented spaces and the axiom of choice for Baire space, so its verdicts are relative to the chosen representations, exactly as in Computable Analysis, where the decimal representation already makes multiplication by three non-computable.

© 2026 Lingenic LLC