Finite axiomatizability of theories in infinitary logic? I know that the use of axiom schema in first-order theories can usually be eliminated by allowing higher-order quantification. So, a theory that isn’t finitely axiomatizable in a first-order language might be finitely axiomatizible in a higher-order. (Although I know that when this is done with the full semantics, the proof system loses many desirable properties.)
I’ve never seen discussion of finite axiomatizability in the context of infinitary logic, though. While I know that, similar to the higher-order case, infinitary languages allow for a finite number of axioms in place of first-order schema, I don’t know what effect (if any) the fact that these axioms will be infinitely long has on the applicability of “finite axiomatizability”. Is it just that the proof system will lose desirable properties, as in the higher-order case (with Barwise compact theories presumably enjoying somewhat “nicer” proof theoretic properties)? Does the concept of “finite axiomatizability” require the axioms be of finite length?
(I apologize for the lack of clarity, I’m grasping a bit here.)
 A: Well, the particular case you describe is trivial: every first-order theory (in a countable language anyways) can be expressed by a single $\mathcal{L}_{\omega_1,\omega}$-sentence - just take the conjunction of all the axioms in the theory. So things trivialize there.
However, the notion of axiomatizability by a single $\mathcal{L}_{\omega_1,\omega}$-sentence (it's linguistically convenient to replace "finitely many axioms" with "single axiom") is nonetheless interesting and important in other contexts. A major example of this is Scott's isomorphism theorem:

Suppose $\mathfrak{A}$ is a countable structure in a countable language. Then there is a single $\mathcal{L}_{\omega_1,\omega}$-sentence $\varphi$ - a so-called Scott sentence of $\mathfrak{A}$ - such that every countable model of $\varphi$ is isomorphic to $\mathfrak{A}$.


*

*Caveat: A Scott sentence may still  have uncountable models.


*Cute observation: Scott's theorem provides a simple example of the failure of Barwise compactness for uncountable admissible sets:

*

*Let $\mathsf{HC}$ be the set of hereditarily countable sets; note that $\mathsf{HC}$ is an uncountable admissibile set. We can whip up an $\mathsf{HC}$-c.e. set $X$ of $\mathcal{L}_{\omega_1,\omega}$-sentences which up to logical equivalence is the set of negations of Scott sentences for structures in the language of (say) a single binary relation symbol $R$. (Basically, look at the sentences whose syntactic structure describes some particular model with domain $\omega$ and the "Scott process" demonstrating that it is in fact a Scott sentence for that structure.)


*Now consider a new binary relation symbol $S$, let $\theta$ be the $\mathcal{L}_{\omega_1,\omega}$-sentence which says that the domain equipped with $S$ is isomorphic to $\mathbb{N}$ with the successor operation, and consider $Y=X\cup\{\theta\}$. Since there are uncountably many countable $\{R\}$-structures up to isomorphism, $Y$ is $\mathsf{HC}$-finitely satisfiable. However, any model of $Y$ would have to be a countable structure (due to $\theta$) whose $\{R\}$-reduct doesn't satisfy any of the Scott sentences for countable $\{R\}$-structures (due to the $X$-part). So $Y$ is unsatisfiable after all, despite being $\mathsf{HC}$-c.e. and $\mathsf{HC}$-finitely axiomatizable.


*"Scott-sentence-ness" was used in showing that every countable subset of $X$ is satisfiable: we used a cardinality argument, which hinged on each element of $X$ being violated in only a "few" models.
