In the proof method of sequent calculi, the sequents that form the leaves of the proof, i.e., the sequents that are not introduced by earlier sequents. Identity axioms—sequents of the form $\phi \Rightarrow \phi$—are typically employed as initial sequents, although some sequent calculi allow other axioms, e.g., the sequent

that corresponds to the introduction of a falsum constant.