This question is primarily concerned with the construction of formal systems, what are the necessary assumptions in the meta-theory, and notions of a priori vs a posteriori existence of generative procedures.
Suppose that we are working within the meta-theory consisting of natural language and basic primitive notions dependent upon the philosophical stance taken.
1) Must we necessarily assume that any notion we use to build our formal system, namely a collection of object variables/formal symbols and strings of symbols exist a priori in the meta-theory? Are we necessarily working within a fixed meta-theory background?
2) Often, to accommodate various finitist stances, one builds procedures within a formal system to allow the user to generate on demand, new symbols as object variables. To what extent, must the output strings of these generative procedures exist in the meta-theory a priori? This seems like it could not be true, otherwise one would necessarily have infinitely many symbols in the meta-theory to begin with.
3) Can the notions of "working within a theory/formal system" and having a "procedure to generate object variables on demand" be made more precise? In other words, is it up to interpretation whether we allow the user to truly generate new strings with an algorithm or are they only allowed to use pre-existing objects built into the system?