Inductively Defined Subsets

A statement like the following: "the set F⊆N of natural numbers is the least set of natural numbers satisfying

  1. 0∈F, and
  2. n∈F⇒f(n)∈F"

means that

In this case we say that F is inductively defined by the rules (1) and (2).

An alternative way of writing a rule is


The rules (1) and (2) above could then be rewritten as:



The form for a rule which defines a subset S of a set X is

	   x1∈S, ..., xn∈S

The hypothesis is specified by the finite subset {x1, ..., xn}∈X. The conclusion is specified by an element x∈X. The subset S⊆X is closed under the rule R if x∈S whenever, x1∈S, ..., xn∈S.

A subset S of a set X is inductively defined by a collection of rules R if

  1. S is closed under each rule in R
  2. if S'⊆X is also closed under each rule in R, then S⊆S'.

Inductively defined subsets are unique. To see why, consider two subsets S1 and S2 which satisfy (1) and (2) above. In this case S1⊆S2 and S2⊆S1, so S1=S2.

We could also define S above as the intersection of all S'⊆X that are closed under each rule in R. Obviously S would also be a subset of R which is closed under each rule in R.

Simultaneously Inductively Defined Subsets

Given sets X1, ..., Xk, the subsets S1⊆X1, ..., Sk⊆Xk are inductively defined by a set of rules of the form

	   x1∈Si1, ..., xn∈Sin

where i, i1, ..., in∈{1, ...,k}, x∈Xi and x1∈Xi1, ...,xn∈Xin, provided

  1. S1, ...,Sk are closed under each of the rules, and
  2. if S'1, ...,S'k are also subsets of X1, ..., Xk and are closed under the rules, then S1⊆S'1, ...,Sk⊆Sk.


As an example of an inductively defined subset, we'll construct the set of λ-terms of the λ-calculus.

The alphabet of λ-terms, Α, is defined as follows:

We can define the set of λ-terms, Λ⊆Α*, as follows

	Variable: ------

	Abstraction:   M∈Λ

	Application: M∈Λ, N∈Λ
		      (M N)∈Λ



Suppose we have subsets S1⊆X1, ...,Sk⊆Xk which are inductively defined by a set of rules R. A proof that x∈Si is a finite non-empty list:

	x1∈Si1, ..., xn∈Sin

such that

Proofs can be drawn as trees or written as lists. As an example here is a proof in list form of the claim that λv1λ.v2.v1∈Λ:

  1. v1∈Λ [Variable rule]
  2. λv2.v1∈Λ [Abstraction rule on (1)]
  3. λv1λ.v2.v1∈Λ [Abstraction rule on (2)]


R. Burstall. Language Semantics and Implementation. Course Notes. 1994.