On the Computational Content of Moduli of Regularity and their Logical Strength

TL;DR

This paper explores the computational aspects of moduli of regularity, demonstrating their ability to compute zeros of functions in various settings and analyzing their logical strength within reverse mathematics and Weihrauch degrees.

Contribution

It establishes the computational power of moduli of regularity for finding zeros and minimal norm solutions, and analyzes their logical strength and limitations.

Findings

Moduli of regularity enable zero computation for continuous functions on compact spaces.

They can compute the minimal norm zero in convex subsets of Banach spaces.

No proof-theoretically tame principle replaces compactness with boundedness while preserving bounds.

Abstract

We continue the investigation into the computational status of the existence of moduli of regularity (and their use for rates of convergence) in the sense of Kohlenbach, Lopez and Nicolae (2019), carried out w.r.t. classical reverse mathematics and Weihrauch degrees in a previous paper and determine the amount of LEM involved. We also show that the existence of a modulus of regularity always yields an algorithm for the computation of a zero in the case of continuous real-valued functions F on a compact metric space K (in F equipped with a modulus of uniform continuity and K given in standard representation) whenever such a zero exists. If K is a compact subset of a uniformly convex Banach space X and the zero set of F is convex one can compute even the zero of minimal norm. A modulus of regularity can also be used to compute the left-most infinite path of an infinite 0/1-tree. We also show that there is no proof-theoretically tame nonstandard uniformity principle which would make it possible to replace in the regularity assumption compactness by metric boundedness and still guarantee classically correct bounds.