In logic, a metavariable (also metalinguistic variable or syntactical variable) is a symbol or symbol string which belongs to a metalanguage and stands for elements of some object language. For instance, in the sentence
Let A and B be two sentences of a language ℒ the symbols A and B are part of the metalanguage in which the statement about the object language ℒ is formulated. John Corcoran considered 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.
See also Explicit substitution
Notes
References Corcoran, J. (2006). "Schemata: the Concept of Schema in the History of Logic" (PDF). Bulletin of Symbolic Logic. 12 (2): 219–240. doi:10.2178/bsl/1146620060. S2CID 6909703. Hunter, Geoffrey (1996) [1971]. Metalogic: An Introduction to the Metatheory of Standard First-Order Logic. University of California Press (published 1973). ISBN 9780520023567. OCLC 36312727. (accessible to patrons with print disabilities) Shoenfield, Joseph R. (2001) [1967]. Mathematical Logic (2nd ed.). A K Peters. ISBN 978-1-56881-135-2. Tennent, R. D. (2002). Specifying Software: A Hands-On Introduction. Cambridge University Press. ISBN 978-0-521-00401-5.
