Metavariable

A metavariable is a symbol in a meta-language used to denote a term, formula, or other syntactic construct in the object language, with the understanding that it will be replaced by a concrete expression in a later step. It is a stand‑in for something within the language being described, not a part of the language itself. Metavariables are distinguished from object-language variables, which range over elements of the domain within the language’s own rules.

In formal grammars and specification languages, metavariables appear in rules that define syntax. For example, in a Backus–Naur Form–like presentation, <expr> and <term> are metavariables that stand for any valid expression or term defined by the grammar. A rule such as <expr> ::= <expr> + <term> | <term> describes a schematic form that must be instantiated with concrete expressions, such as 3 + 4 or a + (b * c), when a specific parse is constructed.

In logic, mathematics, and metatheory, metavariables such as Φ or M are used to denote arbitrary formulas, terms, or predicates. Axiom schemas or inference rules are stated with metavariables, and instances are obtained by substituting concrete formulas or terms for those metavariables. This allows general reasoning to be carried out in a single rule or schema while permitting many concrete cases to be derived.

Metavariables thus play a central role in describing and reasoning about the structure of languages, proofs, and programs at a level above the object language, enabling generic definitions, proofs, and transformations.