Recursive definitions in formal logic

Question

A binary tree $T$ is either

1. A single vertex, or
2. A graph formed by taking two binary trees, adding a vertex, and adding an edge directed from the new vertex to the root of each binary tree.

Suppose we want to formalize the recursive definition of a binary tree in formal logic, and justify using structural induction on it. How would we go about doing it normally?

I'm thinking about using the same method for the construction of the naturals (please correct me if there is a better or more standard way to do this). That is,

$$ \forall T. BTree(T) \iff T \in \bigcap \{S \subseteq GRAPHS: K_1 \in S \land (T_1 \in S \land T_2 \in S \implies MakeTreeWithRoot(T_1,T_2) \in S)\}$$

First, how do we know that the intersection is non-empty? Second, suppose we know that. Then we know that $$ BTree(K_1) $$ and $$ \forall T_1, T_2. BTree(T_1) \land BTree(T_2) \implies BTree(MakeTreeWithRoot(T_1,T_2)) $$ but how do we know that $$ \forall T_1, T_2. BTree(MakeTreeWithRoot(T_1,T_2)) \implies BTree(T_1) \land BTree(T_2)? $$

Third, how would we show that the intersection set has a well-founded relation of "subtree", which allows us to perform structural induction on it? It just seems that many texts simply brush off the fact that such relations are well-founded as "obvious", but I would like to know the formal basis for this.

Answer 1

Yep, your definition is the right way to do this. The collection of sets you are intersecting is nonempty, since it trivally contains (for instance) the set of all finite graphs. To prove $$\forall T_1, T_2. BTree(MakeTreeWithRoot(T_1,T_2)) \implies BTree(T_1) \land BTree(T_2),$$ you can use "induction", which really just means directly using the definition of $BTree$: let $S$ be the set of binary trees $T$ such that if $T_1$ and $T_2$ are graphs such that $T=MakeTreeWithRoot(T_1,T_2)$, then $T_1$ and $T_2$ are also binary trees. Prove that $S$ contains $K_1$ and is closed under $MakeTreeWithRoot$, and you can conclude it contains all binary trees.

I am not sure exactly what you want "subtree" to mean, but whatever it means, well-foundedness of the relation "subtree" will be very easy, because every binary tree has a finite set of vertices (prove this by induction as in the previous paragraph) and a proper subtree (for any reasonable definition) has a strictly smaller number of vertices. So since the ordering on $\mathbb{N}$ is well-founded, so is the subtree order.