証明可能性論理GLのシークエント計算体系
メモ
H. Kushida; "A proof theory for the logic of provability in true arithmetic"
に
様相論理GLS
の
シークエント計算
が載っており，それの部分体系としても得られる．
メモ
H. Kushida; "A proof theory for the logic of provability in true arithmetic"
による
統語論的なカット除去定理証明
S. Valentini; 1983; "The Modal Logic of Provability: Cut-Elimination"
初めて導入された？
A. Avron; 1984; "On Modal Systems Having Arithmetical Interpretations"
J. Brighton; "Cut-elimination for GLS using the terminability of its regress process"
M. Borga; "On Some Proof Theoretical Properties of the Modal Logic GL"
Sara Negri; 2005; "Proof Analysis in Modal Logic"
R. Goré, R. Ramanayake; 2008; "Valentini's Cut-Elimination for Provability Logic Resolved"
Valentini1983の再訪．
F. Poggiolesi; 2009; "A Purely Syntatic and Cut-Free Sequent Calculus for the Modal Logic of Provability"
K. Sasaki; "Löb's Axiom and Cut-Elimination Theorem"
https://core.ac.uk/download/pdf/236153639.pdf
意味論的カット除去定理
G. Sambin, S. Valentini; 1980; "The Modal Logic of Provability. The Sequential Approach"
A. Avron; 1984; "On Modal Systems Having Arithmetical Interpretations"