Question

I read in Proofs and Types by Girard et alii. the following excerpt that talks about the calculus of natural deduction:

Now a sentence at a leaf (of the deduction tree) can be dead, when it no longer plays an active part in the proof. Dead sentences are obtained by killing live ones. The typical example is the $\implies$-introduction rule:

$$ \dfrac{\stackrel{[A]}{\stackrel{\vdots}{B}}}{A \implies B} $$

It must be understood thus: starting from a deduction of B, in which we choose a certain number of occurrences of $A$ as hypotheses (the number is arbitrary: 0,1,250,$\ldots$), we form a new deduction of which the conclusion is $A \implies B$, but in which all these occurrences of $A$ have been dicharged, ie. killed. There may be other occurrences of $A$ which we have chosen not to discharge.

This rule illustrates very well the illusion of the tree-like notation: it is of critical importance to know when a hypothesis was discharged, and so it is essential to record this. But if we do this in the exmaple above, this means we have to link the crossed A with the line of the $\implies$I rule; but it is no longer a genuine tree we are considering.

May I ask you for an explanation and example of this situation?

No correct solution

Licensed under: CC-BY-SA with attribution
Not affiliated with cs.stackexchange
scroll top