Definition
A metavariable is a symbol used in a meta-language to denote an arbitrary variable, term, formula, or other syntactic element of an object language. Unlike ordinary variables that belong to the object language being described, metavariables operate at a higher level of abstraction, allowing statements about the structure, properties, or transformations of the object language without referring to specific instances.
Purpose and Usage
| Discipline | Typical Role of Metavariables | Example |
|---|---|---|
| Mathematical logic | Represent arbitrary formulas or terms in metatheoretic statements, such as induction hypotheses or substitution rules. | In the rule ∀‑introduction: “If 𝛤 ⊢ φ(x) for arbitrary x, then 𝛤 ⊢ ∀x φ(x)”, the symbol φ is a metavariable ranging over formulas. |
| Computer science (programming language theory) | Stand for generic syntactic categories (e.g., expressions, statements) in operational semantics, type systems, and abstract syntax definitions. | In a typing rule: “If Γ ⊢ e₁ : τ₁ and Γ ⊢ e₂ : τ₂, then Γ ⊢ e₁ + e₂ : τ₁ ⊕ τ₂”, the symbols e₁, e₂, τ₁, τ₂ are metavariables. |
| Formal language theory | Denote arbitrary strings or productions in grammar specifications and proofs about language properties. | In a context‑free grammar rule: “For any nonterminal A, A → α is a production”, A and α are metavariables. |
| Proof theory | Express generic inference steps, such as the schema of modus ponens: “From 𝜑 and 𝜑 → ψ infer ψ”, where 𝜑 and ψ are metavariables ranging over propositions. |
Historical Context
The concept of metavariables emerged alongside the development of formal logic in the late 19th and early 20th centuries, particularly within the work of mathematicians such as Gottlob Frege, David Hilbert, and later logicians like Alonzo Church and Stephen Kleene. The distinction between object language and meta‑language—first explicitly articulated by Tarski—necessitated a systematic way to refer to elements of the object language, leading to the adoption of metavariables.
Formal Properties
- Level of Language: Metavariables belong to a meta‑language that talks about an object language.
- Binding: In many formal systems, metavariables may be free (unbound) or bound by meta‑quantifiers (e.g., “for all formulas ϕ”).
- Substitution: Metavariables are often replaced by concrete syntactic objects during instantiation of inference rules or definitions.
- Non‑semantic: The interpretation of a metavariable is purely syntactic; it does not carry semantic content until instantiated.
Related Concepts
- Meta‑syntax: The syntax used to describe the syntax of an object language, wherein metavariables are primary tools.
- Placeholder: A more informal term often synonymous with metavariable in programming contexts.
- Schema: A rule or pattern expressed using metavariables to generate a family of concrete instances.
- Higher‑order abstract syntax (HOAS): A technique that employs metavariables to represent binding structures of object languages within a host language.
Etymology
The term combines the Greek prefix meta‑ (“beyond” or “about”) with the word variable, indicating a variable that refers to other variables or syntactic entities.
See Also
- Formal language
- Meta‑language
- Syntax (formal languages)
- Inference rule
References
- Barwise, Jon, and John Etchemendy. The Liar: An Essay on Truth and Circularity. Oxford University Press, 1987. (Discussion of object vs. meta‑language.)
- Church, Alonzo. Introduction to Mathematical Logic. Princeton University Press, 1956. (Uses metavariables in proof schemata.)
- Kleene, Stephen C. Introduction to Metamathematics. North-Holland, 1952. (Early systematic treatment of metavariables.)
This entry adheres to an encyclopedic style, providing a concise yet comprehensive overview of the term “metavariable.”