Inference Rule

Abstract

An inference rule is a formal specification of how to derive a judgement from other judgements. In type theory, inference rules define the structure of valid typing derivations, specifying when terms have types and when types are well-formed.

Definition

An inference rule consists of:

• Zero or more premises (judgements that must hold)
• A single conclusion (the judgement being derived)
• Optional side conditions (constraints on variables or contexts)

The rule is written: $\frac{{\text{premise}}_1{\text{premise}}_2\cdots {\text{premise}}_n}{\text{conclusion}}$

When there are no premises, the rule is an axiom: $\frac{}{\text{conclusion}}$

In Type Theory

Type theories are presented as collections of inference rules organized into classes:

Formation Rules

Formation rules specify when a type is well-formed in a given context. $\frac{\Gamma ⊢A:\mathcal{U}\Gamma ,x:A⊢B:\mathcal{U}}{\Gamma ⊢\Pi x:A.B:\mathcal{U}}$ This rule states that $\Pi x:A.B$ is a well-formed type if $A$ is a type and $B$ is a type depending on $x:A$.

Introduction Rules

Introduction rules specify how to construct elements of a type (constructors). $\frac{\Gamma ,x:A⊢b:B}{\Gamma ⊢\lambda x.b:\Pi x:A.B}$ This introduces a function via lambda abstraction.

Elimination Rules

Elimination rules specify how to use elements of a type (destructors). $\frac{\Gamma ⊢f:\Pi x:A.B\Gamma ⊢a:A}{\Gamma ⊢fa:B[x:=a]}$ This eliminates a function via application.

Computation Rules

Computation rules (or $\beta$-rules) specify how eliminators compute on constructors. $(\lambda x.b)a\equiv b[x:=a]$ This is typically written as a definitional equality rather than a judgement rule.

Eta Rules

Eta rules express extensionality principles, stating that elements are determined by their behavior under elimination. $f\equiv \lambda x.fx$

Judgements

Inference rules operate on judgements, which are statements about terms and types. Common judgements in type theory include:

• $\Gamma ⊢A:\mathcal{U}$: Type formation judgement
• $\Gamma ⊢t:A$: Typing judgement
• $\Gamma ⊢A\equiv B$: Type equality judgement
• $\Gamma ⊢t\equiv u:A$: Term equality judgement
• $\Gamma \text{ctx}$: Context well-formedness judgement

Derivation Trees

A derivation is a tree of inference rule applications showing how a judgement follows from axioms. Each node applies one inference rule, with the premises as children and the conclusion as the label.

For example, deriving $⊢\lambda x.x:\Pi A:\mathcal{U}.A\to A$: $\frac{\frac{\frac{}{⊢\mathcal{U}:\mathcal{U}}}{⊢A:\mathcal{U},A:\mathcal{U}}\frac{\frac{}{A:\mathcal{U}⊢A:\mathcal{U}}\frac{}{A:\mathcal{U}⊢A:\mathcal{U}}}{A:\mathcal{U}⊢A\to A:\mathcal{U}}}{\frac{A:\mathcal{U},x:A⊢x:A}{⊢\lambda x.x:\Pi A:\mathcal{U}.A\to A}}$

Admissibility and Derivability

An inference rule is admissible if its conclusion can be derived whenever its premises can be derived, possibly using other rules. An inference rule is derivable if it can be constructed as a sequence of existing rules.

Admissible rules preserve consistency: adding them does not change what is provable. The cut rule in sequent calculus is admissible but not derivable in cut-free systems.

Structural Rules

Structural rules govern the manipulation of contexts rather than the logical content:

• Weakening: $\frac{\Gamma ⊢t:A}{\Gamma ,x:B⊢t:A}$ (unused variables can be added)
• Exchange: Permuting variables in the context
• Contraction: Using a variable multiple times

Substructural logics restrict these rules to model resource-sensitive reasoning.

Related Concepts

• Judgement: Statements that inference rules derive
• Type Theory: Formal systems defined by inference rules
• Natural Deduction: Proof system organized by introduction and elimination
• Curry-Howard Correspondence: Inference rules as type system specifications
• Derivable (proof theory): Property of rules constructible from existing rules
• Context: Environment of variable assumptions
• Substitution: Operation appearing in premises and side conditions
• Computation Rule: Rules specifying definitional equality