Discharged hypotheses in ->Introduction I have a question about page 9 in Proofs and Types.

The given $\rightarrow$Introduction rule says that $A \rightarrow B$ can be deduced from $B$ if the deduction of $B$ contains an arbitrary number of $A$s (0 or more).  How can this be true if there are zero $A$s in the deduction of $B$?
Dave Clarke's answer basically says it all: this is the standard convention in classical and constructive mathematics.  Nonetheless, your objection is the source of a century-old subdiscipline of philosophical logic called "relevance logic", which can be seen as rejecting the axiom p → (q → p) -- or in terms of natural deduction, rejecting precisely this ability to use a hypothesis zero times, or equivalently in terms of sequent calculus, rejecting the structural rule of weakening. Reconsidering other structural rules/axioms leads more generally to substructural logics, which have found applications in linguistics and theoretical computer science.  (One important example, linear logic, is mentioned in the appendix to Proofs and Types.)