7
$\begingroup$

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

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

3 Answers 3

21
$\begingroup$

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

$\endgroup$
0
20
$\begingroup$

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

$\endgroup$
2
  • 17
    $\begingroup$ I checked on the web. It's not raining in Belgium. $\endgroup$ Feb 1, 2011 at 18:55
  • 3
    $\begingroup$ @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. $\endgroup$ Feb 1, 2011 at 19:42
0
$\begingroup$

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

$\endgroup$
1
  • $\begingroup$ this is not correct. $\endgroup$
    – Kaveh
    Sep 6, 2012 at 20:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.