Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
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.)
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$.
It is the case when B is not derived from any previous rule/axiom; that is, B is an axiom/tautology itself.
