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

DOI10.4467/20842589RM.18.006.8839MaRDI QIDQ4627727zbMATH OpenFDO

Authors Yoshihito Tanaka

Publication date 11 March 2019

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

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

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)

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.

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

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)