Introduction Rule

Definition

An introduction rule in Type Theory specifies how to construct or introduce elements of a given type. Introduction rules describe the canonical ways to form terms of a type.

For a type $T$, an introduction rule has the general form:

$\frac{\text{premises}}{t:T}$

where the premises specify the conditions under which we can conclude that $t$ is an element of type $T$.

Examples

Product Type Introduction

For Product Type $A\times B$:

$\frac{\Gamma ⊢a:A\Gamma ⊢b:B}{\Gamma ⊢(a,b):A\times B}$

Given elements of $A$ and $B$, we can form a pair.

Function Type Introduction

For Function Type $A\to B$:

$\frac{\Gamma ,x:A⊢e:B}{\Gamma ⊢\lambda x.e:A\to B}$

If we can derive $e:B$ under the assumption $x:A$, we can form the function $\lambda x.e$.

Sum Type

For Sum Type $A+B$:

$\frac{\Gamma ⊢a:A}{\Gamma ⊢\text{inl}(a):A+B}\frac{\Gamma ⊢b:B}{\Gamma ⊢\text{inr}(b):A+B}$

We can inject elements from either component into the sum.

Natural Numbers

For natural numbers $\mathbb{N}$:

$\frac{}{\text{zero}:\mathbb{N}}\frac{n:\mathbb{N}}{\text{succ}(n):\mathbb{N}}$

Zero is a natural number, and the successor of any natural number is a natural number.

Properties

• Introduction rules define the canonical forms of a type
• They specify how to construct elements rather than how to use them
• In proof theory, introduction rules correspond to proof construction

Related Concepts

• Elimination Rule: The dual concept for using or deconstructing elements of a type
• Computation Rule: Rules governing how elimination reduces on introduction forms
• Type Theory: The formal system in which these rules are defined
• Product Type: A type with pair introduction
• Function Type: A type with lambda abstraction introduction