Switch to: References

Add citations

You must login to add citations.
  1. Paris-Harrington Principles, Reflection Principles and Transfinite Induction Up to Epsilon 0.Reijiro Kurata - 1986 - Annals of Pure and Applied Logic 31 (2):237.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Kripke Models and the Intuitionistic Theory of Species.D. H. J. de Jongh - 1976 - Annals of Pure and Applied Logic 9 (1):157.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Disquotation and Infinite Conjunctions.Lavinia Picollo & Thomas Schindler - 2017 - Erkenntnis (5):1-30.
    One of the main logical functions of the truth predicate is to enable us to express so-called ‘infinite conjunctions’. Several authors claim that the truth predicate can serve this function only if it is fully disquotational, which leads to triviality in classical logic. As a consequence, many have concluded that classical logic should be rejected. The purpose of this paper is threefold. First, we consider two accounts available in the literature of what it means to express infinite conjunctions with a (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Axiomatization of Provable N-Provability.Evgeny Kolmakov & Lev Beklemishev - 2019 - Journal of Symbolic Logic 84 (2):849-869.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Arithmetical Reflection and the Provability of Soundness.Walter Dean - 2015 - Philosophia Mathematica 23 (1):31-64.
    Proof-theoretic reflection principles are schemas which attempt to express the soundness of arithmetical theories within their own language, e.g., ${\mathtt{{Prov}_{\mathsf {PA}} \rightarrow \varphi }}$ can be understood to assert that any statement provable in Peano arithmetic is true. It has been repeatedly suggested that justification for such principles follows directly from acceptance of an arithmetical theory $\mathsf {T}$ or indirectly in virtue of their derivability in certain truth-theoretic extensions thereof. This paper challenges this consensus by exploring relationships between reflection principles (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • On Interpreting Chaitin's Incompleteness Theorem.Panu Raatikainen - 1998 - Journal of Philosophical Logic 27 (6):569-586.
    The aim of this paper is to comprehensively question the validity of the standard way of interpreting Chaitin's famous incompleteness theorem, which says that for every formalized theory of arithmetic there is a finite constant c such that the theory in question cannot prove any particular number to have Kolmogorov complexity larger than c. The received interpretation of theorem claims that the limiting constant is determined by the complexity of the theory itself, which is assumed to be good measure of (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Algorithmic Information Theory and Undecidability.Panu Raatikainen - 2000 - Synthese 123 (2):217-225.
    Chaitin’s incompleteness result related to random reals and the halting probability has been advertised as the ultimate and the strongest possible version of the incompleteness and undecidability theorems. It is argued that such claims are exaggerations.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • My Route to Arithmetization.Solomon Feferman - 1997 - Theoria 63 (3):168-181.
    I had the pleasure of renewing my acquaintance with Per Lindström at the meeting of the Seventh Scandinavian Logic Symposium, held in Uppsala in August 1996. There at lunch one day, Per said he had long been curious about the development of some of the ideas in my paper [1960] on the arithmetization of metamathematics. In particular, I had used the construction of a non-standard definition !* of the set of axioms of P (Peano Arithmetic) to show that P + (...)
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Positive Provability Logic for Uniform Reflection Principles.Lev Beklemishev - 2014 - Annals of Pure and Applied Logic 165 (1):82-105.
    We deal with the fragment of modal logic consisting of implications of formulas built up from the variables and the constant ‘true’ by conjunction and diamonds only. The weaker language allows one to interpret the diamonds as the uniform reflection schemata in arithmetic, possibly of unrestricted logical complexity. We formulate an arithmetically complete calculus with modalities labeled by natural numbers and ω, where ω corresponds to the full uniform reflection schema, whereas n<ω corresponds to its restriction to arithmetical Πn+1-formulas. This (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Local Reflection, Definable Elements and 1-Provability.Evgeny Kolmakov - forthcoming - Archive for Mathematical Logic:1-18.
    In this note we study several topics related to the schema of local reflection \\) and its partial and relativized variants. Firstly, we introduce the principle of uniform reflection with \-definable parameters, establish its relationship with relativized local reflection principles and corresponding versions of induction with definable parameters. Using this schema we give a new model-theoretic proof of the \-conservativity of uniform \-reflection over relativized local \-reflection. We also study the proof-theoretic strength of Feferman’s theorem, i.e., the assertion of 1-provability (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • On Axiom Schemes for T-Provably $${\Delta_{1}}$$ Δ 1 Formulas.A. Cordón-Franco, A. Fernández-Margarit & F. F. Lara-Martín - 2014 - Archive for Mathematical Logic 53 (3-4):327-349.
    This paper investigates the status of the fragments of Peano Arithmetic obtained by restricting induction, collection and least number axiom schemes to formulas which are Δ1\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\Delta_1}$$\end{document} provably in an arithmetic theory T. In particular, we determine the provably total computable functions of this kind of theories. As an application, we obtain a reduction of the problem whether IΔ0+¬exp\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${I\Delta_0 + \neg \mathit{exp}}$$\end{document} implies BΣ1\documentclass[12pt]{minimal} (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • A Note on Iterated Consistency and Infinite Proofs.Anton Freund - 2019 - Archive for Mathematical Logic 58 (3-4):339-346.
    Schmerl and Beklemishev’s work on iterated reflection achieves two aims: it introduces the important notion of \-ordinal, characterizing the \-theorems of a theory in terms of transfinite iterations of consistency; and it provides an innovative calculus to compute the \-ordinals for a range of theories. The present note demonstrates that these achievements are independent: we read off \-ordinals from a Schütte-style ordinal analysis via infinite proofs, in a direct and transparent way.
    Download  
     
    Export citation  
     
    Bookmark  
  • Provability: The Emergence of a Mathematical Modality.George Boolos & Giovanni Sambin - 1991 - Studia Logica 50 (1):1 - 23.
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • On the Complexity of Arithmetical Interpretations of Modal Formulae.Lev D. Beklemishev - 1993 - Archive for Mathematical Logic 32 (3):229-238.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • 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)+ (...)
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Too Naturalist and Not Naturalist Enough: Reply to Horsten.Luca Incurvati - 2008 - Erkenntnis 69 (2):261 - 274.
    Leon Horsten has recently claimed that the class of mathematical truths coincides with the class of theorems of ZFC. I argue that the naturalistic character of Horsten’s proposal undermines his contention that this claim constitutes an analogue of a thesis that Daniel Isaacson has advanced for PA. I argue, moreover, that Horsten’s defence of his claim against an obvious objection makes use of a distinction which is not available to him given his naturalistic approach. I suggest a way out of (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • The Implicit Commitment of Arithmetical Theories and Its Semantic Core.Carlo Nicolai & Mario Piazza - 2019 - Erkenntnis 84 (4):913-937.
    According to the implicit commitment thesis, once accepting a mathematical formal system S, one is implicitly committed to additional resources not immediately available in S. Traditionally, this thesis has been understood as entailing that, in accepting S, we are bound to accept reflection principles for S and therefore claims in the language of S that are not derivable in S itself. It has recently become clear, however, that such reading of the implicit commitment thesis cannot be compatible with well-established positions (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Slow Reflection.Anton Freund - 2017 - Annals of Pure and Applied Logic 168 (12):2103-2128.
    Download  
     
    Export citation  
     
    Bookmark  
  • Gödel's Second Incompleteness Theorem for Q.A. Bezboruah & J. C. Shepherdson - 1976 - Journal of Symbolic Logic 41 (2):503-512.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Remarks on Weak Notions of Saturation in Models of Peano Arithmetic.Matt Kaufmann & James H. Schmerl - 1987 - Journal of Symbolic Logic 52 (1):129-148.
    Download  
     
    Export citation  
     
    Bookmark   6 citations  
  • Algorithmic Information Theory.Michiel van Lambalgen - 1989 - Journal of Symbolic Logic 54 (4):1389-1400.
    We present a critical discussion of the claim (most forcefully propounded by Chaitin) that algorithmic information theory sheds new light on Godel's first incompleteness theorem.
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • 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 of Peano arithmetic. In particular he proved, using a complicated $\varepsilon$-substitution method, that for every theorem A of first-order Peano arithmetic PA one can find ordinal recursive functionals $\Phi_A$ of order type < $\varepsilon_0$ which realize the Herbrand normal form A$^H$ of A. Subsequently more perspicuous proofs of this fact via functional interpretation and cut-elimination were found. These proofs however do not carry out the no-counterexample interpretation as a local proof interpretation (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • A Note on Applicability of the Incompleteness Theorem to Human Mind.Pavel Pudlák - 1999 - Annals of Pure and Applied Logic 96 (1-3):335-342.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Finitary Inductively Presented Logics.Solomon Feferman - manuscript
    A notion of finitary inductively presented (f.i.p.) logic is proposed here, which includes all syntactically described logics (formal systems)met in practice. A f.i.p. theory FS0 is set up which is universal for all f.i.p. logics; though formulated as a theory of functions and classes of expressions, FS0 is a conservative extension of PRA. The aims of this work are (i)conceptual, (ii)pedagogical and (iii)practical. The system FS0 serves under (i)and (ii)as a theoretical framework for the formalization of metamathematics. The general approach (...)
    Download  
     
    Export citation  
     
    Bookmark   8 citations  
  • Iterated Local Reflection Versus Iterated Consistency.Lev Beklemishev - 1995 - Annals of Pure and Applied Logic 75 (1-2):25-48.
    For “natural enough” systems of ordinal notation we show that α times iterated local reflection schema over a sufficiently strong arithmetic T proves the same Π 1 0 -sentences as ω α times iterated consistency. A corollary is that the two hierarchies catch up modulo relative interpretability exactly at ε-numbers. We also derive the following more general “mixed” formulas estimating the consistency strength of iterated local reflection: for all ordinals α ⩾ 1 and all β, β ≡ Π 1 0 (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • Iterated Reflection Principles and the Ω-Rule.Ulf R. Schmerl - 1982 - Journal of Symbolic Logic 47 (4):721-733.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • The Relation of a to Prov ⌜a ⌝ in the Lindenbaum Sentence Algebra.C. F. Kent - 1973 - Journal of Symbolic Logic 38 (2):295-298.
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • A Survey of Proof Theory.G. Kreisel - 1968 - Journal of Symbolic Logic 33 (3):321-388.
    Download  
     
    Export citation  
     
    Bookmark   39 citations  
  • Predicativity Through Transfinite Reflection.Andrés Cordón-Franco, David Fernández-Duque, Joost J. Joosten & Francisco Félix Lara-martín - 2017 - Journal of Symbolic Logic 82 (3):787-808.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • 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 (...)
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Set Existence Property for Intuitionistic Theories with Dependent Choice.Harvey M. Friedman & Andrej Ščedrov - 1983 - Annals of Pure and Applied Logic 25 (2):129-140.
    Download  
     
    Export citation  
     
    Bookmark   5 citations  
  • Induction Rules, Reflection Principles, and Provably Recursive Functions.Lev D. Beklemishev - 1997 - Annals of Pure and Applied Logic 85 (3):193-242.
    A well-known result states that, over basic Kalmar elementary arithmetic EA, the induction schema for ∑n formulas is equivalent to the uniform reflection principle for ∑n + 1 formulas . We show that fragments of arithmetic axiomatized by various forms of induction rules admit a precise axiomatization in terms of reflection principles as well. Thus, the closure of EA under the induction rule for ∑n formulas is equivalent to ω times iterated ∑n reflection principle. Moreover, for k < ω, k (...)
    Download  
     
    Export citation  
     
    Bookmark   22 citations  
  • Some Results on Cut-Elimination, Provable Well-Orderings, Induction and Reflection.Toshiyasu Arai - 1998 - Annals of Pure and Applied Logic 95 (1-3):93-184.
    We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • The Paradox of the Knower Revisited.Walter Dean & Hidenori Kurokawa - 2014 - Annals of Pure and Applied Logic 165 (1):199-224.
    The Paradox of the Knower was originally presented by Kaplan and Montague [26] as a puzzle about the everyday notion of knowledge in the face of self-reference. The paradox shows that any theory extending Robinson arithmetic with a predicate K satisfying the factivity axiom K → A as well as a few other epistemically plausible principles is inconsistent. After surveying the background of the paradox, we will focus on a recent debate about the role of epistemic closure principles in the (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Henkin Sentences and Local Reflection Principles for Rosser Provability.Taishi Kurahashi - 2016 - Annals of Pure and Applied Logic 167 (2):73-94.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Generalizations of Gödel’s Incompleteness Theorems for ∑N-Definable Theories of Arithmetic.Makoto Kikuchi & Taishi Kurahashi - 2017 - Review of Symbolic Logic 10 (4):603-616.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • On the Optimality of Conservation Results for Local Reflection in Arithmetic.A. Cordón-Franco, A. Fernández-Margarit & F. F. Lara-Martín - 2013 - Journal of Symbolic Logic 78 (4):1025-1035.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Levy and Set Theory.Akihiro Kanamori - 2006 - Annals of Pure and Applied Logic 140 (1):233-252.
    Azriel Levy did fundamental work in set theory when it was transmuting into a modern, sophisticated field of mathematics, a formative period of over a decade straddling Cohen’s 1963 founding of forcing. The terms “Levy collapse”, “Levy hierarchy”, and “Levy absoluteness” will live on in set theory, and his technique of relative constructibility and connections established between forcing and definability will continue to be basic to the subject. What follows is a detailed account and analysis of Levy’s work and contributions (...)
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • Unifying the Model Theory of First-Order and Second-Order Arithmetic viaWKL0⁎.Ali Enayat & Tin Lok Wong - 2017 - Annals of Pure and Applied Logic 168 (6):1247-1283.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Bimodal Logics for Extensions of Arithmetical Theories.Lev D. Beklemishev - 1996 - Journal of Symbolic Logic 61 (1):91-124.
    We characterize the bimodal provability logics for certain natural (classes of) pairs of recursively enumerable theories, mostly related to fragments of arithmetic. For example, we shall give axiomatizations, decision procedures, and introduce natural Kripke semantics for the provability logics of (IΔ 0 + EXP, PRA); (PRA, IΣ 1 ); (IΣ m , IΣ n ) for $1 \leq m etc. For the case of finitely axiomatized extensions of theories these results are extended to modal logics with propositional constants.
    Download  
     
    Export citation  
     
    Bookmark   4 citations  
  • Bar Induction and Π11-CA.Harvey Friedman - 1969 - Journal of Symbolic Logic 34 (3):353 - 362.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Herbrand-Analysen Zweier Beweise Des Satzes Von Roth: Polynomiale Anzahlschranken.H. Luckhardt - 1989 - Journal of Symbolic Logic 54 (1):234-263.
    A previously unexplored method, combining logical and mathematical elements, is shown to yield substantial numerical improvements in the area of Diophantine approximations. Kreisel illustrated the method abstractly by noting that effective bounds on the number of elements are ensured if Herbrand terms from ineffective proofs of Σ 2 -finiteness theorems satisfy certain simple growth conditions. Here several efficient growth conditions for the same purpose are presented that are actually satisfied in practice, in particular, by the proofs of Roth's theorem due (...)
    Download  
     
    Export citation  
     
    Bookmark   10 citations  
  • The Ω-Consistency of Number Theory Via Herbrand's Theorem.W. D. Goldfarb & T. M. Scanlon - 1974 - Journal of Symbolic Logic 39 (4):678-692.
    Download  
     
    Export citation  
     
    Bookmark  
  • Notes on Local Reflection Principles.Lev Beklemishev - 1997 - Theoria 63 (3):139-146.
    Download  
     
    Export citation  
     
    Bookmark   4 citations