3 papers
cs.LO2024
Syntactic Cut-Elimination for Provability Logic GL via Nested Sequents
Akinori Maniwa, Ryo Kashima
The cut-elimination procedure for the provability logic is known to be problematic: a Löb-like rule keeps cut-formulae intact on reduction, even in the principal case, thereby comp…
math.LO2023
Cut-free sequent calculi for the provability logic D
Ryo Kashima, Taishi Kurahashi, Sohei Iwata +1
We say that a Kripke model is a GL-model if the accessibility relation is transitive and converse well-founded. We say that a Kripke model is a D-model if it is obtained by…
math.LO2023
Semantical cut-elimination for the provability logic of true arithmetic
Ryo Kashima, Yutaka Kato
The quasi-normal modal logic GLS is a provability logic formalizing the arithmetical truth. Kushida (2020) gave a sequent calculus for GLS and proved the cut-elimination theorem. T…