Switch to: References

Add citations

You must login to add citations.
  1. Provability multilattice logic.Yaroslav Petrukhin - 2022 - Journal of Applied Non-Classical Logics 32 (4):239-272.
    In this paper, we introduce provability multilattice logic PMLn and multilattice arithmetic MPAn which extends first-order multilattice logic with equality by multilattice versions of Peano axioms. We show that PMLn has the provability interpretation with respect to MPAn and prove the arithmetic completeness theorem for it. We formulate PMLn in the form of a nested sequent calculus and show that cut is admissible in it. We introduce the notion of a provability multilattice and develop algebraic semantics for PMLn on its (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • A Proof Theory for the Logic of Provability in True Arithmetic.Hirohiko Kushida - 2020 - Studia Logica 108 (4):857-875.
    In a classical 1976 paper, Solovay proved the arithmetical completeness of the modal logic GL; provability of a formula in GL coincides with provability of its arithmetical interpretations of it in Peano Arithmetic. In that paper, he also provided an axiomatic system GLS and proved arithmetical completeness for GLS; provability of a formula in GLS coincides with truth of its arithmetical interpretations in the standard model of arithmetic. Proof theory for GL has been studied intensively up to the present day. (...)
    Download  
     
    Export citation  
     
    Bookmark  
  • Nested sequents for provability logic GLP: FIG. 1.Daniyar Shamkanov - 2015 - Logic Journal of the IGPL 23 (5):789-815.
    Download  
     
    Export citation  
     
    Bookmark  
  • The bounded proof property via step algebras and step frames.Nick Bezhanishvili & Silvio Ghilardi - 2014 - Annals of Pure and Applied Logic 165 (12):1832-1863.
    Download  
     
    Export citation  
     
    Bookmark   7 citations  
  • Cut Elimination for GLS Using the Terminability of its Regress Process.Jude Brighton - 2016 - Journal of Philosophical Logic 45 (2):147-153.
    The system GLS, which is a modal sequent calculus system for the provability logic GL, was introduced by G. Sambin and S. Valentini in Journal of Philosophical Logic, 11, 311–342,, and in 12, 471–476,, the second author presented a syntactic cut-elimination proof for GLS. In this paper, we will use regress trees in order to present a simpler and more intuitive syntactic cut derivability proof for GLS1, which is a variant of GLS without the cut rule.
    Download  
     
    Export citation  
     
    Bookmark   6 citations