Inductive definitions are indispensable tool in the study of PL, so we develop the basic framework thereof and give some concrete examples of their use. Put it simplier, an inductive definition consists of a set of rules for deriving judgements, or assertions, of a variety of formed. Judgements are statements about one or more abstract binding trees of some sort, whereas rules specify necessary and sufficient conditions ofr the validity of a judgment, hence fully determining its meaning.

Judgements

Some examples:

• $n \quad \sf nat$: $n$ is a natural number.
• $n_1 + n_2 = n$.
• $\tau \quad \sf type$: $\tau$ is a type.
• $e:\tau$: expression $e$ has type $\tau$.
• $e \Downarrow v$: expression $e$ has value $v$.

Note that the property or relation itself is called a judgement form, which is also named predicate, and the judgement that an object or objects have that proerpty or stand in that relation is called the instance thereof, or subjects in the predicate.

Inference Rules

An inductive definition of a judgement form consists a collection of rules of the form

$$ \underline{J_1 \cdots J_k}\\ J $$

The rule set $J_1,\cdots J_k$ is called premise, and the rule being derived is called conclusion. If a rule does not have premise, then it is an axiom; otherwise it is called proper rule. A caveat is that this only defines the sufficient condition for $J$ to be held.

A Simple Example of Natural Numbers

Natural numbers are defined recursively in Peano’s axiom system, it says:

$$ \underline{\qquad\qquad} \\ 0 \quad \sf nat $$

and

$$ \underline{a \quad \sf nat}\\ \mathsf{succ}(a)\quad \sf nat $$

A collection of rules is considered to define the strongest judgement form that is closed under, or respects, those rules. Closed means that the rules are sufficient to show the validity of the judgement: $J$ holds if there is a way to obtain it using the given rules. Strongest means that the previous judgement holds vice versa.

Derivations