The bounded proof property via step algebras and step frames

DOI10.1016/j.apal.2014.07.005zbMath1361.03013OpenAlexW2000108579MaRDI QIDQ741087

Silvio Ghilardi, Nick Bezhanishvili

Publication date: 10 September 2014

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.apal.2014.07.005

zbMATH Keywords

modal logicfinite model propertybounded proof propertystep correspondence

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Other algebras related to logic (03G25)

Related Items

Hypersequent rules with restricted contexts for propositional modal logics ⋮ Lattice logic as a fragment of (2-sorted) residuated modal logic ⋮ BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS ⋮ Algebraic proof theory: hypersequents and hypercompletions ⋮ Modal translation of substructural logics ⋮ COMPLETE ADDITIVITY AND MODAL INCOMPLETENESS

Uses Software

• SQEMA
• Pesca

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Algebraic proof theory for substructural logics: cut-elimination and completions
• Algorithmic correspondence and canonicity for distributive modal logic
• Sahlqvist correspondence for modal mu-calculus
• MacNeille completions of FL-algebras
• The modal logic of provability: cut-elimination
• Gentzen calculi for modal propositional logic
• The modal logic of provability. The sequential approach
• Topology and duality in modal logic
• A modal sequent calculus for a fragment of arithmetic
• Model theory.
• Tools and techniques in modal logic
• Admissibility of logical inference rules
• An algebraic theory of normal forms
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Algebraic aspects of cut elimination
• Modal frame correspondences and fixed-points
• Elementary canonical formulae: extending Sahlqvist's theorem
• Normal forms in modal logic
• Sahlqvist Formulas in Hybrid Polyadic Modal Logics
• Bounded Proofs and Step Frames
• Correspondence between Modal Hilbert Axioms and Sequent Rules with an Application to S5
• Continuity, freeness, and filtrations
• Constructing Cut Free Sequent Systems with Context Restrictions Based on Classical or Intuitionistic Logic
• A unified semantic framework for fully structural propositional sequent systems
• Finitely generated free Heyting algebras via Birkhoff duality and coalgebra
• A Cook's Tour of the Finitary Non-Well-Founded Sets
• Kripke Semantics for Basic Sequent Systems
• Cut Elimination for Shallow Modal Logics
• Free Modal Algebras: A Coalgebraic Perspective
• Canonical rules
• On modal systems having arithmetical interpretations
• A Cut‐Free Calculus For Dummett's LC Quantified
• A new proof of Sahlqvist's theorem on modal definability and completeness
• The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination
• Unified Correspondence
• Free Modal Algebras Revisited: The Step-by-Step Method
• From Frame Properties to Hypersequent Rules in Modal Logics
• On generalizing free algebras for a functor
• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
• Minimal predicates, fixed-points, and definability