TY - JOUR
AU - Schwartz, Yehuda
AU - Tourlakis, George
PY - 2013/09/18
Y2 - 2024/06/23
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 -