finite axiomatizability of first order theories?

Question

If we consider a single schema as a single axiom, so ZFC for example would be finitely axiomatizable after this kind of counting axioms.

By schema its meant a syntactical expression (string of symbols) that contains among its symbols free meta-theoretic variable symbols that range over a decidable set of formulas of the language of the theory in such a manner that each substitution of all those metatheoretic variables in the expression by instances (formulas) from what they range over would result in a sentence of the language of the theory. For example the separation schema of Zermelo written as: $$\forall A \exists x \forall y (y \in x \leftrightarrow y \in A \land \phi) \text { is an axiom }$$; Where $\phi$ is a metatheoretic variable that ranges over all formulas of the language in which $A$ doesn't occur free.

This is considered as a single axiom. While the separation schema written as: $$for \ n=1,2,3,...\\ \forall p_1,.., \forall p_n \forall A \exists x \forall y (y \in x \leftrightarrow y \in A \land \phi)$$, that is not a single schema, it is an infinite collection of schemas, so it is not considered as a single axiom.

Now is it the case that every effectively generated first order theory (with finitely many primitives) is finitely axiomatizable in this sense?

Answer 1

Let $n\mapsto\phi_n$ be a recursive enumeration of the provable formulas in the given theory, and define $\phi_n'$ to be $\phi_n\wedge\dots\wedge\phi_n$ where $\phi_n$ is repeated $n+1$ times. Given a formula you can check if it's equal to some $\phi_n'$ by seeing if it's equal to some formula repeated $n+1$ times, and then using the fact that $n\mapsto\phi_n$ is computable to calculate $\phi_n'$ and check if it's your formula. Thus the $\phi_n'$s form a decidable set of formulas, and hence a single axiom schema. This construction is also used in the proof of Craig's Theorem.