Following logician Gerhard Gentzen’s (1909–1945) thesis that introduction and elimination define or constitute the meaning of logical connectives, describes a pair of introduction and elimination rules when the two match or align in an appropriate way. Suppose that the steps preceding the introduction rules for a connective constitute the grounds under which formulae with that connective may be asserted. Then harmony corresponds to the thesis that the accompanying elimination rule ought to yield nothing over and above those grounds, i.e., the rules are harmonious when the elimination rule for a connective can yield no inference not already derivable from the grounds under which that connective is introduced. Conjunction provides an example of rules that are paradigmatically harmonious:

The alignment between these two rules is found in the fact that the grounds for asserting a conjunction ${\phi }_0\wedge {\phi }_1$—that ${\phi }_0$ and ${\phi }_1$ hold—are precisely what may be inferred from ${\phi }_0\wedge {\phi }_1$. A fortiori, anything that can be derived from ${\phi }_0\wedge {\phi }_1$ can be derived from the joint appearance of ${\phi }_0$ and ${\phi }_1$. Proof-theoretic harmony has been essential in one way of making precise the defect of logician Arthur Prior’s (1914–1969) connective tonk, which has the following rules:

The converse to harmony is stability, the condition that the grounds under which a complex formula is introduced can always be recovered by means of the elimination rules. In this sense, harmony is the thesis that nothing is gained from an introduction rule while stability is the thesis that nothing is lost in an elimination rule.