A rule of inference that governs when one may add a connective $\circ$ to a formula. For example, the introduction rules for disjunction $\vee$ in classical logic are:

These rules describe the conditions under which a disjunction may be introduced in a proof. Introduction rules are dual to elimination rules, which describe cases in which a formula may be simplified by eliminating its main connective.

In sequent calculi, there are no elimination rules but two types of introduction rules: left-introduction and right-introduction. Returning to disjunction, the left introduction rule for disjunction is represented as:

while the right introduction rules are: