Cut elimination for GLS using the terminability of its regress process

DOI10.1007/S10992-015-9368-4zbMath1392.03057OpenAlexW2031842318MaRDI QIDQ288243

Jude Brighton

Publication date: 25 May 2016

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

Full work available at URL: https://doi.org/10.1007/s10992-015-9368-4

zbMATH Keywords

modal logiccut-eliminationGentzen-style logicGLregress trees

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Cut-elimination and normal-form theorems (03F05) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Related Items (4)

Cut-elimination for provability logic by terminating proof-search: formalised and deconstructed using Coq ⋮ Tautology Elimination, Cut Elimination, and S5 ⋮ A proof theory for the logic of provability in true arithmetic ⋮ Cut elimination by unthreading

Cites Work

• The modal logic of provability: cut-elimination
• On some proof theoretical properties of the modal logic GL
• The modal logic of provability. The sequential approach
• Provability interpretations of modal logic
• Solution of a problem of Leon Henkin
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Cut elimination for GLS using the terminability of its regress process