I started reading Karp, and there, it seems that a formula in an infintary logic is a "string" of symbols in a given alphabet having certain properties, where by "string", we mean an $\alpha$-sequence of symbols, where $\alpha$ is an ordinal. Karp goes through great pains to carefully define the concatenation of these strings, the notion of a substring, and so on.
But in Marker, after saying that the connectives, $\bigwedge$ and $\bigvee$, are in our alphabet, he goes on to say that if $X$ is a set of formulas, then
$$
\bigvee_{\phi\in X}\phi \text{ and } \bigwedge_{\phi\in X}\phi
$$
are formulas. But such an object is not even a "string" in the Karp sense. The symbols $\in$ and $X$, for instance, are not even in our alphabet. So what then are formulas, if not strings?
Looking at Keisler, I am guessing that a formula is what I might call, for lack of a better term, a "generalized string", by which I mean a finite sequence of objects, where each term in the sequence is either a symbol in our alphabet or a set of generalized strings. But if that is the case, then shouldn't more care be taken to ensure such a concept is well-defined, given the recursive nature of the definition? Also, if that is the case, then many of the notions from first-order logic, such as substring and subformula, need to be treated differently. And yet, Marker simply says, "We can inductively define the notions of free variable, subformula, sentence, theory and satisfiability in the usual ways." Finally, even if we carefully define everything, doesn't this different foundation make it difficult to cite results from Karp, since she constructs the fundamental objects in the subject in a completely different way?
Best Answer
I have answered this question to my own satisfaction and would like to post the answer. First, though, I want to say that, in hindsight, I now see that the question is both vague and poorly phrased. As a partial defense of myself, it was only through answering it that the question became clearer in my own mind.
The question, as I intended it, was something like, "What kind of objects are formulas?" As a pure mathematical question, it is trivial. They are formulas! What I had in mind was something more like, "Where do we begin in the construction?" For instance, "a formula is a [blank] such that [insert conditions]." How do we fill in that blank? And to clarify, I didn't want to fill it in with simply "set" or "sequence". In that case, my follow-up would have been, "A sequence of what?" I was looking for a starting universe of objects from which formulas are specified.
In Karp's original construction, we have an alphabet of symbols, $A$. A formula is an $\alpha$-sequence in $A$ satisfying certain conditions, where $\alpha$ is a countable ordinal. So in Karp's construction, the blank is filled in roughly by "infinite string of symbols in $A$."
In the construction suggested by Keisler, which Marker also follows, we could define formulas recursively as follows. Let $S_0$ be the set of atomic formulas from first-order logic. In particular, this means that an element of $S_0$ is a finite string of symbols in $A$. For a countable ordinal $\alpha$, let \[ S_\alpha' = S_\alpha \cup \{ \langle \neg, \varphi \rangle \mid \varphi \in S_\alpha \} \cup \{ \langle \forall, x, \varphi \rangle \mid x \in \mathrm{Var}, \varphi \in S_\alpha \}. \] As with strings, when writing tuples such as these, we omit the commas and angled brackets, so that, for instance, $\forall x \varphi = \langle \forall, x, \varphi \rangle$.
We then define \[ S_{\alpha + 1} = S_\alpha' \cup \{ \langle \textstyle{\bigwedge}, \Phi \rangle \mid \Phi \subseteq S_\alpha' \text{ is nonempty and countable} \}. \] Here, countable means finite or countably infinite. As above, we write $\bigwedge \Phi$ as shorthand for ordered pairs of this type.
In the case that $\alpha$ is a nonzero limit ordinal, we define $S_\alpha = \bigcup_{\xi < \alpha} S_\xi$. Finally, we define the set of formulas $\mathcal{L}_{\omega_1, \omega} = \bigcup_{\alpha < \omega_1} S_\alpha$, where $\omega_1$ is the first uncountable ordinal.
How, then, do we fill in the blank for Keisler's construction? What kind of object is a formula? It seems the most we can say is that it is a finite tuple. We might ask, a tuple of what? And here we have an answer that is recursive. With Karp, a formula is an infinite tuple of symbols from our alphabet. With Keisler, a formula is a finite tuple, where each element in the tuple is either a symbol from our alphabet, a formula, or a countable set of formulas.
Regarding the questions in the last paragraph of the OP, it seems the issues are all easily resolved as follows. We can use the above construction and transfinite induction to prove that $\mathcal{L}_{\omega_1, \omega}$ is the smallest set such that
This is precisely the characterization that Keisler gives, and it allows us to do anything we might want to do with formulas. It reminds me of the situation with ordered pairs. It doesn't matter how we formally define the ordered pair, only that it has the property, $(a, b) = (c, d)$ if and only if $a = c$ and $b = d$. The only practical thing we gain from a formal definition is a proof that there exists an object with this property. In the same way, the only practical thing we gain from the above construction of formulas is a proof that there exists a smallest set with properties (1)–(3). This, I believe, is the essence of Eric Wofsey's comment.
As for defining things like subformulas, I can now see that they can all be defined, even in first-order logic, without reference to strings, using only a characterization like (1)–(3). A similar thing is true for any results of Karp that we might wish to cite.