A statement like the following: "the set `F⊆N`

of natural numbers is the least set of natural numbers satisfying

`0∈F`

, and`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

x_{1}∈S, ..., x_{n}∈S R:----------------- x∈S

The hypothesis is specified by the finite subset `{x`

.
The conclusion is specified by an element _{1}, ..., x_{n}}∈X`x∈X`

.
The subset `S⊆X`

is closed under the rule
`R`

if `x∈S`

whenever, `x`

, ..., _{1}∈S`x`

.
_{n}∈S

A subset `S`

of a set `X`

is inductively defined by a collection of rules `R`

if

`S`

is closed under each rule in`R`

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

and _{1}`S`

which satisfy (1) and (2) above.
In this case _{2}`S`

and _{1}⊆S_{2}`S`

, so
_{2}⊆S_{1}`S`

.
_{1}=S_{2}

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`

.

Given sets `X`

, ..., _{1}`X`

,
the subsets _{k}`S`

, ..., _{1}⊆X_{1}`S`

are inductively defined by a set of rules of the form
_{k}⊆X_{k}

x_{1}∈S_{i1}, ..., x_{n}∈S_{in}R:--------------------- x∈S_{i}

where `i`

, `i`

, ..., _{1}`i`

,
_{n}∈{1, ...,k}`x∈X`

and _{i}`x`

,
...,_{1}∈X_{i1}`x`

,
provided
_{n}∈X_{in}

`S`

, ...,_{1}`S`

are closed under each of the rules, and_{k}- if
`S'`

, ...,_{1}`S'`

are also subsets of_{k}`X`

, ...,_{1}`X`

and are closed under the rules, then_{k}`S`

, ...,_{1}⊆S'_{1}`S`

._{k}⊆S_{k}

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:
`v`

,_{0}`v`

,_{1}`v`

, ...,_{2} - abstractor:
`λ`

, - parentheses and dot:
`(`

,`)`

,`.`

.

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

, as follows
^{*}

Variable: ------ v_{i}∈Λ Abstraction: M∈Λ --------- λv_{i}.M∈Λ Application: M∈Λ, N∈Λ --------- (M N)∈Λ

Suppose we have subsets `S`

, ...,_{1}⊆X_{1}`S`

which are inductively defined by a set of rules _{k}⊆X_{k}`R`

.
A proof that `x∈S`

is a finite non-empty list:
_{i}

x_{1}∈S_{i1}, ..., x_{n}∈S_{in}

such that

`x∈S`

is the last entry in the list, i.e., the conclusion of the proof, and_{i}- each element of the list
`x`

is the conclusion of a rule in_{j}∈S_{ij}`R`

all of whose hypotheses occur in the list before`x`

._{j}∈S_{ij}

Proofs can be drawn as trees or written as lists. As an example here is a proof in list form of
the claim that `λv`

:
_{1}λ.v_{2}.v_{1}∈Λ

`v`

[Variable rule]_{1}∈Λ`λv`

[Abstraction rule on (1)]_{2}.v_{1}∈Λ`λv`

[Abstraction rule on (2)]_{1}λ.v_{2}.v_{1}∈Λ

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

Copyright © 2014 Barry Watson. All rights reserved.