Are there precise definitions for what a variable, a symbol, a name, an indeterminate, a meta-variable, and a parameter are?


In informal mathematics, they are used in a variety of ways, and often in incompatible ways. But one nevertheless gets the feeling (when reading mathematicians who are very precise) that many of these terms have subtly different semantics.


For example, an 'indeterminate' is almost always a 'dummy' in the sense that the meaning of a sentence in which it occurs is not changed in any if that indeterminate is replaced by a fresh 'name' ($\alpha$-equivalence). A parameter is usually meant to represent an arbitrary (but fixed) value of a particular 'domain'; in practice, one frequently does case-analysis over parameters when solving a parametric problem. And while a parameter is meant to represent a value, an 'indeterminate' usually does not represent anything -- unlike a variable, which is usually a placeholder for a value. But variables and parameters are nevertheless qualitatively different.


The above 2 paragraphs are meant to make the intent of my question (the first sentence of this post) more precise. I am looking for answers of the form "an X denotes a Y".



Defining variable, symbol, indeterminate and parameter
Regarding the status of variables, you probably want to look at Chung-Kil Hur's PhD thesis ["Categorical equational systems: algebraic models and equational reasoning"](http://www.pps.jussieu.fr/~gil/publications/thesis.pdf). Roughly speaking, he extends the notion of formal (as in formal polynomials) to signatures with binding structure and equations. He was a student of Fiore's, and I think they've been interested in giving better models (inspired by the nominal sets approach) to things like higher-order abstract syntax. I've been meaning to read his thesis for a while, to see if his treatment of variables can suggest techniques that could be used for writing reflective decision procedures which work over formulas with quantifiers.


For schematic variables or metavariables, there's a formal treatment of them in MJ Gabbay's (excellently-titled) paper ["One and a Halfth-Order Logic"](http://portal.acm.org/citation.cfm?id=1140359)


