Description

• Title:
  Hypersequent Calculi for S5: The Methods of Cut Elimination
• Creator:
  Bednarska, Kaja;
  Indrzejczak, Andrzej
• Description:
  S5 is one of the most important modal logic with nice syntactic, semantic and algebraic properties. In spite of that, a successful (i.e. cut-free) formalization of S5 on the ground of standard sequent calculus (SC) was problematic and led to the invention of numerous nonstandard, generalized forms of SC. One of the most interesting framework which was very often used for this aim is that of hypersequent calculi (HC). The paper is a survey of HC for S5 proposed by Pottinger, Avron, Restall, Poggiolesi, Lahav and Kurokawa. We are particularly interested in examining different methods which were used for proving the eliminability/admissibility of cut in these systems and present our own variant of a system which admits relatively simple proof of cut elimination.
• Object availability:
  free access
• Rights:
  Prawa autorskie (c) 2017 Logic and Logical Philosophy
• Date:
  2015.08.25
• Type:
  info:eu-repo/semantics/article;
  info:eu-repo/semantics/publishedVersion
• Language:
  English
• Source:
  Logic and Logical Philosophy; Vol. 24 No. 3 (2015): September; 277–311;
  Logic and Logical Philosophy; Tom 24 Nr 3 (2015): September; 277–311;
  2300-9802;
  1425-3305
• Format:
  application/pdf
• Publisher:
  Uniwersytet Mikołaja Kopernika w Toruniu
• Relation: https://apcz.umk.pl/LLP/article/view/LLP.2015.018/6733
• Subject:
  cut elimination;
  modal logic;
  hypersequent calculi;
  proof theory
• Identifier: https://apcz.umk.pl/LLP/article/view/LLP.2015.018
• Data provider:
  Akademicka Platforma Czasopism
• Can I use it?:
  seek permission
• Type:
  text