For a long time I have been interested in the idea of computationally
enumerating every possible expression of a formal theory.
Who hasn't! :) As one with a background in linguistics, I am sure you will appreciate the distinction syntax/semantics, which is very relevant to mathematical and formal logic, too: formal statements and even, with some caution, their provability, is a syntactic/formal notion, while the truth of statements, i.e. theoremhood, is a semantic one, and not subordinate to provability.
Another distinction that is crucial is first-order vs higher-order theories: standard ZF(C) is a first-order theory, though already a very strong one relatively speaking, indeed first-order is the much weaker arithmetic system in Goedel's incompleteness theorem. And we are usually (mostly?) interested in first-order theories because these are the ones that can be effectively implemented say in a real computer: with higher-order we can only implement higher-order symbolic computation.
In particular, you may want to look at two fundamental results to begin with:
Goedel's incompleteness theorem: where Goedel constructs a statement of plain natural number arithmetic (PM is the underlying theory there), that is not provable from the axioms and rules of inference, despite at a meta-level we conclude the the statement must be true, whence it is indeed unprovable: notice in particular the distinction between a mathematical notion being expressible in the language/system (we can say it in that system) and the corresponding statement being provable in that system (we can derive it).
Tarski's undefinability theorem, about the undefinability of arithmetic truth in arithmetic itself, still about first-order theories in particular.
And I won't say much at all about semantics, that's an even tougher topic, except for mentioning two keywords here: proof theory, and model theory:
That much for a very quick intro, now back to "enumerating every possible expression", at least two cautions there: 1) despite there is some sense to doing such an operation up to the notion of "cumulative hierarchy", incompleteness means you are never going to enumerate them all (more precisely: no effective procedure exists that can systematically enumerate all and only the valid formulas of any such system: which is incompleteness and, under another form, the halting problem); and, 2) you'd still be enumerating syntactic constructs only, namely, formulae: whether those correspond to "sets" or anything else is not per se a syntactic thing...
I am sure much more could be said and I am also sure I have botched some details, I am more of a symbolic/abstract/natural language logician (a la P.F. Strawson, see Introduction to Logical Theory, a wonderful book and intro to the subject IMO) than any expert in mathematical or even formal logic: so I am myself more of a student here, sharing notes and hoping some teacher might jump on this and correct us both. :)