Description

• Title:
  On the proof-theory of a first-order extension of GL
• Creator:
  Schwartz, Yehuda;
  Tourlakis, George
• Description:
  We introduce a first order extension of GL, called ML3, 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 ML3, as well as proofs for Craig’s interpolation theorem for GLTS. Turning to semantics we prove that ML3 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 ML3 is possible.
• Object availability:
  free access
• Rights:
  Prawa autorskie (c) 2017 Logic and Logical Philosophy
• Date:
  2013.09.18
• Type:
  info:eu-repo/semantics/article;
  info:eu-repo/semantics/publishedVersion
• Language:
  English
• Source:
  Logic and Logical Philosophy; Vol. 23 No. 3 (2014): September; 329–363;
  Logic and Logical Philosophy; Tom 23 Nr 3 (2014): September; 329–363;
  2300-9802;
  1425-3305
• Format:
  application/pdf
• Publisher:
  Uniwersytet Mikołaja Kopernika w Toruniu
• Relation: https://apcz.umk.pl/LLP/article/view/LLP.2013.030/1901
• Subject:
  Gentzen-style logic;
  Gentzen’s Hauptsatz;
  Hilbert-style logic;
  GL;
  K4;
  provability logic;
  provability predicate;
  modal first-order logic;
  sequent calculus;
  cut-elimination;
  reflection theorem;
  Craig interpolation;
  arithmetical interpretation;
  soundness;
  a
• Identifier: https://apcz.umk.pl/LLP/article/view/LLP.2013.030
• Data provider:
  Akademicka Platforma Czasopism
• Can I use it?:
  seek permission
• Type:
  text