# 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

• `F` satisfies (1) and (2), and
• if `X⊆N` also satisfies (1) and (2) then `F⊆X`.

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

An alternative way of writing a rule is

```	hypothesis
----------
conclusion
```

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

```	----
0∈F

n∈F
-------
f(n)∈F
```

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

```	   x1∈S, ..., xn∈S
R:-----------------
x∈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
R:---------------------
x∈Si
```

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

## Example

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:

• variables: `v0`, `v1`, `v2`, ...,
• abstractor: `λ`,
• parentheses and dot: `(`, `)`, `.`.

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

```
Variable: ------
vi∈Λ

Abstraction:   M∈Λ
---------
λvi.M∈Λ

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

```

## Proofs

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

• `x∈Si` is the last entry in the list, i.e., the conclusion of the proof, and
• each element of the list `xj∈Sij` is the conclusion of a rule in `R` all of whose hypotheses occur in the list before `xj∈Sij`.

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)]

## References

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