Switch to: References

Add citations

You must login to add citations.
  1. Inductive Full Satisfaction Classes.Henryk Kotlarski & Zygmunt Ratajczyk - 1990 - Annals of Pure and Applied Logic 47 (1):199--223.
  • Peano Arithmetic as Axiomatization of the Time Frame in Logics of Programs and in Dynamic Logics.Balázs Biró & Ildikó Sain - 1993 - Annals of Pure and Applied Logic 63 (3):201-225.
    Biró, B. and I. Sain, Peano arithmetic as axiomatization of the time frame in logics of programs and in dynamic logics, Annals of Pure and Applied Logic 63 201-225. We show that one can prove the partial correctness of more programs using Peano's axioms for the time frames of three-sorted time models than using only Presburger's axioms, that is it is useful to allow multiplication of time points at program verification and in dynamic and temporal logics. We organized the paper (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • Slow Consistency.Sy-David Friedman, Michael Rathjen & Andreas Weiermann - 2013 - Annals of Pure and Applied Logic 164 (3):382-393.
    The fact that “natural” theories, i.e. theories which have something like an “idea” to them, are almost always linearly ordered with regard to logical strength has been called one of the great mysteries of the foundation of mathematics. However, one easily establishes the existence of theories with incomparable logical strengths using self-reference . As a result, PA+Con is not the least theory whose strength is greater than that of PA. But still we can ask: is there a sense in which (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   8 citations  
  • Reflection Principles in Fragments of Peano Arithmetic.Hiroakira Ono - 1987 - Mathematical Logic Quarterly 33 (4):317-333.
  • Reflection Principles in Fragments of Peano Arithmetic.Hiroakira Ono - 1987 - Zeitschrift fur mathematische Logik und Grundlagen der Mathematik 33 (4):317-333.
  • Short Proofs for Slow Consistency.Anton Freund & Fedor Pakhomov - 2020 - Notre Dame Journal of Formal Logic 61 (1):31-49.
    Let Con↾x denote the finite consistency statement “there are no proofs of contradiction in T with ≤x symbols.” For a large class of natural theories T, Pudlák has shown that the lengths of the shortest proofs of Con↾n in the theory T itself are bounded by a polynomial in n. At the same time he conjectures that T does not have polynomial proofs of the finite consistency statements Con)↾n. In contrast, we show that Peano arithmetic has polynomial proofs of Con)↾n, (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • A Model-Theoretic Approach to Ordinal Analysis.Jeremy Avigad & Richard Sommer - 1997 - Bulletin of Symbolic Logic 3 (1):17-52.
    We describe a model-theoretic approach to ordinal analysis via the finite combinatorial notion of an α-large set of natural numbers. In contrast to syntactic approaches that use cut elimination, this approach involves constructing finite sets of numbers with combinatorial properties that, in nonstandard instances, give rise to models of the theory being analyzed. This method is applied to obtain ordinal analyses of a number of interesting subsystems of first- and second-order arithmetic.
    Direct download (11 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  • Transfinite Induction Within Peano Arithmetic.Richard Sommer - 1995 - Annals of Pure and Applied Logic 76 (3):231-289.
    The relative strengths of first-order theories axiomatized by transfinite induction, for ordinals less-than 0, and formulas restricted in quantifier complexity, is determined. This is done, in part, by describing the provably recursive functions of such theories. Upper bounds for the provably recursive functions are obtained using model-theoretic techniques. A variety of additional results that come as an application of such techniques are mentioned.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   16 citations  
  • Subsystems of True Arithmetic and Hierarchies of Functions.Z. Ratajczyk - 1993 - Annals of Pure and Applied Logic 64 (2):95-152.
    Ratajczyk, Z., Subsystems of true arithmetic and hierarchies of functions, Annals of Pure and Applied Logic 64 95–152. The combinatorial method coming from the study of combinatorial sentences independent of PA is developed. Basing on this method we present the detailed analysis of provably recursive functions associated with higher levels of transfinite induction, I, and analyze combinatorial sentences independent of I. Our treatment of combinatorial sentences differs from the one given by McAloon [18] and gives more natural sentences. The same (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  • A Sharpened Version of McAloon's Theorem on Initial Segments of Models of IΔ0.Paola D'Aquino - 1993 - Annals of Pure and Applied Logic 61 (1-2):49-62.
    A generalization is given of McAloon's result on initial segments ofmodels of GlΔ0, the fragment of Peano Arithmetic where the induction scheme is restricted to formulas with bounded quantifiers.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  • On the Number of Steps in Proofs.Jan Kraj\mIček - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.
    In this paper we prove some results about the complexity of proofs. We consider proofs in Hilbert-style formal systems such as in [17]. Thus a proof is a sequence offormulas satisfying certain conditions. We can view the formulas as being strings of symbols; hence the whole proof is a string too. We consider the following measures of complexity of proofs: length , depth and number of steps For a particular formal system and a given formula A we consider the shortest (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  • On Me Number of Steps in Proofs.Jan Krajíèek - 1989 - Annals of Pure and Applied Logic 41 (2):153-178.
    In this paper we prove some results about the complexity of proofs. We consider proofs in Hilbert-style formal systems such as in [17]. Thus a proof is a sequence offormulas satisfying certain conditions. We can view the formulas as being strings of symbols; hence the whole proof is a string too. We consider the following measures of complexity of proofs: length , depth and number of steps For a particular formal system and a given formula A we consider the shortest (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   11 citations  
  • On Gödel Incompleteness and Finite Combinatorics.Akihiro Kanamori & Kenneth McAloon - 1987 - Annals of Pure and Applied Logic 33 (1):23-41.