Gödel numbering of natural deduction derivations using =Intro #417
Description
The current definition of the Gödel number of a natural deduction derivation is unclear when the =Intro rule is used. This is presented as an inference rule, not an assumption, but one with 0 premises. But the definition of the Gödel numbering assumes that natural deduction inferences have 1, 2, or 3 premises. It's therefore unclear how to code a derivation in which the =Intro rule is used.
One natural thing to do would be to set them to <0,x,n,k> where x is the Gödel number of the equation being introduced, n = 0 (since it doesn't discharge any assumptions), and k = 15 (the number of =Intro in the lookup table). This is simple, but confuses assumptions with applications of inference rules.
An alternative would be to set them to <1,y,x,n,k>, where y is the Gödel number of an empty tree, i.e. one with no subtrees and no labels, and x, n, and k are as above. This is a bit ugly, but perhaps semantically slightly more honest.
I don't have a strong view either way, although for pragmatic reasons I probably lean towards the first idea, but regardless of the decision we should clarify this. (I personally tend to think that having =Intro as a rule at all is a weakness of taking too seriously the natural deduction viewpoint that everything logical should be a rule, but that's a discussion for another day.)