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". Roughly speaking, he extends the notion of formal (as in forming 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"
