The modal logic of provability. The sequential approach

DOI10.1007/BF00293433zbMath0523.03014OpenAlexW2034070758MaRDI QIDQ1056745

Giovanni Sambin, Silvio Valentini

Publication date: 1982

Published in: Journal of Philosophical Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00293433

zbMATH Keywords

modal logicarithmeticfixed point theoremsemanticsprovabilitycut-eliminationarithmetical completeness theoremsequentsproof-theory

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05)

Related Items (34)

VALENTINI’S CUT-ELIMINATION FOR PROVABILITY LOGIC RESOLVED ⋮ Cut elimination for GLS using the terminability of its regress process ⋮ An epistemic logic for becoming informed ⋮ Effectively constructible fixed points in Sacchetti's modal logics of provability ⋮ Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq ⋮ The Henkin Sentence ⋮ A formalization of Sambins's normalization for GL ⋮ Uniform interpolation and propositional quantifiers in modal logics ⋮ Provability in finite subtheories of PA and relative interpretability: a modal investigation ⋮ Provability multilattice logic ⋮ Polynomially and superexponentially shorter proofs in fragments of arithmetic ⋮ On the proof-theory of two formalisations of modal first-order logic ⋮ A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs ⋮ A realization theorem for the Gödel-Löb provability logic ⋮ A proof theory for the logic of provability in true arithmetic ⋮ The fixed point property in modal logic ⋮ Provability: The emergence of a mathematical modality ⋮ Modal interpolation via nested sequents ⋮ Intuitionistic Decision Procedures Since Gentzen ⋮ Kripke Semantics for Basic Sequent Systems ⋮ Cut-elimination for weak Grzegorczyk logic Go ⋮ 2003 European Summer Meeting of the Association for Symbolic Logic. Logic Colloquim '03 ⋮ Note on some fixed point constructions in provability logic ⋮ The Method of Tree-Hypersequents for Modal Propositional Logic ⋮ Formal topological characterizations of various continuous domains ⋮ The bounded proof property via step algebras and step frames ⋮ Unnamed Item ⋮ The modal logic of provability: cut-elimination ⋮ Interpolation properties for Sacchetti's logics ⋮ Modal tableau calculi and interpolation ⋮ On some proof theoretical properties of the modal logic GL ⋮ Circular proofs for the Gödel-Löb provability logic ⋮ Syntactical results on the arithmetical completeness of modal logic ⋮ Proof analysis in modal logic

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The modal logic of provability: cut-elimination
• Intuitionistic diagonalizable algebras
• A modal sequent calculus for a fragment of arithmetic
• The uniqueness of the fixed-point in every diagonalizable algebra. (The algebraization of the theories which express Theor. VIII.)
• Provability interpretations of modal logic
• An effective fixed-point theorem in intuitionistic diagonalizable algebras. (The algebraization of the theories which express Theor. IX.)
• Solution of a problem of Leon Henkin
• THE MODAL LOGIC OF CONSISTENCY ASSERTIONS OF PEANO ARITHMETIC
• On the proof theory of the modal logic for arithmetic provability
• Extremely undecidable sentences

This page was built for publication: The modal logic of provability. The sequential approach