The bounded proof property via step algebras and step frames

DOI10.1016/J.APAL.2014.07.005MaRDI QIDQ741087zbMATH OpenOpenAlexFDO

Authors Nick Bezhanishvili, Silvio Ghilardi

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)

Recommendations

• Bounded proofs and step frames
• One-step Heyting algebras and hypersequent calculi with the bounded proof property
• Steps towards a proof-theoretical semantics
• Logic of Proofs for Bounded Arithmetic
• On Extending Bounded Proofs to Inductive Proofs
• Proving consistency of equational theories in bounded arithmetic
• On the provability logic of bounded arithmetic
• Axiomatizing proof tree concepts in bounded arithmetic
• scientific article; zbMATH DE number 2196511
• scientific article; zbMATH DE number 4006236

Cites work

• scientific article; zbMATH DE number 1003731 (Why is no real title available?)
• scientific article; zbMATH DE number 3131074 (Why is no real title available?)
• scientific article; zbMATH DE number 4041866 (Why is no real title available?)
• scientific article; zbMATH DE number 956466 (Why is no real title available?)
• scientific article; zbMATH DE number 496003 (Why is no real title available?)
• scientific article; zbMATH DE number 6863852 (Why is no real title available?)
• scientific article; zbMATH DE number 2196598 (Why is no real title available?)
• A Cook's tour of the finitary non-well-founded sets
• A Cut‐Free Calculus For Dummett's LC Quantified
• A modal sequent calculus for a fragment of arithmetic
• A new proof of Sahlqvist's theorem on modal definability and completeness
• A unified semantic framework for fully structural propositional sequent systems
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Admissibility of logical inference rules
• Algebraic aspects of cut elimination
• Algebraic proof theory for substructural logics: cut-elimination and completions
• Algorithmic correspondence and canonicity for distributive modal logic
• Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA
• An algebraic theory of normal forms
• Bounded proofs and step frames
• Canonical rules
• Constructing cut free sequent systems with context restrictions based on classical or intuitionistic logic
• Continuity, freeness, and filtrations
• Correspondence between modal Hilbert axioms and sequent rules with an application to S5
• Cut elimination for shallow modal logics
• Cut-free hypersequent calculus for S4.3.
• Elementary canonical formulae: a survey on syntactic, algorithmic, and model-theoretic aspects
• Elementary canonical formulae: extending Sahlqvist's theorem
• Finitely generated free Heyting algebras via Birkhoff duality and coalgebra
• Free Modal Algebras: A Coalgebraic Perspective
• Free algebras for Gödel-Löb provability logic
• Free modal algebras revisited: the step-by-step method
• From Frame Properties to Hypersequent Rules in Modal Logics
• Gentzen calculi for modal propositional logic
• Kripke Semantics for Basic Sequent Systems
• MacNeille completions of FL-algebras
• Minimal predicates, fixed-points, and definability
• Modal frame correspondences and fixed-points
• Modal logic
• Model theory.
• Normal forms in modal logic
• On generalizing free algebras for a functor.
• On modal systems having arithmetical interpretations
• Sahlqvist correspondence for modal mu-calculus
• Sahlqvist formulas in hybrid polyadic modal logics
• Structural proof theory. With an appendix by Aarne Ranta
• The logic of transitive and dense frames: from the step-frame analysis to full cut-elimination
• The modal logic of provability. The sequential approach
• The modal logic of provability: cut-elimination
• Tools and techniques in modal logic
• Topology and duality in modal logic
• Unified correspondence
• Valentini's cut-elimination for provability logic resolved

Cited in

(8)

• Hypersequent rules with restricted contexts for propositional modal logics
• Lattice logic as a fragment of (2-sorted) residuated modal logic
• Algebraic proof theory: hypersequents and hypercompletions
• COMPLETE ADDITIVITY AND MODAL INCOMPLETENESS
• Modal translation of substructural logics
• BOUNDED-ANALYTIC SEQUENT CALCULI AND EMBEDDINGS FOR HYPERSEQUENT LOGICS
• Bounded proofs and step frames
• One-step Heyting algebras and hypersequent calculi with the bounded proof property

Describes a project that uses

Uses Software

• SQEMA
• Pesca

This page was built for publication: The bounded proof property via step algebras and step frames

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q741087)