21 found
Order:
  1.  24
    The Omega-Rule Interpretation of Transfinite Provability Logic.David Fernández-Duque & Joost J. Joosten - 2018 - Annals of Pure and Applied Logic 169 (4):333-371.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   4 citations  
  2.  14
    On Provability Logics with Linearly Ordered Modalities.Lev D. Beklemishev, David Fernández-Duque & Joost J. Joosten - 2014 - Studia Logica 102 (3):541-566.
    We introduce the logics GLP Λ, a generalization of Japaridze’s polymodal provability logic GLP ω where Λ is any linearly ordered set representing a hierarchy of provability operators of increasing strength. We shall provide a reduction of these logics to GLP ω yielding among other things a finitary proof of the normal form theorem for the variable-free fragment of GLP Λ and the decidability of GLP Λ for recursive orderings Λ. Further, we give a restricted axiomatization of the variable-free fragment (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  3.  7
    Models of Transfinite Provability Logic.David Fernández-Duque & Joost J. Joosten - 2013 - Journal of Symbolic Logic 78 (2):543-561.
    For any ordinal $\Lambda$, we can define a polymodal logic $\mathsf{GLP}_\Lambda$, with a modality $[\xi]$ for each $\xi < \Lambda$. These represent provability predicates of increasing strength. Although $\mathsf{GLP}_\Lambda$ has no Kripke models, Ignatiev showed that indeed one can construct a Kripke model of the variable-free fragment with natural number modalities, denoted $\mathsf{GLP}^0_\omega$. Later, Icard defined a topological model for $\mathsf{GLP}^0_\omega$ which is very closely related to Ignatiev's. In this paper we show how to extend these constructions for arbitrary $\Lambda$. (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   10 citations  
  4.  30
    Hyperations, Veblen Progressions and Transfinite Iteration of Ordinal Functions.David Fernández-Duque & Joost J. Joosten - 2013 - Annals of Pure and Applied Logic 164 (7-8):785-801.
    Ordinal functions may be iterated transfinitely in a natural way by taking pointwise limits at limit stages. However, this has disadvantages, especially when working in the class of normal functions, as pointwise limits do not preserve normality. To this end we present an alternative method to assign to each normal function f a family of normal functions Hyp[f]=〈fξ〉ξ∈OnHyp[f]=〈fξ〉ξ∈On, called its hyperation, in such a way that f0=idf0=id, f1=ff1=f and fα+β=fα∘fβfα+β=fα∘fβ for all α, β.Hyperations are a refinement of the Veblen hierarchy (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   7 citations  
  5.  15
    Two New Series of Principles in the Interpretability Logic of All Reasonable Arithmetical Theories.Evan Goris & Joost J. Joosten - 2020 - Journal of Symbolic Logic 85 (1):1-25.
    The provability logic of a theory T captures the structural behavior of formalized provability in T as provable in T itself. Like provability, one can formalize the notion of relative interpretability giving rise to interpretability logics. Where provability logics are the same for all moderately sound theories of some minimal strength, interpretability logics do show variations.The logic IL is defined as the collection of modal principles that are provable in any moderately sound theory of some minimal strength. In this article (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  6.  48
    The Interpretability Logic of All Reasonable Arithmetical Theories.Joost J. Joosten & Albert Visser - 2000 - Erkenntnis 53 (1-2):3-26.
    This paper is a presentation of astatus quæstionis, to wit of the problemof the interpretability logic of all reasonablearithmetical theories.We present both the arithmetical side and themodal side of the question.Dedicated to Dick de Jongh on the occasion of his 60th birthday.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   9 citations  
  7.  37
    Provability and Interpretability Logics with Restricted Realizations.Thomas F. Icard & Joost J. Joosten - 2012 - Notre Dame Journal of Formal Logic 53 (2):133-154.
    The provability logic of a theory $T$ is the set of modal formulas, which under any arithmetical realization are provable in $T$. We slightly modify this notion by requiring the arithmetical realizations to come from a specified set $\Gamma$. We make an analogous modification for interpretability logics. We first study provability logics with restricted realizations and show that for various natural candidates of $T$ and restriction set $\Gamma$, the result is the logic of linear frames. However, for the theory Primitive (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  8.  12
    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.
    Let T be a second-order arithmetical theory, Λ a well-order, λ < Λ and X ⊆ ℕ. We use $[\lambda |X]_T^{\rm{\Lambda }}\varphi$ as a formalization of “φ is provable from T and an oracle for the set X, using ω-rules of nesting depth at most λ”.For a set of formulas Γ, define predicative oracle reflection for T over Γ ) to be the schema that asserts that, if X ⊆ ℕ, Λ is a well-order and φ ∈ Γ, then$$\forall \,\lambda (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  9.  1
    Kripke Models of Transfinite Provability Logic.David Fernández-Duque & Joost J. Joosten - 2012 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 185-199.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   3 citations  
  10.  18
    Empirical Encounters with Computational Irreducibility and Unpredictability.Hector Zenil, Fernando Soler-Toscano & Joost J. Joosten - 2012 - Minds and Machines 22 (3):149-165.
    The paper presents an exploration of conceptual issues that have arisen in the course of investigating speed-up and slowdown phenomena in small Turing machines, in particular results of a test that may spur experimental approaches to the notion of computational irreducibility. The test involves a systematic attempt to outrun the computation of a large number of small Turing machines (3 and 4 state, 2 symbol) by means of integer sequence prediction using a specialized function for that purpose. The experiment prompts (...)
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  11.  14
    The Closed Fragment of the Interpretability Logic of PRA with a Constant for $\mathrm{I}\sigma_1$.Joost J. Joosten - 2005 - Notre Dame Journal of Formal Logic 46 (2):127-146.
    In this paper we carry out a comparative study of $\mathrm{I}\Sigma_1$ and PRA. We will in a sense fully determine what these theories have to say about each other in terms of provability and interpretability. Our study will result in two arithmetically complete modal logics with simple universal models.
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  12.  9
    Interpretability in PRA.Marta Bílková, Dick de Jongh & Joost J. Joosten - 2010 - Annals of Pure and Applied Logic 161 (2):128-138.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  13.  7
    Interpretability In.Marta Bílková, Dick de Jongh & Joost J. Joosten - 2010 - Annals of Pure and Applied Logic 161 (2):128-138.
    In this paper, we study IL(), the interpretability logic of . As is neither an essentially reflexive theory nor finitely axiomatizable, the two known arithmetical completeness results do not apply to : IL() is not or . IL() does, of course, contain all the principles known to be part of IL, the interpretability logic of the principles common to all reasonable arithmetical theories. In this paper, we take two arithmetical properties of and see what their consequences in the modal logic (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  14.  12
    The Closed Fragment of the Interpretability Logic of PRA with a Constant For.Joost J. Joosten - 2005 - Notre Dame Journal of Formal Logic 46 (2):127-146.
    In this paper we carry out a comparative study of and PRA. We will in a sense fully determine what these theories have to say about each other in terms of provability and interpretability. Our study will result in two arithmetically complete modal logics with simple universal models.
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  15.  3
    An Escape From Vardanyan’s Theorem.Ana de Almeida Borges & Joost J. Joosten - forthcoming - Journal of Symbolic Logic:1-26.
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  16.  2
    Theory and Application of Labelling Techniques for Interpretability Logics.Evan Goris, Marta Bílková, Joost J. Joosten & Luka Mikec - 2022 - Mathematical Logic Quarterly 68 (3):352-374.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  17.  5
    Münchhausen Provability.Joost J. Joosten - 2021 - Journal of Symbolic Logic 86 (3):1006-1034.
    By Solovay’s celebrated completeness result [31] on formal provability we know that the provability logic ${\textbf {GL}}$ describes exactly all provable structural properties for any sound and strong enough arithmetical theory with a decidable axiomatisation. Japaridze generalised this result in [22] by considering a polymodal version ${\mathsf {GLP}}$ of ${\textbf {GL}}$ with modalities $[n]$ for each natural number n referring to ever increasing notions of provability. Modern treatments of ${\mathsf {GLP}}$ tend to interpret the $[n]$ provability notion as “provable in (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  18.  40
    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 (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark  
  19.  11
    The Logic of Turing Progressions.Eduardo Hermo Reyes & Joost J. Joosten - 2020 - Notre Dame Journal of Formal Logic 61 (1):155-180.
    Turing progressions arise by iteratedly adding consistency statements to a base theory. Different notions of consistency give rise to different Turing progressions. In this paper we present a logic that generates exactly all relations that hold between these different Turing progressions given a particular set of natural consistency notions. Thus, the presented logic is proven to be arithmetically sound and complete for a natural interpretation, named the formalized Turing progressions interpretation.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark  
  20.  3
    Kripke Models of Transfinite Provability Logic.David Fernández-Duque & Joost J. Joosten - 2012 - In Thomas Bolander, Torben Braüner, Silvio Ghilardi & Lawrence Moss (eds.), Advances in Modal Logic, Volume 9. CSLI Publications. pp. 185-199.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  21.  27
    Propositional Proof Systems and Fast Consistency Provers.Joost J. Joosten - 2007 - Notre Dame Journal of Formal Logic 48 (3):381-398.
    A fast consistency prover is a consistent polytime axiomatized theory that has short proofs of the finite consistency statements of any other polytime axiomatized theory. Krajíček and Pudlák have proved that the existence of an optimal propositional proof system is equivalent to the existence of a fast consistency prover. It is an easy observation that NP = coNP implies the existence of a fast consistency prover. The reverse implication is an open question. In this paper we define the notion of (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark