More precise definition of derivations in natural deduction

[beastaugh]

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.

[rzach]

This is a great point. One thing though: that section is used first of all by students who come to proofs in natural deduction (Gentzen-style) for the first time. Hitting them with an inductive definition will be a bit off-putting. I suggest we add a section at the end of the chapter that shows how (correct) derivations can be defined inductively. This section can then be left out if it doesn't match the level of the material (as compiled, eg in SLC), or can be inserted somewhere else (eg in the arithmetization of syntax chapter before the arithmetization of derivations).

We should have a parallel section for sequents (and eventually also for tableaux, although we don't show how tableaux can be arithmetized).

[rzach]

(The problem with infinite derivations can be fixed simply by requiring that the tree is finite.)

[beastaugh]

Adding a new section with the inductive definition sounds like a good compromise: I very much agree that we don't want to scare off the students. I'll start working something up for natural deduction, and if that looks reasonable then I can perhaps add the other proof systems too.

Simply adding the requirement that the tree is finite is what I did when I was teaching this last term, so I'm happy with that as a fix for the current section. :)

[rzach]

I've added "finite" to the definitions.