PaperlayerView exact revision on arXiv

Source-linked AI summary

Effective Choice and Boundedness Principles in Computable Analysis

Vasco Brattka, Guido Gherardi

arXiv:0905.4685v4math.LO

TL;DR

The paper asks how the computational content of mathematical theorems can be compared. It represents theorems by realizers and uses Weihrauch reducibility to relate them, establishing reductions among choice and boundedness principles and noting that closed choice is less well-behaved than compact choice.

  • Problem

    The paper asks whether a realizer of one theorem can be computably or continuously transformed into a realizer of another, to compare their computational content.

    Source: §1.1 · p. 2

  • Method

    The paper represents theorems as operations mapping input data to possible outputs and compares them using computable or continuous transformations of realizers.

    Source: §1.1 · p. 2

  • Results

    The paper establishes reductions including CN ≤W BF and LLPO ≤sW BI−, and states that its given reductions are strict except where equivalence is stated.

    Source: §3. Choice and boundedness principles · pp. 14, 17

  • Takeaways & Limitations

    The Baire Category Theorem is used as a separation tool to show it does not prove the Intermediate Value Theorem, whose degree classification also yields a noncomputability result for sequences of roots.

    Source: §4. Separation techniques · p. 22, §6. Interval Choice and the… · p. 30

    Closed choice is much less well-behaved than compact choice; some co-c.e. closed sets have no hyperarithmetical points.

    Source: §8. Metatheorems and Applications · p. 34

Abstract

from arXiv · show

In this paper we study a new approach to classify mathematical theorems according to their computational content. Basically, we are asking the question which theorems can be continuously or computably transferred into each other? For this purpose theorems are considered via their realizers which are operations with certain input and output data. The technical tool to express continuous or computable relations between such operations is Weihrauch reducibility and the partially ordered degree structure induced by it. We have identified certain choice principles which are cornerstones among Weihrauch degrees and it turns out that certain core theorems in analysis can be classified naturally in this structure. In particular, we study theorems such as the Intermediate Value Theorem, the Baire Category Theorem, the Banach Inverse Mapping Theorem and others. We also explore how existing classifications of the Hahn-Banach Theorem and Weak K"onig's Lemma fit into this picture. We compare the results of our classification with existing classifications in constructive and reverse mathematics and we claim that in a certain sense our classification is finer and sheds some new light on the computational content of the respective theorems. We develop a number of separation techniques based on a new parallelization principle, on certain invariance properties of Weihrauch reducibility, on the Low Basis Theorem of Jockusch and Soare and based on the Baire Category Theorem. Finally, we present a number of metatheorems that allow to derive upper bounds for the classification of the Weihrauch degree of many theorems and we discuss the Brouwer Fixed Point Theorem as an example.

§1. Introduction.

The paper uses Weihrauch reducibility to classify the computational content of theorem realizers, developing choice and boundedness principles as tools and applying the framework to analysis while comparing it with other approaches. It also relates omniscience principles and compact choice to Weihrauch degrees and characterizes weak computability and its consequences for single-valued operations.

1.1. Realizability of theorems and Weihrauch reducibility.

  • Theorems are represented by multi-valued realizers, and Weihrauch reducibility compares their computational content; the paper emphasizes non-parallelized degrees for finer classification while using parallelization as a closure operator.The Intermediate Value Theorem is represented by an operation taking a continuous function with opposite-sign endpoint values to a zero.Source: §1.1 · pp. 2–3

1.2. Effective choice and boundedness principles.

  • Choice principles form a hierarchy of discontinuous operations, with boundedness formulations useful for analysis; the paper relates these principles to omniscience and identifies parallelized LPO and LLPO as classification cornerstones.The paper describes parallelized LPO as complete for limit-computable operations and parallelized LLPO as complete for weakly computable operations.Source: §1.2 · pp. 3–4
  • The paper applies separation techniques to distinguish choice and omniscience principles, finding that all choice principles are separated except co-finite and discrete choice, which are equivalent.Techniques include parallelization, mind-change, computable and low invariance, and Baire-category arguments.Source: §1.2 · pp. 4–5

1.3. Theorems in functional analysis.

  • The paper classifies analysis and functional-analysis theorems by Weihrauch degree, showing that BCT₀ has a computable realizer whereas BCT is discontinuous.The classification is presented as a way to answer questions about uniform and non-uniform computability and effective complexity.Source: §1.3 · pp. 5–7
  • Topological-form metatheorems yield Weihrauch upper bounds, including reduction to compact choice for a stated class of closed relations and upper bounds for the Brouwer fixed-point and Peano existence theorems.The stated class has co-c.e. closed A ⊆ X × Y and co-c.e. compact Y.Source: §1.3 · p. 7

1.4. Related approaches.

  • The authors present their approach as a refinement of Borel-complexity classification and claim it makes finer distinctions than other approaches, including constructive analysis and reverse mathematics.They also situate it alongside computable-mathematics classifications by Borel complexity [5, 19, 10, 20].Source: §1.4 · pp. 7–8
  • LLPO is below LPO, and their parallelizations retain that ordering; parallelized LPO is Σ0_2-measurable, or limit computable [5].Source: §1.4 · p. 10
  • Weak K˝onig’s Lemma is Weihrauch-equivalent to parallelized LLPO, and the class of operations reducible to parallelized LLPO is closed under composition.Source: §1.4 · pp. 10–11
  • Compact choice CK(X) is strongly Weihrauch reducible to parallelized LLPO, and is equivalent to it when X computably embeds Cantor space.Source: §1.4 · p. 11
  • Weakly computable operations are exactly those with upper semi-computable compact-valued selectors; consequently, single-valued operations into computable metric spaces are computable.The selector characterization yields the single-valued conclusion.Source: §1.4 · p. 11

§3. Choice and boundedness principles.

The section relates choice and boundedness principles through Weihrauch reducibility, showing how their computational degrees connect to omniscience principles. It establishes equivalences and ordered chains among these principles, with the non-equivalent reductions shown to be strict.

§3. Choice and boundedness principles.

  • Choice seeks members of negatively represented closed sets, while boundedness variants often make the missing information explicit as bounds for the desired output.These principles are classically valid, but finding a guaranteed bound algorithmically has computational content.Source: §3. Choice and boundedness principles · pp. 11–12
  • Co-finite choice CF is strongly equivalent to BF, whereas discrete choice CN is equivalent to BF only under ordinary Weihrauch reducibility, using direct access to the input.The reduction from CN to BF depends essentially on that direct access.Source: §3. Choice and boundedness principles · p. 13
  • Interval choice CI and boundedness BI, and proper interval choice CI− and BI−, are strongly equivalent; BI+ requires two separately presented bounds because its underlying space is noncompact.For interval choice, negative information may instead be supplied as intervals exhausting the complement.Source: §3. Choice and boundedness principles · p. 14
  • To reduce BI− to BF, the construction records stages when a guessed interval center is rejected, obtains a bound on those stages, then replays the guesses through that bound.The center at the final bounded stage need not itself be the surviving choice; replaying the computation ensures the selected center is never later dismissed.Source: §3. Choice and boundedness principles · pp. 15–16
  • LPO reduces to BF, while LLPO reduces to proper interval choice BI− by encoding sequence information in bounds and extracting a choice from the resulting interval.For LLPO, the constructed interval depends on whether a nonzero entry occurs at an even or odd position.Source: §3. Choice and boundedness principles · pp. 16–17
  • The principal chains place LPO ≤W CN ≤W BI+ ≤W CA ≤W C ≡W d LPO and LLPO ≤W CI− ≤W CI ≤W CK ≤W CA; non-equivalent reductions are strict.The section also establishes CI− ≤W CN and CI ≤W BI+.Source: §3. Choice and boundedness principles · p. 17
  • The parallelized countable choice principles form two strict degree classes: parallelized LLPO, proper interval choice, and compact choice lie below parallelized LPO, discrete choice, and closed choice.The classes are separated by a strict Weihrauch reduction.Source: §3. Choice and boundedness principles · p. 18

§4. Separation techniques.

The section develops downward-preserved properties of realizers and uses them to separate Weihrauch degrees. These techniques establish strict choice hierarchies and show that discrete choice and interval choice are incomparable.

Parallelization principle

  • If LPO ≤W f and g ≤W LLPO, then f is not Weihrauch reducible to g.This parallelization principle also shows that co-finite, discrete, and closed choice are not reducible to compact choice.Source: §4. Separation techniques · p. 18

Invariance principles

  • Mind-change, computable-invariance, and low-invariance properties pass from a Weihrauch upper bound to the reduced operation.The section treats these as instances of a general invariance principle for properties of realizers.Source: §4. Separation techniques · pp. 18–19

Mind-change principle

  • LPO and LLPO are strictly below BF and BI−, respectively, because the latter have no realizers computable with at most one mind change.LPO and LLPO do have realizers computable with one mind change.Source: §4. Separation techniques · p. 20

Computable invariance principle

  • Computable invariance gives CK ≰W CI and CA ≰W CN: intervals have computable members on computable inputs, while some non-empty co-c.e. compact sets have none.The cited example is a non-empty co-c.e. compact set containing no computable points.Source: §4. Separation techniques · pp. 20–21

Low invariance principle

  • The Real Low Basis Theorem supplies a low-name point in every non-empty co-c.e. subset of R, yielding CA <W C.Together with low invariance, this separates closed choice from countable choice.Source: §4. Separation techniques · p. 21

Baire Category principle

  • The Baire Category Principle and parallelization establish that discrete choice and interval choice are incomparable.The section first proves CI ≰W CN, then obtains the reverse non-reduction using the parallelization principle.Source: §4. Separation techniques · pp. 22–23

Choice hierarchies

  • The resulting strict hierarchies include LLPO <W CI− <W CI <W CK ≡W \LLPO <W CA and LPO <W CN <W BI+ <W CA <W C ≡W dLPO.The authors state that the displayed arrows are correct and no additional arrows can be added except by transitivity.Source: §4. Separation techniques · p. 23

§5. Discrete Choice and the Baire Category Theorem.

The section classifies the Baire Category Theorem and several functional-analysis theorems by Weihrauch degree. Discrete choice captures these results in their stated settings, while the inverse mapping theorem also exhibits a finite-dimensional exception.

Baire Category Theorem

  • For every non-empty complete computable metric space X, BCTX ≡W CN; the paper excludes the computable BCT0 version and studies the contrapositive BCT instead.The fixed-space formulation is equivalent to discrete choice without making the space part of the input.Source: §5. Discrete Choice and the Baire… · p. 24
  • BCTX asks for an index n such that a closed-set cover member An has non-empty interior, and the paper reduces this task in both directions to discrete choice.The proof encodes candidate balls and uses discrete choice to select one that witnesses the required interior.Source: §5. Discrete Choice and the Baire… · p. 24

Banach Inverse Mapping Theorem

  • For computable Banach spaces X and Y, IMTX,Y ≤W CN ≡W IMTℓ2,ℓ2, while finite-dimensional spaces make the inverse operation computable.An upper bound on ||T^-1|| is the extra information needed to compute the inverse; the worst-case degree is already attained on ℓ2.Source: §5. Discrete Choice and the Baire… · pp. 25–26

Open Mapping Theorem

Closed Graph Theorem

  • The Closed Graph Theorem satisfies CGTX,Y ≤W CN ≡W CGTℓ2,ℓ2 and is computable for finite-dimensional X and Y.Positive information on the graph gives lower bounds on the operator norm; discrete choice supplies an upper bound.Source: §5. Discrete Choice and the Baire… · p. 27

Uniform Boundedness Theorem

Consequences of the classifications

  • The theorems classified as equivalent to CN are discontinuous and non-computable, admit non-uniform computable solutions, and have Δ0 2-complete sequential counterexamples.These are degree-theoretic properties that follow from the classification.Source: §5. Discrete Choice and the Baire… · p. 28

§6. Interval Choice and the Intermediate Value Theorem.

The Intermediate Value Theorem has the same strong Weihrauch degree as Interval Choice. This classification yields consequences for computability and noncomputability of zero-finding, alongside characterizations of its reductions and zero sets.

§6. Interval Choice and the Intermediate Value Theorem.

  • The classification entails that IVT is discontinuous and non-computable, yet has computable solutions for computable inputs and is computable when the zero is unique.IVT is also computable when restricted to functions whose zero set is nowhere dense, a fact requiring analysis beyond the degree classification.Source: §6. Interval Choice and the… · pp. 28–29
  • IVT is strongly Weihrauch-equivalent to Interval Choice: IVT ≡sW CI.The section identifies this equivalence as the classification of the theorem's degree.Source: §6. Interval Choice and the… · p. 29
  • To reduce IVT to bounded interval choice, the proof searches for nested rational intervals with opposite endpoint signs, whose limiting interval lies in the function's zero set.An interval-choice realizer can then select a zero from that limiting interval.Source: §6. Interval Choice and the… · p. 29
  • For the reverse reduction, rational bounds on an interval are encoded by effectively convergent polygons whose limiting function has zero set [y, z].An IVT realizer selects a point between the supplied lower and upper bounds.Source: §6. Interval Choice and the… · p. 29
  • Every sequence of zeros for a suitable computable sequence of sign-changing functions is non-computable, a consequence of the classification rather than a direct proof of nearly two pages.The stated sequence consists of continuous functions on [0, 1].Source: §6. Interval Choice and the… · pp. 29–30
  • A nonempty A⊆(0,1) is the zero set of a computable sign-changing function exactly when it is co-c.e. closed and contains a computable interior point.The section also gives the equivalent form A=B∪{x}, where B is co-c.e. closed and x is a computable point.Source: §6. Interval Choice and the… · p. 30

§7. Compact Choice and the Hahn-Banach Theorem.

The Hahn-Banach Theorem is Weihrauch-equivalent to compact choice. The section relates this degree to discontinuity, computability under uniqueness conditions, and the range of non-uniform solution types.

§7. Compact Choice and the Hahn-Banach Theorem.

  • The Hahn-Banach Theorem is Weihrauch-equivalent to compact choice: HBT ≡W CK.The formalization includes the underlying space as input data.Source: §7. Compact Choice and the Hahn-Banach… · p. 31
  • Like other theorems equivalent to CK, HBT is discontinuous and non-computable, but uniformly computable when classical conditions uniquely determine its solution.Uniform convexity of the dual space, as in Hilbert spaces, is one such condition.Source: §7. Compact Choice and the Hahn-Banach… · p. 31
  • The theorem has non-uniform solutions of any basis type and limit-computable counterexamples, while non-uniform computability fails in general, even in finite dimensions.The paper's earlier summary of HBT states these latter properties directly.Source: §7. Compact Choice and the Hahn-Banach… · p. 31

§8. Metatheorems and Applications.

The section develops metatheorems that bound the Weihrauch complexity of theorem realizers from the logical form and effective properties of their solution sets. Applications include approximation, fixed-point, and locally compact settings, with computability improving under uniqueness in the compact case.

§8. Metatheorems and Applications.

  • The metatheorems target Π2-theorems and provide upper bounds from structural conditions; the open metatheorem makes solution selection computable for c.e. open predicates.Open choice itself is computable, and the Weierstraß Approximation Theorem is an example: its realizer is Weihrauch-equivalent to identity.Source: §8. Metatheorems and Applications · pp. 31–32
  • For c.e. open approximation predicates, rational polynomials approximating a continuous function to precision 2^-k can be found effectively, and WAT ≡W id.The passage gives the predicate ||f−pn|| < 2^-k as c.e. open.Source: §8. Metatheorems and Applications · p. 32
  • When Y is co-c.e. compact and A⊆X×Y is co-c.e. closed, the compact metatheorem makes the solution operation weakly computable, R ≤W CK.The operation maps each input x to the y values paired with x in A.Source: §8. Metatheorems and Applications · p. 33
  • The compact metatheorem gives BFT ≤W WKL; using the Low Basis Theorem and Low Invariance Principle, every computable self-map of [0,1]^n has a low fixed point.The fixed point has a low name in NN.Source: §8. Metatheorems and Applications · p. 33
  • Under the compact metatheorem's conditions, uniqueness makes the solution operation computable, covering unique solutions for Brouwer, intermediate-value, Hahn-Banach, and Peano theorems.The general result applies when Y is co-c.e. compact and A is co-c.e. closed.Source: §8. Metatheorems and Applications · p. 34
  • Closed choice depends sensitively on the space, but for effectively locally compact X it is reducible to C: CA(X) ≤W C.Some co-c.e. closed subsets of NN have no hyperarithmetical points.Source: §8. Metatheorems and Applications · p. 34
  • If Y is effectively locally compact and A⊆X×Y is co-c.e. closed, the solution operation satisfies R ≤W CA(Y) and is limit computable.This is the locally compact metatheorem's bound under its stated conditions.Source: §8. Metatheorems and Applications · p. 34
  • A function with co-c.e. closed graph into an effectively locally compact space is limit computable; the unique locally compact case also maps computable inputs to computable outputs and is computable on compact input sets.The graph result includes inverses of computable bijections as an application.Source: §8. Metatheorems and Applications · p. 35

§9. Conclusions.

The conclusions compare the paper’s Weihrauch-based classification with constructive and reverse mathematics, identifying both differences and rough correspondences. The authors regard their classification as finer in some respects, while noting that its exact relation to the other approaches needs further study.

§9. Conclusions.

  • The authors propose a computational classification using topology and computability theory, and claim it yields finer classifications in some respects.They do not provide an exhaustive comparison with existing constructive and reverse-mathematics results and call for further study of the relationship.Source: §9. Conclusions · p. 35, §9.2 · p. 37

9.1. Constructive mathematics.

  • Constructive analysis places Weak König’s Lemma [24], the Intermediate Value Theorem [15], Hahn–Banach [24], and a form of Heine–Borel [24] at LLPO, but this approach makes Heine–Borel fully computable.The paper attributes the difference to systematically searching for finite subcovers, which constructive analysis cannot do without Markov’s principle.Source: §9.1 · pp. 35–36
  • In constructive analysis, LPO equivalence extends more broadly than in this framework: it includes Bolzano–Weierstraß, which is not below parallelized LPO here.The approaches also differ because this framework equates LPO with WLPO, while constructive analysis allows parallel and sequential LLPO applications without distinguishing LLPO from its parallelization.Source: §9.1 · p. 36

9.2. Reverse mathematics.

  • RCA0 roughly corresponds to non-uniform computability, while WKL0 corresponds to weakly computable operations and ACA0 to effectively Borel measurable maps.The authors also note that composition is free in reverse mathematics, making Borel hierarchy levels difficult to distinguish, whereas parallelization does not seem to be free.Source: §9.2 · pp. 36–37
  • Reverse mathematics proves the Baire Category Theorem, Intermediate Value Theorem, and Uniform Boundedness Theorem in RCA0; its classical logic converts the BCT0 proof into BCT.The authors describe RCA0 as roughly corresponding to their non-uniform computability results.Source: §9.2 · p. 36
  • The uniform reverse-mathematics analogue of LPO appears equivalent to uniform Weak König’s Lemma, whereas the two principles are incomparable in this approach.The authors state that the exact relationship between their approach and constructive and proof-theoretic analyses requires further study.Source: §9.2 · p. 37
Loading 0905.4685v4…