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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  • 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  
  • 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.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  • Classical predicative logic-enriched type theories.Robin Adams & Zhaohui Luo - 2010 - Annals of Pure and Applied Logic 161 (11):1315-1345.
    A logic-enriched type theory is a type theory extended with a primitive mechanism for forming and proving propositions. We construct two LTTs, named and , which we claim correspond closely to the classical predicative systems of second order arithmetic and . We justify this claim by translating each second order system into the corresponding LTT, and proving that these translations are conservative. This is part of an ongoing research project to investigate how LTTs may be used to formalise different approaches (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   1 citation