 Gentzen (1934) remarked that the introduction rules were like definitions of the logical operators, and that the elimination rules were consequences of their definitions. Making this remark precise is not easy, but it has an intuitive plausibility. In the paradigmatically simple case of conjunction, the premises needed for an application of \(\land\)-I are simply the two conjuncts, so the rule can be seen as “defining” a conjunction to be true in the case that both of its conjuncts are. In an application of \(\land\)-E, the conclusion is one of the conjuncts, and so something that has to be true if the conjunction is, supposing conjunction to be “defined” that way. For other operators it is a bit less straightforward. The required subproof for \(\rightarrow\)-I is one in which the consequent is derived from the antecedent: thought of as a definition, this says that \(A\rightarrow B\) is true just in case \(B\) is (somehow) obtainable from \(A\). The rule of \(\rightarrow\)-E can be seen as a kind of consequence: to infer \(B\) from the (major) premiss \(A\rightarrow B\) and the (minor) premiss \(A\) is to treat \(A\rightarrow B\) as licensing one to infer \(B\) when \(A\) is given. (The special rules needed for Classical logic are harder to fit into this framework, an issue we discuss further, in the context of harmony, which we introduce in  §7.)