On logical aspects of extensionality and continuity for set-valued operators with applications to nonlinear analysis

We discuss the logical principle of extensionality for set-valued operators and its relation to mathematical notions of continuity for these operators in the context of systems of finite types as used in proof mining. Concretely, we initially exhibit an issue that arises with treating full extensionality in the context of the prevalent intensional approach to set-valued operators in such systems. Motivated by these issues, we discuss a range of useful fragments of this full extensionality statement where these issues are avoided and discuss their interrelations. Further, we study the continuity principles associated with these fragments of extensionality and show how they can be introduced in the logical systems via a collection of axioms that do not contribute to the growth of extractable bounds from proofs. In particular, we place an emphasis on a variant of extensionality and continuity formulated using the Hausdorff-metric and, in the course of our discussion, we in particular employ a tame treatment of suprema over bounded sets developed by the author in previous work to provide the first proof-theoretically tame treatment of the Hausdorff metric in systems geared for proof mining. To illustrate the applicability of these treatments for the extraction of quantitative information from proofs, we provide an application of proof mining to the Mann iteration of set-valued mappings which are nonexpansive w.r.t. the Hausdorff metric and extract highly uniform and effective quantitative information on the convergence of that method.