Switch to: Citations

Add references

You must login to add references.
  1. Über eine bisher noch nicht benützte erweiterung Des finiten standpunktes.Von Kurt Gödel - 1958 - Dialectica 12 (3‐4):280-287.
    ZusammenfassungP. Bernays hat darauf hingewiesen, dass man, um die Widerspruchs freiheit der klassischen Zahlentheorie zu beweisen, den Hilbertschen flniter Standpunkt dadurch erweitern muss, dass man neben den auf Symbole sich beziehenden kombinatorischen Begriffen gewisse abstrakte Begriffe zulässt, Die abstrakten Begriffe, die bisher für diesen Zweck verwendet wurden, sinc die der konstruktiven Ordinalzahltheorie und die der intuitionistischer. Logik. Es wird gezeigt, dass man statt deesen den Begriff einer berechenbaren Funktion endlichen einfachen Typs über den natürlichen Zahler benutzen kann, wobei keine anderen (...)
    Download  
     
    Export citation  
     
    Bookmark   162 citations  
  • (1 other version)Notation systems for infinitary derivations.Wilfried Buchholz - 1991 - Archive for Mathematical Logic 30 (5-6):277-296.
    Download  
     
    Export citation  
     
    Bookmark   30 citations  
  • (1 other version)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.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Continuous normalization for the lambda-calculus and Gödel’s T.Klaus Aehlig & Felix Joachimski - 2005 - Annals of Pure and Applied Logic 133 (1-3):39-71.
    Building on previous work by Mints, Buchholz and Schwichtenberg, a simplified version of continuous normalization for the untyped λ-calculus and Gödel’s is presented and analysed in the coalgebraic framework of non-wellfounded terms with so-called repetition constructors.The primitive recursive normalization function is uniformly continuous w.r.t. the natural metric on non-wellfounded terms. Furthermore, the number of necessary repetition constructors is locally related to the number of reduction steps needed to reach the normal form and its size.It is also shown how continuous normal (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Structure and definability in general bounded arithmetic theories.Chris Pollett - 1999 - Annals of Pure and Applied Logic 100 (1-3):189-245.
    The bounded arithmetic theories R2i, S2i, and T2i are closely connected with complexity theory. This paper is motivated by the questions: what are the Σi+1b-definable multifunctions of R2i? and when is one theory conservative over another? To answer these questions we consider theories , and where induction is restricted to prenex formulas. We also define which has induction up to the 0 or 1-ary L2-terms in the set τ. We show and and for . We show that the -multifunctions of (...)
    Download  
     
    Export citation  
     
    Bookmark   17 citations