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$
  • 8
    $\begingroup$ Is this a research-level question (I believe it's not)? $\endgroup$ – Oleksandr Bondarenko Feb 1 '11 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$ – Dave Clarke Feb 1 '11 at 15:04
  • 3
    $\begingroup$ this is why we need theory B experts here :) $\endgroup$ – Suresh Venkat Feb 1 '11 at 16:44
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$
19
$\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$
  • 17
    $\begingroup$ I checked on the web. It's not raining in Belgium. $\endgroup$ – Andrej Bauer Feb 1 '11 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$ – Dave Clarke Feb 1 '11 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$
  • $\begingroup$ this is not correct. $\endgroup$ – Kaveh Sep 6 '12 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.