TY - JOUR AU - Schwartz, Yehuda AU - Tourlakis, George PY - 2013/09/18 Y2 - 2024/03/29 TI - On the proof-theory of a first-order extension of GL JF - Logic and Logical Philosophy JA - LLP VL - 23 IS - 3 SE - Articles DO - 10.12775/LLP.2013.030 UR - https://apcz.umk.pl/LLP/article/view/LLP.2013.030 SP - 329–363 AB - 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. ER -