A Proof-Theoretic Bound Extraction Theorem for CAT $$(\kappa )$$ ( κ ) -Spaces

&
Studia Logica 105 (3):611-624 (2017)
  Copy   BIBTEX

Abstract

Starting in 2005, general logical metatheorems have been developed that guarantee the extractability of uniform effective bounds from large classes of proofs of theorems that involve abstract metric structures X. In this paper we adapt this to the class of CAT\)-spaces X for \ and establish a new metatheorem that explains specific bound extractions that recently have been achieved in this context as instances of a general logical phenomenon.

Categories

Keywords

Reprint years

DOI

10.1007/s11225-016-9702-z

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,571

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Strongly uniform bounds from semi-constructive proofs.Philipp Gerhardy & Ulrich Kohlenbach - 2006 - Annals of Pure and Applied Logic 141 (1):89-107.
Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
Logical Aspects of Rates of Convergence in Metric Spaces.Eyvind Martol Briseid - 2009 - Journal of Symbolic Logic 74 (4):1401 - 1428.
On the role of the baire category theorem and dependent choice in the foundations of logic.Robert Goldblatt - 1985 - Journal of Symbolic Logic 50 (2):412-422.
Effective moduli from ineffective uniqueness proofs. An unwinding of de La Vallée Poussin's proof for Chebycheff approximation.Ulrich Kohlenbach - 1993 - Annals of Pure and Applied Logic 64 (1):27-94.
Domain representability of metric spaces.Jens Blanck - 1997 - Annals of Pure and Applied Logic 83 (3):225-247.
On the computational content of the Bolzano-Weierstraß Principle.Pavol Safarik & Ulrich Kohlenbach - 2010 - Mathematical Logic Quarterly 56 (5):508-532.
Ah, Chu!Solomon Feferman - unknown
Gödel functional interpretation and weak compactness.Ulrich Kohlenbach - 2012 - Annals of Pure and Applied Logic 163 (11):1560-1579.
Term extraction and Ramsey's theorem for pairs.Alexander P. Kreuzer & Ulrich Kohlenbach - 2012 - Journal of Symbolic Logic 77 (3):853-895.
Expressive power in first order topology.Paul Bankston - 1984 - Journal of Symbolic Logic 49 (2):478-487.
An Omitting Types Theorem for positive bounded formulas in normed spaces.Carlos Ortiz - 2001 - Annals of Pure and Applied Logic 108 (1-3):279-294.
Proof-theoretic investigations on Kruskal's theorem.Michael Rathjen & Andreas Weiermann - 1993 - Annals of Pure and Applied Logic 60 (1):49-88.
Ramsey classes of topological and metric spaces.Jaroslav Nešetřil - 2006 - Annals of Pure and Applied Logic 143 (1-3):147-154.
On me number of steps in proofs.Jan Krajíèek - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.

Analytics

Added to PP
2017-01-07

Downloads
16 (#900,320)

6 months
3 (#967,057)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Alexandru Nicolae
University of Bucharest

Citations of this work

Add more citations

References found in this work

Add more references