
The notion of metavariable plays a fundamental role when we define formal systems such as logical and computational calculi. Yet it has been usually understood only informally as is seen in most textbooks of logic. Based on our observations of the usages of metavariables in textbooks, we propose two formal systems that have the notion of metavariable.
In both calculi, each variable is given a level (nonnegative integer), which classifies variables into object variables (level 0), metavariables (level 1), metametavariables (level 2) and so on. Then, simple arity systems are used to exclude meaningless terms like a metalevel function operating on the metametalevel. A main difference of the two calculi lies in the definitions of substitution. The first calculus uses textual substitution, which can often be found in definitions of quantified formulae: when a term is substituted for a metavariable, free objectlevel variables in the term may be captured. The second calculus is based on the observation that predicates can be regarded as metalevel functions on objectlevel terms, hence uses captureavoiding substitution.
We show both calculi enjoy a number of properties including ChurchRosser and Strong Normalization, which are indispensable when we use them as frameworks to define logical systems.
© 20022003 Kurt Gödel Society, Norbert Preining. 
20030604
 