 Now, as Gerhard Gentzen observed, when we come to formulate similarly compelling principles for introducing and eliminating the other connectives, we find ourselves having to make reference to the discharging of assumptions temporarily made for the sake of argument. Such is the case for instance with formulating an introduction rule for → and with formulating an elimination rule for ∨. In the case of the former rule, for example, Gentzen took it that the way to derive φ → ψ is to assume φ and use the various rules and other assumptions to derive ψ, at which point the rule (also called Conditional Proof) allows us to claim that we have derived φ → ψ from the remaining assumptions, without having to record this conclusion as depending on φ (as ψ itself did before the rule was applied). Thus to extend the present approach, known as natural deduction, from ∧ to these and other connectives, it is necessary to keep track not only of what formulas we are dealing with at a given stage but also of the set of initial formulas, or assumptions, on which that formula depends. We want to say, in the case of the rule just described, that it entitles us to pass from ψ, as depending on Γ ∪ {φ}, to φ → ψ, as depending on Γ. The ordered pair of a finite set of formulas and an individual formula, ⟨Γ, φ⟩ whose first entry records the set of formulas on which its second entry depends, we write in the more suggestive notation Γ ≻ φ, and call a sequent, or more explicitly, a sequent of the logical framework Set-Fmla. For the variant framework Set-Fmla0, we allow also the case in which there is no formula to the right of the “≻”. Some principles for reasoning about sequents which do not involve any specific connectives and were called by Gentzen, structural rules (as opposed to operational rules) are the following, which are respectively a zero-premiss, a one-premiss and a two-premiss sequent-to-sequent rule: