{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T06:00:55Z","timestamp":1770444055695,"version":"3.49.0"},"reference-count":68,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T00:00:00Z","timestamp":1751932800000},"content-version":"unspecified","delay-in-days":188,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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.<\/jats:p>","DOI":"10.1017\/s0960129525000167","type":"journal-article","created":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T03:43:27Z","timestamp":1751946207000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["On logical aspects of extensionality and continuity for set-valued operators with applications to nonlinear analysis"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1243-6787","authenticated-orcid":false,"given":"Nicholas","family":"Pischke","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2025,7,8]]},"reference":[{"key":"S0960129525000167_ref56","doi-asserted-by":"publisher","DOI":"10.1016\/j.jmaa.2023.128078"},{"key":"S0960129525000167_ref49","doi-asserted-by":"publisher","DOI":"10.4171\/zaa\/1724"},{"key":"S0960129525000167_ref39","doi-asserted-by":"publisher","DOI":"10.1142\/9789813237315_0008"},{"key":"S0960129525000167_ref17","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-04-03515-9"},{"key":"S0960129525000167_ref10","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-07-04429-7"},{"key":"S0960129525000167_ref27","doi-asserted-by":"publisher","DOI":"10.1142\/S0219199717500158"},{"key":"S0960129525000167_ref59","doi-asserted-by":"publisher","DOI":"10.1017\/jsl.2019.55"},{"key":"S0960129525000167_ref25","doi-asserted-by":"publisher","DOI":"10.1007\/s11590-021-01738-9"},{"key":"S0960129525000167_ref4","first-page":"1016","volume-title":"Encyclopedia of Optimization","author":"Combettes","year":"2009"},{"key":"S0960129525000167_ref51","unstructured":"Pischke, N. (2024a). A proof-theoretic bound extraction theorem for monotone operators in Banach spaces. https:\/\/nicholaspischke.github.io"},{"key":"S0960129525000167_ref11","doi-asserted-by":"publisher","DOI":"10.1111\/j.1746-8361.1958.tb01464.x"},{"key":"S0960129525000167_ref40","doi-asserted-by":"crossref","first-page":"219","DOI":"10.23952\/jnva.2.2018.2.08","article-title":"Effective strong convergence of the proximal point algorithm in CAT(0) spaces","volume":"2","author":"Leu\u015ftean","year":"2018","journal-title":"Journal of Nonlinear and Variational Analysis"},{"key":"S0960129525000167_ref67","doi-asserted-by":"publisher","DOI":"10.1090\/mbk\/059"},{"key":"S0960129525000167_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-016-9702-z"},{"key":"S0960129525000167_ref46","doi-asserted-by":"publisher","DOI":"10.1080\/01630563.2021.1876726"},{"key":"S0960129525000167_ref52","doi-asserted-by":"publisher","DOI":"10.1080\/02331934.2024.2390114"},{"key":"S0960129525000167_ref20","first-page":"3361","article-title":"Recent progress in proof mining in nonlinear analysis","volume":"10","author":"Kohlenbach","year":"2017","journal-title":"IFCoLog Journal of Logics and Their Applications"},{"key":"S0960129525000167_ref33","first-page":"241","article-title":"On the interpretation of non-finitist proofs\u2013Part I","volume":"16","author":"Kreisel","year":"1951","journal-title":"The Journal of Symbolic Logic"},{"key":"S0960129525000167_ref43","unstructured":"Neri, M. and Pischke, N. (2024). Proof mining and probability theory. https:\/\/arxiv.org\/abs\/2403.00659v2"},{"key":"S0960129525000167_ref65","volume-title":"Nonlinear Functional Analysis","author":"Takahashi","year":"2000"},{"key":"S0960129525000167_ref19","volume-title":"Applied Proof Theory: Proof Interpretations and Their Use in Mathematics","author":"Kohlenbach","year":"2008"},{"key":"S0960129525000167_ref37","doi-asserted-by":"publisher","DOI":"10.1007\/s10898-018-0655-9"},{"key":"S0960129525000167_ref14","doi-asserted-by":"publisher","DOI":"10.2307\/2275367"},{"key":"S0960129525000167_ref68","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0066739"},{"key":"S0960129525000167_ref13","first-page":"454","volume-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Volume 344 of Lecture Notes in Mathematics","author":"Howard","year":"1973"},{"key":"S0960129525000167_ref28","doi-asserted-by":"publisher","DOI":"10.1080\/02331934.2016.1200577"},{"key":"S0960129525000167_ref41","doi-asserted-by":"publisher","DOI":"10.1016\/S0898-1221(01)00138-9"},{"key":"S0960129525000167_ref15","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198538622.003.0010"},{"key":"S0960129525000167_ref22","first-page":"61","volume-title":"Proc. ICM 2018","volume":"2","author":"Kohlenbach","year":"2019"},{"key":"S0960129525000167_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/s10208-018-9377-0"},{"key":"S0960129525000167_ref45","doi-asserted-by":"publisher","DOI":"10.1002\/malq.202200048"},{"key":"S0960129525000167_ref58","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9939-1974-0346608-8"},{"key":"S0960129525000167_ref63","doi-asserted-by":"publisher","DOI":"10.2307\/2267043"},{"key":"S0960129525000167_ref31","first-page":"136","article-title":"Proof mining: a systematic way of analysing proofs in mathematics","volume":"242","author":"Kohlenbach","year":"2003","journal-title":"Proceedings of the Steklov Institute of Mathematics"},{"key":"S0960129525000167_ref55","doi-asserted-by":"publisher","DOI":"10.26083\/tuprints-00026584"},{"key":"S0960129525000167_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/s11856-019-1870-x"},{"key":"S0960129525000167_ref35","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.05.039"},{"key":"S0960129525000167_ref64","first-page":"103","article-title":"Strong convergence theorems for infinite families of nonexpansive mappings in general Banach spaces","volume":"2005","author":"Suzuki","year":"2005","journal-title":"Journal of Fixed Point Theory and Applications"},{"key":"S0960129525000167_ref54","first-page":"7475","article-title":"Proof mining for the dual of a Banach space with extensions for uniformly Fr\u00e9chet differentiable functions","volume":"377","author":"Pischke","year":"2024","journal-title":"Transactions of the American Mathematical Society"},{"key":"S0960129525000167_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2014.04.015"},{"key":"S0960129525000167_ref24","first-page":"11","article-title":"Quantitative results on the proximal point algorithm in uniformly convex Banach spaces","volume":"28","author":"Kohlenbach","year":"2021","journal-title":"Journal of Convex Analysis"},{"key":"S0960129525000167_ref34","doi-asserted-by":"publisher","DOI":"10.2307\/2267457"},{"key":"S0960129525000167_ref8","doi-asserted-by":"publisher","DOI":"10.1080\/01630563.2024.2318597"},{"key":"S0960129525000167_ref9","doi-asserted-by":"publisher","DOI":"10.1215\/00294527-2008-022"},{"key":"S0960129525000167_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/j.jmaa.2014.10.035"},{"key":"S0960129525000167_ref3","doi-asserted-by":"publisher","DOI":"10.1016\/S1570-579X(01)80010-0"},{"key":"S0960129525000167_ref42","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1969.30.475"},{"key":"S0960129525000167_ref47","doi-asserted-by":"publisher","DOI":"10.4171\/dm\/924"},{"key":"S0960129525000167_ref61","unstructured":"Sipo\u015f, A. (2023). The computational content of super strongly nonexpansive mappings and uniformly monotone operators. Israel Journal of Mathematics. arXiv:2303.02768."},{"key":"S0960129525000167_ref23","first-page":"2125","article-title":"Quantitative analysis of a Halpern-type proximal point algorithm for accretive operators in Banach spaces","volume":"21","author":"Kohlenbach","year":"2020","journal-title":"Journal of Nonlinear and Convex Analysis"},{"key":"S0960129525000167_ref1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48311-5"},{"key":"S0960129525000167_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2015.12.007"},{"key":"S0960129525000167_ref18","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2006.05.038"},{"key":"S0960129525000167_ref60","doi-asserted-by":"publisher","DOI":"10.1007\/s11590-021-01812-2"},{"key":"S0960129525000167_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s001530050055"},{"key":"S0960129525000167_ref48","doi-asserted-by":"publisher","DOI":"10.1007\/s00029-025-01027-8"},{"key":"S0960129525000167_ref50","first-page":"295","article-title":"Quantitative results on algorithms for zeros of differences of monotone operators in Hilbert space","volume":"30","author":"Pischke","year":"2023b","journal-title":"Journal of Convex Analysis"},{"key":"S0960129525000167_ref38","doi-asserted-by":"publisher","DOI":"10.1007\/s10589-021-00263-w"},{"key":"S0960129525000167_ref2","doi-asserted-by":"publisher","DOI":"10.1016\/j.na.2006.10.015"},{"key":"S0960129525000167_ref53","doi-asserted-by":"publisher","DOI":"10.1142\/S0219061323500083"},{"key":"S0960129525000167_ref7","doi-asserted-by":"publisher","DOI":"10.1016\/j.aim.2019.106728"},{"key":"S0960129525000167_ref44","first-page":"1","article-title":"Computational problems in metric fixed point theory and their Weihrauch degrees","volume":"11","author":"Neumann","year":"2015","journal-title":"Logical Methods in Computer Science"},{"key":"S0960129525000167_ref66","doi-asserted-by":"publisher","DOI":"10.1017\/S0143385708000011"},{"key":"S0960129525000167_ref32","doi-asserted-by":"publisher","DOI":"10.1016\/j.camwa.2020.04.002"},{"key":"S0960129525000167_ref6","first-page":"729","article-title":"Quantitative results on the multi-parameters proximal point algorithm","volume":"28","author":"Dinis","year":"2021","journal-title":"Journal of Convex Analysis"},{"key":"S0960129525000167_ref57","doi-asserted-by":"publisher","DOI":"10.1007\/s11228-024-00736-0"},{"key":"S0960129525000167_ref62","doi-asserted-by":"publisher","DOI":"10.1016\/j.na.2008.02.034"},{"key":"S0960129525000167_ref5","doi-asserted-by":"publisher","DOI":"10.4171\/pm\/2054"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129525000167","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,8]],"date-time":"2025-07-08T03:43:32Z","timestamp":1751946212000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129525000167\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":68,"alternative-id":["S0960129525000167"],"URL":"https:\/\/doi.org\/10.1017\/s0960129525000167","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e15"}}