Metavariable
In logic, a metavariable is a symbol or symbol string which belongs to a metalanguage and stands for elements of some object language. For instance, in the sentence
the symbols A and B are part of the metalanguage in which the statement about the object language ℒ is formulated.
John Corcoran considers this terminology unfortunate because it obscures the use of schemata and because such "variables" do not actually range over a domain.
The convention is that a metavariable is to be uniformly substituted with the same instance in all its appearances in a given schema. This is in contrast with nonterminal symbols in formal grammars where the nonterminals on the right of a production can be substituted by different instances.
Attempts to formalize the notion of metavariable result in some kind of type theory.