A cut-free proof system for a predicate extension of the logic of provability

DOI10.4467/20842589RM.18.006.8839zbMATH Open1432.03126arXiv1802.10261MaRDI QIDQ4627727FDOQ4627727

Authors: Yoshihito Tanaka 

Publication date: 11 March 2019

Published in: Reports on Mathematical Logic (Search for Journal in Brave)

Abstract: In this paper, we introduce a proof system $mathsfNQGL$ for a Kripke complete predicate extension of the logic $mathbfGL$, that is, the logic of provability, which is defned by $mathbfK$ and the L"{o}b formula $Box(Boxpsupsetp)supsetBoxp$. $mathsfNQGL$ is a modal extension of Gentzen's sequent calculus $mathsfLK$. Although the propositional fragment of $mathsfNQGL$ axiomatizes $mathbfGL$, it does not have the L"{o}b formula as its axiom. Instead, it has a non-compact rule, that is, a derivation rule with countably many premises. We show that $mathsfNQGL$ enjoys cut admissibility and is complete with respect to the class of Kripke frames such that for each world, the supremum of the length of the paths from the world is finite.

Full work available at URL: https://arxiv.org/abs/1802.10261

Recommendations

• The predicate modal logic of provability
• Provability logics with quantifiers on proofs
• Nested sequents for provability logic GLP: FIG. 1.
• Arithmetical interpretations and Kripke frames of predicate modal logic of provability
• A proof theory for the logic of provability in true arithmetic

zbMATH Keywords

predicate logicprovability logiccut-free system

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Cited In (2)

• An \(\omega\)-rule for the logic of provability and its models
• Strong extension-free proof systems

This page was built for publication: A cut-free proof system for a predicate extension of the logic of provability

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