43 found
Order:
Disambiguations
Ulrich Kohlenbach [47]Ulrich Wilhelm Kohlenbach [1]Ulrich W. Kohlenbach [1]
  1.  37
    Effective Bounds from ineffective proofs in analysis: An application of functional interpretation and majorization.Ulrich Kohlenbach - 1992 - 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 (9 more)  
     
    Export citation  
     
    Bookmark   29 citations  
  2.  60
    (1 other version)Mathematically strong subsystems of analysis with low rate of growth of provably recursive functionals.Ulrich Kohlenbach - 1996 - Archive for Mathematical Logic 36 (1):31-71.
  3.  29
    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.
    Kohlenbach, U., 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 27–94.We consider uniqueness theorems in classical analysis having the form u ε U, v1, v2 ε Vu = 0 = G→v 1 = v2), where U, V are complete separable metric spaces, Vu is compact in V and G:U x V → is a constructive function.If is proved by arithmetical means from analytical assumptions x (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   23 citations  
  4.  25
    Shoenfield is Gödel after Krivine.Thomas Streicher & Ulrich Kohlenbach - 2007 - 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).
    Direct download  
     
    Export citation  
     
    Bookmark   16 citations  
  5.  37
    Interrelation between weak fragments of double negation shift and related principles.Makoto Fujiwara & Ulrich Kohlenbach - 2018 - Journal of Symbolic Logic 83 (3):991-1012.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  6.  49
    Pointwise hereditary majorization and some applications.Ulrich Kohlenbach - 1992 - 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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   14 citations  
  7. (1 other version)Relative constructivity.Ulrich Kohlenbach - 1998 - Journal of Symbolic Logic 63 (4):1218-1238.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  8.  20
    On the Disjunctive Markov Principle.Ulrich Kohlenbach - 2015 - Studia Logica 103 (6):1313-1317.
    In this note we show that over a strong intuitionistic base theory, the recursive comprehension principle \ -CA does not imply the disjunctive Markov principle MP\.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  9.  44
    On the no-counterexample interpretation.Ulrich Kohlenbach - 1999 - 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 (9 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  10.  36
    (1 other version)Proof mining in L1-approximation.Ulrich Kohlenbach & Paulo Oliva - 2003 - Annals of Pure and Applied Logic 121 (1):1-38.
    In this paper, we present another case study in the general project of proof mining which means the logical analysis of prima facie non-effective proofs with the aim of extracting new computationally relevant data. We use techniques based on monotone functional interpretation developed in Kohlenbach , Oxford University Press, Oxford, 1996, pp. 225–260) to analyze Cheney's simplification 189) of Jackson's original proof 320) of the uniqueness of the best L1-approximation of continuous functions fC[0,1] by polynomials pPn of degree n. Cheney's (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  11.  43
    Elimination of Skolem functions for monotone formulas in analysis.Ulrich Kohlenbach - 1998 - 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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  12.  28
    On the computational content of the Bolzano-Weierstraß Principle.Pavol Safarik & Ulrich Kohlenbach - 2010 - Mathematical Logic Quarterly 56 (5):508-532.
    We will apply the methods developed in the field of ‘proof mining’ to the Bolzano-Weierstraß theorem BW and calibrate the computational contribution of using this theorem in proofs of combinatorial statements. We provide an explicit solution of the Gödel functional interpretation as well as the monotone functional interpretation of BW for the product space Πi ∈ℕ[–ki, ki] . This results in optimal program and bound extraction theorems for proofs based on fixed instances of BW, i.e. for BW applied to fixed (...)
    Direct download  
     
    Export citation  
     
    Bookmark   6 citations  
  13.  22
    On uniform weak König's lemma.Ulrich Kohlenbach - 2002 - Annals of Pure and Applied Logic 114 (1-3):103-116.
    The so-called weak König's lemma WKL asserts the existence of an infinite path b in any infinite binary tree . Based on this principle one can formulate subsystems of higher-order arithmetic which allow to carry out very substantial parts of classical mathematics but are Π 2 0 -conservative over primitive recursive arithmetic PRA . In Kohlenbach 1239–1273) we established such conservation results relative to finite type extensions PRA ω of PRA . In this setting one can consider also a uniform (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  14.  21
    Extracting Herbrand disjunctions by functional interpretation.Philipp Gerhardy & Ulrich Kohlenbach - 2005 - Archive for Mathematical Logic 44 (5):633-644.
    Abstract.Carrying out a suggestion by Kreisel, we adapt Gödel’s functional interpretation to ordinary first-order predicate logic(PL) 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 (3 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  15.  48
    Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - 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)  
     
    Export citation  
     
    Bookmark   5 citations  
  16.  22
    Things that can and things that cannot be done in PRA.Ulrich Kohlenbach - 2000 - Annals of Pure and Applied Logic 102 (3):223-245.
    It is well known by now that large parts of mathematical reasoning can be carried out in systems which are conservative over primitive recursive arithmetic PRA . On the other hand there are principles S of elementary analysis which are known to be equivalent to arithmetical comprehension and therefore go far beyond the strength of PRA . In this paper we determine precisely the arithmetical and computational strength of weaker function parameter-free schematic versions S− of S, thereby exhibiting different levels (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  17.  19
    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  
  18.  50
    Term extraction and Ramsey's theorem for pairs.Alexander P. Kreuzer & Ulrich Kohlenbach - 2012 - 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 (7 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  19.  58
    A note on Spector's quantifier-free rule of extensionality.Ulrich Kohlenbach - 2001 - 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.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  20.  26
    Remarks on Herbrand normal forms and Herbrand realizations.Ulrich Kohlenbach - 1992 - 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)+ (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  21.  54
    On Tao's “finitary” infinite pigeonhole principle.Jaime Gaspar & Ulrich Kohlenbach - 2010 - 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 (7 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  22.  35
    Fluctuations, effective learnability and metastability in analysis.Ulrich Kohlenbach & Pavol Safarik - 2014 - Annals of Pure and Applied Logic 165 (1):266-304.
    This paper discusses what kind of quantitative information one can extract under which circumstances from proofs of convergence statements in analysis. We show that from proofs using only a limited amount of the law-of-excluded-middle, one can extract functionals , where L is a learning procedure for a rate of convergence which succeeds after at most B-many mind changes. This -learnability provides quantitative information strictly in between a full rate of convergence and a rate of metastability in the sense of Tao (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  23.  20
    Intuitionistic Choice and Restricted Classical Logic.Ulrich Kohlenbach - 2001 - Mathematical Logic Quarterly 47 (4):455-460.
    Recently, Coquand and Palmgren considered systems of intuitionistic arithmetic in a finite types together with various forms of the axiom of choice and a numerical omniscience schema which implies classical logic for arithmetical formulas. Feferman subsequently observed that the proof theoretic strength of such systems can be determined by functional interpretation based on a non-constructive μ-operator and his well-known results on the strength of this operator from the 70's. In this note we consider a weaker form LNOS of NOS which (...)
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  24.  40
    (1 other version)On the arithmetical content of restricted forms of comprehension, choice and general uniform boundedness.Ulrich Kohlenbach - 1998 - Annals of Pure and Applied Logic 95 (1-3):257-285.
    In this paper the numerical strength of fragments of arithmetical comprehension, choice and general uniform boundedness is studied systematically. These principles are investigated relative to base systems Tnω in all finite types which are suited to formalize substantial parts of analysis but nevertheless have provably recursive functions of low growth. We reduce the use of instances of these principles in Tnω-proofs of a large class of formulas to the use of instances of certain arithmetical principles thereby determining faithfully the arithmetical (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  25.  33
    Maria Hämeen-Anttila* and Jan von Plato,** eds, Kurt Gödel: The Princeton Lectures on Intuitionism.Ulrich Kohlenbach - 2023 - Philosophia Mathematica 31 (1):112-119.
    This book publishes for the first time notes from two notebooks of Gödel which formed the basis of a course on intuitionism Gödel delivered at Princeton in the.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  26.  53
    A note on Goodman's theorem.Ulrich Kohlenbach - 1999 - 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 (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  27.  45
    (2 other versions)A note on theΠ 2 0 -induction rule.Ulrich Kohlenbach - 1995 - 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 (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  28. Gödel's functional interpretation and its use in current mathematics.Ulrich Kohlenbach - 2008 - Dialectica 62 (2):223–267.
  29.  25
    Preface.Klaus Ambos-Spies, Joan Bagaria, Enrique Casanovas & Ulrich Kohlenbach - 2013 - Annals of Pure and Applied Logic 164 (12):1177.
  30.  28
    New Orleans Marriott and Sheraton New Orleans Hotels New Orleans, LA January 8–9, 2011.Jeremy Avigad, Ulrich W. Kohlenbach, Henry Towsner, Samson Abramsky, Andreas Blass, Larry Moss, Alf Onshuus Nino, Patrick Speissegger, Juris Steprans & Monica VanDieren - 2012 - Bulletin of Symbolic Logic 18 (1).
    Direct download  
     
    Export citation  
     
    Bookmark  
  31. University of Illinois at Chicago, Chicago, IL, June 1–4, 2003.Gregory Cherlin, Alan Dow, Yuri Gurevich, Leo Harrington, Ulrich Kohlenbach, Phokion Kolaitis, Leonid Levin, Michael Makkai, Ralph McKenzie & Don Pigozzi - 2004 - Bulletin of Symbolic Logic 10 (1).
     
    Export citation  
     
    Bookmark  
  32.  12
    Logic Colloquium 2007.Françoise Delon, Ulrich Kohlenbach, Penelope Maddy & Frank Stephan (eds.) - 2010 - New York: Cambridge University Press.
    The 2007 proceedings from the Annual European Meeting of the Association for Symbolic Logic.
    Direct download  
     
    Export citation  
     
    Bookmark  
  33.  25
    Preface.Yuri L. Ershov, Klaus Keimel, Ulrich Kohlenbach & Andrei Morozov - 2009 - Annals of Pure and Applied Logic 159 (3):249-250.
  34.  57
    New Orleans Marriott and Sheraton New Orleans New Orleans, Louisiana January 7–8, 2007.Matthew Foreman, Su Gao, Valentina Harizanov, Ulrich Kohlenbach, Michael Rathjen, Reed Solomon, Carol Wood & Marcia Groszek - 2007 - Bulletin of Symbolic Logic 13 (3).
    Direct download  
     
    Export citation  
     
    Bookmark  
  35.  32
    Classical provability of uniform versions and intuitionistic provability.Makoto Fujiwara & Ulrich Kohlenbach - 2015 - Mathematical Logic Quarterly 61 (3):132-150.
    Along the line of Hirst‐Mummert and Dorais, we analyze the relationship between the classical provability of uniform versions Uni(S) of Π2‐statements S with respect to higher order reverse mathematics and the intuitionistic provability of S. Our main theorem states that (in particular) for every Π2‐statement S of some syntactical form, if its uniform version derives the uniform variant of over a classical system of arithmetic in all finite types with weak extensionality, then S is not provable in strong semi‐intuitionistic systems (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  36.  25
    A note on the monotone functional interpretation.Ulrich Kohlenbach - 2011 - Mathematical Logic Quarterly 57 (6):611-614.
    We prove a result relating the author's monotone functional interpretation to the bounded functional interpretation due to Ferreira and Oliva. More precisely we show that largely a solution for the bounded interpretation also is a solution for the monotone functional interpretation although the latter uses the existence of an underlying precise witness. This makes it possible to focus on the extraction of bounds while using the conceptual benefit of having precise realizers at the same time without having to construct them.
    Direct download  
     
    Export citation  
     
    Bookmark  
  37.  28
    Gödel functional interpretation and weak compactness.Ulrich Kohlenbach - 2012 - Annals of Pure and Applied Logic 163 (11):1560-1579.
    In recent years, proof theoretic transformations that are based on extensions of monotone forms of Gödel’s famous functional interpretation have been used systematically to extract new content from proofs in abstract nonlinear analysis. This content consists both in effective quantitative bounds as well as in qualitative uniformity results. One of the main ineffective tools in abstract functional analysis is the use of sequential forms of weak compactness. As we recently verified, the sequential form of weak compactness for bounded closed and (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  38.  28
    On Weak Markov's Principle.Ulrich Kohlenbach - 2002 - Mathematical Logic Quarterly 48 (S1):59-65.
    We show that the so-called weak Markov's principle which states that every pseudo-positive real number is positive is underivable in [MATHEMATICAL SCRIPT CAPITAL T]ω ≔ E-HAω + AC. Since [MATHEMATICAL SCRIPT CAPITAL T]ω allows one to formalize Bishop's constructive mathematics, this makes it unlikely that WMP can be proved within the framework of Bishop-style mathematics . The underivability even holds if the ine.ective schema of full comprehension for negated formulas is added, which allows one to derive the law of excluded (...)
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  39.  17
    Proof-theoretic uniform boundedness and bounded collection principles and countable Heine–Borel compactness.Ulrich Kohlenbach - 2021 - Archive for Mathematical Logic 60 (7):995-1003.
    In this note we show that proof-theoretic uniform boundedness or bounded collection principles which allow one to formalize certain instances of countable Heine–Borel compactness in proofs using abstract metric structures must be carefully distinguished from an unrestricted use of countable Heine–Borel compactness.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  40.  34
    21st Workshop on Logic, Language, Information and Computation.Ulrich Kohlenbach, Pablo Barceló & Ruy de Queiroz - 2015 - Logic Journal of the IGPL 23 (5):848-859.
  41. Logic, Language, Information and Computation (Lecture Notes in Computer Science 8071).Leonid Libkin, Ulrich Kohlenbach & Ruy de Queiroz (eds.) - 2013 - Springer.
  42.  10
    Grigori Mints, Sergei Tupailo, and Wilfried Buchholz. Epsilon substitution method for elementary analysis. Archive for mathematical logic, vol. 35 , pp. 103–130. [REVIEW]Ulrich Kohlenbach - 2000 - Bulletin of Symbolic Logic 6 (3):356-357.
  43. Review of: Jäger, G.; Kahle, R.; Studer, T.: Universes in explicit mathematics. [REVIEW]Ulrich Wilhelm Kohlenbach - 2002 - Annals of Pure and Applied Logic 109 (3):141-162.