
Introduction to Logic

Tools for Thought

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 treelike. 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.




a 







↙ 

↘ 





f(a) 



g(a) 



↙ 

↘ 

↙ 

↘ 


f(f(a)) 

g(f(a)) 

f(g(a)) 

g(g(a)) 


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.
Tree Induction 
φ[a] 
∀μ.(φ[μ] ⇒ φ[f(μ)]) 
∀μ.(φ[μ] ⇒ φ[g(μ)]) 

∀ν.φ[ν] 

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 say that a dog is purebred if and only if both its father and its mother are purebred. 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.)
∀x.(purebred(x) ⇔ purebred(f(x)) ∧ purebred(g(x)))
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, and then we use Biconditional Elimination on the biconditional in line 3 to produce the implication on line 4.
1. 

purebred(rex) 

Premise 
2. 

∀x.(purebred(x) ⇔ purebred(f(x)) ∧ purebred(g(x))) 

Premise 
3. 

purebred(x) ⇔ purebred(f(x)) ∧ purebred(g(x)) 

UE: 2 
4. 

purebred(x) ⇒ purebred(f(x)) ∧ purebred(g(x)) 

BE: 3 

On line 5, we start a subproof with the assumption the x is purebred. We use Implication Elimination to derive the conjunction on line 6, and then we use And Elimination to pick out the first conjunct. We then use Implication Introduction to discharge our assumption, and we Universal Introduction to produce the inductive case for f.
5. 

purebred(x) 

Assumption 
6. 

purebred(f(x)) ∧ purebred(g(x)) 

IE: 4, 5 
7. 

purebred(f(x)) 

AE: 6 
8. 

purebred(x) ⇒ purebred(f(x)) 

II: 5, 7 
9. 

∀x.(purebred(x) ⇒ purebred(f(x))) 

UI: 8 

We then repeat this process to produce an analogous result for g on line 14.
10. 

purebred(x) 

Assumption 
11. 

purebred(f(x)) ∧ purebred(g(x)) 

IE: 4, 10 
12. 

purebred(g(x)) 

AE: 11 
13. 

purebred(x) ⇒ purebred(g(x)) 

II: 10, 12 
14. 

∀x.(purebred(x) ⇒ purebred(g(x))) 

UI: 13 

Finally, we use the tree induction rule on the sentences on lines 1, 9, and 14 and thereby derive the desired overall conclusion.
1. 

purebred(rex) 

Premise 


... 


9. 

∀x.purebred(x) ⇒ purebred(f(x)) 

UI: 8 


... 


14. 

∀x.purebred(x) ⇒ purebred(g(x)) 

UI: 13 
15. 

∀x.purebred(x) 

Ind: 1, 9, 14 

Use the arrow keys to navigate.
