Tree Induction

Tree languages are a superset of linear languages. While in linear languages the terms in the language form a linear sequence, in tree languages the structure is more tree-like. Consider a language with an object constant a and two unary function constants f and g. Some of the terms in this language are shown below.

As with linear languages, we can write an inductive rule of inference for tree languages. The tree induction rule of inference for the language just described is shown below. Suppose we know that a schema φ holds of a. Suppose we know that, whenever the schema holds of any element, it holds of the term formed by applying f to that element. And suppose we know that, whenever the schema holds of any element, it holds of the term formed by applying g to that element. Then, we can conclude that the schema holds of every element.

In order to see an example of tree induction in action, consider the ancestry tree for a particular dog. We use the object constant rex to refer to the dog; we use the unary function constant f to map an arbitrary dog to its father; and we use g map a dog to its mother. Finally, we have a single unary relation constant purebred that is true of a dog if and only if it is purebred.

Now, we write down the fundamental rule of dog breeding - we know that, if a dog is purebred, then both its father and its mother must be purebred as well. See below. (This is a bit oversimplified on several grounds. Properly, the father and mother should be of the same breed. Also, this formalization suggests that every dog has an ancestry tree that stretches back without end. However, let's ignore these imperfections for the purposes of our example.)

Suppose now that we discover the fact that our dog rex is purebred. Then, we know that every dog in his ancestry tree must be purebred. We can prove this by a simple application of tree induction.

A proof of our conclusion is shown below. We start with the premise that Rex is purebred. We also have our constraint on purebred animals as a premise. We use Universal Elimination to instantiate the second premise with placeholder [c]. We then assume purebred([c]). We use Implication Elimination to derive the conjunction on line 5, and then we use And Elimination to pick out the first conjunct. We use Implication Introduction to discharge our assumption, and we Universal Introduction to produce the inductive case for f. We then repeat this process to produce an analogous result for g on line 13. Finally, we use the tree induction rule on the sentences on lines 1, 8, and 13 and thereby derive the desired overall conclusion.