Induction for finite languages is trivial. We simply use the Domain Closure rule of inference. For a language with object constants σ1, ... , σn, the rule is written as shown below. If we believe a schema is true for every instance, then we can infer a universally quantified version of that schema.
Recall that, in our formalization of the Sorority World, we have just four constants - abby, bess, cody, and dana. For this language, we would have the following Domain Closure rule.
Domain Closure (DC)
The following proof shows how we can use this rule to derive an inductive conclusion. Given the premises we considered earlier in this book, it is possible to infer that Abby likes someone, Bess likes someone, Cody likes someone, and Dana likes someone. Taking these conclusions as premises and using our Domain Closure rule, we can then derive the inductive conclusion ∀x.∃y.likes(x,y), i.e. everybody likes somebody.
Domain Closure: 1, 2, 3, 4
Unfortunately, this technique does not work when there are infinitely many ground terms. Suppose, for example, we have a language with ground terms σ1, σ2, ... A direct generalization of the Domain Closure rule is shown below.
This rule is sound in the sense that the conclusion of the rule is logically entailed by the premises of the rule. However, it does not help us produce a proof of this conclusion. To use the rule, we would need to prove all of the rule's premises. Unfortunately, there are infinitely many premises. So, the rule cannot be used in generating a finite proof.
All is not lost. It is sometimes possible to write rules that cover all instances without enumerating them individually. The method depends on the structure of the language. The next sections describe how this can be done for languages with different structures.