@article{Schwartz_Tourlakis_2013, title={On the proof-theory of a first-order extension of GL}, volume={23}, url={https://apcz.umk.pl/LLP/article/view/LLP.2013.030}, DOI={10.12775/LLP.2013.030}, abstractNote={We introduce a first order extension of GL, called ML<sup>3</sup>, and develop its proof theory via a proxy cut-free sequent calculus GLTS. We prove the highly nontrivial result that cut is a derived rule in GLTS, a result that is unavailable in other known first-order extensions of GL. This leads to proofs of weak reflection and the related conservation result for ML<sup>3</sup>, as well as proofs for Craig’s interpolation theorem for GLTS. Turning to semantics we prove that ML<sup>3</sup> is sound with respect to arithmetical interpretations and that it is also sound and complete with respect to converse well-founded and transitive finite Kripke models. This leads us to expect that a Solovay-like proof of arithmetical completeness of ML<sup>3</sup> is possible.}, number={3}, journal={Logic and Logical Philosophy}, author={Schwartz, Yehuda and Tourlakis, George}, year={2013}, month={Sep.}, pages={329–363} }