Metavariables

Metavariables are placeholders used at the meta level of a formal system to denote objects that are not fixed in advance. They differ from object-level variables, which range over elements of the domain being studied. Metavariables can stand for formulas, terms, types, or syntactic constructs, enabling reasoning about patterns, schemas, and general rules without committing to specific instances.

In logic and formal languages, metavariables appear in schemas and in the description of inference rules. They allow statements such as “for any formula F, if F is provable then …” to be expressed without choosing a particular F. This use supports meta-theoretic discussions, such as substitution schemas, induction principles, and structural properties of the object language.

In grammars and specification languages, metavariables denote placeholder syntactic categories or templates that will later be instantiated by concrete strings or symbols. In type theory and proof assistants, metavariables often appear as holes or placeholders during interactive development. They guide type inference and term construction, with the system attempting to fill them through a process related to unification or constraint solving.

Commonly, the practice of working with metavariables involves solving for their instantiations to obtain a complete, fully concrete object-language expression. Metavariables thus facilitate general reasoning, meta-level analysis, and automated or semi-automated construction of proofs, programs, and syntactic definitions, while requiring careful handling to avoid ambiguity or circularity.