4 found
  1.  13
    The Role of Quantifier Alternations in Cut Elimination.Philipp Gerhardy - 2005 - Notre Dame Journal of Formal Logic 46 (2):165-171.
    Extending previous results from work on the complexity of cut elimination for the sequent calculus LK, we discuss the role of quantifier alternations and develop a measure to describe the complexity of cut elimination in terms of quantifier alternations in cut formulas and contractions on such formulas.
    Direct download (5 more)  
    Export citation  
    Bookmark   8 citations  
  2.  7
    Strongly Uniform Bounds From Semi-Constructive Proofs.Philipp Gerhardy & Ulrich Kohlenbach - 2006 - Annals of Pure and Applied Logic 141 (1):89-107.
    In [U. Kohlenbach, Some logical metatheorems with applications in functional analysis, Trans. Amer. Math. Soc. 357 89–128], the second author obtained metatheorems for the extraction of effective bounds from classical, prima facie non-constructive proofs in functional analysis. These metatheorems for the first time cover general classes of structures like arbitrary metric, hyperbolic, CAT and normed linear spaces and guarantee the independence of the bounds from parameters ranging over metrically bounded spaces. Recently ]), the authors obtained generalizations of these metatheorems which (...)
    Direct download (4 more)  
    Export citation  
    Bookmark   5 citations  
  3.  10
    Extracting Herbrand Disjunctions by Functional Interpretation.Philipp Gerhardy & Ulrich Kohlenbach - 2005 - Archive for Mathematical Logic 44 (5):633-644.
    .Carrying out a suggestion by Kreisel, we adapt Gödel’s functional interpretation to ordinary first-order predicate logic and thus devise an algorithm to extract Herbrand terms from PL-proofs. The extraction is carried out in an extension of PL to higher types. The algorithm consists of two main steps: first we extract a functional realizer, next we compute the β-normal-form of the realizer from which the Herbrand terms can be read off. Even though the extraction is carried out in the extended language, (...)
    Direct download (4 more)  
    Export citation  
    Bookmark   4 citations  
  4.  33
    Proof Mining in Topological Dynamics.Philipp Gerhardy - 2008 - Notre Dame Journal of Formal Logic 49 (4):431-446.
    A famous theorem by van der Waerden states the following: Given any finite coloring of the integers, one color contains arbitrarily long arithmetic progressions. Equivalently, for every q,k, there is an N = N(q,k) such that for every q-coloring of an interval of length N one color contains a progression of length k. An obvious question is what is the growth rate of N = N(q,k). Some proofs, like van der Waerden's combinatorial argument, answer this question directly, while the topological (...)
    Direct download (3 more)  
    Export citation  
    Bookmark   1 citation