35 found
Sort by:
  1. Ulrich Kohlenbach & Pavol Safarik (2014). Fluctuations, Effective Learnability and Metastability in Analysis. Annals of Pure and Applied Logic 165 (1):266-304.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  2. Klaus Ambos-Spies, Joan Bagaria, Enrique Casanovas & Ulrich Kohlenbach (2013). Preface. Annals of Pure and Applied Logic 164 (12):1177.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  3. Jeremy Avigad, Ulrich W. Kohlenbach, Henry Towsner, Samson Abramsky, Andreas Blass, Larry Moss, Alf Onshuus Nino, Patrick Speissegger, Juris Steprans & Monica VanDieren (2012). New Orleans Marriott and Sheraton New Orleans Hotels New Orleans, LA January 8–9, 2011. Bulletin of Symbolic Logic 18 (1).
    Direct download  
     
    My bibliography  
     
    Export citation  
  4. Ulrich Kohlenbach (2012). Gödel Functional Interpretation and Weak Compactness. Annals of Pure and Applied Logic 163 (11):1560-1579.
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  5. Alexander P. Kreuzer & Ulrich Kohlenbach (2012). Term Extraction and Ramsey's Theorem for Pairs. Journal of Symbolic Logic 77 (3):853-895.
    In this paper we study with proof-theoretic methods the function(al) s provably recursive relative to Ramsey's theorem for pairs and the cohesive principle (COH). Our main result on COH is that the type 2 functional provably recursive from $RCA_0 + COH + \Pi _1^0 - CP$ are primitive recursive. This also provides a uniform method to extract bounds from proofs that use these principles. As a consequence we obtain a new proof of the fact that $WKL_0 + \Pi _1^0 - (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  6. Ulrich Kohlenbach (2011). A Note on the Monotone Functional Interpretation. Mathematical Logic Quarterly 57 (6):611-614.
    No categories
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  7. Jaime Gaspar & Ulrich Kohlenbach (2010). On Tao's “Finitary” Infinite Pigeonhole Principle. Journal of Symbolic Logic 75 (1):355-371.
    In 2007. Terence Tao wrote on his blog an essay about soft analysis, hard analysis and the finitization of soft analysis statements into hard analysis statements. One of his main examples was a quasi-finitization of the infinite pigeonhole principle IPP, arriving at the "finitary" infinite pigeonhole principle FIPP₁. That turned out to not be the proper formulation and so we proposed an alternative version FIPP₂. Tao himself formulated yet another version FIPP₃ in a revised version of his essay. We give (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  8. Pavol Safarik & Ulrich Kohlenbach (2010). On the Computational Content of the Bolzano-Weierstraß Principle. Mathematical Logic Quarterly 56 (5):508-532.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  9. Yuri L. Ershov, Klaus Keimel, Ulrich Kohlenbach & Andrei Morozov (2009). Preface. Annals of Pure and Applied Logic 159 (3):249-250.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  10. Alexander Kreuzer & Ulrich Kohlenbach (2009). Ramsey's Theorem for Pairs and Provably Recursive Functions. Notre Dame Journal of Formal Logic 50 (4):427-444.
    This paper addresses the strength of Ramsey's theorem for pairs ($RT^2_2$) over a weak base theory from the perspective of 'proof mining'. Let $RT^{2-}_2$ denote Ramsey's theorem for pairs where the coloring is given by an explicit term involving only numeric variables. We add this principle to a weak base theory that includes weak König's Lemma and a substantial amount of $\Sigma^0_1$-induction (enough to prove the totality of all primitive recursive functions but not of all primitive recursive functionals). In the (...)
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  11. Ulrich Kohlenbach (2008). Gödel's Functional Interpretation and its Use in Current Mathematics. Dialectica 62 (2):223–267.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  12. Matthew Foreman, Su Gao, Valentina Harizanov, Ulrich Kohlenbach, Michael Rathjen, Reed Solomon, Carol Wood & Marcia Groszek (2007). New Orleans Marriott and Sheraton New Orleans New Orleans, Louisiana January 7–8, 2007. Bulletin of Symbolic Logic 13 (3).
    Direct download  
     
    My bibliography  
     
    Export citation  
  13. Thomas Streicher & Ulrich Kohlenbach (2007). Shoenfield is Gödel After Krivine. Mathematical Logic Quarterly 53 (2):176-179.
    We show that Shoenfield's functional interpretation of Peano arithmetic can be factorized as a negative translation due to J. L. Krivine followed by Gödel's Dialectica interpretation. (© 2007 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim).
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  14. Philipp Gerhardy & Ulrich Kohlenbach (2006). Strongly Uniform Bounds From Semi-Constructive Proofs. Annals of Pure and Applied Logic 141 (1):89-107.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  15. Philipp Gerhardy & Ulrich Kohlenbach (2005). Extracting Herbrand Disjunctions by Functional Interpretation. Archive for Mathematical Logic 44 (5):633-644.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  16. Gregory Cherlin, Alan Dow, Yuri Gurevich, Leo Harrington, Ulrich Kohlenbach, Phokion Kolaitis, Leonid Levin, Michael Makkai, Ralph McKenzie & Don Pigozzi (2004). University of Illinois at Chicago, Chicago, IL, June 1–4, 2003. Bulletin of Symbolic Logic 10 (1).
    Direct download  
     
    My bibliography  
     
    Export citation  
  17. Ulrich Kohlenbach & Paulo Oliva (2003). Proof Mining in L1-Approximation. Annals of Pure and Applied Logic 121 (1):1-38.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  18. Ulrich Kohlenbach & Paulo Oliva (2003). Proof Mining in< I> L_< Sub> 1-Approximation. Annals of Pure and Applied Logic 121 (1):1-38.
    Direct download  
     
    My bibliography  
     
    Export citation  
  19. Ulrich Kohlenbach (2002). On Uniform Weak König's Lemma. Annals of Pure and Applied Logic 114 (1-3):103-116.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  20. Ulrich Wilhelm Kohlenbach (2002). Review Of: Jäger, G.; Kahle, R.; Studer, T.: Universes in Explicit Mathematics. [REVIEW] Annals of Pure and Applied Logic 109 (3):141-162.
     
    My bibliography  
     
    Export citation  
  21. Ulrich Kohlenbach (2001). A Note on Spector's Quantifier-Free Rule of Extensionality. Archive for Mathematical Logic 40 (2):89-92.
    In this note we show that the so-called weakly extensional arithmetic in all finite types, which is based on a quantifier-free rule of extensionality due to C. Spector and which is of significance in the context of Gödel"s functional interpretation, does not satisfy the deduction theorem for additional axioms. This holds already for Π0 1-axioms. Previously, only the failure of the stronger deduction theorem for deductions from (possibly open) assumptions (with parameters kept fixed) was known.
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  22. Ulrich Kohlenbach (2000). Review: Grigori Mints, Sergei Tupailo, Wilfried Buchholz, Epsilon Substitution Method for Elementary Analysis. [REVIEW] Bulletin of Symbolic Logic 6 (3):356-357.
    Direct download (2 more)  
     
    My bibliography  
     
    Export citation  
  23. Ulrich Kohlenbach (2000). Things That Can and Things That Cannot Be Done in PRA. Annals of Pure and Applied Logic 102 (3):223-245.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  24. Ulrich Kohlenbach (1999). A Note on Goodman's Theorem. Studia Logica 63 (1):1-5.
    Goodman's theorem states that intuitionistic arithmetic in all finite types plus full choice, HA + AC, is conservative over first-order intuitionistic arithmetic HA. We show that this result does not extend to various subsystems of HA, HA with restricted induction.
    Direct download (8 more)  
     
    My bibliography  
     
    Export citation  
  25. Ulrich Kohlenbach (1999). On the No-Counterexample Interpretation. Journal of Symbolic Logic 64 (4):1491-1511.
    In [15], [16] G. Kreisel introduced the no-counterexample interpretation (n.c.i.) of Peano arithmetic. In particular he proved, using a complicated ε-substitution method (due to W. Ackermann), that for every theorem A (A prenex) of first-order Peano arithmetic PA one can find ordinal recursive functionals Φ A of order type 0 which realize the Herbrand normal form A H of A. Subsequently more perspicuous proofs of this fact via functional interpretation (combined with normalization) and cut-elimination were found. These proofs however do (...)
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  26. Ulrich Kohlenbach (1998). Elimination of Skolem Functions for Monotone Formulas in Analysis. Archive for Mathematical Logic 37 (5-6):363-390.
    In this paper a new method, elimination of Skolem functions for monotone formulas, is developed which makes it possible to determine precisely the arithmetical strength of instances of various non-constructive function existence principles. This is achieved by reducing the use of such instances in a given proof to instances of certain arithmetical principles. Our framework are systems ${\cal T}^{\omega} :={\rm G}_n{\rm A}^{\omega} +{\rm AC}$ -qf $+\Delta$ , where (G $_n$ A $^{\omega})_{n \in {\Bbb N}}$ is a hierarchy of (weak) subsystems (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  27. Ulrich Kohlenbach (1998). On the Arithmetical Content of Restricted Forms of Comprehension, Choice and General Uniform Boundedness. Annals of Pure and Applied Logic 95 (1-3):257-285.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  28. Ulrich Kohlenbach (1998). Relative Constructivity. Journal of Symbolic Logic 63 (4):1218-1238.
    Direct download (7 more)  
     
    My bibliography  
     
    Export citation  
  29. Ulrich Kohlenbach (1996). Mathematically Strong Subsystems of Analysis with Low Rate of Growth of Provably Recursive Functionals. Archive for Mathematical Logic 36 (1):31-71.
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  30. Ulrich Kohlenbach (1995). A Note on theΠ 2 0 -Induction Rule. Archive for Mathematical Logic 34 (4):279-283.
    It is well-known (due to C. Parsons) that the extension of primitive recursive arithmeticPRA by first-order predicate logic and the rule ofΠ 2 0 -inductionΠ 2 0 -IR isΠ 2 0 -conservative overPRA. We show that this is no longer true in the presence of function quantifiers and quantifier-free choice for numbersAC 0,0-qf. More precisely we show that ℐ :=PRA 2 +Π 2 0 -IR+AC 0,0-qf proves the totality of the Ackermann function, wherePRA 2 is the extension ofPRA by number (...)
    No categories
    Direct download (5 more)  
     
    My bibliography  
     
    Export citation  
  31. Ulrich Kohlenbach (1995). A Note on the [Mathematical Formula]-Induction Rule. Archive for Mathematical Logic 4.
    No categories
    Direct download  
     
    My bibliography  
     
    Export citation  
  32. Ulrich Kohlenbach (1993). Effective Moduli From Ineffective Uniqueness Proofs. An Unwinding of de La Vallée Poussin's Proof for Chebycheff Approximation. Annals of Pure and Applied Logic 64 (1):27-94.
    Direct download (3 more)  
     
    My bibliography  
     
    Export citation  
  33. Ulrich Kohlenbach (1992). Effective Bounds From Ineffective Proofs in Analysis: An Application of Functional Interpretation and Majorization. Journal of Symbolic Logic 57 (4):1239-1273.
    We show how to extract effective bounds Φ for $\bigwedge u^1 \bigwedge v \leq_\gamma tu \bigvee w^\eta G_0$ -sentences which depend on u only (i.e. $\bigwedge u \bigwedge v \leq_\gamma tu \bigvee w \leq_\eta \Phi uG_0$ ) from arithmetical proofs which use analytical assumptions of the form \begin{equation*}\tag{*}\bigwedge x^\delta\bigvee y \leq_\rho sx \bigwedge z^\tau F_0\end{equation*} (γ, δ, ρ, and τ are arbitrary finite types, η ≤ 2, G0 and F0 are quantifier-free, and s and t are closed terms). If τ (...)
    Direct download (6 more)  
     
    My bibliography  
     
    Export citation  
  34. Ulrich Kohlenbach (1992). Pointwise Hereditary Majorization and Some Applications. Archive for Mathematical Logic 31 (4):227-241.
    A pointwise version of the Howard-Bezem notion of hereditary majorization is introduced which has various advantages, and its relation to the usual notion of majorization is discussed. This pointwise majorization of primitive recursive functionals (in the sense of Gödel'sT as well as Kleene/Feferman's ) is applied to systems of intuitionistic and classical arithmetic (H andH c) in all finite types with full induction as well as to the corresponding systems with restricted inductionĤ↾ andĤ↾c.H and Ĥ↾ are closed under a generalized (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation  
  35. Ulrich Kohlenbach (1992). Remarks on Herbrand Normal Forms and Herbrand Realizations. Archive for Mathematical Logic 31 (5):305-317.
    LetA H be the Herbrand normal form ofA andA H,D a Herbrand realization ofA H. We showThere is an example of an (open) theory ℐ+ with function parameters such that for someA not containing function parameters Similar for first order theories ℐ+ if the index functions used in definingA H are permitted to occur in instances of non-logical axiom schemata of ℐ, i.e. for suitable ℐ,A In fact, in (1) we can take for ℐ+ the fragment (Σ 1 0 -IA)+ (...)
    No categories
    Direct download (4 more)  
     
    My bibliography  
     
    Export citation