A proof-theoretic bound extraction theorem for CAT(κ)-spaces

Description

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 κ > 0 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.

Abstract

German Science Foundation

Abstract

Dirección General de Enseñanza Superior

Additional details