New section of the Relations chapter on trees, just after graphs.

[beastaugh]

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.

[rzach]

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?

[rzach]

I did some things see commit c2dd8a2

I think this makes the set theoretic definition easier to understand. I'm still a bit worried that it's a bit much at this point in the development (well-orders, chains, minimal elements). Maybe it's ok that it's a bit advanced if it's the closing section for the chapter. I worry that someone will think that every non-root element has exactly one predecessor and try to prove that, or worry why it's not a requirement. But at least we can say now that when we say "tree" anywhere later we can point to the example of N^* and say think of it as a finite subtree of that, with labels assigned.

What do you think @beastaugh ?