26 found
Order:
  1.  25
    Polynomial Local Search in the Polynomial Hierarchy and Witnessing in Fragments of Bounded Arithmetic.Arnold Beckmann & Samuel R. Buss - 2009 - Journal of Mathematical Logic 9 (1):103-138.
  2.  12
    Safe Recursive Set Functions.Arnold Beckmann, Samuel R. Buss & Sy-David Friedman - 2015 - Journal of Symbolic Logic 80 (3):730-762.
  3.  9
    Linear Kripke Frames and Gödel Logics.Arnold Beckmann & Norbert Preining - 2007 - Journal of Symbolic Logic 72 (1):26 - 44.
    We investigate the relation between intermediate predicate logics based on countable linear Kripke frames with constant domains and Gödel logics. We show that for any such Kripke frame there is a Gödel logic which coincides with the logic defined by this Kripke frame on constant domains and vice versa. This allows us to transfer several recent results on Gödel logics to logics based on countable linear Kripke frames with constant domains: We obtain a complete characterisation of axiomatisability of logics based (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  4.  20
    Dynamic Ordinal Analysis.Arnold Beckmann - 2003 - Archive for Mathematical Logic 42 (4):303-334.
    Dynamic ordinal analysis is ordinal analysis for weak arithmetics like fragments of bounded arithmetic. In this paper we will define dynamic ordinals – they will be sets of number theoretic functions measuring the amount of sΠ b 1(X) order induction available in a theory. We will compare order induction to successor induction over weak theories. We will compute dynamic ordinals of the bounded arithmetic theories sΣ b n (X)−L m IND for m=n and m=n+1, n≥0. Different dynamic ordinals lead to (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   5 citations  
  5.  19
    A Term Rewriting Characterization of the Polytime Functions and Related Complexity Classes.Arnold Beckmann & Andreas Weiermann - 1996 - Archive for Mathematical Logic 36 (1):11-30.
  6.  6
    Separation Results for the Size of Constant-Depth Propositional Proofs.Arnold Beckmann & Samuel R. Buss - 2005 - Annals of Pure and Applied Logic 136 (1-2):30-55.
    This paper proves exponential separations between depth d-LK and depth -LK for every utilizing the order induction principle. As a consequence, we obtain an exponential separation between depth d-LK and depth -LK for . We investigate the relationship between the sequence-size, tree-size and height of depth d-LK-derivations for , and describe transformations between them. We define a general method to lift principles requiring exponential tree-size -LK-refutations for to principles requiring exponential sequence-size d-LK-refutations, which will be described for the Ramsey principle (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  33
    Exact Bounds for Lengths of Reductions in Typed Λ-Calculus.Arnold Beckmann - 2001 - Journal of Symbolic Logic 66 (3):1277-1285.
    We determine the exact bounds for the length of an arbitrary reduction sequence of a term in the typed λ-calculus with β-, ξ- and η-conversion. There will be two essentially different classifications, one depending on the height and the degree of the term and the other depending on the length and the degree of the term.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  8.  18
    Characterizing the Elementary Recursive Functions by a Fragment of Gödel's T.Arnold Beckmann & Andreas Weiermann - 2000 - Archive for Mathematical Logic 39 (7):475-491.
    Let T be Gödel's system of primitive recursive functionals of finite type in a combinatory logic formulation. Let $T^{\star}$ be the subsystem of T in which the iterator and recursor constants are permitted only when immediately applied to type 0 arguments. By a Howard-Schütte-style argument the $T^{\star}$ -derivation lengths are classified in terms of an iterated exponential function. As a consequence a constructive strong normalization proof for $T^{\star}$ is obtained. Another consequence is that every $T^{\star}$ -representable number-theoretic function is elementary (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  9.  14
    Applications of Cut-Free Infinitary Derivations to Generalized Recursion Theory.Arnold Beckmann & Wolfram Pohlers - 1998 - Annals of Pure and Applied Logic 94 (1-3):7-19.
    We prove that the boundedness theorem of generalized recursion theory can be derived from the ω-completeness theorem for number theory. This yields a proof of the boundedness theorem which does not refer to the analytical hierarchy theorem.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  10.  20
    Analyzing Godel's T Via Expanded Head Reduction Trees.Arnold Beckmann & Andreas Weiermann - 2000 - Mathematical Logic Quarterly 46 (4):517-536.
    Inspired from Buchholz' ordinal analysis of ID1 and Beckmann's analysis of the simple typed λ-calculus we classify the derivation lengths for Gödel's system T in the λ-formulation.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  11.  22
    Proving Consistency of Equational Theories in Bounded Arithmetic.Arnold Beckmann - 2002 - Journal of Symbolic Logic 67 (1):279-296.
    We consider equational theories for functions defined via recursion involving equations between closed terms with natural rules based on recursive definitions of the function symbols. We show that consistency of such equational theories can be proved in the weak fragment of arithmetic S 1 2 . In particular this solves an open problem formulated by TAKEUTI (c.f. [5, p.5 problem 9.]).
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  12.  4
    Ordinal Notations and Well-Orderings in Bounded Arithmetic.Arnold Beckmann, Chris Pollett & Samuel R. Buss - 2003 - Annals of Pure and Applied Logic 120 (1-3):197-223.
    This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  13.  2
    Preservation Theorems and Restricted Consistency Statements in Bounded Arithmetic.Arnold Beckmann - 2004 - Annals of Pure and Applied Logic 126 (1-3):255-280.
    We define and study a new restricted consistency notion RCon ∗ for bounded arithmetic theories T 2 j . It is the strongest ∀ Π 1 b -statement over S 2 1 provable in T 2 j , similar to Con in Krajíček and Pudlák, 29) or RCon in Krajı́ček and Takeuti 107). The advantage of our notion over the others is that RCon ∗ can directly be used to construct models of T 2 j . We apply this by (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  14.  20
    A Non-Well-Founded Primitive Recursive Tree Provably Well-Founded for Co-R.E. Sets.Arnold Beckmann - 2002 - Archive for Mathematical Logic 41 (3):251-257.
    We construct by diagonalization a non-well-founded primitive recursive tree, which is well-founded for co-r.e. sets, provable in Σ1 0. It follows that the supremum of order-types of primitive recursive well-orderings, whose well-foundedness on co-r.e. sets is provable in Σ1 0, equals the limit of all recursive ordinals ω1 ck . RID=""ID="" Mathematics Subject Classification (2000): 03B30, 03F15 RID=""ID="" Supported by the Deutschen Akademie der Naturforscher Leopoldina grant #BMBF-LPD 9801-7 with funds from the Bundesministerium für Bildung, Wissenschaft, Forschung und Technologie. RID=""ID="" (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  15.  17
    Computability in Europe 2008.Arnold Beckmann, Costas Dimitracopoulos & Benedikt Löwe - 2010 - Archive for Mathematical Logic 49 (2):119-121.
  16.  14
    An Unexpected Separation Result in Linearly Bounded Arithmetic.Arnold Beckmann & Jan Johannsen - 2005 - Mathematical Logic Quarterly 51 (2):191-200.
    The theories Si1 and Ti1 are the analogues of Buss' relativized bounded arithmetic theories in the language where every term is bounded by a polynomial, and thus all definable functions grow linearly in length. For every i, a Σbi+1-formula TOPi, which expresses a form of the total ordering principle, is exhibited that is provable in Si+11 , but unprovable in Ti1. This is in contrast with the classical situation, where Si+12 is conservative over Ti2 w. r. t. Σbi+1-sentences. The independence (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark  
  17.  14
    Preface.Arnold Beckmann, Jeremy Avigad & Georg Moser - 2005 - Annals of Pure and Applied Logic 136 (1-2):1-2.
  18.  13
    On the Computational Complexity of Cut-Reduction.Klaus Aehlig & Arnold Beckmann - 2010 - Annals of Pure and Applied Logic 161 (6):711-736.
    Using appropriate notation systems for proofs, cut-reduction can often be rendered feasible on these notations. Explicit bounds can be given. Developing a suitable notation system for Bounded Arithmetic, and applying these bounds, all the known results on definable functions of certain such theories can be reobtained in a uniform way.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  19.  9
    Erratum to “Ordinal Notations and Well-Orderings in Bounded Arithmetic” [Annals of Pure and Applied Logic 120 197–223]. [REVIEW]Arnold Beckmann, Samuel R. Buss & Chris Pollett - 2003 - Annals of Pure and Applied Logic 123 (1-3):291.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  20.  6
    2002 European Summer Meeting of the Association for Symbolic Logic Logic Colloquium'02.Lev D. Beklemishev, Stephen Cook, Olivier Lessmann, Simon Thomas, Jeremy Avigad, Arnold Beckmann, Tim Carlson, Robert L. Constable & Kosta Došen - 2003 - Bulletin of Symbolic Logic 9 (1):71.
  21.  6
    16th Workshop on Logic, Language, Information and Computation (WoLLIC 2009).Hans Tompits, Ken Satoh, Arnold Beckmann, Carlos Caleiro, Thomas Eiter, Sylvain Salvati, Taisuke Sato & Frank Wolter - 2010 - Bulletin of Symbolic Logic 16 (1):805-815.
  22.  3
    Cobham Recursive Set Functions.Arnold Beckmann, Sam Buss, Sy-David Friedman, Moritz Müller & Neil Thapen - 2016 - Annals of Pure and Applied Logic 167 (3):335-369.
  23.  4
    Takeuti Gaisi. Incompleteness Theorems and Versus. Logic Colloquium'96, Proceedings of the Colloquium Held in San Sebastián, Spain, July 9–15, 1996, Edited by Larrazabal JM, Lascar D., and Mints G., Lecture Notes in Logic, No. 12, Springer, Berlin, Heidelberg, New York, Etc., 1998, Pp. 247–261. Takeuti Gaisi. Gödel Sentences of Bounded Arithmetic. The Journal of Symbolic Logic, Vol. 65 (2000), Pp. 1338–1346. [REVIEW]Arnold Beckmann - 2002 - Bulletin of Symbolic Logic 8 (3):433-435.
  24.  3
    Computability in Europe 2009.Klaus Ambos-Spies, Arnold Beckmann, Samuel R. Buss & Benedikt Löwe - 2012 - Annals of Pure and Applied Logic 163 (5):483-484.
  25.  1
    Incompleteness Theorems and S I 2 Versus S I+1 2Godel Sentences of Bounded Arithmetic.Arnold Beckmann & Gaisi Takeuti - 2002 - Bulletin of Symbolic Logic 8 (3):433.
  26.  1
    Review: , Incompleteness Theorems and $S^I2$ Versus $S^{I+1}2$; Gaisi Takeuti, Gödel Sentences of Bounded Arithmetic. [REVIEW]Arnold Beckmann - 2002 - Bulletin of Symbolic Logic 8 (3):433-435.