# 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$?

• Is this a research-level question (I believe it's not)? Feb 1, 2011 at 14:32
• Not really, but the connection with relevance logic that this question unwittingly hints at is certainly interesting, albeit also known. Feb 1, 2011 at 15:04
• this is why we need theory B experts here :) Feb 1, 2011 at 16:44

Think about the hypothesis: It rains in Belgium. This is true. Assume that the proof of this fact does not contain the assumption Cows eat grass. What the $\to$ introduction rule states is that I can nonetheless conclude Cows eat grass $\to$ It rains in Belgium. Classically, this is true whether or not Cows eat grass is true. Constructively, if I have a proof of Cows eat grass, I can simply throw it away and return the previous proof of It rains in Belgium, as implicitly this is what the meaning of $A\to B$ is: it takes proofs of $A$ and converts them into proofs of $B$.