Switch to: References

Add citations

You must login to add citations.
  1. Reducing omega-model reflection to iterated syntactic reflection.Fedor Pakhomov & James Walsh - 2021 - Journal of Mathematical Logic 23 (2).
    Journal of Mathematical Logic, Volume 23, Issue 02, August 2023. In mathematical logic there are two seemingly distinct kinds of principles called “reflection principles.” Semantic reflection principles assert that if a formula holds in the whole universe, then it holds in a set-sized model. Syntactic reflection principles assert that every provable sentence from some complexity class is true. In this paper, we study connections between these two kinds of reflection principles in the setting of second-order arithmetic. We prove that, for (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • PROOF THEORY. Gödel and the metamathematical tradition.Jeremy Avigad - 2010 - In Kurt Gödel, Solomon Feferman, Charles Parsons & Stephen G. Simpson (eds.), Kurt Gödel: essays for his centennial. Ithaca, NY: Association for Symbolic Logic.
    At the turn of the nineteenth century, mathematics exhibited a style of argumentation that was more explicitly computational than is common today. Over the course of the century, the introduction of abstract algebraic methods helped unify developments in analysis, number theory, geometry, and the theory of equations; and work by mathematicians like Dedekind, Cantor, and Hilbert towards the end of the century introduced set-theoretic language and infinitary methods that served to downplay or suppress computational content. This shift in emphasis away (...)
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Algebraic proofs of cut elimination.Jeremy Avigad - manuscript
    Algebraic proofs of the cut-elimination theorems for classical and intuitionistic logic are presented, and are used to show how one can sometimes extract a constructive proof and an algorithm from a proof that is nonconstructive. A variation of the double-negation translation is also discussed: if ϕ is provable classically, then ¬(¬ϕ)nf is provable in minimal logic, where θnf denotes the negation-normal form of θ. The translation is used to show that cut-elimination theorems for classical logic can be viewed as special (...)
    Download  
     
    Export citation  
     
    Bookmark   9 citations  
  • Number theory and elementary arithmetic.Jeremy Avigad - 2003 - Philosophia Mathematica 11 (3):257-284.
    is a fragment of first-order aritlimetic so weak that it cannot prove the totality of an iterated exponential fimction. Surprisingly, however, the theory is remarkably robust. I will discuss formal results that show that many theorems of number theory and combinatorics are derivable in elementary arithmetic, and try to place these results in a broader philosophical context.
    Download  
     
    Export citation  
     
    Bookmark   19 citations  
  • Finitary Set Theory.Laurence Kirby - 2009 - Notre Dame Journal of Formal Logic 50 (3):227-244.
    I argue for the use of the adjunction operator (adding a single new element to an existing set) as a basis for building a finitary set theory. It allows a simplified axiomatization for the first-order theory of hereditarily finite sets based on an induction schema and a rigorous characterization of the primitive recursive set functions. The latter leads to a primitive recursive presentation of arithmetical operations on finite sets.
    Download  
     
    Export citation  
     
    Bookmark   11 citations  
  • Forcing in proof theory.Jeremy Avigad - 2004 - Bulletin of Symbolic Logic 10 (3):305-333.
    Paul Cohen’s method of forcing, together with Saul Kripke’s related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. Here, I argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or syntactic terms. I will discuss the aspects (...)
    Download  
     
    Export citation  
     
    Bookmark   15 citations  
  • Semi-honest subrecursive degrees and the collection rule in arithmetic.Andrés Cordón-Franco & F. Félix Lara-Martín - 2023 - Archive for Mathematical Logic 63 (1):163-180.
    By a result of L.D. Beklemishev, the hierarchy of nested applications of the $$\Sigma _1$$ -collection rule over any $$\Pi _2$$ -axiomatizable base theory extending Elementary Arithmetic collapses to its first level. We prove that this result cannot in general be extended to base theories of arbitrary quantifier complexity. In fact, given any recursively enumerable set of true $$\Pi _2$$ -sentences, S, we construct a sound $$(\Sigma _2 \! \vee \! \Pi _2)$$ -axiomatized theory T extending S such that the (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • A Simple Proof of Parsons' Theorem.Fernando Ferreira - 2005 - Notre Dame Journal of Formal Logic 46 (1):83-91.
    Let be the fragment of elementary Peano arithmetic in which induction is restricted to -formulas. More than three decades ago, Parsons showed that the provably total functions of are exactly the primitive recursive functions. In this paper, we observe that Parsons' result is a consequence of Herbrand's theorem concerning the -consequences of universal theories. We give a self-contained proof requiring only basic knowledge of mathematical logic.
    Download  
     
    Export citation  
     
    Bookmark   3 citations  
  • 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  
  • Truth, Pretense and the Liar Paradox.Bradley Armour-Garb & James A. Woodbridge - 2015 - In T. Achourioti, H. Galinon, J. Martínez Fernández & K. Fujimoto (eds.), Unifying the Philosophy of Truth. Dordrecht: Imprint: Springer. pp. 339-354.
    In this paper we explain our pretense account of truth-talk and apply it in a diagnosis and treatment of the Liar Paradox. We begin by assuming that some form of deflationism is the correct approach to the topic of truth. We then briefly motivate the idea that all T-deflationists should endorse a fictionalist view of truth-talk, and, after distinguishing pretense-involving fictionalism (PIF) from error- theoretic fictionalism (ETF), explain the merits of the former over the latter. After presenting the basic framework (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • Preservation theorems for bounded formulas.Morteza Moniri - 2007 - Archive for Mathematical Logic 46 (1):9-14.
    In this paper we naturally define when a theory has bounded quantifier elimination, or is bounded model complete. We give several equivalent conditions for a theory to have each of these properties. These results provide simple proofs for some known results in the model theory of the bounded arithmetic theories like CPV and PV1. We use the mentioned results to obtain some independence results in the context of intuitionistic bounded arithmetic. We show that, if the intuitionistic theory of polynomial induction (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • An ordinal analysis of admissible set theory using recursion on ordinal notations.Jeremy Avigad - 2002 - Journal of Mathematical Logic 2 (1):91-112.
    The notion of a function from ℕ to ℕ defined by recursion on ordinal notations is fundamental in proof theory. Here this notion is generalized to functions on the universe of sets, using notations for well orderings longer than the class of ordinals. The generalization is used to bound the rate of growth of any function on the universe of sets that is Σ1-definable in Kripke–Platek admissible set theory with an axiom of infinity. Formalizing the argument provides an ordinal analysis.
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • 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):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 $${\Delta_1}$$ 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\Delta_0 + \neg \mathit{exp}}$$ implies $${B\Sigma_1}$$ to a purely recursion-theoretic question.
    Download  
     
    Export citation  
     
    Bookmark   2 citations  
  • Local induction and provably total computable functions.Andrés Cordón-Franco & F. Félix Lara-Martín - 2014 - Annals of Pure and Applied Logic 165 (9):1429-1444.
    Let Iπ2 denote the fragment of Peano Arithmetic obtained by restricting the induction scheme to parameter free Π2Π2 formulas. Answering a question of R. Kaye, L. Beklemishev showed that the provably total computable functions of Iπ2 are, precisely, the primitive recursive ones. In this work we give a new proof of this fact through an analysis of certain local variants of induction principles closely related to Iπ2. In this way, we obtain a more direct answer to Kaye's question, avoiding the (...)
    Download  
     
    Export citation  
     
    Bookmark   1 citation  
  • (15 other versions)2010 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquium '10.Uri Abraham & Ted Slaman - 2011 - Bulletin of Symbolic Logic 17 (2):272-329.
    Download  
     
    Export citation  
     
    Bookmark  
  • Polynomial time ultrapowers and the consistency of circuit lower bounds.Jan Bydžovský & Moritz Müller - 2020 - Archive for Mathematical Logic 59 (1-2):127-147.
    A polynomial time ultrapower is a structure given by the set of polynomial time computable functions modulo some ultrafilter. They model the universal theory \ of all polynomial time functions. Generalizing a theorem of Hirschfeld :111–126, 1975), we show that every countable model of \ is isomorphic to an existentially closed substructure of a polynomial time ultrapower. Moreover, one can take a substructure of a special form, namely a limit polynomial time ultrapower in the classical sense of Keisler Ultrafilters across (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Consistency statements and iterations of computable functions in IΣ1 and PRA.Joost J. Joosten - 2010 - Archive for Mathematical Logic 49 (7-8):773-798.
    In this paper we will state and prove some comparative theorems concerning PRA and IΣ1. We shall provide a characterization of IΣ1 in terms of PRA and iterations of a class of functions. In particular, we prove that for this class of functions the difference between IΣ1 and PRA is exactly that, where PRA is closed under iterations of these functions, IΣ1 is moreover provably closed under iteration. We will formulate a sufficient condition for a model of PRA to be (...)
    Download  
     
    Export citation  
     
    Bookmark