More precise definition of derivations in natural deduction

The current definition of a derivation of a sentence !A from a set of assumptions \Gamma in natural deduction is a tree of sentences in which the bottommost sentence is !A, the topmost sentences are in \Gamma or are discharged by an application of a rule, and every sentence in the tree apart from the conclusion is a premise of a correct application of an inference whose conclusion stands immediately below that sentence in the tree.

Unless I'm missing something, this does not appear to rule out infinite derivations. Definitions of the set of derivations in other standard textbooks, e.g. van Dalen's Logic and Structure, use an inductive definition to ensure the finiteness of definitions. I propose that we do the same, and make explicit the fact that this implies that all derivations are finite. This would thereby fix a hole in the proof that the derivability relation is compact, which makes explicit and essential use of the fact that derivations are finite. It's also implicitly used when we arithmetize derivations.

If this sounds like a reasonable idea then I'm happy to put together a patch with a proposed solution. Obviously it's important to preserve the virtues of the current definition, namely its approachability and relative informality.

Any changes would (I think) be restricted to content/first-order-logic/natural-deduction/derivations.tex, although the effects of the correction would be felt in other places where the proposition that the derivability relation is compact is used.

Start with content/first-order-logic/natural-deduction/derivations.tex and read the current definition of derivations and the proof of compactness. Check where finiteness is used, including the arithmetization discussion. Done means the definition explicitly ensures finite derivations while preserving its approachable presentation, with the affected uses remaining correct.