Thursday, December 28, 2006

Naturally deducing an addendum

In my previous post I said that Prawitz included forall intro in his deduction rules rather than his inference rules but I couldn't remember why. I looked at his book again and it makes sense now. The forall-intro is a deduction rule for the following reason. While it has the form of an inference from A to \forall x A, there is something left implicit in the rule. The premiss A must be obtained from a deduction, that is one cannot assume A and then infer \forall x A, i.e. A can't be an undischarged hypothesis. (This happened to be my favorite mistake to make in doing natural deduction proofs.) If one could do this then one could obtain A->\forall x A, for arbitrary A, but this doesn't hold in general. E.g. you'd get if x is 0, then for all x, x is 0. I'm not sure why it wasn't built into the formulation of the natural deduction rule for forall-intro that the premiss be the conclusion of a deduction, but this is explicit when the specific deduction rule formulation is given.

No comments: