<p>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 "<a href="http://plato.stanford.edu/entries/logic-relevance/">relevance logic</a>", 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 <strong>weakening</strong>. Reconsidering other structural rules/axioms leads more generally to <a href="http://plato.stanford.edu/entries/logic-substructural/">substructural logics</a>, which have found applications in linguistics and theoretical computer science.  (One important example, linear logic, is mentioned in the appendix to Proofs and Types.)</p>

CC BY-SA 2.5
2011-02-01T13:58:33.193Z
2011-02-01T13:58:33.193Z
Noam Zeilberger
<p>Think about the hypothesis: <em>It rains in Belgium</em>. This is true. Assume that the proof of this fact does not contain the assumption <em>Cows eat grass</em>. What the $\to$ introduction rule states is that I can nonetheless conclude <em>Cows eat grass</em> $\to$ <em>It rains in Belgium</em>. Classically, this is true whether or not <em>Cows eat grass</em> is true. Constructively, if I have a proof of <em>Cows eat grass</em>, I can simply throw it away and return the previous proof of <em>It rains in Belgium</em>, as implicitly this is what the meaning of $A\to B$ is: it takes proofs of $A$ and converts them into proofs of $B$.</p>

CC BY-SA 2.5
2011-02-01T18:55:32.360Z
I checked on the web. It's not raining in Belgium.
Andrej Bauer
CC BY-SA 2.5
2011-02-01T19:42:43.767Z
@Andrej: Logic or no logic. The web's wrong. It was raining when I came home and it's raining now. I dare not say that it's always raining, lest we venture into modal territory.
Dave Clarke
CC BY-SA 2.5
2011-02-01T13:37:24.257Z
2011-02-01T13:51:11.733Z
2011-02-01T13:51:11.733Z
Dave Clarke
<p>It is the case when B is not derived from any previous rule/axiom; that is, B is an axiom/tautology itself.</p>

CC BY-SA 3.0
2012-09-06T20:28:59.113Z
this is not correct.
Kaveh
CC BY-SA 2.5
2011-02-01T13:34:08.827Z
2011-02-01T13:34:08.827Z
Sadeq Dousti
<p>I have a question about page 9 in <a href="http://www.paultaylor.eu/stable/prot.pdf">Proofs and Types</a>.</p>

<p>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$?</p>

CC BY-SA 2.5
2011-02-01T14:32:26.033Z
Is this a research-level question (I believe it's not)?
Oleksandr Bondarenko
CC BY-SA 2.5
2011-02-01T15:04:45.477Z
Not really, but the connection with relevance logic that this question unwittingly hints at is certainly interesting, albeit also known.
Dave Clarke
CC BY-SA 2.5
2011-02-01T16:44:20.340Z
this is why we need theory B experts here :)
Suresh Venkat
<lo.logic><natural-deduction>
Discharged hypotheses in ->Introduction
brooksbp
# Discharged hypotheses in ->Introduction

(Asked by: username_0 on 2011-02-01)

I have a question about page 9 in [Proofs and Types](http://www.paultaylor.eu/stable/prot.pdf).

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

**Tags:** lo.logic, natural-deduction
> **Comments:**
> **username_1**: Is this a research-level question (I believe it's not)?  
> **username_2**: Not really, but the connection with relevance logic that this question unwittingly hints at is certainly interesting, albeit also known.  
> **username_3**: this is why we need theory B experts here :)  

---

## 3 answers

### Answer by username_4 on 2011-02-01. Score: 21

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](http://plato.stanford.edu/entries/logic-relevance/)", 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](http://plato.stanford.edu/entries/logic-substructural/), which have found applications in linguistics and theoretical computer science. (One important example, linear logic, is mentioned in the appendix to Proofs and Types.)


---

### Answer by username_2 on 2011-02-01. Score: 20

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$.

> **Comments:**
> **username_5**: I checked on the web. It's not raining in Belgium.  
> **username_2**: @Andrej: Logic or no logic. The web's wrong. It was raining when I came home and it's raining now. I dare not say that it's always raining, lest we venture into modal territory.  

---

### Answer by username_6 on 2011-02-01. Score: 0

It is the case when B is not derived from any previous rule/axiom; that is, B is an axiom/tautology itself.

> **Comments:**
> **username_7**: this is not correct.  

---

