Set-theoretic foundations for formal language theory? Has anyone ever seen any papers or books including set-theoretic descriptions of formal language theory? Specifically, I'm interested in how one would formalize context-free grammars with sets.
Some of this, I suppose is fairly obvious. For example, strings would use a foundational formalism much like ordered pairs (e.g.  Kuratowski's definition or similar) but what about objects like production rules and their semantics?
This isn't really necessary for me to get any actual work done, I just thought it would help me build a better intuition around formal language theory.
Thanks in advance,


*

*Anthony


Update:
An example of what I'm looking for would be string concatenation. How would one construct this in pure set theroy? If we consider the strings "a" and "b", and consider their set representations to be { { a } } and { { b }} (as per Kuratowski), then the desired result would be { { a }, { a, b } }. Clearly this cannot be accomplished by a defining string concatenation to be set union but there are obviously numerous ways of doing so. The choice at each point in defining how to do something in formal language theory using pure set theory will, in some cases, determine how other notions can be defined. As a consequence, some definitions may be more complex than others (or less elegant than others, one might say). I'm just curious if anyone has done anything like this before. 
 A: One can do this using less technology, too...
Let $\Sigma$ be an alphabet, $N$ a set of non-terminals, and $\Sigma^\*$ and $(\Sigma\cup N)^\*$ the full languages on $\Sigma$ and $\Sigma\cup N$, respectively. A context-free grammar is a finite subset $G\subset N\times(\Sigma\cup N)^\*$. Given one such grammar $G$ there is a relation $\mathord\rightarrow_G\subseteq(\Sigma\cup N)^\*\times(\Sigma\cup N)^\*$ which is the least transitive reflexive relation which contains $G$ (notice that $N\times(\Sigma\cup N)^\*\subseteq (\Sigma\cup N)^\*\times(\Sigma\cup N)^\*$, so this makes sense) and such that
$$a\rightarrow_Gb \wedge a'\rightarrow_Gb'\implies ab\rightarrow_Ga'b'.$$ The language generated by $G$ from a non-terminal $n\in N$ is just $L(G, n)=\{w\in \Sigma^\*:n\rightarrow_Gw\}$. This is, in fact, the standard way to do this...
A: Hi Anthony, 
The question you're asking in your text isn't quite the same as the question in your title, but the answer to the title subsumes the one you ask in the text. 
To define a grammar, we start with a an alphabet $\Sigma$, and a set of nonterminal variable $N$, and then define a grammatical expression as an element of the formal semiring $G$ over $\Sigma + N$. (It's a good exercise to see how the semiring axioms let you convert grammatical expressions into their Backus normal form.) Next, a grammar is a map from $N \to G$ -- that is, it assigns a grammatical expression to each variable. 
Now, consider the free monoid over $\Sigma$. Concretely, these are sequences of characters in $\Sigma$. A language is a set of these strings, and our goal is to give an interpretion sending nonterminals to languages. If we had a map $f$ sending nonterminals to languages, we could interpret grammatical expressions inductively, by interpreting the formal multiplication in the ring as concatenation (using the monoid operation) of elements in each language, and interpreting the formal sum as set union of languages. 
Now, consider the free monoid over $\Sigma$. Concretely, these are sequences of characters in $\Sigma$. A language is a set of these strings (ie, an element of $\mathcal{P}(\Sigma^{*})$), and our goal is to give an interpretion sending nonterminals to languages. If we had a map $f$ sending nonterminals to languages, we could interpret grammatical expressions inductively, by interpreting the formal multiplication in the ring as concatenation (using the monoid operation) of elements in each language, and interpreting the formal sum as set union of languages. 
If we have such an interpretation (a function $N \to \mathcal{P}(\Sigma^{*})$) and a grammar (a map $N \to G$), we can lift the grammar to an endofunction on interpretations -- that is, to a function $(N \to L) \to (N \to L)$. (I'm using $L$ for a set of strings due to jsMath flakiness -- it should be powerset-sigma-star.) 
The language for each nonterminal will be the least fixed point of this functional. (As a technical detail, to make this functional monotone, so that the Knaster-Tarski theorem applies, you need to ensure that each interpretation also unions the new language with the old argument language -- ie, you take an interpretation $i$ sketched above and change it to $\lambda f.\;\lambda n.\; f(n) \cup i(n)$.) 
I should also add that this is all standard material, which should appear in every textbook on formal language theory. (I'm pretty sure it's in Sipser.) 
A: For the foundations of formal language theory, the following ideas show up: 


*

*Universal algebra (here for 'free' monoids and basic logic involving simple equation only proofs, just variables and no connectives or quantifiers)

*Term rewriting systems (take a look at the wikipedia article)
As for foundations, I have found that much FOM (Foundations of Mathematics) is done assuming full blown ZFC set theory.  You can certainly think of formal language theory, computability theory, model theory, etc... as subjects in ZFC just like any other subject such as abstract algebra or topology/geometry.  There is no danger here as long as the context in which the results were derived is clear.
Meta-mathematical work is often done in ZFC first and then under weaker systems later.
