HARMONY AND NORMALISATION IN BILATERAL LOGIC.

In a recent paper del Valle-Inclan and Schloder 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 Kurbis, and HB2-normal form is neither stronger nor weaker than a similar proposal by Marcello D'Agostino, Dov Gabbay, and Sanjay Modgyl. [ABSTRACT FROM AUTHOR]