  Gentzen’s sequent calculus exhibits a symmetry between right and left introduction rules which suggest to look for a harmony principle that makes this symmetry significant to proof-theoretic semantics. At least three lines have been pursued to deal with this phenomenon. (i) Either the right-introduction or or the left-introduction rules are considered to be introduction rules. The opposite rules (left-introductions and right-introductions, respectively) are then justified using the corresponding elimination rules. This means that the methods discussed before are applied to whole sequents rather than formulas within sequents. Unlike these formulas, the sequents are not logically structured. Therefore this approach builds on definitional reflection, which applies harmony and inversion to rules for arbitrarily structured entities rather than for logical composites only. It has been pursued by de Campos Sanz and Piecha (2009). (ii) The right- and left-introduction rules are derived from a characterization in the sense of Došen’s double line rules (section  2.4),  which is then read as a definition of some sort. The top-down direction of a double-line rule is already a right- or a left-introduction rule. The other one can be derived from the bottom-up direction by means of certain principles. This is the basic meaning-theoretic ingredient of Sambin et al.’s Basic Logic (Sambin, Battilotti, and Faggian, 2000). (iii) The right- and left-introduction rules are seen as expressing an interaction between sequents using the rule of cut. Given either the right- or the left-rules, the complementary rules express that everything that interacts with its premisses in a certain way so does with its conclusion. This idea of interaction is a generalized symmetric principle of definitional reflection. It can be considered to be a generalization of the inversion principle, using the notion of interaction rather than the derivability of consequences (see Schroeder-Heister, 2013). All three approaches apply to the sequent calculus in its classical form, with possibly more than one formula in the succedent of a sequent, including structurally restricted versions as investigated in linear and other logics.