rzach
commented
3 months ago I'm fully in favor of defining trees, thanks for getting this started. This is a bit fast for where it appears though: we're assuming that a reader has just learned about sets and relations; defining trees as they are defined in set theory is a little much I think. For instance, we don't yet have a definition of well-order at this point. Since we only need it (so far) for proof trees, maybe a more basic, discrete definition (acyclic graph, maybe in the graph theory section itself) might be more appropriate?
I developed this section on trees for my metatheory teaching, as it's useful in teaching both natural deduction and the completeness theorem (at least for mathematicians) to have precise definitions of trees, branches etc. in the logic/set theory context. I kept it short, comparable to the section on graphs, but of course it could potentially be expanded in future.