Description

• Title:
  Harmony and Normalisation in Bilateral Logic
• Creator:
  del Valle-Inclan, Pedro
• Contributor:
  Scuola Normale Superiore, Department of Philosophy;
  pedro.delvalleinclan@sns.it
• Description:
  In a recent paper del Valle-Inclan and Schlöder argue that bilateral calculi call for their own notion of proof-theoretic harmony, distinct from the usual (or ‘unilateral’) ones. They then put forward a specifically bilateral criterion of harmony, and present a harmonious bilateral calculus for classical logic.In this paper, I show how del Valle-Inclan and Schlöder’s criterion of harmony suggests a notion of normal form for bilateral systems, and prove normalisation for two (harmonious) bilateral calculi for classical logic, HB1 and HB2. The resulting normal derivations have the usual desirable features, like the separation and subformula properties. HB1-normal form turns out to be strictly stronger that the notion of normal form proposed by Nils Kürbis, and HB2-normal form is neither stronger nor weaker than a similar proposal by Marcello D’Agostino, Dov Gabbay, and Sanjay Modgyl.
• Object availability:
  free access
• Rights: https://creativecommons.org/licenses/by-nc-nd/4.0
• Date:
  2023.10.26;
  2023.07.18
• Type:
  Other
• Language:
  English
• Format:
  application/pdf
• Publisher:
  Wydawnictwo Uniwersytetu Łódzkiego
• Relation:
  Bulletin of the Section of Logic;3;
  52
• Subject:
  bilateralism;
  normalisation;
  harmony
• Identifier:
  0138-0680;
  http://hdl.handle.net/11089/48186 ;
  2449-836X;
  10.18778/0138-0680.2023.14
• Data provider:
  Repozytorium Uniwersytetu Łódzkiego
• Can I use it?:
  check license
• Type:
  other