Metatheory-Object Theory Distinction

Definition

A metatheory is a theory that takes another formal system, called the object theory, as its subject of study. While the object theory consists of formal symbols and rules for manipulating them, the metatheory is the framework used to describe, analyze, and prove properties about those rules.

In type theory, the distinction is central:

• Object Theory: The formal language (e.g., MLTT or lambda calculus) consisting of terms, types, and derivation rules.
• Metatheory: The mathematical environment (often informal mathematics or a stronger logic) where we prove that the object theory is consistent, has the normalization property, or satisfies decidability of type-checking.

Metatheoretic Concepts

• judgements: Assertions made in the metatheory about the object theory. For example, $\Gamma ⊢a:A$ is a metatheoretic statement that $a$ is a term of type $A$ in the context $\Gamma$.
• Admissible Rules: Rules that are not explicitly part of the object theory’s definition but can be shown to hold in the metatheory (e.g., substitution or Weakening in many systems).
• Properties:
  • Consistency: The proof that there is no term $t:\perp$ in the empty context.
  • Canonicity: The proof that every closed term of a type evaluates to a constructor.
  • Strong Normalization: The proof that every sequence of reductions terminates.

Relation to Definitional Equality

Definitional equality is a metatheoretic relation. When we say $a\equiv b$, we are not making a claim inside the type theory (which would be a propositional equality type), but rather stating a fact about how the object theory’s terms behave under the reduction rules defined in the metatheory.

References

kleene1952-metamathematics troelstra2000-proof-theory hott2013-book